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 ?
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... : )