Opened 4 months ago

Last modified 4 months ago

#14042 new bug

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: 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 (15)

comment:1 Changed 4 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 4 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 4 months ago by RyanGlScott

Keywords: newcomer added

comment:4 Changed 4 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 4 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 4 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 4 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 4 months ago by goldfire (previous) (diff)

comment:8 in reply to:  7 Changed 4 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 4 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 4 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 4 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 4 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 4 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 4 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 4 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
Note: See TracTickets for help on using tickets.