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 |