GitLab

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