- go outer ty1 ty2
- | Just ty1' <- tcView ty1 = go False ty1' ty2
- | Just ty2' <- tcView ty2 = go False ty1 ty2'
-
- -- Variables; go for uVar
- go outer (TyVarTy tyvar1) ty2 = uVar outer False tyvar1 nb2 orig_ty2 ty2
- go outer ty1 (TyVarTy tyvar2) = uVar outer True tyvar2 nb1 orig_ty1 ty1
- -- "True" means args swapped
- -- Predicates
- go outer (PredTy p1) (PredTy p2) = uPred outer nb1 p1 nb2 p2
-
- -- Type constructors must match
- go _ (TyConApp con1 tys1) (TyConApp con2 tys2)
- | con1 == con2 = uTys_s nb1 tys1 nb2 tys2
- -- See Note [TyCon app]
-
- -- Functions; just check the two parts
- go _ (FunTy fun1 arg1) (FunTy fun2 arg2)
- = do { uTys nb1 fun1 nb2 fun2
- ; uTys nb1 arg1 nb2 arg2 }
-
- -- Applications need a bit of care!
- -- They can match FunTy and TyConApp, so use splitAppTy_maybe
- -- NB: we've already dealt with type variables and Notes,
- -- so if one type is an App the other one jolly well better be too
- go outer (AppTy s1 t1) ty2
+ go _ sty1 ty1 sty2 ty2
+ | Just ty1' <- tcView ty1 = go (Unify False ty1' ty2 ) sty1 ty1' sty2 ty2
+ | Just ty2' <- tcView ty2 = go (Unify False ty1 ty2') sty1 ty1 sty2 ty2'
+
+ -- Variables; go for uVar
+ go outer _ (TyVarTy tyvar1) sty2 ty2 = uVar outer False tyvar1 nb2 sty2 ty2
+ go outer sty1 ty1 _ (TyVarTy tyvar2) = uVar outer True tyvar2 nb1 sty1 ty1
+ -- "True" means args swapped
+
+ -- 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 { traceTc (text "We have sigma types: equalLength" <+> ppr tvs1 <+> ppr tvs2)
+ ; unless (equalLength tvs1 tvs2) (bale_out outer)
+ ; traceTc (text "We're past the first length test")
+ ; tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo
+ -- Get location from monad, not from tvs1
+ ; let tys = mkTyVarTys tvs
+ in_scope = mkInScopeSet (mkVarSet tvs)
+ phi1 = substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1
+ phi2 = substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2
+ (theta1,tau1) = tcSplitPhiTy phi1
+ (theta2,tau2) = tcSplitPhiTy phi2
+
+ ; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do
+ { unless (equalLength theta1 theta2) (bale_out outer)
+ ; cois <- uPreds outer nb1 theta1 nb2 theta2
+ ; coi <- uTys nb1 tau1 nb2 tau2
+
+ -- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a)
+ ; free_tvs <- zonkTcTyVarsAndFV (varSetElems (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
+ ; when (any (`elemVarSet` free_tvs) tvs)
+ (bleatEscapedTvs free_tvs tvs tvs)
+
+ -- 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.
+ ; when (nb1 && nb2) (notMonoType ty1)
+ ; let mk_fun (pred, coi_pred) (ty, coi)
+ = (mkFunTy pred_ty ty, mkFunTyCoI pred_ty coi_pred ty coi)
+ where
+ pred_ty = mkPredTy pred
+ ; return (foldr mkForAllTyCoI
+ (snd (foldr mk_fun (tau1,coi) (theta1 `zip` cois)))
+ tvs)
+ }}
+ where
+ (tvs1, body1) = tcSplitForAllTys ty1
+ (tvs2, body2) = tcSplitForAllTys ty2
+
+ -- Predicates
+ go outer _ (PredTy p1) _ (PredTy p2)
+ = uPred outer nb1 p1 nb2 p2
+
+ -- Non-synonym type constructors must match
+ go outer _ (TyConApp con1 tys1) _ (TyConApp con2 tys2)
+ | con1 == con2 && not (isOpenSynTyCon con1)
+ = do { traceTc (text "utys1" <+> ppr con1 <+> (ppr tys1 $$ ppr tys2))
+ ; cois <- uTys_s outer nb1 tys1 nb2 tys2
+ ; return $ mkTyConAppCoI con1 tys1 cois
+ }
+ -- Family synonyms See Note [TyCon app]
+ | con1 == con2 && identicalOpenSynTyConApp
+ = do { traceTc (text "utys2" <+> ppr con1 <+> (ppr tys1' $$ ppr tys2'))
+ ; cois <- uTys_s outer nb1 tys1' nb2 tys2'
+ ; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois)
+ }
+ where
+ n = tyConArity con1
+ (idxTys1, tys1') = splitAt n tys1
+ (idxTys2, tys2') = splitAt n tys2
+ identicalOpenSynTyConApp = idxTys1 `tcEqTypes` idxTys2
+ -- See Note [OpenSynTyCon app]
+
+ -- Functions; just check the two parts
+ go _ _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
+ = do { coi_l <- uTys nb1 fun1 nb2 fun2
+ ; coi_r <- uTys nb1 arg1 nb2 arg2
+ ; return $ mkFunTyCoI fun1 coi_l arg1 coi_r
+ }
+
+ -- Applications need a bit of care!
+ -- They can match FunTy and TyConApp, so use splitAppTy_maybe
+ -- NB: we've already dealt with type variables and Notes,
+ -- so if one type is an App the other one jolly well better be too
+ -- See Note [Mismatched type lists and application decomposition]
+ go outer _ (AppTy s1 t1) _ ty2