X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSMonad.lhs;h=ad24eb76d8a82158ac5bdb370067bb34de1b1dca;hp=3c1961b13a6480df31cf6aaa8bdaeece1507c104;hb=50d0293555691012f96259de7f8682b94db58517;hpb=27225b0c9f799a251c96242f502e8cfd6bf76d7c diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index 3c1961b..ad24eb7 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -4,60 +4,65 @@ module TcSMonad ( -- Canonical constraints CanonicalCts, emptyCCan, andCCan, andCCans, - singleCCan, extendCCans, isEmptyCCan, - CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, - mkWantedConstraints, deCanonicaliseWanted, - makeGivens, makeSolved, + singleCCan, extendCCans, isEmptyCCan, isCTyEqCan, + isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe, + isCFrozenErr, - CtFlavor (..), isWanted, isGiven, isDerived, canRewrite, - combineCtLoc, mkGivenFlavor, + CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts, + deCanonicalise, mkFrozenError, - TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality - tryTcS, nestImplicTcS, wrapErrTcS, wrapWarnTcS, + isWanted, isGiven, isDerived, + isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising, + + isFlexiTcsTv, + + canRewrite, canSolve, + combineCtLoc, mkGivenFlavor, mkWantedFlavor, + getWantedLoc, + + TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality + traceFireTcS, bumpStepCountTcS, + tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS, SimplContext(..), isInteractive, simplEqsOnly, performDefaulting, - - -- Creation of evidence variables - newWantedCoVar, newGivOrDerCoVar, newGivOrDerEvVar, + -- Creation of evidence variables + newEvVar, newCoVar, newWantedCoVar, newGivenCoVar, + newDerivedId, newIPVar, newDictVar, newKindConstraint, -- Setting evidence variables - setWantedCoBind, setDerivedCoBind, + setWantedCoBind, setIPBind, setDictBind, setEvBind, setWantedTyBind, - newTcEvBindsTcS, - - getInstEnvs, getFamInstEnvs, -- Getting the environments + getInstEnvs, getFamInstEnvs, -- Getting the environments getTopEnv, getGblEnv, getTcEvBinds, getUntouchables, getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, - newFlattenSkolemTy, -- Flatten skolems instDFunTypes, -- Instantiation - instDFunConstraints, + instDFunConstraints, + newFlexiTcSTy, instFlexiTcS, - isGoodRecEv, + compatKind, + TcsUntouchables, isTouchableMetaTyVar, + isTouchableMetaTyVar_InRange, getDefaultInfo, getDynFlags, matchClass, matchFam, MatchInstResult (..), checkWellStagedDFun, warnTcS, - pprEq, -- Smaller utils, re-exported from TcM + pprEq -- Smaller utils, re-exported from TcM -- TODO (DV): these are only really used in the -- instance matcher in TcSimplify. I am wondering -- if the whole instance matcher simply belongs -- here - - - mkWantedFunDepEqns -- Instantiation of 'Equations' from FunDeps - ) where #include "HsVersions.h" @@ -70,14 +75,11 @@ import InstEnv import FamInst import FamInstEnv -import NameSet ( addOneToNameSet ) - import qualified TcRnMonad as TcM import qualified TcMType as TcM import qualified TcEnv as TcM ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys ) import TcType -import Module import DynFlags import Coercion @@ -96,7 +98,6 @@ import FastString import HsBinds -- for TcEvBinds stuff import Id -import FunDeps import TcRnTypes @@ -133,7 +134,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 +142,18 @@ 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 + -- * typeKind xi `compatKind` typeKind tv + -- See Note [Spontaneous solving and kind compatibility] + -- * We prefer unification variables on the left *JUST* for efficiency 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 + -- * typeKind (F xis) `compatKind` typeKind xi cc_id :: EvVar, cc_flavor :: CtFlavor, cc_fun :: TyCon, -- A type function @@ -163,34 +163,34 @@ data CanonicalCt } -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 --- 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 } - | otherwise = ct - -mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints -mkWantedConstraints flats implics - = mapBag (WcEvVar . deCanonicaliseWanted) flats `unionBags` mapBag WcImplic implics - -deCanonicaliseWanted :: CanonicalCt -> WantedEvVar -deCanonicaliseWanted ct - = WARN( not (isWanted $ cc_flavor ct), ppr ct ) - let Wanted loc = cc_flavor ct - in WantedEvVar (cc_id ct) loc + | CFrozenErr { -- A "frozen error" does not interact with anything + -- See Note [Frozen Errors] + cc_id :: EvVar, + cc_flavor :: CtFlavor + } + +mkFrozenError :: CtFlavor -> EvVar -> CanonicalCt +mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl } + +compatKind :: Kind -> Kind -> Bool +compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 + +deCanonicalise :: CanonicalCt -> FlavoredEvVar +deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct) tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) = extendVarSet (tyVarsOfType xi) tv tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys) tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys -tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty +tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty +tyVarsOfCanonical (CFrozenErr { cc_id = ev }) = tyVarsOfEvVar ev + +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 @@ -204,26 +204,10 @@ instance Outputable CanonicalCt where = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty) ppr (CFunEqCan co fl tc tys ty) = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty) + ppr (CFrozenErr co fl) + = ppr fl <+> pprEvVarWithType co \end{code} - -Note [No touchables as FunEq RHS] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Notice that (F xis ~ beta), where beta is an touchable unification -variable, is not canonical. Why? - * If (F xis ~ beta) was the only wanted constraint, we'd - definitely want to spontaneously-unify it - - * But suppose we had an earlier wanted (beta ~ Int), and - have already spontaneously unified it. Then we have an - identity given (id : beta ~ Int) in the inert set. - - * But (F xis ~ beta) does not react with that given (because we - don't subsitute on the RHS of a function equality). So there's a - serious danger that we'd spontaneously unify it a second time. - -Hence the invariant. - Note [Canonical implicit parameter constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The type in a canonical implicit parameter constraint doesn't need to @@ -253,6 +237,27 @@ emptyCCan = emptyBag isEmptyCCan :: CanonicalCts -> Bool isEmptyCCan = isEmptyBag + +isCTyEqCan :: CanonicalCt -> Bool +isCTyEqCan (CTyEqCan {}) = True +isCTyEqCan (CFunEqCan {}) = False +isCTyEqCan _ = False + +isCDictCan_Maybe :: CanonicalCt -> Maybe Class +isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls +isCDictCan_Maybe _ = Nothing + +isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name) +isCIPCan_Maybe (CIPCan {cc_ip_nm = nm }) = Just nm +isCIPCan_Maybe _ = Nothing + +isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon +isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc +isCFunEqCan_Maybe _ = Nothing + +isCFrozenErr :: CanonicalCt -> Bool +isCFrozenErr (CFrozenErr {}) = True +isCFrozenErr _ = False \end{code} %************************************************************************ @@ -263,55 +268,60 @@ 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; - -- *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. - -instance Outputable CtFlavor where - ppr (Given _) = ptext (sLit "[Given]") - ppr (Wanted _) = ptext (sLit "[Wanted]") - ppr (Derived _) = ptext (sLit "[Derived]") - -isWanted :: CtFlavor -> Bool -isWanted (Wanted {}) = True -isWanted _ = False - -isGiven :: CtFlavor -> Bool -isGiven (Given {}) = True -isGiven _ = False - -isDerived :: CtFlavor -> Bool -isDerived (Derived {}) = True -isDerived _ = False +getWantedLoc :: CanonicalCt -> WantedLoc +getWantedLoc ct + = ASSERT (isWanted (cc_flavor ct)) + case cc_flavor ct of + Wanted wl -> wl + _ -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty + +isWantedCt :: CanonicalCt -> Bool +isWantedCt ct = isWanted (cc_flavor ct) +isGivenCt :: CanonicalCt -> Bool +isGivenCt ct = isGiven (cc_flavor ct) +isDerivedCt :: CanonicalCt -> Bool +isDerivedCt ct = isDerived (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 {}) = False -- DV: changing the semantics +canSolve (Derived {}) (Derived {}) = True -- DV: changing the semantics of derived +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 +-- 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 (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) -\end{code} +mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) +mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk) +mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk) +mkWantedFlavor :: CtFlavor -> CtFlavor +mkWantedFlavor (Wanted loc) = Wanted loc +mkWantedFlavor (Derived loc) = Wanted loc +mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl) +\end{code} + %************************************************************************ %* * %* The TcS solver monad * @@ -341,15 +351,26 @@ data TcSEnv -- Global type bindings tcs_context :: SimplContext, + + tcs_untch :: TcsUntouchables, - tcs_untch :: Untouchables + tcs_ic_depth :: Int, -- Implication nesting depth + tcs_count :: IORef Int -- Global step count } +type TcsUntouchables = (Untouchables,TcTyVarSet) +-- Like the TcM Untouchables, +-- but records extra TcsTv variables generated during simplification +-- See Note [Extra TcsTv untouchables] in TcSimplify +\end{code} + +\begin{code} data SimplContext = SimplInfer -- Inferring type of a let-bound thing | SimplRuleLhs -- Inferring type of a RULE lhs | SimplInteractive -- Inferring type at GHCi prompt | SimplCheck -- Checking a type signature or RULE rhs + deriving Eq instance Outputable SimplContext where ppr SimplInfer = ptext (sLit "SimplInfer") @@ -410,8 +431,21 @@ panicTcS doc = pprPanic "TcCanonical" doc traceTcS :: String -> SDoc -> TcS () traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc -traceTcS0 :: String -> SDoc -> TcS () -traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc +bumpStepCountTcS :: TcS () +bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env + ; n <- TcM.readTcRef ref + ; TcM.writeTcRef ref (n+1) } + +traceFireTcS :: Int -> SDoc -> TcS () +-- Dump a rule-firing trace +traceFireTcS depth doc + = TcS $ \env -> + TcM.ifDOptM Opt_D_dump_cs_trace $ + do { n <- TcM.readTcRef (tcs_count env) + ; let msg = int n + <> text (replicate (tcs_ic_depth env) '>') + <> brackets (int depth) <+> doc + ; TcM.dumpTcRn msg } runTcS :: SimplContext -> Untouchables -- Untouchables @@ -420,42 +454,64 @@ runTcS :: SimplContext runTcS context untouch tcs = do { ty_binds_var <- TcM.newTcRef emptyVarEnv ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds + ; step_count <- TcM.newTcRef 0 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var , tcs_ty_binds = ty_binds_var - , tcs_context = context - , tcs_untch = untouch } + , tcs_context = context + , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet + , tcs_count = step_count + , tcs_ic_depth = 0 + } -- Run the computation ; res <- unTcS tcs env - -- Perform the type unifications required ; ty_binds <- TcM.readTcRef ty_binds_var ; mapM_ do_unification (varEnvElts ty_binds) +#ifdef DEBUG + ; count <- TcM.readTcRef step_count + ; TcM.dumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count) +#endif -- And return - ; ev_binds <- TcM.readTcRef evb_ref + ; ev_binds <- TcM.readTcRef evb_ref ; return (res, evBindMapBinds ev_binds) } where do_unification (tv,ty) = TcM.writeMetaTyVar tv ty - -nestImplicTcS :: EvBindsVar -> Untouchables -> TcS a -> TcS a -nestImplicTcS ref untch (TcS thing_inside) - = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } -> +nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a +nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside) + = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds + , tcs_untch = (_outer_range, outer_tcs) + , tcs_count = count + , tcs_ic_depth = idepth + , tcs_context = ctxt } -> let + inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs) + -- The inner_range should be narrower than the outer one + -- (thus increasing the set of untouchables) but + -- the inner Tcs-untouchables must be unioned with the + -- outer ones! nest_env = TcSEnv { tcs_ev_binds = ref , tcs_ty_binds = ty_binds - , tcs_untch = untch + , tcs_untch = inner_untch + , tcs_count = count + , tcs_ic_depth = idepth+1 , tcs_context = ctxtUnderImplic ctxt } in 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 :: 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 tcs @@ -477,13 +533,13 @@ getTcSContext = TcS (return . tcs_context) getTcEvBinds :: TcS EvBindsVar getTcEvBinds = TcS (return . tcs_ev_binds) -getUntouchables :: TcS Untouchables +getUntouchables :: TcS TcsUntouchables getUntouchables = TcS (return . tcs_untch) getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType))) getTcSTyBinds = TcS (return . tcs_ty_binds) -getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType)) +getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType)) getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) @@ -497,16 +553,19 @@ setWantedCoBind cv co = setEvBind cv (EvCoercion co) -- Was: wrapTcS $ TcM.writeWantedCoVar cv co -setDerivedCoBind :: CoVar -> Coercion -> TcS () -setDerivedCoBind cv co - = setEvBind cv (EvCoercion co) - setWantedTyBind :: TcTyVar -> TcType -> TcS () -- Add a type binding +-- We never do this twice! setWantedTyBind tv ty = do { ref <- getTcSTyBinds ; wrapTcS $ do { ty_binds <- TcM.readTcRef ref +#ifdef DEBUG + ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $ + vcat [ text "TERRIBLE ERROR: double set of meta type variable" + , ppr tv <+> text ":=" <+> ppr ty + , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)] +#endif ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } } setIPBind :: EvVar -> EvTerm -> TcS () @@ -518,12 +577,9 @@ setDictBind = setEvBind setEvBind :: EvVar -> EvTerm -> TcS () -- Internal setEvBind ev rhs - = do { tc_evbinds <- getTcEvBinds + = do { tc_evbinds <- getTcEvBinds ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) } -newTcEvBindsTcS :: TcS EvBindsVar -newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds) - warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS () warnTcS loc warn_if doc | warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc @@ -567,13 +623,21 @@ pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2) isTouchableMetaTyVar :: TcTyVar -> TcS Bool isTouchableMetaTyVar tv - = case tcTyVarDetails tv of - MetaTv TcsTv _ -> return True -- See Note [Touchable meta type variables] - MetaTv {} -> do { untch <- getUntouchables - ; return (inTouchableRange untch tv) } - _ -> return False + = do { untch <- getUntouchables + ; return $ isTouchableMetaTyVar_InRange untch tv } + +isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool +isTouchableMetaTyVar_InRange (untch,untch_tcs) tv + = case tcTyVarDetails tv of + MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs) + -- 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 @@ -595,9 +659,12 @@ newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar 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) } + = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique + ; let name = TcM.mkTcTyVarName uniq (fsLit "f") + ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } + ; traceTcS "New Flatten Skolem Born" $ + (ppr tv <+> text "[:= " <+> ppr ty <+> text "]") + ; return tv } -- Instantiations -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -607,33 +674,65 @@ 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 (Left tv) = mkTyVarTy <$> instFlexiTcS 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 + +instFlexiTcS :: 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] +instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv) + +newFlexiTcSTy :: Kind -> TcS TcType +newFlexiTcSTy knd + = wrapTcS $ + do { uniq <- TcM.newUnique + ; ref <- TcM.newMutVar Flexi + ; let name = TcM.mkTcTyVarName uniq (fsLit "uf") + ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) } + +isFlexiTcsTv :: TyVar -> Bool +isFlexiTcsTv tv + | not (isTcTyVar tv) = False + | MetaTv TcsTv _ <- tcTyVarDetails tv = True + | otherwise = False + +newKindConstraint :: TcTyVar -> Kind -> TcS CoVar +-- Create new wanted CoVar that constrains the type to have the specified kind. +newKindConstraint tv knd + = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd + ; let ty_k = mkTyVarTy tv_k + ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k + ; return co_var } + +instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar +instFlexiTcSHelper 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 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar -newGivOrDerEvVar pty evtrm - = do { ev <- wrapTcS $ TcM.newEvVar pty - ; setEvBind ev evtrm - ; return ev } +newEvVar :: TcPredType -> TcS EvVar +newEvVar pty = wrapTcS $ TcM.newEvVar pty + +newDerivedId :: TcPredType -> TcS EvVar +newDerivedId pty = wrapTcS $ TcM.newEvVar pty -newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar +newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar -- Note we create immutable variables for given or derived, since we -- must bind them to TcEvBinds (because their evidence may involve -- superclasses). However we should be able to override existing -- 'derived' evidence, even in TcEvBinds -newGivOrDerCoVar ty1 ty2 co +newGivenCoVar ty1 ty2 co = do { cv <- newCoVar ty1 ty2 ; setEvBind cv (EvCoercion co) ; return cv } @@ -641,10 +740,7 @@ 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 :: TcType -> TcType -> TcS EvVar newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2 newIPVar :: IPName Name -> TcType -> TcS EvVar @@ -656,83 +752,6 @@ newDictVar cl tys = wrapTcS $ TcM.newDict cl tys \begin{code} -isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool --- In a call (isGoodRecEv ev wv), we are considering solving wv --- using some term that involves ev, such as: --- by setting wv = ev --- or wv = EvCast x |> ev --- etc. --- But that would be Very Bad if the evidence for 'ev' mentions 'wv', --- in an "unguarded" way. So isGoodRecEv looks at the evidence ev --- recursively through the evidence binds, to see if uses of 'wv' are guarded. --- --- Guarded means: more instance calls than superclass selections. We --- compute this by chasing the evidence, adding +1 for every instance --- call (constructor) and -1 for every superclass selection (destructor). --- --- See Note [Superclasses and recursive dictionaries] in TcInteract -isGoodRecEv ev_var (WantedEvVar wv _) - = do { tc_evbinds <- getTcEvBindsBag - ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var - ; return $ case mb of - Nothing -> True - Just min_guardedness -> min_guardedness > 0 - } - - where chase_ev_var :: EvBindMap -- Evidence binds - -> EvVar -- Target variable whose gravity we want to return - -> Int -- Current gravity - -> [EvVar] -- Visited nodes - -> EvVar -- Current node - -> TcS (Maybe Int) - chase_ev_var assocs trg curr_grav visited orig - | trg == orig = return $ Just curr_grav - | orig `elem` visited = return $ Nothing - | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig - = chase_ev assocs trg curr_grav (orig:visited) ev_trm - -{- No longer needed: evidence is in the EvBinds - | isTcTyVar orig && isMetaTyVar orig - = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig - ; case meta_details of - Flexi -> return Nothing - Indirect tyco -> chase_ev assocs trg curr_grav - (orig:visited) (EvCoercion tyco) - } --} - | otherwise = return Nothing - - chase_ev assocs trg curr_grav visited (EvId v) - = chase_ev_var assocs trg curr_grav visited v - chase_ev assocs trg curr_grav visited (EvSuperClass d_id _) - = chase_ev_var assocs trg (curr_grav-1) visited d_id - chase_ev assocs trg curr_grav visited (EvCast v co) - = do { m1 <- chase_ev_var assocs trg curr_grav visited v - ; m2 <- chase_co assocs trg curr_grav visited co - ; return (comb_chase_res Nothing [m1,m2]) } - - chase_ev assocs trg curr_grav visited (EvCoercion co) - = chase_co assocs trg curr_grav visited co - chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars) - = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars - ; return (comb_chase_res Nothing chase_results) } - - chase_co assocs trg curr_grav visited co - = -- Look for all the coercion variables in the coercion - -- chase them, and combine the results. This is OK since the - -- coercion will not contain any superclass terms -- anything - -- that involves dictionaries will be bound in assocs. - let co_vars = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) [] - (tyVarsOfType co) - in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars - ; return (comb_chase_res Nothing chase_results) } - - comb_chase_res f [] = f - comb_chase_res f (Nothing:rest) = comb_chase_res f rest - comb_chase_res Nothing (Just n:rest) = comb_chase_res (Just n) rest - comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest - - -- Matching and looking up classes and family instances -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -747,7 +766,7 @@ matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcT matchClass clas tys = do { let pred = mkClassPred clas tys ; instEnvs <- getInstEnvs - ; case lookupInstEnv instEnvs clas tys of { + ; case lookupInstEnv instEnvs clas tys of { ([], unifs) -- Nothing matches -> do { traceTcS "matchClass not matching" (vcat [ text "dict" <+> ppr pred, @@ -759,10 +778,9 @@ matchClass clas tys ; traceTcS "matchClass success" (vcat [text "dict" <+> ppr pred, text "witness" <+> ppr dfun_id - <+> ppr (idType dfun_id) ]) + <+> ppr (idType dfun_id) ]) -- Record that this dfun is needed - ; record_dfun_usage dfun_id - ; return $ MatchInstSingle (dfun_id, inst_tys) + ; return $ MatchInstSingle (dfun_id, inst_tys) } ; (matches, unifs) -- More than one matches -> do { traceTcS "matchClass multiple matches, deferring choice" @@ -773,26 +791,8 @@ matchClass clas tys } } } - where record_dfun_usage :: Id -> TcS () - record_dfun_usage dfun_id - = do { hsc_env <- getTopEnv - ; let dfun_name = idName dfun_id - dfun_mod = ASSERT( isExternalName dfun_name ) - nameModule dfun_name - ; if isInternalName dfun_name || -- Internal name => defined in this module - modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env) - then return () -- internal, or in another package - else do updInstUses dfun_id - } - - updInstUses :: Id -> TcS () - updInstUses dfun_id - = do { tcg_env <- getGblEnv - ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env) - (`addOneToNameSet` idName dfun_id) - } - -matchFam :: TyCon + +matchFam :: TyCon -> [Type] -> TcS (MatchInstResult (TyCon, [Type])) matchFam tycon args @@ -803,32 +803,4 @@ matchFam tycon args -- DV: We never return MatchInstMany, since tcLookupFamInst never returns -- multiple matches. Check. } - - --- Functional dependencies, instantiation of equations -------------------------------------------------------- - -mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))] - -> TcS [WantedEvVar] -mkWantedFunDepEqns _ [] = return [] -mkWantedFunDepEqns loc eqns - = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns)) - ; wevvars <- mapM to_work_item eqns - ; return $ concat wevvars } - where - to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar] - to_work_item ((qtvs, pairs), _, _) - = do { let tvs = varSetElems qtvs - ; tvs' <- mapM newFlexiTcS tvs - ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs') - ; mapM (do_one subst) pairs } - - do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1 - sty2 = substTy subst ty2 - ; ev <- newWantedCoVar sty1 sty2 - ; return (WantedEvVar ev loc) } - -pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc -pprEquationDoc (eqn, (p1, _), (p2, _)) - = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)] \end{code}