GHC 8.6 Core Lint regression (Kind application error)
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 |