-u_tys :: Outer
- -> InBox -> TcType -> TcType -- ty1 is the *actual* type
- -> InBox -> TcType -> TcType -- ty2 is the *expected* type
- -> TcM CoercionI
-
-u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
- = do { traceTc (text "u_tys " <+> ppr ty1 <+> text " " <+> ppr ty2)
- ; coi <- go outer ty1 ty2
- ; traceTc (case coi of
- ACo co -> text "u_tys yields coercion: " <+> ppr co
- IdCo -> text "u_tys yields no coercion")
- ; return coi
- }
- where
-
- go :: Outer -> TcType -> TcType -> TcM CoercionI
- go outer ty1 ty2 =
- do { traceTc (text "go " <+> ppr orig_ty1 <+> text "/" <+> ppr ty1
- <+> ppr orig_ty2 <+> text "/" <+> ppr ty2)
- ; go1 outer ty1 ty2
- }
-
- go1 :: Outer -> TcType -> TcType -> TcM CoercionI
- -- Always expand synonyms: see Note [Unification and synonyms]
- -- (this also throws away FTVs)
- go1 outer ty1 ty2
- | Just ty1' <- tcView ty1 = go False ty1' ty2
- | Just ty2' <- tcView ty2 = go False ty1 ty2'
-
- -- Variables; go for uVar
- go1 outer (TyVarTy tyvar1) ty2 = uVar outer False tyvar1 nb2 orig_ty2 ty2
- go1 outer ty1 (TyVarTy tyvar2) = uVar outer True tyvar2 nb1 orig_ty1 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
- go1 _ ty1 ty2
- | isSigmaTy ty1 || isSigmaTy ty2
- = do { traceTc (text "We have sigma types: equalLength" <+> ppr tvs1 <+> ppr tvs2)
- ; checkM (equalLength tvs1 tvs2)
- (unifyMisMatch outer False orig_ty1 orig_ty2)
- ; 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
- { checkM (equalLength theta1 theta2)
- (unifyMisMatch outer False orig_ty1 orig_ty2)
-
- ; cois <- uPreds False 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))
- ; ifM (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.
- ; ifM (nb1 && nb2) (notMonoType ty1)
- ; return coi
- }}
- where
- (tvs1, body1) = tcSplitForAllTys ty1
- (tvs2, body2) = tcSplitForAllTys ty2
-
- -- Predicates
- go1 outer (PredTy p1) (PredTy p2)
- = uPred False nb1 p1 nb2 p2
-
- -- Type constructors must match
- go1 _ (TyConApp con1 tys1) (TyConApp con2 tys2)
- | con1 == con2 && not (isOpenSynTyCon con1)
- = do { cois <- uTys_s nb1 tys1 nb2 tys2
- ; return $ mkTyConAppCoI con1 tys1 cois
- }
- -- 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]
-
- -- Functions; just check the two parts
- go1 _ (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
- go1 outer (AppTy s1 t1) ty2
+-- Push a new item on the origin stack (the most common case)
+uType origin ty1 ty2 -- Push a new item on the origin stack
+ = uType_np (pushOrigin ty1 ty2 origin) ty1 ty2
+
+--------------
+-- unify_np (short for "no push" on the origin stack) does the work
+uType_np origin orig_ty1 orig_ty2
+ = do { traceTc "u_tys " $ vcat
+ [ sep [ ppr orig_ty1, text "~", ppr orig_ty2]
+ , ppr origin]
+ ; coi <- go orig_ty1 orig_ty2
+ ; case coi of
+ ACo co -> traceTc "u_tys yields coercion:" (ppr co)
+ IdCo _ -> traceTc "u_tys yields no coercion" empty
+ ; return coi }
+ where
+ bale_out :: [EqOrigin] -> TcM a
+ bale_out origin = failWithMisMatch origin
+
+ go :: TcType -> TcType -> TcM CoercionI
+ -- The arguments to 'go' are always semantically identical
+ -- to orig_ty{1,2} except for looking through type synonyms
+
+ -- Variables; go for uVar
+ -- Note that we pass in *original* (before synonym expansion),
+ -- so that type variables tend to get filled in with
+ -- the most informative version of the type
+ go (TyVarTy tyvar1) ty2 = uVar origin NotSwapped tyvar1 ty2
+ go ty1 (TyVarTy tyvar2) = uVar origin IsSwapped tyvar2 ty1
+
+ -- Expand synonyms:
+ -- see Note [Unification and synonyms]
+ -- Do this after the variable case so that we tend to unify
+ -- variables with un-expanded type synonym
+ --
+ -- Also NB that we recurse to 'go' so that we don't push a
+ -- new item on the origin stack. As a result if we have
+ -- type Foo = Int
+ -- and we try to unify Foo ~ Bool
+ -- we'll end up saying "can't match Foo with Bool"
+ -- rather than "can't match "Int with Bool". See Trac #4535.
+ go ty1 ty2
+ | Just ty1' <- tcView ty1 = go ty1' ty2
+ | Just ty2' <- tcView ty2 = go ty1 ty2'
+
+
+ -- Predicates
+ go (PredTy p1) (PredTy p2) = uPred origin p1 p2
+
+ -- Coercion functions: (t1a ~ t1b) => t1c ~ (t2a ~ t2b) => t2c
+ go ty1 ty2
+ | Just (t1a,t1b,t1c) <- splitCoPredTy_maybe ty1,
+ Just (t2a,t2b,t2c) <- splitCoPredTy_maybe ty2
+ = do { co1 <- uType origin t1a t2a
+ ; co2 <- uType origin t1b t2b
+ ; co3 <- uType origin t1c t2c
+ ; return $ mkCoPredCoI co1 co2 co3 }
+
+ -- Functions (or predicate functions) just check the two parts
+ go (FunTy fun1 arg1) (FunTy fun2 arg2)
+ = do { coi_l <- uType origin fun1 fun2
+ ; coi_r <- uType origin arg1 arg2
+ ; return $ mkFunTyCoI coi_l coi_r }
+
+ -- Always defer if a type synonym family (type function)
+ -- is involved. (Data families behave rigidly.)
+ go ty1@(TyConApp tc1 _) ty2
+ | isSynFamilyTyCon tc1 = uType_defer origin ty1 ty2
+ go ty1 ty2@(TyConApp tc2 _)
+ | isSynFamilyTyCon tc2 = uType_defer origin ty1 ty2
+
+ go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
+ | tc1 == tc2 -- See Note [TyCon app]
+ = do { cois <- uList origin uType tys1 tys2
+ ; return $ mkTyConAppCoI tc1 cois }
+
+ -- See Note [Care with type applications]
+ go (AppTy s1 t1) ty2