Commit 9308c736 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Fix a number of subtle solver bugs

As a result of some other unrelated changes I found that
IndTypesPerf was failing, and opened Trac #11408.  There's
a test in indexed-types/should-compile/T11408.

The bug was that a type like
 forall t. (MT (UL t) (UR t) ~ t) => UL t -> UR t -> Int
is in fact unambiguous, but it's a bit subtle to prove
that it is unambiguous.

In investigating, Dimitrios and I found several subtle
bugs in the constraint solver, fixed by this patch

* canRewrite was missing a Derived/Derived case.  This was
  lost by accident in Richard's big kind-equality patch.

* Interact.interactTyVarEq would discard [D] a ~ ty if there
  was a [W] a ~ ty in the inert set.  But that is wrong because
  the former can rewrite things that the latter cannot.
  Fix: a new function eqCanDischarge

* In TcSMonad.addInertEq, the process was outright wrong for
  a Given/Wanted in the (GWModel) case.  We were adding a new
  Derived without kicking out things that it could rewrite.
  Now the code is simpler (no special GWModel case), and works
  correctly.

* The special case in kickOutRewritable for [W] fsk ~ ty,
  turns out not to be needed.  (We emit a [D] fsk ~ ty which
  will do the job.

I improved comments and documentation, esp in TcSMonad.
parent 3a1babd6
...@@ -1453,9 +1453,9 @@ canEqTyVarTyVar ev eq_rel swapped tv1 tv2 kco2 ...@@ -1453,9 +1453,9 @@ canEqTyVarTyVar ev eq_rel swapped tv1 tv2 kco2
-- the floating step looks for meta tyvars on the left -- the floating step looks for meta tyvars on the left
| isMetaTyVar tv2 = True | isMetaTyVar tv2 = True
-- So neither is a meta tyvar -- So neither is a meta tyvar (including FlatMetaTv)
-- If only one is a flatten tyvar, put it on the left -- If only one is a flatten skolem, put it on the left
-- See Note [Eliminate flat-skols] -- See Note [Eliminate flat-skols]
| not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True
......
...@@ -242,7 +242,7 @@ BUT this works badly for Trac #10340: ...@@ -242,7 +242,7 @@ BUT this works badly for Trac #10340:
For 'foo' we instantiate 'get' at types mm ss For 'foo' we instantiate 'get' at types mm ss
[W] MonadState ss mm, [W] mm ss ~ State Any Any [W] MonadState ss mm, [W] mm ss ~ State Any Any
Flatten, and decompose Flatten, and decompose
[W] MnadState ss mm, [W] Any ~ fmv, [W] mm ~ State fmv, [W] fmv ~ ss [W] MonadState ss mm, [W] Any ~ fmv, [W] mm ~ State fmv, [W] fmv ~ ss
Unify mm := State fmv: Unify mm := State fmv:
[W] MonadState ss (State fmv), [W] Any ~ fmv, [W] fmv ~ ss [W] MonadState ss (State fmv), [W] Any ~ fmv, [W] fmv ~ ss
If we orient with (untouchable) fmv on the left we are now stuck: If we orient with (untouchable) fmv on the left we are now stuck:
...@@ -1147,7 +1147,7 @@ flatten_exact_fam_app_fully tc tys ...@@ -1147,7 +1147,7 @@ flatten_exact_fam_app_fully tc tys
; fr <- getFlavourRole ; fr <- getFlavourRole
; case mb_ct of ; case mb_ct of
Just (co, rhs_ty, flav) -- co :: F xis ~ fsk Just (co, rhs_ty, flav) -- co :: F xis ~ fsk
| (flav, NomEq) `canDischargeFR` fr | (flav, NomEq) `funEqCanDischargeFR` fr
-> -- Usable hit in the flat-cache -> -- Usable hit in the flat-cache
-- We certainly *can* use a Wanted for a Wanted -- We certainly *can* use a Wanted for a Wanted
do { traceFlat "flatten/flat-cache hit" $ (ppr tc <+> ppr xis $$ ppr rhs_ty) do { traceFlat "flatten/flat-cache hit" $ (ppr tc <+> ppr xis $$ ppr rhs_ty)
......
...@@ -506,7 +506,7 @@ solveOneFromTheOther :: CtEvidence -- Inert ...@@ -506,7 +506,7 @@ solveOneFromTheOther :: CtEvidence -- Inert
-> TcS (InteractResult, StopNowFlag) -> TcS (InteractResult, StopNowFlag)
-- Preconditions: -- Preconditions:
-- 1) inert and work item represent evidence for the /same/ predicate -- 1) inert and work item represent evidence for the /same/ predicate
-- 2) ip/class/irred evidence (no coercions) only -- 2) ip/class/irred constraints only; not used for equalities
solveOneFromTheOther ev_i ev_w solveOneFromTheOther ev_i ev_w
| isDerived ev_w -- Work item is Derived; just discard it | isDerived ev_w -- Work item is Derived; just discard it
= return (IRKeep, True) = return (IRKeep, True)
...@@ -843,7 +843,7 @@ interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc ...@@ -843,7 +843,7 @@ interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
, cc_tyargs = args, cc_fsk = fsk }) , cc_tyargs = args, cc_fsk = fsk })
| Just (CFunEqCan { cc_ev = ev_i | Just (CFunEqCan { cc_ev = ev_i
, cc_fsk = fsk_i }) <- matching_inerts , cc_fsk = fsk_i }) <- matching_inerts
= if ev_i `canDischarge` ev = if ev_i `funEqCanDischarge` ev
then -- Rewrite work-item using inert then -- Rewrite work-item using inert
do { traceTcS "reactFunEq (discharge work item):" $ do { traceTcS "reactFunEq (discharge work item):" $
vcat [ text "workItem =" <+> ppr workItem vcat [ text "workItem =" <+> ppr workItem
...@@ -851,7 +851,7 @@ interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc ...@@ -851,7 +851,7 @@ interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
; reactFunEq ev_i fsk_i ev fsk ; reactFunEq ev_i fsk_i ev fsk
; stopWith ev "Inert rewrites work item" } ; stopWith ev "Inert rewrites work item" }
else -- Rewrite inert using work-item else -- Rewrite inert using work-item
ASSERT2( ev `canDischarge` ev_i, ppr ev $$ ppr ev_i ) ASSERT2( ev `funEqCanDischarge` ev_i, ppr ev $$ ppr ev_i )
do { traceTcS "reactFunEq (rewrite inert item):" $ do { traceTcS "reactFunEq (rewrite inert item):" $
vcat [ text "workItem =" <+> ppr workItem vcat [ text "workItem =" <+> ppr workItem
, text "inertItem=" <+> ppr ev_i ] , text "inertItem=" <+> ppr ev_i ]
...@@ -881,15 +881,15 @@ improveLocalFunEqs loc inerts fam_tc args fsk ...@@ -881,15 +881,15 @@ improveLocalFunEqs loc inerts fam_tc args fsk
= do { traceTcS "interactFunEq improvements: " $ = do { traceTcS "interactFunEq improvements: " $
vcat [ ptext (sLit "Eqns:") <+> ppr improvement_eqns vcat [ ptext (sLit "Eqns:") <+> ppr improvement_eqns
, ptext (sLit "Candidates:") <+> ppr funeqs_for_tc , ptext (sLit "Candidates:") <+> ppr funeqs_for_tc
, ptext (sLit "TvEqs:") <+> ppr tv_eqs ] , ptext (sLit "Model:") <+> ppr model ]
; mapM_ (unifyDerived loc Nominal) improvement_eqns } ; mapM_ (unifyDerived loc Nominal) improvement_eqns }
| otherwise | otherwise
= return () = return ()
where where
tv_eqs = inert_model inerts model = inert_model inerts
funeqs = inert_funeqs inerts funeqs = inert_funeqs inerts
funeqs_for_tc = findFunEqsByTyCon funeqs fam_tc funeqs_for_tc = findFunEqsByTyCon funeqs fam_tc
rhs = lookupFlattenTyVar tv_eqs fsk rhs = lookupFlattenTyVar model fsk
-------------------- --------------------
improvement_eqns improvement_eqns
...@@ -906,14 +906,14 @@ improveLocalFunEqs loc inerts fam_tc args fsk ...@@ -906,14 +906,14 @@ improveLocalFunEqs loc inerts fam_tc args fsk
-------------------- --------------------
do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk }) do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
= sfInteractInert ops args rhs iargs (lookupFlattenTyVar tv_eqs ifsk) = sfInteractInert ops args rhs iargs (lookupFlattenTyVar model ifsk)
do_one_built_in _ _ = pprPanic "interactFunEq 1" (ppr fam_tc) do_one_built_in _ _ = pprPanic "interactFunEq 1" (ppr fam_tc)
-------------------- --------------------
-- See Note [Type inference for type families with injectivity] -- See Note [Type inference for type families with injectivity]
do_one_injective injective_args do_one_injective injective_args
(CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk }) (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
| rhs `tcEqType` lookupFlattenTyVar tv_eqs ifsk | rhs `tcEqType` lookupFlattenTyVar model ifsk
= [Pair arg iarg | (arg, iarg, True) = [Pair arg iarg | (arg, iarg, True)
<- zip3 args iargs injective_args ] <- zip3 args iargs injective_args ]
| otherwise | otherwise
...@@ -922,8 +922,7 @@ improveLocalFunEqs loc inerts fam_tc args fsk ...@@ -922,8 +922,7 @@ improveLocalFunEqs loc inerts fam_tc args fsk
------------- -------------
lookupFlattenTyVar :: InertModel -> TcTyVar -> TcType lookupFlattenTyVar :: InertModel -> TcTyVar -> TcType
-- ^ Look up a flatten-tyvar in the inert nominal TyVarEqs; -- See Note [lookupFlattenTyVar]
-- this is used only when dealing with a CFunEqCan
lookupFlattenTyVar model ftv lookupFlattenTyVar model ftv
= case lookupVarEnv model ftv of = case lookupVarEnv model ftv of
Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq }) -> rhs Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq }) -> rhs
...@@ -950,7 +949,18 @@ reactFunEq from_this fsk1 solve_this fsk2 ...@@ -950,7 +949,18 @@ reactFunEq from_this fsk1 solve_this fsk2
; traceTcS "reactFunEq done" (ppr from_this $$ ppr fsk1 $$ ; traceTcS "reactFunEq done" (ppr from_this $$ ppr fsk1 $$
ppr solve_this $$ ppr fsk2) } ppr solve_this $$ ppr fsk2) }
{- {- Note [lookupFlattenTyVar]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Supppose we have an injective function F and
inert_funeqs: F t1 ~ fsk1
F t2 ~ fsk2
model fsk1 ~ fsk2
We never rewrite the RHS (cc_fsk) of a CFunEqCan. But we /do/ want to
get the [D] t1 ~ t2 from the injectiveness of F. So we look up the
cc_fsk of CFunEqCans in the model when trying to find derived
equalities arising from injectivity.
Note [Type inference for type families with injectivity] Note [Type inference for type families with injectivity]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have a type family with an injectivity annotation: Suppose we have a type family with an injectivity annotation:
...@@ -1086,10 +1096,10 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv ...@@ -1086,10 +1096,10 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
, cc_eq_rel = eq_rel }) , cc_eq_rel = eq_rel })
| (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i } | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
<- findTyEqs inerts tv <- findTyEqs inerts tv
, ev_i `canDischarge` ev , ev_i `eqCanDischarge` ev
, rhs_i `tcEqType` rhs ] , rhs_i `tcEqType` rhs ]
= -- Inert: a ~ b = -- Inert: a ~ ty
-- Work item: a ~ b -- Work item: a ~ ty
do { setEvBindIfWanted ev $ do { setEvBindIfWanted ev $
EvCoercion (tcDowngradeRole (eqRelRole eq_rel) EvCoercion (tcDowngradeRole (eqRelRole eq_rel)
(ctEvRole ev_i) (ctEvRole ev_i)
...@@ -1100,7 +1110,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv ...@@ -1100,7 +1110,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
| Just tv_rhs <- getTyVar_maybe rhs | Just tv_rhs <- getTyVar_maybe rhs
, (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i } , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
<- findTyEqs inerts tv_rhs <- findTyEqs inerts tv_rhs
, ev_i `canDischarge` ev , ev_i `eqCanDischarge` ev
, rhs_i `tcEqType` mkTyVarTy tv ] , rhs_i `tcEqType` mkTyVarTy tv ]
= -- Inert: a ~ b = -- Inert: a ~ b
-- Work item: b ~ a -- Work item: b ~ a
...@@ -1530,7 +1540,7 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args ...@@ -1530,7 +1540,7 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
`mkTcTransCo` ctEvCoercion old_ev) ) `mkTcTransCo` ctEvCoercion old_ev) )
; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk } ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
; emitWorkCt new_ct ; updWorkListTcS (extendWorkListFunEq new_ct)
; stopWith old_ev "Fun/Top (given, shortcut)" } ; stopWith old_ev "Fun/Top (given, shortcut)" }
| otherwise | otherwise
...@@ -1549,8 +1559,9 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args ...@@ -1549,8 +1559,9 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
(ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal fam_tc cos) (ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal fam_tc cos)
`mkTcTransCo` new_co) `mkTcTransCo` new_co)
; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk } ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc
; emitWorkCt new_ct , cc_tyargs = xis, cc_fsk = fsk }
; updWorkListTcS (extendWorkListFunEq new_ct)
; stopWith old_ev "Fun/Top (wanted, shortcut)" } ; stopWith old_ev "Fun/Top (wanted, shortcut)" }
where where
loc = ctEvLoc old_ev loc = ctEvLoc old_ev
...@@ -1631,7 +1642,7 @@ Note [Cached solved FunEqs] ...@@ -1631,7 +1642,7 @@ Note [Cached solved FunEqs]
When trying to solve, say (FunExpensive big-type ~ ty), it's important When trying to solve, say (FunExpensive big-type ~ ty), it's important
to see if we have reduced (FunExpensive big-type) before, lest we to see if we have reduced (FunExpensive big-type) before, lest we
simply repeat it. Hence the lookup in inert_solved_funeqs. Moreover simply repeat it. Hence the lookup in inert_solved_funeqs. Moreover
we must use `canDischarge` because both uses might (say) be Wanteds, we must use `funEqCanDischarge` because both uses might (say) be Wanteds,
and we *still* want to save the re-computation. and we *still* want to save the re-computation.
Note [MATCHING-SYNONYMS] Note [MATCHING-SYNONYMS]
......
...@@ -112,7 +112,8 @@ module TcRnTypes( ...@@ -112,7 +112,8 @@ module TcRnTypes(
CtFlavour(..), ctEvFlavour, CtFlavour(..), ctEvFlavour,
CtFlavourRole, ctEvFlavourRole, ctFlavourRole, CtFlavourRole, ctEvFlavourRole, ctFlavourRole,
eqCanRewrite, eqCanRewriteFR, canDischarge, canDischargeFR, eqCanRewrite, eqCanRewriteFR, eqCanDischarge,
funEqCanDischarge, funEqCanDischargeFR,
-- Pretty printing -- Pretty printing
pprEvVarTheta, pprEvVarTheta,
...@@ -2273,54 +2274,74 @@ we can; straight from the Wanteds during improvment. And from a Derived ...@@ -2273,54 +2274,74 @@ we can; straight from the Wanteds during improvment. And from a Derived
ReprEq we could conceivably get a Derived NomEq improvment (by decomposing ReprEq we could conceivably get a Derived NomEq improvment (by decomposing
a type constructor with Nomninal role), and hence unify. a type constructor with Nomninal role), and hence unify.
Note [canDischarge] Note [funEqCanDischarge]
~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~
(x1:c1 `canDischarge` x2:c2) returns True if we can use c1 to Suppose we have two CFunEqCans with the same LHS:
/discharge/ c2; that is, if we can simply drop (x2:c2) altogether, (x1:F ts ~ f1) `funEqCanDischarge` (x2:F ts ~ f2)
perhaps adding a binding for x2 in terms of x1. We only ask this Can we drop x2 in favour of x1, either unifying
question in two cases: f2 (if it's a flatten meta-var) or adding a new Given
(f1 ~ f2), if x2 is a Given?
* Identical equality constraints:
(x1:s~t) `canDischarge` (xs:s~t) Answer: yes if funEqCanDischarge is true.
In this case we can just drop x2 in favour of x1.
Note [eqCanDischarge]
* Function calls with the same LHS: ~~~~~~~~~~~~~~~~~~~~~
(x1:F ts ~ f1) `canDischarge` (x2:F ts ~ f2) Suppose we have two identicla equality constraints
Here we can drop x2 in favour of x1, either unifying (i.e. both LHS and RHS are the same)
f2 (if it's a flatten meta-var) or adding a new Given (x1:s~t) `eqCanDischarge` (xs:s~t)
(f1 ~ f2), if x2 is a Given. Can we just drop x2 in favour of x1?
This is different from eqCanRewrite; for exammple, a Wanted Answer: yes if eqCanDischarge is true.
can certainly discharge an identical Wanted. So canDicharge
does /not/ define a can-rewrite relation in the sense of Note that we do /not/ allow Wanted to discharge Derived.
Definition [Can-rewrite relation] in TcSMonad. We must keep both. Why? Because the Derived may rewrite
other Deriveds in the model whereas the Wanted cannot.
However a Wanted can certainly discharge an identical Wanted. So
eqCanDischarge does /not/ define a can-rewrite relation in the
sense of Definition [Can-rewrite relation] in TcSMonad.
-} -}
-----------------
eqCanRewrite :: CtEvidence -> CtEvidence -> Bool eqCanRewrite :: CtEvidence -> CtEvidence -> Bool
eqCanRewrite ev1 ev2 = eqCanRewriteFR (ctEvFlavourRole ev1)
(ctEvFlavourRole ev2)
eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
-- Very important function! -- Very important function!
-- See Note [eqCanRewrite] -- See Note [eqCanRewrite]
-- See Note [Wanteds do not rewrite Wanteds] -- See Note [Wanteds do not rewrite Wanteds]
-- See Note [Deriveds do rewrite Deriveds] -- See Note [Deriveds do rewrite Deriveds]
eqCanRewriteFR (Given, NomEq) (_, _) = True eqCanRewrite ev1 ev2 = eqCanRewriteFR (ctEvFlavourRole ev1)
eqCanRewriteFR (Given, ReprEq) (_, ReprEq) = True (ctEvFlavourRole ev2)
eqCanRewriteFR _ _ = False
canDischarge :: CtEvidence -> CtEvidence -> Bool eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
-- See Note [canDischarge] eqCanRewriteFR (Given, NomEq) (_, _) = True
canDischarge ev1 ev2 = canDischargeFR (ctEvFlavourRole ev1) eqCanRewriteFR (Given, ReprEq) (_, ReprEq) = True
eqCanRewriteFR (Derived, NomEq) (Derived, NomEq) = True
eqCanRewriteFR _ _ = False
-----------------
funEqCanDischarge :: CtEvidence -> CtEvidence -> Bool
-- See Note [funEqCanDischarge]
funEqCanDischarge ev1 ev2 = funEqCanDischargeFR (ctEvFlavourRole ev1)
(ctEvFlavourRole ev2) (ctEvFlavourRole ev2)
canDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool funEqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool
canDischargeFR (_, ReprEq) (_, NomEq) = False funEqCanDischargeFR (_, ReprEq) (_, NomEq) = False
canDischargeFR (Given, _) _ = True funEqCanDischargeFR (Given, _) _ = True
canDischargeFR (Wanted, _) (Wanted, _) = True funEqCanDischargeFR (Wanted, _) (Wanted, _) = True
canDischargeFR (Wanted, _) (Derived, _) = True funEqCanDischargeFR (Wanted, _) (Derived, _) = True
canDischargeFR (Derived, _) (Derived, _) = True funEqCanDischargeFR (Derived, _) (Derived, _) = True
canDischargeFR _ _ = False funEqCanDischargeFR _ _ = False
-----------------
eqCanDischarge :: CtEvidence -> CtEvidence -> Bool
-- See Note [eqCanDischarge]
eqCanDischarge ev1 ev2 = eqCanDischargeFR (ctEvFlavourRole ev1)
(ctEvFlavourRole ev2)
eqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool
eqCanDischargeFR (_, ReprEq) (_, NomEq) = False
eqCanDischargeFR (Given, _) (Given,_) = True
eqCanDischargeFR (Wanted, _) (Wanted, _) = True
eqCanDischargeFR (Derived, _) (Derived, _) = True
eqCanDischargeFR _ _ = False
{- {-
************************************************************************ ************************************************************************
......
...@@ -6,7 +6,8 @@ module TcSMonad ( ...@@ -6,7 +6,8 @@ module TcSMonad (
-- The work list -- The work list
WorkList(..), isEmptyWorkList, emptyWorkList, WorkList(..), isEmptyWorkList, emptyWorkList,
extendWorkListNonEq, extendWorkListCt, extendWorkListDerived, extendWorkListNonEq, extendWorkListCt, extendWorkListDerived,
extendWorkListCts, extendWorkListEq, appendWorkList, extendWorkListCts, extendWorkListEq, extendWorkListFunEq,
appendWorkList,
selectNextWorkItem, selectNextWorkItem,
workListSize, workListWantedCount, workListSize, workListWantedCount,
updWorkListTcS, updWorkListTcS,
...@@ -53,7 +54,7 @@ module TcSMonad ( ...@@ -53,7 +54,7 @@ module TcSMonad (
getUnsolvedInerts, getUnsolvedInerts,
removeInertCts, getPendingScDicts, isPendingScDict, removeInertCts, getPendingScDicts, isPendingScDict,
addInertCan, addInertEq, insertFunEq, addInertCan, addInertEq, insertFunEq,
emitInsoluble, emitWorkNC, emitWorkCt, emitInsoluble, emitWorkNC,
-- The Model -- The Model
InertModel, kickOutAfterUnification, InertModel, kickOutAfterUnification,
...@@ -243,7 +244,7 @@ extendWorkListDerived loc ev wl ...@@ -243,7 +244,7 @@ extendWorkListDerived loc ev wl
extendWorkListDeriveds :: CtLoc -> [CtEvidence] -> WorkList -> WorkList extendWorkListDeriveds :: CtLoc -> [CtEvidence] -> WorkList -> WorkList
extendWorkListDeriveds loc evs wl extendWorkListDeriveds loc evs wl
| isDroppableDerivedLoc loc = wl { wl_deriv = evs ++ wl_deriv wl } | isDroppableDerivedLoc loc = wl { wl_deriv = evs ++ wl_deriv wl }
| otherwise = extendWorkListEqs (map mkNonCanonical evs) wl | otherwise = extendWorkListEqs (map mkNonCanonical evs) wl
extendWorkListImplic :: Implication -> WorkList -> WorkList extendWorkListImplic :: Implication -> WorkList -> WorkList
extendWorkListImplic implic wl = wl { wl_implics = implic `consBag` wl_implics wl } extendWorkListImplic implic wl = wl { wl_implics = implic `consBag` wl_implics wl }
...@@ -553,12 +554,16 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more ...@@ -553,12 +554,16 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more
, inert_funeqs :: FunEqMap Ct , inert_funeqs :: FunEqMap Ct
-- All CFunEqCans; index is the whole family head type. -- All CFunEqCans; index is the whole family head type.
-- All Nominal (that's an invarint of all CFunEqCans) -- All Nominal (that's an invarint of all CFunEqCans)
-- LHS is fully rewritten (modulo eqCanRewrite constraints)
-- wrt inert_eqs/inert_model
-- We can get Derived ones from e.g. -- We can get Derived ones from e.g.
-- (a) flattening derived equalities -- (a) flattening derived equalities
-- (b) emitDerivedShadows -- (b) emitDerivedShadows
, inert_dicts :: DictMap Ct , inert_dicts :: DictMap Ct
-- Dictionaries only -- Dictionaries only
-- All fully rewritten (modulo flavour constraints)
-- wrt inert_eqs/inert_model
, inert_safehask :: DictMap Ct , inert_safehask :: DictMap Ct
-- Failed dictionary resolution due to Safe Haskell overlapping -- Failed dictionary resolution due to Safe Haskell overlapping
...@@ -634,34 +639,38 @@ Type-family equations, of form (ev : F tys ~ ty), live in three places ...@@ -634,34 +639,38 @@ Type-family equations, of form (ev : F tys ~ ty), live in three places
Note [inert_model: the inert model] Note [inert_model: the inert model]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Part of the inert set is the “model” * Part of the inert set is the “model”
* The “Model” is an non-idempotent but no-occurs-check * The “Model” is an non-idempotent but no-occurs-check
substitution, reflecting *all* *Nominal* equalities (a ~N ty) substitution, reflecting *all* *Nominal* equalities (a ~N ty)
that are not immediately soluble by unification. that are not immediately soluble by unification.
* The principal reason for maintaining the model is to generate equalities * All the constraints in the model are Derived CTyEqCans
that tell us how unify a variable: that is, what Mark Jones calls That is if (a -> ty) is in the model, then
"improvement". The same idea is sometimes also called "saturation"; we have an inert constraint [D] a ~N ty.
find all the equalities that must hold in any solution.
* There are two sources of constraints in the model: * There are two sources of constraints in the model:
- Derived constraints arising from functional dependencies, or - Derived constraints arising from functional dependencies, or
decomposing injective arguments of type functions, and suchlike. decomposing injective arguments of type functions, and
suchlike.
- A "shadow copy" for every Given or Wanted (a ~N ty) in - A Derived "shadow copy" for every Given or Wanted (a ~N ty) in
inert_eqs. We imagine that every G/W immediately generates its shadow inert_eqs.
constraint, but we refrain from actually generating the constraint itself
until necessary. See (DShadow) and (GWShadow) in
Note [Adding an inert canonical constraint the InertCans]
* If (a -> ty) is in the model, then it is * The principal reason for maintaining the model is to generate
as if we had an inert constraint [D] a ~N ty. equalities that tell us how to unify a variable: that is, what
Mark Jones calls "improvement". The same idea is sometimes also
called "saturation"; find all the equalities that must hold in
any solution.
* Domain of the model = skolems + untouchables * Domain of the model = skolems + untouchables.
A touchable unification variable wouuld have been unified first.
* The inert_eqs are all Given/Wanted. The Derived ones are in the * The inert_eqs are all Given/Wanted. The Derived ones are in the
inert_model only. inert_model only.
* However inert_dicts, inert_irreds may well contain derived costraints. * However inert_dicts, inert_funeqs, inert_irreds
may well contain derived costraints.
Note [inert_eqs: the inert equalities] Note [inert_eqs: the inert equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
...@@ -783,7 +792,7 @@ The idea is that ...@@ -783,7 +792,7 @@ The idea is that
* Lemma (L2): if not (fw >= fw), then K1-K3 all hold. * Lemma (L2): if not (fw >= fw), then K1-K3 all hold.
Proof: using Definition [Can-rewrite relation], fw can't rewrite anything Proof: using Definition [Can-rewrite relation], fw can't rewrite anything
and so K1-K3 hold. Intuitivel, since fw can't rewrite anything, and so K1-K3 hold. Intuitively, since fw can't rewrite anything,
adding it cannot cause any loops adding it cannot cause any loops
This is a common case, because Wanteds cannot rewrite Wanteds. This is a common case, because Wanteds cannot rewrite Wanteds.
...@@ -1085,18 +1094,9 @@ Note [Adding an inert canonical constraint the InertCans] ...@@ -1085,18 +1094,9 @@ Note [Adding an inert canonical constraint the InertCans]
* Adding a *nominal* CTyEqCan (a ~N ty) to the inert set (TcSMonad.addInertEq). * Adding a *nominal* CTyEqCan (a ~N ty) to the inert set (TcSMonad.addInertEq).
* We always (G/W/D) kick out constraints that can be rewritten * Always (G/W/D) kick out constraints that can be rewritten
(respecting flavours) by the new constraint. (respecting flavours) by the new constraint. This is done
- This is done by kickOutRewritable; by kickOutRewritable.
see Note [inert_eqs: the inert equalities].
- We do not need to kick anything out from the model; we only
add [D] constraints to the model (in effect) and they are
fully rewritten by the model, so (K2b) holds
- A Derived equality can kick out [D] constraints in inert_dicts,
inert_irreds etc. Nothing in inert_eqs because there are no
Derived constraints in inert_eqs (they are in the model)
Then, when adding: Then, when adding:
...@@ -1104,7 +1104,7 @@ Note [Adding an inert canonical constraint the InertCans] ...@@ -1104,7 +1104,7 @@ Note [Adding an inert canonical constraint the InertCans]
1. Add (a~ty) to the model 1. Add (a~ty) to the model
NB: 'a' cannot be in fv(ty), because the constraint is canonical. NB: 'a' cannot be in fv(ty), because the constraint is canonical.
2. (DShadow) Emit shadow-copies (emitDerivedShadows): 2. (DShadow) Do emitDerivedShadows
For every inert G/W constraint c, st For every inert G/W constraint c, st
(a) (a~ty) can rewrite c (see Note [Emitting shadow constraints]), (a) (a~ty) can rewrite c (see Note [Emitting shadow constraints]),
and and
...@@ -1114,18 +1114,18 @@ Note [Adding an inert canonical constraint the InertCans] ...@@ -1114,18 +1114,18 @@ Note [Adding an inert canonical constraint the InertCans]
generated a shadow copy generated a shadow copy
* [Given/Wanted] a ~N ty * [Given/Wanted] a ~N ty
1. Add it to inert_eqs 1. Add it to inert_eqs
2. If the model can rewrite (a~ty) 2. Emit [D] a~ty
then (GWShadow) emit [D] a~ty As a result of (2), the current model will rewrite teh new [D] a~ty
else (GWModel) Use emitDerivedShadows just like (DShadow) during canonicalisation, and then it'll be added to the model using
and add a~ty to the model the steps of [Derived] above.
(Reason:[D] a~ty is inert wrt model, and (K2b) holds)
* [Given/Wanted] a ~R ty: just add it to inert_eqs * [Representational equalities] a ~R ty: just add it to inert_eqs
* Unifying a:=ty, is like adding [G] a~ty, but we can't make a [D] a~ty, as in * Unifying a:=ty, is like adding [G] a~ty, but we can't make a [D]
step (1) of the [G/W] case above. So instead, do kickOutAfterUnification: a~ty, as in step (1) of the [G/W] case above. So instead, do
kickOutAfterUnification:
- Kick out from the model any equality (b~ty2) that mentions 'a' - Kick out from the model any equality (b~ty2) that mentions 'a'
(i.e. a=b or a in ty2). Example: (i.e. a=b or a in ty2). Example:
[G] a ~ [b], model [D] b ~ [a] [G] a ~ [b], model [D] b ~ [a]
...@@ -1196,33 +1196,32 @@ add_inert_eq ics@(IC { inert_count = n ...@@ -1196,33 +1196,32 @@ add_inert_eq ics@(IC { inert_count = n
, inert_eqs = old_eqs , inert_eqs = old_eqs
, inert_model = old_model })