GitLab

The following program produces a Core Lint error on GHC 8.6.3 and HEAD:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

data SameKind :: forall k. k -> k -> Type
data Foo :: forall a k (b :: k). SameKind a b -> Type where
  MkFoo :: Foo sameKind

$ /opt/ghc/8.6.3/bin/ghc Bug.hs -dcore-lint 
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
*** Core Lint errors : in result of CorePrep ***
<no location info>: warning:
    In the type ‘forall k (a :: k) k (b :: k) (sameKind :: SameKind
                                                             a b).
                 Foo sameKind’
    Kind application error in type ‘SameKind a_aWE b_aWG’
      Function kind = forall k. k -> k -> *
      Arg kinds = [(k_aWF, *), (a_aWE, k_aWD), (b_aWG, k_aWF)]
    Fun: k_aWF
         (a_aWE, k_aWD)
*** Offending Program ***

<elided>

MkFoo
  :: forall k (a :: k) k (b :: k) (sameKind :: SameKind a b).
     Foo sameKind

(Confusingly, the type of MkFoo is rendered as forall k (a :: k) k (b :: k) (sameKind :: SameKind a b). Foo sameKind in that -dcore-lint error, but I think it really should be forall k1 (a :: k1) k2 (b :: k2) (sameKind :: SameKind a b). Foo sameKind.)

On GHC 8.4.4 and earlier, this simply produces an error message:

$ /opt/ghc/8.4.4/bin/ghc Bug.hs -dcore-lint
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:9:13: error:
    • 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 kind ‘forall a k (b :: k). SameKind a b -> Type’
  |
9 | data Foo :: forall a k (b :: k). SameKind a b -> Type where
  |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Trac metadata

Trac field	Value
Version	8.6.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture