Re: [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)

30 Jul 2017

      #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