[Git][ghc/ghc][wip/T23070-dicts] More
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Thu May 11 23:26:08 UTC 2023
Simon Peyton Jones pushed to branch wip/T23070-dicts at Glasgow Haskell Compiler / GHC
Commits:
064080f9 by Simon Peyton Jones at 2023-05-12T00:25:49+01:00
More
- - - - -
8 changed files:
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Irred.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/Tc/Solver/Dict.hs
=====================================
@@ -23,7 +23,7 @@ import GHC.Tc.Solver.Types
import GHC.Hs.Type( HsIPName(..) )
-import GHC.Builtin.Names ( coercibleTyConKey, heqTyConKey, eqTyConKey, ipClassKey )
+import GHC.Builtin.Names ( coercibleTyConKey, heqTyConKey, eqTyConKey )
import GHC.Core
import GHC.Core.Type
@@ -56,7 +56,7 @@ import Data.Maybe ( listToMaybe, mapMaybe, isJust )
import Control.Monad.Trans.Maybe( MaybeT, runMaybeT )
import Control.Monad.Trans.Class( lift )
-import Control.Monad( mzero )
+import Control.Monad( mzero, when )
{- *********************************************************************
@@ -65,36 +65,45 @@ import Control.Monad( mzero )
* *
********************************************************************* -}
-solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage Ct
+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 <- Stage $ canDictCt ev cls tys
+ = do { dict_ct <- simpleStage (canDictCt ev cls tys)
; solveDict dict_ct }
-solveDict :: DictCt -> SolverStage Ct
+solveDict :: DictCt -> SolverStage ()
-- Preconditions: `tys` are already rewritten by the inert set
-solveDict dict_ct@(DictCt { di_ev = ev, di_class = cls, di_tyargs = tys })
+solveDict dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = tys })
= assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $
do { tryInertDicts dict_ct
; tryInstances dict_ct
; tryFunDeps dict_ct
; tryLastResortProhibitedSuperClass dict_ct
- ; return (CDictCan dict_ct) }
+ ; simpleStage (updInertDicts dict_ct)
+ ; Stage (stopWith (dictCtEvidence dict_ct) "Kept inert DictCt") }
-canDictCt :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue DictCt)
+updInertDicts :: DictCt -> TcS ()
+updInertDicts dict_ct@(DictCt { di_cls = cls, di_ev = ev })
+ = do { -- See [Kick out existing binding for implicit parameter]
+ ; when (isGiven ev && isIPClass cls) $
+ updInertCans (updDicts (delIPDict dict_ct))
+
+ -- Add the new constraint to the inert set
+ ; updInertCans (updDicts (addDict dict_ct)) }
+
+canDictCt :: CtEvidence -> Class -> [Type] -> TcS DictCt
-- Once-only processing of Dict constraints:
-- * expand superclasses
-- * deal with CallStack
--- After this we have a (CDictCan (DictCt ..))
canDictCt 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]
; emitWork (listToBag sc_cts)
- ; continueWith (DictCt { di_ev = ev, di_class = cls
- , di_tyargs = tys, di_pend_sc = doNotExpand }) }
+ ; return (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
@@ -122,8 +131,8 @@ canDictCt ev cls tys
(ctLocSpan loc) (ctEvExpr new_ev)
; solveCallStack ev ev_cs
- ; continueWith (DictCt { di_ev = new_ev, di_class = cls
- , di_tyargs = tys, di_pend_sc = doNotExpand }) }
+ ; return (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
@@ -132,8 +141,8 @@ canDictCt ev cls tys
; let fuel | classHasSCs cls = wantedsFuel dflags
| otherwise = doNotExpand
-- See Invariants in `CCDictCan.cc_pend_sc`
- ; continueWith (DictCt { di_ev = ev, di_class = cls
- , di_tyargs = tys, di_pend_sc = fuel }) }
+ ; return (DictCt { di_ev = ev, di_cls = cls
+ , di_tys = tys, di_pend_sc = fuel }) }
where
loc = ctEvLoc ev
orig = ctLocOrigin loc
@@ -150,6 +159,22 @@ solveCallStack ev ev_cs
; setEvBindIfWanted ev IsCoherent ev_tm }
+{- Note [Kick out existing binding for implicit parameter]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have (typecheck/should_compile/ImplicitParamFDs)
+ flub :: (?x :: Int) => (Int, Integer)
+ flub = (?x, let ?x = 5 in ?x)
+When we are checking the last ?x occurrence, we guess its type
+to be a fresh unification variable alpha and emit an (IP "x" alpha)
+constraint. But the given (?x :: Int) has been translated to an
+IP "x" Int constraint, which has a functional dependency from the
+name to the type. So fundep interaction tells us that alpha ~ Int,
+and we get a type error. This is bad.
+
+Instead, we wish to excise any old given for an IP when adding a
+new one.
+-}
+
{- ******************************************************************************
* *
interactDict
@@ -431,7 +456,7 @@ tryInertDicts dict_ct
; try_inert_dicts inerts dict_ct }
try_inert_dicts :: InertCans -> DictCt -> TcS (StopOrContinue ())
-try_inert_dicts inerts dict_w@(DictCt { di_ev = ev_w, di_class = cls, di_tyargs = tys })
+try_inert_dicts inerts dict_w@(DictCt { di_ev = ev_w, di_cls = cls, di_tys = tys })
| Just dict_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
, let ev_i = dictCtEvidence dict_i
loc_i = ctEvLoc ev_i
@@ -461,12 +486,14 @@ try_inert_dicts inerts dict_w@(DictCt { di_ev = ev_w, di_class = cls, di_tyargs
; 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
+ ; updInertCans (updDicts $ delDict dict_w)
; continueWith () } } }
+{-
| cls `hasKey` ipClassKey
, isGiven ev_w
= interactGivenIP inerts dict_w
+-}
| otherwise
= continueWith ()
@@ -478,31 +505,31 @@ shortCutSolver :: DynFlags
-> TcS Bool -- True <=> success
shortCutSolver dflags ev_w ev_i
| isWanted ev_w
- && isGiven ev_i
- -- We are about to solve a [W] constraint from a [G] constraint. We take
- -- a moment to see if we can get a better solution using an instance.
- -- Note that we only do this for the sake of performance. Exactly the same
- -- programs should typecheck regardless of whether we take this step or
- -- not. See Note [Shortcut solving]
+ , isGiven ev_i
+ -- We are about to solve a [W] constraint from a [G] constraint. We take
+ -- a moment to see if we can get a better solution using an instance.
+ -- Note that we only do this for the sake of performance. Exactly the same
+ -- programs should typecheck regardless of whether we take this step or
+ -- not. See Note [Shortcut solving]
- && not (isIPLikePred (ctEvPred ev_w)) -- Not for implicit parameters (#18627)
+ , not (isIPLikePred (ctEvPred ev_w)) -- Not for implicit parameters (#18627)
- && not (xopt LangExt.IncoherentInstances dflags)
- -- If IncoherentInstances is on then we cannot rely on coherence of proofs
- -- in order to justify this optimization: The proof provided by the
- -- [G] constraint's superclass may be different from the top-level proof.
- -- See Note [Shortcut solving: incoherence]
+ , not (xopt LangExt.IncoherentInstances dflags)
+ -- If IncoherentInstances is on then we cannot rely on coherence of proofs
+ -- in order to justify this optimization: The proof provided by the
+ -- [G] constraint's superclass may be different from the top-level proof.
+ -- See Note [Shortcut solving: incoherence]
- && gopt Opt_SolveConstantDicts dflags
- -- Enabled by the -fsolve-constant-dicts flag
+ , gopt Opt_SolveConstantDicts dflags
+ -- Enabled by the -fsolve-constant-dicts flag
= do { ev_binds_var <- getTcEvBindsVar
; ev_binds <- assertPpr (not (isCoEvBindsVar ev_binds_var )) (ppr ev_w) $
getTcEvBindsMap ev_binds_var
; solved_dicts <- getSolvedDicts
- ; mb_stuff <- runMaybeT $ try_solve_from_instance
- (ev_binds, solved_dicts) ev_w
+ ; mb_stuff <- runMaybeT $
+ try_solve_from_instance (ev_binds, solved_dicts) ev_w
; case mb_stuff of
Nothing -> return False
@@ -524,7 +551,6 @@ shortCutSolver dflags ev_w ev_i
-> MaybeT TcS (EvBindMap, DictMap CtEvidence)
try_solve_from_instance (ev_binds, solved_dicts) ev
| let pred = ctEvPred ev
- loc = ctEvLoc ev
, ClassPred cls tys <- classifyPredType pred
= do { inst_res <- lift $ matchGlobalInst dflags True cls tys
; case inst_res of
@@ -534,13 +560,13 @@ shortCutSolver dflags ev_w ev_i
, cir_what = what }
| safeOverlap what
, all isTyFamFree preds -- Note [Shortcut solving: type families]
- -> do { let solved_dicts' = addDict solved_dicts cls tys ev
+ -> do { let solved_dicts' = addSolvedDict cls tys ev solved_dicts
-- solved_dicts': it is important that we add our goal
-- to the cache before we solve! Otherwise we may end
-- up in a loop while solving recursive dictionaries.
; lift $ traceTcS "shortCutSolver: found instance" (ppr preds)
- ; loc' <- lift $ checkInstanceOK loc what pred
+ ; loc' <- lift $ checkInstanceOK (ctEvLoc ev) what pred
; lift $ checkReductionDepth loc' pred
@@ -552,12 +578,13 @@ shortCutSolver dflags ev_w ev_i
ev_binds' = extendEvBinds ev_binds $
mkWantedEvBind (ctEvEvId ev) coherence ev_tm
- ; foldlM try_solve_from_instance
- (ev_binds', solved_dicts')
- (freshGoals evc_vs) }
+ ; foldlM try_solve_from_instance (ev_binds', solved_dicts') $
+ freshGoals evc_vs }
_ -> mzero }
- | otherwise = mzero
+
+ | otherwise
+ = mzero
-- Use a local cache of solved dicts while emitting EvVars for new work
@@ -580,12 +607,13 @@ shortCutSolver dflags ev_w ev_i
**********************************************************************
-}
-interactGivenIP :: InertCans -> DictCt -> TcS (StopOrContinue a)
+{-
+interactGivenIP :: InertCans -> DictCt -> TcS (StopOrContinue ())
-- Work item is Given (?x:ty)
-- See Note [Shadowing of Implicit Parameters]
-interactGivenIP inerts workItem@(DictCt { di_ev = ev, di_class = cls
- , di_tyargs = tys })
- = do { updInertCans $ \cans -> cans { inert_dicts = addDict filtered_dicts cls tys workItem }
+interactGivenIP inerts workItem@(DictCt { di_ev = ev, di_cls = cls
+ , di_tys = tys })
+ = do { updInertCans $ \cans -> cans { inert_dicts = addDict workItem filtered_dicts }
; stopWith ev "Given IP" }
where
dicts = inert_dicts inerts
@@ -598,10 +626,10 @@ interactGivenIP inerts workItem@(DictCt { di_ev = ev, di_class = cls
[] -> pprPanic "interactGivenIP" (ppr workItem)
-- Pick out any Given constraints for the same implicit parameter
- is_this_ip (DictCt { di_ev = ev, di_tyargs = ip_str':_ })
+ is_this_ip (DictCt { di_ev = ev, di_tys = ip_str':_ })
= isGiven ev && ip_str `tcEqType` ip_str'
is_this_ip _ = False
-
+-}
{- Note [Shadowing of Implicit Parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following example:
@@ -678,8 +706,8 @@ tryInstances dict_ct
try_instances :: InertSet -> DictCt -> TcS (StopOrContinue ())
-- Try to use type-class instance declarations to simplify the constraint
-try_instances inerts work_item@(DictCt { di_ev = ev, di_class = cls
- , di_tyargs = xis })
+try_instances inerts work_item@(DictCt { di_ev = ev, di_cls = cls
+ , di_tys = xis })
| isGiven ev -- Never use instances for Given constraints
= continueWith ()
-- See Note [No Given/Given fundeps]
@@ -694,7 +722,7 @@ try_instances inerts work_item@(DictCt { di_ev = ev, di_class = cls
; case lkup_res of
OneInst { cir_what = what }
-> do { insertSafeOverlapFailureTcS what work_item
- ; addSolvedDict what ev cls xis
+ ; updSolvedDicts what work_item
; chooseInstance ev lkup_res }
_ -> -- NoInstance or NotSure
-- We didn't solve it; so try functional dependencies
@@ -1199,7 +1227,7 @@ tryLastResortProhibitedSuperClass dict_ct
; last_resort inerts dict_ct }
last_resort :: InertSet -> DictCt -> TcS (StopOrContinue ())
-last_resort inerts (DictCt { di_ev = ev_w, di_class = cls, di_tyargs = xis })
+last_resort inerts (DictCt { di_ev = ev_w, di_cls = cls, di_tys = xis })
| let loc_w = ctEvLoc ev_w
orig_w = ctLocOrigin loc_w
, ScOrigin _ NakedSc <- orig_w -- work_item is definitely Wanted
@@ -1477,7 +1505,7 @@ tryFunDeps dict_ct
doLocalFunDepImprovement :: DictCt -> TcS Bool
-- Add wanted constraints from type-class functional dependencies.
-doLocalFunDepImprovement (DictCt { di_ev = work_ev, di_class = cls })
+doLocalFunDepImprovement (DictCt { di_ev = work_ev, di_cls = cls })
= do { inerts <- getInertCans
; foldlM add_fds False (findDictsByClass (inert_dicts inerts) cls) }
where
@@ -1519,7 +1547,7 @@ doTopFunDepImprovement :: DictCt -> TcS Bool
-- and the top-level instance declarations
-- See Note [Fundeps with instances, and equality orientation]
-- See also Note [Weird fundeps]
-doTopFunDepImprovement work_item@(DictCt { di_ev = ev, di_class = cls, di_tyargs = xis })
+doTopFunDepImprovement work_item@(DictCt { di_ev = ev, di_cls = cls, di_tys = xis })
= do { traceTcS "try_fundeps" (ppr work_item)
; instEnvs <- getInstEnvs
; let fundep_eqns = improveFromInstEnv instEnvs mk_ct_loc cls xis
@@ -1817,7 +1845,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 (DictCt { di_ev = ev, di_class = cls, di_tyargs = tys, di_pend_sc = fuel }))
+ go (CDictCan (DictCt { di_ev = ev, di_cls = cls, di_tys = 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 }))
@@ -1999,8 +2027,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 (DictCt { di_ev = ev, di_class = cls
- , di_tyargs = tys, di_pend_sc = fuel })
+ = CDictCan (DictCt { di_ev = ev, di_cls = cls
+ , di_tys = 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/Equality.hs
=====================================
@@ -102,7 +102,7 @@ indeed they are!
-}
solveEquality :: CtEvidence -> EqRel -> Type -> Type
- -> SolverStage Ct
+ -> SolverStage ()
solveEquality ev eq_rel ty1 ty2
= do { Pair ty1' ty2' <- zonkEqTypes ev eq_rel ty1 ty2
; let ev' | debugIsOn = setCtEvPredType ev $
@@ -117,15 +117,21 @@ solveEquality ev eq_rel ty1 ty2
-- An IrredCt equality may be insoluble; but maybe not!
-- E.g. m a ~R# m b is not canonical, but may be
-- solved by a quantified constraint (T15290)
- Left irred_ct -> do { tryInertIrreds irred_ct
- ; tryQCsIrredEqCt irred_ct
- ; return (CIrredCan irred_ct) } ;
+ Left irred_ct -> solveIrred irred_ct ;
Right eq_ct -> do { tryInertEqs eq_ct
; tryFunDeps eq_ct
; tryQCsEqCt eq_ct
- ; return (CEqCan eq_ct) } } }
+ ; simpleStage (updInertEqs eq_ct) } } }
+updInertEqs :: EqCt -> TcS ()
+updInertEqs eq_ct@(EqCt { eq_lhs = lhs, eq_ev = ev, eq_eq_rel = eq_rel })
+ = do { ics <- getInertCans
+ ; (_, ics') <- kickOutRewritable (ctEvFlavour ev, eq_rel) lhs ics
+ ; tclvl <- getTcLevel
+ ; updInertCans (updateGivenEqs tc_lvl (CEqCan eq_ct) .
+ addEqToCans eq_ct)
+ }
{- *********************************************************************
@@ -294,9 +300,9 @@ canonicaliseEquality ev eq_rel ty1 ty2
vcat [ ppr ev, ppr eq_rel, ppr ty1, ppr ty2 ]
; rdr_env <- getGlobalRdrEnvTcS
; fam_insts <- getFamInstEnvs
- ; can_eq_nc' False rdr_env fam_insts ev eq_rel ty1 ty1 ty2 ty2 }
+ ; can_eq_nc False rdr_env fam_insts ev eq_rel ty1 ty1 ty2 ty2 }
-can_eq_nc'
+can_eq_nc
:: Bool -- True => both input types are rewritten
-> GlobalRdrEnv -- needed to see which newtypes are in scope
-> FamInstEnvs -- needed to unwrap data instances
@@ -307,27 +313,27 @@ can_eq_nc'
-> TcS (StopOrContinue (Either IrredCt EqCt))
-- See Note [Comparing nullary type synonyms] in GHC.Core.Type.
-can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(TyConApp tc1 []) _ps_ty1 (TyConApp tc2 []) _ps_ty2
+can_eq_nc _flat _rdr_env _envs ev eq_rel ty1@(TyConApp tc1 []) _ps_ty1 (TyConApp tc2 []) _ps_ty2
| tc1 == tc2
= canEqReflexive ev eq_rel ty1
-- Expand synonyms first; see Note [Type synonyms and canonicalization]
-can_eq_nc' rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
- | Just ty1' <- coreView ty1 = can_eq_nc' rewritten rdr_env envs ev eq_rel ty1' ps_ty1 ty2 ps_ty2
- | Just ty2' <- coreView ty2 = can_eq_nc' rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2' ps_ty2
+can_eq_nc rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
+ | Just ty1' <- coreView ty1 = can_eq_nc rewritten rdr_env envs ev eq_rel ty1' ps_ty1 ty2 ps_ty2
+ | Just ty2' <- coreView ty2 = can_eq_nc rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2' ps_ty2
-- need to check for reflexivity in the ReprEq case.
-- See Note [Eager reflexivity check]
-- Check only when rewritten because the zonk_eq_types check in canEqNC takes
-- care of the non-rewritten case.
-can_eq_nc' True _rdr_env _envs ev ReprEq ty1 _ ty2 _
+can_eq_nc True _rdr_env _envs ev ReprEq ty1 _ ty2 _
| ty1 `tcEqType` ty2
= canEqReflexive ev ReprEq ty1
-- When working with ReprEq, unwrap newtypes.
-- See Note [Unwrap newtypes first]
-- This must be above the TyVarTy case, in order to guarantee (TyEq:N)
-can_eq_nc' _rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
+can_eq_nc _rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
| ReprEq <- eq_rel
, Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1
= can_eq_newtype_nc rdr_env envs ev NotSwapped ty1 stuff1 ty2 ps_ty2
@@ -337,10 +343,10 @@ can_eq_nc' _rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
= can_eq_newtype_nc rdr_env envs ev IsSwapped ty2 stuff2 ty1 ps_ty1
-- Then, get rid of casts
-can_eq_nc' rewritten rdr_env envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2
+can_eq_nc rewritten rdr_env envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2
| isNothing (canEqLHS_maybe ty2) -- See (W3) in Note [Equalities with incompatible kinds]
= canEqCast rewritten rdr_env envs ev eq_rel NotSwapped ty1 co1 ty2 ps_ty2
-can_eq_nc' rewritten rdr_env envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _
+can_eq_nc rewritten rdr_env envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _
| isNothing (canEqLHS_maybe ty1) -- See (W3) in Note [Equalities with incompatible kinds]
= canEqCast rewritten rdr_env envs ev eq_rel IsSwapped ty2 co2 ty1 ps_ty1
@@ -349,14 +355,14 @@ can_eq_nc' rewritten rdr_env envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _
----------------------
-- Literals
-can_eq_nc' _rewritten _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
+can_eq_nc _rewritten _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
| l1 == l2
= do { setEvBindIfWanted ev IsCoherent (evCoercion $ mkReflCo (eqRelRole eq_rel) ty1)
; stopWith ev "Equal LitTy" }
-- Decompose FunTy: (s -> t) and (c => t)
-- NB: don't decompose (Int -> blah) ~ (Show a => blah)
-can_eq_nc' _rewritten _rdr_env _envs ev eq_rel
+can_eq_nc _rewritten _rdr_env _envs ev eq_rel
(FunTy { ft_mult = am1, ft_af = af1, ft_arg = ty1a, ft_res = ty1b }) _ps_ty1
(FunTy { ft_mult = am2, ft_af = af2, ft_arg = ty2a, ft_res = ty2b }) _ps_ty2
| af1 == af2 -- See Note [Decomposing FunTy]
@@ -364,7 +370,7 @@ can_eq_nc' _rewritten _rdr_env _envs ev eq_rel
-- Decompose type constructor applications
-- NB: we have expanded type synonyms already
-can_eq_nc' _rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _
+can_eq_nc _rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _
| Just (tc1, tys1) <- tcSplitTyConApp_maybe ty1
, Just (tc2, tys2) <- tcSplitTyConApp_maybe ty2
-- we want to catch e.g. Maybe Int ~ (Int -> Int) here for better
@@ -374,7 +380,7 @@ can_eq_nc' _rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _
, not (isTypeFamilyTyCon tc2)
= canTyConApp ev eq_rel tc1 tys1 tc2 tys2
-can_eq_nc' _rewritten _rdr_env _envs ev eq_rel
+can_eq_nc _rewritten _rdr_env _envs ev eq_rel
s1@(ForAllTy (Bndr _ vis1) _) _
s2@(ForAllTy (Bndr _ vis2) _) _
| vis1 `eqForAllVis` vis2 -- Note [ForAllTy and type equality]
@@ -384,7 +390,7 @@ can_eq_nc' _rewritten _rdr_env _envs ev eq_rel
-- Use tcSplitAppTy, not matching on AppTy, to catch oversaturated type families
-- NB: Only decompose AppTy for nominal equality.
-- See Note [Decomposing AppTy equalities]
-can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ ty2 _
+can_eq_nc True _rdr_env _envs ev NomEq ty1 _ ty2 _
| Just (t1, s1) <- tcSplitAppTy_maybe ty1
, Just (t2, s2) <- tcSplitAppTy_maybe ty2
= can_eq_app ev t1 s1 t2 s2
@@ -394,13 +400,13 @@ can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ ty2 _
-------------------
-- No similarity in type structure detected. Rewrite and try again.
-can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
+can_eq_nc False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
= -- Rewrite the two types and try again
do { (redn1@(Reduction _ xi1), rewriters1) <- rewrite ev ps_ty1
; (redn2@(Reduction _ xi2), rewriters2) <- rewrite ev ps_ty2
; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2
; traceTcS "can_eq_nc: go round again" (ppr new_ev $$ ppr xi1 $$ ppr xi2)
- ; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
+ ; can_eq_nc True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
----------------------------
-- Look for a canonical LHS.
@@ -410,7 +416,8 @@ can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
-- NB: pattern match on True: we want only rewritten types sent to canEqLHS
-- This means we've rewritten any variables and reduced any type family redexes
-- See also Note [No top-level newtypes on RHS of representational equalities]
-can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
+
+can_eq_nc True _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
| Just can_eq_lhs1 <- canEqLHS_maybe ty1
= do { traceTcS "can_eq1" (ppr ty1 $$ ppr ty2)
; canEqCanLHS ev eq_rel NotSwapped can_eq_lhs1 ps_ty1 ty2 ps_ty2 }
@@ -425,15 +432,15 @@ can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
-- _both_ sides of the equality are AppTy-like... but if one side is
-- AppTy-like and the other isn't (and it also isn't a variable or
-- saturated type family application, both of which are handled by
- -- can_eq_nc'), we're in a failure mode and can just fall through.
+ -- can_eq_nc), we're in a failure mode and can just fall through.
----------------------------
-- Fall-through. Give up.
----------------------------
-- We've rewritten and the types don't match. Give up.
-can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
- = do { traceTcS "can_eq_nc' catch-all case" (ppr ps_ty1 $$ ppr ps_ty2)
+can_eq_nc True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
+ = do { traceTcS "can_eq_nc catch-all case" (ppr ps_ty1 $$ ppr ps_ty2)
; case eq_rel of -- See Note [Unsolved equalities]
ReprEq -> finishCanWithIrred ReprEqReason ev
NomEq -> finishCanWithIrred ShapeMismatchReason ev }
@@ -665,7 +672,7 @@ can_eq_newtype_nc rdr_env envs ev swapped ty1 ((gres, co1), ty1') ty2 ps_ty2
; new_ev <- rewriteEqEvidence emptyRewriterSet ev' swapped
redn1 (mkReflRedn Representational ps_ty2)
- ; can_eq_nc' False rdr_env envs new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
+ ; can_eq_nc False rdr_env envs new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
---------
-- ^ Decompose a type application.
@@ -742,7 +749,7 @@ canEqCast rewritten rdr_env envs ev eq_rel swapped ty1 co1 ty2 ps_ty2
; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped
(mkGReflLeftRedn role ty1 co1)
(mkReflRedn role ps_ty2)
- ; can_eq_nc' rewritten rdr_env envs new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
+ ; can_eq_nc rewritten rdr_env envs new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
where
role = eqRelRole eq_rel
@@ -1029,7 +1036,7 @@ There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete:
which is unsatisfiable. Unwrapping, though, leads to a solution.
Conclusion: always unwrap newtypes before attempting to decompose
- them. This is done in can_eq_nc'. Of course, we can't unwrap if the data
+ them. This is done in can_eq_nc. Of course, we can't unwrap if the data
constructor isn't in scope. See Note [Unwrap newtypes first].
* Incompleteness example (EX2): available Givens
@@ -1205,7 +1212,7 @@ and all will be well. See also Note [Unwrap newtypes first].
Bottom line:
* Always decompose AppTy at nominal role: can_eq_app
* Never decompose AppTy at representational role (neither Given nor Wanted):
- the lack of an equation in can_eq_nc'
+ the lack of an equation in can_eq_nc
Extra points
{1} Decomposing a Given AppTy over a representational role is simply
@@ -1734,7 +1741,7 @@ canEqCanLHSFinish, canEqCanLHSFinish_try_unification,
-- preserved as much as possible
-- Guaranteed preconditions that
-- (TyEq:K) handled in canEqCanLHSHomo
- -- (TyEq:N) checked in can_eq_nc'
+ -- (TyEq:N) checked in can_eq_nc
-- (TyEq:TV) handled in canEqCanLHS2
---------------------------
@@ -1903,7 +1910,7 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
----------------------
swapAndFinish :: CtEvidence -> EqRel -> SwapFlag
-> TcType -> CanEqLHS -- ty ~ F tys
- -> TcS (StopOrContinue (Either IrredCt EqCt))
+ -> TcS (StopOrContinue (Either unused EqCt))
-- We have an equality alpha ~ F tys, that we can't unify e.g because 'tys'
-- mentions alpha, it would not be a canonical constraint as-is.
-- We want to flip it to (F tys ~ a), whereupon it is canonical
@@ -1917,8 +1924,9 @@ swapAndFinish ev eq_rel swapped lhs_ty can_rhs
, eq_lhs = can_rhs, eq_rhs = lhs_ty } }
----------------------
-tryIrredInstead :: CheckTyEqResult -> CtEvidence -> EqRel -> SwapFlag
- -> CanEqLHS -> TcType -> TcS (StopOrContinue (Either IrredCt a))
+tryIrredInstead :: CheckTyEqResult -> CtEvidence
+ -> EqRel -> SwapFlag -> CanEqLHS -> TcType
+ -> TcS (StopOrContinue (Either IrredCt unused))
-- We have a non-canonical equality
-- We still swap it if 'swapped' says so, so that it is oriented
-- in the direction that the error-reporting machinery
@@ -2033,7 +2041,7 @@ Wrinkles:
And this is an improvement regardless: because tyvars can, generally,
unify with casted types, there's no reason to go through the work of
stripping off the cast when the cast appears opposite a tyvar. This is
- implemented in the cast case of can_eq_nc'.
+ implemented in the cast case of can_eq_nc.
Historical note:
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -17,9 +17,8 @@ module GHC.Tc.Solver.InertSet (
-- * The inert set
InertSet(..),
InertCans(..),
- InertEqs,
emptyInert,
- addInertItem,
+ addInertItem, addInertDict,
noMatchableGivenDicts,
noGivenNewtypeReprEqs,
@@ -27,12 +26,17 @@ module GHC.Tc.Solver.InertSet (
prohibitedSuperClassSolve,
-- * Inert equalities
+ InertEqs,
foldTyEqs, delEq, findEq,
partitionInertEqs, partitionFunEqs,
- foldFunEqs,
+ foldFunEqs, addEqToCans,
+
+ -- * Inert Dicts
+ updDicts, delDict, delIPDict, addDict, filterDicts, partitionDicts,
+ addSolvedDict,
-- * Inert Irreds
- InertIrreds, delIrred, extendIrreds, foldIrreds,
+ InertIrreds, delIrred, addIrreds, addIrred, foldIrreds,
findMatchingIrreds,
-- * Kick-out
@@ -66,6 +70,7 @@ import GHC.Core.TyCo.FVs
import qualified GHC.Core.TyCo.Rep as Rep
import GHC.Core.Class( Class )
import GHC.Core.TyCon
+import GHC.Core.Class( classTyCon )
import GHC.Core.Unify
import GHC.Utils.Misc ( partitionWith )
@@ -305,8 +310,8 @@ data InertSet
-- (We have no way of "kicking out" from the cache, so putting
-- wanteds here means we can end up solving a Wanted with itself. Bad)
- , inert_solved_dicts :: DictMap CtEvidence
- -- All Wanteds, of form ev :: C t1 .. tn
+ , inert_solved_dicts :: DictMap CtEvidence
+ -- All Wanteds, of form (C t1 .. tn)
-- See Note [Solved dictionaries]
-- and Note [Do not add superclasses of solved dictionaries]
}
@@ -1203,6 +1208,13 @@ instance Outputable InertCans where
emptyTyEqs :: InertEqs
emptyTyEqs = emptyDVarEnv
+addEqToCans :: EqCt -> InertCans -> InertCans
+addEqToCans eq_ct@(EqCt { eq_lhs = lhs })
+ ics@(IC { inert_funeqs = funeqs, inert_eqs = eqs })
+ = case lhs of
+ TyFamLHS tc tys -> ics { inert_funeqs = addCanFunEq funeqs tc tys eq_ct }
+ TyVarLHS tv -> ics { inert_eqs = addTyEq eqs tv eq_ct }
+
addTyEq :: InertEqs -> TcTyVar -> EqCt -> InertEqs
addTyEq old_eqs tv ct
= extendDVarEnv_C add_eq old_eqs tv [ct]
@@ -1216,8 +1228,8 @@ foldTyEqs k eqs z
findTyEqs :: InertCans -> TyVar -> [EqCt]
findTyEqs icans tv = concat @Maybe (lookupDVarEnv (inert_eqs icans) tv)
-delEq :: InertCans -> EqCt -> InertCans
-delEq ic (EqCt { eq_lhs = lhs, eq_rhs = rhs }) = case lhs of
+delEq :: EqCt -> InertCans -> InertCans
+delEq (EqCt { eq_lhs = lhs, eq_rhs = rhs }) ic = case lhs of
TyVarLHS tv
-> ic { inert_eqs = alterDVarEnv upd (inert_eqs ic) tv }
TyFamLHS tf args
@@ -1286,23 +1298,78 @@ extendFunEqs fun_eqs eq_ct@(EqCt { eq_lhs = TyFamLHS tc args })
extendFunEqs _ other = pprPanic "extendFunEqs" (ppr other)
+
+{- *********************************************************************
+* *
+ Inert Dicts
+* *
+********************************************************************* -}
+
+updDicts :: (DictMap DictCt -> DictMap DictCt) -> InertCans -> InertCans
+updDicts upd ics = ics { inert_dicts = upd (inert_dicts ics) }
+
+delDict :: DictCt -> DictMap a -> DictMap a
+delDict (DictCt { di_cls = cls, di_tys = tys }) m
+ = delTcApp m (classTyCon cls) tys
+
+delIPDict :: DictCt -> DictMap DictCt -> DictMap DictCt
+delIPDict (DictCt { di_cls = cls, di_tys = tys }) m
+ | [ip_str, _] <- tys
+ = assert (isIPClass cls) $
+ filterDicts (doesn't_match ip_str) m
+ | otherwise
+ = m
+ where
+ doesn't_match :: TcType -> DictCt -> Bool
+ doesn't_match ip_str (DictCt { di_cls = cls, di_tys = tys })
+ | isIPClass cls
+ , [ip_str', _] <- tys
+ = not (ip_str `eqType` ip_str')
+ | otherwise
+ = True
+
+addDict :: DictCt -> DictMap DictCt -> DictMap DictCt
+addDict item@(DictCt { di_cls = cls, di_tys = tys }) dm
+ = insertTcApp dm (classTyCon cls) tys item
+
+addSolvedDict :: Class -> [Type] -> CtEvidence
+ -> DictMap CtEvidence -> DictMap CtEvidence
+addSolvedDict cls tys ev dm
+ = insertTcApp dm (classTyCon cls) tys ev
+
+filterDicts :: (DictCt -> Bool) -> DictMap DictCt -> DictMap DictCt
+filterDicts f m = filterTcAppMap f m
+
+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, addDict ct noes)
+
+
{- *********************************************************************
* *
Inert Irreds
* *
********************************************************************* -}
-extendIrreds :: [IrredCt] -> InertIrreds -> InertIrreds
-extendIrreds extras irreds
+addIrreds :: [IrredCt] -> InertIrreds -> InertIrreds
+addIrreds extras irreds
| null extras = irreds
| otherwise = irreds `unionBags` listToBag extras
-delIrred :: InertCans -> IrredCt -> InertCans
+addIrred :: IrredCt -> InertIrreds -> InertIrreds
+addIrred extra irreds = irreds `snocBag` extra
+
+updIrreds :: (InertIrreds -> InertIrreds) -> InertCans -> InertCans
+updIrreds upd ics = ics { inert_irreds = upd (inert_irreds ics) }
+
+delIrred :: IrredCt -> InertCans -> InertCans
-- Remove a particular (Given) Irred, on the instructions of a plugin
-- For some reason this is done vis the evidence Id, not the type
-- Compare delEq. I have not idea why
-delIrred ics (IrredCt { ir_ev = ev })
- = ics { inert_irreds = filterBag keep (inert_irreds ics) }
+delIrred (IrredCt { ir_ev = ev }) ics
+ = updIrreds (filterBag keep) ics
where
ev_id = ctEvEvId ev
keep (IrredCt { ir_ev = ev' }) = ev_id == ctEvEvId ev'
@@ -1374,13 +1441,15 @@ addInertItem tc_lvl ics@(IC { inert_irreds = irreds }) ct@(CIrredCan irred)
-- equality, so we play safe
ics { inert_irreds = irreds `snocBag` irred }
-addInertItem _ ics (CDictCan dict@(DictCt { di_class = cls, di_tyargs = tys }))
- = ics { inert_dicts = addDict (inert_dicts ics) cls tys dict }
+addInertItem _ ics (CDictCan dict_ct) = addInertDict dict_ct ics
addInertItem _ _ item
= pprPanic "upd_inert set: can't happen! Inserting " $
ppr item -- Can't be CNonCanonical because they only land in inert_irreds
+addInertDict :: DictCt -> InertCans -> InertCans
+addInertDict dict ics = ics { inert_dicts = addDict dict (inert_dicts ics) }
+
updateGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans
-- Set the inert_given_eq_level to the current level (tclvl)
-- if the constraint is a given equality that should prevent
=====================================
compiler/GHC/Tc/Solver/Irred.hs
=====================================
@@ -3,7 +3,7 @@
{-# LANGUAGE RecursiveDo #-}
module GHC.Tc.Solver.Irred(
- solveIrred, tryInertIrreds, tryQCsIrredCt
+ solveIrred
) where
import GHC.Prelude
@@ -31,11 +31,20 @@ import GHC.Data.Bag
* *
********************************************************************* -}
-solveIrred :: IrredCt -> SolverStage Ct
+solveIrred :: IrredCt -> SolverStage ()
solveIrred irred
= do { tryInertIrreds irred
; tryQCsIrredCt irred
- ; return (CIrredCan irred) }
+ ; simpleStage (updInertIrreds irred) }
+
+
+updInertIrreds :: IrredCt -> TcS ()
+updInertIrreds irred
+ = do { tc_lvl <- getTcLevel
+ ; updInertCans $ (updateGivenEqs tc_lvl (CIrredCan irred) .
+ updIrreds (addIrred irred))
+ ; traceFireTcS (irredCtEvidence irred)
+ (text "Added Irred to inert set") }
{- *********************************************************************
* *
@@ -73,7 +82,7 @@ try_inert_irreds inerts irred_w@(IrredCt { ir_ev = ev_w, ir_reason = reason })
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)
+ ; updInertCans (updIrreds (\_ -> others))
; continueWith () } }
| otherwise
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -32,8 +32,8 @@ module GHC.Tc.Solver.Monad (
QCInst(..),
-- The pipeline
- StopOrContinue(..), continueWith, stopWith, andWhenContinue,
- startAgainWith, SolverStage(Stage, runSolverStage),
+ StopOrContinue(..), continueWith, stopWith,
+ startAgainWith, SolverStage(Stage, runSolverStage), simpleStage,
-- Tracing etc
panicTcS, traceTcS,
@@ -64,7 +64,7 @@ module GHC.Tc.Solver.Monad (
-- Inerts
- updInertTcS, updInertCans, updInertDicts, updInertIrreds,
+ updInertTcS, updInertCans,
getHasGivenEqs, setInertCans,
getInertEqs, getInertCans, getInertGivens,
getInertInsols, getInnermostGivenEqLevel,
@@ -83,7 +83,7 @@ module GHC.Tc.Solver.Monad (
getSafeOverlapFailures,
-- Inert solved dictionaries
- addSolvedDict, lookupSolvedDict,
+ updSolvedDicts, lookupSolvedDict,
-- Irreds
foldIrreds,
@@ -239,6 +239,10 @@ instance Monad SolverStage where
Stop ev d -> return (Stop ev d)
ContinueWith x -> runSolverStage (k x) }
+simpleStage :: TcS a -> SolverStage a
+-- Always does a ContinueWith; no Stop or StartAgain
+simpleStage thing = Stage (do { res <- thing; continueWith res })
+
startAgainWith :: Ct -> TcS (StopOrContinue a)
startAgainWith ct = return (StartAgain ct)
@@ -248,16 +252,6 @@ continueWith ct = return (ContinueWith ct)
stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
stopWith ev s = return (Stop ev (text s))
-andWhenContinue :: TcS (StopOrContinue a)
- -> (a -> TcS (StopOrContinue a))
- -> TcS (StopOrContinue a)
-andWhenContinue tcs1 tcs2
- = do { r <- tcs1
- ; case r of
- ContinueWith ct -> tcs2 ct
- _ -> return r }
-infixr 0 `andWhenContinue` -- allow chaining with ($)
-
{- *********************************************************************
* *
@@ -329,22 +323,6 @@ When adding an equality to the inerts:
* Note that unifying a:=ty, is like adding [G] a~ty; just use
kickOutRewritable with Nominal, Given. See kickOutAfterUnification.
-Note [Kick out existing binding for implicit parameter]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we have (typecheck/should_compile/ImplicitParamFDs)
- flub :: (?x :: Int) => (Int, Integer)
- flub = (?x, let ?x = 5 in ?x)
-When we are checking the last ?x occurrence, we guess its type
-to be a fresh unification variable alpha and emit an (IP "x" alpha)
-constraint. But the given (?x :: Int) has been translated to an
-IP "x" Int constraint, which has a functional dependency from the
-name to the type. So fundep interaction tells us that alpha ~ Int,
-and we get a type error. This is bad.
-
-Instead, we wish to excise any old given for an IP when adding a
-new one. We also must make sure not to float out
-any IP constraints outside an implication that binds an IP of
-the same name; see GHC.Tc.Solver.floatConstraints.
-}
addInertCan :: Ct -> TcS ()
@@ -369,26 +347,6 @@ maybeKickOut ics ct
= do { (_, ics') <- kickOutRewritable (ctEvFlavour ev, eq_rel) lhs ics
; return ics' }
- -- See [Kick out existing binding for implicit parameter]
- | isGivenCt 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 :: 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
- = True
-
- in
- return (ics { inert_dicts = dict_map' })
-
| otherwise
= return ics
@@ -479,8 +437,8 @@ kickOutAfterFillingCoercionHole hole
--------------
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 ics item
+ = ics { inert_safehask = addDict item (inert_dicts ics) }
insertSafeOverlapFailureTcS :: InstanceWhat -> DictCt -> TcS ()
-- See Note [Safe Haskell Overlapping Instances Implementation] in GHC.Tc.Solver
@@ -495,15 +453,15 @@ getSafeOverlapFailures
; return $ foldDicts consBag safehask emptyBag }
--------------
-addSolvedDict :: InstanceWhat -> CtEvidence -> Class -> [Type] -> TcS ()
+updSolvedDicts :: InstanceWhat -> DictCt -> TcS ()
-- Conditionally add a new item in the solved set of the monad
-- See Note [Solved dictionaries] in GHC.Tc.Solver.InertSet
-addSolvedDict what item cls tys
- | isWanted item
+updSolvedDicts what dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = tys })
+ | isWanted ev
, instanceReturnsDictCon what
- = do { traceTcS "updSolvedSetTcs:" $ ppr item
+ = do { traceTcS "updSolvedDicts:" $ ppr dict_ct
; updInertTcS $ \ ics ->
- ics { inert_solved_dicts = addDict (inert_solved_dicts ics) cls tys item } }
+ ics { inert_solved_dicts = addSolvedDict cls tys ev (inert_solved_dicts ics) } }
| otherwise
= return ()
@@ -548,21 +506,11 @@ updInertCans :: (InertCans -> InertCans) -> TcS ()
updInertCans upd_fn
= updInertTcS $ \ inerts -> inerts { inert_cans = upd_fn (inert_cans inerts) }
-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 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) }
-updInertIrreds :: (Bag IrredCt -> Bag IrredCt) -> TcS ()
--- Modify the inert set with the supplied function
-updInertIrreds upd_fn
- = updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) }
-
getInertEqs :: TcS InertEqs
getInertEqs = do { inert <- getInertCans; return (inert_eqs inert) }
@@ -629,10 +577,9 @@ get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts })
(sc_pend_insts, insts') = mapAccumL get_pending_inst [] insts
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
+ exhaustAndAdd ct dicts = addDict (ct {di_pend_sc = doNotExpand}) 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
@@ -739,11 +686,9 @@ removeInertCt :: InertCans -> Ct -> InertCans
removeInertCt is ct =
case ct of
- CDictCan (DictCt { di_class = cl, di_tyargs = tys }) ->
- is { inert_dicts = delDict (inert_dicts is) cl tys }
-
- CEqCan eq_ct -> delEq is eq_ct
- CIrredCan ir_ct -> delIrred is ir_ct
+ CDictCan dict_ct -> is { inert_dicts = delDict dict_ct (inert_dicts is) }
+ CEqCan eq_ct -> delEq eq_ct is
+ CIrredCan ir_ct -> delIrred ir_ct is
CQuantCan {} -> panic "removeInertCt: CQuantCan"
CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
@@ -792,9 +737,7 @@ lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
-- Returns just if exactly this predicate type exists in the solved.
lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys
- = case findDict solved loc cls tys of
- Just ev -> Just ev
- _ -> Nothing
+ = findDict solved loc cls tys
---------------------------
lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe Reduction)
=====================================
compiler/GHC/Tc/Solver/Types.hs
=====================================
@@ -4,17 +4,17 @@
-- | Utility types used within the constraint solver
module GHC.Tc.Solver.Types (
-- Inert CDictCans
- DictMap, emptyDictMap, addDict,
+ DictMap, emptyDictMap,
findDictsByTyConKey, findDictsByClass,
- addDictsByClass, delDict, foldDicts, filterDicts, findDict,
- dictsToBag, partitionDicts,
+ foldDicts, findDict,
+ dictsToBag,
FunEqMap, emptyFunEqs, findFunEq, insertFunEq,
findFunEqsByTyCon,
TcAppMap, emptyTcAppMap, isEmptyTcAppMap,
insertTcApp, alterTcApp, filterTcAppMap,
- tcAppMapToBag, foldTcAppMap,
+ tcAppMapToBag, foldTcAppMap, delTcApp,
EqualCtList, filterEqualCtList, addToEqualCtList
@@ -151,28 +151,6 @@ findDictsByTyConKey m tc
| Just tm <- lookupUDFM_Directly m tc = foldTM consBag tm emptyBag
| otherwise = emptyBag
-delDict :: DictMap a -> Class -> [Type] -> DictMap a
-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 DictCt -> Class -> Bag DictCt -> DictMap DictCt
-addDictsByClass m cls items
- = extendDTyConEnv m (classTyCon cls) (foldr add emptyTM items)
- where
- add ct@(DictCt { di_tyargs = tys }) tm = insertTM tys ct tm
-
-filterDicts :: (DictCt -> Bool) -> DictMap DictCt -> DictMap DictCt
-filterDicts f m = filterTcAppMap f m
-
-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@(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
=====================================
@@ -196,25 +196,24 @@ assertFuelPreconditionStrict fuel = assertPpr (pendingFuel fuel) insufficientFue
data Ct
= CDictCan DictCt
- | CNonCanonical CtEvidence -- See Note [NonCanonical Semantics] in GHC.Tc.Solver.Monad
| CIrredCan IrredCt -- A "irreducible" constraint (non-canonical)
| CEqCan EqCt -- A canonical equality constraint
| CQuantCan QCInst -- A quantified constraint
-
+ | CNonCanonical CtEvidence -- See Note [NonCanonical Semantics] in GHC.Tc.Solver.Monad
--------------- DictCt --------------
data DictCt -- e.g. Num ty
- = DictCt { di_ev :: CtEvidence -- See Note [Ct/evidence invariant]
+ = 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
+ , di_cls :: Class
+ , di_tys :: [Xi] -- di_tys are rewritten w.r.t. inerts, so Xi
, di_pend_sc :: ExpansionFuel
-- See Note [The superclass story] in GHC.Tc.Solver.Dict
-- See Note [Expanding Recursive Superclasses and ExpansionFuel] in GHC.Tc.Solver
-- Invariants: di_pend_sc > 0 <=>
- -- (a) di_class has superclasses
+ -- (a) di_cls has superclasses
-- (b) those superclasses are not yet explored
}
@@ -650,7 +649,7 @@ Note [Ct/evidence invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If ct :: Ct, then extra fields of 'ct' cache precisely the ctev_pred field
of (cc_ev ct), and is fully rewritten wrt the substitution. Eg for DictCt,
- ctev_pred (di_ev ct) = (di_class ct) (di_tyargs ct)
+ ctev_pred (di_ev ct) = (di_cls ct) (di_tys ct)
This holds by construction; look at the unique place where DictCt is
built (in GHC.Tc.Solver.Dict.canDictNC).
@@ -1065,8 +1064,8 @@ superClassesMightHelp (WC { wc_simple = simples, wc_impl = implics })
might_help_ct ct = not (is_ip ct)
- is_ip (CDictCan (DictCt { di_class = cls })) = isIPClass cls
- is_ip _ = False
+ is_ip (CDictCan (DictCt { di_cls = cls })) = isIPClass cls
+ is_ip _ = False
getPendingWantedScs :: Cts -> ([Ct], Cts)
-- in the return values [Ct] has original fuel while Cts has fuel exhausted
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -2455,10 +2455,10 @@ reduced. -}
zonkCt :: Ct -> TcM Ct
-- See Note [zonkCt behaviour]
-zonkCt (CDictCan dict@(DictCt { di_ev = ev, di_tyargs = args }))
+zonkCt (CDictCan dict@(DictCt { di_ev = ev, di_tys = args }))
= do { ev' <- zonkCtEvidence ev
; args' <- mapM zonkTcType args
- ; return (CDictCan (dict { di_ev = ev', di_tyargs = args' })) }
+ ; return (CDictCan (dict { di_ev = ev', di_tys = args' })) }
zonkCt (CEqCan (EqCt { eq_ev = ev }))
= mkNonCanonical <$> zonkCtEvidence ev
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/064080f90fde3135209d8fdfb7f848e0abe84082
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/064080f90fde3135209d8fdfb7f848e0abe84082
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/20230511/daac0ed6/attachment-0001.html>
More information about the ghc-commits
mailing list