[Git][ghc/ghc][wip/T21909] Constraint simplification loop now depends on `ExpansionFuel`
Apoorv Ingle (@ani)
gitlab at gitlab.haskell.org
Wed Feb 22 00:36:57 UTC 2023
Apoorv Ingle pushed to branch wip/T21909 at Glasgow Haskell Compiler / GHC
Commits:
f2fcc3d5 by Apoorv Ingle at 2023-02-21T18:36:43-06:00
Constraint simplification loop now depends on `ExpansionFuel`
instead of a boolean flag for `CDictCan.cc_pend_sc`.
Pending givens get a fuel of 3 while Wanted and quantified constraints get a fuel of 1.
This helps pending given constraints to keep up with pending wanted constraints in case of
`UndecidableSuperClasses` and superclass expansions while simplifying the infered type.
Adds 3 dynamic flags for controlling the fuels for each type of constraints
`-fgivens-expansion-fuel` for givens `-fwanteds-expansion-fuel` for wanteds and `-fqcs-expansion-fuel` for quantified constraints
Fixes #21909
Added Tests T21909, T21909b
Added Note [SimplifyInfer and UndecidableSuperClasses]
- - - - -
10 changed files:
- compiler/GHC/Driver/Session.hs
- compiler/GHC/Settings/Constants.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- docs/users_guide/expected-undocumented-flags.txt
- + testsuite/tests/typecheck/should_compile/T21909.hs
- + testsuite/tests/typecheck/should_compile/T21909b.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
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
+ -- Should be < solverIterations
+ -- See Note [SimplifyInfer with UndecidableSuperClasses]
+ wantedsFuel :: Int, -- ^ Number of layers of superclass expansion
+ -- Should be < givensFuel
+ -- See Note [SimplifyInfer with UndecidableSuperClasses]
+ qcsFuel :: Int, -- ^ Number of layers of superclass expansion
+ -- Should be < givensFuel
+ -- See Note [SimplifyInfer with UndecidableSuperClasses]
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"
=====================================
compiler/GHC/Settings/Constants.hs
=====================================
@@ -30,6 +30,21 @@ 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
+mAX_QC_FUEL :: Int
+mAX_QC_FUEL = 3
+
+-- | In case of loopy wanted constraints,
+-- how many times should we allow superclass expansions
+mAX_WANTEDS_FUEL :: Int
+mAX_WANTEDS_FUEL = 1
+
+-- | In case of loopy given constraints,
+-- how many times should we allow superclass expansions
+mAX_GIVENS_FUEL :: Int
+mAX_GIVENS_FUEL = 3
+
wORD64_SIZE :: Int
wORD64_SIZE = 8
=====================================
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,43 @@ superclasses. In that case we check whether the new Wanteds actually led to
any new unifications, and iterate the implications only if so.
-}
+{- Note [SimplifyInfer with UndecidableSuperClasses]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the program (T21909)
+
+ class C [a] => C a where
+ foo :: a -> Int
+
+ bar :: C a => a -> Int
+ bar x = foolocal x
+ where
+ foolocal x = foo x
+
+While infering the type of `foolocal`, it is necessary that
+we limit the wanted superclass expansions. Expanding too many layers
+of wanted constraints will lead to the given constraint superclass expansion not being able catch up
+all the wanted constraints, by entering in a perpetual loop and erroring out on
+too many solver iterations. On the other hand expanding them too little
+will may not give us a simplified type signature.
+
+We infer the type of foolocal to be `(C a) => a -> Int`
+and then simplify it to `(C a, C [[a]]) => a -> Int`
+
+This indeed is not simplification per say, but we are in UndecidableSuperclass case
+so we cannot guarantee simplification of contraints. What we aim for is for the
+the solver to not to loop unnecessarily generating more wanted constraints than
+in can solve in `maybe_simplify_again`.
+
+If we did not limit the wanteds superclass expansion we would simplify the type signature of
+foolocal as `(C a , C [[a]], C[[[[a]]]], C[[[[a]]]], C [[[[[[[[a]]]]]]]]) => a -> Int`
+Definitely _worse_ than above type!
+
+The current limit the expansion of such recursive wanted constraints to 1 (mAX_WANTEDS_FUEL),
+and limit the expansion of recursive given constraints to 3 (mAX_GIVENS_FUEL).
+
+-}
+
+
solveNestedImplications :: Bag Implication
-> TcS (Bag Implication)
-- Precondition: the TcS inerts may contain unsolved simples which have
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -58,7 +58,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 )
@@ -153,9 +153,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
+ ; let gf = givensFuel dflags -- See Note [SimplifyInfer with UndecidableSuperClasses]
+ ; sc_cts <- mkStrictSuperClasses gf ev [] [] cls tys
; emitWork sc_cts
- ; canClass ev cls tys False }
+ ; canClass ev cls tys doNotExpand }
+ -- doNotExpand We have already expanded superclasses for this class
+ -- so set the fuel to doNotExpand to avoid repeating expansion
| CtWanted { ctev_rewriters = rewriters } <- ev
, Just ip_name <- isCallStackPred cls tys
@@ -167,7 +171,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]
@@ -181,14 +185,21 @@ 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 -- No superclasses
+ -- doNotExpand: we have just expanded /this/ dict's superclasses
+ -- so set the fuel doNotExpand to avoid repeating that expansion.
}
| otherwise
- = canClass ev cls tys (has_scs cls)
+ = do { dflags <- getDynFlags
+ ; let fuel | cls_has_scs = wantedsFuel dflags
+ | otherwise = doNotExpand -- No superclasses hence no need for any expansions
+ ; canClass ev cls tys fuel
+ }
where
- has_scs cls = not (null (classSCTheta cls))
+ cls_has_scs = not (null (classSCTheta cls))
loc = ctEvLoc ev
orig = ctLocOrigin loc
pred = ctEvPred ev
@@ -205,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
@@ -483,7 +494,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
@@ -492,39 +502,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 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 })
+ = checkFuelPreconditionStrict 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
+ checkFuelPreconditionStrict 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
@@ -542,7 +558,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 }
+ ; checkFuelPrecondition fuel
+ $ mk_superclasses fuel rec_clss given_ev tvs theta sc_pred }
where
sc_pred = classMethodInstTy sel_id tys
@@ -603,7 +620,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]
@@ -618,7 +635,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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -633,46 +650,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
+ = checkFuelPrecondition 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
+ ; checkFuelPrecondition 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 <- checkFuelPrecondition 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]
@@ -827,19 +851,27 @@ 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 [SimplifyInfer with UndecidableSuperClasses]
; 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 | isJust cls_pred_tys_maybe = qcsFuel dflags
+ -- Superclass expansion makes sense only if we have a class constraint
+ -- qcsFuel dflags: See Note [SimplifyInfer with UndecidableSuperClasses]
+ -- 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
@@ -849,14 +881,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
@@ -902,12 +934,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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
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)
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -11,6 +11,8 @@ module GHC.Tc.Types.Constraint (
-- Canonical constraints
Xi, Ct(..), Cts,
+ ExpansionFuel, doNotExpand, consumeFuel, pendingFuel,
+ checkFuelPrecondition, checkFuelPreconditionStrict,
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,36 @@ type Xi = TcType
type Cts = Bag Ct
+-- | Says how many layers of superclasses can we expand.
+-- Invarient: ExpansionFuel should always be >= 0
+-- see Note [SimplifyInfer with UndecidableSuperClasses]
+type ExpansionFuel = Int
+
+doNotExpand :: ExpansionFuel -- Do not expand superclasses any further
+doNotExpand = 0
+
+-- | Consumes one unit of fuel.
+-- Precondition: fuel > 0
+consumeFuel :: ExpansionFuel -> ExpansionFuel
+consumeFuel fuel = checkFuelPreconditionStrict 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"
+
+-- | checks if fuel is non-negative
+checkFuelPrecondition :: ExpansionFuel -> a -> a
+{-# INLINE checkFuelPrecondition #-}
+checkFuelPrecondition fuel = assertPpr (fuel >= 0) insufficientFuelError
+
+-- | checks if fuel is strictly greater than 0
+checkFuelPreconditionStrict :: ExpansionFuel -> a -> a
+{-# INLINE checkFuelPreconditionStrict #-}
+checkFuelPreconditionStrict fuel = assertPpr (pendingFuel fuel) insufficientFuelError
+
data Ct
-- Atomic canonical constraints
= CDictCan { -- e.g. Num ty
@@ -199,11 +229,11 @@ 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 [SimplifyInfer with UndecidableSuperClasses] in GHC.Tc.Solver
+ -- n > 0 <=> (a) cc_class has superclasses
+ -- (b) we have not (yet) explored those superclasses
}
| CIrredCan { -- These stand for yet-unusable predicates
@@ -273,8 +303,11 @@ 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 => qci_pred is a ClassPred
+ -- and the superclasses are unexplored
+ -- Same as cc_pend_sc flag in CDictCan
+ -- See Note [SimplifyInfer with UndecidableSuperClasses]
+ -- in GHC.Tc.Solver
}
instance Outputable QCInst where
@@ -673,11 +706,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 +926,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 +962,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)
=====================================
docs/users_guide/expected-undocumented-flags.txt
=====================================
@@ -33,6 +33,9 @@
-fbang-patterns
-fbuilding-cabal-package
-fconstraint-solver-iterations
+-fgivens-expansion-fuel
+-fwanteds-expansion-fuel
+-fqcs-expansion-fuel
-fcontext-stack
-fcross-module-specialize
-fdiagnostics-color=always
=====================================
testsuite/tests/typecheck/should_compile/T21909.hs
=====================================
@@ -0,0 +1,24 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+
+module T21909 where
+
+import Data.Kind
+
+class (Monad m, MyMonad (Inner m)) => MyMonad m where
+ type Inner m :: Type -> Type
+ foo :: m Int
+
+works :: MyMonad m => m String
+works = show <$> ((+ 1) <$> foo)
+
+fails :: MyMonad m => m String
+fails = show <$> fooPlusOne
+ where
+ fooPlusOne = (+ 1) <$> foo
+
+alsoFails :: MyMonad m => m String
+alsoFails =
+ let fooPlusOne = (+ 1) <$> foo
+ in show <$> fooPlusOne
=====================================
testsuite/tests/typecheck/should_compile/T21909b.hs
=====================================
@@ -0,0 +1,12 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableSuperClasses, FunctionalDependencies, MultiParamTypeClasses, GADTs #-}
+
+module T21909b where
+
+class C [a] => C a where
+ foo :: a -> Int
+
+bar :: C a => a -> Int
+bar x = foolocal x
+ where
+ foolocal a = foo a
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -863,3 +863,5 @@ test('T22912', normal, compile, [''])
test('T22924', normal, compile, [''])
test('T22985a', normal, compile, ['-O'])
test('T22985b', normal, compile, [''])
+test('T21909', normal, compile, [''])
+test('T21909b', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f2fcc3d5153a5a0585356553d919f2e3cf7aa95a
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f2fcc3d5153a5a0585356553d919f2e3cf7aa95a
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230221/af2a9f79/attachment-0001.html>
More information about the ghc-commits
mailing list