## 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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information