Fix an infinite loop in niFixTCvSubst

Authored by simonpj on Jun 16 2018, 5:25 PM.


Fix an infinite loop in niFixTCvSubst

Trac Trac #14164 made GHC loop, a pretty serious error. It turned
out that Unify.niFixTCvSubst was looping forever, because we
had a substitution like

a :-> ....(b :: (c :: d))....
d :-> ...

We correctly recognised that d was free in the range of the
substitution, but then failed to apply it "deeeply enough"
to the range of the substiuttion, so d was /still/ free in
the range, and we kept on going.

Trac Trac #9106 was caused by a similar problem, but alas my
fix to Trac Trac #9106 was inadequate when the offending type
variable is more deeply buried. Urk.

This time I think I've fixed it! It's much more subtle
than I though, and it took most of a long train journey
to figure it out. I wrote a long note to explain:
Note [Finding the substitution fixpoint]

This seems reasonable. But it makes me worried. How do we know when performing a subst over an open type that we're not forgetting to subst in kinds?

The in-scope set of a subst is always closed over kinds. But we need the (in-scope set) - (the subst domain), using set subtraction, to also be closed over kinds. Otherwise, we're substing a kind variable without substing the type variable, leading to problems like the ones here. So I propose adding this to the substitution invariants and checking it appropriately.


Shouldn't this have G b (z :: b) on the right?