X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSMonad.lhs;h=7b7a9f483dd26b918f004be0940ad050ecdd9bba;hp=c98681139dea0eb4b6723a259d15a53e37b2b32f;hb=61f93d4611724685c5808bcfd41e3d3e0f3aa94f;hpb=2072edcfe180f617d8f9f8990f682589c4e35082 diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index c986811..7b7a9f4 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -4,16 +4,25 @@ module TcSMonad ( -- Canonical constraints CanonicalCts, emptyCCan, andCCan, andCCans, - singleCCan, extendCCans, isEmptyCCan, - CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, + singleCCan, extendCCans, isEmptyCCan, isCTyEqCan, + isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe, + + CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts, mkWantedConstraints, deCanonicaliseWanted, - makeGivens, makeSolved, + makeGivens, makeSolvedByInst, + + CtFlavor (..), isWanted, isGiven, isDerived, + isGivenCt, isWantedCt, pprFlavorArising, + + isFlexiTcsTv, - CtFlavor (..), isWanted, isGiven, isDerived, canRewrite, - joinFlavors, mkGivenFlavor, + DerivedOrig (..), + canRewrite, canSolve, + combineCtLoc, mkGivenFlavor, mkWantedFlavor, + getWantedLoc, 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,20 +39,27 @@ module TcSMonad ( newTcEvBindsTcS, getInstEnvs, getFamInstEnvs, -- Getting the environments - getTopEnv, getGblEnv, getTcEvBinds, getUntouchablesTcS, - getTcEvBindsBag, getTcSContext, getTcSTyBinds, - + getTopEnv, getGblEnv, getTcEvBinds, getUntouchables, + getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, getTcSErrors, + getTcSErrorsBag, FrozenError (..), + addErrorTcS, + ErrorKind(..), newFlattenSkolemTy, -- Flatten skolems - zonkFlattenedType, instDFunTypes, -- Instantiation - instDFunConstraints, + instDFunConstraints, + newFlexiTcSTy, isGoodRecEv, + compatKind, + + + TcsUntouchables, isTouchableMetaTyVar, + isTouchableMetaTyVar_InRange, getDefaultInfo, getDynFlags, @@ -71,14 +87,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 @@ -88,6 +101,7 @@ import TypeRep import Name import Var +import VarEnv import Outputable import Bag import MonadUtils @@ -134,7 +148,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 } @@ -142,19 +156,19 @@ 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] + -- * 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 + -- * If constraint is given then + -- typeKind (F xis) `compatKind` typeKind xi cc_id :: EvVar, cc_flavor :: CtFlavor, cc_fun :: TyCon, -- A type function @@ -164,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 @@ -193,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 @@ -207,24 +231,6 @@ instance Outputable CanonicalCt where = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty) \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 @@ -254,6 +260,24 @@ 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 + \end{code} %************************************************************************ @@ -266,16 +290,22 @@ 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 | DerSelf +-- Deriveds are either superclasses of other wanteds or deriveds, or partially +-- solved wanteds from instances, or 'self' dictionaries containing yet wanted +-- superclasses. + 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 @@ -289,26 +319,61 @@ isDerived :: CtFlavor -> Bool isDerived (Derived {}) = True isDerived _ = False +pprFlavorArising :: CtFlavor -> SDoc +pprFlavorArising (Derived wl _) = pprArisingAt wl +pprFlavorArising (Wanted wl) = pprArisingAt wl +pprFlavorArising (Given gl) = pprArisingAt gl + +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) + +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) + +mkWantedFlavor :: CtFlavor -> CtFlavor +mkWantedFlavor (Wanted loc) = Wanted loc +mkWantedFlavor (Derived loc _) = Wanted loc +mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl) \end{code} @@ -337,12 +402,58 @@ 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_errors :: IORef (Bag FrozenError), + -- Frozen errors that we defer reporting as much as possible, in order to + -- make them as informative as possible. See Note [Frozen Errors] + + tcs_untch :: TcsUntouchables } +type TcsUntouchables = (Untouchables,TcTyVarSet) +-- Like the TcM Untouchables, +-- but records extra TcsTv variables generated during simplification +-- See Note [Extra TcsTv untouchables] in TcSimplify + +data FrozenError + = FrozenError ErrorKind CtFlavor TcType TcType + +data ErrorKind + = MisMatchError | OccCheckError | KindError + +instance Outputable FrozenError where + ppr (FrozenError _frknd fl ty1 ty2) = ppr fl <+> pprEq ty1 ty2 <+> text "(frozen)" + +\end{code} + +Note [Frozen Errors] +~~~~~~~~~~~~~~~~~~~~ +Some of the errors that we get during canonicalization are best reported when all constraints +have been simplified as much as possible. For instance, assume that during simplification +the following constraints arise: + + [Wanted] F alpha ~ uf1 + [Wanted] beta ~ uf1 beta + +When canonicalizing the wanted (beta ~ uf1 beta), if we eagerly fail we will simply +see a message: + 'Can't construct the infinite type beta ~ uf1 beta' +and the user has no idea what the uf1 variable is. + +Instead our plan is that we will NOT fail immediately, but: + (1) Record the "frozen" error in the tcs_errors field + (2) Isolate the offending constraint from the rest of the inerts + (3) Keep on simplifying/canonicalizing + +At the end, we will hopefully have substituted uf1 := F alpha, and we will be able to +report a more informative error: + 'Can't construct the infinite type beta ~ F alpha beta' +\begin{code} + data SimplContext = SimplInfer -- Inferring type of a let-bound thing | SimplRuleLhs -- Inferring type of a RULE lhs @@ -412,53 +523,68 @@ 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) + -> TcM (a, Bag FrozenError, 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 + ; err_ref <- TcM.newTcRef emptyBag ; let env = TcSEnv { tcs_ev_binds = ev_binds_var , tcs_ty_binds = ty_binds_var - , tcs_context = context } + , tcs_context = context + , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet + , tcs_errors = err_ref + } -- 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 - ; return (res, evBindMapBinds ev_binds) } + ; frozen_errors <- TcM.readTcRef err_ref + ; ev_binds <- TcM.readTcRef evb_ref + ; return (res, frozen_errors, evBindMapBinds ev_binds) } where do_unification (tv,ty) = TcM.writeMetaTyVar tv ty - -nestImplicTcS :: EvBindsVar -> TcTyVarSet -> TcS a -> TcS a -nestImplicTcS ref untouch tcs - = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } -> + +nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a +nestImplicTcS ref untch (TcS thing_inside) + = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, + tcs_context = ctxt, + tcs_errors = err_ref } -> let nest_env = TcSEnv { tcs_ev_binds = ref , tcs_ty_binds = ty_binds - , tcs_context = ctxtUnderImplic ctxt } + , tcs_untch = untch + , tcs_context = ctxtUnderImplic ctxt + , tcs_errors = err_ref } 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 + ; err_ref <- TcM.newTcRef emptyBag ; let env1 = env { tcs_ev_binds = ev_binds_var - , tcs_ty_binds = ty_binds_var } - ; TcM.setUntouchables untch (unTcS tcs env1) }) + , tcs_ty_binds = ty_binds_var + , tcs_errors = err_ref } + ; unTcS tcs env1 }) -- Update TcEvBinds -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -472,9 +598,23 @@ getTcSContext = TcS (return . tcs_context) getTcEvBinds :: TcS EvBindsVar getTcEvBinds = TcS (return . tcs_ev_binds) -getTcSTyBinds :: TcS (IORef (Bag (TcTyVar, TcType))) +getUntouchables :: TcS TcsUntouchables +getUntouchables = TcS (return . tcs_untch) + +getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType))) getTcSTyBinds = TcS (return . tcs_ty_binds) +getTcSErrors :: TcS (IORef (Bag FrozenError)) +getTcSErrors = TcS (return . tcs_errors) + +getTcSErrorsBag :: TcS (Bag FrozenError) +getTcSErrorsBag = do { err_ref <- getTcSErrors + ; wrapTcS $ TcM.readTcRef err_ref } + +getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType)) +getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) + + getTcEvBindsBag :: TcS EvBindMap getTcEvBindsBag = do { EvBindsVar ev_ref _ <- getTcEvBinds @@ -491,11 +631,18 @@ setDerivedCoBind cv 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 - ; TcM.writeTcRef ref (ty_binds `snocBag` (tv,ty)) } } +#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 () setIPBind = setEvBind @@ -523,6 +670,25 @@ getDefaultInfo ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt)) ; return (ctxt, tys, flags) } + + +-- Recording errors in the TcS monad +-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +addErrorTcS :: ErrorKind -> CtFlavor -> TcType -> TcType -> TcS () +addErrorTcS frknd fl ty1 ty2 + = do { err_ref <- getTcSErrors + ; wrapTcS $ do + { TcM.updTcRef err_ref $ \ errs -> + consBag (FrozenError frknd fl ty1 ty2) errs + + -- If there's an error in the *given* constraints, + -- stop right now, to avoid a cascade of errors + -- in the wanteds + ; when (isGiven fl) TcM.failM + + ; return () } } + -- Just get some environments needed for instance looking up and matching -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -538,9 +704,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] -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -557,61 +720,102 @@ 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 :: 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 --- 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) - } +\end{code} -zonkFlattenedType :: TcType -> TcS TcType -zonkFlattenedType ty = wrapTcS (TcM.zonkTcType ty) +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. -{-- -tyVarsOfUnflattenedType :: TcType -> TcTyVarSet --- A version of tyVarsOfType which looks through flatSkols -tyVarsOfUnflattenedType ty - = foldVarSet (unionVarSet . do_tv) emptyVarSet (tyVarsOfType ty) - where - do_tv :: TyVar -> TcTyVarSet - do_tv tv = ASSERT( isTcTyVar tv) - case tcTyVarDetails tv of - FlatSkol _ ty -> tyVarsOfUnflattenedType ty - _ -> unitVarSet tv ---} +\begin{code} +-- Flatten skolems +-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +newFlattenSkolemTy :: TcType -> TcS TcType +newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty +newFlattenSkolemTyVar :: TcType -> TcS TcTyVar +newFlattenSkolemTyVar ty + = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique + ; let name = mkSysTvName uniq (fsLit "f") + ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } + ; traceTcS "New Flatten Skolem Born" $ + (ppr tv <+> text "[:= " <+> ppr ty <+> text "]") + ; return tv } -- 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 <$> instFlexiTcS tv + inst_tv (Right ty) = return ty instDFunConstraints :: TcThetaType -> TcS [EvVar] instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds +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 = mkSysTvName 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 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -634,8 +838,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 @@ -649,7 +851,7 @@ newDictVar cl tys = wrapTcS $ TcM.newDict cl tys \begin{code} -isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool +isGoodRecEv :: EvVar -> EvVar -> 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 @@ -664,7 +866,7 @@ isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool -- call (constructor) and -1 for every superclass selection (destructor). -- -- See Note [Superclasses and recursive dictionaries] in TcInteract -isGoodRecEv ev_var (WantedEvVar wv _) +isGoodRecEv ev_var wv = do { tc_evbinds <- getTcEvBindsBag ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var ; return $ case mb of @@ -684,16 +886,7 @@ isGoodRecEv ev_var (WantedEvVar wv _) | 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 + | otherwise = return Nothing chase_ev assocs trg curr_grav visited (EvId v) = chase_ev_var assocs trg curr_grav visited v @@ -706,9 +899,11 @@ isGoodRecEv ev_var (WantedEvVar wv _) 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_ev assocs trg curr_grav visited (EvDFunApp _ _ _ev_vars ev_deps) + = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_deps + -- Notice that we chase the ev_deps and not the ev_vars + -- See Note [Dependencies in self dictionaries] in TcSimplify + ; return (comb_chase_res Nothing chase_results) } chase_co assocs trg curr_grav visited co = -- Look for all the coercion variables in the coercion @@ -754,8 +949,7 @@ matchClass clas tys text "witness" <+> ppr 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" @@ -766,26 +960,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 @@ -801,7 +977,8 @@ matchFam tycon args -- Functional dependencies, instantiation of equations ------------------------------------------------------- -mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))] +mkWantedFunDepEqns :: WantedLoc + -> [(Equation, (PredType, SDoc), (PredType, SDoc))] -> TcS [WantedEvVar] mkWantedFunDepEqns _ [] = return [] mkWantedFunDepEqns loc eqns @@ -810,16 +987,32 @@ mkWantedFunDepEqns loc eqns ; return $ concat wevvars } 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_one tenv (ty1, ty2) = do { let sty1 = substTy tenv ty1 - sty2 = substTy tenv ty2 - ; ev <- newWantedCoVar sty1 sty2 - ; return (WantedEvVar ev loc) } + to_work_item ((qtvs, pairs), d1, d2) + = do { let tvs = varSetElems qtvs + ; tvs' <- mapM instFlexiTcS tvs + ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs') + loc' = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc + ; mapM (do_one subst loc') pairs } + + do_one subst loc' (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)] + +mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv + -> TcM (TidyEnv, SDoc) +mkEqnMsg (pred1,from1) (pred2,from2) tidy_env + = do { pred1' <- TcM.zonkTcPredType pred1 + ; pred2' <- TcM.zonkTcPredType pred2 + ; let { pred1'' = tidyPred tidy_env pred1' + ; pred2'' = tidyPred tidy_env pred2' } + ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"), + nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]), + nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])] + ; return (tidy_env, msg) } \end{code}