Further wibbleswip/T8095-spj

2 files changed, 24 insertions, 15 deletions

diff --git a/compiler/GHC/Core/TyCo/FVs.hs b/compiler/GHC/Core/TyCo/FVs.hs
index 7b2bcac310..0cf3db19c7 100644
--- a/compiler/GHC/Core/TyCo/FVs.hs
+++ b/compiler/GHC/Core/TyCo/FVs.hs
@@ -268,6 +268,7 @@ type InScopeBndrs  = TyCoVarSet
 newtype TyCoAcc acc = TCA' { runTCA :: InScopeBndrs -> acc -> acc }
 
 pattern TCA :: forall acc. (InScopeBndrs -> acc -> acc) -> TyCoAcc acc
+-- See GHC.Core.Unify Note [The one-shot state monad trick]
 {-# COMPLETE TCA #-}
 pattern TCA f <- TCA' f
   where
@@ -290,17 +291,17 @@ emptyInScope :: InScopeBndrs
 emptyInScope = emptyVarSet
 
 addTyCoVar :: TyCoVar -> TyCoAcc TyCoVarSet -> TyCoAcc TyCoVarSet
--- Add a variable tcv, and the extras, to the free vars unless
--- tcv is in the in-scope
---  or is already in the in-scope set-
--- The 'extras' start from an empty in-scope set;
---    see Note [Closing over free variable kinds]
-addTyCoVar tcv (TCA add_extras) = TCA add_it
+-- If 'tcv' is (a) in scope or (b) in the accumulator, then do nothing
+-- Otherwise:
+--   - Add 'tcv' to the accumulator, and
+--   - Run 'add_kind_fvs' starting from an empty in-scope set;
+--     see Note [Closing over free variable kinds]
+addTyCoVar tcv (TCA add_kind_fvs) = TCA add_it
   where
     add_it is acc
       | tcv `elemVarSet` is  = acc
       | tcv `elemVarSet` acc = acc
-      | otherwise            = add_extras emptyVarSet (acc `extendVarSet` tcv)
+      | otherwise            = add_kind_fvs emptyVarSet (acc `extendVarSet` tcv)
 
 extendInScope :: TyCoVar -> TyCoAcc acc -> TyCoAcc acc
 -- Gather the argument free vars in an empty in-scope set
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index 2dec90a6e7..300f177e76 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -1820,11 +1820,15 @@ coercion witnessing the reduction. The reduction will proceed as follows:
     ~> S (S (S (Z + S Z)))     |>              CoAx2 (CoAx2 (CoAx2 Refl))
     ~> S (S (S (S (S Z))))     |>              CoAx1 (CoAx2 (CoAx2 (CoAx2 Refl)))
 
-Moreover, coercions are really only useful when validating core transformations
-(i.e. by the Core Linter). To avoid burdening users who aren't linting with the
-cost of maintaining these structures, we replace coercions with placeholders
-("zap" them) them unless -dcore-lint is enabled. These placeholders are
-represented by UnivCo with ZappedProv provenance. Concretely, a coercion
+This looks linear, but the type arguments to CoAx2 are of size N, N-1
+etc; hence quadratic.
+
+Moreover, coercions are really only useful when validating core
+transformations (i.e. by the Core Linter). To avoid burdening users
+who aren't linting with the cost of maintaining these structures, we
+replace coercions with placeholders ("zap" them) them (under control
+of -ddrop-coercions).  These placeholders are represented by UnivCo
+with ZappedProv provenance. Concretely, a coercion
 
     co :: t1 ~r t2
 
@@ -1975,6 +1979,8 @@ keyword):
    to avoid unsound floating. This means that the free variable lists of zapped
    coercions loaded from interface files will lack top-level things (e.g. type
    constructors) that appear only in the unzapped proof.
+
+* coercionSize gives a smaller size, of course.
 -}
 
 
@@ -2078,6 +2084,7 @@ data TyCoFolder a
           -- See Note [Coercion holes] in "GHC.Core.TyCo.Rep".
 
       , tcf_tycobinder :: TyCoVar -> ArgFlag -> a -> a
+          -- ^ Modify the result of folding over the body of the forall
       }
 
 noView :: Type -> Maybe Type  -- Simplest form of tcf_view
@@ -2108,7 +2115,7 @@ foldTyCo (TyCoFolder { tcf_view       = view
     go_ty (ForAllTy (Bndr tv vis) inner)
       = go_ty (varType tv) `mappend` tycobinder tv vis (go_ty inner)
 
-    -- Explicit recursion becuase using foldr builds a local
+    -- Explicit recursion because using foldr builds a local
     -- loop (with free) and I'm not confident it'll be
     -- lambda lifted in the end
     go_tys []     = mempty
@@ -2148,8 +2155,9 @@ foldTyCo (TyCoFolder { tcf_view       = view
     go_prov (ZapCoProv cvs)     = go_cvs (dVarSetElems cvs)
       -- This use of dVarSetElems does a sort, which seems very
       -- inefficient.  But it seems required for determinism, alas.
-      -- Unless the 'a' is instantiated with a non-deterministic kind
-      -- of thing...could we exploit that somehow?  ToDo.
+      -- Unless the 'a' is instantiated with a commutative monoid,
+      -- such as (VarSet -> VarSet) ...could we exploit that somehow?
+      -- ToDo.
 
     go_cvs []       = mempty
     go_cvs (cv:cvs) = covar cv `mappend` go_cvs cvs