[GHC] #14042: Misleading error message when type family is used in datatype's return kind

GHC ghc-devs at haskell.org
Sun Jul 30 22:27:58 UTC 2017


#14042: Misleading error message when type family is used in datatype's 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, newcomer
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:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 All I'll say is that I think it'd be worth singling out type families as a
 special case for error messages. FWIW, the example I actually tried (but
 boiled down to just `Id Type` for demonstration purposes) was something
 like this:

 {{{#!hs
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 import Data.Kind

 type family MkFun (args :: [Type]) (ret :: Type) :: Type where
   MkFun '[]        ret = ret
   MkFun (arg:args) ret = arg -> MkFun args ret

 data Foo (args :: [Type]) :: MkFun args Type
 }}}

 This is a perfectly natural thing to do in a dependently typed language
 like Idris:

 {{{#!idris
 MkFun : (args : List Type) -> Type -> Type
 MkFun []          ret = ret
 MkFun (arg::args) ret = arg -> MkFun args ret

 data Foo : (args : List Type) -> MkFun args Type
 }}}

 So I was quite surprised to find out that GHC can't do the same thing,
 even with `TypeInType`. It would be nice to mention in the error message
 that type families are the culprit in that particular scenario, since one
 would intuitively expect the language to recognize the fact that `MkFun
 args Type` does in fact expand to something which ends in `Type`.

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


More information about the ghc-tickets mailing list