Make unification robust to a boxy type variable meeting itself

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.