Reform the free variable finders for types

This patch delivers on (much of) #17509.

* Introduces the shallow vs deep free variable distinction

* Introduce TyCoRep.foldType,
    foldType :: Monoid a => TyCoFolder env a
                         -> env -> Type -> a
  and use it in the free variable finders.

* Substitution in TyCoSubst
   * ASSERTs are on for checkValidSubst
   * checkValidSubst uses shallowTyCoVarsOfTypes etc

Quite a few things still to do

* We could use foldType in lots of other places

* We could use mapType for substitution.  (Check that we get
  good code!)

* Some (but not yet all) clients of substitution can now
  save time by using shallowTyCoVarsOfTypes

* All calls to tyCoVarsOfTypes should be inspected; most of
  them should be shallow.  Maybe.

* Currently shallowTyCoVarsOfTypes still returns
  unification variables, but not CoVarHoles.
  Reason: we need to return unification variables
  in some of the calls in TcSimplify, eg when promoting.

* We should do the same thing for tyCoFVsOfTypes, which is
  currently unchanged.

* tyCoFVsOfTypes returns CoVarHoles, because of the
  use in TcSimplify.mkResidualConstraints.  See
  Note [Emitting the residual implication in simplifyInfer]

* #17509 talks about "relevant" variables too.

4 files changed, 543 insertions, 239 deletions

diff --git a/compiler/types/TyCoFVs.hs b/compiler/types/TyCoFVs.hs
index d4a0179f88..e1e3df94ed 100644
--- a/compiler/types/TyCoFVs.hs
+++ b/compiler/types/TyCoFVs.hs
@@ -1,24 +1,35 @@
+{-# LANGUAGE CPP #-}
+
 module TyCoFVs
-  (
-        tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet,
-        exactTyCoVarsOfType, exactTyCoVarsOfTypes,
+  (     shallowTyCoVarsOfType, shallowTyCoVarsOfTypes,
+        tyCoVarsOfType,        tyCoVarsOfTypes,
+        tyCoVarsOfTypeDSet, tyCoVarsOfTypesDSet,
+
         tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs,
         tyCoFVsOfType, tyCoVarsOfTypeList,
         tyCoFVsOfTypes, tyCoVarsOfTypesList,
-        tyCoVarsOfTypesSet, tyCoVarsOfCosSet,
+
+        shallowTyCoVarsOfTyVarEnv, shallowTyCoVarsOfCoVarEnv,
+
+        shallowTyCoVarsOfCo, shallowTyCoVarsOfCos,
+        tyCoVarsOfCo,        tyCoVarsOfCos,
         coVarsOfType, coVarsOfTypes,
         coVarsOfCo, coVarsOfCos,
-        tyCoVarsOfCo, tyCoVarsOfCos,
         tyCoVarsOfCoDSet,
         tyCoFVsOfCo, tyCoFVsOfCos,
-        tyCoVarsOfCoList, tyCoVarsOfProv,
+        tyCoVarsOfCoList,
+
         almostDevoidCoVarOfCo,
+
+        -- Injective free vars
         injectiveVarsOfType, injectiveVarsOfTypes,
         invisibleVarsOfType, invisibleVarsOfTypes,
 
-        noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,
+        -- Exact free vars
+        exactTyCoVarsOfType, exactTyCoVarsOfTypes,
 
-        mkTyCoInScopeSet,
+        -- No Free vars
+        noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,
 
         -- * Well-scoped free variables
         scopedSort, tyCoVarsOfTypeWellScoped,
@@ -30,17 +41,21 @@ module TyCoFVs
 
   ) where
 
+#include "HsVersions.h"
+
 import GhcPrelude
 
-import {-# SOURCE #-} Type (coreView, tcView, partitionInvisibleTypes)
+import {-# SOURCE #-} Type   (coreView, tcView, partitionInvisibleTypes)
 
+-- import Data.Monoid as DM ( Endo(..), All(..) )
+import Data.Monoid as DM ( Endo(..) )
 import TyCoRep
 import TyCon
 import Var
 import FV
 
 import UniqFM
-import UniqSet (nonDetEltsUniqSet)
+import UniqSet( nonDetEltsUniqSet )
 import VarSet
 import VarEnv
 import Util
@@ -176,102 +191,233 @@ So if we're looking at a variable occurrence at all, then all variables in its
 kind are free.
 -}
 
+{- *********************************************************************
+*                                                                      *
+          Endo for free variables
+*                                                                      *
+********************************************************************* -}
+
+{- Note [Acumulating parameter free variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We can use foldType to build an accumulating-parameter version of a
+free-var finder, thus:
+
+    fvs :: Type -> TyCoVarSet
+    fvs ty = appEndo (foldType folder ty) emptyVarSet
+
+Recall that
+    foldType :: TyCoFolder env a -> env -> Type -> a
+
+    newtype Endo a = Endo (a -> a)   -- In Data.Monoid
+    instance Monoid a => Monoid (Endo a) where
+       (Endo f) `mappend` (Endo g) = Endo (f.g)
+
+    appEndo :: Endo a -> a -> a
+    appEndo (Endo f) x = f x
+
+So `mappend` for Endos is just function composition.
+
+It's very important that, after optimisation, we end up
+with an arity-three function, something like this:
+
+   fvs env (TyVarTy v) acc
+      | v `elemVarSet` env = acc
+      | v `elemVarSet` acc = acc
+      | otherwise          = acc `extendVarSet` v
+   fvs env (AppTy t1 t2)   = fvs env t1 (fvs env t2 acc)
+   ...
+
+The optimiser does do this, but not very robustly. It depends
+critially on the basic arity-2 function not being exported, so that
+all its calls are visibly to three arguments. This analysis is
+done by the Call Arity pass.
+-}
+
+runTyCoVars :: Endo TyCoVarSet -> TyCoVarSet
+{-# INLINE runTyCoVars #-}
+runTyCoVars f = appEndo f emptyVarSet
+
+
+{- *********************************************************************
+*                                                                      *
+          Deep free variables
+*                                                                      *
+********************************************************************* -}
+
 tyCoVarsOfType :: Type -> TyCoVarSet
--- See Note [Free variables of types]
-tyCoVarsOfType ty = ty_co_vars_of_type ty emptyVarSet emptyVarSet
+tyCoVarsOfType ty = runTyCoVars (deep_ty ty)
+-- Alternative:
+--   tyCoVarsOfType ty = closeOverKinds (shallowTyCoVarsOfType ty)
 
 tyCoVarsOfTypes :: [Type] -> TyCoVarSet
-tyCoVarsOfTypes tys = ty_co_vars_of_types tys emptyVarSet emptyVarSet
-
-ty_co_vars_of_type :: Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
-ty_co_vars_of_type (TyVarTy v) is acc
-  | v `elemVarSet` is  = acc
-  | v `elemVarSet` acc = acc
-  | otherwise          = ty_co_vars_of_type (tyVarKind v)
-                            emptyVarSet  -- See Note [Closing over free variable kinds]
-                            (extendVarSet acc v)
-
-ty_co_vars_of_type (TyConApp _ tys)   is acc = ty_co_vars_of_types tys is acc
-ty_co_vars_of_type (LitTy {})         _  acc = acc
-ty_co_vars_of_type (AppTy fun arg)    is acc = ty_co_vars_of_type fun is (ty_co_vars_of_type arg is acc)
-ty_co_vars_of_type (FunTy _ arg res)  is acc = ty_co_vars_of_type arg is (ty_co_vars_of_type res is acc)
-ty_co_vars_of_type (ForAllTy (Bndr tv _) ty) is acc = ty_co_vars_of_type (varType tv) is $
-                                                      ty_co_vars_of_type ty (extendVarSet is tv) acc
-ty_co_vars_of_type (CastTy ty co)     is acc = ty_co_vars_of_type ty is (ty_co_vars_of_co co is acc)
-ty_co_vars_of_type (CoercionTy co)    is acc = ty_co_vars_of_co co is acc
-
-ty_co_vars_of_types :: [Type] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
-ty_co_vars_of_types []       _  acc = acc
-ty_co_vars_of_types (ty:tys) is acc = ty_co_vars_of_type ty is (ty_co_vars_of_types tys is acc)
+tyCoVarsOfTypes tys = runTyCoVars (deep_tys tys)
+-- Alternative:
+--   tyCoVarsOfTypes tys = closeOverKinds (shallowTyCoVarsOfTypes tys)
 
 tyCoVarsOfCo :: Coercion -> TyCoVarSet
--- See Note [Free variables of types]
-tyCoVarsOfCo co = ty_co_vars_of_co co emptyVarSet emptyVarSet
+-- See Note [Free variables of Coercions]
+tyCoVarsOfCo co = runTyCoVars (deep_co co)
 
 tyCoVarsOfCos :: [Coercion] -> TyCoVarSet
-tyCoVarsOfCos cos = ty_co_vars_of_cos cos emptyVarSet emptyVarSet
-
-
-ty_co_vars_of_co :: Coercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
-ty_co_vars_of_co (Refl ty)            is acc = ty_co_vars_of_type ty is acc
-ty_co_vars_of_co (GRefl _ ty mco)     is acc = ty_co_vars_of_type ty is $
-                                               ty_co_vars_of_mco mco is acc
-ty_co_vars_of_co (TyConAppCo _ _ cos) is acc = ty_co_vars_of_cos cos is acc
-ty_co_vars_of_co (AppCo co arg)       is acc = ty_co_vars_of_co co is $
-                                               ty_co_vars_of_co arg is acc
-ty_co_vars_of_co (ForAllCo tv kind_co co) is acc = ty_co_vars_of_co kind_co is $
-                                                   ty_co_vars_of_co co (extendVarSet is tv) acc
-ty_co_vars_of_co (FunCo _ co1 co2)    is acc = ty_co_vars_of_co co1 is $
-                                               ty_co_vars_of_co co2 is acc
-ty_co_vars_of_co (CoVarCo v)          is acc = ty_co_vars_of_co_var v is acc
-ty_co_vars_of_co (HoleCo h)           is acc = ty_co_vars_of_co_var (coHoleCoVar h) is acc
-    -- See Note [CoercionHoles and coercion free variables]
-ty_co_vars_of_co (AxiomInstCo _ _ cos) is acc = ty_co_vars_of_cos cos is acc
-ty_co_vars_of_co (UnivCo p _ t1 t2)    is acc = ty_co_vars_of_prov p is $
-                                                ty_co_vars_of_type t1 is $
-                                                ty_co_vars_of_type t2 is acc
-ty_co_vars_of_co (SymCo co)          is acc = ty_co_vars_of_co co is acc
-ty_co_vars_of_co (TransCo co1 co2)   is acc = ty_co_vars_of_co co1 is $
-                                              ty_co_vars_of_co co2 is acc
-ty_co_vars_of_co (NthCo _ _ co)      is acc = ty_co_vars_of_co co is acc
-ty_co_vars_of_co (LRCo _ co)         is acc = ty_co_vars_of_co co is acc
-ty_co_vars_of_co (InstCo co arg)     is acc = ty_co_vars_of_co co is $
-                                              ty_co_vars_of_co arg is acc
-ty_co_vars_of_co (KindCo co)         is acc = ty_co_vars_of_co co is acc
-ty_co_vars_of_co (SubCo co)          is acc = ty_co_vars_of_co co is acc
-ty_co_vars_of_co (AxiomRuleCo _ cs)  is acc = ty_co_vars_of_cos cs is acc
-
-ty_co_vars_of_mco :: MCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
-ty_co_vars_of_mco MRefl    _is acc = acc
-ty_co_vars_of_mco (MCo co) is  acc = ty_co_vars_of_co co is acc
-
-ty_co_vars_of_co_var :: CoVar -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
-ty_co_vars_of_co_var v is acc
-  | v `elemVarSet` is  = acc
-  | v `elemVarSet` acc = acc
-  | otherwise          = ty_co_vars_of_type (varType v)
-                            emptyVarSet  -- See Note [Closing over free variable kinds]
-                            (extendVarSet acc v)
-
-ty_co_vars_of_cos :: [Coercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
-ty_co_vars_of_cos []       _  acc = acc
-ty_co_vars_of_cos (co:cos) is acc = ty_co_vars_of_co co is (ty_co_vars_of_cos cos is acc)
-
-tyCoVarsOfProv :: UnivCoProvenance -> TyCoVarSet
-tyCoVarsOfProv prov = ty_co_vars_of_prov prov emptyVarSet emptyVarSet
-
-ty_co_vars_of_prov :: UnivCoProvenance -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
-ty_co_vars_of_prov (PhantomProv co)    is acc = ty_co_vars_of_co co is acc
-ty_co_vars_of_prov (ProofIrrelProv co) is acc = ty_co_vars_of_co co is acc
-ty_co_vars_of_prov UnsafeCoerceProv    _  acc = acc
-ty_co_vars_of_prov (PluginProv _)      _  acc = acc
-
--- | Generates an in-scope set from the free variables in a list of types
--- and a list of coercions
-mkTyCoInScopeSet :: [Type] -> [Coercion] -> InScopeSet
-mkTyCoInScopeSet tys cos
-  = mkInScopeSet (ty_co_vars_of_types tys emptyVarSet $
-                  ty_co_vars_of_cos   cos emptyVarSet emptyVarSet)
+tyCoVarsOfCos cos = runTyCoVars (deep_cos cos)
+
+deep_ty  :: Type -> Endo TyCoVarSet
+deep_tys :: [Type] -> Endo TyCoVarSet
+deep_co  :: Coercion -> Endo TyCoVarSet
+deep_cos :: [Coercion] -> Endo TyCoVarSet
+(deep_ty, deep_tys, deep_co, deep_cos) = foldTyCo deepTcvFolder emptyVarSet
+
+deepTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
+deepTcvFolder = TyCoFolder { tcf_tyvar = do_tcv, tcf_covar = do_tcv
+                           , tcf_hole  = do_hole, tcf_tycobinder = do_bndr }
+  where
+    do_tcv is v = Endo do_it
+      where
+        do_it acc | v `elemVarSet` is  = acc
+                  | v `elemVarSet` acc = acc
+                  | otherwise          = appEndo (deep_ty (varType v)) $
+                                         acc `extendVarSet` v
+
+    do_bndr is tcv _ = extendVarSet is tcv
+    do_hole is hole  = do_tcv is (coHoleCoVar hole)
+                       -- See Note [CoercionHoles and coercion free variables]
+                       -- in TyCoRep
+
+{- *********************************************************************
+*                                                                      *
+          Shallow free variables
+*                                                                      *
+********************************************************************* -}
+
+shallowTyCoVarsOfType :: Type -> TyCoVarSet
+-- See Note [Free variables of types]
+shallowTyCoVarsOfType ty = runTyCoVars (shallow_ty ty)
+
+shallowTyCoVarsOfTypes :: [Type] -> TyCoVarSet
+shallowTyCoVarsOfTypes tys = runTyCoVars (shallow_tys tys)
+
+shallowTyCoVarsOfCo :: Coercion -> TyCoVarSet
+shallowTyCoVarsOfCo co = runTyCoVars (shallow_co co)
+
+shallowTyCoVarsOfCos :: [Coercion] -> TyCoVarSet
+shallowTyCoVarsOfCos cos = runTyCoVars (shallow_cos cos)
+
+-- | Returns free variables of types, including kind variables as
+-- a non-deterministic set. For type synonyms it does /not/ expand the
+-- synonym.
+shallowTyCoVarsOfTyVarEnv :: TyVarEnv Type -> TyCoVarSet
+-- See Note [Free variables of types]
+shallowTyCoVarsOfTyVarEnv tys = shallowTyCoVarsOfTypes (nonDetEltsUFM tys)
+  -- It's OK to use nonDetEltsUFM here because we immediately
+  -- forget the ordering by returning a set
+
+shallowTyCoVarsOfCoVarEnv :: CoVarEnv Coercion -> TyCoVarSet
+shallowTyCoVarsOfCoVarEnv cos = shallowTyCoVarsOfCos (nonDetEltsUFM cos)
+  -- It's OK to use nonDetEltsUFM here because we immediately
+  -- forget the ordering by returning a set
+
+shallow_ty  :: Type -> Endo TyCoVarSet
+shallow_tys :: [Type] -> Endo TyCoVarSet
+shallow_co  :: Coercion -> Endo TyCoVarSet
+shallow_cos :: [Coercion] -> Endo TyCoVarSet
+(shallow_ty, shallow_tys, shallow_co, shallow_cos) = foldTyCo shallowTcvFolder emptyVarSet
+
+shallowTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
+shallowTcvFolder = TyCoFolder { tcf_tyvar = do_tcv, tcf_covar = do_tcv
+                              , tcf_hole  = do_hole, tcf_tycobinder = do_bndr }
+  where
+    do_tcv is v = Endo do_it
+      where
+        do_it acc | v `elemVarSet` is  = acc
+                  | v `elemVarSet` acc = acc
+                  | otherwise          = acc `extendVarSet` v
+
+    do_bndr is tcv _ = extendVarSet is tcv
+    do_hole _ _  = mempty   -- Ignore coercion holes
+
+
+{- *********************************************************************
+*                                                                      *
+          Closing over kinds
+*                                                                      *
+********************************************************************* -}
+
+------------- Closing over kinds -----------------
+
+closeOverKinds :: TyVarSet -> TyVarSet
+closeOverKinds = fvVarSet . closeOverKindsFV . nonDetEltsUniqSet
+
+{- ---------------- Alternative version 1 (preferred) -------------
+
+-- | Add the kind variables free in the kinds of the tyvars in the given set.
+-- Returns a non-deterministic set.
+closeOverKinds :: TyCoVarSet -> TyCoVarSet
+closeOverKinds vs
+   = go vs vs
+  where
+    go :: VarSet   -- Work list
+       -> VarSet   -- Accumulator, always a superset of wl
+       -> VarSet
+    go wl acc
+      | isEmptyVarSet wl = acc
+      | otherwise        = go wl_kvs (acc `unionVarSet` wl_kvs)
+      where
+        k v inner_acc = ty_co_vars_of_type (varType v) acc inner_acc
+        wl_kvs = nonDetFoldVarSet k emptyVarSet wl
+        -- wl_kvs = union of shallow free vars of the kinds of wl
+        --          but don't bother to collect vars in acc
+
+-}
+
+{- ---------------- Alternative version -------------
+-- | Add the kind variables free in the kinds of the tyvars in the given set.
+-- Returns a non-deterministic set.
+closeOverKinds :: TyVarSet -> TyVarSet
+closeOverKinds vs = close_over_kinds vs emptyVarSet
+
+
+close_over_kinds :: TyVarSet  -- Work list
+                 -> TyVarSet  -- Accumulator
+                 -> TyVarSet
+-- Precondition: in any call (close_over_kinds wl acc)
+--  for every tv in acc, the shallow kind-vars of tv
+--  are either in the work list wl, or in acc
+-- Postcondition: result is the deep free vars of (wl `union` acc)
+close_over_kinds wl acc
+  = nonDetFoldVarSet do_one acc wl
+  where
+    do_one :: Var -> TyVarSet -> TyVarSet
+    -- (do_one v acc) adds v and its deep free-vars to acc
+    do_one v acc | v `elemVarSet` acc
+                 = acc
+                 | otherwise
+                 = close_over_kinds (shallowTyCoVarsOfType (varType v)) $
+                   acc `extendVarSet` v
+-}
+
+
+{- *********************************************************************
+*                                                                      *
+          The FV versions return deterministic results
+*                                                                      *
+********************************************************************* -}
+
+-- | Given a list of tyvars returns a deterministic FV computation that
+-- returns the given tyvars with the kind variables free in the kinds of the
+-- given tyvars.
+closeOverKindsFV :: [TyVar] -> FV
+closeOverKindsFV tvs =
+  mapUnionFV (tyCoFVsOfType . tyVarKind) tvs `unionFV` mkFVs tvs
+
+-- | Add the kind variables free in the kinds of the tyvars in the given set.
+-- Returns a deterministically ordered list.
+closeOverKindsList :: [TyVar] -> [TyVar]
+closeOverKindsList tvs = fvVarList $ closeOverKindsFV tvs
+
+-- | Add the kind variables free in the kinds of the tyvars in the given set.
+-- Returns a deterministic set.
+closeOverKindsDSet :: DTyVarSet -> DTyVarSet
+closeOverKindsDSet = fvDVarSet . closeOverKindsFV . dVarSetElems
 
 -- | `tyCoFVsOfType` that returns free variables of a type in a deterministic
 -- set. For explanation of why using `VarSet` is not deterministic see
@@ -288,15 +434,6 @@ tyCoVarsOfTypeList :: Type -> [TyCoVar]
 tyCoVarsOfTypeList ty = fvVarList $ tyCoFVsOfType ty
 
 -- | Returns free variables of types, including kind variables as
--- a non-deterministic set. For type synonyms it does /not/ expand the
--- synonym.
-tyCoVarsOfTypesSet :: TyVarEnv Type -> TyCoVarSet
--- See Note [Free variables of types]
-tyCoVarsOfTypesSet tys = tyCoVarsOfTypes $ nonDetEltsUFM tys
-  -- It's OK to use nonDetEltsUFM here because we immediately forget the
-  -- ordering by returning a set
-
--- | Returns free variables of types, including kind variables as
 -- a deterministic set. For type synonyms it does /not/ expand the
 -- synonym.
 tyCoVarsOfTypesDSet :: [Type] -> DTyCoVarSet
@@ -310,75 +447,6 @@ tyCoVarsOfTypesList :: [Type] -> [TyCoVar]
 -- See Note [Free variables of types]
 tyCoVarsOfTypesList tys = fvVarList $ tyCoFVsOfTypes tys
 
-{-
-************************************************************************
-*                                                                      *
-          The "exact" free variables of a type
-*                                                                      *
-************************************************************************
-
-Note [Silly type synonym]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-  type T a = Int
-What are the free tyvars of (T x)?  Empty, of course!
-
-exactTyCoVarsOfType is used by the type checker to figure out exactly
-which type variables are mentioned in a type.  It only matters
-occasionally -- see the calls to exactTyCoVarsOfType.
--}
-
-exactTyCoVarsOfType :: Type -> TyCoVarSet
--- Find the free type variables (of any kind)
--- but *expand* type synonyms.  See Note [Silly type synonym] above.
-exactTyCoVarsOfType ty
-  = go ty
-  where
-    go ty | Just ty' <- tcView ty = go ty'  -- This is the key line
-    go (TyVarTy tv)         = goVar tv
-    go (TyConApp _ tys)     = exactTyCoVarsOfTypes tys
-    go (LitTy {})           = emptyVarSet
-    go (AppTy fun arg)      = go fun `unionVarSet` go arg
-    go (FunTy _ arg res)    = go arg `unionVarSet` go res
-    go (ForAllTy bndr ty)   = delBinderVar (go ty) bndr `unionVarSet` go (binderType bndr)
-    go (CastTy ty co)       = go ty `unionVarSet` goCo co
-    go (CoercionTy co)      = goCo co
-
-    goMCo MRefl    = emptyVarSet
-    goMCo (MCo co) = goCo co
-
-    goCo (Refl ty)            = go ty
-    goCo (GRefl _ ty mco)     = go ty `unionVarSet` goMCo mco
-    goCo (TyConAppCo _ _ args)= goCos args
-    goCo (AppCo co arg)     = goCo co `unionVarSet` goCo arg
-    goCo (ForAllCo tv k_co co)
-      = goCo co `delVarSet` tv `unionVarSet` goCo k_co
-    goCo (FunCo _ co1 co2)   = goCo co1 `unionVarSet` goCo co2
-    goCo (CoVarCo v)         = goVar v
-    goCo (HoleCo h)          = goVar (coHoleCoVar h)
-    goCo (AxiomInstCo _ _ args) = goCos args
-    goCo (UnivCo p _ t1 t2)  = goProv p `unionVarSet` go t1 `unionVarSet` go t2
-    goCo (SymCo co)          = goCo co
-    goCo (TransCo co1 co2)   = goCo co1 `unionVarSet` goCo co2
-    goCo (NthCo _ _ co)      = goCo co
-    goCo (LRCo _ co)         = goCo co
-    goCo (InstCo co arg)     = goCo co `unionVarSet` goCo arg
-    goCo (KindCo co)         = goCo co
-    goCo (SubCo co)          = goCo co
-    goCo (AxiomRuleCo _ c)   = goCos c
-
-    goCos cos = foldr (unionVarSet . goCo) emptyVarSet cos
-
-    goProv UnsafeCoerceProv     = emptyVarSet
-    goProv (PhantomProv kco)    = goCo kco
-    goProv (ProofIrrelProv kco) = goCo kco
-    goProv (PluginProv _)       = emptyVarSet
-
-    goVar v = unitVarSet v `unionVarSet` go (varType v)
-
-exactTyCoVarsOfTypes :: [Type] -> TyVarSet
-exactTyCoVarsOfTypes tys = mapUnionVarSet exactTyCoVarsOfType tys
-
 -- | The worker for `tyCoFVsOfType` and `tyCoFVsOfTypeList`.
 -- The previous implementation used `unionVarSet` which is O(n+m) and can
 -- make the function quadratic.
@@ -435,11 +503,6 @@ tyCoFVsOfMCo :: MCoercion -> FV
 tyCoFVsOfMCo MRefl    = emptyFV
 tyCoFVsOfMCo (MCo co) = tyCoFVsOfCo co
 
-tyCoVarsOfCosSet :: CoVarEnv Coercion -> TyCoVarSet
-tyCoVarsOfCosSet cos = tyCoVarsOfCos $ nonDetEltsUFM cos
-  -- It's OK to use nonDetEltsUFM here because we immediately forget the
-  -- ordering by returning a set
-
 tyCoFVsOfCo :: Coercion -> FV
 -- Extracts type and coercion variables from a coercion
 -- See Note [Free variables of types]
@@ -489,11 +552,8 @@ tyCoFVsOfCos (co:cos) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOf
 
 ------------- Extracting the CoVars of a type or coercion -----------
 
-{-
-
-Note [CoVarsOfX and the InterestingVarFun]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
+{- Note [CoVarsOfX and the InterestingVarFun]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The coVarsOfType, coVarsOfTypes, coVarsOfCo, and coVarsOfCos functions are
 implemented in terms of the respective FV equivalents (tyCoFVsOf...), rather
 than the VarSet-based flavors (tyCoVarsOf...), despite the performance
@@ -613,7 +673,82 @@ almost_devoid_co_var_of_types (ty:tys) cv
   = almost_devoid_co_var_of_type ty cv
   && almost_devoid_co_var_of_types tys cv
 
-------------- Injective free vars -----------------
+
+
+{- *********************************************************************
+*                                                                      *
+          The "exact" free variables of a type
+*                                                                      *
+********************************************************************* -}
+
+{- Note [Silly type synonym]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  type T a = Int
+What are the free tyvars of (T x)?  Empty, of course!
+
+exactTyCoVarsOfType is used by the type checker to figure out exactly
+which type variables are mentioned in a type.  It only matters
+occasionally -- see the calls to exactTyCoVarsOfType.
+-}
+
+exactTyCoVarsOfType :: Type -> TyCoVarSet
+-- Find the free type variables (of any kind)
+-- but *expand* type synonyms.  See Note [Silly type synonym] above.
+exactTyCoVarsOfType ty
+  = go ty
+  where
+    go ty | Just ty' <- tcView ty = go ty'  -- This is the key line
+    go (TyVarTy tv)         = goVar tv
+    go (TyConApp _ tys)     = exactTyCoVarsOfTypes tys
+    go (LitTy {})           = emptyVarSet
+    go (AppTy fun arg)      = go fun `unionVarSet` go arg
+    go (FunTy _ arg res)    = go arg `unionVarSet` go res
+    go (ForAllTy bndr ty)   = delBinderVar (go ty) bndr `unionVarSet` go (binderType bndr)
+    go (CastTy ty co)       = go ty `unionVarSet` goCo co
+    go (CoercionTy co)      = goCo co
+
+    goMCo MRefl    = emptyVarSet
+    goMCo (MCo co) = goCo co
+
+    goCo (Refl ty)            = go ty
+    goCo (GRefl _ ty mco)     = go ty `unionVarSet` goMCo mco
+    goCo (TyConAppCo _ _ args)= goCos args
+    goCo (AppCo co arg)     = goCo co `unionVarSet` goCo arg
+    goCo (ForAllCo tv k_co co)
+      = goCo co `delVarSet` tv `unionVarSet` goCo k_co
+    goCo (FunCo _ co1 co2)   = goCo co1 `unionVarSet` goCo co2
+    goCo (CoVarCo v)         = goVar v
+    goCo (HoleCo h)          = goVar (coHoleCoVar h)
+    goCo (AxiomInstCo _ _ args) = goCos args
+    goCo (UnivCo p _ t1 t2)  = goProv p `unionVarSet` go t1 `unionVarSet` go t2
+    goCo (SymCo co)          = goCo co
+    goCo (TransCo co1 co2)   = goCo co1 `unionVarSet` goCo co2
+    goCo (NthCo _ _ co)      = goCo co
+    goCo (LRCo _ co)         = goCo co
+    goCo (InstCo co arg)     = goCo co `unionVarSet` goCo arg
+    goCo (KindCo co)         = goCo co
+    goCo (SubCo co)          = goCo co
+    goCo (AxiomRuleCo _ c)   = goCos c
+
+    goCos cos = foldr (unionVarSet . goCo) emptyVarSet cos
+
+    goProv UnsafeCoerceProv     = emptyVarSet
+    goProv (PhantomProv kco)    = goCo kco
+    goProv (ProofIrrelProv kco) = goCo kco
+    goProv (PluginProv _)       = emptyVarSet
+
+    goVar v = unitVarSet v `unionVarSet` go (varType v)
+
+exactTyCoVarsOfTypes :: [Type] -> TyVarSet
+exactTyCoVarsOfTypes tys = mapUnionVarSet exactTyCoVarsOfType tys
+
+
+{- *********************************************************************
+*                                                                      *
+                 Injective free vars
+*                                                                      *
+********************************************************************* -}
 
 -- | Returns the free variables of a 'Type' that are in injective positions.
 -- Specifically, it finds the free variables while:
@@ -681,7 +816,13 @@ injectiveVarsOfTypes :: Bool -- ^ look under injective type families?
 injectiveVarsOfTypes look_under_tfs = mapUnionFV (injectiveVarsOfType look_under_tfs)
 
 
-------------- Invisible vars -----------------
+{- *********************************************************************
+*                                                                      *
+                 Invisible vars
+*                                                                      *
+********************************************************************* -}
+
+
 -- | Returns the set of variables that are used invisibly anywhere within
 -- the given type. A variable will be included even if it is used both visibly
 -- and invisibly. An invisible use site includes:
@@ -711,7 +852,31 @@ invisibleVarsOfTypes :: [Type] -> FV
 invisibleVarsOfTypes = mapUnionFV invisibleVarsOfType
 
 
-------------- No free vars -----------------
+{- *********************************************************************
+*                                                                      *
+                 No free vars
+*                                                                      *
+********************************************************************* -}
+
+{-   Desired!
+
+nfvFolder :: TyCoFolder TyCoVarSet DM.All
+nfvFolder = TyCoFolder { tcf_tyvar = do_tcv, tcf_covar = do_tcv
+                       , tcf_hole = do_hole, tcf_tycobinder = do_bndr }
+  where
+    do_tcv is tv = All (tv `elemVarSet` is)
+    do_hole _ _  = All True    -- I'm unsure; probably never happens
+    do_bndr is tv _ = is `extendVarSet` tv
+
+noFreeVarsOfType :: Type -> Bool
+noFreeVarsOfType = DM.getAll . foldType nfvFolder emptyVarSet
+
+noFreeVarsOfTypes :: [Type] -> Bool
+noFreeVarsOfTypes = DM.getAll . foldTypes nfvFolder emptyVarSet
+
+noFreeVarsOfCo :: Coercion -> Bool
+noFreeVarsOfCo = getAll . foldCoercion nfvFolder emptyVarSet
+-}
 
 -- | Returns True if this type has no free variables. Should be the same as
 -- isEmptyVarSet . tyCoVarsOfType, but faster in the non-forall case.
@@ -764,15 +929,14 @@ noFreeVarsOfProv (PhantomProv co)    = noFreeVarsOfCo co
 noFreeVarsOfProv (ProofIrrelProv co) = noFreeVarsOfCo co
 noFreeVarsOfProv (PluginProv {})     = True
 
-{-
-%************************************************************************
-%*                                                                      *
-         Well-scoped tyvars
+{- *********************************************************************
 *                                                                      *
-************************************************************************
+                 scopedSort
+*                                                                      *
+********************************************************************* -}
 
-Note [ScopedSort]
-~~~~~~~~~~~~~~~~~
+{- Note [ScopedSort]
+~~~~~~~~~~~~~~~~~~~~
 Consider
 
   foo :: Proxy a -> Proxy (b :: k) -> Proxy (a :: k2) -> ()
@@ -866,28 +1030,3 @@ tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList
 tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
 tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList
 
-------------- Closing over kinds -----------------
-
--- | Add the kind variables free in the kinds of the tyvars in the given set.
--- Returns a non-deterministic set.
-closeOverKinds :: TyVarSet -> TyVarSet
-closeOverKinds = fvVarSet . closeOverKindsFV . nonDetEltsUniqSet
-  -- It's OK to use nonDetEltsUniqSet here because we immediately forget
-  -- about the ordering by returning a set.
-
--- | Given a list of tyvars returns a deterministic FV computation that
--- returns the given tyvars with the kind variables free in the kinds of the
--- given tyvars.
-closeOverKindsFV :: [TyVar] -> FV
-closeOverKindsFV tvs =
-  mapUnionFV (tyCoFVsOfType . tyVarKind) tvs `unionFV` mkFVs tvs
-
--- | Add the kind variables free in the kinds of the tyvars in the given set.
--- Returns a deterministically ordered list.
-closeOverKindsList :: [TyVar] -> [TyVar]
-closeOverKindsList tvs = fvVarList $ closeOverKindsFV tvs
-
--- | Add the kind variables free in the kinds of the tyvars in the given set.
--- Returns a deterministic set.
-closeOverKindsDSet :: DTyVarSet -> DTyVarSet
-closeOverKindsDSet = fvDVarSet . closeOverKindsFV . dVarSetElems
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index f55141d928..59ccc8f884 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -61,6 +61,9 @@ module TyCoRep (
         -- * Functions over coercions
         pickLR,
 
+        -- ** Analyzing types
+        TyCoFolder(..), foldTyCo,
+
         -- * Sizes
         typeSize, coercionSize, provSize
     ) where
@@ -1635,6 +1638,165 @@ Here,
 
 {- *********************************************************************
 *                                                                      *
+                foldType  and   foldCoercion
+*                                                                      *
+********************************************************************* -}
+
+{- Note [foldType]
+~~~~~~~~~~~~~~~~~~
+foldType is a bit more powerful than perhaps it looks:
+
+* You can fold with an accumulating parameter, via
+     TyCoFolder env (Endo a)
+  Recall newtype Endo a = Endo (a->a)
+
+* You can fold monadically with a monad M, via
+     TyCoFolder env (M a)
+  provided you have
+     instance ..  => Monoid (M a)
+
+Note [mapType vs foldType]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+We define foldType here, but mapType in module Type. Why?
+
+* foldType is used in TyCoFVs for finding free variables.
+  It's a very simple function that analyses a type,
+  but does not construct one.
+
+* mapType constructs new types, and so it needs to call
+  the "smart constructors", mkAppTy, mkCastTy, and so on.
+  These are sophisticated functions, and can't be defined
+  here in TyCoRep.
+
+Note [Specialising foldType]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We inline foldType at every call site (there are not many), so that it
+becomes specialised for the particular monoid *and* TyCoFolder at
+that site.  This is just for efficiency, but walking over types is
+done a *lot* in GHC, so worth optimising.
+
+We were worried that
+    TyCoFolder env (Endo a)
+might not eta-expand.  Recall newtype Endo a = Endo (a->a).
+
+In particular, given
+   fvs :: Type -> TyCoVarSet
+   fvs ty = appEndo (foldType tcf emptyVarSet ty) emptyVarSet
+
+   tcf :: TyCoFolder enf (Endo a)
+   tcf = TyCoFolder { tcf_tyvar = do_tv, ... }
+      where
+        do_tvs is tv = Endo do_it
+           where
+             do_it acc | tv `elemVarSet` is  = acc
+                       | tv `elemVarSet` acc = acc
+                       | otherwise = acc `extendVarSet` tv
+
+
+we want to end up with
+   fvs ty = go emptyVarSet ty emptyVarSet
+     where
+       go env (TyVarTy tv) acc = acc `extendVarSet` tv
+       ..etc..
+
+And indeed this happens.
+  - Selections from 'tcf' are done at compile time
+  - 'go' is nicely eta-expanded.
+
+We were also worried about
+   deep_fvs :: Type -> TyCoVarSet
+   deep_fvs ty = appEndo (foldType deep_tcf emptyVarSet ty) emptyVarSet
+
+   deep_tcf :: TyCoFolder enf (Endo a)
+   deep_tcf = TyCoFolder { tcf_tyvar = do_tv, ... }
+      where
+        do_tvs is tv = Endo do_it
+           where
+             do_it acc | tv `elemVarSet` is  = acc
+                       | tv `elemVarSet` acc = acc
+                       | otherwise = deep_fvs (varType tv)
+                                     `unionVarSet` acc
+                                     `extendVarSet` tv
+
+Here deep_fvs and deep_tcf are mutually recursive, unlike fvs and tcf.
+But, amazingly, we get good code here too. GHC is careful not to makr
+TyCoFolder data constructor for deep_tcf as a loop breaker, so the
+record selections still cancel.  And eta expansion still happens too.
+-}
+
+data TyCoFolder env a
+  = TyCoFolder
+      { tcf_tyvar :: env -> TyVar -> a
+      , tcf_covar :: env -> CoVar -> a
+      , tcf_hole  :: env -> CoercionHole -> a
+          -- ^ What to do with coercion holes.
+          -- See Note [Coercion holes] in TyCoRep.
+
+      , tcf_tycobinder :: env -> TyCoVar -> ArgFlag -> env
+          -- ^ The returned env is used in the extended scope
+      }
+
+{-# INLINE foldTyCo  #-}  -- See Note [Specialising foldType]
+foldTyCo :: Monoid a => TyCoFolder env a -> env
+         -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
+foldTyCo (TyCoFolder { tcf_tyvar      = tyvar
+                      , tcf_tycobinder = tycobinder
+                      , tcf_covar      = covar
+                      , tcf_hole       = cohole }) env
+  = (go_ty env, go_tys env, go_co env, go_cos env)
+  where
+    go_ty env (TyVarTy tv)      = tyvar env tv
+    go_ty env (AppTy t1 t2)     = go_ty env t1 `mappend` go_ty env t2
+    go_ty _   (LitTy {})        = mempty
+    go_ty env (CastTy ty co)    = go_ty env ty `mappend` go_co env co
+    go_ty env (CoercionTy co)   = go_co env co
+    go_ty env (FunTy _ arg res) = go_ty env arg `mappend` go_ty env res
+    go_ty env (TyConApp _ tys)  = go_tys env tys
+    go_ty env (ForAllTy (Bndr tv vis) inner)
+      = let env' = tycobinder env tv vis
+        in go_ty env (varType tv) `mappend` go_ty env' inner
+
+    -- Explicit recursion becuase using foldr builds a local
+    -- loop (with env free) and I'm not confident it'll be
+    -- lambda lifted in the end
+    go_tys _   []     = mempty
+    go_tys env (t:ts) = go_ty env t `mappend` go_tys env ts
+
+    go_cos _   []     = mempty
+    go_cos env (c:cs) = go_co env c `mappend` go_cos env cs
+
+    go_co env (Refl ty)               = go_ty env ty
+    go_co env (GRefl _ ty MRefl)      = go_ty env ty
+    go_co env (GRefl _ ty (MCo co))   = go_ty env ty `mappend` go_co env co
+    go_co env (TyConAppCo _ _ args)   = go_cos env args
+    go_co env (AppCo c1 c2)           = go_co env c1 `mappend` go_co env c2
+    go_co env (FunCo _ c1 c2)         = go_co env c1 `mappend` go_co env c2
+    go_co env (CoVarCo cv)            = covar env cv
+    go_co env (AxiomInstCo _ _ args)  = go_cos env args
+    go_co env (HoleCo hole)           = cohole env hole
+    go_co env (UnivCo p _ t1 t2)      = go_prov env p `mappend` go_ty env t1
+                                                      `mappend` go_ty env t2
+    go_co env (SymCo co)              = go_co env co
+    go_co env (TransCo c1 c2)         = go_co env c1 `mappend` go_co env c2
+    go_co env (AxiomRuleCo _ cos)     = go_cos env cos
+    go_co env (NthCo _ _ co)          = go_co env co
+    go_co env (LRCo _ co)             = go_co env co
+    go_co env (InstCo co arg)         = go_co env co `mappend` go_co env arg
+    go_co env (KindCo co)             = go_co env co
+    go_co env (SubCo co)              = go_co env co
+    go_co env (ForAllCo tv kind_co co)
+      = go_co env kind_co `mappend` go_ty env (varType tv)
+                          `mappend` go_co env' co
+      where
+        env' = tycobinder env tv Inferred
+
+    go_prov env (PhantomProv co)    = go_co env co
+    go_prov env (ProofIrrelProv co) = go_co env co
+    go_prov _   UnsafeCoerceProv    = mempty
+    go_prov _   (PluginProv _)      = mempty
+
+{- *********************************************************************
+*                                                                      *
                    typeSize, coercionSize
 *                                                                      *
 ********************************************************************* -}
diff --git a/compiler/types/TyCoSubst.hs b/compiler/types/TyCoSubst.hs
index 27e2ab9f77..0d676ed5fa 100644
--- a/compiler/types/TyCoSubst.hs
+++ b/compiler/types/TyCoSubst.hs
@@ -26,7 +26,7 @@ module TyCoSubst
         extendTvSubst, extendTvSubstBinderAndInScope, extendTvSubstWithClone,
         extendTvSubstList, extendTvSubstAndInScope,
         extendTCvSubstList,
-        unionTCvSubst, zipTyEnv, zipCoEnv, mkTyCoInScopeSet,
+        unionTCvSubst, zipTyEnv, zipCoEnv,
         zipTvSubst, zipCvSubst,
         zipTCvSubst,
         mkTvSubstPrs,
@@ -283,8 +283,8 @@ getTCvSubstRangeFVs :: TCvSubst -> VarSet
 getTCvSubstRangeFVs (TCvSubst _ tenv cenv)
     = unionVarSet tenvFVs cenvFVs
   where
-    tenvFVs = tyCoVarsOfTypesSet tenv
-    cenvFVs = tyCoVarsOfCosSet cenv
+    tenvFVs = shallowTyCoVarsOfTyVarEnv tenv
+    cenvFVs = shallowTyCoVarsOfCoVarEnv cenv
 
 isInScope :: Var -> TCvSubst -> Bool
 isInScope v (TCvSubst in_scope _ _) = v `elemInScopeSet` in_scope
@@ -395,7 +395,7 @@ unionTCvSubst (TCvSubst in_scope1 tenv1 cenv1) (TCvSubst in_scope2 tenv2 cenv2)
 -- environment. No CoVars, please!
 zipTvSubst :: HasDebugCallStack => [TyVar] -> [Type] -> TCvSubst
 zipTvSubst tvs tys
-  = mkTvSubst (mkInScopeSet (tyCoVarsOfTypes tys)) tenv
+  = mkTvSubst (mkInScopeSet (shallowTyCoVarsOfTypes tys)) tenv
   where
     tenv = zipTyEnv tvs tys
 
@@ -403,13 +403,14 @@ zipTvSubst tvs tys
 -- environment.  No TyVars, please!
 zipCvSubst :: HasDebugCallStack => [CoVar] -> [Coercion] -> TCvSubst
 zipCvSubst cvs cos
-  = TCvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv cenv
+  = TCvSubst (mkInScopeSet (shallowTyCoVarsOfCos cos)) emptyTvSubstEnv cenv
   where
     cenv = zipCoEnv cvs cos
 
 zipTCvSubst :: HasDebugCallStack => [TyCoVar] -> [Type] -> TCvSubst
 zipTCvSubst tcvs tys
-  = zip_tcvsubst tcvs tys (mkEmptyTCvSubst $ mkInScopeSet (tyCoVarsOfTypes tys))
+  = zip_tcvsubst tcvs tys $
+    mkEmptyTCvSubst $ mkInScopeSet $ shallowTyCoVarsOfTypes tys
   where zip_tcvsubst :: [TyCoVar] -> [Type] -> TCvSubst -> TCvSubst
         zip_tcvsubst (tv:tvs) (ty:tys) subst
           = zip_tcvsubst tvs tys (extendTCvSubst subst tv ty)
@@ -424,7 +425,7 @@ mkTvSubstPrs prs =
     ASSERT2( onlyTyVarsAndNoCoercionTy, text "prs" <+> ppr prs )
     mkTvSubst in_scope tenv
   where tenv = mkVarEnv prs
-        in_scope = mkInScopeSet $ tyCoVarsOfTypes $ map snd prs
+        in_scope = mkInScopeSet $ shallowTyCoVarsOfTypes $ map snd prs
         onlyTyVarsAndNoCoercionTy =
           and [ isTyVar tv && not (isCoercionTy ty)
               | (tv, ty) <- prs ]
@@ -618,8 +619,8 @@ isValidTCvSubst (TCvSubst in_scope tenv cenv) =
   (tenvFVs `varSetInScope` in_scope) &&
   (cenvFVs `varSetInScope` in_scope)
   where
-  tenvFVs = tyCoVarsOfTypesSet tenv
-  cenvFVs = tyCoVarsOfCosSet cenv
+  tenvFVs = shallowTyCoVarsOfTyVarEnv tenv
+  cenvFVs = shallowTyCoVarsOfCoVarEnv cenv
 
 -- | This checks if the substitution satisfies the invariant from
 -- Note [The substitution invariant].
@@ -628,9 +629,9 @@ checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a
   = ASSERT2( isValidTCvSubst subst,
              text "in_scope" <+> ppr in_scope $$
              text "tenv" <+> ppr tenv $$
-             text "tenvFVs" <+> ppr (tyCoVarsOfTypesSet tenv) $$
+             text "tenvFVs" <+> ppr (shallowTyCoVarsOfTyVarEnv tenv) $$
              text "cenv" <+> ppr cenv $$
-             text "cenvFVs" <+> ppr (tyCoVarsOfCosSet cenv) $$
+             text "cenvFVs" <+> ppr (shallowTyCoVarsOfCoVarEnv cenv) $$
              text "tys" <+> ppr tys $$
              text "cos" <+> ppr cos )
     ASSERT2( tysCosFVsInScope,
@@ -645,8 +646,9 @@ checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a
   substDomain = nonDetKeysUFM tenv ++ nonDetKeysUFM cenv
     -- It's OK to use nonDetKeysUFM here, because we only use this list to
     -- remove some elements from a set
-  needInScope = (tyCoVarsOfTypes tys `unionVarSet` tyCoVarsOfCos cos)
-                  `delListFromUniqSet_Directly` substDomain
+  needInScope = (shallowTyCoVarsOfTypes tys `unionVarSet`
+                 shallowTyCoVarsOfCos cos)
+                `delListFromUniqSet_Directly` substDomain
   tysCosFVsInScope = needInScope `varSetInScope` in_scope
 
 
@@ -958,7 +960,7 @@ substTyVarBndrUsing subst_fn subst@(TCvSubst in_scope tenv cenv) old_var
     new_env | no_change = delVarEnv tenv old_var
             | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
 
-    _no_capture = not (new_var `elemVarSet` tyCoVarsOfTypesSet tenv)
+    _no_capture = not (new_var `elemVarSet` shallowTyCoVarsOfTyVarEnv tenv)
     -- Assertion check that we are not capturing something in the substitution
 
     old_ki = tyVarKind old_var
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index e5859b2f4b..3d2b90c2ed 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -82,6 +82,7 @@ module Type (
 
         -- ** Analyzing types
         TyCoMapper(..), mapType, mapCoercion,
+        TyCoFolder(..), foldTyCo,
 
         -- (Newtypes)
         newTyConInstRhs,
@@ -552,10 +553,9 @@ isRuntimeRepVar :: TyVar -> Bool
 isRuntimeRepVar = isRuntimeRepTy . tyVarKind
 
 
-{-
-************************************************************************
+{- *********************************************************************
 *                                                                      *
-   Analyzing types
+               mapType
 *                                                                      *
 ************************************************************************
 
@@ -696,6 +696,7 @@ mapCoercion mapper@(TyCoMapper { tcm_covar = covar
     go_prov (ProofIrrelProv co) = ProofIrrelProv <$> go co
     go_prov p@(PluginProv _)    = return p
 
+
 {-
 ************************************************************************
 *                                                                      *