Universe issue with polymorphic function arguments ?

[kyoDralliam]

I've stumbled on the following code which does not compiles

#set-options "--print_universes --print_implicits"

val test_wrong : (#a:Type -> a -> Tot unit) -> Tot unit
let test_wrong f = f ()
//                          ^^^^
// Implicit argument: Expected expression of type "Type(n107288)";

val test_wrong2 : (a:Type -> a -> Tot unit) -> Tot unit
let test_wrong2 f = f unit ()
//                              ^^^^
// Expected expression of type "Type(n107359)";

I am not exactly sure of what is going wrong. In particular I don't understand if
the function argument should be universe polymorphic or not and how I can
specify that in F* syntax...

Everything works fine if I restrict the argument function to Type0 type parameters

val test_valid : (a:Type0 -> a -> Tot unit) -> Tot unit
let test_valid f = f (squash True) ()

[nikswamy]

Hi Kenji,
Let's focus on test_wrong2. The first one is just a special case of the second.
In a forthcoming explicit notation, the type of test_wrong2 is

val test_wrong2: forall (u:universe). (a:Type u -> a -> Tot unit) -> Tot unit

As such, applying f to unit is not type-correct, since u <> 0.

I would suggest to write this example as:

let test_wrong2 (f:(a:Type -> a -> Tot unit)) : Tot unit = f unit ()

Or

let test_wrong (f:(#a:Type -> a -> Tot unit)) : Tot unit = f ()

In both cases, F* will infer the universe of f's first argument to be 0.

FYI, I recommend this style, notwithstanding #517, which I hope to fix today.

Note, this issue is a duplicate of #604. We can continue to discuss there. Closing this issue.