Make the canonicaliser do unification
Look at canEqTyVarFunEqCan
- This function calls
unifyTest
, andcheckTyVarEq
, both of which are fairly elaborate tests. - Then we go to
canEqCanLHSFinish
, which callscanEqOK
which callscheckTypeEq
, repeating thatcheckTyVarEq
- All this just gets the orientation right. Then we forget all that, and later, in
tryToSolveByUnification
we callunifyTest
again. What a mess.
One thing that discouraged me was the miasma of rewriteEqEvidence
and rewriteCastedEquality
and do-swap stuff. I just can't get my head round it. In some of my traces (eg EqCanOccursCheck) we seem to swap and swap back. Bizarre.
@rae and I agree that the canonicaliser should just do unification on the spot. This ticket is to track that point.