[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