## Confusing error message

For test `indexed-types/should_fail/T4272`

we get this type error

```
T4272.hs:11:16:
Occurs check: cannot construct the infinite type:
x0 = TermFamily x0 x0
Expected type: TermFamily x0 x0
Actual type: TermFamily a a
In the first argument of `prune', namely `t'
In the expression: prune t (terms (undefined :: TermFamily a a))
In an equation for `laws':
laws t = prune t (terms (undefined :: TermFamily a a))
```

It's not at all obvious why unifying `(TermFamily x0 x0)`

with `(TermFamily a a)`

should yield an occurs check. Especially as `TermFamily`

is a type function with arity 1, and `x0`

is a unification variable. So the natural way to solve this constraint would be to unify `x0`

with `a`

, and then the constraint is satisfied.

What goes wrong is that there is *another* insolube constraint (which is also reported):

```
T4272.hs:11:19:
Could not deduce (a ~ TermFamily x0 x0)
from the context (TermLike a)
bound by the type signature for
laws :: TermLike a => TermFamily a a -> b
at T4272.hs:11:1-54
`a' is a rigid type variable bound by
the type signature for laws :: TermLike a => TermFamily a a -> b
at T4272.hs:11:1
In the return type of a call of `terms'
In the second argument of `prune', namely
`(terms (undefined :: TermFamily a a))'
In the expression: prune t (terms (undefined :: TermFamily a a))
```

The constraint solver finds this latter constraint, can't solve it, *but still uses it to simplify the first one*, by substituting `(TermFamily x0 x0)`

for `a`

; and that is what gives the occurs check error.

I don't think that we should use *insoluble* constraints to rewrite unsolved constraints. But it's delicate, so I am not trying to fiddle right now. Hence making this ticket.

(Incidentally, it's not a regression; it's been like this forever.)

## Trac metadata

Trac field | Value |
---|---|

Version | 7.2.2 |

Type | Bug |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler |

Test case | indexed-types/should_fail/T4272 |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | dimitris@microsoft.com |

Operating system | |

Architecture |