[Git][ghc/ghc][wip/T23070-dicts] After talking to Richard
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Mon May 15 22:57:34 UTC 2023
Simon Peyton Jones pushed to branch wip/T23070-dicts at Glasgow Haskell Compiler / GHC
Commits:
b9673b56 by Simon Peyton Jones at 2023-05-15T23:56:23+01:00
After talking to Richard
* Use SimplifierStage Void when no ContinueWith
* Fast path for equality classes
- - - - -
8 changed files:
- compiler/GHC/Tc/Instance/Class.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Irred.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Solver/Solve.hs
- compiler/GHC/Utils/Outputable.hs
- testsuite/tests/quantified-constraints/T17267b.hs
Changes:
=====================================
compiler/GHC/Tc/Instance/Class.hs
=====================================
@@ -2,7 +2,7 @@
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module GHC.Tc.Instance.Class (
- matchGlobalInst,
+ matchGlobalInst, matchEqualityInst,
ClsInstResult(..),
safeOverlap, instanceReturnsDictCon,
AssocInstInfo(..), isNotAssociated,
@@ -127,9 +127,6 @@ matchGlobalInst dflags short_cut clas tys
| isCTupleClass clas = matchCTuple clas tys
| cls_name == typeableClassName = matchTypeable clas tys
| cls_name == withDictClassName = matchWithDict tys
- | clas `hasKey` heqTyConKey = matchHeteroEquality tys
- | clas `hasKey` eqTyConKey = matchHomoEquality tys
- | clas `hasKey` coercibleTyConKey = matchCoercible tys
| cls_name == hasFieldClassName = matchHasField dflags short_cut clas tys
| cls_name == unsatisfiableClassName = return NoInstance -- See (B) in Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors
| otherwise = matchInstEnv dflags short_cut clas tys
@@ -798,33 +795,24 @@ if you'd written
***********************************************************************-}
-- See also Note [The equality types story] in GHC.Builtin.Types.Prim
-matchHeteroEquality :: [Type] -> TcM ClsInstResult
--- Solves (t1 ~~ t2)
-matchHeteroEquality args
- = return (OneInst { cir_new_theta = [ mkTyConApp eqPrimTyCon args ]
- , cir_mk_ev = evDataConApp heqDataCon args
- , cir_coherence = IsCoherent
- , cir_what = BuiltinEqInstance })
+matchEqualityInst :: Class -> [Type] -> (DataCon, Role, Type, Type)
-matchHomoEquality :: [Type] -> TcM ClsInstResult
--- Solves (t1 ~ t2)
-matchHomoEquality args@[k,t1,t2]
- = return (OneInst { cir_new_theta = [ mkTyConApp eqPrimTyCon [k,k,t1,t2] ]
- , cir_mk_ev = evDataConApp eqDataCon args
- , cir_coherence = IsCoherent
- , cir_what = BuiltinEqInstance })
-matchHomoEquality args = pprPanic "matchHomoEquality" (ppr args)
+matchEqualityInst cls args
+ | cls `hasKey` eqTyConKey -- Solves (t1 ~ t2)
+ , [_,t1,t2] <- args
+ = (eqDataCon, Nominal, t1, t2)
+
+ | cls `hasKey` heqTyConKey -- Solves (t1 ~~ t2)
+ , [_,_,t1,t2] <- args
+ = (heqDataCon, Nominal, t1, t2)
+
+ | cls `hasKey` coercibleTyConKey -- Solves (Coercible t1 t2)
+ , [_, t1, t2] <- args
+ = (coercibleDataCon, Representational, t1, t2)
+
+ | otherwise
+ = pprPanic "matchEqualityInst" (ppr (mkClassPred cls args))
--- See also Note [The equality types story] in GHC.Builtin.Types.Prim
-matchCoercible :: [Type] -> TcM ClsInstResult
-matchCoercible args@[k, t1, t2]
- = return (OneInst { cir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
- , cir_mk_ev = evDataConApp coercibleDataCon args
- , cir_coherence = IsCoherent
- , cir_what = BuiltinEqInstance })
- where
- args' = [k, k, t1, t2]
-matchCoercible args = pprPanic "matchLiftedCoercible" (ppr args)
{- ********************************************************************
* *
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -10,9 +10,8 @@ module GHC.Tc.Solver.Dict (
import GHC.Prelude
import GHC.Tc.Errors.Types
-import GHC.Tc.Utils.TcType
import GHC.Tc.Instance.FunDeps
-import GHC.Tc.Instance.Class( safeOverlap )
+import GHC.Tc.Instance.Class( safeOverlap, matchEqualityInst )
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Origin
@@ -20,6 +19,8 @@ import GHC.Tc.Types.EvTerm( evCallStack )
import GHC.Tc.Solver.InertSet
import GHC.Tc.Solver.Monad
import GHC.Tc.Solver.Types
+import GHC.Tc.Utils.TcType
+import GHC.Tc.Utils.Unify( uType )
import GHC.Hs.Type( HsIPName(..) )
@@ -53,6 +54,7 @@ import GHC.Driver.Session
import qualified GHC.LanguageExtensions as LangExt
import Data.Maybe ( listToMaybe, mapMaybe, isJust )
+import Data.Void( Void )
import Control.Monad.Trans.Maybe( MaybeT, runMaybeT )
import Control.Monad.Trans.Class( lift )
@@ -65,15 +67,27 @@ import Control.Monad( mzero, when )
* *
********************************************************************* -}
-solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage ()
+{- Note [Solving equality classes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We have a special solver for the "equality classes"
+ (t1 ~ t2), (t1 ~~ t2), and (Coercible t1 t2)
+
+ TODO: expand this Note
+-}
+
+solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage Void
-- NC: this comes from CNonCanonical or CIrredCan
-- Precondition: already rewritten by inert set
solveDictNC ev cls tys
+ | isEqualityClass cls
+ = solveEqualityDict ev cls tys
+
+ | otherwise
= do { simpleStage $ traceTcS "solveDictNC" (ppr (mkClassPred cls tys) $$ ppr ev)
; dict_ct <- canDictCt ev cls tys
; solveDict dict_ct }
-solveDict :: DictCt -> SolverStage ()
+solveDict :: DictCt -> SolverStage Void
-- Preconditions: `tys` are already rewritten by the inert set
solveDict dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = tys })
= assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $
@@ -96,7 +110,7 @@ solveDict dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = tys })
updInertDicts :: DictCt -> TcS ()
updInertDicts dict_ct@(DictCt { di_cls = cls, di_ev = ev })
- = do { -- See [Kick out existing binding for implicit parameter]
+ = do { -- See Note [Shadowing of Implicit Parameters]
; when (isGiven ev && isIPClass cls) $
updInertCans (updDicts (delIPDict dict_ct))
@@ -113,19 +127,10 @@ canDictCt ev cls tys
do { dflags <- getDynFlags
; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev [] [] cls tys
-- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel]
+ ; emitWork (listToBag sc_cts)
- -- For equality classes, /replace/ the current constraint with its
- -- superclasses, rather than /adding/ them.
- -- See (NC1) in Note [Naturally coherent classes]
- ; if isEqualityClass cls
- then case sc_cts of
- [ct] -> startAgainWith ct
- _ -> pprPanic "canDictCt" (ppr cls)
- else
-
- do { emitWork (listToBag sc_cts)
; continueWith (DictCt { di_ev = ev, di_cls = cls
- , di_tys = tys, di_pend_sc = doNotExpand }) } }
+ , di_tys = tys, di_pend_sc = doNotExpand }) }
-- doNotExpand: We have already expanded superclasses for /this/ dict
-- so set the fuel to doNotExpand to avoid repeating expansion
@@ -183,10 +188,17 @@ solveCallStack ev ev_cs
; setEvBindIfWanted ev IsCoherent ev_tm }
-{- Note [Kick out existing binding for implicit parameter]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- 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.
+any existing givens for the same implicit parameter. This makes a difference
+in two places:
+
+* In `GHC.Tc.Solver.InertSet.solveOneFromTheOther`, be careful when we have
+ (?x :: ty) in the inert set and an identical (?x :: ty) as the work item.
+
+* In `updInertDicts` in this module, when adding [G] (?x :: ty), remove any
+ existing [G] (?x :: ty'), regardless of ty'
Example 1:
@@ -263,6 +275,37 @@ I can think of two ways to fix this:
-}
+{- ******************************************************************************
+* *
+ solveEqualityDict
+* *
+****************************************************************************** -}
+
+solveEqualityDict :: CtEvidence -> Class -> [Type] -> SolverStage Void
+-- Precondition: (isEqualityClass cls) True, so cls is (~), (~~), or Coercible
+solveEqualityDict ev cls tys
+ | CtWanted { ctev_dest = dest } <- ev
+ = Stage $
+ do { let (data_con, role, t1, t2) = matchEqualityInst cls tys
+ -- Unify t1~t2, putting anything that can't be solved
+ -- immediately into the work list
+ ; (co, _, _) <- wrapUnifierTcS ev role $ \uenv ->
+ uType uenv t1 t2
+ -- Set d :: (t1~t2) = Eq# co
+ ; setWantedEvTerm dest IsCoherent $
+ evDataConApp data_con tys [Coercion co]
+ ; stopWith ev "Solved wanted lifted equality" }
+
+ | CtGiven { ctev_evar = ev_id, ctev_loc = loc } <- ev
+ , [sel_id] <- classSCSelIds cls -- Equality classes have just one superclass
+ = Stage $
+ do { let sc_pred = classMethodInstTy sel_id tys
+ ev_expr = EvExpr $ Var sel_id `mkTyApps` tys `App` evId ev_id
+ ; given_ev <- newGivenEvVar loc (sc_pred, ev_expr)
+ ; startAgainWith (mkNonCanonical given_ev) }
+ | otherwise
+ = pprPanic "solveEqualityDict" (ppr cls)
+
{- ******************************************************************************
* *
interactDict
@@ -770,7 +813,6 @@ matchClassInst dflags inerts clas tys loc
-- whether top level, or local quantified constraints.
-- See Note [Instance and Given overlap]
| not (xopt LangExt.IncoherentInstances dflags)
- , not (naturallyCoherentClass clas) -- See (NC3) in Note [Naturally coherent classes]
, not (noMatchableGivenDicts inerts loc clas tys)
= do { traceTcS "Delaying instance application" $
vcat [ text "Work item=" <+> pprClassPred clas tys ]
@@ -796,6 +838,7 @@ matchClassInst dflags inerts clas tys loc
where
pred = mkClassPred clas tys
+{-
-- | If a class is "naturally coherent", then we needn't worry at all, in any
-- way, about overlapping/incoherent instances. Just solve the thing!
-- See Note [Naturally coherent classes]
@@ -803,6 +846,7 @@ matchClassInst dflags inerts clas tys loc
naturallyCoherentClass :: Class -> Bool
naturallyCoherentClass cls
= isCTupleClass cls || isEqualityClass cls
+-}
isEqualityClass :: Class -> Bool
-- True of (~), (~~), and Coercible
@@ -903,14 +947,15 @@ this:
(See Note [The equality types story] in GHC.Builtin.Types.Prim.)
PS: the term "naturally coherent" doesn't really seem helpful.
-Perhaps "invertible" or something? I left it for now though.
+Perhaps "invertible" or "bidirectional" or something? I left it for
+now though.
For naturally coherent classes:
-(NC1) For Givens, when expanding superclasses, we /replace/ the constraint
- with its superclasses (which, remember, are equally powerful) rather than
- /adding/ them. This can make a huge difference. Consider T17836, which
- has a constraint like
+(NC1) For Givens, when expanding the superclasses of a naturally coherent class,
+ we can /replace/ the constraint with its superclasses (which, remember, are
+ equally powerful) rather than /adding/ them. This can make a huge difference.
+ Consider T17836, which has a constraint like
forall b,c. a ~ (b,c) =>
forall d,e. c ~ (d,e) =>
...etc...
@@ -923,7 +968,7 @@ For naturally coherent classes:
Originally I tried this for all naturally-coherent classes, including
tuples. But discarding the tuple Given (which "replacing" does) means that
we may have to reconstruct it for a recursive call, and the optimiser isn't
- quite clever enought to figure that out: see #10359 and its test case.
+ quite clever enough to figure that out: see #10359 and its test case.
This is less pressing for equality classes because they have to be unpacked
strictly, so CSE-ing away the reconstuction works fine. Hence the use
of isEqualityClass rather than naturallyCoherentClass in canDictCt.
@@ -944,7 +989,7 @@ For naturally coherent classes:
so the reduction of the [W] constraint does not risk losing any solutions.
On the other hand, it can be fatal to /fail/ to reduce such equalities
- on the grounds of Note [Instance and Given overlap], fbecause many good
+ on the grounds of Note [Instance and Given overlap], because many good
things flow from [W] t1 ~# t2.
The same reasoning applies to
@@ -1923,8 +1968,8 @@ mk_strict_superclasses fuel rec_clss ev@(CtGiven { ctev_evar = evar, ctev_loc =
| otherwise
= do { given_ev <- newGivenEvVar sc_loc $
mk_given_desc sel_id sc_pred
- ; assertFuelPrecondition fuel
- $ mk_superclasses fuel rec_clss given_ev tvs theta sc_pred }
+ ; assertFuelPrecondition fuel $
+ mk_superclasses fuel rec_clss given_ev tvs theta sc_pred }
where
sc_pred = classMethodInstTy sel_id tys
@@ -1952,7 +1997,7 @@ mk_strict_superclasses fuel rec_clss ev@(CtGiven { ctev_evar = evar, ctev_loc =
`App` (evId evar `mkVarApps` (tvs ++ dict_ids))
`mkVarApps` sc_tvs
- sc_loc | naturallyCoherentClass cls
+ sc_loc | isCTupleClass cls
= loc -- See (NC2) in Note [Naturally coherent classes]
| otherwise
= loc { ctl_origin = mk_sc_origin (ctLocOrigin loc) }
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -60,7 +60,7 @@ import Data.List ( zip4 )
import qualified Data.Semigroup as S
import Data.Bifunctor ( bimap )
-
+import Data.Void( Void )
{- *********************************************************************
* *
@@ -102,7 +102,7 @@ indeed they are!
-}
solveEquality :: CtEvidence -> EqRel -> Type -> Type
- -> SolverStage ()
+ -> SolverStage Void
solveEquality ev eq_rel ty1 ty2
= do { Pair ty1' ty2' <- zonkEqTypes ev eq_rel ty1 ty2
; let ev' | debugIsOn = setCtEvPredType ev $
=====================================
compiler/GHC/Tc/Solver/Irred.hs
=====================================
@@ -21,9 +21,10 @@ import GHC.Types.Basic( SwapFlag(..) )
import GHC.Utils.Outputable
-
import GHC.Data.Bag
+import Data.Void( Void )
+
{- *********************************************************************
* *
@@ -31,7 +32,7 @@ import GHC.Data.Bag
* *
********************************************************************* -}
-solveIrred :: IrredCt -> SolverStage ()
+solveIrred :: IrredCt -> SolverStage Void
solveIrred irred
= do { simpleStage $ traceTcS "solveIrred:" (ppr irred)
; tryInertIrreds irred
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -211,8 +211,9 @@ 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
+ | ContinueWith !a -- The constraint was not solved, although it may have
+ -- been rewritten. It is strict so that
+ -- ContinueWith Void can't happen
| Stop CtEvidence -- The (rewritten) constraint was solved
SDoc -- Tells how it was solved
=====================================
compiler/GHC/Tc/Solver/Solve.hs
=====================================
@@ -43,6 +43,7 @@ import Data.List( deleteFirstsBy )
import Control.Monad
import Data.Semigroup as S
+import Data.Void( Void )
{-
**********************************************************************
@@ -196,7 +197,10 @@ solveOne workItem
; traceTcS "End solver pipeline }" empty
; return () }
- ContinueWith {} -> pprPanic "Pipeline finished without solving" (ppr ct) }
+ -- ContinueWith can't happen: res :: SolverStage Void
+ -- solveCt either solves the constraint, or puts
+ -- the unsolved constraint in the inert set.
+ }
{- *********************************************************************
* *
@@ -224,7 +228,9 @@ it must be recanonicalized. But we know a bit about its shape from the
last time through, so we can skip the classification step.
-}
-solveCt :: Ct -> SolverStage ()
+solveCt :: Ct -> SolverStage Void
+-- The Void result tells us that solveCt cannot return
+-- a ContinueWith; it must return Stop or StartAgain.
solveCt (CNonCanonical ev) = solveNC ev
solveCt (CIrredCan (IrredCt { ir_ev = ev })) = solveNC ev
@@ -234,12 +240,18 @@ solveCt (CEqCan (EqCt { eq_ev = ev, eq_eq_rel = eq_rel
solveCt (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc }))
= do { ev <- rewriteEvidence ev
+ -- It is (much) easier to rewrite and re-classify than to
+ -- rewrite the pieces and build a Reduction that will rewrite
+ -- the whole constraint
; case classifyPredType (ctEvPred ev) of
ForAllPred tvs th p -> Stage $ solveForAll ev tvs th p pend_sc
_ -> pprPanic "SolveCt" (ppr ev) }
solveCt (CDictCan (DictCt { di_ev = ev, di_pend_sc = pend_sc }))
= do { ev <- rewriteEvidence ev
+ -- It is easier to rewrite and re-classify than to rewrite
+ -- the pieces and build a Reduction that will rewrite the
+ -- whole constraint
; case classifyPredType (ctEvPred ev) of
ClassPred cls tys
-> solveDict (DictCt { di_ev = ev, di_cls = cls
@@ -247,7 +259,7 @@ solveCt (CDictCan (DictCt { di_ev = ev, di_pend_sc = pend_sc }))
_ -> pprPanic "solveCt" (ppr ev) }
------------------
-solveNC :: CtEvidence -> SolverStage ()
+solveNC :: CtEvidence -> SolverStage Void
solveNC ev
= -- Instead of rewriting the evidence before classifying, it's possible we
-- can make progress without the rewrite. Try this first.
@@ -354,7 +366,7 @@ type signature.
-}
solveForAllNC :: CtEvidence -> [TcTyVar] -> TcThetaType -> TcPredType
- -> TcS (StopOrContinue ())
+ -> TcS (StopOrContinue Void)
-- NC: this came from CNonCanonical, so we have not yet expanded superclasses
-- Precondition: already rewritten by inert set
solveForAllNC ev tvs theta pred
@@ -380,7 +392,7 @@ solveForAllNC ev tvs theta pred
cls_pred_tys_maybe = getClassPredTys_maybe pred
solveForAll :: CtEvidence -> [TcTyVar] -> TcThetaType -> PredType -> ExpansionFuel
- -> TcS (StopOrContinue ())
+ -> TcS (StopOrContinue Void)
-- Precondition: already rewritten by inert set
solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_loc = loc })
tvs theta pred _fuel
=====================================
compiler/GHC/Utils/Outputable.hs
=====================================
@@ -891,6 +891,9 @@ class Outputable a where
-- There's no Outputable for Char; it's too easy to use Outputable
-- on String and have ppr "hello" rendered as "h,e,l,l,o".
+instance Outputable Void where
+ ppr _ = text "<<Void>>"
+
instance Outputable Bool where
ppr True = text "True"
ppr False = text "False"
=====================================
testsuite/tests/quantified-constraints/T17267b.hs
=====================================
@@ -14,3 +14,22 @@ uc = oops where
oops :: (a ~ b => a ~ b) => a -> b
oops x = x
+{-
+Consider the ambiguity check for oops.
+
+[G] (a ~ b => a ~ b)
+[W] (a ~ b => a ~ b)
+==>
+
+[G] (a ~ b => a ~ b)
+[G] (a ~# b) was [G] (a ~ b) [G] a ~# b
+
+kick out the QC and (old) (a~b)
+[G] (b ~ b => b ~ b) Quantified constraint
+[G] (a ~# b) was [G] (b ~ b) [G] a ~# b
+
+[W] (a~b) DictCt
+
+Wanted is rewritten
+ (b~b) DictCt
+-}
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b9673b563bb28eaab4482c2be402d0de9a02530f
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b9673b563bb28eaab4482c2be402d0de9a02530f
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/20230515/8d82010b/attachment-0001.html>
More information about the ghc-commits
mailing list