X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSMonad.lhs;h=416ac80499b5ae26e7debce3ecd2c9f0e6fcfbf5;hp=f8b357a8d5a69753f9947dc497f266851dd42bbc;hb=0dc2b9de4dd4681aa11dfa5419c931a51b274fa6;hpb=67ed735fab12c12a1d48878d7bda33588c67fb78 diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index f8b357a..416ac80 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -4,16 +4,20 @@ module TcSMonad ( -- Canonical constraints CanonicalCts, emptyCCan, andCCan, andCCans, - singleCCan, extendCCans, isEmptyCCan, - CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, + singleCCan, extendCCans, isEmptyCCan, isTyEqCCan, + CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts, mkWantedConstraints, deCanonicaliseWanted, - makeGivens, makeSolved, + makeGivens, makeSolvedByInst, - CtFlavor (..), isWanted, isGiven, isDerived, canRewrite, - joinFlavors, mkGivenFlavor, + CtFlavor (..), isWanted, isGiven, isDerived, isDerivedSC, isDerivedByInst, + isGivenCt, isWantedCt, + + DerivedOrig (..), + canRewrite, canSolve, + combineCtLoc, mkGivenFlavor, TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality - tryTcS, nestImplicTcS, wrapErrTcS, wrapWarnTcS, + tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS, SimplContext(..), isInteractive, simplEqsOnly, performDefaulting, -- Creation of evidence variables @@ -30,8 +34,8 @@ module TcSMonad ( newTcEvBindsTcS, getInstEnvs, getFamInstEnvs, -- Getting the environments - getTopEnv, getGblEnv, getTcEvBinds, getUntouchablesTcS, - getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsBag, + getTopEnv, getGblEnv, getTcEvBinds, getUntouchables, + getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, newFlattenSkolemTy, -- Flatten skolems @@ -42,7 +46,12 @@ module TcSMonad ( isGoodRecEv, + zonkTcTypeTcS, -- Zonk through the TyBinds of the Tcs Monad + compatKind, + + isTouchableMetaTyVar, + isTouchableMetaTyVar_InRange, getDefaultInfo, getDynFlags, @@ -87,6 +96,7 @@ import TypeRep import Name import Var +import VarEnv import Outputable import Bag import MonadUtils @@ -99,7 +109,6 @@ import FunDeps import TcRnTypes -import Control.Monad import Data.IORef \end{code} @@ -133,7 +142,7 @@ data CanonicalCt | CIPCan { -- ?x::tau -- See note [Canonical implicit parameter constraints]. cc_id :: EvVar, - cc_flavor :: CtFlavor, + cc_flavor :: CtFlavor, cc_ip_nm :: IPName Name, cc_ip_ty :: TcTauType } @@ -141,19 +150,25 @@ data CanonicalCt | CTyEqCan { -- tv ~ xi (recall xi means function free) -- Invariant: -- * tv not in tvs(xi) (occurs check) - -- * If tv is a MetaTyVar, then typeKind xi <: typeKind tv - -- a skolem, then typeKind xi = typeKind tv + -- * If constraint is given then typeKind xi `compatKind` typeKind tv + -- See Note [Spontaneous solving and kind compatibility] + -- * If 'xi' is a flatten skolem then 'tv' can only be: + -- - a flatten skolem or a unification variable + -- i.e. equalities prefer flatten skolems in their LHS + -- See Note [Loopy Spontaneous Solving, Example 4] + -- Also related to [Flatten Skolem Equivalence Classes] cc_id :: EvVar, cc_flavor :: CtFlavor, - cc_tyvar :: TcTyVar, - cc_rhs :: Xi + cc_tyvar :: TcTyVar, + cc_rhs :: Xi } | CFunEqCan { -- F xis ~ xi -- Invariant: * isSynFamilyTyCon cc_fun -- * cc_rhs is not a touchable unification variable -- See Note [No touchables as FunEq RHS] - -- * typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs + -- * If constraint is given then + -- typeKind (TyConApp cc_fun cc_tyargs) `compatKind` typeKind cc_rhs cc_id :: EvVar, cc_flavor :: CtFlavor, cc_fun :: TyCon, -- A type function @@ -163,17 +178,20 @@ data CanonicalCt } +compatKind :: Kind -> Kind -> Bool +compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 + makeGivens :: CanonicalCts -> CanonicalCts makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol }) -- The UnkSkol doesn't matter because these givens are -- not contradictory (else we'd have rejected them already) -makeSolved :: CanonicalCt -> CanonicalCt +makeSolvedByInst :: CanonicalCt -> CanonicalCt -- Record that a constraint is now solved -- Wanted -> Derived -- Given, Derived -> no-op -makeSolved ct - | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc } +makeSolvedByInst ct + | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc DerInst } | otherwise = ct mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints @@ -192,6 +210,13 @@ tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes ( tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty +tyVarsOfCDict :: CanonicalCt -> TcTyVarSet +tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys +tyVarsOfCDict _ct = emptyVarSet + +tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet +tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet + tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet @@ -224,6 +249,8 @@ variable, is not canonical. Why? Hence the invariant. +The invariant is + Note [Canonical implicit parameter constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The type in a canonical implicit parameter constraint doesn't need to @@ -253,6 +280,12 @@ emptyCCan = emptyBag isEmptyCCan :: CanonicalCts -> Bool isEmptyCCan = isEmptyBag + +isTyEqCCan :: CanonicalCt -> Bool +isTyEqCCan (CTyEqCan {}) = True +isTyEqCCan (CFunEqCan {}) = False +isTyEqCCan _ = False + \end{code} %************************************************************************ @@ -265,16 +298,21 @@ isEmptyCCan = isEmptyBag \begin{code} data CtFlavor = Given GivenLoc -- We have evidence for this constraint in TcEvBinds - | Derived WantedLoc -- We have evidence for this constraint in TcEvBinds; + | Derived WantedLoc DerivedOrig + -- We have evidence for this constraint in TcEvBinds; -- *however* this evidence can contain wanteds, so -- it's valid only provisionally to the solution of -- these wanteds | Wanted WantedLoc -- We have no evidence bindings for this constraint. +data DerivedOrig = DerSC | DerInst +-- Deriveds are either superclasses of other wanteds or deriveds, or partially +-- solved wanteds from instances. + instance Outputable CtFlavor where - ppr (Given _) = ptext (sLit "[Given]") - ppr (Wanted _) = ptext (sLit "[Wanted]") - ppr (Derived _) = ptext (sLit "[Derived]") + ppr (Given _) = ptext (sLit "[Given]") + ppr (Wanted _) = ptext (sLit "[Wanted]") + ppr (Derived {}) = ptext (sLit "[Derived]") isWanted :: CtFlavor -> Bool isWanted (Wanted {}) = True @@ -288,26 +326,51 @@ isDerived :: CtFlavor -> Bool isDerived (Derived {}) = True isDerived _ = False +isDerivedSC :: CtFlavor -> Bool +isDerivedSC (Derived _ DerSC) = True +isDerivedSC _ = False + +isDerivedByInst :: CtFlavor -> Bool +isDerivedByInst (Derived _ DerInst) = True +isDerivedByInst _ = False + +isWantedCt :: CanonicalCt -> Bool +isWantedCt ct = isWanted (cc_flavor ct) +isGivenCt :: CanonicalCt -> Bool +isGivenCt ct = isGiven (cc_flavor ct) + +canSolve :: CtFlavor -> CtFlavor -> Bool +-- canSolve ctid1 ctid2 +-- The constraint ctid1 can be used to solve ctid2 +-- "to solve" means a reaction where the active parts of the two constraints match. +-- active(F xis ~ xi) = F xis +-- active(tv ~ xi) = tv +-- active(D xis) = D xis +-- active(IP nm ty) = nm +----------------------------------------- +canSolve (Given {}) _ = True +canSolve (Derived {}) (Wanted {}) = True +canSolve (Derived {}) (Derived {}) = True +canSolve (Wanted {}) (Wanted {}) = True +canSolve _ _ = False + canRewrite :: CtFlavor -> CtFlavor -> Bool -- canRewrite ctid1 ctid2 --- The constraint ctid1 can be used to rewrite ctid2 -canRewrite (Given {}) _ = True -canRewrite (Derived {}) (Wanted {}) = True -canRewrite (Derived {}) (Derived {}) = True -canRewrite (Wanted {}) (Wanted {}) = True -canRewrite _ _ = False - -joinFlavors :: CtFlavor -> CtFlavor -> CtFlavor -joinFlavors (Wanted loc) _ = Wanted loc -joinFlavors _ (Wanted loc) = Wanted loc -joinFlavors (Derived loc) _ = Derived loc -joinFlavors _ (Derived loc) = Derived loc -joinFlavors (Given loc) _ = Given loc +-- The *equality_constraint* ctid1 can be used to rewrite inside ctid2 +canRewrite = canSolve + +combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc +-- Precondition: At least one of them should be wanted +combineCtLoc (Wanted loc) _ = loc +combineCtLoc _ (Wanted loc) = loc +combineCtLoc (Derived loc _) _ = loc +combineCtLoc _ (Derived loc _) = loc +combineCtLoc _ _ = panic "combineCtLoc: both given" mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor -mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) -mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk) -mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk) +mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) +mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk) +mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk) \end{code} @@ -336,10 +399,12 @@ data TcSEnv tcs_ev_binds :: EvBindsVar, -- Evidence bindings - tcs_ty_binds :: IORef (Bag (TcTyVar, TcType)), + tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)), -- Global type bindings - tcs_context :: SimplContext + tcs_context :: SimplContext, + + tcs_untch :: Untouchables } data SimplContext @@ -411,22 +476,23 @@ traceTcS0 :: String -> SDoc -> TcS () traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc runTcS :: SimplContext - -> TcTyVarSet -- Untouchables + -> Untouchables -- Untouchables -> TcS a -- What to run -> TcM (a, Bag EvBind) runTcS context untouch tcs - = do { ty_binds_var <- TcM.newTcRef emptyBag + = do { ty_binds_var <- TcM.newTcRef emptyVarEnv ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds ; let env = TcSEnv { tcs_ev_binds = ev_binds_var , tcs_ty_binds = ty_binds_var - , tcs_context = context } + , tcs_context = context + , tcs_untch = untouch } -- Run the computation - ; res <- TcM.setUntouchables untouch (unTcS tcs env) + ; res <- unTcS tcs env -- Perform the type unifications required ; ty_binds <- TcM.readTcRef ty_binds_var - ; mapBagM_ do_unification ty_binds + ; mapM_ do_unification (varEnvElts ty_binds) -- And return ; ev_binds <- TcM.readTcRef evb_ref @@ -435,30 +501,36 @@ runTcS context untouch tcs do_unification (tv,ty) = TcM.writeMetaTyVar tv ty -nestImplicTcS :: EvBindsVar -> TcTyVarSet -> TcS a -> TcS a -nestImplicTcS ref untouch tcs +nestImplicTcS :: EvBindsVar -> Untouchables -> TcS a -> TcS a +nestImplicTcS ref untch (TcS thing_inside) = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } -> let nest_env = TcSEnv { tcs_ev_binds = ref , tcs_ty_binds = ty_binds - , tcs_context = ctxtUnderImplic ctxt } + , tcs_untch = untch + , tcs_context = ctxtUnderImplic ctxt } in - TcM.setUntouchables untouch (unTcS tcs nest_env) + thing_inside nest_env + +recoverTcS :: TcS a -> TcS a -> TcS a +recoverTcS (TcS recovery_code) (TcS thing_inside) + = TcS $ \ env -> + TcM.recoverM (recovery_code env) (thing_inside env) ctxtUnderImplic :: SimplContext -> SimplContext -- See Note [Simplifying RULE lhs constraints] in TcSimplify ctxtUnderImplic SimplRuleLhs = SimplCheck ctxtUnderImplic ctxt = ctxt -tryTcS :: TcTyVarSet -> TcS a -> TcS a +tryTcS :: TcS a -> TcS a -- Like runTcS, but from within the TcS monad -- Ignore all the evidence generated, and do not affect caller's evidence! -tryTcS untch tcs - = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyBag +tryTcS tcs + = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv ; ev_binds_var <- TcM.newTcEvBinds ; let env1 = env { tcs_ev_binds = ev_binds_var , tcs_ty_binds = ty_binds_var } - ; TcM.setUntouchables untch (unTcS tcs env1) }) + ; unTcS tcs env1 }) -- Update TcEvBinds -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -472,11 +544,14 @@ getTcSContext = TcS (return . tcs_context) getTcEvBinds :: TcS EvBindsVar getTcEvBinds = TcS (return . tcs_ev_binds) -getTcSTyBinds :: TcS (IORef (Bag (TcTyVar, TcType))) +getUntouchables :: TcS Untouchables +getUntouchables = TcS (return . tcs_untch) + +getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType))) getTcSTyBinds = TcS (return . tcs_ty_binds) -getTcSTyBindsBag :: TcS (Bag (TcTyVar, TcType)) -getTcSTyBindsBag = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) +getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType)) +getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) getTcEvBindsBag :: TcS EvBindMap @@ -499,7 +574,7 @@ setWantedTyBind tv ty = do { ref <- getTcSTyBinds ; wrapTcS $ do { ty_binds <- TcM.readTcRef ref - ; TcM.writeTcRef ref (ty_binds `snocBag` (tv,ty)) } } + ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } } setIPBind :: EvVar -> EvTerm -> TcS () setIPBind = setEvBind @@ -542,9 +617,6 @@ getTopEnv = wrapTcS $ TcM.getTopEnv getGblEnv :: TcS TcGblEnv getGblEnv = wrapTcS $ TcM.getGblEnv -getUntouchablesTcS :: TcS TcTyVarSet -getUntouchablesTcS = wrapTcS $ TcM.getUntouchables - -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher] -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -561,41 +633,90 @@ pprEq :: TcType -> TcType -> SDoc pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2) isTouchableMetaTyVar :: TcTyVar -> TcS Bool --- is touchable variable! -isTouchableMetaTyVar v - | isMetaTyVar v = wrapTcS $ do { untch <- TcM.isUntouchable v; - ; return (not untch) } - | otherwise = return False +isTouchableMetaTyVar tv + = do { untch <- getUntouchables + ; return $ isTouchableMetaTyVar_InRange untch tv } +isTouchableMetaTyVar_InRange :: Untouchables -> TcTyVar -> Bool +isTouchableMetaTyVar_InRange untch tv + = case tcTyVarDetails tv of + MetaTv TcsTv _ -> True -- See Note [Touchable meta type variables] + MetaTv {} -> inTouchableRange untch tv + _ -> False + +\end{code} + + +Note [Touchable meta type variables] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Meta type variables allocated *by the constraint solver itself* are always +touchable. Example: + instance C a b => D [a] where... +if we use this instance declaration we "make up" a fresh meta type +variable for 'b', which we must later guess. (Perhaps C has a +functional dependency.) But since we aren't in the constraint *generator* +we can't allocate a Unique in the touchable range for this implication +constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable. + + +\begin{code} -- Flatten skolems -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ newFlattenSkolemTy :: TcType -> TcS TcType newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty - where newFlattenSkolemTyVar :: TcType -> TcS TcTyVar - newFlattenSkolemTyVar ty - = wrapTcS $ do { uniq <- TcM.newUnique - ; let name = mkSysTvName uniq (fsLit "f") - ; return $ - mkTcTyVar name (typeKind ty) (FlatSkol ty) - } + +newFlattenSkolemTyVar :: TcType -> TcS TcTyVar +newFlattenSkolemTyVar ty + = wrapTcS $ do { uniq <- TcM.newUnique + ; let name = mkSysTvName uniq (fsLit "f") + ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } -- Instantiations -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ instDFunTypes :: [Either TyVar TcType] -> TcS [TcType] -instDFunTypes mb_inst_tys = - let inst_tv :: Either TyVar TcType -> TcS Type - inst_tv (Left tv) = wrapTcS $ TcM.tcInstTyVar tv >>= return . mkTyVarTy - inst_tv (Right ty) = return ty - in mapM inst_tv mb_inst_tys - +instDFunTypes mb_inst_tys + = mapM inst_tv mb_inst_tys + where + inst_tv :: Either TyVar TcType -> TcS Type + inst_tv (Left tv) = mkTyVarTy <$> newFlexiTcS tv + inst_tv (Right ty) = return ty instDFunConstraints :: TcThetaType -> TcS [EvVar] instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds +-- newFlexiTcS :: TyVar -> TcS TcTyVar +-- -- Make a TcsTv meta tyvar; it is always touchable, +-- -- but we are supposed to guess its instantiation +-- -- See Note [Touchable meta type variables] +-- newFlexiTcS tv = wrapTcS $ TcM.instMetaTyVar TcsTv tv + +newFlexiTcS :: TyVar -> TcS TcTyVar +-- Like TcM.instMetaTyVar but the variable that is created is always +-- touchable; we are supposed to guess its instantiation. +-- See Note [Touchable meta type variables] +newFlexiTcS tv = newFlexiTcSHelper (tyVarName tv) (tyVarKind tv) + +newKindConstraint :: TcTyVar -> Kind -> TcS (CoVar, Type) +-- Create new wanted CoVar that constrains the type to have the specified kind. +newKindConstraint tv knd + = do { tv_k <- newFlexiTcSHelper (tyVarName tv) knd + ; let ty_k = mkTyVarTy tv_k + ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k + ; return (co_var, ty_k) } + +newFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar +newFlexiTcSHelper tvname tvkind + = wrapTcS $ + do { uniq <- TcM.newUnique + ; ref <- TcM.newMutVar Flexi + ; let name = setNameUnique tvname uniq + kind = tvkind + ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) } + -- Superclasses and recursive dictionaries -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -618,8 +739,6 @@ newGivOrDerCoVar ty1 ty2 co newWantedCoVar :: TcType -> TcType -> TcS EvVar newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2 -newKindConstraint :: TcType -> Kind -> TcS (CoVar, TcType) -newKindConstraint ty kind = wrapTcS $ TcM.newKindConstraint ty kind newCoVar :: TcType -> TcType -> TcS EvVar newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2 @@ -782,6 +901,20 @@ matchFam tycon args } +zonkTcTypeTcS :: TcType -> TcS TcType +-- Zonk through the TyBinds of the Tcs Monad +zonkTcTypeTcS ty + = do { subst <- getTcSTyBindsMap >>= return . varEnvElts + ; let (dom,rng) = unzip subst + apply_once = substTyWith dom rng + ; let rng_idemp = [ substTyWith dom rng_idemp (apply_once t) | t <- rng ] + ; return (substTyWith dom rng_idemp ty) } + + + + + + -- Functional dependencies, instantiation of equations ------------------------------------------------------- @@ -795,11 +928,13 @@ mkWantedFunDepEqns loc eqns where to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar] to_work_item ((qtvs, pairs), _, _) - = do { (_, _, tenv) <- wrapTcS $ TcM.tcInstTyVars (varSetElems qtvs) - ; mapM (do_one tenv) pairs } + = do { let tvs = varSetElems qtvs + ; tvs' <- mapM newFlexiTcS tvs + ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs') + ; mapM (do_one subst) pairs } - do_one tenv (ty1, ty2) = do { let sty1 = substTy tenv ty1 - sty2 = substTy tenv ty2 + do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1 + sty2 = substTy subst ty2 ; ev <- newWantedCoVar sty1 sty2 ; return (WantedEvVar ev loc) }