- 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 -- TOMDO: do something with these pred_cois
+ ; traceTc (text "TOMDO!")
+ ; 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)
+ ; return coi
+ }}
+ 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 _ _ (TyConApp con1 tys1) _ (TyConApp con2 tys2)
+ | con1 == con2 && not (isOpenSynTyCon con1)
+ = do { cois <- uTys_s nb1 tys1 nb2 tys2
+ ; return $ mkTyConAppCoI con1 tys1 cois
+ }
+ -- Family synonyms See Note [TyCon app]
+ | con1 == con2 && identicalOpenSynTyConApp
+ = do { cois <- uTys_s 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]
+
+ -- If we can reduce a family app => proceed with reduct
+ -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must
+ -- defer oversaturated applications!
+ go outer sty1 ty1@(TyConApp con1 _) sty2 ty2
+ | isOpenSynTyCon con1
+ = do { (coi1, ty1') <- tcNormaliseFamInst ty1
+ ; case coi1 of
+ IdCo -> defer -- no reduction, see [Deferred Unification]
+ _ -> liftM (coi1 `mkTransCoI`) $ go outer sty1 ty1' sty2 ty2
+ }
+
+ -- If we can reduce a family app => proceed with reduct
+ -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must
+ -- defer oversaturated applications!
+ go outer sty1 ty1 sty2 ty2@(TyConApp con2 _)
+ | isOpenSynTyCon con2
+ = do { (coi2, ty2') <- tcNormaliseFamInst ty2
+ ; case coi2 of
+ IdCo -> defer -- no reduction, see [Deferred Unification]
+ _ -> liftM (`mkTransCoI` mkSymCoI coi2) $
+ go outer sty1 ty1 sty2 ty2'
+ }
+
+ -- 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
+ go outer _ (AppTy s1 t1) _ ty2