[GHC] #14042: Data type with type family in return kind spuriously rejected

27 Jul 2017

      #14042: Data type with type family in return kind spuriously rejected
-------------------------------------+-------------------------------------
           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
  TypeFamilies                       |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This typechecks:

 {{{#!hs
 {-# LANGUAGE TypeInType #-}

 import Data.Kind

 type Id (a :: Type) = a

 data Foo :: Id Type
 }}}

 But changing the type synonym to a type family causes it to fail:

 {{{#!hs
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}

 import Data.Kind

 type family Id (a :: Type) :: Type where
   Id a = a

 data Foo :: Id Type
 }}}
 {{{
 $ ghci Foo.hs
 GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Main             ( Foo.hs, interpreted )

 Foo.hs:9:1: error:
     • Kind signature on data type declaration has non-* return kind
         Id *
     • In the data declaration for ‘Foo’
   |
 9 | data Foo :: Id Type
   | ^^^^^^^^
 }}}

 That error message is wrong, since `Id * = *`.

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