diff options
Diffstat (limited to 'compiler/GHC/Tc/Solver/Monad.hs')
| -rw-r--r-- | compiler/GHC/Tc/Solver/Monad.hs | 696 |
1 files changed, 163 insertions, 533 deletions
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index 2cd004053d..9f75491dd0 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -3,6 +3,7 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ViewPatterns #-} @@ -13,8 +14,9 @@ module GHC.Tc.Solver.Monad ( -- The TcS monad - TcS, runTcS, runTcSDeriveds, runTcSDerivedsEarlyAbort, runTcSWithEvBinds, - runTcSInerts, failTcS, warnTcS, addErrTcS, wrapTcS, runTcSEqualities, + TcS, runTcS, runTcSEarlyAbort, runTcSWithEvBinds, runTcSInerts, + failTcS, warnTcS, addErrTcS, wrapTcS, + runTcSEqualities, nestTcS, nestImplicTcS, setEvBindsTcS, emitImplicationTcS, emitTvImplicationTcS, @@ -38,16 +40,14 @@ module GHC.Tc.Solver.Monad ( MaybeNew(..), freshGoals, isFresh, getEvExpr, newTcEvBinds, newNoTcEvBinds, - newWantedEq, newWantedEq_SI, emitNewWantedEq, - newWanted, newWanted_SI, newWantedEvVar, + newWantedEq, emitNewWantedEq, + newWanted, newWantedNC, newWantedEvVarNC, - newDerivedNC, newBoundEvVarId, unifyTyVar, reportUnifications, touchabilityTest, TouchabilityTestResult(..), setEvBind, setWantedEq, setWantedEvTerm, setEvBindIfWanted, newEvVar, newGivenEvVar, newGivenEvVars, - emitNewDeriveds, emitNewDerivedEq, checkReductionDepth, getSolvedDicts, setSolvedDicts, @@ -67,7 +67,6 @@ module GHC.Tc.Solver.Monad ( removeInertCts, getPendingGivenScs, addInertCan, insertFunEq, addInertForAll, emitWorkNC, emitWork, - isImprovable, lookupInertDict, -- The Model @@ -130,7 +129,8 @@ import qualified GHC.Tc.Utils.Monad as TcM import qualified GHC.Tc.Utils.TcMType as TcM import qualified GHC.Tc.Instance.Class as TcM( matchGlobalInst, ClsInstResult(..) ) import qualified GHC.Tc.Utils.Env as TcM - ( checkWellStaged, tcGetDefaultTys, tcLookupClass, tcLookupId, topIdLvl ) + ( checkWellStaged, tcGetDefaultTys, tcLookupClass, tcLookupId, topIdLvl + , tcInitTidyEnv ) import GHC.Tc.Instance.Class( InstanceWhat(..), safeOverlap, instanceReturnsDictCon ) import GHC.Tc.Utils.TcType import GHC.Driver.Session @@ -145,8 +145,8 @@ import GHC.Tc.Solver.InertSet import GHC.Tc.Types.Evidence import GHC.Core.Class import GHC.Core.TyCon -import GHC.Tc.Errors ( solverDepthErrorTcS ) import GHC.Tc.Errors.Types +import GHC.Types.Error ( mkPlainError, noHints ) import GHC.Types.Name import GHC.Types.TyThing @@ -167,15 +167,14 @@ import GHC.Tc.Types.Origin import GHC.Tc.Types.Constraint import GHC.Tc.Utils.Unify import GHC.Core.Predicate - -import GHC.Types.Unique.Set +import GHC.Types.Unique.Set (nonDetEltsUniqSet) +import GHC.Utils.Panic.Plain import Control.Monad import GHC.Utils.Monad import Data.IORef import GHC.Exts (oneShot) -import Data.List ( mapAccumL, partition ) -import Data.List.NonEmpty ( NonEmpty(..) ) +import Data.List ( mapAccumL, partition, find ) #if defined(DEBUG) import GHC.Data.Graph.Directed @@ -183,358 +182,6 @@ import GHC.Data.Graph.Directed {- ********************************************************************* * * - Shadow constraints and improvement -* * -************************************************************************ - -Note [The improvement story and derived shadows] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Because Wanteds cannot rewrite Wanteds (see Note [Wanteds do not -rewrite Wanteds] in GHC.Tc.Types.Constraint), we may miss some opportunities for -solving. Here's a classic example (indexed-types/should_fail/T4093a) - - Ambiguity check for f: (Foo e ~ Maybe e) => Foo e - - We get [G] Foo e ~ Maybe e (CEqCan) - [W] Foo ee ~ Foo e (CEqCan) -- ee is a unification variable - [W] Foo ee ~ Maybe ee (CEqCan) - - The first Wanted gets rewritten to - - [W] Foo ee ~ Maybe e - - But now we appear to be stuck, since we don't rewrite Wanteds with - Wanteds. This is silly because we can see that ee := e is the - only solution. - -The basic plan is - * generate Derived constraints that shadow Wanted constraints - * allow Derived to rewrite Derived - * in order to cause some unifications to take place - * that in turn solve the original Wanteds - -The ONLY reason for all these Derived equalities is to tell us how to -unify a variable: that is, what Mark Jones calls "improvement". - -The same idea is sometimes also called "saturation"; find all the -equalities that must hold in any solution. - -Or, equivalently, you can think of the derived shadows as implementing -the "model": a non-idempotent but no-occurs-check substitution, -reflecting *all* *Nominal* equalities (a ~N ty) that are not -immediately soluble by unification. - -More specifically, here's how it works (Oct 16): - -* Wanted constraints are born as [WD]; this behaves like a - [W] and a [D] paired together. - -* When we are about to add a [WD] to the inert set, if it can - be rewritten by a [D] a ~ ty, then we split it into [W] and [D], - putting the latter into the work list (see maybeEmitShadow). - -In the example above, we get to the point where we are stuck: - [WD] Foo ee ~ Foo e - [WD] Foo ee ~ Maybe ee - -But now when [WD] Foo ee ~ Maybe ee is about to be added, we'll -split it into [W] and [D], since the inert [WD] Foo ee ~ Foo e -can rewrite it. Then: - work item: [D] Foo ee ~ Maybe ee - inert: [W] Foo ee ~ Maybe ee - [WD] Foo ee ~ Maybe e - -See Note [Splitting WD constraints]. Now the work item is rewritten -by the [WD] and we soon get ee := e. - -Additional notes: - - * The derived shadow equalities live in inert_eqs, along with - the Givens and Wanteds; see Note [EqualCtList invariants] - in GHC.Tc.Solver.Types. - - * We make Derived shadows only for Wanteds, not Givens. So we - have only [G], not [GD] and [G] plus splitting. See - Note [Add derived shadows only for Wanteds] - - * We also get Derived equalities from functional dependencies - and type-function injectivity; see calls to unifyDerived. - - * It's worth having [WD] rather than just [W] and [D] because - * efficiency: silly to process the same thing twice - * inert_dicts is a finite map keyed by - the type; it's inconvenient for it to map to TWO constraints - -Another example requiring Deriveds is in -Note [Put touchable variables on the left] in GHC.Tc.Solver.Canonical. - -Note [Splitting WD constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We are about to add a [WD] constraint to the inert set; and we -know that the inert set has fully rewritten it. Should we split -it into [W] and [D], and put the [D] in the work list for further -work? - -* CDictCan (C tys): - Yes if the inert set could rewrite tys to make the class constraint, - or type family, fire. That is, yes if the inert_eqs intersects - with the free vars of tys. For this test we use - (anyRewritableTyVar True) which ignores casts and coercions in tys, - because rewriting the casts or coercions won't make the thing fire - more often. - -* CEqCan (lhs ~ ty): Yes if the inert set could rewrite 'lhs' or 'ty'. - We need to check both 'lhs' and 'ty' against the inert set: - - Inert set contains [D] a ~ ty2 - Then we want to put [D] a ~ ty in the worklist, so we'll - get [D] ty ~ ty2 with consequent good things - - - Inert set contains [D] b ~ a, where b is in ty. - We can't just add [WD] a ~ ty[b] to the inert set, because - that breaks the inert-set invariants. If we tried to - canonicalise another [D] constraint mentioning 'a', we'd - get an infinite loop - - Moreover we must use (anyRewritableTyVar False) for the RHS, - because even tyvars in the casts and coercions could give - an infinite loop if we don't expose it - -* CIrredCan: Yes if the inert set can rewrite the constraint. - We used to think splitting irreds was unnecessary, but - see Note [Splitting Irred WD constraints] - -* Others: nothing is gained by splitting. - -Note [Splitting Irred WD constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Splitting Irred constraints can make a difference. Here is the -scenario: - - a[sk] :: F v -- F is a type family - beta :: alpha - - work item: [WD] a ~ beta - -This is heterogeneous, so we emit a kind equality and make the work item an -inert Irred. - - work item: [D] F v ~ alpha - inert: [WD] (a |> co) ~ beta (CIrredCan) - -Can't make progress on the work item. Add to inert set. This kicks out the -old inert, because a [D] can rewrite a [WD]. - - work item: [WD] (a |> co) ~ beta - inert: [D] F v ~ alpha (CEqCan) - -Can't make progress on this work item either (although GHC tries by -decomposing the cast and rewriting... but that doesn't make a difference), -which is still hetero. Emit a new kind equality and add to inert set. But, -critically, we split the Irred. - - work list: - [D] F v ~ alpha (CEqCan) - [D] (a |> co) ~ beta (CIrred) -- this one was split off - inert: - [W] (a |> co) ~ beta - [D] F v ~ alpha - -We quickly solve the first work item, as it's the same as an inert. - - work item: [D] (a |> co) ~ beta - inert: - [W] (a |> co) ~ beta - [D] F v ~ alpha - -We decompose the cast, yielding - - [D] a ~ beta - -We then rewrite the kinds. The lhs kind is F v, which flattens to alpha. - - co' :: F v ~ alpha - [D] (a |> co') ~ beta - -Now this equality is homo-kinded. So we swizzle it around to - - [D] beta ~ (a |> co') - -and set beta := a |> co', and go home happy. - -If we don't split the Irreds, we loop. This is all dangerously subtle. - -This is triggered by test case typecheck/should_compile/SplitWD. - -Note [Add derived shadows only for Wanteds] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We only add shadows for Wanted constraints. That is, we have -[WD] but not [GD]; and maybeEmitShaodw looks only at [WD] -constraints. - -It does just possibly make sense ot add a derived shadow for a -Given. If we created a Derived shadow of a Given, it could be -rewritten by other Deriveds, and that could, conceivably, lead to a -useful unification. - -But (a) I have been unable to come up with an example of this - happening - (b) see #12660 for how adding the derived shadows - of a Given led to an infinite loop. - (c) It's unlikely that rewriting derived Givens will lead - to a unification because Givens don't mention touchable - unification variables - -For (b) there may be other ways to solve the loop, but simply -reraining from adding derived shadows of Givens is particularly -simple. And it's more efficient too! - -Still, here's one possible reason for adding derived shadows -for Givens. Consider - work-item [G] a ~ [b], inerts has [D] b ~ a. -If we added the derived shadow (into the work list) - [D] a ~ [b] -When we process it, we'll rewrite to a ~ [a] and get an -occurs check. Without it we'll miss the occurs check (reporting -inaccessible code); but that's probably OK. - -Note [Keep CDictCan shadows as CDictCan] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we have - class C a => D a b -and [G] D a b, [G] C a in the inert set. Now we insert -[D] b ~ c. We want to kick out a derived shadow for [D] D a b, -so we can rewrite it with the new constraint, and perhaps get -instance reduction or other consequences. - -BUT we do not want to kick out a *non-canonical* (D a b). If we -did, we would do this: - - rewrite it to [D] D a c, with pend_sc = True - - use expandSuperClasses to add C a - - go round again, which solves C a from the givens -This loop goes on for ever and triggers the simpl_loop limit. - -Solution: kick out the CDictCan which will have pend_sc = False, -because we've already added its superclasses. So we won't re-add -them. If we forget the pend_sc flag, our cunning scheme for avoiding -generating superclasses repeatedly will fail. - -See #11379 for a case of this. - -Note [Do not do improvement for WOnly] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We do improvement between two constraints (e.g. for injectivity -or functional dependencies) only if both are "improvable". And -we improve a constraint wrt the top-level instances only if -it is improvable. - -Improvable: [G] [WD] [D} -Not improvable: [W] - -Reasons: - -* It's less work: fewer pairs to compare - -* Every [W] has a shadow [D] so nothing is lost - -* Consider [WD] C Int b, where 'b' is a skolem, and - class C a b | a -> b - instance C Int Bool - We'll do a fundep on it and emit [D] b ~ Bool - That will kick out constraint [WD] C Int b - Then we'll split it to [W] C Int b (keep in inert) - and [D] C Int b (in work list) - When processing the latter we'll rewrite it to - [D] C Int Bool - At that point it would be /stupid/ to interact it - with the inert [W] C Int b in the inert set; after all, - it's the very constraint from which the [D] C Int Bool - was split! We can avoid this by not doing improvement - on [W] constraints. This came up in #12860. --} - -maybeEmitShadow :: InertCans -> Ct -> TcS Ct --- See Note [The improvement story and derived shadows] -maybeEmitShadow ics ct - | let ev = ctEvidence ct - , CtWanted { ctev_pred = pred, ctev_loc = loc - , ctev_nosh = WDeriv } <- ev - , shouldSplitWD (inert_eqs ics) (inert_funeqs ics) ct - = do { traceTcS "Emit derived shadow" (ppr ct) - ; let derived_ev = CtDerived { ctev_pred = pred - , ctev_loc = loc } - shadow_ct = ct { cc_ev = derived_ev } - -- Te shadow constraint keeps the canonical shape. - -- This just saves work, but is sometimes important; - -- see Note [Keep CDictCan shadows as CDictCan] - ; emitWork [shadow_ct] - - ; let ev' = ev { ctev_nosh = WOnly } - ct' = ct { cc_ev = ev' } - -- Record that it now has a shadow - -- This is /the/ place we set the flag to WOnly - ; return ct' } - - | otherwise - = return ct - -shouldSplitWD :: InertEqs -> FunEqMap EqualCtList -> Ct -> Bool --- Precondition: 'ct' is [WD], and is inert --- True <=> we should split ct ito [W] and [D] because --- the inert_eqs can make progress on the [D] --- See Note [Splitting WD constraints] - -shouldSplitWD inert_eqs fun_eqs (CDictCan { cc_tyargs = tys }) - = should_split_match_args inert_eqs fun_eqs tys - -- NB True: ignore coercions - -- See Note [Splitting WD constraints] - -shouldSplitWD inert_eqs fun_eqs (CEqCan { cc_lhs = TyVarLHS tv, cc_rhs = ty - , cc_eq_rel = eq_rel }) - = tv `elemDVarEnv` inert_eqs - || anyRewritableCanEqLHS eq_rel (canRewriteTv inert_eqs) (canRewriteTyFam fun_eqs) ty - -- NB False: do not ignore casts and coercions - -- See Note [Splitting WD constraints] - -shouldSplitWD inert_eqs fun_eqs (CEqCan { cc_ev = ev, cc_eq_rel = eq_rel }) - = anyRewritableCanEqLHS eq_rel (canRewriteTv inert_eqs) (canRewriteTyFam fun_eqs) - (ctEvPred ev) - -shouldSplitWD inert_eqs fun_eqs (CIrredCan { cc_ev = ev }) - = anyRewritableCanEqLHS (ctEvEqRel ev) (canRewriteTv inert_eqs) - (canRewriteTyFam fun_eqs) (ctEvPred ev) - -shouldSplitWD _ _ _ = False -- No point in splitting otherwise - -should_split_match_args :: InertEqs -> FunEqMap EqualCtList -> [TcType] -> Bool --- True if the inert_eqs can rewrite anything in the argument types -should_split_match_args inert_eqs fun_eqs tys - = any (anyRewritableCanEqLHS NomEq (canRewriteTv inert_eqs) (canRewriteTyFam fun_eqs)) tys - -- See Note [Splitting WD constraints] - -canRewriteTv :: InertEqs -> EqRel -> TyVar -> Bool -canRewriteTv inert_eqs eq_rel tv - | Just (EqualCtList (ct :| _)) <- lookupDVarEnv inert_eqs tv - , CEqCan { cc_eq_rel = eq_rel1 } <- ct - = eq_rel1 `eqCanRewrite` eq_rel - | otherwise - = False - -canRewriteTyFam :: FunEqMap EqualCtList -> EqRel -> TyCon -> [Type] -> Bool -canRewriteTyFam fun_eqs eq_rel tf args - | Just (EqualCtList (ct :| _)) <- findFunEq fun_eqs tf args - , CEqCan { cc_eq_rel = eq_rel1 } <- ct - = eq_rel1 `eqCanRewrite` eq_rel - | otherwise - = False - -isImprovable :: CtEvidence -> Bool --- See Note [Do not do improvement for WOnly] -isImprovable (CtWanted { ctev_nosh = WOnly }) = False -isImprovable _ = True - - -{- ********************************************************************* -* * Inert instances: inert_insts * * ********************************************************************* -} @@ -601,14 +248,28 @@ Note [Adding an equality to the InertCans] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When adding an equality to the inerts: -* Split [WD] into [W] and [D] if the inerts can rewrite the latter; - done by maybeEmitShadow. - * Kick out any constraints that can be rewritten by the thing we are adding. Done by kickOutRewritable. * Note that unifying a:=ty, is like adding [G] a~ty; just use kickOutRewritable with Nominal, Given. See kickOutAfterUnification. + +Note [Kick out existing binding for implicit parameter] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have (typecheck/should_compile/ImplicitParamFDs) + flub :: (?x :: Int) => (Int, Integer) + flub = (?x, let ?x = 5 in ?x) +When we are checking the last ?x occurrence, we guess its type +to be a fresh unification variable alpha and emit an (IP "x" alpha) +constraint. But the given (?x :: Int) has been translated to an +IP "x" Int constraint, which has a functional dependency from the +name to the type. So fundep interaction tells us that alpha ~ Int, +and we get a type error. This is bad. + +Instead, we wish to excise any old given for an IP when adding a +new one. We also must make sure not to float out +any IP constraints outside an implication that binds an IP of +the same name; see GHC.Tc.Solver.floatConstraints. -} addInertCan :: Ct -> TcS () @@ -620,7 +281,6 @@ addInertCan ct = ; mkTcS (\TcSEnv{tcs_abort_on_insoluble=abort_flag} -> when (abort_flag && insolubleEqCt ct) TcM.failM) ; ics <- getInertCans - ; ct <- maybeEmitShadow ics ct ; ics <- maybeKickOut ics ct ; tclvl <- getTcLevel ; setInertCans (addInertItem tclvl ics ct) @@ -633,6 +293,27 @@ maybeKickOut ics ct | CEqCan { cc_lhs = lhs, cc_ev = ev, cc_eq_rel = eq_rel } <- ct = do { (_, ics') <- kickOutRewritable (ctEvFlavour ev, eq_rel) lhs ics ; return ics' } + + -- See [Kick out existing binding for implicit parameter] + | isGivenCt ct + , CDictCan { cc_class = cls, cc_tyargs = [ip_name_strty, _ip_ty] } <- ct + , isIPClass cls + , Just ip_name <- isStrLitTy ip_name_strty + -- Would this be more efficient if we used findDictsByClass and then delDict? + = let dict_map = inert_dicts ics + dict_map' = filterDicts doesn't_match_ip_name dict_map + + doesn't_match_ip_name :: Ct -> Bool + doesn't_match_ip_name ct + | Just (inert_ip_name, _inert_ip_ty) <- isIPPred_maybe (ctPred ct) + = inert_ip_name /= ip_name + + | otherwise + = True + + in + return (ics { inert_dicts = dict_map' }) + | otherwise = return ics @@ -682,8 +363,10 @@ kickOutAfterUnification new_tv ; return n_kicked } -- See Wrinkle (2) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical -kickOutAfterFillingCoercionHole :: CoercionHole -> Coercion -> TcS () -kickOutAfterFillingCoercionHole hole filled_co +-- It's possible that this could just go ahead and unify, but could there be occurs-check +-- problems? Seems simpler just to kick out. +kickOutAfterFillingCoercionHole :: CoercionHole -> TcS () +kickOutAfterFillingCoercionHole hole = do { ics <- getInertCans ; let (kicked_out, ics') = kick_out ics n_kicked = workListSize kicked_out @@ -698,39 +381,25 @@ kickOutAfterFillingCoercionHole hole filled_co ; setInertCans ics' } where - holes_of_co = coercionHolesOfCo filled_co - kick_out :: InertCans -> (WorkList, InertCans) - kick_out ics@(IC { inert_blocked = blocked }) - = let (to_kick, to_keep) = partitionBagWith kick_ct blocked - - kicked_out = extendWorkListCts (bagToList to_kick) emptyWorkList - ics' = ics { inert_blocked = to_keep } - in - (kicked_out, ics') - - kick_ct :: Ct -> Either Ct Ct - -- Left: kick out; Right: keep. But even if we keep, we may need - -- to update the set of blocking holes - kick_ct ct@(CIrredCan { cc_reason = HoleBlockerReason holes }) - | hole `elementOfUniqSet` holes - = let new_holes = holes `delOneFromUniqSet` hole - `unionUniqSets` holes_of_co - updated_ct = ct { cc_reason = HoleBlockerReason new_holes } - in - if isEmptyUniqSet new_holes - then Left updated_ct - else Right updated_ct - - | otherwise - = Right ct - - kick_ct other = pprPanic "kickOutAfterFillingCoercionHole" (ppr other) + kick_out ics@(IC { inert_eqs = eqs, inert_funeqs = funeqs }) + = (kicked_out, ics { inert_eqs = eqs_to_keep, inert_funeqs = funeqs_to_keep }) + where + (eqs_to_kick, eqs_to_keep) = partitionInertEqs kick_ct eqs + (funeqs_to_kick, funeqs_to_keep) = partitionFunEqs kick_ct funeqs + kicked_out = extendWorkListCts (eqs_to_kick ++ funeqs_to_kick) emptyWorkList + + kick_ct :: Ct -> Bool + -- True: kick out; False: keep. + kick_ct (CEqCan { cc_rhs = rhs, cc_ev = ctev }) + = isWanted ctev && -- optimisation: givens don't have coercion holes anyway + rhs `hasThisCoercionHoleTy` hole + kick_ct other = pprPanic "kick_ct (coercion hole)" (ppr other) -------------- addInertSafehask :: InertCans -> Ct -> InertCans addInertSafehask ics item@(CDictCan { cc_class = cls, cc_tyargs = tys }) - = ics { inert_safehask = addDictCt (inert_dicts ics) (classTyCon cls) tys item } + = ics { inert_safehask = addDict (inert_dicts ics) cls tys item } addInertSafehask _ item = pprPanic "addInertSafehask: can't happen! Inserting " $ ppr item @@ -816,7 +485,7 @@ updInertIrreds :: (Cts -> Cts) -> TcS () updInertIrreds upd_fn = updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) } -getInertEqs :: TcS (DTyVarEnv EqualCtList) +getInertEqs :: TcS InertEqs getInertEqs = do { inert <- getInertCans; return (inert_eqs inert) } getInnermostGivenEqLevel :: TcS TcLevel @@ -840,9 +509,8 @@ getInertGivens :: TcS [Ct] getInertGivens = do { inerts <- getInertCans ; let all_cts = foldDicts (:) (inert_dicts inerts) - $ foldFunEqs (\ecl out -> equalCtListToList ecl ++ out) - (inert_funeqs inerts) - $ concatMap equalCtListToList (dVarEnvElts (inert_eqs inerts)) + $ foldFunEqs (++) (inert_funeqs inerts) + $ foldDVarEnv (++) [] (inert_eqs inerts) ; return (filter isGivenCt all_cts) } getPendingGivenScs :: TcS [Ct] @@ -878,7 +546,7 @@ get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts }) add :: Ct -> DictMap Ct -> DictMap Ct add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts - = addDictCt dicts (classTyCon cls) tys ct + = addDict dicts cls tys ct add ct _ = pprPanic "getPendingScDicts" (ppr ct) get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst) @@ -895,27 +563,24 @@ get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts }) getUnsolvedInerts :: TcS ( Bag Implication , Cts ) -- All simple constraints --- Return all the unsolved [Wanted] or [Derived] constraints +-- Return all the unsolved [Wanted] constraints -- -- Post-condition: the returned simple constraints are all fully zonked -- (because they come from the inert set) -- the unsolved implics may not be getUnsolvedInerts - = do { IC { inert_eqs = tv_eqs - , inert_funeqs = fun_eqs - , inert_irreds = irreds - , inert_blocked = blocked - , inert_dicts = idicts + = do { IC { inert_eqs = tv_eqs + , inert_funeqs = fun_eqs + , inert_irreds = irreds + , inert_dicts = idicts } <- getInertCans - ; let unsolved_tv_eqs = foldTyEqs add_if_unsolved tv_eqs emptyCts - unsolved_fun_eqs = foldFunEqs add_if_unsolveds fun_eqs emptyCts - unsolved_irreds = Bag.filterBag is_unsolved irreds - unsolved_blocked = blocked -- all blocked equalities are W/D - unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts - unsolved_others = unionManyBags [ unsolved_irreds - , unsolved_dicts - , unsolved_blocked ] + ; let unsolved_tv_eqs = foldTyEqs add_if_unsolved tv_eqs emptyCts + unsolved_fun_eqs = foldFunEqs add_if_unsolveds fun_eqs emptyCts + unsolved_irreds = Bag.filterBag isWantedCt irreds + unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts + unsolved_others = unionManyBags [ unsolved_irreds + , unsolved_dicts ] ; implics <- getWorkListImplics @@ -930,14 +595,11 @@ getUnsolvedInerts unsolved_others) } where add_if_unsolved :: Ct -> Cts -> Cts - add_if_unsolved ct cts | is_unsolved ct = ct `consCts` cts - | otherwise = cts + add_if_unsolved ct cts | isWantedCt ct = ct `consCts` cts + | otherwise = cts add_if_unsolveds :: EqualCtList -> Cts -> Cts - add_if_unsolveds new_cts old_cts = foldr add_if_unsolved old_cts - (equalCtListToList new_cts) - - is_unsolved ct = not (isGivenCt ct) -- Wanted or Derived + add_if_unsolveds new_cts old_cts = foldr add_if_unsolved old_cts new_cts getHasGivenEqs :: TcLevel -- TcLevel of this implication -> TcS ( HasGivenEqs -- are there Given equalities? @@ -970,15 +632,8 @@ getHasGivenEqs tclvl insoluble_given_equality ct = insolubleEqCt ct && isGivenCt ct -{- Note [Unsolved Derived equalities] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -In getUnsolvedInerts, we return a derived equality from the inert_eqs -because it is a candidate for floating out of this implication. We -only float equalities with a meta-tyvar on the left, so we only pull -those out here. - -Note [What might equal later?] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [What might equal later?] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We must determine whether a Given might later equal a Wanted. We definitely need to account for the possibility that any metavariable might be arbitrarily instantiated. Yet we do *not* want @@ -1084,16 +739,17 @@ removeInertCt is ct = pprPanic "removeInertCt" (ppr "CSpecialCan" <+> parens (ppr special_pred)) -- | Looks up a family application in the inerts. -lookupFamAppInert :: TyCon -> [Type] -> TcS (Maybe (Reduction, CtFlavourRole)) -lookupFamAppInert fam_tc tys +lookupFamAppInert :: (CtFlavourRole -> Bool) -- can it rewrite the target? + -> TyCon -> [Type] -> TcS (Maybe (Reduction, CtFlavourRole)) +lookupFamAppInert rewrite_pred fam_tc tys = do { IS { inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts ; return (lookup_inerts inert_funeqs) } where lookup_inerts inert_funeqs - | Just (EqualCtList (CEqCan { cc_ev = ctev, cc_rhs = rhs } :| _)) - <- findFunEq inert_funeqs fam_tc tys - = Just (mkReduction (ctEvCoercion ctev) rhs - ,ctEvFlavourRole ctev) + | Just ecl <- findFunEq inert_funeqs fam_tc tys + , Just (CEqCan { cc_ev = ctev, cc_rhs = rhs }) + <- find (rewrite_pred . ctFlavourRole) ecl + = Just (mkReduction (ctEvCoercion ctev) rhs, ctEvFlavourRole ctev) | otherwise = Nothing lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence) @@ -1139,7 +795,6 @@ extendFamAppCache tc xi_args stuff@(Reduction _ ty) ; when (gopt Opt_FamAppCache dflags) $ do { traceTcS "extendFamAppCache" (vcat [ ppr tc <+> ppr xi_args , ppr ty ]) - -- 'co' can be bottom, in the case of derived items ; updInertTcS $ \ is@(IS { inert_famapp_cache = fc }) -> is { inert_famapp_cache = insertFunEq fc tc xi_args stuff } } } @@ -1330,19 +985,11 @@ runTcS tcs ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var ; return (res, ev_binds) } --- | This variant of 'runTcS' will keep solving, even when only Deriveds --- are left around. It also doesn't return any evidence, as callers won't --- need it. -runTcSDeriveds :: TcS a -> TcM a -runTcSDeriveds tcs - = do { ev_binds_var <- TcM.newTcEvBinds - ; runTcSWithEvBinds ev_binds_var tcs } - - --- | This variant of 'runTcSDeriveds' will immediatley fail upon encountering an --- insoluble ct. See Note [Speeding up valid hole-fits] -runTcSDerivedsEarlyAbort :: TcS a -> TcM a -runTcSDerivedsEarlyAbort tcs +-- | This variant of 'runTcS' will immediatley fail upon encountering an +-- insoluble ct. See Note [Speeding up valid hole-fits]. Its one usage +-- site does not need the ev_binds, so we do not return them. +runTcSEarlyAbort :: TcS a -> TcM a +runTcSEarlyAbort tcs = do { ev_binds_var <- TcM.newTcEvBinds ; runTcSWithEvBinds' True True ev_binds_var tcs } @@ -1915,7 +1562,7 @@ an example: * There's a deeply-nested chain of implication constraints. ?x:alpha => ?y1:beta1 => ... ?yn:betan => [W] ?x:Int - * From the innermost one we get a [D] alpha[1] ~ Int, + * From the innermost one we get a [W] alpha[1] ~ Int, so we can unify. * It's better not to iterate the inner implications, but go all the @@ -2082,7 +1729,7 @@ Yuk! fillCoercionHole :: CoercionHole -> Coercion -> TcS () fillCoercionHole hole co = do { wrapTcS $ TcM.fillCoercionHole hole co - ; kickOutAfterFillingCoercionHole hole co } + ; kickOutAfterFillingCoercionHole hole } setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS () setEvBindIfWanted ev tm @@ -2119,103 +1766,69 @@ newBoundEvVarId pred rhs newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence] newGivenEvVars loc pts = mapM (newGivenEvVar loc) pts -emitNewWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS Coercion +emitNewWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS Coercion -- | Emit a new Wanted equality into the work-list -emitNewWantedEq loc role ty1 ty2 - = do { (ev, co) <- newWantedEq loc role ty1 ty2 +emitNewWantedEq loc rewriters role ty1 ty2 + = do { (ev, co) <- newWantedEq loc rewriters role ty1 ty2 ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev)) ; return co } -- | Make a new equality CtEvidence -newWantedEq :: CtLoc -> Role -> TcType -> TcType +newWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS (CtEvidence, Coercion) -newWantedEq = newWantedEq_SI WDeriv - -newWantedEq_SI :: ShadowInfo -> CtLoc -> Role - -> TcType -> TcType - -> TcS (CtEvidence, Coercion) -newWantedEq_SI si loc role ty1 ty2 +newWantedEq loc rewriters role ty1 ty2 = do { hole <- wrapTcS $ TcM.newCoercionHole pty ; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty) - ; return ( CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole - , ctev_nosh = si - , ctev_loc = loc} + ; return ( CtWanted { ctev_pred = pty + , ctev_dest = HoleDest hole + , ctev_loc = loc + , ctev_rewriters = rewriters } , mkHoleCo hole ) } where pty = mkPrimEqPredRole role ty1 ty2 -- no equalities here. Use newWantedEq instead -newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence -newWantedEvVarNC = newWantedEvVarNC_SI WDeriv - -newWantedEvVarNC_SI :: ShadowInfo -> CtLoc -> TcPredType -> TcS CtEvidence +newWantedEvVarNC :: CtLoc -> RewriterSet + -> TcPredType -> TcS CtEvidence -- Don't look up in the solved/inerts; we know it's not there -newWantedEvVarNC_SI si loc pty +newWantedEvVarNC loc rewriters pty = do { new_ev <- newEvVar pty ; traceTcS "Emitting new wanted" (ppr new_ev <+> dcolon <+> ppr pty $$ pprCtLoc loc) - ; return (CtWanted { ctev_pred = pty, ctev_dest = EvVarDest new_ev - , ctev_nosh = si - , ctev_loc = loc })} - -newWantedEvVar :: CtLoc -> TcPredType -> TcS MaybeNew -newWantedEvVar = newWantedEvVar_SI WDeriv + ; return (CtWanted { ctev_pred = pty + , ctev_dest = EvVarDest new_ev + , ctev_loc = loc + , ctev_rewriters = rewriters })} -newWantedEvVar_SI :: ShadowInfo -> CtLoc -> TcPredType -> TcS MaybeNew +newWantedEvVar :: CtLoc -> RewriterSet + -> TcPredType -> TcS MaybeNew -- For anything except ClassPred, this is the same as newWantedEvVarNC -newWantedEvVar_SI si loc pty - = do { mb_ct <- lookupInInerts loc pty +newWantedEvVar loc rewriters pty + = assert (not (isHoleDestPred pty)) $ + do { mb_ct <- lookupInInerts loc pty ; case mb_ct of Just ctev - | not (isDerived ctev) -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev ; return $ Cached (ctEvExpr ctev) } - _ -> do { ctev <- newWantedEvVarNC_SI si loc pty + _ -> do { ctev <- newWantedEvVarNC loc rewriters pty ; return (Fresh ctev) } } -newWanted :: CtLoc -> PredType -> TcS MaybeNew +newWanted :: CtLoc -> RewriterSet -> PredType -> TcS MaybeNew -- Deals with both equalities and non equalities. Tries to look -- up non-equalities in the cache -newWanted = newWanted_SI WDeriv - -newWanted_SI :: ShadowInfo -> CtLoc -> PredType -> TcS MaybeNew -newWanted_SI si loc pty +newWanted loc rewriters pty | Just (role, ty1, ty2) <- getEqPredTys_maybe pty - = Fresh . fst <$> newWantedEq_SI si loc role ty1 ty2 + = Fresh . fst <$> newWantedEq loc rewriters role ty1 ty2 | otherwise - = newWantedEvVar_SI si loc pty + = newWantedEvVar loc rewriters pty -- deals with both equalities and non equalities. Doesn't do any cache lookups. -newWantedNC :: CtLoc -> PredType -> TcS CtEvidence -newWantedNC loc pty +newWantedNC :: CtLoc -> RewriterSet -> PredType -> TcS CtEvidence +newWantedNC loc rewriters pty | Just (role, ty1, ty2) <- getEqPredTys_maybe pty - = fst <$> newWantedEq loc role ty1 ty2 + = fst <$> newWantedEq loc rewriters role ty1 ty2 | otherwise - = newWantedEvVarNC loc pty - -emitNewDeriveds :: CtLoc -> [TcPredType] -> TcS () -emitNewDeriveds loc preds - | null preds - = return () - | otherwise - = do { evs <- mapM (newDerivedNC loc) preds - ; traceTcS "Emitting new deriveds" (ppr evs) - ; updWorkListTcS (extendWorkListDeriveds evs) } - -emitNewDerivedEq :: CtLoc -> Role -> TcType -> TcType -> TcS () --- Create new equality Derived and put it in the work list --- There's no caching, no lookupInInerts -emitNewDerivedEq loc role ty1 ty2 - = do { ev <- newDerivedNC loc (mkPrimEqPredRole role ty1 ty2) - ; traceTcS "Emitting new derived equality" (ppr ev $$ pprCtLoc loc) - ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev)) } - -- Very important: put in the wl_eqs - -- See Note [Prioritise equalities] in GHC.Tc.Solver.InertSet - -- (Avoiding fundep iteration) - -newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence -newDerivedNC loc pred - = return $ CtDerived { ctev_pred = pred, ctev_loc = loc } + = newWantedEvVarNC loc rewriters pty -- --------- Check done in GHC.Tc.Solver.Interact.selectNewWorkItem???? --------- -- | Checks if the depth of the given location is too much. Fails if @@ -2225,8 +1838,7 @@ checkReductionDepth :: CtLoc -> TcType -- ^ type being reduced checkReductionDepth loc ty = do { dflags <- getDynFlags ; when (subGoalDepthExceeded dflags (ctLocDepth loc)) $ - wrapErrTcS $ - solverDepthErrorTcS loc ty } + wrapErrTcS $ solverDepthError loc ty } matchFam :: TyCon -> [Type] -> TcS (Maybe ReductionN) matchFam tycon args = wrapTcS $ matchFamTcM tycon args @@ -2248,6 +1860,28 @@ matchFamTcM tycon args 2 (vcat [ text "Rewrites to:" <+> ppr ty , text "Coercion:" <+> ppr co ]) +solverDepthError :: CtLoc -> TcType -> TcM a +solverDepthError loc ty + = TcM.setCtLocM loc $ + do { ty <- TcM.zonkTcType ty + ; env0 <- TcM.tcInitTidyEnv + ; let tidy_env = tidyFreeTyCoVars env0 (tyCoVarsOfTypeList ty) + tidy_ty = tidyType tidy_env ty + msg = TcRnUnknownMessage $ mkPlainError noHints $ + vcat [ text "Reduction stack overflow; size =" <+> ppr depth + , hang (text "When simplifying the following type:") + 2 (ppr tidy_ty) + , note ] + ; TcM.failWithTcM (tidy_env, msg) } + where + depth = ctLocDepth loc + note = vcat + [ text "Use -freduction-depth=0 to disable this check" + , text "(any upper bound you could choose might fail unpredictably with" + , text " minor updates to GHC, so disabling the check is recommended if" + , text " you're sure that type checking should terminate)" ] + + {- ************************************************************************ * * @@ -2287,16 +1921,12 @@ breakTyVarCycle_maybe ev cte_result (TyVarLHS lhs_tv) rhs flavour = ctEvFlavour ev eq_rel = ctEvEqRel ev - final_check - | Given <- flavour - = return True - | ctFlavourContainsDerived flavour - = do { result <- touchabilityTest Derived lhs_tv rhs - ; return $ case result of - Untouchable -> False - _ -> True } - | otherwise - = return False + final_check = case flavour of + Given -> return True + Wanted -> do { result <- touchabilityTest Wanted lhs_tv rhs + ; return $ case result of + Untouchable -> False + _ -> True } -- This could be considerably more efficient. See Detail (5) of Note. go :: TcType -> TcS ReductionN @@ -2349,10 +1979,10 @@ breakTyVarCycle_maybe ev cte_result (TyVarLHS lhs_tv) rhs ; return $ mkReflRedn Nominal new_ty } -- Why reflexive? See Detail (4) of the Note - _derived_or_wd -> + Wanted -> do { new_tv <- wrapTcS (TcM.newFlexiTyVar fun_app_kind) ; let new_ty = mkTyVarTy new_tv - ; co <- emitNewWantedEq new_loc Nominal new_ty fun_app + ; co <- emitNewWantedEq new_loc (ctEvRewriters ev) Nominal new_ty fun_app ; return $ mkReduction (mkSymCo co) new_ty } -- See Detail (7) of the Note |