When *pre-matching* two types
forall a. C1 => t1 ~ forall a. C2 => t2
we were matching t1~t2, but totally ignoring C1,C2
That's utterly wrong when pre-matching
(?p::Int) => String ~ a
because we emerge with a:=String!
All this is part of the impredicative story, which is about
to go away, but still.
Worth merging this to 6.12
go ty1 ty2 -- C.f. the isSigmaTy case for boxySubMatchType
| isSigmaTy ty1
go ty1 ty2 -- C.f. the isSigmaTy case for boxySubMatchType
| isSigmaTy ty1
- , (tvs1, _, tau1) <- tcSplitSigmaTy ty1
- , (tvs2, _, tau2) <- tcSplitSigmaTy ty2
+ , (tvs1, ps1, tau1) <- tcSplitSigmaTy ty1
+ , (tvs2, ps2, tau2) <- tcSplitSigmaTy ty2
= boxy_match (tmpl_tvs `delVarSetList` tvs1) tau1
(boxy_tvs `extendVarSetList` tvs2) tau2 subst
= boxy_match (tmpl_tvs `delVarSetList` tvs1) tau1
(boxy_tvs `extendVarSetList` tvs2) tau2 subst