Singleton list for Unique typechecks

[Pat-Lafon]

I'm getting back into the swing of things and identifying blockers for Cobb(Coverage Type synthesis). The following is a program that Poirot typechecks incorrectly using

dune exec -- bin/main.exe type-check meta-config.json data/issue/singleton_unique.ml

let rec unique_list_gen (s : int) : int list =
  if sizecheck s then []
  else
    let (l : int list) = unique_list_gen (subs s) in
    let (x : int) = int_gen () in
    if list_mem l x then Err else x :: Nil

let[@assert] unique_list_gen =
  let s = (v >= 0 : [%v: int]) [@over] in
  (len v s && uniq v : [%v: int list]) [@under]

Note that the branch with the mem check does seem relevant, though l can be assigned to Nil without issue.

Ideally this is just a simple issue around the axioms for len/uniq predicates or messing with the measure