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

[chak]

We agreed that this

tailList :: (b ~ Flip (Flip b)) => List a b -> List a (Flip b)

is not the right signature.

The new solver doesn't produce the infinite-type error message, but the usual one where it complains about not being able to instantiate a rigid type.

[simonpj]

Just to fill in the details here. The type of Cons is

Cons :: forall a b. forall c. (b ~ Flip c) => a -> List a c -> List a b

The task is this:

b ~ Flip (Flip b), b ~ Flip c  |-  List a (Flip b) ~ List a c

And indeed that isn't provable. If we'd written the type of Cons the other way about, thus:

Cons :: forall a b. a -> List a (Flip b) -> List a b

then we could prove it; but doubtless something else would go wrong. To do it right we'd have to give this type to Cons

Cons :: forall a b c. (b ~ Flip c, c ~ Flip b) => a -> List a c -> List a b

Which we could. But it seems uncomfortably fragile.

Simon