
#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