Opened 16 months ago

Closed 10 months ago

Last modified 10 months ago

#14042 closed bug (duplicate)

Datatypes cannot use a type family in their return kind

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.0.1
Keywords: TypeInType, TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: #14645 Differential Rev(s):
Wiki Page:

Description (last modified by goldfire)

This typechecks:

{-# 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:

{-# 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.

Change History (18)

comment:1 Changed 16 months ago by simonpj

There are other places where we don't accept a type-function application; e.g.

type instance F Int = Bool

instance C (F Int) where ...

And rightly so.

This one is, I grant you, less justifiable. But I think it'd be fiddly to support, and the motivation seems weak. After all, data families always have result kind * so why not say so?

comment:2 Changed 16 months ago 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.

comment:3 Changed 16 months ago by RyanGlScott

Keywords: newcomer added

comment:4 Changed 16 months ago by RyanGlScott

Summary: Data type with type family in return kind spuriously rejectedMisleading error message when type family is used in datatype's return kind

comment:5 Changed 16 months ago by goldfire

What would you like the error message to say? It looks correct to me. Perhaps it could have an "NB: no type functions" or something, but it's not too far off.

comment:6 Changed 16 months ago 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.

comment:7 Changed 16 months ago by goldfire

Well, the problem is that the result is not *. It's Something Else. It doesn't really have to do with type families, just the rigidity around *. What's perhaps frustrating here is that type equality in Haskell usually accounts for type family reduction and in-scope equalities, but this is not true in a datatype return kind. (Perhaps it should be, but I think there are complications there we don't want to get involved with.)

Last edited 16 months ago by goldfire (previous) (diff)

comment:8 in reply to:  7 Changed 16 months ago 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:

{-# 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:

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.

comment:9 Changed 16 months ago by goldfire

Description: modified (diff)
Keywords: newcomer removed
Summary: Misleading error message when type family is used in datatype's return kindDatatypes cannot use a type family in their return kind

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.

comment:10 Changed 16 months ago 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?

comment:11 Changed 16 months ago by goldfire

I thought of the same problem (comment:10) afterward, too. But regardless, we could require that the ending kind is Type at all usage sites, instead of at the definition site. Indeed, I wonder if we can just omit the check entirely, as long as we check the types of data constructors. Those types end in -> T blah blah blah, so if T blah blah blah's kind is other than Type, the data constructor type will fail to kind-check.

comment:12 Changed 16 months ago by simonpj

I wonder if we can just omit the check entirely, as long as we check 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.

comment:13 Changed 16 months ago by goldfire

This ticket is actually about regular old datatypes, not data families. Let's solve the datatype problem first, I think. The only part I haven't quite figured out is if we need the coercion relating the declared return kind to Type somewhere, but I don't see where it would go, other than the types of constructors. What would the constructor workers look like? I'm not sure.

comment:14 Changed 16 months ago 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.

comment:15 Changed 16 months ago by RyanGlScott

Can someone produce an example with some actual data constructors? I'm a bit lost as to the actual goal.

This is the sort of thing that I want to write:

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

data Nat = Z | S Nat

type family MkFun (args :: Nat) :: Type where
  MkFun Z     = Type
  MkFun (S n) = Type -> MkFun n

data Foo (args :: Nat) :: MkFun args where
  MkFoo0 :: Foo Z
  MkFoo1 :: a -> Foo (S Z) a
  MkFoo2 :: a -> b -> Foo (S (S Z)) a b

comment:16 Changed 10 months ago 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:

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?

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.

comment:17 Changed 10 months ago by RyanGlScott

Resolution: duplicate
Status: newclosed

I would be quite happy to have this for only data families, so I'll close this in favor of #14645.

comment:18 Changed 10 months ago by goldfire

Oh wow. That was easy. I was expecting a mind-bending battle here. :)

Note: See TracTickets for help on using tickets.