[GHC] #13761: Can't create poly-kinded GADT with TypeInType enabled, but can without

27 May 2017

      #13761: Can't create poly-kinded GADT with TypeInType enabled, but can without
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Surprisingly, this compiles without `TypeInType`:

 {{{#!hs
 {-# 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`:

 {{{#!hs
 {-# 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:

 {{{#!hs
 data T (a :: k) where
   MkT :: T Int
 }}}

 Then it will work with `TypeInType` enabled.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13761
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler