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,,,,,,,