Comments only, on inert_fsks and inert_no_eqs
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 9 May 2014 09:40:50 +0000 (10:40 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 12 May 2014 15:04:10 +0000 (16:04 +0100)
I wrote these when studying Trac #9090

compiler/typecheck/TcInteract.lhs
compiler/typecheck/TcRnTypes.lhs
compiler/typecheck/TcSMonad.lhs

index b8c4c81..064bda2 100644 (file)
@@ -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 }
index d598764..7670566 100644 (file)
@@ -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
 
index 51f4945..dee4fe4 100644 (file)
@@ -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)