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