Data families should not instantiate to non-Type kinds
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 = 2ghci> :kind! F True
F True :: Nat
= 0
ghci> :kind! F False
F False :: Nat
= 1
ghci> :kind! F Any
F Any :: Nat
= 2Oh dear.
We should require that any instantiation of a data family be to a kind that ends in Type.
Inspired by ticket:9429#comment:144757
Trac metadata
| Trac field | Value |
|---|---|
| Version | 8.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information