Opened 23 months ago

Last modified 8 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:

Description

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 23 months 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 23 months ago by Iceland_jack (previous) (diff)

comment:2 Changed 23 months 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 23 months ago by simonpj

Keywords: TypeInType added

comment:4 Changed 23 months 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 23 months 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 20 months ago by ekmett

Cc: ekmett added

comment:7 Changed 19 months ago by kcsongor

Cc: kcsongor added

comment:8 Changed 19 months ago by simonpj

According to Adam, this bug somehow imperils #7259.

comment:9 Changed 17 months ago by oerjan

Cc: oerjan added

comment:10 Changed 10 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 10 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 8 months ago by glaebhoerl

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