Applicative functor in F*: Type checking error

Question

As an experiment while trying to get familiar with F*, I tried implementing an applicative functor. I'm stuck at a weird-looking type checking error. I'm not sure yet if this is due to some feature / logic in the type checking that I'm not aware of, or if this is caused by a genuine bug.

Here is the part of the code that is causing me trouble :

module Test

noeq type test : Type -> Type =
    | Apply : test ('a -> 'b) -> test 'a -> test 'b

val apply : test ('a -> 'b) -> test 'a -> test 'b
let apply f x = Apply f x

And here is the corresponding error :

Test(7,24-7,25): (Error 54) Test.test 'a is not a subtype of the expected type Test.test 'a (see also Test(7,12-7,13))
1 error was reported (see above)

Could someone kindly point out to me what I'm missing ? Is the behaviour of type unification affected by subtyping ? Or should this type-check and this is a compiler bug ?

Answer 1

I believe there is a universe inequality constraint on inductives that you are not enforcing.

The following code will typecheck:

noeq type test : Type0 -> Type =
    | Apply : test ('a -> 'b) -> test 'a -> test 'b

val apply : test ('a -> 'b) -> test 'a -> test 'b
let apply f x = Apply f x

Notice the 0 I added on the first line.

This works because this states that the first Type0 is in a lower universe than than Type (which itself, I believe, means any universe). In your case, F* doesn't know how to compare the universes for these two types, hence fails.

If you had written noeq type test : Type -> Type0 you would have seen a slightly better error message: "Failed to solve universe inequalities for inductives". So I blame the error message here.

I apologize if the explanation lacks precision, I am not a PL person... : )