A little tidying up in the flattener
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 9 Jan 2015 11:51:52 +0000 (11:51 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 9 Jan 2015 11:52:16 +0000 (11:52 +0000)
Particularly, flatten_many was exported, but the caller was not doing
runFlatten.  Moreover it was always used at nominal role.

This patch makes the API clearer, and more robust

compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcFlatten.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcRnTypes.hs

index 65ebfd9..62efe90 100644 (file)
@@ -231,7 +231,7 @@ canClassNC ev cls tys
 canClass ev cls tys
   =   -- all classes do *nominal* matching
     ASSERT2( ctEvRole ev == Nominal, ppr ev $$ ppr cls $$ ppr tys )
-    do { (xis, cos) <- flattenMany FM_FlattenAll ev (repeat Nominal) tys
+    do { (xis, cos) <- flattenManyNom ev tys
        ; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos
              xi = mkClassPred cls xis
              mk_ct new_ev = CDictCan { cc_ev = new_ev
@@ -931,7 +931,7 @@ canCFunEqCan :: CtEvidence
 -- and the RHS is a fsk, which we must *not* substitute.
 -- So just substitute in the LHS
 canCFunEqCan ev fn tys fsk
-  = do { (tys', cos) <- flattenMany FM_FlattenAll ev (repeat Nominal) tys
+  = do { (tys', cos) <- flattenManyNom ev tys
                         -- cos :: tys' ~ tys
        ; let lhs_co  = mkTcTyConAppCo Nominal fn cos
                         -- :: F tys' ~ F tys
@@ -952,8 +952,7 @@ canEqTyVar :: CtEvidence -> EqRel -> SwapFlag
 -- A TyVar on LHS, but so far un-zonked
 canEqTyVar ev eq_rel swapped tv1 ty2 ps_ty2              -- ev :: tv ~ s2
   = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ty2 $$ ppr swapped)
-       ; let fmode = mkFlattenEnv FM_FlattenAll ev  -- the FM_ param is ignored
-       ; mb_yes <- flattenTyVarOuter fmode tv1
+       ; mb_yes <- flattenTyVar ev tv1
        ; case mb_yes of
          { Right (ty1, co1) -> -- co1 :: ty1 ~ tv1
              do { traceTcS "canEqTyVar2"
index 2a76023..9554bb0 100644 (file)
@@ -2,9 +2,10 @@
 
 module TcFlatten(
    FlattenEnv(..), FlattenMode(..), mkFlattenEnv,
-   flatten, flattenMany, flatten_many,
-   flattenFamApp, flattenTyVarOuter,
+   flatten, flattenManyNom, flattenFamApp, flattenTyVar,
+
    unflatten,
+
    eqCanRewrite, eqCanRewriteFR, canRewriteOrSame,
    CtFlavourRole, ctEvFlavourRole, ctFlavourRole
  ) where
@@ -23,7 +24,6 @@ import Var
 import VarEnv
 import NameEnv
 import Outputable
-import VarSet
 import TcSMonad as TcS
 import DynFlags( DynFlags )
 
@@ -523,57 +523,11 @@ wanteds, we will
 
 ************************************************************************
 *                                                                      *
-*           The main flattening functions
+*                     FlattenEnv
+*             The flattening environment 
 *                                                                      *
 ************************************************************************
 
-Note [Flattening]
-~~~~~~~~~~~~~~~~~~~~
-  flatten ty  ==>   (xi, cc)
-    where
-      xi has no type functions, unless they appear under ForAlls
-
-      cc = Auxiliary given (equality) constraints constraining
-           the fresh type variables in xi.  Evidence for these
-           is always the identity coercion, because internally the
-           fresh flattening skolem variables are actually identified
-           with the types they have been generated to stand in for.
-
-Note that it is flatten's job to flatten *every type function it sees*.
-flatten is only called on *arguments* to type functions, by canEqGiven.
-
-Recall that in comments we use alpha[flat = ty] to represent a
-flattening skolem variable alpha which has been generated to stand in
-for ty.
-
------ Example of flattening a constraint: ------
-  flatten (List (F (G Int)))  ==>  (xi, cc)
-    where
-      xi  = List alpha
-      cc  = { G Int ~ beta[flat = G Int],
-              F beta ~ alpha[flat = F beta] }
-Here
-  * alpha and beta are 'flattening skolem variables'.
-  * All the constraints in cc are 'given', and all their coercion terms
-    are the identity.
-
-NB: Flattening Skolems only occur in canonical constraints, which
-are never zonked, so we don't need to worry about zonking doing
-accidental unflattening.
-
-Note that we prefer to leave type synonyms unexpanded when possible,
-so when the flattener encounters one, it first asks whether its
-transitive expansion contains any type function applications.  If so,
-it expands the synonym and proceeds; if not, it simply returns the
-unexpanded synonym.
-
-Note [Flattener EqRels]
-~~~~~~~~~~~~~~~~~~~~~~~
-When flattening, we need to know which equality relation -- nominal
-or representation -- we should be respecting. The only difference is
-that we rewrite variables by representational equalities when fe_eq_rel
-is ReprEq.
-
 -}
 
 data FlattenEnv
@@ -585,15 +539,15 @@ data FlattenEnv
 data FlattenMode  -- Postcondition for all three: inert wrt the type substitution
   = FM_FlattenAll          -- Postcondition: function-free
 
-  | FM_Avoid TcTyVar Bool  -- See Note [Lazy flattening]
-                           -- Postcondition:
-                           --  * tyvar is only mentioned in result under a rigid path
-                           --    e.g.   [a] is ok, but F a won't happen
-                           --  * If flat_top is True, top level is not a function application
-                           --   (but under type constructors is ok e.g. [F a])
-
   | FM_SubstOnly           -- See Note [Flattening under a forall]
 
+--  | FM_Avoid TcTyVar Bool  -- See Note [Lazy flattening]
+--                           -- Postcondition:
+--                           --  * tyvar is only mentioned in result under a rigid path
+--                           --    e.g.   [a] is ok, but F a won't happen
+--                           --  * If flat_top is True, top level is not a function application
+--                           --   (but under type constructors is ok e.g. [F a])
+
 mkFlattenEnv :: FlattenMode -> CtEvidence -> FlattenEnv
 mkFlattenEnv fm ctev = FE { fe_mode    = fm
                           , fe_loc     = ctEvLoc ctev
@@ -603,7 +557,33 @@ mkFlattenEnv fm ctev = FE { fe_mode    = fm
 feRole :: FlattenEnv -> Role
 feRole = eqRelRole . fe_eq_rel
 
+-- | Change the 'EqRel' in a 'FlattenEnv'. Avoids allocating a
+-- new 'FlattenEnv' where possible.
+setFEEqRel :: FlattenEnv -> EqRel -> FlattenEnv
+setFEEqRel fmode@(FE { fe_eq_rel = old_eq_rel }) new_eq_rel
+  | old_eq_rel == new_eq_rel = fmode
+  | otherwise                = fmode { fe_eq_rel = new_eq_rel }
+
+-- | Change the 'FlattenMode' in a 'FlattenEnv'. Avoids allocating
+-- a new 'FlattenEnv' where possible.
+setFEMode :: FlattenEnv -> FlattenMode -> FlattenEnv
+setFEMode fmode@(FE { fe_mode = old_mode }) new_mode
+  | old_mode `eq` new_mode = fmode
+  | otherwise              = fmode { fe_mode = new_mode }
+  where
+    FM_FlattenAll   `eq` FM_FlattenAll   = True
+    FM_SubstOnly    `eq` FM_SubstOnly    = True
+--  FM_Avoid tv1 b1 `eq` FM_Avoid tv2 b2 = tv1 == tv2 && b1 == b2
+    _               `eq` _               = False
+
 {-
+Note [Flattener EqRels]
+~~~~~~~~~~~~~~~~~~~~~~~
+When flattening, we need to know which equality relation -- nominal
+or representation -- we should be respecting. The only difference is
+that we rewrite variables by representational equalities when fe_eq_rel
+is ReprEq.
+
 Note [Lazy flattening]
 ~~~~~~~~~~~~~~~~~~~~~~
 The idea of FM_Avoid mode is to flatten less aggressively.  If we have
@@ -644,6 +624,96 @@ soon throw out the phantoms when decomposing a TyConApp. (Or, the
 canonicaliser will emit an insoluble, in which case the unflattened version
 yields a better error message anyway.)
 
+-}
+
+{- *********************************************************************
+*                                                                      *
+*      Externally callable flattening functions                        *
+*                                                                      *
+*  They are all wrapped in runFlatten, so their                        *
+*  flattening work gets put into the work list                         *
+*                                                                      *
+********************************************************************* -}
+
+flatten :: FlattenMode -> CtEvidence -> TcType -> TcS (Xi, TcCoercion)
+flatten mode ev ty
+  = runFlatten (flatten_one fmode ty)
+  where
+    fmode = mkFlattenEnv mode ev
+
+flattenManyNom :: CtEvidence -> [TcType] -> TcS ([Xi], [TcCoercion])
+-- Externally-callable, hence runFlatten
+-- Flatten a bunch of types all at once; in fact they are
+-- always the arguments of a saturated type-family, so
+--      ctEvFlavour ev = Nominal
+-- and we want to flatten all at nominal role
+flattenManyNom ev tys
+  = runFlatten (flatten_many_nom fmode tys)
+  where
+    fmode = mkFlattenEnv FM_FlattenAll ev
+
+flattenFamApp :: FlattenMode -> CtEvidence
+              -> TyCon -> [TcType] -> TcS (Xi, TcCoercion)
+-- Externally callable, hence runFlatten
+flattenFamApp mode ev tc tys
+  = runFlatten (flatten_fam_app fmode tc tys)
+  where
+    fmode = mkFlattenEnv mode ev
+
+flattenTyVar :: CtEvidence -> TcTyVar
+             -> TcS (Either TyVar (TcType, TcCoercion))
+flattenTyVar ev tv
+  = runFlatten (flatten_tyvar fmode tv)
+  where
+    fmode = mkFlattenEnv FM_FlattenAll ev
+
+
+{- *********************************************************************
+*                                                                      *
+*           The main flattening functions
+*                                                                      *
+********************************************************************* -}
+
+{- Note [Flattening]
+~~~~~~~~~~~~~~~~~~~~
+  flatten ty  ==>   (xi, cc)
+    where
+      xi has no type functions, unless they appear under ForAlls
+
+      cc = Auxiliary given (equality) constraints constraining
+           the fresh type variables in xi.  Evidence for these
+           is always the identity coercion, because internally the
+           fresh flattening skolem variables are actually identified
+           with the types they have been generated to stand in for.
+
+Note that it is flatten's job to flatten *every type function it sees*.
+flatten is only called on *arguments* to type functions, by canEqGiven.
+
+Recall that in comments we use alpha[flat = ty] to represent a
+flattening skolem variable alpha which has been generated to stand in
+for ty.
+
+----- Example of flattening a constraint: ------
+  flatten (List (F (G Int)))  ==>  (xi, cc)
+    where
+      xi  = List alpha
+      cc  = { G Int ~ beta[flat = G Int],
+              F beta ~ alpha[flat = F beta] }
+Here
+  * alpha and beta are 'flattening skolem variables'.
+  * All the constraints in cc are 'given', and all their coercion terms
+    are the identity.
+
+NB: Flattening Skolems only occur in canonical constraints, which
+are never zonked, so we don't need to worry about zonking doing
+accidental unflattening.
+
+Note that we prefer to leave type synonyms unexpanded when possible,
+so when the flattener encounters one, it first asks whether its
+transitive expansion contains any type function applications.  If so,
+it expands the synonym and proceeds; if not, it simply returns the
+unexpanded synonym.
+
 Note [flatten_many performance]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In programs with lots of type-level evaluation, flatten_many becomes
@@ -674,33 +744,8 @@ and T5321Fun.
 If we need to make this yet more performant, a possible way forward is to
 duplicate the flattener code for the nominal case, and make that case
 faster. This doesn't seem quite worth it, yet.
-
 -}
 
-------------------
-flatten :: FlattenMode -> CtEvidence -> TcType -> TcS (Xi, TcCoercion)
-flatten mode ev ty
-  = runFlatten (flatten_one fmode ty)
-  where
-    fmode = mkFlattenEnv mode ev
-
-flattenMany :: FlattenMode -> CtEvidence -> [Role]
-            -> [TcType] -> TcS ([Xi], [TcCoercion])
--- Flatten a bunch of types all at once. Roles on the coercions returned
--- always match the corresponding roles passed in.
-flattenMany mode ev roles tys
-  = runFlatten (flatten_many fmode roles tys)
-  where
-    fmode = mkFlattenEnv mode ev
-
-flattenFamApp :: FlattenMode -> CtEvidence
-              -> TyCon -> [TcType] -> TcS (Xi, TcCoercion)
-flattenFamApp mode ev tc tys
-  = runFlatten (flatten_fam_app fmode tc tys)
-  where
-    fmode = mkFlattenEnv mode ev
-
-------------------
 flatten_many :: FlattenEnv -> [Role] -> [Type] -> TcS ([Xi], [TcCoercion])
 -- Coercions :: Xi ~ Type, at roles given
 -- Returns True iff (no flattening happened)
@@ -738,7 +783,18 @@ flatten_one :: FlattenEnv -> TcType -> TcS (Xi, TcCoercion)
 flatten_one fmode xi@(LitTy {}) = return (xi, mkTcReflCo (feRole fmode) xi)
 
 flatten_one fmode (TyVarTy tv)
-  = flattenTyVar fmode tv
+  = do { mb_yes <- flatten_tyvar fmode tv
+       ; case mb_yes of
+           Left tv' -> -- Done
+                       do { traceTcS "flattenTyVar1" (ppr tv $$ ppr (tyVarKind tv'))
+                          ; return (ty', mkTcReflCo (feRole fmode) ty') }
+                    where
+                       ty' = mkTyVarTy tv'
+
+           Right (ty1, co1)  -- Recurse
+                    -> do { (ty2, co2) <- flatten_one fmode ty1
+                          ; traceTcS "flattenTyVar2" (ppr tv $$ ppr ty2)
+                          ; return (ty2, co2 `mkTcTransCo` co1) } }
 
 flatten_one fmode (AppTy ty1 ty2)
   = do { (xi1,co1) <- flatten_one fmode ty1
@@ -888,12 +944,12 @@ flatten_exact_fam_app fmode tc tys
                           ; return ( mkTyConApp tc xis
                                    , mkTcTyConAppCo (feRole fmode) tc cos ) }
 
-       FM_Avoid tv flat_top ->
-         do { (xis, cos) <- flatten_many fmode roles tys
-            ; if flat_top || tv `elemVarSet` tyVarsOfTypes xis
-              then flatten_exact_fam_app_fully fmode tc tys
-              else return ( mkTyConApp tc xis
-                          , mkTcTyConAppCo (feRole fmode) tc cos ) }
+--       FM_Avoid tv flat_top ->
+--         do { (xis, cos) <- flatten_many fmode roles tys
+--            ; if flat_top || tv `elemVarSet` tyVarsOfTypes xis
+--              then flatten_exact_fam_app_fully fmode tc tys
+--              else return ( mkTyConApp tc xis
+--                          , mkTcTyConAppCo (feRole fmode) tc cos ) }
   where
     -- These are always going to be Nominal for now,
     -- but not if #8177 is implemented
@@ -902,10 +958,12 @@ flatten_exact_fam_app fmode tc tys
 flatten_exact_fam_app_fully fmode tc tys
   -- See Note [Reduce type family applications eagerly]
   = try_to_reduce tc tys False id $
-    do { (xis, cos) <- flatten_many_nom (setFEEqRel (setFEMode fmode FM_FlattenAll) NomEq) tys
+    do { -- First, flatten the arguments
+         (xis, cos) <- flatten_many_nom (setFEEqRel fmode NomEq) tys
        ; let ret_co = mkTcTyConAppCo (feRole fmode) tc cos
               -- ret_co :: F xis ~ F tys
 
+        -- Now, look in the cache
        ; mb_ct <- lookupFlatCache tc xis
        ; case mb_ct of
            Just (co, rhs_ty, flav)  -- co :: F xis ~ fsk
@@ -1232,39 +1290,16 @@ subsitution means that the proof in Note [The inert equalities] may need
 to be revisited, but we don't think that the end conclusion is wrong.
 -}
 
-flattenTyVar :: FlattenEnv -> TcTyVar -> TcS (Xi, TcCoercion)
+flatten_tyvar :: FlattenEnv -> TcTyVar
+              -> TcS (Either TyVar (TcType, TcCoercion))
 -- "Flattening" a type variable means to apply the substitution to it
--- The substitution is actually the union of
---     * the unifications that have taken place (either before the
---       solver started, or in TcInteract.solveByUnification)
---     * the CTyEqCans held in the inert set
---
--- Postcondition: co : xi ~ tv
-flattenTyVar fmode tv
-  = do { mb_yes <- flattenTyVarOuter fmode tv
-       ; case mb_yes of
-           Left tv' -> -- Done
-                       do { traceTcS "flattenTyVar1" (ppr tv $$ ppr (tyVarKind tv'))
-                          ; return (ty', mkTcReflCo (feRole fmode) ty') }
-                    where
-                       ty' = mkTyVarTy tv'
-
-           Right (ty1, co1)  -- Recurse
-                    -> do { (ty2, co2) <- flatten_one fmode ty1
-                          ; traceTcS "flattenTyVar3" (ppr tv $$ ppr ty2)
-                          ; return (ty2, co2 `mkTcTransCo` co1) }
-       }
-
-flattenTyVarOuter :: FlattenEnv -> TcTyVar
-                  -> TcS (Either TyVar (TcType, TcCoercion))
--- Look up the tyvar in
---   a) the internal MetaTyVar box
---   b) the tyvar binds
---   c) the inerts
+-- Specifically, look up the tyvar in
+--   * the internal MetaTyVar box
+--   * the inerts
 -- Return (Left tv')      if it is not found, tv' has a properly zonked kind
 --        (Right (ty, co) if found, with co :: ty ~ tv;
 
-flattenTyVarOuter fmode tv
+flatten_tyvar fmode tv
   | not (isTcTyVar tv)             -- Happens when flatten under a (forall a. ty)
   = Left `liftM` flattenTyVarFinal fmode tv
           -- So ty contains refernces to the non-TcTyVar a
@@ -1589,21 +1624,3 @@ unsolved constraints.  The flat form will be
 Flatten using the fun-eqs first.
 -}
 
--- | Change the 'EqRel' in a 'FlattenEnv'. Avoids allocating a
--- new 'FlattenEnv' where possible.
-setFEEqRel :: FlattenEnv -> EqRel -> FlattenEnv
-setFEEqRel fmode@(FE { fe_eq_rel = old_eq_rel }) new_eq_rel
-  | old_eq_rel == new_eq_rel = fmode
-  | otherwise                = fmode { fe_eq_rel = new_eq_rel }
-
--- | Change the 'FlattenMode' in a 'FlattenEnv'. Avoids allocating
--- a new 'FlattenEnv' where possible.
-setFEMode :: FlattenEnv -> FlattenMode -> FlattenEnv
-setFEMode fmode@(FE { fe_mode = old_mode }) new_mode
-  | old_mode `eq` new_mode = fmode
-  | otherwise            = fmode { fe_mode = new_mode }
-  where
-    FM_FlattenAll   `eq` FM_FlattenAll   = True
-    FM_SubstOnly    `eq` FM_SubstOnly    = True
-    FM_Avoid tv1 b1 `eq` FM_Avoid tv2 b2 = tv1 == tv2 && b1 == b2
-    _               `eq` _               = False
index d38036c..c401aca 100644 (file)
@@ -1341,7 +1341,7 @@ doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
               -- flattening, occurs-check, and ufsk := ufsk issues
           ; let final_co = ax_co `mkTcTransCo` mkTcSymCo (ctEvCoercion new_ev)
               --    ax_co :: fam_tc args ~ rhs_ty
-              --       ev :: alpha ~ rhs_ty
+              --   new_ev :: alpha ~ rhs_ty
               --     ufsk := alpha
               -- final_co :: fam_tc args ~ alpha
           ; dischargeFmv (ctEvId old_ev) fsk final_co alpha_ty
@@ -1370,8 +1370,7 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
   | isGiven old_ev
   = ASSERT( ctEvEqRel old_ev == NomEq )
     runFlatten $
-    do { let fmode = mkFlattenEnv FM_FlattenAll old_ev
-       ; (xis, cos) <- flatten_many fmode (repeat Nominal) tc_args
+    do { (xis, cos) <- flattenManyNom old_ev tc_args
                -- ax_co :: F args ~ G tc_args
                -- cos   :: xis ~ tc_args
                -- old_ev :: F args ~ fsk
@@ -1390,16 +1389,15 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
   | otherwise
   = ASSERT( not (isDerived old_ev) )   -- Caller ensures this
     ASSERT( ctEvEqRel old_ev == NomEq )
-    runFlatten $
-    do { let fmode = mkFlattenEnv FM_FlattenAll old_ev
-       ; (xis, cos) <- flatten_many fmode (repeat Nominal) tc_args
+    do { (xis, cos) <- flattenManyNom old_ev tc_args
                -- ax_co :: F args ~ G tc_args
                -- cos   :: xis ~ tc_args
                -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
                -- new_ev :: G xis ~ fsk
                -- old_ev :: F args ~ fsk := ax_co ; sym (G cos) ; new_ev
 
-       ; new_ev <- newWantedEvVarNC loc (mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk))
+       ; new_ev <- newWantedEvVarNC deeper_loc 
+                                    (mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk))
        ; setWantedEvBind (ctEvId old_ev)
                    (EvCoercion (ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal fam_tc cos)
                                       `mkTcTransCo` ctEvCoercion new_ev))
index 90aba1d..dbafa52 100644 (file)
@@ -1811,9 +1811,9 @@ subGoalCounterValue CountTyFunApps   (SubGoalDepth _ f) = f
 
 subGoalDepthExceeded :: SubGoalDepth -> SubGoalDepth -> Maybe SubGoalCounter
 subGoalDepthExceeded (SubGoalDepth mc mf) (SubGoalDepth c f)
-        | c > mc    = Just CountConstraints
-        | f > mf    = Just CountTyFunApps
-        | otherwise = Nothing
+  | c > mc    = Just CountConstraints
+  | f > mf    = Just CountTyFunApps
+  | otherwise = Nothing
 
 -- | Checks whether the evidence can be used to solve a goal with the given minimum depth
 -- See Note [Preventing recursive dictionaries]