[Git][ghc/ghc][wip/T21909] 3 commits: abstract default fuel into constants
Apoorv Ingle (@ani)
gitlab at gitlab.haskell.org
Thu Feb 9 22:54:21 UTC 2023
Apoorv Ingle pushed to branch wip/T21909 at Glasgow Haskell Compiler / GHC
Commits:
493ba50a by Apoorv Ingle at 2023-02-09T16:53:49-06:00
abstract default fuel into constants
- - - - -
8e8e1162 by Apoorv Ingle at 2023-02-09T16:53:56-06:00
added note [SimplifyInfer and UndecidableSuperClasses]
- - - - -
55922356 by Apoorv Ingle at 2023-02-09T16:53:56-06:00
make expansion fuel a dynamic flag
- - - - -
5 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/Types/Constraint.hs
Changes:
=====================================
compiler/GHC/Driver/Session.hs
=====================================
@@ -517,6 +517,12 @@ 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
+ wantedsFuel :: Int, -- ^ Number of layers of superclass expansion
+ -- Should be < givensFuel
+ qcsFuel :: Int, -- ^ Number of layers of superclass expansion
+ -- Should be < givensFuel
homeUnitId_ :: UnitId, -- ^ Target home unit-id
homeUnitInstanceOf_ :: Maybe UnitId, -- ^ Id of the unit to instantiate
@@ -1148,6 +1154,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,
@@ -2732,6 +2741,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
=====================================
@@ -2370,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]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In some cases while infering the type of a term well typed term, it is necessary to ensure
+we limit the wanted superclass expansions.
+Expanding them too many times will lead to the given constraint superclass expansion
+not being able solve all the wanted constraints, by entering a perpetual loop and erroring out on
+too many solver iterations. Expanding them too little will not give us a simplified type signature.
+
+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
+
+In the current implimentation
+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 ( DynFlags, givensFuel, wantedsFuel, qcsFuel )
import qualified Data.Semigroup as S
import Data.Bifunctor ( bimap )
@@ -127,14 +127,16 @@ canonicalize (CEqCan { cc_ev = ev
canNC :: CtEvidence -> TcS (StopOrContinue Ct)
canNC ev =
case classifyPredType pred of
- ClassPred cls tys -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
- canClassNC ev cls tys
+ ClassPred cls tys -> do dflags <- getDynFlags
+ traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
+ canClassNC dflags ev cls tys
EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
canEqNC ev eq_rel ty1 ty2
IrredPred {} -> do traceTcS "canEvNC:irred" (ppr pred)
canIrred ev
- ForAllPred tvs th p -> do traceTcS "canEvNC:forall" (ppr pred)
- canForAllNC ev tvs th p
+ ForAllPred tvs th p -> do dflags <- getDynFlags
+ traceTcS "canEvNC:forall" (ppr pred)
+ canForAllNC dflags ev tvs th p
where
pred = ctEvPred ev
@@ -147,13 +149,14 @@ canNC ev =
************************************************************************
-}
-canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
+canClassNC :: DynFlags -> CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
-- "NC" means "non-canonical"; that is, we have got here
-- from a NonCanonical constraint, not from a CDictCan
-- Precondition: EvVar is class evidence
-canClassNC ev cls tys
+canClassNC dflags ev cls tys
| isGiven ev -- See Note [Eagerly expand given superclasses]
- = do { sc_cts <- mkStrictSuperClasses defaultFuelGivens ev [] [] cls tys
+ = do { let gf = givensFuel dflags
+ ; sc_cts <- mkStrictSuperClasses gf ev [] [] cls tys
; emitWork sc_cts
; canClass ev cls tys doNotExpand }
@@ -188,8 +191,8 @@ canClassNC ev cls tys
= canClass ev cls tys fuel
where
- fuel | cls_has_scs = defaultFuelWanteds
- | otherwise = doNotExpand
+ fuel | cls_has_scs = wantedsFuel dflags
+ | otherwise = doNotExpand
cls_has_scs = not (null (classSCTheta cls))
loc = ctEvLoc ev
orig = ctLocOrigin loc
@@ -729,6 +732,7 @@ canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
-- Precondition: ty not a tuple and no other evidence form
canIrred ev
= do { let pred = ctEvPred ev
+ ; dflags <- getDynFlags
; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
; (redn, rewriters) <- rewrite ev pred
; rewriteEvidence rewriters ev redn `andWhenContinue` \ new_ev ->
@@ -737,7 +741,7 @@ canIrred ev
-- Code is like the canNC, except
-- that the IrredPred branch stops work
; case classifyPredType (ctEvPred new_ev) of
- ClassPred cls tys -> canClassNC new_ev cls tys
+ ClassPred cls tys -> canClassNC dflags new_ev cls tys
EqPred eq_rel ty1 ty2 -> -- IrredPreds have kind Constraint, so
-- cannot become EqPreds
pprPanic "canIrred: EqPred"
@@ -746,7 +750,7 @@ canIrred ev
-- should never leave a meta-var filled
-- in with a polytype. This is #18987.
do traceTcS "canEvNC:forall" (ppr pred)
- canForAllNC ev tvs th p
+ canForAllNC dflags ev tvs th p
IrredPred {} -> continueWith $
mkIrredCt IrredShapeReason new_ev } }
@@ -828,21 +832,23 @@ type signature.
-}
-canForAllNC :: CtEvidence -> [TyVar] -> TcThetaType -> TcPredType
+canForAllNC :: DynFlags -> CtEvidence -> [TyVar] -> TcThetaType -> TcPredType
-> TcS (StopOrContinue Ct)
-canForAllNC ev tvs theta pred
+canForAllNC dflags ev tvs theta pred
| isGiven ev -- See Note [Eagerly expand given superclasses]
, Just (cls, tys) <- cls_pred_tys_maybe
- = do { sc_cts <- mkStrictSuperClasses defaultFuelGivens ev tvs theta cls tys
+ = do { let gf = givensFuel dflags
+ ; sc_cts <- mkStrictSuperClasses gf ev tvs theta cls tys
; emitWork sc_cts
; canForAll ev doNotExpand }
| otherwise
- = canForAll ev fuel
+ = do { let qcf = qcsFuel dflags
+ fuel | isJust cls_pred_tys_maybe = qcf
+ | otherwise = doNotExpand
+ ; canForAll ev fuel }
where
- fuel | isJust cls_pred_tys_maybe = defaultFuelQC
- | otherwise = doNotExpand
cls_pred_tys_maybe = getClassPredTys_maybe pred
canForAll :: CtEvidence -> ExpansionFuel -> TcS (StopOrContinue Ct)
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -11,8 +11,7 @@ module GHC.Tc.Types.Constraint (
-- Canonical constraints
Xi, Ct(..), Cts,
- ExpansionFuel, doNotExpand, defaultFuelGivens, defaultFuelWanteds,
- defaultFuelQC, consumeFuel,
+ ExpansionFuel, doNotExpand, consumeFuel,
emptyCts, andCts, andManyCts, pprCts,
singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
isEmptyCts,
@@ -140,8 +139,6 @@ import Data.Word ( Word8 )
import Data.List ( intersperse )
-
-
{-
************************************************************************
* *
@@ -194,14 +191,11 @@ type Xi = TcType
type Cts = Bag Ct
-- | Says how many layers of superclasses can we expand.
--- see T21909
+-- see Note [SimplifyIner with UndecidableSuperClasses]
type ExpansionFuel = Int
-doNotExpand, defaultFuelGivens, defaultFuelWanteds, defaultFuelQC :: ExpansionFuel
+doNotExpand :: ExpansionFuel -- Do not expand superclasses anymore
doNotExpand = 0
-defaultFuelQC = 1
-defaultFuelWanteds = 1
-defaultFuelGivens = 3
consumeFuel :: ExpansionFuel -> ExpansionFuel
consumeFuel fuel = fuel - 1
@@ -216,6 +210,7 @@ data Ct
cc_pend_sc :: ExpansionFuel
-- See Note [The superclass story] in GHC.Tc.Solver.Canonical
+ -- See Note [SimplifyInfer with UndecidableSuperClasses] in GHC.Tc.Solver
-- n > 0 <=> (a) cc_class has superclasses
-- (b) we have not (yet) explored those superclasses
}
@@ -287,9 +282,11 @@ data QCInst -- A much simplified version of ClsInst
-- Always Given
, qci_tvs :: [TcTyVar] -- The tvs
, qci_pred :: TcPredType -- The ty
- , qci_pend_sc :: ExpansionFuel -- Same as cc_pend_sc flag in CDictCan
- -- Invariants: qci_pend_sc > 0 => qci_pred is a ClassPred
- -- the superclasses are unexplored
+ , 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
@@ -915,7 +912,7 @@ isPendingScDict _ = False
pendingScDict_maybe :: Ct -> Maybe Ct
-- Says whether this is a CDictCan with cc_pend_sc has fuel left,
--- AND if so flips the flag
+-- AND if so exhausts the fuel so that they are not expanded again
pendingScDict_maybe ct@(CDictCan { cc_pend_sc = n })
| n > 0 = Just (ct { cc_pend_sc = doNotExpand })
| otherwise = Nothing
@@ -944,12 +941,12 @@ superClassesMightHelp (WC { wc_simple = simples, wc_impl = implics })
is_ip _ = False
getPendingWantedScs :: Cts -> ([Ct], Cts)
--- [Ct] has original fuel while Cts has fuel exhausted
+-- 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)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/4cb98f17e040e0c22ea24ebe3f431090d127dd20...55922356bdb0c29b20ca15839d1a82037389ce9d
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/4cb98f17e040e0c22ea24ebe3f431090d127dd20...55922356bdb0c29b20ca15839d1a82037389ce9d
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/20230209/91ab8a2c/attachment-0001.html>
More information about the ghc-commits
mailing list