+
+ -- The case for sigma-types must *follow* the variable cases
+ -- because a boxy variable can be filed with a polytype;
+ -- but must precede FunTy, because ((?x::Int) => ty) look
+ -- like a FunTy; there isn't necy a forall at the top
+ go _ ty1 ty2
+ | isSigmaTy ty1 || isSigmaTy ty2
+ = do { checkM (equalLength tvs1 tvs2)
+ (unifyMisMatch outer False orig_ty1 orig_ty2)
+
+ ; tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo
+ -- Get location from monad, not from tvs1
+ ; let tys = mkTyVarTys tvs
+ in_scope = mkInScopeSet (mkVarSet tvs)
+ subst1 = mkTvSubst in_scope (zipTyEnv tvs1 tys)
+ subst2 = mkTvSubst in_scope (zipTyEnv tvs2 tys)
+ (theta1,tau1) = tcSplitPhiTy (substTy subst1 body1)
+ (theta2,tau2) = tcSplitPhiTy (substTy subst2 body2)
+
+ ; checkM (equalLength theta1 theta2)
+ (unifyMisMatch outer False orig_ty1 orig_ty2)
+
+ ; uPreds False nb1 theta1 nb2 theta2
+ ; uTys nb1 tau1 nb2 tau2
+
+ -- If both sides are inside a box, we are in a "box-meets-box"
+ -- situation, and we should not have a polytype at all.
+ -- If we get here we have two boxes, already filled with
+ -- the same polytype... but it should be a monotype.
+ -- This check comes last, because the error message is
+ -- extremely unhelpful.
+ ; ifM (nb1 && nb2) (notMonoType ty1)
+ }
+ where
+ (tvs1, body1) = tcSplitForAllTys ty1
+ (tvs2, body2) = tcSplitForAllTys ty2
+