## #2235 closed bug (invalid)

# Bogus occurs check with type families

Reported by: | simonpj | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | 6.10 branch |

Component: | Compiler | Version: | 6.8.2 |

Keywords: | Cc: | ||

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | None/Unknown | Test Case: | |

Blocked By: | Blocking: | ||

Related Tickets: | Differential Rev(s): | ||

Wiki Page: |

### Description

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

### Change History (5)

### comment:1 Changed 11 years ago by

Milestone: | → 6.10 branch |
---|

### comment:2 Changed 11 years ago by

Architecture: | Unknown → Unknown/Multiple |
---|

### comment:3 Changed 11 years ago by

Operating System: | Unknown → Unknown/Multiple |
---|

### comment:4 Changed 11 years ago by

Resolution: | → invalid |
---|---|

Status: | new → closed |

### comment:5 Changed 11 years ago by

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

**Note:**See TracTickets for help on using tickets.

We agreed that this

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.