Kind and type arguments out of dependency order [GHC-97739]

Language extension: PolyKinds

Normally, Haskell’s lexical scoping rules suffice to ensure that arguments to functions, whether they are type arguments or value arguments, are in scope in every position where they are used. In particular, because type and kind arguments form telescopes in which each argument’s name is in scope for the remaining arguments, lexical scope ensures that kind arguments occur before the types that they classify. However, in some cases, unannotated types can have kinds that are forced through unification to be equal to kinds that occur later in the argument list. This would lead to a scope error in the resulting fully-annotated program, so it is not allowed.

Examples

Kind and type variables out of dependency order

Message

DependencyOrder.hs:8:15: error: [GHC-97739]
    • These kind and type variables: a k (b :: k)
      are out of dependency order. Perhaps try this ordering:
        k (a :: k) (b :: k)
    • In the type signature: foo :: forall a k (b :: k). SameKind a b
  |
8 | foo :: forall a k (b :: k). SameKind a b
  |               ^^^^^^^^^^^^

Explanation

The type SameKind a b forces types a and b to have the same kind, because the kind variable k is used for both in its declaration. Thus, a’s kind is forced to be k, based on b’s kind annotation. However, this would result in a’s kind not being in scope when a is declared. The error can be fixed by reversing the arguments a and k so that a is in k’s scope.

DependencyOrder.hs

Before

{-# LANGUAGE DataKinds, PolyKinds, ExplicitForAll #-}
module DependencyOrder where

import Data.Kind

data SameKind :: k -> k -> *

foo :: forall a k (b :: k). SameKind a b
foo = undefined

After

{-# LANGUAGE DataKinds, PolyKinds, ExplicitForAll #-}
module DependencyOrder where

import Data.Kind

data SameKind :: k -> k -> *

foo :: forall k a (b :: k). SameKind a b
foo = undefined