Skip to content

GitLab

GHC
GHC
Closed
Opened by Eric Crockett@crockeeaReporter

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.

Edited by Ben Gamari