[Git][ghc/ghc][wip/T23070-unify] Maybe working now
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Thu Apr 6 23:13:45 UTC 2023
Simon Peyton Jones pushed to branch wip/T23070-unify at Glasgow Haskell Compiler / GHC
Commits:
3017ff40 by Simon Peyton Jones at 2023-04-07T00:13:38+01:00
Maybe working now
- - - - -
8 changed files:
- compiler/GHC/Core/TyCo/Subst.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Interact.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Core/TyCo/Subst.hs
=====================================
@@ -387,9 +387,9 @@ extendTvSubstWithClone :: Subst -> TyVar -> TyVar -> Subst
-- those variables should be in scope already
extendTvSubstWithClone (Subst in_scope idenv tenv cenv) tv tv'
= Subst (extendInScopeSet in_scope tv')
- idenv
- (extendVarEnv tenv tv (mkTyVarTy tv'))
- cenv
+ idenv
+ (extendVarEnv tenv tv (mkTyVarTy tv'))
+ cenv
-- | Add a substitution from a 'CoVar' to a 'Coercion' to the 'Subst':
-- you must ensure that the in-scope set satisfies
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -5,7 +5,6 @@
module GHC.Tc.Solver.Canonical(
canonicalize,
- unifyWanted,
makeSuperClasses,
StopOrContinue(..), stopWith, continueWith, andWhenContinue,
solveCallStack -- For GHC.Tc.Solver
@@ -211,15 +210,13 @@ 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@(Reduction _ xi) = mkClassPredRedn cls redns
- mk_ct new_ev = CDictCan { cc_ev = new_ev
- , cc_tyargs = xis
- , cc_class = cls
- , cc_pend_sc = pend_sc }
- ; mb <- rewriteEvidence rewriters ev redn
- ; traceTcS "canClass" (vcat [ ppr ev
- , ppr xi, ppr mb ])
- ; return (fmap mk_ct mb) }
+ ; 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
@@ -738,7 +735,7 @@ canIrred ev
= do { let pred = ctEvPred ev
; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
; (redn, rewriters) <- rewrite ev pred
- ; rewriteEvidence rewriters ev redn `andWhenContinue` \ new_ev ->
+ ; rewriteEvidence rewriters ev redn $ \ new_ev ->
do { -- Re-classify, in case rewriting has improved its shape
-- Code is like the canNC, except
@@ -863,9 +860,8 @@ 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
- let pred = ctEvPred ev
- ; (redn, rewriters) <- rewrite ev pred
- ; rewriteEvidence rewriters ev redn `andWhenContinue` \ new_ev ->
+ ; (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.)
@@ -979,32 +975,29 @@ 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
- -> TcS (StopOrContinue CtEvidence)
--- Returns Just new_ev iff either (i) 'co' is reflexivity
--- or (ii) 'co' is not reflexivity, and 'new_pred' not cached
--- In either case, there is nothing new to do with new_ev
-{-
- rewriteEvidence old_ev new_pred co
-Main purpose: create new evidence for new_pred;
- unless new_pred is cached already
-* Returns a new_ev : new_pred, with same wanted/given flag as old_ev
-* If old_ev was wanted, create a binding for old_ev, in terms of new_ev
-* If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
-* Returns Nothing if new_ev is already cached
-
- Old evidence New predicate is Return new evidence
- flavour of same flavor
- -------------------------------------------------------------------
- Wanted Already solved or in inert Nothing
- Not Just new_evidence
-
- Given Already in inert Nothing
- Not Just new_evidence
-
-Note [Rewriting with Refl]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
+ -> (CtEvidence -> TcS (StopOrContinue Ct))
+ -> TcS (StopOrContinue Ct)
+-- (rewriteEvidence old_ev new_pred co do_next)
+-- Main purpose: create new evidence for new_pred;
+-- unless new_pred is cached already
+-- * Calls do_next with (new_ev :: new_pred), with same wanted/given flag as old_ev
+-- * If old_ev was wanted, create a binding for old_ev, in terms of new_ev
+-- * If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
+-- * Stops if new_ev is already cached
+--
+-- Old evidence New predicate is Return new evidence
+-- flavour of same flavor
+-- -------------------------------------------------------------------
+-- Wanted Already solved or in inert Stop
+-- Not do_next new_evidence
+--
+-- Given Already in inert Stop
+-- Not do_next new_evidence
+
+{- Note [Rewriting with Refl]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If the coercion is just reflexivity then you may re-use the same
-variable. But be careful! Although the coercion is Refl, new_pred
+evidence variable. But be careful! Although the coercion is Refl, new_pred
may reflect the result of unification alpha := ty, so new_pred might
not _look_ the same as old_pred, and it's vital to proceed from now on
using new_pred.
@@ -1017,16 +1010,16 @@ the rewriter set. We check this with an assertion.
-}
-rewriteEvidence rewriters old_ev (Reduction co new_pred)
+rewriteEvidence rewriters old_ev (Reduction co new_pred) do_next
| isReflCo co -- See Note [Rewriting with Refl]
= assert (isEmptyRewriterSet rewriters) $
- continueWith (setCtEvPredType old_ev new_pred)
+ do_next (setCtEvPredType old_ev new_pred)
rewriteEvidence rewriters ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc })
- (Reduction co new_pred)
+ (Reduction co new_pred) do_next
= assert (isEmptyRewriterSet rewriters) $ -- this is a Given, not a wanted
do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
- ; continueWith new_ev }
+ ; do_next new_ev }
where
-- mkEvCast optimises ReflCo
new_tm = mkEvCast (evId old_evar)
@@ -1036,14 +1029,14 @@ rewriteEvidence new_rewriters
ev@(CtWanted { ctev_dest = dest
, ctev_loc = loc
, ctev_rewriters = rewriters })
- (Reduction co new_pred)
+ (Reduction co new_pred) do_next
= 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 -> continueWith new_ev
+ Fresh new_ev -> do_next new_ev
Cached _ -> stopWith ev "Cached wanted" }
where
rewriters' = rewriters S.<> new_rewriters
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -71,8 +71,10 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
_ -> -- NoInstance or NotSure
-- We didn't solve it; so try functional dependencies with
-- the instance environment
- do { doTopFundepImprovement work_item
- ; tryLastResortProhibitedSuperclass inerts work_item } }
+ do { improved <- doTopFundepImprovement work_item
+ ; if improved
+ then startAgainWith work_item
+ else tryLastResortProhibitedSuperclass inerts work_item } }
where
dict_loc = ctEvLoc ev
@@ -831,7 +833,7 @@ as the fundeps.
#7875 is a case in point.
-}
-doTopFundepImprovement :: Ct -> TcS ()
+doTopFundepImprovement :: Ct -> TcS Bool
-- Try to functional-dependency improvement between the constraint
-- and the top-level instance declarations
-- See Note [Fundeps with instances, and equality orientation]
@@ -841,7 +843,7 @@ doTopFundepImprovement work_item@(CDictCan { cc_ev = ev, cc_class = cls
= do { traceTcS "try_fundeps" (ppr work_item)
; instEnvs <- getInstEnvs
; let fundep_eqns = improveFromInstEnv instEnvs mk_ct_loc cls xis
- ; emitFunDepWanteds (ctEvRewriters ev) fundep_eqns }
+ ; emitFunDepWanteds ev fundep_eqns }
where
dict_pred = mkClassPred cls xis
dict_loc = ctEvLoc ev
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -651,11 +651,12 @@ can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2
-- to an irreducible constraint; see typecheck/should_compile/T10494
-- See Note [Decomposing AppTy equalities]
can_eq_app ev s1 t1 s2 t2
- | CtWanted { ctev_dest = dest, ctev_rewriters = rewriters } <- ev
- = do { co_s <- unifyWanted rewriters loc Nominal s1 s2
- ; let arg_loc = adjustCtLoc (isNextArgVisible s1) False loc
- ; co_t <- unifyWanted rewriters arg_loc Nominal t1 t2
- ; let co = mkAppCo co_s co_t
+ | CtWanted { ctev_dest = dest } <- ev
+ = do { (co,_) <- unifyWanteds ev Nominal $ \uenv ->
+ do { co_s <- uType uenv s1 s2
+ ; let arg_env = updUEnvLoc uenv (adjustCtLoc (isNextArgVisible s1) False)
+ ; co_t <- uType arg_env t1 t2
+ ; return (mkAppCo co_s co_t) }
; setWantedEq dest co
; stopWith ev "Decomposed [W] AppTy" }
@@ -802,7 +803,7 @@ then we will just decompose s1~s2, and it might be better to
do so on the spot. An important special case is where s1=s2,
and we get just Refl.
-So canDecomposableTyConAppOK uses unifyWanted etc to short-cut that work.
+So canDecomposableTyConAppOK uses unifyWanteds etc to short-cut that work.
See also Note [Decomposing Dependent TyCons and Processing Wanted Equalities]
Note [Decomposing TyConApp equalities]
@@ -1172,15 +1173,17 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
do { traceTcS "canDecomposableTyConAppOK"
(ppr ev $$ ppr eq_rel $$ ppr tc $$ ppr tys1 $$ ppr tys2)
; case ev of
- CtWanted { ctev_dest = dest, ctev_rewriters = rewriters }
+ CtWanted { ctev_dest = dest }
-- new_locs and tc_roles are both infinite, so
-- we are guaranteed that cos has the same lengthm
-- as tys1 and tys2
-- See Note [Fast path when decomposing TyConApps]
-- Caution: unifyWanteds is order sensitive
-- See Note [Decomposing Dependent TyCons and Processing Wanted Equalities]
- -> do { cos <- unifyWanteds rewriters new_locs tc_roles tys1 tys2
- ; setWantedEq dest (mkTyConAppCo role tc cos) }
+ -> do { (co, _) <- unifyWanteds ev role $ \uenv ->
+ do { cos <- zipWith4M (u_arg uenv) new_locs tc_roles tys1 tys2
+ ; return (mkTyConAppCo role tc cos) }
+ ; setWantedEq dest co }
CtGiven { ctev_evar = evar }
-> do { let ev_co = mkCoVarCo evar
@@ -1198,6 +1201,11 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
loc = ctEvLoc ev
role = eqRelRole eq_rel
+ u_arg uenv arg_loc arg_role = uType arg_env
+ where
+ arg_env = uenv `setUEnvRole` arg_role
+ `updUEnvLoc` const arg_loc
+
-- Infinite, to allow for over-saturated TyConApps
tc_roles = tyConRoleListX role tc
@@ -1223,11 +1231,15 @@ canDecomposableFunTy ev eq_rel af f1@(m1,a1,r1) f2@(m2,a2,r2)
= do { traceTcS "canDecomposableFunTy"
(ppr ev $$ ppr eq_rel $$ ppr f1 $$ ppr f2)
; case ev of
- CtWanted { ctev_dest = dest, ctev_rewriters = rewriters }
- -> do { mult <- unifyWanted rewriters mult_loc (funRole role SelMult) m1 m2
- ; arg <- unifyWanted rewriters loc (funRole role SelArg) a1 a2
- ; res <- unifyWanted rewriters loc (funRole role SelRes) r1 r2
- ; setWantedEq dest (mkNakedFunCo1 role af mult arg res) }
+ CtWanted { ctev_dest = dest }
+ -> do { (co, _) <- unifyWanteds ev Nominal $ \ uenv ->
+ do { let mult_env = uenv `updUEnvLoc` toInvisibleLoc
+ `setUEnvRole` funRole role SelMult
+ ; mult <- uType mult_env m1 m2
+ ; arg <- uType (uenv `setUEnvRole` funRole role SelArg) a1 a2
+ ; res <- uType (uenv `setUEnvRole` funRole role SelRes) r1 r2
+ ; return (mkNakedFunCo1 role af mult arg res) }
+ ; setWantedEq dest co }
CtGiven { ctev_evar = evar }
-> do { let ev_co = mkCoVarCo evar
@@ -1243,9 +1255,8 @@ canDecomposableFunTy ev eq_rel af f1@(m1,a1,r1) f2@(m2,a2,r2)
; stopWith ev "Decomposed TyConApp" }
where
- loc = ctEvLoc ev
- role = eqRelRole eq_rel
- mult_loc = updateCtLocOrigin loc toInvisibleOrigin
+ loc = ctEvLoc ev
+ role = eqRelRole eq_rel
-- | Call when canonicalizing an equality fails, but if the equality is
-- representational, there is some hope for the future.
@@ -1549,46 +1560,13 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
-- See Note [Decomposing type family applications]
= do { traceTcS "canEqCanLHS2 two type families" (ppr lhs1 $$ ppr lhs2)
- -- emit wanted equalities for injective type families
- ; let inj_eqns :: [TypeEqn] -- TypeEqn = Pair Type
- inj_eqns
- | ReprEq <- eq_rel = [] -- injectivity applies only for nom. eqs.
- | fun_tc1 /= fun_tc2 = [] -- if the families don't match, stop.
-
- | Injective inj <- tyConInjectivityInfo fun_tc1
- = [ Pair arg1 arg2
- | (arg1, arg2, True) <- zip3 fun_args1 fun_args2 inj ]
-
- -- built-in synonym families don't have an entry point
- -- for this use case. So, we just use sfInteractInert
- -- and pass two equal RHSs. We *could* add another entry
- -- point, but then there would be a burden to make
- -- sure the new entry point and existing ones were
- -- internally consistent. This is slightly distasteful,
- -- but it works well in practice and localises the
- -- problem.
- | Just ops <- isBuiltInSynFamTyCon_maybe fun_tc1
- = let ki1 = canEqLHSKind lhs1
- ki2 | MRefl <- mco
- = ki1 -- just a small optimisation
- | otherwise
- = canEqLHSKind lhs2
-
- fake_rhs1 = anyTypeOfKind ki1
- fake_rhs2 = anyTypeOfKind ki2
- in
- sfInteractInert ops fun_args1 fake_rhs1 fun_args2 fake_rhs2
-
- | otherwise -- ordinary, non-injective type family
- = []
-
- ; case ev of
- CtWanted { ctev_rewriters = rewriters } ->
- mapM_ (\ (Pair t1 t2) -> unifyWanted rewriters (ctEvLoc ev) Nominal t1 t2) inj_eqns
- CtGiven {} -> return ()
- -- See Note [No Given/Given fundeps] in GHC.Tc.Solver.Interact
-
- ; tclvl <- getTcLevel
+ ; unifications_done <- tryFamFamInjectivity ev eq_rel
+ fun_tc1 fun_args1 fun_tc2 fun_args2 mco
+ ; if unifications_done
+ then -- Go round again, since the unifications affect lhs/rhs
+ startAgainWith (mkNonCanonical ev)
+ else
+ do { tclvl <- getTcLevel
; let tvs1 = tyCoVarsOfTypes fun_args1
tvs2 = tyCoVarsOfTypes fun_args2
@@ -1603,7 +1581,7 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
; if swap_for_rewriting || swap_for_size
then finish_with_swapping
- else finish_without_swapping }
+ else finish_without_swapping } }
where
sym_mco = mkSymMCo mco
role = eqRelRole eq_rel
@@ -2138,7 +2116,7 @@ in `GHC.Tc.Solver.Monad.checkTouchableTyVarEq`.
Why TauTvs? See [Why TauTvs] below.
Critically, we emit the two new constraints (the last two above)
-directly instead of calling unifyWanted. (Otherwise, we'd end up
+directly instead of calling unifyWanteds. (Otherwise, we'd end up
unifying cbv1 and cbv2 immediately, achieving nothing.) Next, we
unify alpha := cbv1 -> cbv2, having eliminated the occurs check. This
unification happens immediately following a successful call to
@@ -2472,9 +2450,11 @@ interactEq work_item@(EqCt { eq_lhs = lhs, eq_ev = ev, eq_eq_rel = eq_rel })
| otherwise
-> case lhs of
TyVarLHS {} -> finishEqCt work_item
- TyFamLHS tc args -> do { improveLocalFunEqs inerts tc args work_item
- ; improveTopFunEqs tc args work_item
- ; finishEqCt work_item } }
+ TyFamLHS tc args -> do { imp1 <- improveLocalFunEqs inerts tc args work_item
+ ; imp2 <- improveTopFunEqs tc args work_item
+ ; if (imp1 || imp2)
+ then startAgainWith (mkNonCanonical ev)
+ else finishEqCt work_item } }
inertsCanDischarge :: InertCans -> EqCt
@@ -2695,7 +2675,7 @@ Of course, if we solve the first wanted first, the second becomes homogeneous.
When looking for injectivity-inspired equalities, we work left-to-right,
producing the two equalities in the order written above. However, these
-equalities are then passed into unifyWanted, which will fail, adding these
+equalities are then passed into unifyWanteds, which will fail, adding these
to the work list. However, crucially, the work list operates like a *stack*.
So, because we add w1 and then w2, we process w2 first. This is silly: solving
w1 would unlock w2. So we make sure to add equalities to the work
@@ -2753,28 +2733,72 @@ equality with the template on the left. Delicate, but it works.
-}
+tryFamFamInjectivity :: CtEvidence -> EqRel
+ -> TyCon -> [TcType] -> TyCon -> [TcType] -> MCoercion
+ -> TcS Bool -- True <=> some unification happened
+tryFamFamInjectivity ev eq_rel fun_tc1 fun_args1 fun_tc2 fun_args2 mco
+ | ReprEq <- eq_rel
+ = return False -- Injectivity applies only for Nominal equalities
+ | fun_tc1 /= fun_tc2
+ = return False -- If the families don't match, stop.
+ | isGiven ev
+ = return False -- See Note [No Given/Given fundeps] in GHC.Tc.Solver.Interact
+
+ -- So this is a [W] (F tys1 ~N# F tys2)
+
+ -- Is F an injective type family
+ | Injective inj <- tyConInjectivityInfo fun_tc1
+ = unifyFunDeps ev Nominal $ \uenv ->
+ uPairsTcM uenv [ Pair ty1 ty2
+ | (ty1,ty2,True) <- zip3 fun_args1 fun_args2 inj ]
+
+ -- Built-in synonym families don't have an entry point for this
+ -- use case. So, we just use sfInteractInert and pass two equal
+ -- RHSs. We *could* add another entry point, but then there would
+ -- be a burden to make sure the new entry point and existing ones
+ -- were internally consistent. This is slightly distasteful, but
+ -- it works well in practice and localises the problem. Ugh.
+ | Just ops <- isBuiltInSynFamTyCon_maybe fun_tc1
+ = let tc_kind = tyConKind fun_tc1
+ ki1 = piResultTys tc_kind fun_args1
+ ki2 | MRefl <- mco
+ = ki1 -- just a small optimisation
+ | otherwise
+ = piResultTys tc_kind fun_args2
+
+ fake_rhs1 = anyTypeOfKind ki1
+ fake_rhs2 = anyTypeOfKind ki2
+
+ eqs :: [TypeEqn]
+ eqs = sfInteractInert ops fun_args1 fake_rhs1 fun_args2 fake_rhs2
+ in
+ unifyFunDeps ev Nominal $ \uenv ->
+ uPairsTcM uenv eqs
+
+ | otherwise -- ordinary, non-injective type family
+ = return False
+
--------------------
-improveTopFunEqs :: TyCon -> [TcType] -> EqCt -> TcS ()
+improveTopFunEqs :: TyCon -> [TcType] -> EqCt -> TcS Bool
-- See Note [FunDep and implicit parameter reactions]
improveTopFunEqs fam_tc args (EqCt { eq_ev = ev, eq_rhs = rhs })
-
- | isGiven ev = return () -- See Note [No Given/Given fundeps]
+ | isGiven ev
+ = return False -- See Note [No Given/Given fundeps]
| otherwise
= do { fam_envs <- getFamInstEnvs
; eqns <- improve_top_fun_eqs fam_envs fam_tc args rhs
; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr rhs
- , ppr eqns ])
- ; mapM_ (\(Pair ty1 ty2) -> unifyWanted rewriters loc Nominal ty1 ty2)
- (reverse eqns) }
+ , ppr eqns ])
+ ; unifyFunDeps ev Nominal $ \uenv ->
+ uPairsTcM (bump_depth uenv) (reverse eqns) }
-- Missing that `reverse` causes T13135 and T13135_simple to loop.
-- See Note [Reverse order of fundep equations]
where
- loc = bumpCtLocDepth (ctEvLoc ev)
+ bump_depth env = env { u_loc = bumpCtLocDepth (u_loc env) }
-- ToDo: this location is wrong; it should be FunDepOrigin2
-- See #14778
- rewriters = ctEvRewriters ev
improve_top_fun_eqs :: FamInstEnvs
-> TyCon -> [TcType] -> TcType
@@ -2852,19 +2876,21 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty
, (ax_arg, arg, True) <- zip3 ax_args args inj_args ] }
-improveLocalFunEqs :: InertCans -> TyCon -> [TcType] -> EqCt -> TcS ()
+improveLocalFunEqs :: InertCans -> TyCon -> [TcType] -> EqCt -> TcS Bool
-- Generate improvement equalities, by comparing
-- the current work item with inert CFunEqs
-- E.g. x + y ~ z, x + y' ~ z => [W] y ~ y'
--
-- See Note [FunDep and implicit parameter reactions]
improveLocalFunEqs inerts fam_tc args (EqCt { eq_ev = work_ev, eq_rhs = rhs })
- = unless (null improvement_eqns) $
- do { traceTcS "interactFunEq improvements: " $
+ | null improvement_eqns
+ = return False
+ | otherwise
+ = do { traceTcS "interactFunEq improvements: " $
vcat [ text "Eqns:" <+> ppr improvement_eqns
, text "Candidates:" <+> ppr funeqs_for_tc
, text "Inert eqs:" <+> ppr (inert_eqs inerts) ]
- ; emitFunDepWanteds (ctEvRewriters work_ev) improvement_eqns }
+ ; emitFunDepWanteds work_ev improvement_eqns }
where
funeqs = inert_funeqs inerts
funeqs_for_tc :: [EqCt]
=====================================
compiler/GHC/Tc/Solver/Interact.hs
=====================================
@@ -308,7 +308,7 @@ runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
-> WorkItem -- The work item
-> TcS ()
-- Run this item down the pipeline, leaving behind new work and inerts
-runSolverPipeline pipeline workItem
+runSolverPipeline full_pipeline workItem
= do { wl <- getWorkList
; inerts <- getTcSInerts
; tclevel <- getTcLevel
@@ -320,7 +320,7 @@ runSolverPipeline pipeline workItem
, text "rest of worklist =" <+> ppr wl ]
; bumpStepCountTcS -- One step for each constraint processed
- ; final_res <- run_pipeline pipeline (ContinueWith workItem)
+ ; final_res <- run_pipeline full_pipeline workItem
; case final_res of
Stop ev s -> do { traceFireTcS ev s
@@ -330,26 +330,29 @@ runSolverPipeline pipeline workItem
; traceFireTcS (ctEvidence ct) (text "Kept as inert")
; traceTcS "End solver pipeline (kept as inert) }" $
(text "final_item =" <+> ppr ct) }
+ StartAgain ct -> pprPanic "runSolverPipeline: StartAgain" (ppr ct)
}
- where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct
- -> TcS (StopOrContinue Ct)
- run_pipeline [] res = return res
- run_pipeline _ (Stop ev s) = return (Stop ev s)
- run_pipeline ((stg_name,stg):stgs) (ContinueWith ct)
- = do { traceTcS ("runStage " ++ stg_name ++ " {")
- (text "workitem = " <+> ppr ct)
- ; res <- stg ct
- ; traceTcS ("end stage " ++ stg_name ++ " }") empty
- ; run_pipeline stgs res }
+ where
+ run_pipeline :: [(String,SimplifierStage)] -> Ct -> TcS (StopOrContinue Ct)
+ run_pipeline [] ct = return (ContinueWith ct)
+ run_pipeline ((stage_name,stage):stages) ct
+ = do { traceTcS ("runStage " ++ stage_name ++ " {")
+ (text "workitem = " <+> ppr ct)
+ ; res <- stage ct
+ ; traceTcS ("end stage " ++ stage_name ++ " }") (ppr res)
+ ; case res of
+ Stop {} -> return res
+ StartAgain ct -> run_pipeline full_pipeline ct
+ ContinueWith ct -> run_pipeline stages ct }
{-
Example 1:
Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
Reagent: a ~ [b] (given)
-React with (c~d) ==> IR (ContinueWith (a~[b])) True []
-React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
-React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
+React with (c~d) ==> IR (ContinueWith (a~[b])) True []
+React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
+React with (b ~ Int) ==> IR (ContinueWith (a~[Int])) True []
Example 2:
Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
@@ -1025,8 +1028,10 @@ interactDict inerts ct_w@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = t
= interactGivenIP inerts ct_w
| otherwise
- = do { addFunDepWork inerts ev_w cls
- ; continueWith ct_w }
+ = do { unif_happened <- addFunDepWork inerts ev_w cls
+ ; if unif_happened
+ then startAgainWith ct_w
+ else continueWith ct_w }
interactDict _ wi = pprPanic "interactDict" (ppr wi)
@@ -1131,30 +1136,36 @@ shortCutSolver dflags ev_w ev_i
Nothing -> Fresh <$> newWantedNC loc (ctEvRewriters ev_w) pty
| otherwise = mzero
-addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS ()
+addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS Bool
-- Add wanted constraints from type-class functional dependencies.
addFunDepWork inerts work_ev cls
- = mapBagM_ add_fds (findDictsByClass (inert_dicts inerts) cls)
- -- No need to check flavour; fundeps work between
- -- any pair of constraints, regardless of flavour
- -- Importantly we don't throw workitem back in the
- -- worklist because this can cause loops (see #5236)
+ = foldlM add_fds False (findDictsByClass (inert_dicts inerts) cls)
+ -- No need to check flavour; fundeps work between
+ -- any pair of constraints, regardless of flavour
+ -- Importantly we don't throw workitem back in the
+ -- worklist because this can cause loops (see #5236)
where
work_pred = ctEvPred work_ev
work_loc = ctEvLoc work_ev
- add_fds inert_ct
+ add_fds :: Bool -> Ct -> TcS Bool
+ add_fds so_far inert_ct
+ | isGiven work_ev && isGiven inert_ev
+ -- Do not create FDs from Given/Given interactions: See Note [No Given/Given fundeps]
+ = return so_far
+ | otherwise
= do { traceTcS "addFunDepWork" (vcat
[ ppr work_ev
, pprCtLoc work_loc, ppr (isGivenLoc work_loc)
, pprCtLoc inert_loc, ppr (isGivenLoc inert_loc)
, pprCtLoc derived_loc, ppr (isGivenLoc derived_loc) ])
- ; unless (isGiven work_ev && isGiven inert_ev) $
- emitFunDepWanteds (ctEvRewriters work_ev) $
- improveFromAnother (derived_loc, inert_rewriters) inert_pred work_pred
- -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
- -- Do not create FDs from Given/Given interactions: See Note [No Given/Given fundeps]
+ ; unifs <- emitFunDepWanteds work_ev $
+ improveFromAnother (derived_loc, inert_rewriters)
+ inert_pred work_pred
+ -- We don't really rewrite tys2, see below
+ -- _rewritten_tys2, so that's ok
+ ; return (so_far || unifs)
}
where
inert_ev = ctEvidence inert_ct
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -33,6 +33,7 @@ module GHC.Tc.Solver.Monad (
-- The pipeline
StopOrContinue(..), continueWith, stopWith, andWhenContinue,
+ startAgainWith,
-- Tracing etc
panicTcS, traceTcS,
@@ -94,7 +95,7 @@ module GHC.Tc.Solver.Monad (
instDFunType,
-- Unification
- unifyWanted, unifyWanteds,
+ unifyWanteds, unifyFunDeps, uPairsTcM,
-- MetaTyVars
newFlexiTcSTy, instFlexiX,
@@ -154,6 +155,7 @@ import GHC.Tc.Utils.Unify
import GHC.Core.Type
import GHC.Core.TyCo.Rep as Rep
import GHC.Core.Coercion
+import GHC.Core.Coercion.Axiom( TypeEqn )
import GHC.Core.Predicate
import GHC.Core.Reduction
import GHC.Core.Class
@@ -183,7 +185,7 @@ import GHC.Utils.Monad
import GHC.Exts (oneShot)
import Control.Monad
import Data.IORef
-import Data.List ( mapAccumL, zip4 )
+import Data.List ( mapAccumL )
import Data.Foldable
import qualified Data.Semigroup as S
@@ -199,7 +201,10 @@ import GHC.Data.Graph.Directed
********************************************************************* -}
data StopOrContinue a
- = ContinueWith a -- The constraint was not solved, although it may have
+ = StartAgain a -- Constraint is not solved, but some unifications
+ -- happened, so go back to the beginning of the pipeline
+
+ | ContinueWith a -- The constraint was not solved, although it may have
-- been rewritten
| Stop CtEvidence -- The (rewritten) constraint was solved
@@ -210,21 +215,25 @@ data StopOrContinue a
instance Outputable a => Outputable (StopOrContinue a) where
ppr (Stop ev s) = text "Stop" <> parens s <+> ppr ev
ppr (ContinueWith w) = text "ContinueWith" <+> ppr w
+ ppr (StartAgain w) = text "StartAgain" <+> ppr w
+
+startAgainWith :: a -> TcS (StopOrContinue a)
+startAgainWith ct = return (StartAgain ct)
continueWith :: a -> TcS (StopOrContinue a)
-continueWith = return . ContinueWith
+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 b))
- -> TcS (StopOrContinue b)
+ -> (a -> TcS (StopOrContinue a))
+ -> TcS (StopOrContinue a)
andWhenContinue tcs1 tcs2
= do { r <- tcs1
; case r of
- Stop ev s -> return (Stop ev s)
- ContinueWith ct -> tcs2 ct }
+ ContinueWith ct -> tcs2 ct
+ _ -> return r }
infixr 0 `andWhenContinue` -- allow chaining with ($)
@@ -1610,20 +1619,22 @@ cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)
instFlexiX :: Subst -> [TKVar] -> TcS Subst
-instFlexiX subst tvs
- = wrapTcS (foldlM instFlexiHelper subst tvs)
+instFlexiX subst tvs = wrapTcS (instFlexiXTcM subst tvs)
-instFlexiHelper :: Subst -> TKVar -> TcM Subst
+instFlexiXTcM :: Subst -> [TKVar] -> TcM Subst
-- Makes fresh tyvar, extends the substitution, and the in-scope set
-instFlexiHelper subst tv
+-- Takes account of the case [k::Type, a::k, ...],
+-- where we must substitute for k in a's kind
+instFlexiXTcM subst []
+ = return subst
+instFlexiXTcM subst (tv:tvs)
= do { uniq <- TcM.newUnique
; details <- TcM.newMetaDetails TauTv
; let name = setNameUnique (tyVarName tv) uniq
kind = substTyUnchecked subst (tyVarKind tv)
tv' = mkTcTyVar name kind details
subst' = extendTvSubstWithClone subst tv tv'
- ; TcM.traceTc "instFlexi" (ppr tv')
- ; return (extendTvSubst subst' tv (mkTyVarTy tv')) }
+ ; instFlexiXTcM subst' tvs }
matchGlobalInst :: DynFlags
-> Bool -- True <=> caller is the short-cut solver
@@ -1889,43 +1900,47 @@ solverDepthError loc ty
************************************************************************
-}
-emitFunDepWanteds :: RewriterSet -- from the work item
- -> [FunDepEqn (CtLoc, RewriterSet)] -> TcS ()
+emitFunDepWanteds :: CtEvidence -- The work item
+ -> [FunDepEqn (CtLoc, RewriterSet)]
+ -> TcS Bool -- True <=> some unification happened
-emitFunDepWanteds _ [] = return () -- common case noop
+emitFunDepWanteds _ [] = return False -- common case noop
-- See Note [FunDep and implicit parameter reactions]
-emitFunDepWanteds work_rewriters fd_eqns
- = mapM_ do_one_FDEqn fd_eqns
+emitFunDepWanteds ev fd_eqns
+ = unifyFunDeps ev Nominal do_fundeps
where
- do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = (loc, rewriters) })
- | null tvs -- Common shortcut
- = do { traceTcS "emitFunDepWanteds 1" (ppr (ctl_depth loc) $$ ppr eqs $$ ppr (isGivenLoc loc))
- ; mapM_ (\(Pair ty1 ty2) -> unifyWanted all_rewriters loc Nominal ty1 ty2)
- (reverse eqs) }
- -- See Note [Reverse order of fundep equations]
-
- | otherwise
- = do { traceTcS "emitFunDepWanteds 2" (ppr (ctl_depth loc) $$ ppr tvs $$ ppr eqs)
- ; subst <- instFlexiX emptySubst tvs -- Takes account of kind substitution
- ; mapM_ (do_one_eq loc all_rewriters subst) (reverse eqs) }
- -- See Note [Reverse order of fundep equations]
- where
- all_rewriters = work_rewriters S.<> rewriters
-
- do_one_eq loc rewriters subst (Pair ty1 ty2)
- = unifyWanted rewriters loc Nominal (substTyUnchecked subst' ty1) ty2
- -- ty2 does not mention fd_qtvs, so no need to subst it.
- -- See GHC.Tc.Instance.Fundeps Note [Improving against instances]
- -- Wrinkle (1)
+ do_fundeps :: UnifyEnv -> TcM ()
+ do_fundeps env = mapM_ (do_one env) fd_eqns
+
+ do_one :: UnifyEnv -> FunDepEqn (CtLoc, RewriterSet) -> TcM ()
+ do_one uenv (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = (loc, rewriters) })
+ = do { eqs' <- instantiate_eqs tvs (reverse eqs)
+ -- (reverse eqs): See Note [Reverse order of fundep equations]
+ ; uPairsTcM env_one eqs' }
where
- subst' = extendSubstInScopeSet subst (tyCoVarsOfType ty1)
- -- The free vars of ty1 aren't just fd_qtvs: ty1 is the result
- -- of matching with the [W] constraint. So we add its free
- -- vars to InScopeSet, to satisfy substTy's invariants, even
- -- though ty1 will never (currently) be a poytype, so this
- -- InScopeSet will never be looked at.
+ env_one = uenv { u_rewriters = u_rewriters uenv S.<> rewriters
+ , u_loc = loc }
+ instantiate_eqs :: [TyVar] -> [TypeEqn] -> TcM [TypeEqn]
+ instantiate_eqs tvs eqs
+ | null tvs
+ = return eqs
+ | otherwise
+ = do { TcM.traceTc "emitFunDepWanteds 2" (ppr tvs $$ ppr eqs)
+ ; subst <- instFlexiXTcM emptySubst tvs -- Takes account of kind substitution
+ ; return [ Pair (substTyUnchecked subst' ty1) ty2
+ -- ty2 does not mention fd_qtvs, so no need to subst it.
+ -- See GHC.Tc.Instance.Fundeps Note [Improving against instances]
+ -- Wrinkle (1)
+ | Pair ty1 ty2 <- eqs
+ , let subst' = extendSubstInScopeSet subst (tyCoVarsOfType ty1) ]
+ -- The free vars of ty1 aren't just fd_qtvs: ty1 is the result
+ -- of matching with the [W] constraint. So we add its free
+ -- vars to InScopeSet, to satisfy substTy's invariants, even
+ -- though ty1 will never (currently) be a poytype, so this
+ -- InScopeSet will never be looked at.
+ }
{-
************************************************************************
@@ -1934,38 +1949,55 @@ emitFunDepWanteds work_rewriters fd_eqns
* *
************************************************************************
-Note [unifyWanted]
-~~~~~~~~~~~~~~~~~~
+Note [unifyWanteds]
+~~~~~~~~~~~~~~~~~~~
When decomposing equalities we often create new wanted constraints for
(s ~ t). But what if s=t? Then it'd be faster to return Refl right away.
-Rather than making an equality test (which traverses the structure of the
-type, perhaps fruitlessly), unifyWanted traverses the common structure, and
-bales out when it finds a difference by creating a new Wanted constraint.
-But where it succeeds in finding common structure, it just builds a coercion
-to reflect it.
--}
+Rather than making an equality test (which traverses the structure of
+the type, perhaps fruitlessly), unifyWanteds calls uType to traverse
+the common structure, and bales out when it finds a difference by
+creating a new Wanted constraint. But where it succeeds in finding
+common structure, it just builds a coercion to reflect it. -}
+
-unifyWanted :: RewriterSet -> CtLoc
- -> Role -> TcType -> TcType -> TcS Coercion
--- Return coercion witnessing the equality of the two types,
+uPairsTcM :: UnifyEnv -> [TypeEqn] -> TcM ()
+uPairsTcM uenv eqns = mapM_ (\(Pair ty1 ty2) -> uType uenv ty1 ty2) eqns
+
+unifyFunDeps :: CtEvidence -> Role
+ -> (UnifyEnv -> TcM ())
+ -> TcS Bool
+unifyFunDeps ev role do_unifications
+ = do { (_, unified) <- unifyWanteds ev role do_unifications
+ ; return (not (null unified)) }
+
+unifyWanteds :: CtEvidence -> Role
+ -> (UnifyEnv -> TcM a)
+ -> TcS (a, [TcTyVar])
+-- Return coercions witnessing the equality of the two types,
-- emitting new work equalities where necessary to achieve that
-- Very good short-cut when the two types are equal, or nearly so
-- See Note [unifyWanted]
-- The returned coercion's role matches the input parameter
+--
+-- The [TcTyVar] is the list of unification variables
+-- that were unified the process.
-unifyWanted _rewriters loc role ty1 ty2
- = do { (co, unified, cts) <- wrapTcS $
+unifyWanteds ev role do_unifications
+ = do { (cos, unified, cts) <- wrapTcS $
do { defer_ref <- TcM.newTcRef []
; unified_ref <- TcM.newTcRef []
- ; let env = UE { u_role = role
- , u_loc = loc
- , u_defer = defer_ref
- , u_unified = Just unified_ref}
- ; co <- uType env ty1 ty2
- ; cts <- TcM.readTcRef defer_ref
+ ; let env = UE { u_role = role
+ , u_rewriters = ctEvRewriters ev
+ , u_loc = ctEvLoc ev
+ , u_defer = defer_ref
+ , u_unified = Just unified_ref}
+
+ ; cos <- do_unifications env
+
+ ; cts <- TcM.readTcRef defer_ref
; unified <- TcM.readTcRef unified_ref
- ; return (co, unified, cts) }
+ ; return (cos, unified, cts) }
-- Emit the deferred constraints
; updWorkListTcS (extendWorkListEqs cts)
@@ -1975,58 +2007,10 @@ unifyWanted _rewriters loc role ty1 ty2
-- be more efficient than one by one
; mapM_ kickOutAfterUnification unified
- ; return co }
+ ; return (cos, unified) }
-{-
-unifyWanted rewriters loc Phantom ty1 ty2
- = do { kind_co <- unifyWanted rewriters loc Nominal (typeKind ty1) (typeKind ty2)
- ; return (mkPhantomCo kind_co ty1 ty2) }
-
-unifyWanted rewriters loc role orig_ty1 orig_ty2
- = go orig_ty1 orig_ty2
- where
- go ty1 ty2 | Just ty1' <- coreView ty1 = go ty1' ty2
- go ty1 ty2 | Just ty2' <- coreView ty2 = go ty1 ty2'
-
- go (FunTy af1 w1 s1 t1) (FunTy af2 w2 s2 t2)
- | af1 == af2 -- Important! See #21530
- = do { co_s <- unifyWanted rewriters loc role s1 s2
- ; co_t <- unifyWanted rewriters loc role t1 t2
- ; co_w <- unifyWanted rewriters loc Nominal w1 w2
- ; return (mkNakedFunCo1 role af1 co_w co_s co_t) }
-
- go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
- | tc1 == tc2, tys1 `equalLength` tys2
- , isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality
- = do { cos <- zipWith3M (unifyWanted rewriters loc)
- (tyConRoleListX role tc1) tys1 tys2
- ; return (mkTyConAppCo role tc1 cos) }
-
- go ty1@(TyVarTy tv) ty2
- = do { mb_ty <- isFilledMetaTyVar_maybe tv
- ; case mb_ty of
- Just ty1' -> go ty1' ty2
- Nothing -> bale_out ty1 ty2}
- go ty1 ty2@(TyVarTy tv)
- = do { mb_ty <- isFilledMetaTyVar_maybe tv
- ; case mb_ty of
- Just ty2' -> go ty1 ty2'
- Nothing -> bale_out ty1 ty2 }
-
- go ty1@(CoercionTy {}) (CoercionTy {})
- = return (mkReflCo role ty1) -- we just don't care about coercions!
-
- go ty1 ty2 = bale_out ty1 ty2
-
- bale_out ty1 ty2
- | ty1 `tcEqType` ty2 = return (mkReflCo role ty1)
- -- Check for equality; e.g. a ~ a, or (m a) ~ (m a)
- | otherwise = emitNewWantedEq loc rewriters role orig_ty1 orig_ty2
--}
-
-{-
-Note [Decomposing Dependent TyCons and Processing Wanted Equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Decomposing Dependent TyCons and Processing Wanted Equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we decompose a dependent tycon we obtain a list of
mixed wanted type and kind equalities. Ideally we want
all the kind equalities to get solved first so that we avoid
@@ -2059,21 +2043,6 @@ This is exactly what we do in `unifyWanteds`.
NB: This ordering is not needed when we decompose FunTyCons as they are not dependently typed
-}
--- NB: Length of [CtLoc] and [Roles] may be infinite
--- but list of RHS [TcType] and LHS [TcType] is finite and both are of equal length
-unifyWanteds :: RewriterSet -> [CtLoc] -> [Role]
- -> [TcType] -- List of RHS types
- -> [TcType] -- List of LHS types
- -> TcS [Coercion]
-unifyWanteds rewriters ctlocs roles rhss lhss = unify_wanteds rewriters $ zip4 ctlocs roles rhss lhss
- where
- -- Order is important here
- -- See Note [Decomposing Dependent TyCons and Processing Wanted Equalities]
- unify_wanteds _ [] = return []
- unify_wanteds rewriters ((new_loc, tc_role, ty1, ty2) : rest)
- = do { cos <- unify_wanteds rewriters rest
- ; co <- unifyWanted rewriters new_loc tc_role ty1 ty2
- ; return (co:cos) }
{-
************************************************************************
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -71,7 +71,7 @@ module GHC.Tc.Types.Constraint (
-- CtEvidence
CtEvidence(..), TcEvDest(..),
- mkKindLoc, toKindLoc, mkGivenLoc,
+ mkKindLoc, toKindLoc, toInvisibleLoc, mkGivenLoc,
isWanted, isGiven,
ctEvRole, setCtEvPredType, setCtEvLoc, arisesFromGivens,
tyCoVarsOfCtEvList, tyCoVarsOfCtEv, tyCoVarsOfCtEvsList,
@@ -2429,13 +2429,16 @@ adjustCtLoc is_invis is_kind loc
where
loc1 | is_kind = toKindLoc loc
| otherwise = loc
- loc2 | is_invis = updateCtLocOrigin loc1 toInvisibleOrigin
+ loc2 | is_invis = toInvisibleLoc loc1
| otherwise = loc1
-- | Take a CtLoc and moves it to the kind level
toKindLoc :: CtLoc -> CtLoc
toKindLoc loc = loc { ctl_t_or_k = Just KindLevel }
+toInvisibleLoc :: CtLoc -> CtLoc
+toInvisibleLoc loc = updateCtLocOrigin loc toInvisibleOrigin
+
mkGivenLoc :: TcLevel -> SkolemInfoAnon -> TcLclEnv -> CtLoc
mkGivenLoc tclvl skol_info env
= CtLoc { ctl_origin = GivenOrigin skol_info
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -23,7 +23,8 @@ module GHC.Tc.Utils.Unify (
unifyType, unifyKind, unifyExpectedType,
uTypeAndEmit, promoteTcType,
swapOverTyVars, touchabilityAndShapeTest,
- UnifyEnv(..), uType,
+ UnifyEnv(..), updUEnvLoc, setUEnvRole,
+ uType,
--------------------------------
-- Holes
@@ -1746,6 +1747,7 @@ uTypeAndEmit t_or_k orig ty1 ty2
= do { ref <- newTcRef []
; loc <- getCtLocM orig (Just t_or_k)
; let env = UE { u_loc = loc, u_role = Nominal
+ , u_rewriters = emptyRewriterSet -- ToDo: check this
, u_defer = ref, u_unified = Nothing }
-- The hard work happens here
@@ -1766,16 +1768,24 @@ uType is the heart of the unifier.
-}
data UnifyEnv
- = UE { u_role :: Role
- , u_loc :: CtLoc
+ = UE { u_role :: Role
+ , u_loc :: CtLoc
+ , u_rewriters :: RewriterSet
- , u_defer :: TcRef [Ct]
-- Deferred constraints
+ , u_defer :: TcRef [Ct]
+ -- Which variables are unified;
+ -- if Nothing, we don't care
, u_unified :: Maybe (TcRef [TcTyVar])
- -- If Just, track unified type variables
}
+setUEnvRole :: UnifyEnv -> Role -> UnifyEnv
+setUEnvRole uenv role = uenv { u_role = role }
+
+updUEnvLoc :: UnifyEnv -> (CtLoc -> CtLoc) -> UnifyEnv
+updUEnvLoc uenv@(UE { u_loc = loc }) upd = uenv { u_loc = upd loc }
+
mkKindEnv :: UnifyEnv -> TcType -> TcType -> UnifyEnv
-- Modify the UnifyEnv to be right for unifing
-- the kinds of these two types
@@ -1794,15 +1804,16 @@ uType, uType_defer
-- It is always safe to defer unification to the main constraint solver
-- See Note [Deferred unification]
-uType_defer (UE { u_loc = loc, u_defer = ref, u_role = role })
+uType_defer (UE { u_loc = loc, u_defer = ref
+ , u_role = role, u_rewriters = rewriters })
ty1 ty2 -- ty1 is "actual", ty2 is "expected"
= do { let pred_ty = mkPrimEqPredRole role ty1 ty2
; hole <- newCoercionHole pred_ty
; let ct = mkNonCanonical $
- CtWanted { ctev_pred = pred_ty
- , ctev_dest = HoleDest hole
- , ctev_loc = loc
- , ctev_rewriters = rewriterSetFromTypes [ty1, ty2] }
+ CtWanted { ctev_pred = pred_ty
+ , ctev_dest = HoleDest hole
+ , ctev_loc = loc
+ , ctev_rewriters = rewriters }
co = HoleCo hole
; updTcRef ref (ct :)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3017ff4038d20190ae8887b4562a24df3895f8c1
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3017ff4038d20190ae8887b4562a24df3895f8c1
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/20230406/c41cb5c2/attachment-0001.html>
More information about the ghc-commits
mailing list