diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/GHC/Core/Class.hs | 7 | ||||
| -rw-r--r-- | compiler/GHC/Driver/Session.hs | 19 | ||||
| -rw-r--r-- | compiler/GHC/Settings/Constants.hs | 21 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver.hs | 71 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Canonical.hs | 150 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Monad.hs | 35 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Types/Constraint.hs | 85 |
7 files changed, 290 insertions, 98 deletions
diff --git a/compiler/GHC/Core/Class.hs b/compiler/GHC/Core/Class.hs index 9ad470e9da..1b46f66fca 100644 --- a/compiler/GHC/Core/Class.hs +++ b/compiler/GHC/Core/Class.hs @@ -17,8 +17,8 @@ module GHC.Core.Class ( mkClass, mkAbstractClass, classTyVars, classArity, classKey, className, classATs, classATItems, classTyCon, classMethods, classOpItems, classBigSig, classExtraBigSig, classTvsFds, classSCTheta, - classAllSelIds, classSCSelId, classSCSelIds, classMinimalDef, classHasFds, - isAbstractClass, + classHasSCs, classAllSelIds, classSCSelId, classSCSelIds, classMinimalDef, + classHasFds, isAbstractClass, ) where import GHC.Prelude @@ -295,6 +295,9 @@ classSCTheta (Class { classBody = ConcreteClass { cls_sc_theta = theta_stuff }}) = theta_stuff classSCTheta _ = [] +classHasSCs :: Class -> Bool +classHasSCs cls = not (null (classSCTheta cls)) + classTvsFds :: Class -> ([TyVar], [FunDep TyVar]) classTvsFds c = (classTyVars c, classFunDeps c) diff --git a/compiler/GHC/Driver/Session.hs b/compiler/GHC/Driver/Session.hs index 2ad09bc7c6..20fcc3f6fe 100644 --- a/compiler/GHC/Driver/Session.hs +++ b/compiler/GHC/Driver/Session.hs @@ -517,7 +517,15 @@ data DynFlags = DynFlags { reductionDepth :: IntWithInf, -- ^ Typechecker maximum stack depth solverIterations :: IntWithInf, -- ^ Number of iterations in the constraints solver -- Typically only 1 is needed - + givensFuel :: Int, -- ^ Number of layers of superclass expansion for givens + -- Should be < solverIterations + -- See Note [Expanding Recursive Superclasses and ExpansionFuel] + wantedsFuel :: Int, -- ^ Number of layers of superclass expansion for wanteds + -- Should be < givensFuel + -- See Note [Expanding Recursive Superclasses and ExpansionFuel] + qcsFuel :: Int, -- ^ Number of layers of superclass expansion for quantified constraints + -- Should be < givensFuel + -- See Note [Expanding Recursive Superclasses and ExpansionFuel] homeUnitId_ :: UnitId, -- ^ Target home unit-id homeUnitInstanceOf_ :: Maybe UnitId, -- ^ Id of the unit to instantiate homeUnitInstantiations_ :: [(ModuleName, Module)], -- ^ Module instantiations @@ -1148,6 +1156,9 @@ defaultDynFlags mySettings = mainFunIs = Nothing, reductionDepth = treatZeroAsInf mAX_REDUCTION_DEPTH, solverIterations = treatZeroAsInf mAX_SOLVER_ITERATIONS, + givensFuel = mAX_GIVENS_FUEL, + wantedsFuel = mAX_WANTEDS_FUEL, + qcsFuel = mAX_QC_FUEL, homeUnitId_ = mainUnitId, homeUnitInstanceOf_ = Nothing, @@ -2733,6 +2744,12 @@ dynamic_flags_deps = [ (intSuffix (\n d -> d { reductionDepth = treatZeroAsInf n })) , make_ord_flag defFlag "fconstraint-solver-iterations" (intSuffix (\n d -> d { solverIterations = treatZeroAsInf n })) + , make_ord_flag defFlag "fgivens-expansion-fuel" + (intSuffix (\n d -> d { givensFuel = n })) + , make_ord_flag defFlag "fwanteds-expansion-fuel" + (intSuffix (\n d -> d { wantedsFuel = n })) + , make_ord_flag defFlag "fqcs-expansion-fuel" + (intSuffix (\n d -> d { qcsFuel = n })) , (Deprecated, defFlag "fcontext-stack" (intSuffixM (\n d -> do { deprecate $ "use -freduction-depth=" ++ show n ++ " instead" diff --git a/compiler/GHC/Settings/Constants.hs b/compiler/GHC/Settings/Constants.hs index f2ceea8517..0c0e460ab6 100644 --- a/compiler/GHC/Settings/Constants.hs +++ b/compiler/GHC/Settings/Constants.hs @@ -30,6 +30,27 @@ mAX_REDUCTION_DEPTH = 200 mAX_SOLVER_ITERATIONS :: Int mAX_SOLVER_ITERATIONS = 4 +-- | In case of loopy quantified costraints constraints, +-- how many times should we allow superclass expansions +-- Should be less than mAX_SOLVER_ITERATIONS +-- See Note [Expanding Recursive Superclasses and ExpansionFuel] +mAX_QC_FUEL :: Int +mAX_QC_FUEL = 3 + +-- | In case of loopy wanted constraints, +-- how many times should we allow superclass expansions +-- Should be less than mAX_GIVENS_FUEL +-- See Note [Expanding Recursive Superclasses and ExpansionFuel] +mAX_WANTEDS_FUEL :: Int +mAX_WANTEDS_FUEL = 1 + +-- | In case of loopy given constraints, +-- how many times should we allow superclass expansions +-- Should be less than max_SOLVER_ITERATIONS +-- See Note [Expanding Recursive Superclasses and ExpansionFuel] +mAX_GIVENS_FUEL :: Int +mAX_GIVENS_FUEL = 3 + wORD64_SIZE :: Int wORD64_SIZE = 8 diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index f113820c02..81fa86aea4 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -2338,6 +2338,10 @@ maybe_simplify_again n limit unif_happened wc@(WC { wc_simple = simples }) do { new_given <- makeSuperClasses pending_given ; new_wanted <- makeSuperClasses pending_wanted ; solveSimpleGivens new_given -- Add the new Givens to the inert set + ; traceTcS "maybe_simplify_again" (vcat [ text "pending_given" <+> ppr pending_given + , text "new_given" <+> ppr new_given + , text "pending_wanted" <+> ppr pending_wanted + , text "new_wanted" <+> ppr new_wanted ]) ; simplify_loop n limit (not (null pending_given)) $ wc { wc_simple = simples1 `unionBags` listToBag new_wanted } } } -- (not (null pending_given)): see Note [Superclass iteration] @@ -2366,6 +2370,73 @@ superclasses. In that case we check whether the new Wanteds actually led to any new unifications, and iterate the implications only if so. -} +{- Note [Expanding Recursive Superclasses and ExpansionFuel] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider the class declaration (T21909) + + class C [a] => C a where + foo :: a -> Int + +and suppose during type inference we obtain an implication constraint: + + forall a. C a => C [[a]] + +To solve this implication constraint, we first expand one layer of the superclass +of Given constraints, but not for Wanted constraints. +(See Note [Eagerly expand given superclasses] and Note [Why adding superclasses can help] +in GHC.Tc.Solver.Canonical.) We thus get: + + [G] g1 :: C a + [G] g2 :: C [a] -- new superclass layer from g1 + [W] w1 :: C [[a]] + +Now, we cannot solve `w1` directly from `g1` or `g2` as we may not have +any instances for C. So we expand a layer of superclasses of each Wanteds and Givens +that we haven't expanded yet. +This is done in `maybe_simplify_again`. And we get: + + [G] g1 :: C a + [G] g2 :: C [a] + [G] g3 :: C [[a]] -- new superclass layer from g2, can solve w1 + [W] w1 :: C [[a]] + [W] w2 :: C [[[a]]] -- new superclass layer from w1, not solvable + +Now, although we can solve `w1` using `g3` (obtained from expanding `g2`), +we have a new wanted constraint `w2` (obtained from expanding `w1`) that cannot be solved. +We thus make another go at solving in `maybe_simplify_again` by expanding more +layers of superclasses. This looping is futile as Givens will never be able to catch up with Wanteds. + +Side Note: In principle we don't actually need to /solve/ `w2`, as it is a superclass of `w1` +but we only expand it to expose any functional dependencies (see Note [The superclass story]) +But `w2` is a wanted constraint, so we will try to solve it like any other, +even though ultimately we will discard its evidence. + +Solution: Simply bound the maximum number of layers of expansion for +Givens and Wanteds, with ExpansionFuel. Give the Givens more fuel +(say 3 layers) than the Wanteds (say 1 layer). Now the Givens will +win. The Wanteds don't need much fuel: we are only expanding at all +to expose functional dependencies, and wantedFuel=1 means we will +expand a full recursive layer. If the superclass hierarchy is +non-recursive (the normal case) one layer is therefore full expansion. + +The default value for wantedFuel = Constants.max_WANTEDS_FUEL = 1. +The default value for givenFuel = Constants.max_GIVENS_FUEL = 3. +Both are configurable via the `-fgivens-fuel` and `-fwanteds-fuel` +compiler flags. + +There are two preconditions for the default fuel values: + (1) default givenFuel >= default wantedsFuel + (2) default givenFuel < solverIterations + +Precondition (1) ensures that we expand givens at least as many times as we expand wanted constraints +preferably givenFuel > wantedsFuel to avoid issues like T21909 while +the precondition (2) ensures that we do not reach the solver iteration limit and fail with a +more meaningful error message + +This also applies for quantified constraints; see `-fqcs-fuel` compiler flag and `QCI.qci_pend_sc` field. +-} + + solveNestedImplications :: Bag Implication -> TcS (Bag Implication) -- Precondition: the TcS inerts may contain unsolved simples which have diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index b5c65df24a..bef422c9a2 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -59,7 +59,7 @@ import Control.Monad import Data.Maybe ( isJust, isNothing ) import Data.List ( zip4 ) import GHC.Types.Basic - +import GHC.Driver.Session ( givensFuel, wantedsFuel, qcsFuel ) import qualified Data.Semigroup as S import Data.Bifunctor ( bimap ) @@ -154,9 +154,13 @@ canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct) -- Precondition: EvVar is class evidence canClassNC ev cls tys | isGiven ev -- See Note [Eagerly expand given superclasses] - = do { sc_cts <- mkStrictSuperClasses ev [] [] cls tys + = do { dflags <- getDynFlags + ; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev [] [] cls tys + -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel] ; emitWork sc_cts - ; canClass ev cls tys False } + ; canClass ev cls tys doNotExpand } + -- doNotExpand: We have already expanded superclasses for /this/ dict + -- so set the fuel to doNotExpand to avoid repeating expansion | CtWanted { ctev_rewriters = rewriters } <- ev , Just ip_name <- isCallStackPred cls tys @@ -168,7 +172,7 @@ canClassNC ev cls tys -- and Note [Solving CallStack constraints] in GHC.Tc.Solver.Types = do { -- First we emit a new constraint that will capture the -- given CallStack. - ; let new_loc = setCtLocOrigin loc (IPOccOrigin (HsIPName ip_name)) + let new_loc = setCtLocOrigin loc (IPOccOrigin (HsIPName ip_name)) -- We change the origin to IPOccOrigin so -- this rule does not fire again. -- See Note [Overview of implicit CallStacks] @@ -182,14 +186,20 @@ canClassNC ev cls tys (ctLocSpan loc) (ctEvExpr new_ev) ; solveCallStack ev ev_cs - ; canClass new_ev cls tys False -- No superclasses + ; canClass new_ev cls tys doNotExpand + -- doNotExpand: No superclasses for class CallStack + -- See invariants in CDictCan.cc_pend_sc } | otherwise - = canClass ev cls tys (has_scs cls) + = do { dflags <- getDynFlags + ; let fuel | classHasSCs cls = wantedsFuel dflags + | otherwise = doNotExpand + -- See Invariants in `CCDictCan.cc_pend_sc` + ; canClass ev cls tys fuel + } where - has_scs cls = not (null (classSCTheta cls)) loc = ctEvLoc ev orig = ctLocOrigin loc pred = ctEvPred ev @@ -206,7 +216,7 @@ solveCallStack ev ev_cs = do canClass :: CtEvidence -> Class -> [Type] - -> Bool -- True <=> un-explored superclasses + -> ExpansionFuel -- n > 0 <=> un-explored superclasses -> TcS (StopOrContinue Ct) -- Precondition: EvVar is class evidence @@ -307,10 +317,11 @@ So here's the plan: 4. Go round to (2) again. This loop (2,3,4) is implemented in GHC.Tc.Solver.simpl_loop. -The cc_pend_sc flag in a CDictCan records whether the superclasses of +The cc_pend_sc field in a CDictCan records whether the superclasses of this constraint have been expanded. Specifically, in Step 3 we only -expand superclasses for constraints with cc_pend_sc set to true (i.e. -isPendingScDict holds). +expand superclasses for constraints with cc_pend_sc > 0 +(i.e. isPendingScDict holds). +See Note [Expanding Recursive Superclasses and ExpansionFuel] Why do we do this? Two reasons: @@ -337,7 +348,8 @@ our strategy. Consider f :: C a => a -> Bool f x = x==x Then canClassNC gets the [G] d1: C a constraint, and eager emits superclasses -G] d2: D a, [G] d3: C a (psc). (The "psc" means it has its sc_pend flag set.) +G] d2: D a, [G] d3: C a (psc). (The "psc" means it has its cc_pend_sc has pending +expansion fuel.) When processing d3 we find a match with d1 in the inert set, and we always keep the inert item (d1) if possible: see Note [Replacement vs keeping] in GHC.Tc.Solver.Interact. So d3 dies a quick, happy death. @@ -484,7 +496,6 @@ the sc_theta_ids at all. So our final construction is makeSuperClasses :: [Ct] -> TcS [Ct] -- Returns strict superclasses, transitively, see Note [The superclass story] --- See Note [The superclass story] -- The loop-breaking here follows Note [Expanding superclasses] in GHC.Tc.Utils.TcType -- Specifically, for an incoming (C t) constraint, we return all of (C t)'s -- superclasses, up to /and including/ the first repetition of C @@ -493,39 +504,45 @@ makeSuperClasses :: [Ct] -> TcS [Ct] -- class C [a] => D a -- makeSuperClasses (C x) will return (D x, C [x]) -- --- NB: the incoming constraints have had their cc_pend_sc flag already --- flipped to False, by isPendingScDict, so we are /obliged/ to at --- least produce the immediate superclasses +-- NB: the incoming constraint's superclass will consume a unit of fuel +-- Preconditions on `cts`: 1. They are either `CDictCan` or `CQuantCan` +-- 2. Their fuel (stored in cc_pend_sc or qci_pend_sc) is > 0 makeSuperClasses cts = concatMapM go cts where - go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys }) - = mkStrictSuperClasses ev [] [] cls tys - go (CQuantCan (QCI { qci_pred = pred, qci_ev = ev })) + go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys, cc_pend_sc = fuel }) + = assertFuelPreconditionStrict fuel $ -- fuel needs to be more than 0 always + mkStrictSuperClasses fuel ev [] [] cls tys + go (CQuantCan (QCI { qci_pred = pred, qci_ev = ev, qci_pend_sc = fuel })) = assertPpr (isClassPred pred) (ppr pred) $ -- The cts should all have -- class pred heads - mkStrictSuperClasses ev tvs theta cls tys + assertFuelPreconditionStrict fuel $ -- fuel needs to be more than 0 always + mkStrictSuperClasses fuel ev tvs theta cls tys where (tvs, theta, cls, tys) = tcSplitDFunTy (ctEvPred ev) go ct = pprPanic "makeSuperClasses" (ppr ct) mkStrictSuperClasses - :: CtEvidence + :: ExpansionFuel -> CtEvidence -> [TyVar] -> ThetaType -- These two args are non-empty only when taking -- superclasses of a /quantified/ constraint -> Class -> [Type] -> TcS [Ct] -- Return constraints for the strict superclasses of -- ev :: forall as. theta => cls tys -mkStrictSuperClasses ev tvs theta cls tys - = mk_strict_superclasses (unitNameSet (className cls)) +-- Precondition: fuel > 0 +-- Postcondition: fuel for recursive superclass ct is one unit less than cls fuel +mkStrictSuperClasses fuel ev tvs theta cls tys + = mk_strict_superclasses (consumeFuel fuel) (unitNameSet (className cls)) ev tvs theta cls tys -mk_strict_superclasses :: NameSet -> CtEvidence +mk_strict_superclasses :: ExpansionFuel -> NameSet -> CtEvidence -> [TyVar] -> ThetaType -> Class -> [Type] -> TcS [Ct] -- Always return the immediate superclasses of (cls tys); -- and expand their superclasses, provided none of them are in rec_clss -- nor are repeated -mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc }) +-- The caller of this function is supposed to perform fuel book keeping +-- Precondition: fuel >= 0 +mk_strict_superclasses fuel rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc }) tvs theta cls tys = concatMapM do_one_given $ classSCSelIds cls @@ -543,7 +560,8 @@ mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc }) | otherwise = do { given_ev <- newGivenEvVar sc_loc $ mk_given_desc sel_id sc_pred - ; mk_superclasses rec_clss given_ev tvs theta sc_pred } + ; assertFuelPrecondition fuel + $ mk_superclasses fuel rec_clss given_ev tvs theta sc_pred } where sc_pred = classMethodInstTy sel_id tys @@ -604,7 +622,7 @@ mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc }) newly_blocked (InstSkol _ head_size) = isJust (this_size `ltPatersonSize` head_size) newly_blocked _ = False -mk_strict_superclasses rec_clss ev tvs theta cls tys +mk_strict_superclasses fuel rec_clss ev tvs theta cls tys | all noFreeVarsOfType tys = return [] -- Wanteds with no variables yield no superclass constraints. -- See Note [Improvement from Ground Wanteds] @@ -619,7 +637,7 @@ mk_strict_superclasses rec_clss ev tvs theta cls tys do_one sc_pred = do { traceTcS "mk_strict_superclasses Wanted" (ppr (mkClassPred cls tys) $$ ppr sc_pred) ; sc_ev <- newWantedNC loc (ctEvRewriters ev) sc_pred - ; mk_superclasses rec_clss sc_ev [] [] sc_pred } + ; mk_superclasses fuel rec_clss sc_ev [] [] sc_pred } {- Note [Improvement from Ground Wanteds] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -634,46 +652,53 @@ dependencies. See Note [Why adding superclasses can help] above. But no variables means no improvement; case closed. -} -mk_superclasses :: NameSet -> CtEvidence +mk_superclasses :: ExpansionFuel -> NameSet -> CtEvidence -> [TyVar] -> ThetaType -> PredType -> TcS [Ct] -- Return this constraint, plus its superclasses, if any -mk_superclasses rec_clss ev tvs theta pred +-- Precondition: fuel >= 0 +mk_superclasses fuel rec_clss ev tvs theta pred | ClassPred cls tys <- classifyPredType pred - = mk_superclasses_of rec_clss ev tvs theta cls tys + = assertFuelPrecondition fuel $ + mk_superclasses_of fuel rec_clss ev tvs theta cls tys | otherwise -- Superclass is not a class predicate = return [mkNonCanonical ev] -mk_superclasses_of :: NameSet -> CtEvidence +mk_superclasses_of :: ExpansionFuel -> NameSet -> CtEvidence -> [TyVar] -> ThetaType -> Class -> [Type] -> TcS [Ct] -- Always return this class constraint, -- and expand its superclasses -mk_superclasses_of rec_clss ev tvs theta cls tys +-- Precondition: fuel >= 0 +mk_superclasses_of fuel rec_clss ev tvs theta cls tys | loop_found = do { traceTcS "mk_superclasses_of: loop" (ppr cls <+> ppr tys) - ; return [this_ct] } -- cc_pend_sc of this_ct = True + ; assertFuelPrecondition fuel $ return [mk_this_ct fuel] } + -- cc_pend_sc of returning ct = fuel | otherwise = do { traceTcS "mk_superclasses_of" (vcat [ ppr cls <+> ppr tys , ppr (isCTupleClass cls) , ppr rec_clss ]) - ; sc_cts <- mk_strict_superclasses rec_clss' ev tvs theta cls tys - ; return (this_ct : sc_cts) } - -- cc_pend_sc of this_ct = False + ; sc_cts <- assertFuelPrecondition fuel $ + mk_strict_superclasses fuel rec_clss' ev tvs theta cls tys + ; return (mk_this_ct doNotExpand : sc_cts) } + -- doNotExpand: we have expanded this cls's superclasses, so + -- exhaust the associated constraint's fuel, + -- to avoid duplicate work where cls_nm = className cls loop_found = not (isCTupleClass cls) && cls_nm `elemNameSet` rec_clss -- Tuples never contribute to recursion, and can be nested rec_clss' = rec_clss `extendNameSet` cls_nm - - this_ct | null tvs, null theta - = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys - , cc_pend_sc = loop_found } - -- NB: If there is a loop, we cut off, so we have not - -- added the superclasses, hence cc_pend_sc = True - | otherwise - = CQuantCan (QCI { qci_tvs = tvs, qci_pred = mkClassPred cls tys - , qci_ev = ev - , qci_pend_sc = loop_found }) + mk_this_ct :: ExpansionFuel -> Ct + mk_this_ct fuel | null tvs, null theta + = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys + , cc_pend_sc = fuel } + -- NB: If there is a loop, we cut off, so we have not + -- added the superclasses, hence cc_pend_sc = fuel + | otherwise + = CQuantCan (QCI { qci_tvs = tvs, qci_pred = mkClassPred cls tys + , qci_ev = ev + , qci_pend_sc = fuel }) {- Note [Equality superclasses in quantified constraints] @@ -828,19 +853,28 @@ canForAllNC :: CtEvidence -> [TyVar] -> TcThetaType -> TcPredType canForAllNC ev tvs theta pred | isGiven ev -- See Note [Eagerly expand given superclasses] , Just (cls, tys) <- cls_pred_tys_maybe - = do { sc_cts <- mkStrictSuperClasses ev tvs theta cls tys + = do { dflags <- getDynFlags + ; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev tvs theta cls tys + -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel] ; emitWork sc_cts - ; canForAll ev False } + ; canForAll ev doNotExpand } + -- doNotExpand: as we have already (eagerly) expanded superclasses for this class | otherwise - = canForAll ev (isJust cls_pred_tys_maybe) - + = do { dflags <- getDynFlags + ; let fuel | Just (cls, _) <- cls_pred_tys_maybe + , classHasSCs cls = qcsFuel dflags + -- See invariants (a) and (b) in QCI.qci_pend_sc + -- qcsFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel] + -- See Note [Quantified constraints] + | otherwise = doNotExpand + ; canForAll ev fuel } where cls_pred_tys_maybe = getClassPredTys_maybe pred -canForAll :: CtEvidence -> Bool -> TcS (StopOrContinue Ct) +canForAll :: CtEvidence -> ExpansionFuel -> TcS (StopOrContinue Ct) -- We have a constraint (forall as. blah => C tys) -canForAll ev pend_sc +canForAll ev fuel = do { -- First rewrite it to apply the current substitution let pred = ctEvPred ev ; (redn, rewriters) <- rewrite ev pred @@ -850,14 +884,14 @@ canForAll ev pend_sc -- (It takes a lot less code to rewrite before decomposing.) ; case classifyPredType (ctEvPred new_ev) of ForAllPred tvs theta pred - -> solveForAll new_ev tvs theta pred pend_sc + -> solveForAll new_ev tvs theta pred fuel _ -> pprPanic "canForAll" (ppr new_ev) } } -solveForAll :: CtEvidence -> [TyVar] -> TcThetaType -> PredType -> Bool +solveForAll :: CtEvidence -> [TyVar] -> TcThetaType -> PredType -> ExpansionFuel -> TcS (StopOrContinue Ct) solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_loc = loc }) - tvs theta pred _pend_sc + tvs theta pred _fuel = -- See Note [Solving a Wanted forall-constraint] setLclEnv (ctLocEnv loc) $ -- This setLclEnv is important: the emitImplicationTcS uses that @@ -903,12 +937,12 @@ solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_lo _ -> pSizeType pred -- See Note [Solving a Given forall-constraint] -solveForAll ev@(CtGiven {}) tvs _theta pred pend_sc +solveForAll ev@(CtGiven {}) tvs _theta pred fuel = do { addInertForAll qci ; stopWith ev "Given forall-constraint" } where qci = QCI { qci_ev = ev, qci_tvs = tvs - , qci_pred = pred, qci_pend_sc = pend_sc } + , qci_pred = pred, qci_pend_sc = fuel } {- Note [Solving a Wanted forall-constraint] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index ad4e10ebf6..5fdd4df702 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -513,10 +513,13 @@ getInertGivens ; return (filter isGivenCt all_cts) } getPendingGivenScs :: TcS [Ct] --- Find all inert Given dictionaries, or quantified constraints, --- whose cc_pend_sc flag is True --- and that belong to the current level --- Set their cc_pend_sc flag to False in the inert set, and return that Ct +-- Find all inert Given dictionaries, or quantified constraints, such that +-- 1. cc_pend_sc flag has fuel strictly > 0 +-- 2. belongs to the current level +-- For each such dictionary: +-- * Return it (with unmodified cc_pend_sc) in sc_pending +-- * Modify the dict in the inert set to have cc_pend_sc = doNotExpand +-- to record that we have expanded superclasses for this dict getPendingGivenScs = do { lvl <- getTcLevel ; updRetInertCans (get_sc_pending lvl) } @@ -530,29 +533,33 @@ get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts }) sc_pending = sc_pend_insts ++ sc_pend_dicts sc_pend_dicts = foldDicts get_pending dicts [] - dicts' = foldr add dicts sc_pend_dicts + dicts' = foldr exhaustAndAdd dicts sc_pend_dicts (sc_pend_insts, insts') = mapAccumL get_pending_inst [] insts - get_pending :: Ct -> [Ct] -> [Ct] -- Get dicts with cc_pend_sc = True - -- but flipping the flag + get_pending :: Ct -> [Ct] -> [Ct] -- Get dicts with cc_pend_sc > 0 get_pending dict dicts - | Just dict' <- pendingScDict_maybe dict + | isPendingScDict dict , belongs_to_this_level (ctEvidence dict) - = dict' : dicts + = dict : dicts | otherwise = dicts - add :: Ct -> DictMap Ct -> DictMap Ct - add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts - = addDict dicts cls tys ct - add ct _ = pprPanic "getPendingScDicts" (ppr ct) + exhaustAndAdd :: Ct -> DictMap Ct -> DictMap Ct + exhaustAndAdd ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts + -- exhaust the fuel for this constraint before adding it as + -- we don't want to expand these constraints again + = addDict dicts cls tys (ct {cc_pend_sc = doNotExpand}) + exhaustAndAdd ct _ = pprPanic "getPendingScDicts" (ppr ct) get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst) get_pending_inst cts qci@(QCI { qci_ev = ev }) | Just qci' <- pendingScInst_maybe qci , belongs_to_this_level ev - = (CQuantCan qci' : cts, qci') + = (CQuantCan qci : cts, qci') + -- qci' have their fuel exhausted + -- we don't want to expand these constraints again + -- qci is expanded | otherwise = (cts, qci) diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index bd66282b24..d10c4394f6 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -11,6 +11,8 @@ module GHC.Tc.Types.Constraint ( -- Canonical constraints Xi, Ct(..), Cts, + ExpansionFuel, doNotExpand, consumeFuel, pendingFuel, + assertFuelPrecondition, assertFuelPreconditionStrict, emptyCts, andCts, andManyCts, pprCts, singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList, isEmptyCts, @@ -138,8 +140,6 @@ import Data.Word ( Word8 ) import Data.List ( intersperse ) - - {- ************************************************************************ * * @@ -191,6 +191,37 @@ type Xi = TcType type Cts = Bag Ct +-- | Says how many layers of superclasses can we expand. +-- Invariant: ExpansionFuel should always be >= 0 +-- see Note [Expanding Recursive Superclasses and ExpansionFuel] +type ExpansionFuel = Int + +-- | Do not expand superclasses any further +doNotExpand :: ExpansionFuel +doNotExpand = 0 + +-- | Consumes one unit of fuel. +-- Precondition: fuel > 0 +consumeFuel :: ExpansionFuel -> ExpansionFuel +consumeFuel fuel = assertFuelPreconditionStrict fuel $ fuel - 1 + +-- | Returns True if we have any fuel left for superclass expansion +pendingFuel :: ExpansionFuel -> Bool +pendingFuel n = n > 0 + +insufficientFuelError :: SDoc +insufficientFuelError = text "Superclass expansion fuel should be > 0" + +-- | asserts if fuel is non-negative +assertFuelPrecondition :: ExpansionFuel -> a -> a +{-# INLINE assertFuelPrecondition #-} +assertFuelPrecondition fuel = assertPpr (fuel >= 0) insufficientFuelError + +-- | asserts if fuel is strictly greater than 0 +assertFuelPreconditionStrict :: ExpansionFuel -> a -> a +{-# INLINE assertFuelPreconditionStrict #-} +assertFuelPreconditionStrict fuel = assertPpr (pendingFuel fuel) insufficientFuelError + data Ct -- Atomic canonical constraints = CDictCan { -- e.g. Num ty @@ -199,11 +230,12 @@ data Ct cc_class :: Class, cc_tyargs :: [Xi], -- cc_tyargs are rewritten w.r.t. inerts, so Xi - cc_pend_sc :: Bool + cc_pend_sc :: ExpansionFuel -- See Note [The superclass story] in GHC.Tc.Solver.Canonical - -- True <=> (a) cc_class has superclasses - -- (b) we have not (yet) added those - -- superclasses as Givens + -- See Note [Expanding Recursive Superclasses and ExpansionFuel] in GHC.Tc.Solver + -- Invariants: cc_pend_sc > 0 <=> + -- (a) cc_class has superclasses + -- (b) those superclasses are not yet explored } | CIrredCan { -- These stand for yet-unusable predicates @@ -273,8 +305,13 @@ data QCInst -- A much simplified version of ClsInst -- Always Given , qci_tvs :: [TcTyVar] -- The tvs , qci_pred :: TcPredType -- The ty - , qci_pend_sc :: Bool -- Same as cc_pend_sc flag in CDictCan - -- Invariant: True => qci_pred is a ClassPred + , qci_pend_sc :: ExpansionFuel + -- Invariants: qci_pend_sc > 0 => + -- (a) qci_pred is a ClassPred + -- (b) this class has superclass(es), and + -- (c) the superclass(es) are not explored yet + -- Same as cc_pend_sc flag in CDictCan + -- See Note [Expanding Recursive Superclasses and ExpansionFuel] in GHC.Tc.Solver } instance Outputable QCInst where @@ -673,11 +710,11 @@ instance Outputable Ct where CEqCan {} -> text "CEqCan" CNonCanonical {} -> text "CNonCanonical" CDictCan { cc_pend_sc = psc } - | psc -> text "CDictCan(psc)" - | otherwise -> text "CDictCan" + | psc > 0 -> text "CDictCan" <> parens (text "psc" <+> ppr psc) + | otherwise -> text "CDictCan" CIrredCan { cc_reason = reason } -> text "CIrredCan" <> ppr reason - CQuantCan (QCI { qci_pend_sc = pend_sc }) - | pend_sc -> text "CQuantCan(psc)" + CQuantCan (QCI { qci_pend_sc = psc }) + | psc > 0 -> text "CQuantCan" <> parens (text "psc" <+> ppr psc) | otherwise -> text "CQuantCan" ----------------------------------- @@ -893,23 +930,24 @@ isUserTypeError pred = case getUserTypeErrorMsg pred of _ -> False isPendingScDict :: Ct -> Bool -isPendingScDict (CDictCan { cc_pend_sc = psc }) = psc --- Says whether this is a CDictCan with cc_pend_sc is True; +isPendingScDict (CDictCan { cc_pend_sc = f }) = pendingFuel f +-- Says whether this is a CDictCan with cc_pend_sc has positive fuel; -- i.e. pending un-expanded superclasses isPendingScDict _ = False pendingScDict_maybe :: Ct -> Maybe Ct --- Says whether this is a CDictCan with cc_pend_sc is True, --- AND if so flips the flag -pendingScDict_maybe ct@(CDictCan { cc_pend_sc = True }) - = Just (ct { cc_pend_sc = False }) +-- Says whether this is a CDictCan with cc_pend_sc has fuel left, +-- AND if so exhausts the fuel so that they are not expanded again +pendingScDict_maybe ct@(CDictCan { cc_pend_sc = f }) + | pendingFuel f = Just (ct { cc_pend_sc = doNotExpand }) + | otherwise = Nothing pendingScDict_maybe _ = Nothing pendingScInst_maybe :: QCInst -> Maybe QCInst -- Same as isPendingScDict, but for QCInsts -pendingScInst_maybe qci@(QCI { qci_pend_sc = True }) - = Just (qci { qci_pend_sc = False }) -pendingScInst_maybe _ = Nothing +pendingScInst_maybe qci@(QCI { qci_pend_sc = f }) + | pendingFuel f = Just (qci { qci_pend_sc = doNotExpand }) + | otherwise = Nothing superClassesMightHelp :: WantedConstraints -> Bool -- ^ True if taking superclasses of givens, or of wanteds (to perhaps @@ -928,11 +966,12 @@ superClassesMightHelp (WC { wc_simple = simples, wc_impl = implics }) is_ip _ = False getPendingWantedScs :: Cts -> ([Ct], Cts) +-- in the return values [Ct] has original fuel while Cts has fuel exhausted getPendingWantedScs simples = mapAccumBagL get [] simples where - get acc ct | Just ct' <- pendingScDict_maybe ct - = (ct':acc, ct') + get acc ct | Just ct_exhausted <- pendingScDict_maybe ct + = (ct:acc, ct_exhausted) | otherwise = (acc, ct) |