• simonpj@microsoft.com's avatar
    Make unification robust to a boxy type variable meeting itself · 6493f9d3
    simonpj@microsoft.com authored
    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.
TcUnify.lhs 62.3 KB