Opened 2 years ago

Last modified 12 months ago

#14420 new bug

Data families should not instantiate to non-Type kinds

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.3
Keywords: TypeFamilies Cc: Iceland_jack, ekmett, kcsongor, oerjan, glaebhoerl
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


data family Any :: k  -- allowable now due to fix for #12369

type family F (a :: Bool) :: Nat where
  F True  = 0
  F False = 1
  F Any   = 2
ghci> :kind! F True
F True :: Nat
= 0
ghci> :kind! F False
F False :: Nat
= 1
ghci> :kind! F Any
F Any :: Nat
= 2

Oh dear.

We should require that any instantiation of a data family be to a kind that ends in Type.

Inspired by comment:31:ticket:9429

Change History (12)

comment:1 Changed 2 years ago by Iceland_jack

Cc: Iceland_jack added

Hope this won't roll back what we got in #12369,

interestingly your Constrained Type Families paper doesn't mention constraining data families..

But if we require all data families be associated

class CAny k where
  data Any :: k

then using Any :: Bool as a case in the type family F will create a CAny Bool constraint, we are already barred from actually defining data instance Any :: Bool.

Last edited 2 years ago by Iceland_jack (previous) (diff)

comment:2 Changed 2 years ago by goldfire

Yes, that paper silently ignored data families, but I've thought all along (well, at least since I started thinking about constrained type families) that they should be associated, too. They're simpler because there are no closed data families.

Chalk this up as yet another problem the constrained type families approach would solve...

comment:3 Changed 2 years ago by simonpj

Keywords: TypeInType added

comment:4 Changed 2 years ago by goldfire

Keywords: TypeInType removed

This is not related to TypeInType. I suppose I won't argue if you want to make a new keyword RichardsBailiwick, but this truly isn't TypeInType.

comment:5 Changed 2 years ago by simonpj

Keywords: TypeFamilies added

OK. What keyword should we give it? Otherwise, with 14,000+ tickets, it just gets lost in the sea. Let's try TypeFamilies, summarised here

comment:6 Changed 2 years ago by ekmett

Cc: ekmett added

comment:7 Changed 2 years ago by kcsongor

Cc: kcsongor added

comment:8 Changed 2 years ago by simonpj

According to Adam, this bug somehow imperils #7259.

comment:9 Changed 21 months ago by oerjan

Cc: oerjan added

comment:10 Changed 15 months ago by simonpj

I've got lost about what the actual problem is here. The Description says "Oh dear" but fails to elaborate.

comment:11 Changed 15 months ago by monoidal

The definition data Bool = False | True defines a closed type: the only values of type Bool are False and True, pattern matching on both of them defines a total function. A function Bool -> A is equivalent to a tuple (A,A). It's natural to expect the same behavior on the kind level: the promoted kind Bool should have only two inhabitants, type False and True. Currently, this doesn't hold.

comment:12 Changed 12 months ago by glaebhoerl

Cc: glaebhoerl added
Note: See TracTickets for help on using tickets.