Type contructor alias + refinement causes type checking to fail in constructor

[mushrm88]

I have a constructor with a refinement type. I made an alias for a type constructor to make a complicated dependent type more readable but the alias seems to break type checking when used in combination with the refinement. I put together a simplified example that reproduces the issue:

module DepTest

open FStar.List.Tot.Base

type main : nat -> Type =
  | Main : (a : nat) -> main a

type mylist (a : Type) (b : a -> Type) = list (dtuple2 a b)

let indices (ls : mylist 'a 'b) =
  map dfst ls

type container =
  | Container : numbers : list nat -> ls : mylist nat elem { indices ls = numbers } -> container
and elem (index : nat) = main index

// This works. I am explicitly writing a function instead of using the elem type alias.
let make_container2 (numbers : list nat) (ls : mylist nat (fun i -> main i) { indices ls = numbers }) = Container numbers ls

// This does not work.
let make_container (numbers : list nat) (ls : mylist nat elem { indices ls = numbers }) = Container numbers ls

If I remove the refinement I can use the type alias, and if I don't use the type alias I can use the refinement, but the two features in combination seem to prevent me from constructing a container.

Is this a bug? If not, how can I get make_container to type check? The actual types are significantly more complicated so I'd prefer to be able to use aliases like elem. Note that moving the alias outside of the definition of container does not help.

I am using F* 2022.11.19~dev OCaml 4.14.1 date=2023-02-02 21:18:53 -0300 commit=d6010c1505d8440796c2928251daa43cc9fdca89

[mushrm88]

I can use tcnorm to fix this particular example, but that causes a bunch of problems elsewhere:

[@@tcnorm] type elem (index : nat) = main index

I can also assign the input to an unused variable and this enables the typechecker to figure things out:

let make_container (numbers : list nat) (ls : mylist nat elem { indices ls = numbers }) =
  let (ls' : mylist nat (fun i -> main i) { indices ls = numbers }) = ls in
  Container numbers ls

This does not seem to work consistently but works in this simplified example case. I would also prefer to not have to add the ascription everywhere as it is very long and not easy to read in my actual code.

[aseemr]

Thanks @mushrm88 for the reporting this, this is indeed counterintuitive. I also expected make_container to work smoothly.

Here is a smaller version that exhibits the same problem:

module Test

assume val main (n:int) : Type0
assume val my_t (a:int -> Type0) : Type0
assume val pred (#a:int -> Type0) (ls:my_t a) : Type0

noeq
type container =
  | Container : ls:my_t elem{pred ls} -> container
and elem (index:int) = main index

let make_container (ls:my_t elem{pred ls}) : container = Container ls

The issue here is that, F* inlines the elem type abbreviation in the Container type very early in the pipeline, essentially rewriting the Container to Container: ls:my_t (fun index -> main index){pred ls} -> container. So the version with inlined lambda works smoothly while the version with abbreviation does not, and the reason for latter is some imprecision in the smt encoding of functions.

The workaround here is to hoist the refinement out of the data constructor definition. In the small example above, this would mean:

module Test

assume val main (n:int) : Type0
assume val my_t (a:int -> Type0) : Type0
assume val pred (#a:int -> Type0) (ls:my_t a) : Type0

type refined_my_t (a:int -> Type0) = ls:my_t a{pred ls}

noeq
type container =
  | Container : ls:refined_my_t elem -> container
and elem (index:int) = main index

let make_container (ls:refined_my_t elem) : container = Container ls

Notice the refined_my_t hoisted out.

And in your code snippet:

module Test

open FStar.List.Tot

type main : nat -> Type =
  | Main : (a : nat) -> main a

type mylist (a : Type) (b : a -> Type) = list (dtuple2 a b)

let indices (ls : mylist 'a 'b) =
  map dfst ls

type refined_mylist (#a:Type) (#b:a -> Type) (pred:mylist a b -> Type0) =
  ls:mylist a b {pred ls}

let container_pred (b:nat -> Type) (numbers:list nat) : mylist nat b -> Type0 =
  fun ls -> indices ls = numbers

type container =
  | Container : numbers : list nat -> ls : refined_mylist (container_pred elem numbers) -> container
and elem (index : nat) = main index

let make_container (numbers : list nat) (ls : refined_mylist (container_pred elem numbers)) = Container numbers ls

This can be tweaked as per your requirement, e.g. may be you want to fold in container_pred in refined_mylist itself etc.

Hope this helps, we will also think about what we can do to fix this "discrepancy" in the typechecker.

[mushrm88]

@aseemr This was a big help and I was able to remove many ascriptions and all assumes from my code. Thanks! I don't really understand why hoisting the refinement makes the type checking work better though.

I still observe several odd things. Proof by normalisation sometimes doesn't work the way I'd expect. I have a contrived example:

let test_predicate (c : container) = match c with
  | Container numbers ls -> numbers = [1; 2; 3] || length ls > 1

// Does not work.
let test_lemma (numbers : list nat) (ls : refined_mylist (container_pred elem numbers)) : 
Lemma (length ls > 1 ==> test_predicate (Container numbers ls)) =
  assert_norm (test_predicate (Container numbers ls) = ((numbers = [1; 2; 3]) || (length ls > 1)))

// This also doesn't work in this example, but for some reason changing || to op_BarBar makes the proof by normalisation work in my actual code.
let test_lemma' (numbers : list nat) (ls : refined_mylist (container_pred elem numbers)) : 
Lemma (length ls > 1 ==> test_predicate (Container numbers ls)) =
  assert_norm (test_predicate (Container numbers ls) = (op_BarBar (numbers = [1; 2; 3]) (length ls > 1)))

As mentioned in the comment, in one case, changing || to op_BarBar and changing nothing else caused assert_norm to work, which was surprising to me. I couldn't reproduce it in this example.

In the original example it also looks like I can do an ascription that contains the refinement but omits the rest of the type and that typechecks:

// This type checks
let make_container (numbers : list nat) (ls : mylist nat elem { indices ls = numbers }) =
  let (ls' : _ { indices ls = numbers }) = ls in
  Container numbers ls'

This was surprising to me.

Thanks again! I was able to clean things up significantly.