Make unification robust to a boxy type variable meeting itself
Previously, the implicit assumption in unification is that a boxy type variable could never occur on both sides of the unification, so that we'd never find bx5 :=: bx5 But the pre-subsumption stuff really means that the same variable can occur on both sides. Consider forall a. a->Int <= bx5->Int Then pre-subumption will find a->bx5; and the full subsumption step will find bx5:=bx5. However, I think there is still no possiblity of a full occurs-check failure; that is, bx5 :=: Tree bx5 Although I can't quite see how to prove it! So I've added a DEBUG test in uMetaVar to check for this case.
Showing with 29 additions and 9 deletions