Commit 2745164a by Simon Peyton Jones

### Comments only, on inert_fsks and inert_no_eqs

I wrote these when studying Trac #9090
parent fe8a378c
 ... ... @@ -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 } ... ...
 ... ... @@ -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 ... ...
 ... ... @@ -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) ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!