The big change here is to fix an outright bug in flattening of Givens,
albeit one that is very hard to exhibit. Suppose we have the constraint
forall a. (a ~ F b) => ..., (forall c. ....(F b)...) ...
Then
- we'll flatten the (F) b to a fsk, say (F b ~ fsk1)
- we'll rewrite the (F b) inside the inner implication to 'fsk1'
- when we leave the outer constraint we are suppose to unflatten;
but that fsk1 will still be there
- if we re-simplify the entire outer implication, we'll re-flatten
the Given (F b) to, say, (F b ~ fsk2)
Now we have two fsks standing for the same thing, and that is very
wrong.
Solution: make fsks behave more like fmvs:
- A flatten-skolem is now a MetaTyVar, whose MetaInfo is FlatSkolTv
- We "fill in" that meta-tyvar when leaving the implication
- The old FlatSkol form of TcTyVarDetails is gone completely
- We track the flatten-skolems for the current implication in
a new field of InertSet, inert_fsks.
See Note [The flattening story] in TcFlatten.
In doing this I found various other things to fix:
* I removed the zonkSimples from TcFlatten.unflattenWanteds; it wasn't
needed. But I added one in TcSimplify.floatEqualities, which does
the zonk precisely when it is needed.
* Trac #13674 showed up a case where we had
- an insoluble Given, e.g. a ~ [a]
- the same insoluble Wanted a ~ [a]
We don't use the Given to rewwrite the Wanted (obviously), but
we therefore ended up reporting
Can't deduce (a ~ [a]) from (a ~ [a])
which is silly.
Conclusion: when reporting errors, make the occurs check "win"
See Note [Occurs check wins] in TcErrors