Opened 2 years ago
Last modified 10 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 2 years ago by
Cc: | Iceland_jack added |
---|
comment:2 Changed 2 years ago by
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
Keywords: | TypeInType added |
---|
comment:4 Changed 2 years ago by
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
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 21 months ago by
Cc: | ekmett added |
---|
comment:7 Changed 21 months ago by
Cc: | kcsongor added |
---|
comment:9 Changed 18 months ago by
Cc: | oerjan added |
---|
comment:10 Changed 12 months ago by
I've got lost about what the actual problem is here. The Description says "Oh dear" but fails to elaborate.
comment:11 Changed 12 months ago by
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 10 months ago by
Cc: | glaebhoerl 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
then using
Any :: Bool
as a case in the type familyF
will create aCAny Bool
constraint, we are already barred from actually definingdata instance Any :: Bool
.