[Git][ghc/ghc][wip/T23070-dicts] Progress
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Tue May 9 23:40:25 UTC 2023
Simon Peyton Jones pushed to branch wip/T23070-dicts at Glasgow Haskell Compiler / GHC
Commits:
6279c5c9 by Simon Peyton Jones at 2023-05-10T00:40:05+01:00
Progress
- - - - -
8 changed files:
- compiler/GHC/Core/Predicate.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Interact.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Solver/Types.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/TcMType.hs
Changes:
=====================================
compiler/GHC/Core/Predicate.hs
=====================================
@@ -51,8 +51,6 @@ import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Data.FastString
-import Control.Monad ( guard )
-
-- | A predicate in the solver. The solver tries to prove Wanted predicates
-- from Given ones.
data Pred
@@ -327,12 +325,14 @@ isCallStackTy ty
-- | Decomposes a predicate if it is an implicit parameter. Does not look in
-- superclasses. See also [Local implicit parameters].
-isIPPred_maybe :: Type -> Maybe (FastString, Type)
-isIPPred_maybe ty =
- do (tc,[t1,t2]) <- splitTyConApp_maybe ty
- guard (isIPTyCon tc)
- x <- isStrLitTy t1
- return (x,t2)
+isIPPred_maybe :: Class -> [Type] -> Maybe (FastString, Type)
+isIPPred_maybe cls tys
+ | cls `hasKey` ipClassKey
+ , [t1,t2] <- tys
+ , Just x <- isStrLitTy t1
+ = Just (x,t2)
+ | otherwise
+ = Nothing
{- Note [Local implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -11,37 +11,51 @@ 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.Types.Evidence
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Origin
+import GHC.Tc.Types.EvTerm( evCallStack )
import GHC.Tc.Solver.InertSet
import GHC.Tc.Solver.Monad
import GHC.Tc.Solver.Types
-import GHC.Builtin.Names ( coercibleTyConKey, heqTyConKey, eqTyConKey )
+import GHC.Hs.Type( HsIPName(..) )
-import GHC.Core.Type as Type
+import GHC.Builtin.Names ( coercibleTyConKey, heqTyConKey, eqTyConKey, ipClassKey )
+
+import GHC.Core
+import GHC.Core.Type
import GHC.Core.InstEnv ( DFunInstType, Coherence(..) )
import GHC.Core.Class
import GHC.Core.Predicate
+import GHC.Core.Multiplicity ( scaledThing )
import GHC.Core.Unify ( ruleMatchTyKiX )
+import GHC.Types.Name.Set
import GHC.Types.Var
+import GHC.Types.Id( mkTemplateLocals )
import GHC.Types.Var.Set
import GHC.Types.SrcLoc
import GHC.Types.Var.Env
import GHC.Types.Unique( hasKey )
-import GHC.Utils.Monad ( foldlM )
+import GHC.Utils.Monad ( concatMapM, foldlM )
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Misc
+import GHC.Data.Bag
+
import GHC.Driver.Session
import qualified GHC.LanguageExtensions as LangExt
-import Data.Maybe ( listToMaybe, mapMaybe )
+import Data.Maybe ( listToMaybe, mapMaybe, isJust )
+
+import Control.Monad.Trans.Maybe( MaybeT, runMaybeT )
+import Control.Monad.Trans.Class( lift )
+import Control.Monad( mzero )
{- *********************************************************************
@@ -50,23 +64,23 @@ import Data.Maybe ( listToMaybe, mapMaybe )
* *
********************************************************************* -}
+solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage Ct
+-- NC: this comes from CNonCanonical or CIrredCan
+-- Precondition: already rewritten by inert set
+solveDictNC ev cls tys
+ = do { dict_ct <- Stage $ mkDictCt ev cls tys
+ ; solveDict dict_ct }
+
solveDict :: DictCt -> SolverStage Ct
-- Preconditions: `tys` are already rewritten by the inert set
-solveDict dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tyargs = tys })
+solveDict dict_ct@(DictCt { di_ev = ev, di_class = cls, di_tyargs = tys })
= assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $
- do { tryInertSet dict_ct
+ do { tryInertDicts dict_ct
; tryInstances dict_ct
; tryFunDeps dict_ct
- ; tryLastResortProhibitedSuperclass dict_ct
+ ; tryLastResortProhibitedSuperClass dict_ct
; return (CDictCan dict_ct) }
-solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage Ct
--- NC: this comes from CNonCanonical or CIrredCan
--- Precondition: already rewritten by inert set
-solveDictNC ev cls tys
- = do { dict_ct <- Stage $ mkDictCt ev cls tys
- ; solveClass dict_ct }
-
mkDictCt :: CtEvidence -> Class -> [Type] -> SolverStage DictCt
-- Once-only processing of Dict constraints:
-- * expand superclasses
@@ -78,8 +92,8 @@ mkDictCt ev cls tys
; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev [] [] cls tys
-- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel]
; emitWork (listToBag sc_cts)
- ; continueWith (DictCt { di_ev = ev, di_cls = cls
- , di_tys = tys, di_pend_sc = doNotExpand }) }
+ ; continueWith (DictCt { di_ev = ev, di_class = cls
+ , di_tyargs = tys, di_pend_sc = doNotExpand }) }
-- doNotExpand: We have already expanded superclasses for /this/ dict
-- so set the fuel to doNotExpand to avoid repeating expansion
@@ -107,8 +121,8 @@ mkDictCt ev cls tys
(ctLocSpan loc) (ctEvExpr new_ev)
; solveCallStack ev ev_cs
- ; continueWith (DictCt { di_ev = new_ev, di_cls = cls
- , di_tys = tys, di_pend_sc = doNotExpand }) }
+ ; continueWith (DictCt { di_ev = new_ev, di_class = cls
+ , di_tyargs = tys, di_pend_sc = doNotExpand }) }
-- doNotExpand: No superclasses for class CallStack
-- See invariants in CDictCan.cc_pend_sc
@@ -117,8 +131,8 @@ mkDictCt ev cls tys
; let fuel | classHasSCs cls = wantedsFuel dflags
| otherwise = doNotExpand
-- See Invariants in `CCDictCan.cc_pend_sc`
- ; continueWith (DictCt { di_ev = ev, di_cls = cls
- , di_tys = tys, di_pend_sc = fuel }) }
+ ; continueWith (DictCt { di_ev = ev, di_class = cls
+ , di_tyargs = tys, di_pend_sc = fuel }) }
where
loc = ctEvLoc ev
orig = ctLocOrigin loc
@@ -415,10 +429,10 @@ tryInertDicts dict_ct
= Stage $ do { inerts <- getInertCans
; try_inert_dicts inerts dict_ct }
-try_inert_dicts :: InertCans -> DicCt -> TcS (StopOrContinue ())
-try_inert_dicts inerts ct_w@(DictCt { di_ev = ev_w, di_class = cls, di_tyargs = tys })
- | Just ct_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
- , let ev_i = ctEvidence ct_i
+try_inert_dicts :: InertCans -> DictCt -> TcS (StopOrContinue ())
+try_inert_dicts inerts dict_w@(DictCt { di_ev = ev_w, di_class = cls, di_tyargs = tys })
+ | Just dict_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
+ , let ev_i = dictCtEvidence dict_i
loc_i = ctEvLoc ev_i
loc_w = ctEvLoc ev_w
= -- There is a matching dictionary in the inert set
@@ -440,18 +454,18 @@ try_inert_dicts inerts ct_w@(DictCt { di_ev = ev_w, di_class = cls, di_tyargs =
do { -- The short-cut solver didn't fire, and loopy superclasses
-- are dealt with, so we can either solve
-- the inert from the work-item or vice-versa.
- ; case solveOneFromTheOther ct_i ct_w of
- KeepInert -> do { traceTcS "lookupInertDict:KeepInert" (ppr ct_w)
+ ; case solveOneFromTheOther (CDictCan dict_i) (CDictCan dict_w) of
+ KeepInert -> do { traceTcS "lookupInertDict:KeepInert" (ppr dict_w)
; setEvBindIfWanted ev_w IsCoherent (ctEvTerm ev_i)
- ; return $ Stop ev_w (text "Dict equal" <+> ppr ct_w) }
- KeepWork -> do { traceTcS "lookupInertDict:KeepWork" (ppr ct_w)
+ ; return $ Stop ev_w (text "Dict equal" <+> ppr dict_w) }
+ KeepWork -> do { traceTcS "lookupInertDict:KeepWork" (ppr dict_w)
; setEvBindIfWanted ev_i IsCoherent (ctEvTerm ev_w)
; updInertDicts $ \ ds -> delDict ds cls tys
; continueWith () } } }
| cls `hasKey` ipClassKey
, isGiven ev_w
- = interactGivenIP inerts ct_w
+ = interactGivenIP inerts dict_w
| otherwise
= continueWith ()
@@ -567,7 +581,7 @@ shortCutSolver dflags ev_w ev_i
**********************************************************************
-}
-interactGivenIP :: InertCans -> Ct -> TcS (StopOrContinue a)
+interactGivenIP :: InertCans -> DictCt -> TcS (StopOrContinue a)
-- Work item is Given (?x:ty)
-- See Note [Shadowing of Implicit Parameters]
interactGivenIP inerts workItem@(DictCt { di_ev = ev, di_class = cls
@@ -581,7 +595,7 @@ interactGivenIP inerts workItem@(DictCt { di_ev = ev, di_class = cls
filtered_dicts = addDictsByClass dicts cls other_ip_dicts
-- Pick out any Given constraints for the same implicit parameter
- is_this_ip (CDictCan { cc_ev = ev, cc_tyargs = ip_str':_ })
+ is_this_ip (DictCt { di_ev = ev, di_tyargs = ip_str':_ })
= isGiven ev && ip_str `tcEqType` ip_str'
is_this_ip _ = False
@@ -646,7 +660,7 @@ I can think of two ways to fix this:
2. Move the shadowing machinery to the location where we nest
implications, and add some code here that will produce an
error if we get multiple givens for the same implicit parameter.
-
+-}
{- *******************************************************************
* *
@@ -1163,7 +1177,7 @@ Test cases:
Historical note: a previous solution was to instead pick the local instance
with the least superclass depth (see Note [Replacement vs keeping]),
but that doesn't work for the example from #22216.
-
+-}
{- *******************************************************************
* *
@@ -1171,13 +1185,13 @@ but that doesn't work for the example from #22216.
* *
**********************************************************************-}
-tryLastResortProhibitedSuperclass :: InertSet -> DictCt -> TcS (StopOrContinue Ct)
+tryLastResortProhibitedSuperClass :: DictCt -> TcS (StopOrContinue Ct)
-- ^ As a last resort, we TEMPORARILY allow a prohibited superclass solve,
-- emitting a loud warning when doing so: we might be creating non-terminating
-- evidence (as we are in T22912 for example).
--
-- See Note [Migrating away from loopy superclass solving] in GHC.Tc.TyCl.Instance.
-tryLastResortProhibitedSuperclass dict_ct
+tryLastResortProhibitedSuperClass dict_ct
= Stage $ do { inerts <- getInertCans
; last_resort inerts dict_ct }
@@ -1187,7 +1201,7 @@ last_resort inerts work_item@(DictCt { di_ev = ev_w, di_class = cls, di_tyargs =
orig_w = ctLocOrigin loc_w
, ScOrigin _ NakedSc <- orig_w -- work_item is definitely Wanted
, Just ct_i <- lookupInertDict (inert_cans inerts) loc_w cls xis
- , let ev_i = ctEvidence ct_i
+ , let ev_i = dictCtEvidence ct_i
, isGiven ev_i
= do { setEvBindIfWanted ev_w IsCoherent (ctEvTerm ev_i)
; ctLocWarnTcS loc_w $
@@ -1197,7 +1211,7 @@ tryLastResortProhibitedSuperclass _ _
= continueWith ()
-************************************************************************
+{- *********************************************************************
* *
* Functional dependencies, instantiation of equations
* *
@@ -1467,8 +1481,8 @@ doLocalFunDepImprovement (DictCt { di_ev = work_ev, di_class = cls })
work_pred = ctEvPred work_ev
work_loc = ctEvLoc work_ev
- add_fds :: Bool -> Ct -> TcS Bool
- add_fds so_far inert_ct
+ add_fds :: Bool -> DictCt -> TcS Bool
+ add_fds so_far (DictCt { di_ev = inert_ev })
| isGiven work_ev && isGiven inert_ev
-- Do not create FDs from Given/Given interactions: See Note [No Given/Given fundeps]
= return so_far
@@ -1485,10 +1499,9 @@ doLocalFunDepImprovement (DictCt { di_ev = work_ev, di_class = cls })
; return (so_far || unifs)
}
where
- inert_ev = ctEvidence inert_ct
inert_pred = ctEvPred inert_ev
inert_loc = ctEvLoc inert_ev
- inert_rewriters = ctRewriters inert_ct
+ inert_rewriters = ctEvRewriters inert_ev
derived_loc = work_loc { ctl_depth = ctl_depth work_loc `maxSubGoalDepth`
ctl_depth inert_loc
, ctl_origin = FunDepOrigin1 work_pred
@@ -1500,12 +1513,12 @@ doLocalFunDepImprovement (DictCt { di_ev = work_ev, di_class = cls })
doLocalFunDepImprovement work_item = pprPanic "doLocalFunDepImprovement" (ppr work_item)
-doTopFunDepImprovement :: Ct -> TcS Bool
+doTopFunDepImprovement :: DictCt -> TcS Bool
-- Try to functional-dependency improvement between the constraint
-- and the top-level instance declarations
-- See Note [Fundeps with instances, and equality orientation]
-- See also Note [Weird fundeps]
-doTopFunDepImprovement work_item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = xis })
+doTopFunDepImprovement work_item@(DictCt { di_ev = ev, di_class = cls, di_tyargs = xis })
= do { traceTcS "try_fundeps" (ppr work_item)
; instEnvs <- getInstEnvs
; let fundep_eqns = improveFromInstEnv instEnvs mk_ct_loc cls xis
@@ -1805,7 +1818,7 @@ makeSuperClasses :: [Ct] -> TcS [Ct]
-- 2. Their fuel (stored in cc_pend_sc or qci_pend_sc) is > 0
makeSuperClasses cts = concatMapM go cts
where
- go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys, cc_pend_sc = fuel })
+ go (CDictCan (DictCt { di_ev = ev, di_class = cls, di_tyargs = tys, di_pend_sc = fuel }))
= assertFuelPreconditionStrict fuel $ -- fuel needs to be more than 0 always
mkStrictSuperClasses fuel ev [] [] cls tys
go (CQuantCan (QCI { qci_pred = pred, qci_ev = ev, qci_pend_sc = fuel }))
@@ -1987,8 +2000,8 @@ mk_superclasses_of fuel rec_clss ev tvs theta cls tys
rec_clss' = rec_clss `extendNameSet` cls_nm
mk_this_ct :: ExpansionFuel -> Ct
mk_this_ct fuel | null tvs, null theta
- = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys
- , cc_pend_sc = fuel }
+ = CDictCan (DictCt { di_ev = ev, di_class = cls
+ , di_tyargs = tys, di_pend_sc = fuel })
-- NB: If there is a loop, we cut off, so we have not
-- added the superclasses, hence cc_pend_sc = fuel
| otherwise
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -1125,14 +1125,14 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more
-- wrt inert_eqs
-- Can include both [G] and [W]
- , inert_dicts :: DictMap Ct
+ , inert_dicts :: DictMap DictCt
-- Dictionaries only
-- All fully rewritten (modulo flavour constraints)
-- wrt inert_eqs
, inert_insts :: [QCInst]
- , inert_safehask :: DictMap Ct
+ , inert_safehask :: DictMap DictCt
-- Failed dictionary resolution due to Safe Haskell overlapping
-- instances restriction. We keep this separate from inert_dicts
-- as it doesn't cause compilation failure, just safe inference
@@ -1371,11 +1371,11 @@ addInertItem tc_lvl
addInertItem tc_lvl ics@(IC { inert_irreds = irreds }) ct@(CIrredCan irred)
= updateGivenEqs tc_lvl ct $ -- An Irred might turn out to be an
- -- equality, so we play safe
+ -- equality, so we play safe
ics { inert_irreds = irreds `snocBag` irred }
-addInertItem _ ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
- = ics { inert_dicts = addDict (inert_dicts ics) cls tys item }
+addInertItem _ ics (CDictCan dict@(DictCt { di_class = cls, di_tyargs = tys }))
+ = ics { inert_dicts = addDict (inert_dicts ics) cls tys dict }
addInertItem _ _ item
= pprPanic "upd_inert set: can't happen! Inserting " $
@@ -1437,14 +1437,14 @@ kickOutRewritableLHS new_fr new_lhs
-- constraints, which perhaps may have become soluble after new_lhs
-- is substituted; ditto the dictionaries, which may include (a~b)
-- or (a~~b) constraints.
- kicked_out = (dicts_out `andCts` fmap CIrredCan irs_out)
+ kicked_out = (fmap CDictCan dicts_out `andCts` fmap CIrredCan irs_out)
`extendCtsList` insts_out
`extendCtsList` map CEqCan tv_eqs_out
`extendCtsList` map CEqCan feqs_out
(tv_eqs_out, tv_eqs_in) = partitionInertEqs kick_out_eq tv_eqs
(feqs_out, feqs_in) = partitionFunEqs kick_out_eq funeqmap
- (dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap
+ (dicts_out, dicts_in) = partitionDicts (kick_out_ct . CDictCan) dictmap
(irs_out, irs_in) = partitionBag (kick_out_ct . CIrredCan) irreds
-- Kick out even insolubles: See Note [Rewrite insolubles]
-- Of course we must kick out irreducibles like (c a), in case
@@ -1677,9 +1677,9 @@ noMatchableGivenDicts inerts@(IS { inert_cans = inert_cans }) loc_w clas tys
where
pred_w = mkClassPred clas tys
- matchable_given :: Ct -> Bool
- matchable_given ct
- | CtGiven { ctev_loc = loc_g, ctev_pred = pred_g } <- ctEvidence ct
+ matchable_given :: DictCt -> Bool
+ matchable_given (DictCt { di_ev = ev })
+ | CtGiven { ctev_loc = loc_g, ctev_pred = pred_g } <- ev
= isJust $ mightEqualLater inerts pred_g loc_g pred_w loc_w
| otherwise
=====================================
compiler/GHC/Tc/Solver/Interact.hs
=====================================
@@ -157,7 +157,7 @@ solveSimples cts
do { sel <- selectNextWorkItem
; case sel of
Nothing -> return ()
- Just ct -> do { runSolverPipeline thePipeline ct
+ Just ct -> do { runSolverPipeline ct
; solve_loop } }
-- | Extract the (inert) givens and invoke the plugins on them.
@@ -295,11 +295,9 @@ runTcPluginSolvers solvers all_cts
CtWanted {} -> (givens, (ev,ct):wanteds)
-runSolverPipeline :: [(String, Ct -> SolverStage Ct)] -- The pipeline
- -> Ct -- The work item
- -> TcS ()
+runSolverPipeline :: Ct -> TcS ()
-- Run this item down the pipeline, leaving behind new work and inerts
-runSolverPipeline full_pipeline workItem
+runSolverPipeline workItem
= do { wl <- getWorkList
; inerts <- getTcSInerts
; tclevel <- getTcLevel
@@ -318,7 +316,7 @@ runSolverPipeline full_pipeline workItem
solve ct
= do { traceTcS "solve {" (text "workitem = " <+> ppr ct)
; res <- runSolverStage (solveCt ct)
- ; traceTcS ("end solve }" (ppr res)
+ ; traceTcS "end solve }" (ppr res)
; case res of
StartAgain ct -> do { traceTcS "Go round again" (ppr ct)
; solve ct }
@@ -331,7 +329,7 @@ runSolverPipeline full_pipeline workItem
-> do { addInertCan ct
; traceFireTcS (ctEvidence ct) (text "Kept as inert")
; traceTcS "End solver pipeline (kept as inert) }"
- (text "final_item =" <+> ppr ct) }
+ (text "final_item =" <+> ppr ct) } }
{-
Example 1:
@@ -358,10 +356,6 @@ React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
-}
-thePipeline :: [(String, Ct -> SolverStage Ct)]
-thePipeline = [ ("canonicalization", GHC.Tc.Solver.Canonical.canonicalize)
- , ("interact with inerts", interactWithInertsStage)
- , ("top-level reactions", topReactionsStage) ]
{-
*********************************************************************************
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -371,16 +371,16 @@ maybeKickOut ics ct
-- See [Kick out existing binding for implicit parameter]
| isGivenCt ct
- , CDictCan { cc_class = cls, cc_tyargs = [ip_name_strty, _ip_ty] } <- ct
+ , CDictCan (DictCt { di_class = cls, di_tyargs = [ip_name_strty, _ip_ty] }) <- ct
, isIPClass cls
, Just ip_name <- isStrLitTy ip_name_strty
-- Would this be more efficient if we used findDictsByClass and then delDict?
= let dict_map = inert_dicts ics
dict_map' = filterDicts doesn't_match_ip_name dict_map
- doesn't_match_ip_name :: Ct -> Bool
- doesn't_match_ip_name ct
- | Just (inert_ip_name, _inert_ip_ty) <- isIPPred_maybe (ctPred ct)
+ doesn't_match_ip_name :: DictCt -> Bool
+ doesn't_match_ip_name (DictCt { di_class = cls, di_tyargs = tys })
+ | Just (inert_ip_name, _inert_ip_ty) <- isIPPred_maybe cls tys
= inert_ip_name /= ip_name
| otherwise
@@ -478,24 +478,21 @@ kickOutAfterFillingCoercionHole hole
= False
--------------
-addInertSafehask :: InertCans -> Ct -> InertCans
-addInertSafehask ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
+addInertSafehask :: InertCans -> DictCt -> InertCans
+addInertSafehask ics item@(DictCt { di_class = cls, di_tyargs = tys })
= ics { inert_safehask = addDict (inert_dicts ics) cls tys item }
-addInertSafehask _ item
- = pprPanic "addInertSafehask: can't happen! Inserting " $ ppr item
-
-insertSafeOverlapFailureTcS :: InstanceWhat -> Ct -> TcS ()
+insertSafeOverlapFailureTcS :: InstanceWhat -> DictCt -> TcS ()
-- See Note [Safe Haskell Overlapping Instances Implementation] in GHC.Tc.Solver
insertSafeOverlapFailureTcS what item
| safeOverlap what = return ()
| otherwise = updInertCans (\ics -> addInertSafehask ics item)
-getSafeOverlapFailures :: TcS Cts
+getSafeOverlapFailures :: TcS (Bag DictCt)
-- See Note [Safe Haskell Overlapping Instances Implementation] in GHC.Tc.Solver
getSafeOverlapFailures
= do { IC { inert_safehask = safehask } <- getInertCans
- ; return $ foldDicts consCts safehask emptyCts }
+ ; return $ foldDicts consBag safehask emptyBag }
--------------
addSolvedDict :: InstanceWhat -> CtEvidence -> Class -> [Type] -> TcS ()
@@ -551,12 +548,12 @@ updInertCans :: (InertCans -> InertCans) -> TcS ()
updInertCans upd_fn
= updInertTcS $ \ inerts -> inerts { inert_cans = upd_fn (inert_cans inerts) }
-updInertDicts :: (DictMap Ct -> DictMap Ct) -> TcS ()
+updInertDicts :: (DictMap DictCt -> DictMap DictCt) -> TcS ()
-- Modify the inert set with the supplied function
updInertDicts upd_fn
= updInertCans $ \ ics -> ics { inert_dicts = upd_fn (inert_dicts ics) }
-updInertSafehask :: (DictMap Ct -> DictMap Ct) -> TcS ()
+updInertSafehask :: (DictMap DictCt -> DictMap DictCt) -> TcS ()
-- Modify the inert set with the supplied function
updInertSafehask upd_fn
= updInertCans $ \ ics -> ics { inert_safehask = upd_fn (inert_safehask ics) }
@@ -592,14 +589,14 @@ getInertInsols
= do { inert <- getInertCans
; let insols = filterBag insolubleIrredCt (inert_irreds inert)
unsats = findDictsByTyConKey (inert_dicts inert) unsatisfiableClassNameKey
- ; return $ unsats `unionBags` fmap CIrredCan insols }
+ ; return $ fmap CDictCan unsats `unionBags` fmap CIrredCan insols }
getInertGivens :: TcS [Ct]
-- Returns the Given constraints in the inert set
getInertGivens
= do { inerts <- getInertCans
; let all_cts = foldIrreds ((:) . CIrredCan) (inert_irreds inerts)
- $ foldDicts (:) (inert_dicts inerts)
+ $ foldDicts ((:) . CDictCan) (inert_dicts inerts)
$ foldFunEqs ((:) . CEqCan) (inert_funeqs inerts)
$ foldTyEqs ((:) . CEqCan) (inert_eqs inerts)
$ []
@@ -623,28 +620,28 @@ get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts })
-- there are never any Wanteds in the inert set
(sc_pending, ic { inert_dicts = dicts', inert_insts = insts' })
where
- sc_pending = sc_pend_insts ++ sc_pend_dicts
+ sc_pending = sc_pend_insts ++ map CDictCan sc_pend_dicts
+ sc_pend_dicts :: [DictCt]
sc_pend_dicts = foldDicts get_pending dicts []
dicts' = foldr exhaustAndAdd dicts sc_pend_dicts
(sc_pend_insts, insts') = mapAccumL get_pending_inst [] insts
- get_pending :: Ct -> [Ct] -> [Ct] -- Get dicts with cc_pend_sc > 0
+ exhaustAndAdd :: DictCt -> DictMap DictCt -> DictMap DictCt
+ exhaustAndAdd ct@(DictCt { di_class = cls, di_tyargs = tys }) dicts
+ -- exhaust the fuel for this constraint before adding it as
+ -- we don't want to expand these constraints again
+ = addDict dicts cls tys (ct {di_pend_sc = doNotExpand})
+
+ get_pending :: DictCt -> [DictCt] -> [DictCt] -- Get dicts with cc_pend_sc > 0
get_pending dict dicts
- | isPendingScDict dict
- , belongs_to_this_level (ctEvidence dict)
+ | isPendingScDictCt dict
+ , belongs_to_this_level (dictCtEvidence dict)
= dict : dicts
| otherwise
= dicts
- exhaustAndAdd :: Ct -> DictMap Ct -> DictMap Ct
- exhaustAndAdd ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts
- -- exhaust the fuel for this constraint before adding it as
- -- we don't want to expand these constraints again
- = addDict dicts cls tys (ct {cc_pend_sc = doNotExpand})
- exhaustAndAdd ct _ = pprPanic "getPendingScDicts" (ppr ct)
-
get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst)
get_pending_inst cts qci@(QCI { qci_ev = ev })
| Just qci' <- pendingScInst_maybe qci
@@ -674,32 +671,31 @@ getUnsolvedInerts
, inert_dicts = idicts
} <- getInertCans
- ; let unsolved_tv_eqs = foldTyEqs add_if_unsolved_eq tv_eqs emptyCts
- unsolved_fun_eqs = foldFunEqs add_if_unsolved_eq fun_eqs emptyCts
- unsolved_irreds = Bag.filterBag (isWanted . irredCtEvidence) irreds
- unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts
- unsolved_others = fmap CIrredCan unsolved_irreds `unionBags`
- unsolved_dicts
+ ; let unsolved_tv_eqs = foldTyEqs (add_if_unsolved CEqCan) tv_eqs emptyCts
+ unsolved_fun_eqs = foldFunEqs (add_if_unsolved CEqCan) fun_eqs emptyCts
+ unsolved_irreds = foldr (add_if_unsolved CIrredCan) emptyCts irreds
+ unsolved_dicts = foldDicts (add_if_unsolved CDictCan) idicts emptyCts
; implics <- getWorkListImplics
; traceTcS "getUnsolvedInerts" $
vcat [ text " tv eqs =" <+> ppr unsolved_tv_eqs
, text "fun eqs =" <+> ppr unsolved_fun_eqs
- , text "others =" <+> ppr unsolved_others
+ , text "dicts =" <+> ppr unsolved_dicts
+ , text "irreds =" <+> ppr unsolved_irreds
, text "implics =" <+> ppr implics ]
; return ( implics, unsolved_tv_eqs `unionBags`
unsolved_fun_eqs `unionBags`
- unsolved_others) }
+ unsolved_irreds `unionBags`
+ unsolved_dicts ) }
where
- add_if_unsolved :: Ct -> Cts -> Cts
- add_if_unsolved ct cts | isWantedCt ct = ct `consCts` cts
- | otherwise = cts
-
- add_if_unsolved_eq :: EqCt -> Cts -> Cts
- add_if_unsolved_eq eq_ct cts | isWanted (eq_ev eq_ct) = CEqCan eq_ct `consCts` cts
- | otherwise = cts
+ add_if_unsolved :: (a -> Ct) -> a -> Cts -> Cts
+ add_if_unsolved mk_ct thing cts
+ | isWantedCt ct = ct `consCts` cts
+ | otherwise = cts
+ where
+ ct = mk_ct thing
getHasGivenEqs :: TcLevel -- TcLevel of this implication
-> TcS ( HasGivenEqs -- are there Given equalities?
@@ -743,7 +739,7 @@ removeInertCt :: InertCans -> Ct -> InertCans
removeInertCt is ct =
case ct of
- CDictCan { cc_class = cl, cc_tyargs = tys } ->
+ CDictCan (DictCt { di_class = cl, di_tyargs = tys }) ->
is { inert_dicts = delDict (inert_dicts is) cl tys }
CEqCan eq_ct -> delEq is eq_ct
@@ -771,7 +767,7 @@ lookupInInerts loc pty
| ClassPred cls tys <- classifyPredType pty
= do { inerts <- getTcSInerts
; let mb_solved = lookupSolvedDict inerts loc cls tys
- mb_inert = fmap ctEvidence (lookupInertDict (inert_cans inerts) loc cls tys)
+ mb_inert = fmap dictCtEvidence (lookupInertDict (inert_cans inerts) loc cls tys)
; return $ do -- Maybe monad
found_ev <- mb_solved `mplus` mb_inert
@@ -786,7 +782,7 @@ lookupInInerts loc pty
= return Nothing
-- | Look up a dictionary inert.
-lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe Ct
+lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe DictCt
lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
= case findDict dicts loc cls tys of
Just ct -> Just ct
=====================================
compiler/GHC/Tc/Solver/Types.hs
=====================================
@@ -157,24 +157,21 @@ delDict m cls tys = delTcApp m (classTyCon cls) tys
addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a
addDict m cls tys item = insertTcApp m (classTyCon cls) tys item
-addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
+addDictsByClass :: DictMap DictCt -> Class -> Bag DictCt -> DictMap DictCt
addDictsByClass m cls items
= extendDTyConEnv m (classTyCon cls) (foldr add emptyTM items)
where
- add ct@(CDictCan { cc_tyargs = tys }) tm = insertTM tys ct tm
- add ct _ = pprPanic "addDictsByClass" (ppr ct)
+ add ct@(DictCt { di_tyargs = tys }) tm = insertTM tys ct tm
-filterDicts :: (Ct -> Bool) -> DictMap Ct -> DictMap Ct
+filterDicts :: (DictCt -> Bool) -> DictMap DictCt -> DictMap DictCt
filterDicts f m = filterTcAppMap f m
-partitionDicts :: (Ct -> Bool) -> DictMap Ct -> (Bag Ct, DictMap Ct)
+partitionDicts :: (DictCt -> Bool) -> DictMap DictCt -> (Bag DictCt, DictMap DictCt)
partitionDicts f m = foldTcAppMap k m (emptyBag, emptyDictMap)
where
k ct (yeses, noes) | f ct = (ct `consBag` yeses, noes)
| otherwise = (yeses, add ct noes)
- add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) m
- = addDict m cls tys ct
- add ct _ = pprPanic "partitionDicts" (ppr ct)
+ add ct@(DictCt { di_class = cls, di_tyargs = tys }) m = addDict m cls tys ct
dictsToBag :: DictMap a -> Bag a
dictsToBag = tcAppMapToBag
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -13,7 +13,7 @@ module GHC.Tc.Types.Constraint (
Xi, Ct(..), EqCt(..), Cts,
singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
isEmptyCts, emptyCts, andCts, ctsPreds,
- isPendingScDict, pendingScDict_maybe,
+ isPendingScDictCt, isPendingScDict, pendingScDict_maybe,
superClassesMightHelp, getPendingWantedScs,
isWantedCt, isGivenCt,
isTopLevelUserTypeError, containsUserTypeError, getUserTypeErrorMsg,
@@ -29,6 +29,7 @@ module GHC.Tc.Types.Constraint (
tyCoVarsOfCt, tyCoVarsOfCts,
tyCoVarsOfCtList, tyCoVarsOfCtsList,
+ DictCt(..), dictCtEvidence,
IrredCt(..), mkIrredCt, ctIrredCt, irredCtEvidence, irredCtPred,
ExpansionFuel, doNotExpand, consumeFuel, pendingFuel,
@@ -203,8 +204,8 @@ data Ct
--------------- DictCt --------------
-data DictCt = DictCt { -- e.g. Num ty
- = DictCt { di_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
+data DictCt -- e.g. Num ty
+ = DictCt { di_ev :: CtEvidence -- See Note [Ct/evidence invariant]
, di_class :: Class
, di_tyargs :: [Xi] -- di_tyargs are rewritten w.r.t. inerts, so Xi
@@ -217,6 +218,12 @@ data DictCt = DictCt { -- e.g. Num ty
-- (b) those superclasses are not yet explored
}
+dictCtEvidence :: DictCt -> CtEvidence
+dictCtEvidence = di_ev
+
+instance Outputable DictCt where
+ ppr dict = ppr (CDictCan dict)
+
--------------- EqCt --------------
{- Note [Canonical equalities]
@@ -717,7 +724,7 @@ updCtEvidence upd ct
CEqCan eq@(EqCt { eq_ev = ev }) -> CEqCan (eq { eq_ev = upd ev })
CIrredCan ir@(IrredCt { ir_ev = ev }) -> CIrredCan (ir { ir_ev = upd ev })
CNonCanonical ev -> CNonCanonical (upd ev)
- CDictCan { cc_ev = ev } -> ct { cc_ev = upd ev }
+ CDictCan di@(DictCt { di_ev = ev }) -> CDictCan (di { di_ev = upd ev })
ctLoc :: Ct -> CtLoc
ctLoc = ctEvLoc . ctEvidence
@@ -773,7 +780,7 @@ instance Outputable Ct where
pp_sort = case ct of
CEqCan {} -> text "CEqCan"
CNonCanonical {} -> text "CNonCanonical"
- CDictCan (DictCt { ci_pend_sc = psc })
+ CDictCan (DictCt { di_pend_sc = psc })
| psc > 0 -> text "CDictCan" <> parens (text "psc" <+> ppr psc)
| otherwise -> text "CDictCan"
CIrredCan (IrredCt { ir_reason = reason }) -> text "CIrredCan" <> ppr reason
@@ -1022,16 +1029,19 @@ isUnsatisfiableCt_maybe t
= Nothing
isPendingScDict :: Ct -> Bool
-isPendingScDict (CDictCan (DictCt { di_pend_sc = f })) = pendingFuel f
+isPendingScDict (CDictCan dict_ct) = isPendingScDictCt dict_ct
+isPendingScDict _ = False
+
+isPendingScDictCt :: DictCt -> Bool
-- Says whether this is a CDictCan with di_pend_sc has positive fuel;
-- i.e. pending un-expanded superclasses
-isPendingScDict _ = False
+isPendingScDictCt (DictCt { di_pend_sc = f }) = pendingFuel f
pendingScDict_maybe :: Ct -> Maybe Ct
-- Says whether this is a CDictCan with di_pend_sc has fuel left,
-- AND if so exhausts the fuel so that they are not expanded again
-pendingScDict_maybe ct@(CDictCan (DictCt { di_pend_sc = f }))
- | pendingFuel f = Just (ct { di_pend_sc = doNotExpand })
+pendingScDict_maybe (CDictCan dict@(DictCt { di_pend_sc = f }))
+ | pendingFuel f = Just (CDictCan (dict { di_pend_sc = doNotExpand }))
| otherwise = Nothing
pendingScDict_maybe _ = Nothing
@@ -2156,12 +2166,16 @@ eqCtFlavourRole :: EqCt -> CtFlavourRole
eqCtFlavourRole (EqCt { eq_ev = ev, eq_eq_rel = eq_rel })
= (ctEvFlavour ev, eq_rel)
+dictCtFlavourRole :: DictCt -> CtFlavourRole
+dictCtFlavourRole (DictCt { di_ev = ev })
+ = (ctEvFlavour ev, NomEq)
+
-- | Extract the flavour and role from a 'Ct'
ctFlavourRole :: Ct -> CtFlavourRole
-- Uses short-cuts to role for special cases
-ctFlavourRole (CDictCan { cc_ev = ev }) = (ctEvFlavour ev, NomEq)
-ctFlavourRole (CEqCan eq_ct) = eqCtFlavourRole eq_ct
-ctFlavourRole ct = ctEvFlavourRole (ctEvidence ct)
+ctFlavourRole (CDictCan di_ct) = dictCtFlavourRole di_ct
+ctFlavourRole (CEqCan eq_ct) = eqCtFlavourRole eq_ct
+ctFlavourRole ct = ctEvFlavourRole (ctEvidence ct)
{- Note [eqCanRewrite]
~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -2455,10 +2455,10 @@ creates e.g. a CDictCan where the cc_tyars are /not/ fully reduced.
zonkCt :: Ct -> TcM Ct
-- See Note [zonkCt behaviour]
-zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
+zonkCt (CDictCan dict@(DictCt { di_ev = ev, di_tyargs = args }))
= do { ev' <- zonkCtEvidence ev
; args' <- mapM zonkTcType args
- ; return $ ct { cc_ev = ev', cc_tyargs = args' } }
+ ; return (CDictCan (dict { di_ev = ev', di_tyargs = args' })) }
zonkCt (CEqCan (EqCt { eq_ev = ev }))
= mkNonCanonical <$> zonkCtEvidence ev
@@ -2792,18 +2792,19 @@ naughtyQuantification orig_ty tv escapees
zonkCtRewriterSet :: Ct -> TcM Ct
zonkCtRewriterSet ct
- | isGivenCt ct = return ct
+ | isGivenCt ct
+ = return ct
| otherwise
= case ct of
CEqCan eq@(EqCt { eq_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev
; return (CEqCan (eq { eq_ev = ev' })) }
CIrredCan ir@(IrredCt { ir_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev
; return (CIrredCan (ir { ir_ev = ev' })) }
- CNonCanonical ev -> do { ev' <- zonkCtEvRewriterSet ev
- ; return (CNonCanonical ev') }
- CDictCan { cc_ev = ev } -> do { ev' <- zonkCtEvRewriterSet ev
- ; return (ct { cc_ev = ev' }) }
- CQuantCan {} -> return ct
+ CDictCan di@(DictCt { di_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev
+ ; return (CDictCan (di { di_ev = ev' })) }
+ CQuantCan {} -> return ct
+ CNonCanonical ev -> do { ev' <- zonkCtEvRewriterSet ev
+ ; return (CNonCanonical ev') }
zonkCtEvRewriterSet :: CtEvidence -> TcM CtEvidence
zonkCtEvRewriterSet ev@(CtGiven {})
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6279c5c94f427a84b148daf011e397c535125e26
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6279c5c94f427a84b148daf011e397c535125e26
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/20230509/f4d8e19f/attachment-0001.html>
More information about the ghc-commits
mailing list