Error with polymorphic record fields and eqtypes

[theolaurent]

Here is the code snippet

noeq type test = {
  field : a:Type -> a -> a
  }

val foo : test -> unit
let foo t = t.field unit ()

I got Expected expression of type "Type"; got expression [...] of type "Prims.eqtype"

[aseemr]

Hi Theo:

The type test is polymorphic in one universe (the universe of the type argument to field. As a result, the declaration val foo is also polymorphic in that universe. However, the let binding is not -- it instantiates that universe explicitly with u#0, the universe of unit. And so, F* gives an error. This happens because F* generalizes the universe of val independently of the let (see #604).

A workaround is to just work with let bindings:

noeq type test = {
  field : a:Type -> a -> a
  }

let foo (t:test) = t.field unit ()

But if that's not possible (e.g. when you are writing val foo in an .fsti file), you can instantiate the universe for test explicitly, like:

noeq type test = {
  field : a:Type -> a -> a
  }

val foo : test u#0 -> unit
let foo t = t.field unit ()

I am closing this issue since #604 covers it already, please let us know if you face more issues. Thanks!

[aseemr]

Also, --print_universes flag when running F* on the example would have given a better error message.