Bogus occurs check with type families
Consider this program, using type families:
data Even; data Odd
type family Flip a :: *
type instance Flip Even = Odd
type instance Flip Odd = Even
data List a b where
Nil :: List a Even
Cons :: a -> List a b -> List a (Flip b)
tailList :: List a b -> List a (Flip b)
tailList (Cons _ xs) = xs
I get the error (from the HEAD)
Occurs check: cannot construct the infinite type: b = Flip (Flip b)
In the pattern: Cons _ xs
In the definition of `tailList': tailList (Cons _ xs) = xs
There's a bug here -- reporting an occurs check is premature. We should really be able to infer the type
tailList :: (b ~ Flip (Flip b)) => List a b -> List a (Flip b)
But we get the same bogus occurs-check error with this signature.
This example also illustrates why we might want closed families. If you look at the type constraints arising from tailList you'll see that you get
(c ~ Flip b, b ~ Flip c)
where c is the existential you get from the GADT match. Now, we know that b = Flip (Flip b)
is always true, but GHC doesn't. After all, you could add new type instances
type instance Flip Int = Bool
type instance Flip Bool = Char
and then the equation wouldn't hold. What we really want is a *closed* type family, like this
type family Flip a where
Flip Even = Odd
Flip Odd = Even
(preferably supported by kinds) and even *then* it's not clear whether it's reasonable to expect the compiler to solve the above problem by trying all possiblities. This relates to #2101
Trac metadata
Trac field | Value |
---|---|
Version | 6.8.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | Unknown |
Architecture | Unknown |