[Git][ghc/ghc][wip/T23070-pipeline-monad] Further refactoring
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Sun May 7 22:28:07 UTC 2023
Simon Peyton Jones pushed to branch wip/T23070-pipeline-monad at Glasgow Haskell Compiler / GHC
Commits:
527a4943 by Simon Peyton Jones at 2023-05-07T23:25:00+01:00
Further refactoring
In particular make the Irred pipeline one-stage
(Just the Dict pipeline is left)
- - - - -
9 changed files:
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Interact.hs
- + compiler/GHC/Tc/Solver/Irred.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/ghc.cabal.in
Changes:
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -277,8 +277,8 @@ floatKindEqualities wc = float_wc emptyVarSet wc
= Nothing
where
is_floatable ct
- | insolubleEqCt ct = False
- | otherwise = tyCoVarsOfCt ct `disjointVarSet` trapping_tvs
+ | insolubleCt ct = False
+ | otherwise = tyCoVarsOfCt ct `disjointVarSet` trapping_tvs
float_implic :: TcTyCoVarSet -> Implication -> Maybe (Bag Ct, Bag DelayedError)
float_implic trapping_tvs (Implic { ic_wanted = wanted, ic_given_eqs = given_eqs
@@ -3396,7 +3396,7 @@ approximateWC float_past_equalities wc
is_floatable encl_eqs skol_tvs ct
| isGivenCt ct = False
- | insolubleEqCt ct = False
+ | insolubleCt ct = False
| tyCoVarsOfCt ct `intersectsVarSet` skol_tvs = False
| otherwise
= case classifyPredType (ctPred ct) of
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -17,7 +17,8 @@ import GHC.Tc.Types.Origin
import GHC.Tc.Utils.TcType
import GHC.Tc.Solver.Rewrite
import GHC.Tc.Solver.Monad
-import GHC.Tc.Solver.Equality( solveNonCanonicalEquality, solveCanonicalEquality )
+import GHC.Tc.Solver.Equality( solveEquality )
+import GHC.Tc.Solver.Irred( solveIrred )
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.EvTerm
@@ -87,39 +88,52 @@ last time through, so we can skip the classification step.
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
canonicalize :: Ct -> SolverStage Ct
-canonicalize (CNonCanonical ev)
- = canNC ev
+canonicalize (CNonCanonical ev) = canNC ev
+canonicalize (CIrredCan (IrredCt { ir_ev = ev })) = canNC ev
-canonicalize (CEqCan can_eq_ct)
- = solveCanonicalEquality can_eq_ct
+canonicalize (CEqCan (EqCt { eq_ev = ev, eq_eq_rel = eq_rel
+ , eq_lhs = lhs, eq_rhs = rhs }))
+ = solveEquality ev eq_rel (canEqLHSType lhs) rhs
canonicalize (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc }))
- = Stage $ canForAll ev pend_sc
+ = do { ev <- rewriteEvidence ev
+ ; case classifyPredType (ctEvPred ev) of
+ ForAllPred tvs th p -> Stage $ solveForAll ev tvs th p pend_sc
+ _ -> pprPanic "canonicalise" (ppr ev) }
-canonicalize (CIrredCan (IrredCt { ir_ev = ev }))
- = canNC ev
- -- Instead of rewriting the evidence before classifying, it's possible we
+canonicalize (CDictCan { cc_ev = ev, cc_pend_sc = pend_sc })
+ = do { ev <- rewriteEvidence ev
+ ; case classifyPredType (ctEvPred ev) of
+ ClassPred cls tys -> Stage $ solveClass ev cls tys pend_sc
+ _ -> pprPanic "canonicalise" (ppr ev) }
+
+canNC :: CtEvidence -> SolverStage Ct
+canNC ev
+ = -- Instead of rewriting the evidence before classifying, it's possible we
-- can make progress without the rewrite. Try this first.
-- For insolubles (all of which are equalities), do /not/ rewrite the arguments
-- In #14350 doing so led entire-unnecessary and ridiculously large
-- type function expansion. Instead, canEqNC just applies
-- the substitution to the predicate, and may do decomposition;
-- e.g. a ~ [a], where [G] a ~ [Int], can decompose
+ case classifyPredType (ctEvPred ev) of {
+ EqPred eq_rel ty1 ty2 -> solveEquality ev eq_rel ty1 ty2 ;
+ _ ->
-canonicalize (CDictCan { cc_ev = ev, cc_class = cls
- , cc_tyargs = xis, cc_pend_sc = pend_sc })
- = {-# SCC "canClass" #-}
- Stage $ canClass ev cls xis pend_sc
+ -- Do rewriting on the constraint, especially zonking
+ do { ev <- rewriteEvidence ev
+ ; let irred = IrredCt { ir_ev = ev, ir_reason = IrredShapeReason }
-canNC :: CtEvidence -> SolverStage Ct
-canNC ev =
- case classifyPredType pred of
- ClassPred cls tys -> Stage $ canClassNC ev cls tys
- EqPred eq_rel ty1 ty2 -> solveNonCanonicalEquality ev eq_rel ty1 ty2
- IrredPred {} -> Stage $ canIrred ev
- ForAllPred tvs th p -> Stage $ canForAllNC ev tvs th p
- where
- pred = ctEvPred ev
+ -- And then re-classify
+ ; case classifyPredType (ctEvPred ev) of
+ ClassPred cls tys -> Stage $ solveClassNC ev cls tys
+ ForAllPred tvs th p -> Stage $ solveForAllNC ev tvs th p
+ IrredPred {} -> solveIrred irred
+ EqPred eq_rel ty1 ty2 -> solveEquality ev eq_rel ty1 ty2
+ -- This case only happens if (say) `c` is unified with `a ~# b`,
+ -- but that is rare becuase it requires c :: CONSTRAINT UnliftedRep
+
+ }}
{-
************************************************************************
@@ -129,19 +143,18 @@ canNC ev =
************************************************************************
-}
-canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
--- "NC" means "non-canonical"; that is, we have got here
--- from a NonCanonical constraint, not from a CDictCan
--- Precondition: EvVar is class evidence
-canClassNC ev cls tys
+solveClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
+-- NC: this comes from CNonCanonical or CIrredCan
+-- Precondition: already rewritten by inert set
+solveClassNC ev cls tys
| isGiven ev -- See Note [Eagerly expand given superclasses]
= do { dflags <- getDynFlags
; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev [] [] cls tys
- -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel]
+ -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel]
; emitWork (listToBag sc_cts)
- ; canClass ev cls tys doNotExpand }
- -- doNotExpand: We have already expanded superclasses for /this/ dict
- -- so set the fuel to doNotExpand to avoid repeating expansion
+ ; solveClass ev cls tys doNotExpand }
+ -- doNotExpand: We have already expanded superclasses for /this/ dict
+ -- so set the fuel to doNotExpand to avoid repeating expansion
| CtWanted { ctev_rewriters = rewriters } <- ev
, Just ip_name <- isCallStackPred cls tys
@@ -167,24 +180,30 @@ canClassNC ev cls tys
(ctLocSpan loc) (ctEvExpr new_ev)
; solveCallStack ev ev_cs
- ; canClass new_ev cls tys doNotExpand
- -- doNotExpand: No superclasses for class CallStack
- -- See invariants in CDictCan.cc_pend_sc
- }
+ ; solveClass new_ev cls tys doNotExpand }
+ -- doNotExpand: No superclasses for class CallStack
+ -- See invariants in CDictCan.cc_pend_sc
| otherwise
= do { dflags <- getDynFlags
; let fuel | classHasSCs cls = wantedsFuel dflags
| otherwise = doNotExpand
-- See Invariants in `CCDictCan.cc_pend_sc`
- ; canClass ev cls tys fuel
- }
-
+ ; solveClass ev cls tys fuel }
where
loc = ctEvLoc ev
orig = ctLocOrigin loc
pred = ctEvPred ev
+solveClass :: CtEvidence -> Class -> [Type] -> ExpansionFuel -> TcS (StopOrContinue Ct)
+solveClass ev cls tys pend_sc
+ = -- Sll classes do *nominal* matching
+ assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $
+ continueWith (CDictCan { cc_ev = ev
+ , cc_tyargs = tys
+ , cc_class = cls
+ , cc_pend_sc = pend_sc })
+
solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
-- Also called from GHC.Tc.Solver when defaulting call stacks
solveCallStack ev ev_cs = do
@@ -195,25 +214,6 @@ solveCallStack ev ev_cs = do
let ev_tm = mkEvCast cs_tm (wrapIP (ctEvPred ev))
setEvBindIfWanted ev IsCoherent ev_tm
-canClass :: CtEvidence
- -> Class -> [Type]
- -> ExpansionFuel -- n > 0 <=> un-explored superclasses
- -> TcS (StopOrContinue Ct)
--- Precondition: EvVar is class evidence
-
-canClass ev cls tys pend_sc
- = -- all classes do *nominal* matching
- assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $
- do { (redns@(Reductions _ xis), rewriters) <- rewriteArgsNom ev cls_tc tys
- ; let redn = mkClassPredRedn cls redns
- ; rewriteEvidence rewriters ev redn $ \new_ev ->
- do { traceTcS "canClass" (vcat [ ppr new_ev, ppr (reductionReducedType redn) ])
- ; continueWith (CDictCan { cc_ev = new_ev
- , cc_tyargs = xis
- , cc_class = cls
- , cc_pend_sc = pend_sc }) }}
- where
- cls_tc = classTyCon cls
{- Note [The superclass story]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -715,40 +715,8 @@ which looks for primitive equalities specially in the quantified
constraints.
See also Note [Evidence for quantified constraints] in GHC.Core.Predicate.
-
-
-************************************************************************
-* *
-* Irreducibles canonicalization
-* *
-************************************************************************
-}
-canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
--- Precondition: ty not a tuple and no other evidence form
-canIrred ev
- = do { let pred = ctEvPred ev
- ; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
- ; (redn, rewriters) <- rewrite ev pred
- ; rewriteEvidence rewriters ev redn $ \ new_ev ->
-
- do { -- Re-classify, in case rewriting has improved its shape
- -- Code is like the canNC, except
- -- that the IrredPred branch stops work
- ; case classifyPredType (ctEvPred new_ev) of
- ClassPred cls tys -> canClassNC new_ev cls tys
- EqPred eq_rel ty1 ty2 -> -- IrredPreds have kind Constraint, so
- -- cannot become EqPreds
- pprPanic "canIrred: EqPred"
- (ppr ev $$ ppr eq_rel $$ ppr ty1 $$ ppr ty2)
- ForAllPred tvs th p -> -- this is highly suspect; Quick Look
- -- should never leave a meta-var filled
- -- in with a polytype. This is #18987.
- do traceTcS "canEvNC:forall" (ppr pred)
- canForAllNC ev tvs th p
- IrredPred {} -> continueWith $
- mkIrredCt IrredShapeReason new_ev } }
-
{- *********************************************************************
* *
* Quantified predicates
@@ -827,16 +795,18 @@ type signature.
-}
-canForAllNC :: CtEvidence -> [TyVar] -> TcThetaType -> TcPredType
- -> TcS (StopOrContinue Ct)
-canForAllNC ev tvs theta pred
+solveForAllNC :: CtEvidence -> [TyVar] -> TcThetaType -> TcPredType
+ -> TcS (StopOrContinue Ct)
+-- NC: this came from CNonCanonical, so we have not yet expanded superclasses
+-- Precondition: already rewritten by inert set
+solveForAllNC ev tvs theta pred
| isGiven ev -- See Note [Eagerly expand given superclasses]
, Just (cls, tys) <- cls_pred_tys_maybe
= do { dflags <- getDynFlags
; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev tvs theta cls tys
-- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel]
; emitWork (listToBag sc_cts)
- ; canForAll ev doNotExpand }
+ ; solveForAll ev tvs theta pred doNotExpand }
-- doNotExpand: as we have already (eagerly) expanded superclasses for this class
| otherwise
@@ -847,27 +817,13 @@ canForAllNC ev tvs theta pred
-- qcsFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel]
-- See Note [Quantified constraints]
| otherwise = doNotExpand
- ; canForAll ev fuel }
+ ; solveForAll ev tvs theta pred fuel }
where
cls_pred_tys_maybe = getClassPredTys_maybe pred
-canForAll :: CtEvidence -> ExpansionFuel -> TcS (StopOrContinue Ct)
--- We have a constraint (forall as. blah => C tys)
-canForAll ev fuel
- = do { -- First rewrite it to apply the current substitution
- ; (redn, rewriters) <- rewrite ev (ctEvPred ev)
- ; rewriteEvidence rewriters ev redn $ \ new_ev ->
-
- do { -- Now decompose into its pieces and solve it
- -- (It takes a lot less code to rewrite before decomposing.)
- ; case classifyPredType (ctEvPred new_ev) of
- ForAllPred tvs theta pred
- -> solveForAll new_ev tvs theta pred fuel
- _ -> pprPanic "canForAll" (ppr new_ev)
- } }
-
solveForAll :: CtEvidence -> [TyVar] -> TcThetaType -> PredType -> ExpansionFuel
-> TcS (StopOrContinue Ct)
+-- Precondition: already rewritten by inert set
solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_loc = loc })
tvs theta pred _fuel
= -- See Note [Solving a Wanted forall-constraint]
@@ -966,12 +922,7 @@ we'll find a match in the InstEnv.
************************************************************************
-}
-rewriteEvidence :: RewriterSet -- ^ See Note [Wanteds rewrite Wanteds]
- -- in GHC.Tc.Types.Constraint
- -> CtEvidence -- ^ old evidence
- -> Reduction -- ^ new predicate + coercion, of type <type of old evidence> ~ new predicate
- -> (CtEvidence -> TcS (StopOrContinue Ct))
- -> TcS (StopOrContinue Ct)
+rewriteEvidence :: CtEvidence -> SolverStage CtEvidence
-- (rewriteEvidence old_ev new_pred co do_next)
-- Main purpose: create new evidence for new_pred;
-- unless new_pred is cached already
@@ -1005,33 +956,42 @@ the rewriter set. We check this with an assertion.
-}
-rewriteEvidence rewriters old_ev (Reduction co new_pred) do_next
+rewriteEvidence ev
+ = Stage $ do { traceTcS "rewriteEvidence" (ppr ev)
+ ; (redn, rewriters) <- rewrite ev (ctEvPred ev)
+ ; finish_rewrite ev redn rewriters }
+
+finish_rewrite :: CtEvidence -- ^ old evidence
+ -> Reduction -- ^ new predicate + coercion, of type <type of old evidence> ~ new predicate
+ -> RewriterSet -- ^ See Note [Wanteds rewrite Wanteds]
+ -- in GHC.Tc.Types.Constraint
+ -> TcS (StopOrContinue CtEvidence)
+finish_rewrite old_ev (Reduction co new_pred) rewriters
| isReflCo co -- See Note [Rewriting with Refl]
= assert (isEmptyRewriterSet rewriters) $
- do_next (setCtEvPredType old_ev new_pred)
+ continueWith (setCtEvPredType old_ev new_pred)
-rewriteEvidence rewriters ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc })
- (Reduction co new_pred) do_next
+finish_rewrite ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc })
+ (Reduction co new_pred) rewriters
= assert (isEmptyRewriterSet rewriters) $ -- this is a Given, not a wanted
do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
- ; do_next new_ev }
+ ; continueWith new_ev }
where
-- mkEvCast optimises ReflCo
new_tm = mkEvCast (evId old_evar)
(downgradeRole Representational (ctEvRole ev) co)
-rewriteEvidence new_rewriters
- ev@(CtWanted { ctev_dest = dest
+finish_rewrite ev@(CtWanted { ctev_dest = dest
, ctev_loc = loc
, ctev_rewriters = rewriters })
- (Reduction co new_pred) do_next
+ (Reduction co new_pred) new_rewriters
= do { mb_new_ev <- newWanted loc rewriters' new_pred
; massert (coercionRole co == ctEvRole ev)
; setWantedEvTerm dest IsCoherent $
mkEvCast (getEvExpr mb_new_ev)
(downgradeRole Representational (ctEvRole ev) (mkSymCo co))
; case mb_new_ev of
- Fresh new_ev -> do_next new_ev
+ Fresh new_ev -> continueWith new_ev
Cached _ -> stopWith ev "Cached wanted" }
where
rewriters' = rewriters S.<> new_rewriters
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -2,7 +2,7 @@
{-# LANGUAGE MultiWayIf #-}
module GHC.Tc.Solver.Equality(
- solveCanonicalEquality, solveNonCanonicalEquality
+ solveEquality
) where
@@ -10,6 +10,7 @@ import GHC.Prelude
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 )
@@ -100,14 +101,9 @@ It's as if we treat (->) and (=>) as different type constructors, which
indeed they are!
-}
-solveCanonicalEquality :: EqCt -> SolverStage Ct
-solveCanonicalEquality (EqCt { eq_ev = ev, eq_eq_rel = eq_rel
- , eq_lhs = lhs, eq_rhs = rhs })
- = solveNonCanonicalEquality ev eq_rel (canEqLHSType lhs) rhs
-
-solveNonCanonicalEquality :: CtEvidence -> EqRel -> Type -> Type
- -> SolverStage Ct
-solveNonCanonicalEquality ev eq_rel ty1 ty2
+solveEquality :: CtEvidence -> EqRel -> Type -> Type
+ -> SolverStage Ct
+solveEquality ev eq_rel ty1 ty2
= do { Pair ty1' ty2' <- zonkEqTypes ev eq_rel ty1 ty2
; let ev' | debugIsOn = setCtEvPredType ev $
mkPrimEqPredRole (eqRelRole eq_rel) ty1' ty2'
@@ -118,12 +114,12 @@ solveNonCanonicalEquality ev eq_rel ty1 ty2
; case mb_canon of {
- Left irred_ct -> do { solveIrredEquality irred_ct
+ Left irred_ct -> do { tryInertIrreds irred_ct
; return (CIrredCan irred_ct) } ;
Right eq_ct -> do { interactEq eq_ct
; tryFunDeps eq_ct
- ; tryQuantifiedConstraints eq_ct
+ ; tryQCsEqCt eq_ct
; return (CEqCan eq_ct) } } }
@@ -2674,8 +2670,9 @@ See
-}
--------------------
-solveIrredEquality :: IrredCt -> SolverStage ()
-solveIrredEquality irred@(IrredCt { ir_ev = ev })
+{-
+tryQCsIrredCt :: IrredCt -> SolverStage ()
+tryQCsIrredCt irred@(IrredCt { ir_ev = ev })
| EqPred eq_rel t1 t2 <- classifyPredType (ctEvPred ev)
= lookup_eq_in_qcis (CIrredCan irred) eq_rel t1 t2
-- If the final_qci_check fails, we'll do continueWith on an IrredCt
@@ -2689,10 +2686,11 @@ solveIrredEquality irred@(IrredCt { ir_ev = ev })
-- this can't happen case, but it's not a hot path, and this is
-- simple and robust
= pprPanic "solveIrredEquality" (ppr ev)
+-}
--------------------
-tryQuantifiedConstraints :: EqCt -> SolverStage ()
-tryQuantifiedConstraints work_item@(EqCt { eq_lhs = lhs, eq_rhs = rhs, eq_eq_rel = eq_rel })
+tryQCsEqCt :: EqCt -> SolverStage ()
+tryQCsEqCt work_item@(EqCt { eq_lhs = lhs, eq_rhs = rhs, eq_eq_rel = eq_rel })
= lookup_eq_in_qcis (CEqCan work_item) eq_rel (canEqLHSType lhs) rhs
--------------------
@@ -2701,6 +2699,8 @@ lookup_eq_in_qcis :: Ct -> EqRel -> TcType -> TcType -> SolverStage ()
-- [W] t1 ~# t2
-- and a Given quantified contraint like (forall a b. blah => a ~ b)
-- Why? See Note [Looking up primitive equalities in quantified constraints]
+-- See also GHC.Tc.Solver.Canonical
+-- Note [Equality superclasses in quantified constraints]
lookup_eq_in_qcis work_ct eq_rel lhs rhs
= Stage $
do { ev_binds_var <- getTcEvBindsVar
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -42,7 +42,10 @@ module GHC.Tc.Solver.InertSet (
CycleBreakerVarStack,
pushCycleBreakerVarStack,
addCycleBreakerBindings,
- forAllCycleBreakerBindings_
+ forAllCycleBreakerBindings_,
+
+ -- * Solving one from another
+ InteractResult(..), solveOneFromTheOther
) where
@@ -65,15 +68,17 @@ import GHC.Core.Class( Class )
import GHC.Core.TyCon
import GHC.Core.Unify
-import GHC.Data.Bag
import GHC.Utils.Misc ( partitionWith )
import GHC.Utils.Outputable
import GHC.Utils.Panic
+import GHC.Utils.Panic.Plain
+import GHC.Data.Maybe
+import GHC.Data.Bag
import Data.List.NonEmpty ( NonEmpty(..), (<|) )
import qualified Data.List.NonEmpty as NE
-import GHC.Utils.Panic.Plain
-import GHC.Data.Maybe
+import Data.Function ( on )
+
import Control.Monad ( forM_ )
{-
@@ -1945,3 +1950,198 @@ forAllCycleBreakerBindings_ :: Monad m
forAllCycleBreakerBindings_ (top_env :| _rest_envs) action
= forM_ top_env (uncurry action)
{-# INLINABLE forAllCycleBreakerBindings_ #-} -- to allow SPECIALISE later
+
+
+{- *********************************************************************
+* *
+ Solving one from another
+* *
+********************************************************************* -}
+
+data InteractResult
+ = KeepInert -- Keep the inert item, and solve the work item from it
+ -- (if the latter is Wanted; just discard it if not)
+ | KeepWork -- Keep the work item, and solve the inert item from it
+
+instance Outputable InteractResult where
+ ppr KeepInert = text "keep inert"
+ ppr KeepWork = text "keep work-item"
+
+solveOneFromTheOther :: Ct -- Inert (Dict or Irred)
+ -> Ct -- WorkItem (same predicate as inert)
+ -> InteractResult
+-- Precondition:
+-- * inert and work item represent evidence for the /same/ predicate
+-- * Both are CDictCan or CIrredCan
+--
+-- We can always solve one from the other: even if both are wanted,
+-- although we don't rewrite wanteds with wanteds, we can combine
+-- two wanteds into one by solving one from the other
+
+solveOneFromTheOther ct_i ct_w
+ | CtWanted { ctev_loc = loc_w } <- ev_w
+ , prohibitedSuperClassSolve loc_i loc_w
+ -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
+ = -- Inert must be Given
+ KeepWork
+
+ | CtWanted {} <- ev_w
+ = -- Inert is Given or Wanted
+ case ev_i of
+ CtGiven {} -> KeepInert
+ -- work is Wanted; inert is Given: easy choice.
+
+ CtWanted {} -- Both are Wanted
+ -- If only one has no pending superclasses, use it
+ -- Otherwise we can get infinite superclass expansion (#22516)
+ -- in silly cases like class C T b => C a b where ...
+ | not is_psc_i, is_psc_w -> KeepInert
+ | is_psc_i, not is_psc_w -> KeepWork
+
+ -- If only one is a WantedSuperclassOrigin (arising from expanding
+ -- a Wanted class constraint), keep the other: wanted superclasses
+ -- may be unexpected by users
+ | not is_wsc_orig_i, is_wsc_orig_w -> KeepInert
+ | is_wsc_orig_i, not is_wsc_orig_w -> KeepWork
+
+ -- otherwise, just choose the lower span
+ -- reason: if we have something like (abs 1) (where the
+ -- Num constraint cannot be satisfied), it's better to
+ -- get an error about abs than about 1.
+ -- This test might become more elaborate if we see an
+ -- opportunity to improve the error messages
+ | ((<) `on` ctLocSpan) loc_i loc_w -> KeepInert
+ | otherwise -> KeepWork
+
+ -- From here on the work-item is Given
+
+ | CtWanted { ctev_loc = loc_i } <- ev_i
+ , prohibitedSuperClassSolve loc_w loc_i
+ = KeepInert -- Just discard the un-usable Given
+ -- This never actually happens because
+ -- Givens get processed first
+
+ | CtWanted {} <- ev_i
+ = KeepWork
+
+ -- From here on both are Given
+ -- See Note [Replacement vs keeping]
+
+ | lvl_i == lvl_w
+ = same_level_strategy
+
+ | otherwise -- Both are Given, levels differ
+ = different_level_strategy
+ where
+ ev_i = ctEvidence ct_i
+ ev_w = ctEvidence ct_w
+
+ pred = ctEvPred ev_i
+
+ loc_i = ctEvLoc ev_i
+ loc_w = ctEvLoc ev_w
+ orig_i = ctLocOrigin loc_i
+ orig_w = ctLocOrigin loc_w
+ lvl_i = ctLocLevel loc_i
+ lvl_w = ctLocLevel loc_w
+
+ is_psc_w = isPendingScDict ct_w
+ is_psc_i = isPendingScDict ct_i
+
+ is_wsc_orig_i = isWantedSuperclassOrigin orig_i
+ is_wsc_orig_w = isWantedSuperclassOrigin orig_w
+
+ different_level_strategy -- Both Given
+ | 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]
+
+ same_level_strategy -- Both Given
+ = case (orig_i, orig_w) of
+
+ (GivenSCOrigin _ depth_i blocked_i, GivenSCOrigin _ depth_w blocked_w)
+ | blocked_i, not blocked_w -> KeepWork -- Case 2(a) from
+ | not blocked_i, blocked_w -> KeepInert -- Note [Replacement vs keeping]
+
+ -- Both blocked or both not blocked
+
+ | depth_w < depth_i -> KeepWork -- Case 2(c) from
+ | otherwise -> KeepInert -- Note [Replacement vs keeping]
+
+ (GivenSCOrigin {}, _) -> KeepWork -- Case 2(b) from Note [Replacement vs keeping]
+
+ _ -> KeepInert -- Case 2(d) from Note [Replacement vs keeping]
+
+{-
+Note [Replacement vs keeping]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we have two Given constraints both of type (C tys), say, which should
+we keep? More subtle than you might think! This is all implemented in
+solveOneFromTheOther.
+
+ 1) Constraints come from different levels (different_level_strategy)
+
+ - For implicit parameters we want to keep the innermost (deepest)
+ one, so that it overrides the outer one.
+ See Note [Shadowing of Implicit Parameters]
+
+ - 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,
+ and can be reported as redundant. See Note [Tracking redundant constraints]
+ in GHC.Tc.Solver.
+
+ It transpires that using the outermost one is responsible for an
+ 8% performance improvement in nofib cryptarithm2, compared to
+ just rolling the dice. I didn't investigate why.
+
+ 2) Constraints coming from the same level (i.e. same implication)
+
+ (a) If both are GivenSCOrigin, choose the one that is unblocked if possible
+ according to Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance.
+
+ (b) Prefer constraints that are not superclass selections. Example:
+
+ f :: (Eq a, Ord a) => a -> Bool
+ f x = x == x
+
+ Eager superclass expansion gives us two [G] Eq a constraints. We
+ want to keep the one from the user-written Eq a, not the superclass
+ selection. This means we report the Ord a as redundant with
+ -Wredundant-constraints, not the Eq a.
+
+ Getting this wrong was #20602. See also
+ Note [Tracking redundant constraints] in GHC.Tc.Solver.
+
+ (c) If both are GivenSCOrigin, chooose the one with the shallower
+ superclass-selection depth, in the hope of identifying more correct
+ redundant constraints. This is really a generalization of point (b),
+ because the superclass depth of a non-superclass constraint is 0.
+
+ (If the levels differ, we definitely won't have both with GivenSCOrigin.)
+
+ (d) Finally, when there is still a choice, use KeepInert rather than
+ KeepWork, for two reasons:
+ - to avoid unnecessary munging of the inert set.
+ - to cut off superclass loops; see Note [Superclass loops] in GHC.Tc.Solver.Canonical
+
+Doing the level-check for implicit parameters, rather than making the work item
+always override, is important. Consider
+
+ data T a where { T1 :: (?x::Int) => T Int; T2 :: T a }
+
+ f :: (?x::a) => T a -> Int
+ f T1 = ?x
+ f T2 = 3
+
+We have a [G] (?x::a) in the inert set, and at the pattern match on T1 we add
+two new givens in the work-list: [G] (?x::Int)
+ [G] (a ~ Int)
+Now consider these steps
+ - process a~Int, kicking out (?x::a)
+ - process (?x::Int), the inner given, adding to inert set
+ - process (?x::a), the outer given, overriding the inner given
+Wrong! The level-check ensures that the inner implicit parameter wins.
+(Actually I think that the order in which the work-list is processed means
+that this chain of events won't happen, but that's very fragile.)
+-}
\ No newline at end of file
=====================================
compiler/GHC/Tc/Solver/Interact.hs
=====================================
@@ -15,19 +15,17 @@ import GHC.Tc.Instance.Class ( safeOverlap )
import GHC.Tc.Types.Evidence
import GHC.Tc.Types
import GHC.Tc.Types.Constraint
-import GHC.Tc.Types.Origin
import GHC.Tc.Solver.Types
import GHC.Tc.Solver.InertSet
import GHC.Tc.Solver.Monad
import GHC.Core.InstEnv ( Coherence(..) )
import GHC.Core.Predicate
-import GHC.Core.Coercion
import GHC.Builtin.Names ( ipClassKey )
import GHC.Types.Unique( hasKey )
-import GHC.Types.Basic ( SwapFlag(..), IntWithInf, intGtLimit )
+import GHC.Types.Basic ( IntWithInf, intGtLimit )
import GHC.Data.Bag
@@ -41,7 +39,6 @@ import GHC.Driver.Session
import qualified GHC.LanguageExtensions as LangExt
import Data.List( deleteFirstsBy )
-import Data.Function ( on )
import Control.Monad.Trans.Class
import Control.Monad.Trans.Maybe
@@ -414,262 +411,15 @@ interactWithInertsStage wi
do { inerts <- getTcSInerts
; let ics = inert_cans inerts
; case wi of
- CIrredCan ir_ct -> interactIrred ics ir_ct
- CDictCan {} -> interactDict ics wi
- CEqCan {} -> continueWith wi -- "Canonicalisation" stage is
- -- full solver for equalities
+ CDictCan {} -> interactDict ics wi
+ CEqCan {} -> continueWith wi -- "Canonicalisation" stage is
+ -- full solver for equalities
+ CIrredCan {} -> continueWith wi -- Ditto Irreds
_ -> pprPanic "interactWithInerts" (ppr wi) }
-- CNonCanonical have been canonicalised
-data InteractResult
- = KeepInert -- Keep the inert item, and solve the work item from it
- -- (if the latter is Wanted; just discard it if not)
- | KeepWork -- Keep the work item, and solve the inert item from it
-
-instance Outputable InteractResult where
- ppr KeepInert = text "keep inert"
- ppr KeepWork = text "keep work-item"
-
-solveOneFromTheOther :: Ct -- Inert (Dict or Irred)
- -> Ct -- WorkItem (same predicate as inert)
- -> InteractResult
--- Precondition:
--- * inert and work item represent evidence for the /same/ predicate
--- * Both are CDictCan or CIrredCan
---
--- We can always solve one from the other: even if both are wanted,
--- although we don't rewrite wanteds with wanteds, we can combine
--- two wanteds into one by solving one from the other
-
-solveOneFromTheOther ct_i ct_w
- | CtWanted { ctev_loc = loc_w } <- ev_w
- , prohibitedSuperClassSolve loc_i loc_w
- -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
- = -- Inert must be Given
- KeepWork
-
- | CtWanted {} <- ev_w
- = -- Inert is Given or Wanted
- case ev_i of
- CtGiven {} -> KeepInert
- -- work is Wanted; inert is Given: easy choice.
-
- CtWanted {} -- Both are Wanted
- -- If only one has no pending superclasses, use it
- -- Otherwise we can get infinite superclass expansion (#22516)
- -- in silly cases like class C T b => C a b where ...
- | not is_psc_i, is_psc_w -> KeepInert
- | is_psc_i, not is_psc_w -> KeepWork
-
- -- If only one is a WantedSuperclassOrigin (arising from expanding
- -- a Wanted class constraint), keep the other: wanted superclasses
- -- may be unexpected by users
- | not is_wsc_orig_i, is_wsc_orig_w -> KeepInert
- | is_wsc_orig_i, not is_wsc_orig_w -> KeepWork
-
- -- otherwise, just choose the lower span
- -- reason: if we have something like (abs 1) (where the
- -- Num constraint cannot be satisfied), it's better to
- -- get an error about abs than about 1.
- -- This test might become more elaborate if we see an
- -- opportunity to improve the error messages
- | ((<) `on` ctLocSpan) loc_i loc_w -> KeepInert
- | otherwise -> KeepWork
-
- -- From here on the work-item is Given
-
- | CtWanted { ctev_loc = loc_i } <- ev_i
- , prohibitedSuperClassSolve loc_w loc_i
- = KeepInert -- Just discard the un-usable Given
- -- This never actually happens because
- -- Givens get processed first
-
- | CtWanted {} <- ev_i
- = KeepWork
-
- -- From here on both are Given
- -- See Note [Replacement vs keeping]
-
- | lvl_i == lvl_w
- = same_level_strategy
-
- | otherwise -- Both are Given, levels differ
- = different_level_strategy
- where
- ev_i = ctEvidence ct_i
- ev_w = ctEvidence ct_w
-
- pred = ctEvPred ev_i
-
- loc_i = ctEvLoc ev_i
- loc_w = ctEvLoc ev_w
- orig_i = ctLocOrigin loc_i
- orig_w = ctLocOrigin loc_w
- lvl_i = ctLocLevel loc_i
- lvl_w = ctLocLevel loc_w
-
- is_psc_w = isPendingScDict ct_w
- is_psc_i = isPendingScDict ct_i
-
- is_wsc_orig_i = isWantedSuperclassOrigin orig_i
- is_wsc_orig_w = isWantedSuperclassOrigin orig_w
-
- different_level_strategy -- Both Given
- | 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]
-
- same_level_strategy -- Both Given
- = case (orig_i, orig_w) of
-
- (GivenSCOrigin _ depth_i blocked_i, GivenSCOrigin _ depth_w blocked_w)
- | blocked_i, not blocked_w -> KeepWork -- Case 2(a) from
- | not blocked_i, blocked_w -> KeepInert -- Note [Replacement vs keeping]
-
- -- Both blocked or both not blocked
-
- | depth_w < depth_i -> KeepWork -- Case 2(c) from
- | otherwise -> KeepInert -- Note [Replacement vs keeping]
-
- (GivenSCOrigin {}, _) -> KeepWork -- Case 2(b) from Note [Replacement vs keeping]
-
- _ -> KeepInert -- Case 2(d) from Note [Replacement vs keeping]
-
-{-
-Note [Replacement vs keeping]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When we have two Given constraints both of type (C tys), say, which should
-we keep? More subtle than you might think! This is all implemented in
-solveOneFromTheOther.
-
- 1) Constraints come from different levels (different_level_strategy)
-
- - For implicit parameters we want to keep the innermost (deepest)
- one, so that it overrides the outer one.
- See Note [Shadowing of Implicit Parameters]
-
- - 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,
- and can be reported as redundant. See Note [Tracking redundant constraints]
- in GHC.Tc.Solver.
-
- It transpires that using the outermost one is responsible for an
- 8% performance improvement in nofib cryptarithm2, compared to
- just rolling the dice. I didn't investigate why.
-
- 2) Constraints coming from the same level (i.e. same implication)
-
- (a) If both are GivenSCOrigin, choose the one that is unblocked if possible
- according to Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance.
-
- (b) Prefer constraints that are not superclass selections. Example:
-
- f :: (Eq a, Ord a) => a -> Bool
- f x = x == x
-
- Eager superclass expansion gives us two [G] Eq a constraints. We
- want to keep the one from the user-written Eq a, not the superclass
- selection. This means we report the Ord a as redundant with
- -Wredundant-constraints, not the Eq a.
-
- Getting this wrong was #20602. See also
- Note [Tracking redundant constraints] in GHC.Tc.Solver.
-
- (c) If both are GivenSCOrigin, chooose the one with the shallower
- superclass-selection depth, in the hope of identifying more correct
- redundant constraints. This is really a generalization of point (b),
- because the superclass depth of a non-superclass constraint is 0.
-
- (If the levels differ, we definitely won't have both with GivenSCOrigin.)
-
- (d) Finally, when there is still a choice, use KeepInert rather than
- KeepWork, for two reasons:
- - to avoid unnecessary munging of the inert set.
- - to cut off superclass loops; see Note [Superclass loops] in GHC.Tc.Solver.Canonical
-
-Doing the level-check for implicit parameters, rather than making the work item
-always override, is important. Consider
- data T a where { T1 :: (?x::Int) => T Int; T2 :: T a }
-
- f :: (?x::a) => T a -> Int
- f T1 = ?x
- f T2 = 3
-
-We have a [G] (?x::a) in the inert set, and at the pattern match on T1 we add
-two new givens in the work-list: [G] (?x::Int)
- [G] (a ~ Int)
-Now consider these steps
- - process a~Int, kicking out (?x::a)
- - process (?x::Int), the inner given, adding to inert set
- - process (?x::a), the outer given, overriding the inner given
-Wrong! The level-check ensures that the inner implicit parameter wins.
-(Actually I think that the order in which the work-list is processed means
-that this chain of events won't happen, but that's very fragile.)
-
-*********************************************************************************
-* *
- interactIrred
-* *
-*********************************************************************************
-
-Note [Multiple matching irreds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-You might think that it's impossible to have multiple irreds all match the
-work item; after all, interactIrred looks for matches and solves one from the
-other. However, note that interacting insoluble, non-droppable irreds does not
-do this matching. We thus might end up with several insoluble, non-droppable,
-matching irreds in the inert set. When another irred comes along that we have
-not yet labeled insoluble, we can find multiple matches. These multiple matches
-cause no harm, but it would be wrong to ASSERT that they aren't there (as we
-once had done). This problem can be tickled by typecheck/should_compile/holes.
-
--}
-
--- Two pieces of irreducible evidence: if their types are *exactly identical*
--- we can rewrite them. We can never improve using this:
--- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not
--- mean that (ty1 ~ ty2)
-interactIrred :: InertCans -> IrredCt -> TcS (StopOrContinue Ct)
-
-interactIrred inerts irred_w@(IrredCt { ir_ev = ev_w, ir_reason = reason })
- | isInsolubleReason reason
- -- For insolubles, don't allow the constraint to be dropped
- -- which can happen with solveOneFromTheOther, so that
- -- we get distinct error messages with -fdefer-type-errors
- = carry_on
-
- | let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w
- , ((irred_i, swap) : _rest) <- bagToList matching_irreds
- -- See Note [Multiple matching irreds]
- , let ev_i = irredCtEvidence irred_i
- ct_i = CIrredCan irred_i
- = do { traceTcS "iteractIrred" $
- vcat [ text "wanted:" <+> (ppr ct_w $$ ppr (ctOrigin ct_w))
- , text "inert: " <+> (ppr ct_i $$ ppr (ctOrigin ct_i)) ]
- ; case solveOneFromTheOther ct_i ct_w of
- KeepInert -> do { setEvBindIfWanted ev_w IsCoherent (swap_me swap ev_i)
- ; return (Stop ev_w (text "Irred equal:KeepInert" <+> ppr ct_w)) }
- KeepWork -> do { setEvBindIfWanted ev_i IsCoherent (swap_me swap ev_w)
- ; updInertIrreds (\_ -> others)
- ; carry_on } }
-
- | otherwise
- = carry_on
-
- where
- ct_w = CIrredCan irred_w
- carry_on = continueWith ct_w
-
- swap_me :: SwapFlag -> CtEvidence -> EvTerm
- swap_me swap ev
- = case swap of
- NotSwapped -> ctEvTerm ev
- IsSwapped -> evCoercion (mkSymCo (evTermCoercion (ctEvTerm ev)))
-
-{-
-*********************************************************************************
+{- ******************************************************************************
* *
interactDict
* *
@@ -1192,42 +942,10 @@ topReactionsStage :: Ct -> SolverStage Ct
-- so try interaction with top-level instances.
topReactionsStage work_item
= Stage $
- do { traceTcS "doTopReact" (ppr work_item)
- ; case work_item of
-
- CDictCan {} ->
- do { inerts <- getTcSInerts
- ; doTopReactDict inerts work_item }
-
- CEqCan {} -> continueWith work_item -- "Canonicalisation" stage is
- -- full solver for equalities
-
- CIrredCan {} ->
- doTopReactOther work_item
+ do { case work_item of
+ CDictCan {} -> do { inerts <- getTcSInerts
+ ; doTopReactDict inerts work_item }
-- Any other work item does not react with any top-level equations
_ -> continueWith work_item }
---------------------
-doTopReactOther :: Ct -> TcS (StopOrContinue Ct)
--- Try local quantified constraints for
--- CEqCan e.g. (lhs ~# ty)
--- and CIrredCan e.g. (c a)
---
--- Why equalities? See GHC.Tc.Solver.Canonical
--- Note [Equality superclasses in quantified constraints]
-doTopReactOther work_item
- | isGiven ev
- = continueWith work_item
-
- | otherwise
- = do { res <- matchLocalInst pred loc
- ; case res of
- OneInst {} -> chooseInstance ev res
- _ -> continueWith work_item }
-
- where
- ev = ctEvidence work_item
- loc = ctEvLoc ev
- pred = ctEvPred ev
-
=====================================
compiler/GHC/Tc/Solver/Irred.hs
=====================================
@@ -0,0 +1,124 @@
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE RecursiveDo #-}
+
+module GHC.Tc.Solver.Irred(
+ solveIrred, tryInertIrreds
+ ) where
+
+import GHC.Prelude
+
+import GHC.Tc.Types.Constraint
+import GHC.Tc.Solver.InertSet
+import GHC.Tc.Solver.Dict( matchLocalInst, chooseInstance )
+import GHC.Tc.Solver.Monad
+import GHC.Tc.Types.Evidence
+
+import GHC.Core.Coercion
+import GHC.Core.InstEnv ( Coherence(..) )
+
+import GHC.Types.Basic( SwapFlag(..) )
+
+import GHC.Utils.Outputable
+
+
+import GHC.Data.Bag
+
+
+{- *********************************************************************
+* *
+* Irreducibles
+* *
+********************************************************************* -}
+
+solveIrred :: IrredCt -> SolverStage Ct
+solveIrred irred
+ = do { tryInertIrreds irred
+ ; tryQCsIrredCt irred
+ ; return (CIrredCan irred) }
+
+{- *********************************************************************
+* *
+* Inert Irreducibles
+* *
+********************************************************************* -}
+
+-- Two pieces of irreducible evidence: if their types are *exactly identical*
+-- we can rewrite them. We can never improve using this:
+-- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not
+-- mean that (ty1 ~ ty2)
+tryInertIrreds :: IrredCt -> SolverStage ()
+tryInertIrreds irred
+ = Stage $ do { ics <- getInertCans
+ ; try_inert_irreds ics irred }
+
+try_inert_irreds :: InertCans -> IrredCt -> TcS (StopOrContinue ())
+
+try_inert_irreds inerts irred_w@(IrredCt { ir_ev = ev_w, ir_reason = reason })
+ | isInsolubleReason reason
+ -- For insolubles, don't allow the constraint to be dropped
+ -- which can happen with solveOneFromTheOther, so that
+ -- we get distinct error messages with -fdefer-type-errors
+ = continueWith ()
+
+ | let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w
+ , ((irred_i, swap) : _rest) <- bagToList matching_irreds
+ -- See Note [Multiple matching irreds]
+ , let ev_i = irredCtEvidence irred_i
+ ct_i = CIrredCan irred_i
+ = do { traceTcS "iteractIrred" $
+ vcat [ text "wanted:" <+> (ppr ct_w $$ ppr (ctOrigin ct_w))
+ , text "inert: " <+> (ppr ct_i $$ ppr (ctOrigin ct_i)) ]
+ ; case solveOneFromTheOther ct_i ct_w of
+ KeepInert -> do { setEvBindIfWanted ev_w IsCoherent (swap_me swap ev_i)
+ ; return (Stop ev_w (text "Irred equal:KeepInert" <+> ppr ct_w)) }
+ KeepWork -> do { setEvBindIfWanted ev_i IsCoherent (swap_me swap ev_w)
+ ; updInertIrreds (\_ -> others)
+ ; continueWith () } }
+
+ | otherwise
+ = continueWith ()
+
+ where
+ ct_w = CIrredCan irred_w
+
+ swap_me :: SwapFlag -> CtEvidence -> EvTerm
+ swap_me swap ev
+ = case swap of
+ NotSwapped -> ctEvTerm ev
+ IsSwapped -> evCoercion (mkSymCo (evTermCoercion (ctEvTerm ev)))
+
+
+{- Note [Multiple matching irreds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+You might think that it's impossible to have multiple irreds all match the
+work item; after all, interactIrred looks for matches and solves one from the
+other. However, note that interacting insoluble, non-droppable irreds does not
+do this matching. We thus might end up with several insoluble, non-droppable,
+matching irreds in the inert set. When another irred comes along that we have
+not yet labeled insoluble, we can find multiple matches. These multiple matches
+cause no harm, but it would be wrong to ASSERT that they aren't there (as we
+once had done). This problem can be tickled by typecheck/should_compile/holes.
+-}
+
+{- *********************************************************************
+* *
+* Quantified constraints
+* *
+********************************************************************* -}
+
+tryQCsIrredCt :: IrredCt -> SolverStage ()
+-- Try local quantified constraints for
+-- and CIrredCan e.g. (c a)
+tryQCsIrredCt (IrredCt { ir_ev = ev })
+ | isGiven ev
+ = Stage $ continueWith ()
+
+ | otherwise
+ = Stage $ do { res <- matchLocalInst pred loc
+ ; case res of
+ OneInst {} -> chooseInstance ev res
+ _ -> continueWith () }
+ where
+ loc = ctEvLoc ev
+ pred = ctEvPred ev
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -354,7 +354,7 @@ addInertCan ct =
do { traceTcS "addInertCan {" $
text "Trying to insert new inert item:" <+> ppr ct
; mkTcS (\TcSEnv{tcs_abort_on_insoluble=abort_flag} ->
- when (abort_flag && insolubleEqCt ct) TcM.failM)
+ when (abort_flag && insolubleCt ct) TcM.failM)
; ics <- getInertCans
; ics <- maybeKickOut ics ct
; tclvl <- getTcLevel
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -57,7 +57,7 @@ module GHC.Tc.Types.Constraint (
addInsols, dropMisleading, addSimples, addImplics, addHoles,
addNotConcreteError, addDelayedErrors,
tyCoVarsOfWC, tyCoVarsOfWCList,
- insolubleWantedCt, insolubleEqCt, insolubleCt, insolubleIrredCt,
+ insolubleWantedCt, insolubleCt, insolubleIrredCt,
insolubleImplic, nonDefaultableTyVarsOfWC,
Implication(..), implicationPrototype, checkTelescopeSkol,
@@ -1306,30 +1306,13 @@ insolubleWantedCt ct = insolubleCt ct &&
not (arisesFromGivens ct) &&
not (isWantedWantedFunDepOrigin (ctOrigin ct))
-insolubleEqCt :: Ct -> Bool
--- Returns True of /equality/ constraints
--- that are /definitely/ insoluble
--- It won't detect some definite errors like
--- F a ~ T (F a)
--- where F is a type family, which actually has an occurs check
---
--- The function is tuned for application /after/ constraint solving
--- i.e. assuming canonicalisation has been done
--- E.g. It'll reply True for a ~ [a]
--- but False for [a] ~ a
--- and
--- True for Int ~ F a Int
--- but False for Maybe Int ~ F a Int Int
--- (where F is an arity-1 type function)
-insolubleEqCt (CIrredCan ir_ct) = insolubleIrredCt ir_ct
-insolubleEqCt _ = False
-
insolubleIrredCt :: IrredCt -> Bool
+-- Returns True of Irred constraints that are /definitely/ insoluble
insolubleIrredCt (IrredCt { ir_reason = reason })
= isInsolubleReason reason
--- | Returns True of equality constraints that are definitely insoluble,
--- as well as TypeError constraints.
+-- | Returns True of constraints that are definitely insoluble,
+-- as well as TypeError constraints.
-- Can return 'True' for Given constraints, unlike 'insolubleWantedCt'.
--
-- This function is critical for accurate pattern-match overlap warnings.
@@ -1338,8 +1321,15 @@ insolubleIrredCt (IrredCt { ir_reason = reason })
-- Note that this does not traverse through the constraint to find
-- nested custom type errors: it only detects @TypeError msg :: Constraint@,
-- and not e.g. @Eq (TypeError msg)@.
+--
+-- The function is tuned for application /after/ constraint solving
+-- i.e. assuming canonicalisation has been done
+-- That's why it looks only for IrredCt, with an insoluble IrredCtReason
insolubleCt :: Ct -> Bool
-insolubleCt ct = isTopLevelUserTypeError (ctPred ct) || insolubleEqCt ct
+insolubleCt ct
+ | isTopLevelUserTypeError (ctPred ct) = True
+ | CIrredCan ir_ct <- ct = insolubleIrredCt ir_ct
+ | otherwise = False
where
-- NB: 'isTopLevelUserTypeError' detects constraints of the form "TypeError msg"
-- and "Unsatisfiable msg". It deliberately does not detect TypeError
=====================================
compiler/ghc.cabal.in
=====================================
@@ -726,6 +726,7 @@ Library
GHC.Tc.Solver.Rewrite
GHC.Tc.Solver.InertSet
GHC.Tc.Solver.Interact
+ GHC.Tc.Solver.Irred
GHC.Tc.Solver.Equality
GHC.Tc.Solver.Dict
GHC.Tc.Solver.Monad
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/527a494351981a89b88af927ef144976556e7c7d
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/527a494351981a89b88af927ef144976556e7c7d
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/20230507/88a04eb1/attachment-0001.html>
More information about the ghc-commits
mailing list