Location of `forall` matters with higher-rank kind polymorphism
The following code fails to compile, but probably should:
{-# LANGUAGE RankNTypes, TypeInType #-}
import Data.Kind
data Foo :: forall k . (* -> *) -> k -> * -- Decl 1
class C (a :: forall k . k -> *)
instance C (Foo a) -- error on this line
with the error
• Expected kind ‘forall k. k -> *’, but ‘Foo a’ has kind ‘k0 -> *’
• In the first argument of ‘C’, namely ‘Foo a’
In the instance declaration for ‘C (Foo a)’
Similarly, the following declarations of Foo
also cause a similar error at the instance declaration:
Decl 2: data Foo :: (* -> *) -> k -> *
Decl 3: data Foo (a :: * -> *) (b :: k)
However, if I move the forall
to a point after the first type parameter (which is where the instance is partially applied) thusly:
Decl 4: data Foo :: (* -> *) -> forall k . k -> *
then GHC happily accepts the instance of C
.
From my (admittedly negligible) knowledge of type theory, the signatures for Decls 1 and 4 (and 2) are identical, since the forall
can be floated to the front of Decl 4. GHC should accept any of the four versions of Foo
, since they are all equivalent.