#14042: Data type with type family in return kind spuriously rejected -------------------------------------+------------------------------------- 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: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Fair enough, I can accept GHC rejecting occurrences of type families in data type return kinds. But at the very least the error message ought to be changed here, because the current one misleads readers from the real problem. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14042#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14042#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): Just like type families are rejected in class instances: {{{

:set -XTypeFamilies type family Foo a instance Show (Foo a)

<interactive>:4:10: error: * Illegal type synonym family application in instance: Foo a * In the instance declaration for `Show (Foo a)' }}} I want the error message for type families in data type return kinds to be similarly informative. Something like: {{{

data Foo :: Id Type * Illegal type synonym family application in return kind of data type declaration Id Type }}}

None of this faffery about non-`*` return kinds, since that's not the real issue here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14042#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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: | -------------------------------------+------------------------------------- Comment (by simonpj):

one would intuitively expect the language to recognize the fact that MkFun args Type does in fact expand to something which ends in Type

Would one? That requires somewhat sophisticated reasoning about `MkFun` doesn't it? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14042#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

I wonder if we can just omit the check entirely, as long as we check

#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: | -------------------------------------+------------------------------------- Comment (by simonpj): the types of data constructors Ah yes, that sounds more plausible. And now the whole thing makes more sense. Even today with {{{ data family T a :: * data instance T Int = T1 Bool }}} we desugar to a new type constructor `TInt :: *`, declared thus {{{ data TInt = T1 Bool axiom ax1 :: TInt ~R T Int }}} and occurrences of the original user data constructor `T1` is converted to occurrences of the wrapper {{{ $WT1 :: Bool -> T Int $WT1 x = T1 x |> ax1 }}} Now I suppose that if we instead had {{{ data family T a :: F a -- For some type family F }}} (which is what Ryan suggests), and we can prove `co :: F Int ~ *`, then perhaps we'd get {{{ axiom ax1 :: (TInt :: *) ~R ((T Int |> co) :: *) }}} or something like that? In other words, we relax the checks on the data ''family'' but add checks on the data ''constructors'', including putting the extra proof (e.g. `co :: F Int ~ *` in somewhere. I'm not sure of the details, but there is enough desugaring around data families and their data instances that it looks entirely possible. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14042#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Comment (by simonpj): I'm not sure either. But we do have worker/wrapper for ordinary data cons, so there is room to inject some coercions. Eg {{{ data T = MkT {-# UNPACK #-} !Int }}} We get a worker and a wrapper. {{{ MkT :: Int# -> T -- Worker -- No code; this is the real data constructor in Core $WMkT :: Int -> T -- Wrapper $WMkT x = case x of I# y -> MkT y }}} Occurrences of `MkT` in terms are replaced by `$WMkT`. In patterns we need some impedence matching. Can someone produce an example with some actual data constructors? I'm a bit lost as to the actual goal. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14042#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | -------------------------------------+------------------------------------- Comment (by goldfire): I'm wondering why you want a datatype instead of a data family. A data family makes grand sense here. But I'm still stuck on how a datatype could work this way. For example: {{{#!hs bar :: Foo n -> ... bar f = case f of MkFoo0 -> ... MkFoo1 x -> ... MkFoo2 x y -> ... }}} What are the types of `x` and `y`? I suppose they're existential... but they certainly don't look it from the declaration. And, if we discover that `f` is `MkFoo1`, say, then we learn that type of `bar` is ill-kinded. Indeed, perhaps the fact that `Foo n :: Type` tells us that `n ~ Z` without any pattern matches. (NB: `MkFun` really ''is'' injective, even if GHC can't know it.) Given this fact, I don't know how you could construct a function where there is more than one possible constructor for `Foo`. Also, I like to think about GADTs in terms of their desugaring to uniform datatypes with equality constraints. How would `Foo` desugar? {{{#!hs Foo :: forall (args :: Nat). MkFun args MkFoo0 :: forall (args :: Nat). args ~ Z => Foo args MkFoo1 :: forall (args :: Nat). forall (a :: Type). -- existential?? args ~ S Z => a -> Foo args }}} I've left off the last constructor, as it doesn't illustrate much more. The problem is that, in this formulation, the final result type must always be `Foo args`. That's what uniform means. But, here, `Foo args` is ill-kinded there. So I really have no idea what this construct means. My bottom line (supported more by my first line of argument than my second): you really want a data family, and we should close this ticket in favor of #14645. The only advantage of a datatype over a data family is that one pattern match of a datatype can cover a multitude of cases -- but you don't actually achieve that here. Furthermore, despite my comment:13, I have a much better picture of how to implement this idea for data families than I do for datatypes. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14042#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14042: Datatypes cannot use a type family in their return kind -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: TypeInType, Resolution: duplicate | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #14645 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Oh wow. That was easy. I was expecting a mind-bending battle here. :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14042#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler