[Git][ghc/ghc][wip/T21909] 2 commits: added note [SimplifyInfer and UndecidableSuperClasses]
Apoorv Ingle (@ani)
gitlab at gitlab.haskell.org
Thu Feb 9 23:08:33 UTC 2023
Apoorv Ingle pushed to branch wip/T21909 at Glasgow Haskell Compiler / GHC
Commits:
8fa8b551 by Apoorv Ingle at 2023-02-09T17:08:07-06:00
added note [SimplifyInfer and UndecidableSuperClasses]
- - - - -
a1e7ebe9 by Apoorv Ingle at 2023-02-09T17:08:18-06:00
make expansion fuel a dynamic flag
- - - - -
4 changed files:
- compiler/GHC/Driver/Session.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/Tc/Solver.hs
=====================================
@@ -2372,11 +2372,11 @@ 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 make sure
-we tactfully limit the wanted superclass expansions.
+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
-no not be able to catch up causing a perpetual loop and erroring out on
-too many solver iterations. Expanding them too little might not give us enough to solve them.
+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)
@@ -2388,24 +2388,21 @@ Consider the program (T21909)
where
foolocal x = foo x
-We infer the type of foolocal to be `a -> Int` with an unsolved [W] C a
-after canonicalization and simpliying the constraint we get
- [W] C a (1)
- [W] C [a] (1)
+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`.
-and we then try to simplify the constraint `C a` via `solveWanteds` in `simplifyInfer`
-We have an implication wanted constraint:
- [G] C a0:sk (nonCanonical, lvl 1) => [W] C a1 (NonCanonical lvl 2)
-
-we first canonicalize C a0 and then simplify it and obtain at (level 1)
- [G] C a0 (3, lvl 1)
- [G] C [a0] (3 lvl 1)
-
-we then step in the implication to canonicalize and `C a1` to obtain
- [W] C a1 (1, lvl 2)
- [W] C [a1] (1, lvl 2)
+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).
-}
=====================================
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,
@@ -139,9 +138,6 @@ import Data.List.NonEmpty ( NonEmpty )
import Data.Word ( Word8 )
import Data.List ( intersperse )
-import GHC.Settings.Constants ( mAX_QC_FUEL, mAX_WANTEDS_FUEL, mAX_GIVENS_FUEL )
-
-
{-
************************************************************************
@@ -195,14 +191,11 @@ type Xi = TcType
type Cts = Bag Ct
-- | Says how many layers of superclasses can we expand.
--- see Note [SimplifyIner with UndecidableSuperClasses]
+-- see Note [SimplifyInfer with UndecidableSuperClasses]
type ExpansionFuel = Int
-doNotExpand, defaultFuelGivens, defaultFuelWanteds, defaultFuelQC :: ExpansionFuel
-doNotExpand = 0 -- Do not expand superclasses anymore
-defaultFuelQC = mAX_QC_FUEL -- default fuel for quantified constraints
-defaultFuelWanteds = mAX_WANTEDS_FUEL -- default fuel for wanted constraints
-defaultFuelGivens = mAX_GIVENS_FUEL -- default fule for given constraints
+doNotExpand :: ExpansionFuel -- Do not expand superclasses anymore
+doNotExpand = 0
consumeFuel :: ExpansionFuel -> ExpansionFuel
consumeFuel fuel = fuel - 1
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/55922356bdb0c29b20ca15839d1a82037389ce9d...a1e7ebe91fcc68e5d9857535d8b352a1b95725ae
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/55922356bdb0c29b20ca15839d1a82037389ce9d...a1e7ebe91fcc68e5d9857535d8b352a1b95725ae
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/05229c31/attachment-0001.html>
More information about the ghc-commits
mailing list