[Git][ghc/ghc][wip/T23070-dicts] Fixes
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Fri May 12 12:58:06 UTC 2023
Simon Peyton Jones pushed to branch wip/T23070-dicts at Glasgow Haskell Compiler / GHC
Commits:
e9d00762 by Simon Peyton Jones at 2023-05-12T13:59:53+01:00
Fixes
- - - - -
7 changed files:
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Irred.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Solver/Solve.hs
- compiler/GHC/Tc/Types/Constraint.hs
Changes:
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -81,7 +81,7 @@ solveDict dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = tys })
; tryFunDeps dict_ct
; tryLastResortProhibitedSuperClass dict_ct
; simpleStage (updInertDicts dict_ct)
- ; Stage (stopWith (dictCtEvidence dict_ct) "Kept inert DictCt") }
+ ; stopWithStage (dictCtEvidence dict_ct) "Kept inert DictCt" }
updInertDicts :: DictCt -> TcS ()
updInertDicts dict_ct@(DictCt { di_cls = cls, di_ev = ev })
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -8,10 +8,10 @@ module GHC.Tc.Solver.Equality(
import GHC.Prelude
+import GHC.Tc.Solver.Irred( solveIrred )
+import GHC.Tc.Solver.Dict( matchLocalInst, chooseInstance )
import GHC.Tc.Solver.Rewrite
import GHC.Tc.Solver.Monad
-import GHC.Tc.Solver.Irred( tryInertIrreds )
-import GHC.Tc.Solver.Dict( matchLocalInst, chooseInstance )
import GHC.Tc.Solver.InertSet
import GHC.Tc.Solver.Types( findFunEqsByTyCon )
import GHC.Tc.Types.Evidence
@@ -122,14 +122,14 @@ solveEquality ev eq_rel ty1 ty2
Right eq_ct -> do { tryInertEqs eq_ct
; tryFunDeps eq_ct
; tryQCsEqCt eq_ct
- ; simpleStage (updInertEqs eq_ct) } } }
+ ; simpleStage (updInertEqs eq_ct)
+ ; stopWithStage (eqCtEvidence eq_ct) "Kept inert EqCt" } } }
updInertEqs :: EqCt -> TcS ()
-updInertEqs eq_ct@(EqCt { eq_lhs = lhs, eq_ev = ev, eq_eq_rel = eq_rel })
- = do { ics <- getInertCans
- ; (_, ics') <- kickOutRewritable (ctEvFlavour ev, eq_rel) lhs ics
- ; tclvl <- getTcLevel
- ; updInertCans (updateGivenEqs tc_lvl (CEqCan eq_ct) .
+updInertEqs eq_ct
+ = do { _n_kicked <- kickOutRewritable (eqCtFlavourRole eq_ct) (eqCtLHS eq_ct)
+ ; tc_lvl <- getTcLevel
+ ; updInertCans (updGivenEqs tc_lvl (CEqCan eq_ct) .
addEqToCans eq_ct)
}
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -21,7 +21,7 @@ module GHC.Tc.Solver.InertSet (
addInertItem, addInertDict,
noMatchableGivenDicts,
- noGivenNewtypeReprEqs,
+ noGivenNewtypeReprEqs, updGivenEqs,
mightEqualLater,
prohibitedSuperClassSolve,
@@ -37,7 +37,7 @@ module GHC.Tc.Solver.InertSet (
-- * Inert Irreds
InertIrreds, delIrred, addIrreds, addIrred, foldIrreds,
- findMatchingIrreds,
+ findMatchingIrreds, updIrreds,
-- * Kick-out
kickOutRewritableLHS,
@@ -591,7 +591,7 @@ InertCans tracks
-- (see Note [Unification preconditions] in GHC.Tc.Utils.Unify).
We update inert_given_eq_lvl whenever we add a Given to the
-inert set, in updateGivenEqs.
+inert set, in updGivenEqs.
Then a unification variable alpha[n] is untouchable iff
n < inert_given_eq_lvl
@@ -617,7 +617,7 @@ should update inert_given_eq_lvl?
same example again, but this time we have /not/ yet unified beta:
forall[2] beta[1] => ...blah...
- Because beta might turn into an equality, updateGivenEqs conservatively
+ Because beta might turn into an equality, updGivenEqs conservatively
treats it as a potential equality, and updates inert_give_eq_lvl
* What about something like forall[2] a b. a ~ F b => [W] alpha[1] ~ X y z?
@@ -627,7 +627,7 @@ should update inert_given_eq_lvl?
implication. Such equalities need not make alpha untouchable. (Test
case typecheck/should_compile/LocalGivenEqs has a real-life
motivating example, with some detailed commentary.)
- Hence the 'mentionsOuterVar' test in updateGivenEqs.
+ Hence the 'mentionsOuterVar' test in updGivenEqs.
However, solely to support better error messages
(see Note [HasGivenEqs] in GHC.Tc.Types.Constraint) we also track
@@ -1431,13 +1431,13 @@ addInertItem :: TcLevel -> InertCans -> Ct -> InertCans
addInertItem tc_lvl
ics@(IC { inert_funeqs = funeqs, inert_eqs = eqs })
item@(CEqCan eq_ct)
- = updateGivenEqs tc_lvl item $
+ = updGivenEqs tc_lvl item $
case eq_lhs eq_ct of
TyFamLHS tc tys -> ics { inert_funeqs = addCanFunEq funeqs tc tys eq_ct }
TyVarLHS tv -> ics { inert_eqs = addTyEq eqs tv eq_ct }
addInertItem tc_lvl ics@(IC { inert_irreds = irreds }) ct@(CIrredCan irred)
- = updateGivenEqs tc_lvl ct $ -- An Irred might turn out to be an
+ = updGivenEqs tc_lvl ct $ -- An Irred might turn out to be an
-- equality, so we play safe
ics { inert_irreds = irreds `snocBag` irred }
@@ -1450,12 +1450,12 @@ addInertItem _ _ item
addInertDict :: DictCt -> InertCans -> InertCans
addInertDict dict ics = ics { inert_dicts = addDict dict (inert_dicts ics) }
-updateGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans
+updGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans
-- Set the inert_given_eq_level to the current level (tclvl)
-- if the constraint is a given equality that should prevent
-- filling in an outer unification variable.
-- See Note [Tracking Given equalities]
-updateGivenEqs tclvl ct inerts@(IC { inert_given_eq_lvl = ge_lvl })
+updGivenEqs tclvl ct inerts@(IC { inert_given_eq_lvl = ge_lvl })
| not (isGivenCt ct) = inerts
| not_equality ct = inerts -- See Note [Let-bound skolems]
| otherwise = inerts { inert_given_eq_lvl = ge_lvl'
=====================================
compiler/GHC/Tc/Solver/Irred.hs
=====================================
@@ -35,16 +35,14 @@ solveIrred :: IrredCt -> SolverStage ()
solveIrred irred
= do { tryInertIrreds irred
; tryQCsIrredCt irred
- ; simpleStage (updInertIrreds irred) }
-
+ ; simpleStage (updInertIrreds irred)
+ ; stopWithStage (irredCtEvidence irred) "Kept inert IrredCt" }
updInertIrreds :: IrredCt -> TcS ()
updInertIrreds irred
= do { tc_lvl <- getTcLevel
- ; updInertCans $ (updateGivenEqs tc_lvl (CIrredCan irred) .
- updIrreds (addIrred irred))
- ; traceFireTcS (irredCtEvidence irred)
- (text "Added Irred to inert set") }
+ ; updInertCans $ (updGivenEqs tc_lvl (CIrredCan irred) .
+ updIrreds (addIrred irred)) }
{- *********************************************************************
* *
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -34,6 +34,7 @@ module GHC.Tc.Solver.Monad (
-- The pipeline
StopOrContinue(..), continueWith, stopWith,
startAgainWith, SolverStage(Stage, runSolverStage), simpleStage,
+ stopWithStage,
-- Tracing etc
panicTcS, traceTcS,
@@ -71,12 +72,12 @@ module GHC.Tc.Solver.Monad (
getTcSInerts, setTcSInerts,
getUnsolvedInerts,
removeInertCts, getPendingGivenScs,
- addInertCan, insertFunEq, addInertForAll,
+ insertFunEq, addInertForAll,
emitWorkNC, emitWork,
lookupInertDict,
-- The Model
- kickOutAfterUnification,
+ kickOutAfterUnification, kickOutRewritable,
-- Inert Safe Haskell safe-overlap failures
addInertSafehask, insertSafeOverlapFailureTcS, updInertSafehask,
@@ -252,6 +253,9 @@ continueWith ct = return (ContinueWith ct)
stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
stopWith ev s = return (Stop ev (text s))
+stopWithStage :: CtEvidence -> String -> SolverStage a
+stopWithStage ev s = Stage (stopWith ev s)
+
{- *********************************************************************
* *
@@ -325,6 +329,7 @@ When adding an equality to the inerts:
-}
+{-
addInertCan :: Ct -> TcS ()
-- Precondition: item /is/ canonical
-- See Note [Adding an equality to the InertCans]
@@ -349,16 +354,18 @@ maybeKickOut ics ct
| otherwise
= return ics
+-}
-----------------------------------------
kickOutRewritable :: CtFlavourRole -- Flavour/role of the equality that
-- is being added to the inert set
-> CanEqLHS -- The new equality is lhs ~ ty
- -> InertCans
- -> TcS (Int, InertCans)
-kickOutRewritable new_fr new_lhs ics
- = do { let (kicked_out, ics') = kickOutRewritableLHS new_fr new_lhs ics
+ -> TcS Int
+kickOutRewritable new_fr new_lhs
+ = do { ics <- getInertCans
+ ; let (kicked_out, ics') = kickOutRewritableLHS new_fr new_lhs ics
n_kicked = lengthBag kicked_out
+ ; setInertCans ics'
; unless (isEmptyBag kicked_out) $
do { emitWork kicked_out
@@ -385,18 +392,13 @@ kickOutRewritable new_fr new_lhs ics
, text "kicked_out =" <+> ppr kicked_out
, text "Residual inerts =" <+> ppr ics' ]) }
- ; return (n_kicked, ics') }
+ ; return n_kicked }
kickOutAfterUnification :: TcTyVar -> TcS Int
kickOutAfterUnification new_tv
- = do { ics <- getInertCans
- ; (n_kicked, ics2) <- kickOutRewritable (Given,NomEq)
- (TyVarLHS new_tv) ics
- -- Given because the tv := xi is given; NomEq because
- -- only nominal equalities are solved by unification
-
- ; setInertCans ics2
- ; return n_kicked }
+ = kickOutRewritable (Given,NomEq) (TyVarLHS new_tv)
+ -- Given because the tv := xi is given; NomEq because
+ -- only nominal equalities are solved by unification
-- See Wrinkle (W2a) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality
-- It's possible that this could just go ahead and unify, but could there be occurs-check
=====================================
compiler/GHC/Tc/Solver/Solve.hs
=====================================
@@ -569,8 +569,8 @@ runTcPluginsGiven
do { p <- runTcPluginSolvers solvers (givens,[])
; let (solved_givens, _) = pluginSolvedCts p
insols = map (ctIrredCt PluginReason) (pluginBadCts p)
- ; updInertCans (removeInertCts solved_givens)
- ; updInertIrreds (addIrreds insols)
+ ; updInertCans (removeInertCts solved_givens .
+ updIrreds (addIrreds insols) )
; return (pluginNewCts p) } } }
-- | Given a bag of (rewritten, zonked) wanteds, invoke the plugins on
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -6,11 +6,8 @@
-- | This module defines types and simple operations over constraints, as used
-- in the type-checker and constraint solver.
module GHC.Tc.Types.Constraint (
- -- QCInst
- QCInst(..), pendingScInst_maybe,
-
- -- Canonical constraints
- Xi, Ct(..), EqCt(..), Cts,
+ -- Constraints
+ Xi, Ct(..), Cts,
singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
isEmptyCts, emptyCts, andCts, ctsPreds,
isPendingScDictCt, isPendingScDict, pendingScDict_maybe,
@@ -23,14 +20,16 @@ module GHC.Tc.Types.Constraint (
ctRewriters,
ctEvId, wantedEvId_maybe, mkTcEqPredLikeEv,
mkNonCanonical, mkGivens,
- ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
- ctEvExpr, ctEvTerm, ctEvCoercion, ctEvEvId,
- ctEvRewriters,
tyCoVarsOfCt, tyCoVarsOfCts,
tyCoVarsOfCtList, tyCoVarsOfCtsList,
- DictCt(..), dictCtEvidence,
- IrredCt(..), mkIrredCt, ctIrredCt, irredCtEvidence, irredCtPred,
+ -- Particular forms of constraint
+ EqCt(..), eqCtEvidence, eqCtLHS,
+ DictCt(..), dictCtEvidence,
+ IrredCt(..), irredCtEvidence, mkIrredCt, ctIrredCt, irredCtPred,
+
+ -- QCInst
+ QCInst(..), pendingScInst_maybe,
ExpansionFuel, doNotExpand, consumeFuel, pendingFuel,
assertFuelPrecondition, assertFuelPreconditionStrict,
@@ -75,12 +74,15 @@ module GHC.Tc.Types.Constraint (
-- CtEvidence
CtEvidence(..), TcEvDest(..),
- mkKindEqLoc, toKindLoc, toInvisibleLoc, mkGivenLoc,
isWanted, isGiven,
+ ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
+ ctEvExpr, ctEvTerm, ctEvCoercion, ctEvEvId,
+ ctEvRewriters, ctEvUnique, tcEvDestUnique,
+ mkKindEqLoc, toKindLoc, toInvisibleLoc, mkGivenLoc,
ctEvRole, setCtEvPredType, setCtEvLoc, arisesFromGivens,
tyCoVarsOfCtEvList, tyCoVarsOfCtEv, tyCoVarsOfCtEvsList,
- ctEvUnique, tcEvDestUnique,
+ -- RewriterSet
RewriterSet(..), emptyRewriterSet, isEmptyRewriterSet,
-- exported concretely only for anyUnfilledCoercionHoles
addRewriter, unitRewriterSet, unionRewriterSet, rewriterSetFromCts,
@@ -300,6 +302,12 @@ instance Outputable CanEqLHS where
ppr (TyVarLHS tv) = ppr tv
ppr (TyFamLHS fam_tc fam_args) = ppr (mkTyConApp fam_tc fam_args)
+eqCtEvidence :: EqCt -> CtEvidence
+eqCtEvidence = eq_ev
+
+eqCtLHS :: EqCt -> CanEqLHS
+eqCtLHS = eq_lhs
+
--------------- IrredCt --------------
data IrredCt -- These stand for yet-unusable predicates
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e9d00762824ef56c779625597acb7536f0425e89
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e9d00762824ef56c779625597acb7536f0425e89
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/20230512/b7cb549d/attachment-0001.html>
More information about the ghc-commits
mailing list