[Git][ghc/ghc][wip/T21909] Fixes #21909
Apoorv Ingle (@ani)
gitlab at gitlab.haskell.org
Tue Feb 7 23:16:20 UTC 2023
Apoorv Ingle pushed to branch wip/T21909 at Glasgow Haskell Compiler / GHC
Commits:
bd4624de by Apoorv Ingle at 2023-02-07T17:15:39-06:00
Fixes #21909
Constraint simplification loop now depends on `ExpansionFuel` instead of a boolean flag in `CDictCan.cc_pend_sc`.
Pending Givens get a fuel of 3 to start of with while Wanted constraints get a fuel of 1.
This helps pending given constraints to keep up with pending wanted constraints.
Added tests T21909, T21909b
- - - - -
7 changed files:
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- + testsuite/tests/typecheck/should_compile/T21909.hs
- + testsuite/tests/typecheck/should_compile/T21909b.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
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]
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -153,9 +153,9 @@ 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 { sc_cts <- mkStrictSuperClasses defaultFuelGivens ev [] [] cls tys
; emitWork sc_cts
- ; canClass ev cls tys False }
+ ; canClass ev cls tys doNotExpand }
| CtWanted { ctev_rewriters = rewriters } <- ev
, Just ip_name <- isCallStackPred cls tys
@@ -181,14 +181,16 @@ 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
}
| otherwise
- = canClass ev cls tys (has_scs cls)
+ = canClass ev cls tys fuel
where
- has_scs cls = not (null (classSCTheta cls))
+ fuel | cls_has_scs = defaultFuelWanteds
+ | otherwise = doNotExpand
+ cls_has_scs = not (null (classSCTheta cls))
loc = ctEvLoc ev
orig = ctLocOrigin loc
pred = ctEvPred ev
@@ -205,7 +207,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
@@ -497,34 +499,35 @@ makeSuperClasses :: [Ct] -> TcS [Ct]
-- least produce the immediate superclasses
makeSuperClasses cts = concatMapM go cts
where
- go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
- = mkStrictSuperClasses ev [] [] cls tys
+ go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys, cc_pend_sc = fuel })
+ = assertPpr (fuel > 0) (ppr cls) $ -- fuel needs to be more than 0 always
+ mkStrictSuperClasses (consumeFuel fuel) ev [] [] cls tys
go (CQuantCan (QCI { qci_pred = pred, qci_ev = ev }))
= assertPpr (isClassPred pred) (ppr pred) $ -- The cts should all have
-- class pred heads
- mkStrictSuperClasses ev tvs theta cls tys
+ mkStrictSuperClasses defaultFuelQC 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))
+mkStrictSuperClasses fuel ev tvs theta cls tys
+ = mk_strict_superclasses 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 })
+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 +545,7 @@ 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 }
+ ; mk_superclasses fuel rec_clss given_ev tvs theta sc_pred }
where
sc_pred = classMethodInstTy sel_id tys
@@ -603,7 +606,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 +621,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,29 +636,29 @@ 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
+mk_superclasses fuel rec_clss ev tvs theta pred
| ClassPred cls tys <- classifyPredType pred
- = mk_superclasses_of rec_clss ev tvs theta cls tys
+ = 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
+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
| 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
+ ; sc_cts <- mk_strict_superclasses fuel rec_clss' ev tvs theta cls tys
; return (this_ct : sc_cts) }
-- cc_pend_sc of this_ct = False
where
@@ -664,9 +667,12 @@ mk_superclasses_of rec_clss ev tvs theta cls tys
-- Tuples never contribute to recursion, and can be nested
rec_clss' = rec_clss `extendNameSet` cls_nm
+ this_cc_pend | loop_found = fuel
+ | otherwise = 0
+
this_ct | null tvs, null theta
= CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys
- , cc_pend_sc = loop_found }
+ , cc_pend_sc = this_cc_pend }
-- NB: If there is a loop, we cut off, so we have not
-- added the superclasses, hence cc_pend_sc = True
| otherwise
@@ -827,7 +833,7 @@ 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 { sc_cts <- mkStrictSuperClasses defaultFuelGivens ev tvs theta cls tys
; emitWork sc_cts
; canForAll ev False }
=====================================
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,23 +533,24 @@ 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 })
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -11,6 +11,8 @@ module GHC.Tc.Types.Constraint (
-- Canonical constraints
Xi, Ct(..), Cts,
+ ExpansionFuel, doNotExpand, defaultFuelGivens, defaultFuelWanteds,
+ defaultFuelQC, consumeFuel,
emptyCts, andCts, andManyCts, pprCts,
singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
isEmptyCts,
@@ -191,6 +193,19 @@ type Xi = TcType
type Cts = Bag Ct
+-- | Says how many layers of superclasses can we expand.
+-- see T21909
+type ExpansionFuel = Int
+
+doNotExpand, defaultFuelGivens, defaultFuelWanteds, defaultFuelQC :: ExpansionFuel
+doNotExpand = 0
+defaultFuelQC = 1
+defaultFuelWanteds = 1
+defaultFuelGivens = 3
+
+consumeFuel :: ExpansionFuel -> ExpansionFuel
+consumeFuel fuel = fuel - 1
+
data Ct
-- Atomic canonical constraints
= CDictCan { -- e.g. Num ty
@@ -199,11 +214,10 @@ 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
+ -- n > 0 <=> (a) cc_class has superclasses
+ -- (b) we have not (yet) explored those superclasses
}
| CIrredCan { -- These stand for yet-unusable predicates
@@ -673,8 +687,8 @@ 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)"
@@ -893,16 +907,17 @@ 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 = psc }) = psc > 0
+-- 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,
+-- Says whether this is a CDictCan with cc_pend_sc has fuel left,
-- AND if so flips the flag
-pendingScDict_maybe ct@(CDictCan { cc_pend_sc = True })
- = Just (ct { cc_pend_sc = False })
+pendingScDict_maybe ct@(CDictCan { cc_pend_sc = n })
+ | n > 0 = Just (ct { cc_pend_sc = doNotExpand })
+ | otherwise = Nothing
pendingScDict_maybe _ = Nothing
pendingScInst_maybe :: QCInst -> Maybe QCInst
@@ -932,7 +947,7 @@ getPendingWantedScs simples
= mapAccumBagL get [] simples
where
get acc ct | Just ct' <- pendingScDict_maybe ct
- = (ct':acc, ct')
+ = (ct:acc, ct')
| otherwise
= (acc, ct)
=====================================
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,14 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableSuperClasses, FunctionalDependencies, MultiParamTypeClasses, GADTs #-}
+
+module T21909b where
+
+import Data.Kind
+
+class C [a] => C a where
+ foo :: a -> Int
+
+should_work :: C a => a -> Int
+should_work x = foolocal x
+ where
+ foolocal a = foo a
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -857,3 +857,5 @@ test('T22647', normal, compile, [''])
test('T19577', normal, compile, [''])
test('T22383', normal, compile, [''])
test('T21501', normal, compile, [''])
+test('T21909', normal, compile, [''])
+test('T21909b', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/bd4624de94c4d526e83fff095e4139dceb7f39a4
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/bd4624de94c4d526e83fff095e4139dceb7f39a4
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/20230207/74141dc0/attachment-0001.html>
More information about the ghc-commits
mailing list