[commit: ghc] master: Comments only, on inert_fsks and inert_no_eqs (2745164)
git at git.haskell.org
git at git.haskell.org
Mon May 12 15:04:21 UTC 2014
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/2745164acfd582d930cbc5080fdf052f61f6893e/ghc
>---------------------------------------------------------------
commit 2745164acfd582d930cbc5080fdf052f61f6893e
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Fri May 9 10:40:50 2014 +0100
Comments only, on inert_fsks and inert_no_eqs
I wrote these when studying Trac #9090
>---------------------------------------------------------------
2745164acfd582d930cbc5080fdf052f61f6893e
compiler/typecheck/TcInteract.lhs | 1 +
compiler/typecheck/TcRnTypes.lhs | 2 ++
compiler/typecheck/TcSMonad.lhs | 59 +++++++++++++++++++++++++++++++++------
3 files changed, 53 insertions(+), 9 deletions(-)
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index b8c4c81..064bda2 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -101,6 +101,7 @@ solveInteractGiven loc old_fsks givens
, ctev_loc = loc }
| ev_id <- givens ]
+ -- See Note [Given flatten-skolems] in TcSMonad
fsk_bag = listToBag [ mkNonCanonical $ CtGiven { ctev_evtm = EvCoercion (mkTcNomReflCo tv_ty)
, ctev_pred = pred
, ctev_loc = loc }
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index d598764..7670566 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -1282,6 +1282,8 @@ data Implication
ic_fsks :: [TcTyVar], -- Extra flatten-skolems introduced by
-- by flattening the givens
+ -- See Note [Given flatten-skolems]
+
ic_no_eqs :: Bool, -- True <=> ic_givens have no equalities, for sure
-- False <=> ic_givens might have equalities
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 51f4945..dee4fe4 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -458,6 +458,7 @@ data InertSet
, inert_fsks :: [TcTyVar] -- Rigid flatten-skolems (arising from givens)
-- allocated in this local scope
+ -- See Note [Given flatten-skolems]
, inert_solved_funeqs :: FunEqMap (CtEvidence, TcType)
-- See Note [Type family equations]
@@ -475,8 +476,29 @@ data InertSet
-- - Stored not necessarily as fully rewritten
-- (ToDo: rewrite lazily when we lookup)
}
+\end{code}
+Note [Given flatten-skolems]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we simplify the implication
+ forall b. C (F a) b => (C (F a) beta, blah)
+We'll flatten the givens, introducing a flatten-skolem, so the
+givens effectively look like
+ (C fsk b, F a ~ fsk)
+Then we simplify the wanteds, transforming (C (F a) beta) to (C fsk beta).
+Now, if we don't solve that wanted, we'll put it back into the residual
+implicaiton. But where is fsk bound?
+
+We solve this by recording the given flatten-skolems in the implication
+(the ic_fsks field), so it's as if we change the implication to
+ forall b, fsk. (C fsk b, F a ~ fsk) => (C fsk beta, blah)
+
+We don't need to explicitly record the (F a ~ fsk) constraint in the implication
+because we can recover it from inside the fsk TyVar itself. But we do need
+to treat that (F a ~ fsk) as a new given. See the fsk_bag stuff in
+TcInteract.solveInteractGiven.
+\begin{code}
instance Outputable InertCans where
ppr ics = vcat [ ptext (sLit "Equalities:")
<+> vcat (map ppr (varEnvElts (inert_eqs ics)))
@@ -503,9 +525,9 @@ emptyInert
, inert_funeqs = emptyFunEqs
, inert_irreds = emptyCts
, inert_insols = emptyCts
- , inert_no_eqs = True
+ , inert_no_eqs = True -- See Note [inert_fsks and inert_no_eqs]
}
- , inert_fsks = []
+ , inert_fsks = [] -- See Note [inert_fsks and inert_no_eqs]
, inert_flat_cache = emptyFunEqs
, inert_solved_funeqs = emptyFunEqs
, inert_solved_dicts = emptyDictMap }
@@ -518,10 +540,12 @@ addInertCan ics item@(CTyEqCan { cc_ev = ev })
(inert_eqs ics)
(cc_tyvar item) [item]
, inert_no_eqs = isFlatSkolEv ev && inert_no_eqs ics }
+ -- See Note [When does an implication have given equalities?] in TcSimplify
addInertCan ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys, cc_ev = ev })
= ics { inert_funeqs = addFunEq (inert_funeqs ics) tc tys item
, inert_no_eqs = isFlatSkolEv ev && inert_no_eqs ics }
+ -- See Note [When does an implication have given equalities?] in TcSimplify
addInertCan ics item@(CIrredEvCan {})
= ics { inert_irreds = inert_irreds ics `Bag.snocBag` item
@@ -598,7 +622,7 @@ prepareInertsForImplications is
, inert_irreds = Bag.filterBag isGivenCt irreds
, inert_dicts = filterDicts isGivenCt dicts
, inert_insols = emptyCts
- , inert_no_eqs = True -- Ready for each implication
+ , inert_no_eqs = True -- See Note [inert_fsks and inert_no_eqs]
}
is_given_eq :: [Ct] -> Bool
@@ -1254,19 +1278,36 @@ getUntouchables :: TcS Untouchables
getUntouchables = wrapTcS TcM.getUntouchables
getGivenInfo :: TcS a -> TcS (Bool, [TcTyVar], a)
--- Run thing_inside, returning info on
--- a) whether we got any new equalities
--- b) which new (given) flatten skolems were generated
+-- See Note [inert_fsks and inert_no_eqs]
getGivenInfo thing_inside
- = do { updInertTcS reset_vars
- ; res <- thing_inside
- ; is <- getTcSInerts
+ = do {
+ ; updInertTcS reset_vars -- Set inert_fsks and inert_no_eqs to initial values
+ ; res <- thing_inside -- Run thing_inside
+ ; is <- getTcSInerts -- Get new values of inert_fsks and inert_no_eqs
; return (inert_no_eqs (inert_cans is), inert_fsks is, res) }
where
reset_vars :: InertSet -> InertSet
reset_vars is = is { inert_cans = (inert_cans is) { inert_no_eqs = True }
, inert_fsks = [] }
+\end{code}
+Note [inert_fsks and inert_no_eqs]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The function getGivenInfo runs thing_inside to see what new flatten-skolems
+and equalities are generated by thing_inside. To that end,
+ * it initialises inert_fsks, inert_no_eqs
+ * runs thing_inside
+ * reads out inert_fsks, inert_no_eqs
+This is the only place where it matters what inert_fsks and inert_no_eqs
+are initialised to. In other places (eg emptyIntert), we need to set them
+to something (because they are strict) but they will never be looked at.
+
+See Note [When does an implication have given equalities?] in TcSimplify
+for more details about inert_no_eqs.
+
+See Note [Given flatten-skolems] for more details about inert_fsks.
+
+\begin{code}
getTcSTyBinds :: TcS (IORef (Bool, TyVarEnv (TcTyVar, TcType)))
getTcSTyBinds = TcS (return . tcs_ty_binds)
More information about the ghc-commits
mailing list