[Git][ghc/ghc][wip/T23070-dicts] More wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Thu May 18 15:21:34 UTC 2023
Simon Peyton Jones pushed to branch wip/T23070-dicts at Glasgow Haskell Compiler / GHC
Commits:
b03cc67f by Simon Peyton Jones at 2023-05-18T16:23:21+01:00
More wibbles
- - - - -
6 changed files:
- compiler/GHC/Core/Opt/Arity.hs
- compiler/GHC/Core/Predicate.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Irred.hs
- compiler/GHC/Tc/Solver/Monad.hs
Changes:
=====================================
compiler/GHC/Core/Opt/Arity.hs
=====================================
@@ -1874,7 +1874,7 @@ The no-crap way is
\(y::Int). let j' :: Int -> Bool
j' x = e y
in b[j'/j] y
-where I have written to stress that j's type has
+where I have written b[j'/j] to stress that j's type has
changed. Note that (of course!) we have to push the application
inside the RHS of the join as well as into the body. AND if j
has an unfolding we have to push it into there too. AND j might
=====================================
compiler/GHC/Core/Predicate.hs
=====================================
@@ -343,7 +343,7 @@ initIPRecTc = setRecTcMaxBound 1 initRecTc
{- Note [Local implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-See also Note [Shadowing of Implicit Parameters] in GHC.Tc.Solver.Dict.
+See also Note [Shadowing of implicit parameters] in GHC.Tc.Solver.Dict.
The function isIPLikePred tells if this predicate, or any of its
superclasses, is an implicit parameter.
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -109,7 +109,7 @@ updInertDicts :: DictCt -> TcS ()
updInertDicts dict_ct@(DictCt { di_cls = cls, di_ev = ev, di_tys = tys })
= do { traceTcS "Adding inert dict" (ppr dict_ct $$ ppr cls <+> ppr tys)
- -- See Note [Shadowing of Implicit Parameters]
+ -- See Note [Shadowing of implicit parameters]
; when (isGiven ev && isIPClass cls) $
updInertCans (updDicts (delIPDict dict_ct))
@@ -187,7 +187,7 @@ solveCallStack ev ev_cs
; setEvBindIfWanted ev IsCoherent ev_tm }
-{- Note [Shadowing of Implicit Parameters]
+{- Note [Shadowing of implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we add a new /given/ implicit parameter to the inert set, it /replaces/
any existing givens for the same implicit parameter. This makes a difference
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -2133,7 +2133,8 @@ solveOneFromTheOther ct_i ct_w
| isIPLikePred pred = if lvl_w > lvl_i then KeepWork else KeepInert
| otherwise = if lvl_w > lvl_i then KeepInert else KeepWork
-- See Note [Replacement vs keeping] part (1)
- -- For the isIPLikePred case see Note [Shadowing of Implicit Parameters]
+ -- For the isIPLikePred case see Note [Shadowing of implicit parameters]
+ -- in GHC.Tc.Solver.Dict
same_level_strategy -- Both Given
= case (orig_i, orig_w) of
@@ -2162,7 +2163,7 @@ solveOneFromTheOther.
- For implicit parameters we want to keep the innermost (deepest)
one, so that it overrides the outer one.
- See Note [Shadowing of Implicit Parameters]
+ See Note [Shadowing of implicit parameters] in GHC.Tc.Solver.Dict
- For everything else, we want to keep the outermost one. Reason: that
makes it more likely that the inner one will turn out to be unused,
=====================================
compiler/GHC/Tc/Solver/Irred.hs
=====================================
@@ -64,11 +64,12 @@ try_inert_irreds :: InertCans -> IrredCt -> TcS (StopOrContinue ())
try_inert_irreds inerts irred_w@(IrredCt { ir_ev = ev_w, ir_reason = reason })
| let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w
- , ((irred_i, swap) : _rest) <- bagToList matching_irreds
+ , ((irred_i, swap) : _rest) <- pprTrace "try_inert_irreds" (ppr ev_w $$ ppr matching_irreds) $
+ bagToList matching_irreds
-- See Note [Multiple matching irreds]
, let ev_i = irredCtEvidence irred_i
ct_i = CIrredCan irred_i
- , not (isInsolubleReason reason && (isWanted ev_i || isWanted ev_w))
+ , not (isInsolubleReason reason) || isGiven ev_i || isGiven ev_w
-- See Note [Insoluble irreds]
= do { traceTcS "iteractIrred" $
vcat [ text "wanted:" <+> (ppr ct_w $$ ppr (ctOrigin ct_w))
@@ -113,6 +114,7 @@ so that we get distinct error messages with -fdefer-type-errors
However we do allow an insoluble constraint to be solved from an insoluble
Given. This might seem a little odd, but it's very much a corner case, and
it helps in tests bkpfail24.run, T15450, GivenForallLoop, T20189, T8392a.
+See #23413.
-}
{- *********************************************************************
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -207,13 +207,51 @@ import GHC.Data.Graph.Directed
* *
********************************************************************* -}
+{- Note [The SolverStage monad]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The SolverStage monad allows us to write simple code like this:
+
+ solveEquality :: ... -> SolverStage Void
+ solveEquality ev eq_rel ty1 ty2
+ = do { Pair ty1' ty2' <- zonkEqTypes ev eq_rel ty1 ty2
+ ; mb_canon <- canonicaliseEquality ev' eq_rel ty1' ty2'
+ ; case mb_canon of {
+ Left irred_ct -> do { tryQCsIrredEqCt irred_ct
+ ; solveIrred irred_ct } ;
+ Right eq_ct -> do { tryInertEqs eq_ct
+ ; tryFunDeps eq_ct
+ ; tryQCsEqCt eq_ct
+ ; simpleStage (updInertEqs eq_ct)
+ ; stopWithStage (eqCtEvidence eq_ct) "Kept inert EqCt" } } }
+
+in which each sub-stage can elect to
+ (a) ContinueWith: continue to the next stasge
+ (b) StartAgain: start again at the beginning of the pipeline
+ (c) Stop: stop altogether; constraint is solved
+
+These three possiblities are described by the `StopOrContinue` data type.
+The `SolverStage` monad does the plumbing.
+
+Notes:
+
+(SM1) Each individual stage pretty quickly drops down into
+ TcS (StopOrContinue a)
+ because the monadic plumbing of `SolverStage` is relatively ineffienct,
+ with that three-way split.
+
+(SM2) We use `SolverStage Void` to express the idea that ContinueWith is
+ impossible; we don't need to pattern match on it as a possible outcome:A
+ see GHC.Tc.Solver.Solve.solveOne. To that end, ContinueWith is strict.
+-}
+
data StopOrContinue a
= StartAgain Ct -- Constraint is not solved, but some unifications
-- happened, so go back to the beginning of the pipeline
| ContinueWith !a -- The constraint was not solved, although it may have
-- been rewritten. It is strict so that
- -- ContinueWith Void can't happen
+ -- ContinueWith Void can't happen; see (SM2) in
+ -- Note [The SolverStage monad]
| Stop CtEvidence -- The (rewritten) constraint was solved
SDoc -- Tells how it was solved
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b03cc67fd7ea06cd25bd92875e5cdcd4ff2a8505
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b03cc67fd7ea06cd25bd92875e5cdcd4ff2a8505
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/20230518/81229e3e/attachment-0001.html>
More information about the ghc-commits
mailing list