Can't create poly-kinded GADT with TypeInType enabled, but can without
Surprisingly, this compiles without TypeInType:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
module Works where
import Data.Kind
data T :: k -> Type where
MkT :: T Int
But once you add TypeInType:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data T :: k -> Type where
MkT :: T Int
then it stops working!
GHCi, version 8.3.20170516: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:11:12: error:
• Expected kind ‘k’, but ‘Int’ has kind ‘*’
• In the first argument of ‘T’, namely ‘Int’
In the type ‘T Int’
In the definition of data constructor ‘MkT’
|
11 | MkT :: T Int
| ^^^
This bug is present in GHC 8.0.1, 8.0.2, 8.2.1, and HEAD.
What's strange about this bug is that is requires that you write T with an explicit kind signature. If you write T like this:
data T (a :: k) where
MkT :: T Int
Then it will work with TypeInType enabled.
Trac metadata
| Trac field | Value |
|---|---|
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |