[Git][ghc/ghc][wip/T23070-dicts] Two fast paths
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Sun May 14 13:46:54 UTC 2023
Simon Peyton Jones pushed to branch wip/T23070-dicts at Glasgow Haskell Compiler / GHC
Commits:
41d532da by Simon Peyton Jones at 2023-05-14T14:46:31+01:00
Two fast paths
* Naturally coherent constraints
* Hole-fits
- - - - -
2 changed files:
- compiler/GHC/Tc/Errors/Hole.hs
- compiler/GHC/Tc/Solver/Dict.hs
Changes:
=====================================
compiler/GHC/Tc/Errors/Hole.hs
=====================================
@@ -1,5 +1,6 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE ExistentialQuantification #-}
module GHC.Tc.Errors.Hole
@@ -40,7 +41,10 @@ import GHC.Tc.Utils.TcMType
import GHC.Tc.Types.Evidence
import GHC.Tc.Utils.TcType
import GHC.Core.Type
+import GHC.Core.TyCon( TyCon, isGenerativeTyCon )
+import GHC.Core.TyCo.Rep( Type(..) )
import GHC.Core.DataCon
+import GHC.Core.Predicate( Pred(..), classifyPredType, eqRelRole )
import GHC.Types.Name
import GHC.Types.Name.Reader
import GHC.Builtin.Names ( gHC_ERR )
@@ -981,28 +985,33 @@ tcCheckHoleFit (TypedHole {..}) hole_ty ty = discardErrs $
tcSubTypeSigma orig (ExprSigCtxt NoRRC) ty hole_ty
; traceTc "Checking hole fit {" empty
; traceTc "wanteds are: " $ ppr wanted
- ; if isEmptyWC wanted && isEmptyBag th_relevant_cts
- then do { traceTc "}" empty
- ; return (True, wrap) }
- else do { fresh_binds <- newTcEvBinds
- -- The relevant constraints may contain HoleDests, so we must
- -- take care to clone them as well (to avoid #15370).
- ; cloned_relevants <- mapBagM cloneWantedCtEv th_relevant_cts
- -- We wrap the WC in the nested implications, for details, see
- -- Note [Checking hole fits]
- ; let wrapInImpls cts = foldl (flip (setWCAndBinds fresh_binds)) cts th_implics
- final_wc = wrapInImpls $ addSimples wanted $
- mapBag mkNonCanonical cloned_relevants
- -- We add the cloned relevants to the wanteds generated
- -- by the call to tcSubType_NC, for details, see
- -- Note [Relevant constraints]. There's no need to clone
- -- the wanteds, because they are freshly generated by the
- -- call to`tcSubtype_NC`.
- ; traceTc "final_wc is: " $ ppr final_wc
- -- See Note [Speeding up valid hole-fits]
- ; (rem, _) <- tryTc $ runTcSEarlyAbort $ simplifyTopWanteds final_wc
- ; traceTc "}" empty
- ; return (any isSolvedWC rem, wrap) } }
+ ; if | isEmptyWC wanted, isEmptyBag th_relevant_cts
+ -> do { traceTc "}" empty
+ ; return (True, wrap) }
+
+ | checkInsoluble wanted
+ -> return (False, wrap)
+
+ | otherwise
+ -> do { fresh_binds <- newTcEvBinds
+ -- The relevant constraints may contain HoleDests, so we must
+ -- take care to clone them as well (to avoid #15370).
+ ; cloned_relevants <- mapBagM cloneWantedCtEv th_relevant_cts
+ -- We wrap the WC in the nested implications, for details, see
+ -- Note [Checking hole fits]
+ ; let wrapInImpls cts = foldl (flip (setWCAndBinds fresh_binds)) cts th_implics
+ final_wc = wrapInImpls $ addSimples wanted $
+ mapBag mkNonCanonical cloned_relevants
+ -- We add the cloned relevants to the wanteds generated
+ -- by the call to tcSubType_NC, for details, see
+ -- Note [Relevant constraints]. There's no need to clone
+ -- the wanteds, because they are freshly generated by the
+ -- call to`tcSubtype_NC`.
+ ; traceTc "final_wc is: " $ ppr final_wc
+ -- See Note [Speeding up valid hole-fits]
+ ; (rem, _) <- tryTc $ runTcSEarlyAbort $ simplifyTopWanteds final_wc
+ ; traceTc "}" empty
+ ; return (any isSolvedWC rem, wrap) } }
where
orig = ExprHoleOrigin (hole_occ <$> th_hole)
@@ -1012,3 +1021,31 @@ tcCheckHoleFit (TypedHole {..}) hole_ty ty = discardErrs $
-> WantedConstraints -- The new constraints.
setWCAndBinds binds imp wc
= mkImplicWC $ unitBag $ imp { ic_wanted = wc , ic_binds = binds }
+
+checkInsoluble :: WantedConstraints -> Bool
+checkInsoluble (WC { wc_simple = simples })
+ = any is_insol simples
+ where
+ is_insol ct = case classifyPredType (ctPred ct) of
+ EqPred r t1 t2 -> definitelyNotEqual (eqRelRole r) t1 t2
+ _ -> False
+
+definitelyNotEqual :: Role -> TcType -> TcType -> Bool
+definitelyNotEqual r t1 t2
+ = go t1 t2
+ where
+ go t1 t2
+ | Just t1' <- coreView t1 = go t1' t2
+ | Just t2' <- coreView t2 = go t1 t2'
+
+ go (TyConApp tc _) t2 | isGenerativeTyCon tc r = go_tc tc t2
+ go t1 (TyConApp tc _) | isGenerativeTyCon tc r = go_tc tc t1
+ go (FunTy {ft_af = af1}) (FunTy {ft_af = af2}) = af1 /= af2
+ go _ _ = False
+
+ go_tc :: TyCon -> TcType -> Bool
+ -- The TyCon is generative, and is not a saturated FunTy
+ go_tc tc1 (TyConApp tc2 _) | isGenerativeTyCon tc2 r = tc1 /= tc2
+ go_tc _ (FunTy {}) = True
+ go_tc _ (ForAllTy {}) = True
+ go_tc _ _ = False
\ No newline at end of file
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -69,7 +69,7 @@ solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage ()
-- NC: this comes from CNonCanonical or CIrredCan
-- Precondition: already rewritten by inert set
solveDictNC ev cls tys
- = do { dict_ct <- simpleStage (canDictCt ev cls tys)
+ = do { dict_ct <- canDictCt ev cls tys
; solveDict dict_ct }
solveDict :: DictCt -> SolverStage ()
@@ -100,18 +100,30 @@ updInertDicts dict_ct@(DictCt { di_cls = cls, di_ev = ev })
-- Add the new constraint to the inert set
; updInertCans (updDicts (addDict dict_ct)) }
-canDictCt :: CtEvidence -> Class -> [Type] -> TcS DictCt
+canDictCt :: CtEvidence -> Class -> [Type] -> SolverStage DictCt
-- Once-only processing of Dict constraints:
-- * expand superclasses
-- * deal with CallStack
canDictCt ev cls tys
| isGiven ev -- See Note [Eagerly expand given superclasses]
- = do { dflags <- getDynFlags
+ = Stage $
+ do { dflags <- getDynFlags
; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev [] [] cls tys
- -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel]
- ; emitWork (listToBag sc_cts)
- ; return (DictCt { di_ev = ev, di_cls = cls
- , di_tys = tys, di_pend_sc = doNotExpand }) }
+ -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel]
+
+ -- For "naturally coherent" classes, /replace/ the current constraint with its
+ -- superclasses, rather than /adding/ them.
+ -- See (NC1) in Note [Naturally coherent classes]
+ ; if naturallyCoherentClass cls
+ then case sc_cts of
+ [] -> stopWith ev "Naturally coherent"
+ ct:cts -> do { emitWork (listToBag cts)
+ ; startAgainWith ct }
+ else
+
+ do { emitWork (listToBag sc_cts)
+ ; continueWith (DictCt { di_ev = ev, di_cls = cls
+ , 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
@@ -123,7 +135,8 @@ canDictCt ev cls tys
-- of solving it directly from a given.
-- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
-- and Note [Solving CallStack constraints] in GHC.Tc.Solver.Types
- = do { -- First we emit a new constraint that will capture the
+ = Stage $
+ do { -- First we emit a new constraint that will capture the
-- given CallStack.
let new_loc = setCtLocOrigin loc (IPOccOrigin (HsIPName ip_name))
-- We change the origin to IPOccOrigin so
@@ -139,18 +152,19 @@ canDictCt ev cls tys
(ctLocSpan loc) (ctEvExpr new_ev)
; solveCallStack ev ev_cs
- ; return (DictCt { di_ev = new_ev, di_cls = cls
- , di_tys = tys, di_pend_sc = doNotExpand }) }
+ ; continueWith (DictCt { di_ev = new_ev, di_cls = cls
+ , di_tys = tys, di_pend_sc = doNotExpand }) }
-- doNotExpand: No superclasses for class CallStack
-- See invariants in CDictCan.cc_pend_sc
| otherwise
- = do { dflags <- getDynFlags
+ = Stage $
+ do { dflags <- getDynFlags
; let fuel | classHasSCs cls = wantedsFuel dflags
| otherwise = doNotExpand
-- See Invariants in `CCDictCan.cc_pend_sc`
- ; return (DictCt { di_ev = ev, di_cls = cls
- , di_tys = tys, di_pend_sc = fuel }) }
+ ; continueWith (DictCt { di_ev = ev, di_cls = cls
+ , di_tys = tys, di_pend_sc = fuel }) }
where
loc = ctEvLoc ev
orig = ctLocOrigin loc
@@ -790,7 +804,7 @@ 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)
+ , 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 ]
@@ -917,14 +931,41 @@ this:
instance a ~# b => a ~~ b
(See Note [The equality types story] in GHC.Builtin.Types.Prim.)
-Faced with [W] t1 ~~ t2, it's always OK to reduce it to [W] t1 ~# t2,
-without worrying about Note [Instance and Given overlap]. Why? Because
-if we had [G] s1 ~~ s2, then we'd get the superclass [G] s1 ~# s2, and
-so the reduction of the [W] constraint does not risk losing any solutions.
+PS: the term "naturally coherent" doesn't really seem helpful.
+Perhaps "invertible" or something? I left it for now though.
-On the other hand, it can be fatal to /fail/ to reduce such
-equalities, on the grounds of Note [Instance and Given overlap],
-because many good things flow from [W] t1 ~# t2.
+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
+ forall b,c. a ~ (b,c) =>
+ forall d,e. c ~ (d,e) =>
+ ...etc...
+ If we just /add/ the superclasses of [G] g1:a ~ (b,c), we'll put
+ [G] g1:(a~(b,c)) in the inert set and emit [G] g2:a ~# (b,c). That will
+ kick out g1, and it'll be re-inserted as [G] g1':(b,c)~(b,c) which does
+ no good to anyone. When the implication is deeply nested, this has
+ quadratic cost, and no benefit. Just replace!
+
+(NC2) Because of this replacement, we don't need do the fancy footwork
+ of Note [Solving superclass constraints], so the computation of `sc_loc`
+ in `mk_strict_superclasses` can be simpler.
+
+ For tuple predicates, this matters, because their size can be large,
+ and we don't want to add a big class to the size of the dictionaries
+ in the chain. When we get down to a base predicate, we'll include
+ its size. See #10335
+
+(NC3) Faced with [W] t1 ~ t2, it's always OK to reduce it to [W] t1 ~# t2,
+ without worrying about Note [Instance and Given overlap]. Why? Because
+ if we had [G] s1 ~ s2, then we'd get the superclass [G] s1 ~# s2, and
+ 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
+ things flow from [W] t1 ~# t2.
The same reasoning applies to
@@ -947,9 +988,6 @@ And less obviously to:
Examples: T5853, T10432, T5315, T9222, T2627b, T3028b
-PS: the term "naturally coherent" doesn't really seem helpful.
-Perhaps "invertible" or something? I left it for now though.
-
Note [Local instances and incoherence]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
@@ -1934,18 +1972,8 @@ 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 | isCTupleClass cls
- = loc -- For tuple predicates, just take them apart, without
- -- adding their (large) size into the chain. When we
- -- get down to a base predicate, we'll include its size.
- -- #10335
-
- | isEqPredClass cls || cls `hasKey` coercibleTyConKey
- = loc -- The only superclasses of ~, ~~, and Coercible are primitive
- -- equalities, and they don't use the GivenSCOrigin mechanism
- -- detailed in Note [Solving superclass constraints] in
- -- GHC.Tc.TyCl.Instance. Skip for a tiny performance win.
-
+ sc_loc | naturallyCoherentClass cls
+ = loc -- See (NC2) in Note [Naturally coherence classes]
| otherwise
= loc { ctl_origin = mk_sc_origin (ctLocOrigin loc) }
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/41d532da73d22f3b5f1d761592a3b99aafb6db20
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/41d532da73d22f3b5f1d761592a3b99aafb6db20
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/20230514/c3485778/attachment-0001.html>
More information about the ghc-commits
mailing list