id summary reporter owner description type status priority milestone component version resolution keywords cc os architecture failure testcase blockedby blocking related differential wikipage
2235 Bogus occurs check with type families simonpj "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
" bug closed normal 6.10 branch Compiler 6.8.2 invalid Unknown/Multiple Unknown/Multiple