[GHC] #14042: Datatypes cannot use a type family in their return kind (was: Misleading error message when type family is used in datatype's return kind)

[GHC]

#14042: Datatypes cannot use a type family in their return kind
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeFamilies
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:                    |
-------------------------------------+-------------------------------------
Changes (by goldfire):

 * keywords:  TypeInType, TypeFamilies, newcomer => TypeInType, TypeFamilies


Old description:

> 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 * = *`.

New description:

 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 * = *`. And, besides, the
 definition should be accepted.

 EDIT: This was originally about the error message. But comment:9 changes
 the goal of the bug to fix the behavior.

--

Comment:

 Ah! So I hadn't been aware of a use-case of this non-feature other than to
 annoy the type checker. I think, then, that this could be called a proper
 bug, not just a bad error message.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14042#comment:9>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler