Make the specialiser handle polymorphic specialisation

Ticket #13873 unexpectedly showed that a SPECIALISE pragma made a
program run (a lot) slower, because less specialisation took place
overall. It turned out that the specialiser was missing opportunities
because of quantified type variables.

It was quite easy to fix. The story is given in
    Note [Specialising polymorphic dictionaries]

Two other minor fixes in the specialiser

* There is no benefit in specialising data constructor /wrappers/.
  (They can appear overloaded because they are given a dictionary
  to store in the constructor.)  Small guard in canSpecImport.

* There was a buglet in the UnspecArg case of specHeader, in the
  case where there is a dead binder. We need a LitRubbish filler
  for the specUnfolding stuff.  I expanded
  Note [Drop dead args from specialisations] to explain.

There is a 4% increase in compile time for T15164, because we generate
more specialised code.  This seems OK.

Metric Increase:
    T15164

7 files changed, 419 insertions, 76 deletions

diff --git a/compiler/GHC/Core/Opt/Simplify/Env.hs b/compiler/GHC/Core/Opt/Simplify/Env.hs
index 26dda50d4f..400c3e60d5 100644
--- a/compiler/GHC/Core/Opt/Simplify/Env.hs
+++ b/compiler/GHC/Core/Opt/Simplify/Env.hs
@@ -71,7 +71,8 @@ import GHC.Core.Make            ( mkWildValBinder, mkCoreLet )
 import GHC.Builtin.Types
 import GHC.Core.TyCo.Rep        ( TyCoBinder(..) )
 import qualified GHC.Core.Type as Type
-import GHC.Core.Type hiding     ( substTy, substTyVar, substTyVarBndr, extendTvSubst, extendCvSubst )
+import GHC.Core.Type hiding     ( substTy, substTyVar, substTyVarBndr, substCo
+                                , extendTvSubst, extendCvSubst )
 import qualified GHC.Core.Coercion as Coercion
 import GHC.Core.Coercion hiding ( substCo, substCoVar, substCoVarBndr )
 import GHC.Platform ( Platform )
diff --git a/compiler/GHC/Core/Opt/Specialise.hs b/compiler/GHC/Core/Opt/Specialise.hs
index ff974f9766..d7f29afd6c 100644
--- a/compiler/GHC/Core/Opt/Specialise.hs
+++ b/compiler/GHC/Core/Opt/Specialise.hs
@@ -15,9 +15,7 @@ import GHC.Driver.Config
 import GHC.Driver.Config.Diagnostic
 import GHC.Driver.Config.Core.Rules ( initRuleOpts )
 
-import GHC.Tc.Utils.TcType hiding( substTy )
-
-import GHC.Core.Type  hiding( substTy, extendTvSubstList, zapSubst )
+import GHC.Core.Type  hiding( substTy, substCo, extendTvSubst, zapSubst )
 import GHC.Core.Multiplicity
 import GHC.Core.Predicate
 import GHC.Core.Coercion( Coercion )
@@ -25,12 +23,15 @@ import GHC.Core.Opt.Monad
 import qualified GHC.Core.Subst as Core
 import GHC.Core.Unfold.Make
 import GHC.Core
+import GHC.Core.Make      ( mkLitRubbish )
+import GHC.Core.Unify     ( tcMatchTy )
 import GHC.Core.Rules
 import GHC.Core.Utils     ( exprIsTrivial
                           , mkCast, exprType
                           , stripTicksTop, mkInScopeSetBndrs )
 import GHC.Core.FVs
-import GHC.Core.TyCo.Rep (TyCoBinder (..))
+import GHC.Core.TyCo.Rep ( TyCoBinder (..) )
+import GHC.Core.TyCo.FVs ( tyCoVarsOfTypeList )
 import GHC.Core.Opt.Arity( collectBindersPushingCo )
 
 import GHC.Builtin.Types  ( unboxedUnitTy )
@@ -531,6 +532,48 @@ like
         f :: Eq [(a,b)] => ...
 
 
+Note [Specialisation and overlapping instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Here is at tricky case (see a comment in MR !8916):
+
+    module A where
+      class C a where
+        meth :: a -> String
+      instance {-# OVERLAPPABLE #-} C (Maybe a) where
+        meth _ = "Maybe"
+
+      {-# SPECIALISE f :: Maybe a -> Bool -> String #-}
+      f :: C a => a -> Bool -> String
+      f a True = f a False
+      f a _    = meth a
+
+    module B where
+      import A
+
+      instance C (Maybe Int) where
+        meth _ = "Int"
+
+      main = putStrLn $ f (Just 42 :: Maybe Int) True
+
+Running main without optimisations yields "Int", the correct answer.
+Activating optimisations yields "Maybe" due to a rewrite rule in module
+A generated by the SPECIALISE pragma:
+
+    RULE "USPEC f" forall a (d :: C a). f @a d = $sf
+
+In B we get the call (f @(Maybe Int) (d :: C (Maybe Int))), and
+that rewrites to $sf, but that isn't really right.
+
+Overlapping instances mean that `C (Maybe Int)` is not a singleton
+type: there two distinct dictionaries that have this type.  And that
+spells trouble for specialistion, which really asssumes singleton
+types.
+
+For now, we just accept this problem, but it may bite us one day.
+One solution would be to decline to expose any specialisation rules
+to an importing module -- but that seems a bit drastic.
+
+
 ************************************************************************
 *                                                                      *
 \subsubsection{The new specialiser}
@@ -804,8 +847,12 @@ spec_import top_env callers rb dict_binds cis@(CIS fn _)
 
 canSpecImport :: DynFlags -> Id -> Maybe CoreExpr
 canSpecImport dflags fn
+  | isDataConWrapId fn
+  = Nothing   -- Don't specialise data-con wrappers, even if they
+              -- have dict args; there is no benefit.
+
   | CoreUnfolding { uf_tmpl = rhs } <- unf
-    -- See Note [Specialising imported functions] point (1).
+    -- CoreUnfolding: see Note [Specialising imported functions] point (1).
   , isAnyInlinePragma (idInlinePragma fn)
     -- See Note [Specialising imported functions] point (2).
   = Just rhs
@@ -1508,12 +1555,12 @@ specCalls spec_imp env dict_binds existing_rules calls_for_me fn rhs
 
   | otherwise   -- No calls or RHS doesn't fit our preconceptions
   = warnPprTrace (not (exprIsTrivial rhs) && notNull calls_for_me)
-          "Missed specialisation opportunity" (ppr fn $$ _trace_doc) $
+          "Missed specialisation opportunity for" (ppr fn $$ trace_doc) $
           -- Note [Specialisation shape]
     -- pprTrace "specCalls: none" (ppr fn <+> ppr calls_for_me) $
     return ([], [], emptyUDs)
   where
-    _trace_doc = sep [ ppr rhs_bndrs, ppr (idInlineActivation fn) ]
+    trace_doc = sep [ ppr rhs_bndrs, ppr (idInlineActivation fn) ]
 
     fn_type   = idType fn
     fn_arity  = idArity fn
@@ -1577,8 +1624,16 @@ specCalls spec_imp env dict_binds existing_rules calls_for_me fn rhs
              else
         do { -- Run the specialiser on the specialised RHS
              -- The "1" suffix is before we maybe add the void arg
-           ; (spec_rhs1, rhs_uds) <- specLam rhs_env2 (spec_bndrs1 ++ leftover_bndrs) rhs_body
-           ; let spec_fn_ty1 = exprType spec_rhs1
+           ; (rhs_body', rhs_uds) <- specExpr rhs_env2 rhs_body
+                -- Add the { d1' = dx1; d2' = dx2 } usage stuff
+                -- to the rhs_uds; see Note [Specialising Calls]
+           ; let rhs_uds_w_dx = foldr consDictBind rhs_uds dx_binds
+                 spec_rhs_bndrs  = spec_bndrs1 ++ leftover_bndrs
+                 (spec_uds, dumped_dbs) = dumpUDs spec_rhs_bndrs rhs_uds_w_dx
+                 spec_rhs1 = mkLams spec_rhs_bndrs $
+                             wrapDictBindsE dumped_dbs rhs_body'
+
+                 spec_fn_ty1 = exprType spec_rhs1
 
                  -- Maybe add a void arg to the specialised function,
                  -- to avoid unlifted bindings
@@ -1612,10 +1667,6 @@ specCalls spec_imp env dict_binds existing_rules calls_for_me fn rhs
                                     herald fn rule_bndrs rule_lhs_args
                                     (mkVarApps (Var spec_fn) spec_bndrs)
 
-                -- Add the { d1' = dx1; d2' = dx2 } usage stuff
-                -- See Note [Specialising Calls]
-                spec_uds = foldr consDictBind rhs_uds dx_binds
-
                 simpl_opts = initSimpleOpts dflags
 
                 --------------------------------------
@@ -1798,11 +1849,23 @@ in the specialisation:
     {-# RULE "SPEC f @Int" forall x. f @Int x $dShow = $sf #-}
 
 This doesn’t save us much, since the arg would be removed later by
-worker/wrapper, anyway, but it’s easy to do. Note, however, that we
-only drop dead arguments if:
+worker/wrapper, anyway, but it’s easy to do.
 
-  1. We don’t specialise on them.
-  2. They come before an argument we do specialise on.
+Wrinkles
+
+* Note that we only drop dead arguments if:
+    1. We don’t specialise on them.
+    2. They come before an argument we do specialise on.
+  Doing the latter would require eta-expanding the RULE, which could
+  make it match less often, so it’s not worth it. Doing the former could
+  be more useful --- it would stop us from generating pointless
+  specialisations --- but it’s more involved to implement and unclear if
+  it actually provides much benefit in practice.
+
+* If the function has a stable unfolding, specHeader has to come up with
+  arguments to pass to that stable unfolding, when building the stable
+  unfolding of the specialised function: this is the last field in specHeader's
+  big result tuple.
 
   The right thing to do is to produce a LitRubbish; it should rapidly
   disappear.  Rather like GHC.Core.Opt.WorkWrap.Utils.mk_absent_let.
@@ -2253,11 +2316,11 @@ instance Outputable SpecArg where
   ppr (SpecDict d) = text "SpecDict" <+> ppr d
   ppr UnspecArg    = text "UnspecArg"
 
-specArgFreeVars :: SpecArg -> VarSet
-specArgFreeVars (SpecType ty) = tyCoVarsOfType ty
-specArgFreeVars (SpecDict dx) = exprFreeVars dx
-specArgFreeVars UnspecType    = emptyVarSet
-specArgFreeVars UnspecArg     = emptyVarSet
+specArgFreeIds :: SpecArg -> IdSet
+specArgFreeIds (SpecType {}) = emptyVarSet
+specArgFreeIds (SpecDict dx) = exprFreeIds dx
+specArgFreeIds UnspecType    = emptyVarSet
+specArgFreeIds UnspecArg     = emptyVarSet
 
 isSpecDict :: SpecArg -> Bool
 isSpecDict (SpecDict {}) = True
@@ -2327,24 +2390,33 @@ specHeader
               , [OutBndr]    -- Binders for $sf
               , [DictBind]   -- Auxiliary dictionary bindings
               , [OutExpr]    -- Specialised arguments for unfolding
-                             -- Same length as "args for LHS of rule"
+                             -- Same length as "Args for LHS of rule"
               )
 
 -- We want to specialise on type 'T1', and so we must construct a substitution
 -- 'a->T1', as well as a LHS argument for the resulting RULE and unfolding
 -- details.
-specHeader env (bndr : bndrs) (SpecType t : args)
-  = do { let env' = extendTvSubstList env [(bndr, t)]
-       ; (useful, env'', leftover_bndrs, rule_bs, rule_es, bs', dx, spec_args)
-            <- specHeader env' bndrs args
+specHeader env (bndr : bndrs) (SpecType ty : args)
+  = do { -- Find qvars, the type variables to add to the binders for the rule
+         -- Namely those free in `ty` that aren't in scope
+         -- See (MP2) in Note [Specialising polymorphic dictionaries]
+         let in_scope = Core.getSubstInScope (se_subst env)
+             qvars    = scopedSort $
+                        filterOut (`elemInScopeSet` in_scope) $
+                        tyCoVarsOfTypeList ty
+             (env1, qvars') = substBndrs env qvars
+             ty'            = substTy env1 ty
+             env2           = extendTvSubst env1 bndr ty'
+       ; (useful, env3, leftover_bndrs, rule_bs, rule_es, bs', dx, spec_args)
+            <- specHeader env2 bndrs args
        ; pure ( useful
-              , env''
+              , env3
               , leftover_bndrs
-              , rule_bs
-              , Type t : rule_es
-              , bs'
+              , qvars' ++ rule_bs
+              , Type ty' : rule_es
+              , qvars' ++ bs'
               , dx
-              , Type t : spec_args
+              , Type ty' : spec_args
               )
        }
 
@@ -2371,6 +2443,7 @@ specHeader env (bndr : bndrs) (UnspecType : args)
 -- a wildcard binder to match the dictionary (See Note [Specialising Calls] for
 -- the nitty-gritty), as a LHS rule and unfolding details.
 specHeader env (bndr : bndrs) (SpecDict d : args)
+  | not (isDeadBinder bndr)
   = do { (env1, bndr') <- newDictBndr env bndr -- See Note [Zap occ info in rule binders]
        ; let (env2, dx_bind, spec_dict) = bindAuxiliaryDict env1 bndr bndr' d
        ; (_, env3, leftover_bndrs, rule_bs, rule_es, bs', dx, spec_args)
@@ -2387,29 +2460,44 @@ specHeader env (bndr : bndrs) (SpecDict d : args)
               )
        }
 
--- Finally, we have the unspecialised argument 'i'. We need to produce
--- a binder, LHS and RHS argument for the RULE, and a binder for the
--- specialised body.
+-- Finally, we don't want to specialise on this argument 'i':
+--   - It's an UnSpecArg, or
+--   - It's a dead dictionary
+-- We need to produce a binder, LHS and RHS argument for the RULE, and
+-- a binder for the specialised body.
 --
 -- NB: Calls to 'specHeader' will trim off any trailing 'UnspecArg's, which is
 -- why 'i' doesn't appear in our RULE above. But we have no guarantee that
 -- there aren't 'UnspecArg's which come /before/ all of the dictionaries, so
 -- this case must be here.
-specHeader env (bndr : bndrs) (UnspecArg : args)
+specHeader env (bndr : bndrs) (_ : args)
+    -- The "_" can be UnSpecArg, or SpecDict where the bndr is dead
   = do { -- see Note [Zap occ info in rule binders]
          let (env', bndr') = substBndr env (zapIdOccInfo bndr)
        ; (useful, env'', leftover_bndrs, rule_bs, rule_es, bs', dx, spec_args)
              <- specHeader env' bndrs args
+
+       ; let bndr_ty = idType bndr'
+
+             -- See Note [Drop dead args from specialisations]
+             -- C.f. GHC.Core.Opt.WorkWrap.Utils.mk_absent_let
+             (mb_spec_bndr, spec_arg)
+                | isDeadBinder bndr
+                , Just lit_expr <- mkLitRubbish bndr_ty
+                = (Nothing, lit_expr)
+                | otherwise
+                = (Just bndr', varToCoreExpr bndr')
+
        ; pure ( useful
               , env''
               , leftover_bndrs
               , bndr' : rule_bs
               , varToCoreExpr bndr' : rule_es
-              , if isDeadBinder bndr
-                  then bs' -- see Note [Drop dead args from specialisations]
-                  else bndr' : bs'
+              , case mb_spec_bndr of
+                  Just b' -> b' : bs'
+                  Nothing -> bs'
               , dx
-              , varToCoreExpr bndr' : spec_args
+              , spec_arg : spec_args
               )
        }
 
@@ -2535,6 +2623,88 @@ successfully specialise 'f'.
 
 So the DictBinds in (ud_binds :: OrdList DictBind) may contain
 non-dictionary bindings too.
+
+Note [Specialising polymorphic dictionaries]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+    class M a where { foo :: a -> Int }
+
+    instance M (ST s) where ...
+    -- dMST :: forall s. M (ST s)
+
+    wimwam :: forall a. M a => a -> Int
+    wimwam = /\a \(d::M a). body
+
+    f :: ST s -> Int
+    f = /\s \(x::ST s). wimwam @(ST s) (dMST @s) dx + 1
+
+We'd like to specialise wimwam at (ST s), thus
+    $swimwam :: forall s. ST s -> Int
+    $swimwam = /\s. body[ST s/a, (dMST @s)/d]
+
+    RULE forall s (d :: M (ST s)).
+         wimwam @(ST s) d = $swimwam @s
+
+Here are the moving parts:
+
+(MP1) We must /not/ dump the CallInfo
+        CIS wimwam (CI { ci_key = [@(ST s), dMST @s]
+                       , ci_fvs = {dMST} })
+      when we come to the /\s.  Instead, we simply let it continue to float
+      upwards. Hence ci_fvs is an IdSet, listing the /Ids/ that
+      are free in the call, but not the /TyVars/.  Hence using specArgFreeIds
+      in singleCall.
+
+  NB to be fully kosher we should explicitly quantifying the CallInfo
+  over 's', but we don't bother.  This would matter if there was an
+  enclosing binding of the same 's', which I don't expect to happen.
+
+(MP2) When we come to specialise the call, we must remember to quantify
+      over 's'.  That is done in the SpecType case of specHeader, where
+      we add 's' (called qvars) to the binders of the RULE and the specialised
+      function.
+
+(MP3) If we have f :: forall m. Monoid m => blah, and two calls
+        (f @(Endo b)      (d :: Monoid (Endo b))
+        (f @(Endo (c->c)) (d :: Monoid (Endo (c->c)))
+      we want to generate a specialisation only for the first.  The second
+      is just a substitution instance of the first, with no greater specialisation.
+      Hence the call to `remove_dups` in `filterCalls`.
+
+All this arose in #13873, in the unexpected form that a SPECIALISE
+pragma made the program slower!  The reason was that the specialised
+function $sinsertWith arising from the pragma looked rather like `f`
+above, and failed to specialise a call in its body like wimwam.
+Without the pragma, the original call to `insertWith` was completely
+monomorpic, and specialised in one go.
+
+Wrinkles.
+
+* With -XOverlappingInstances you might worry about this:
+    class C a where ...
+    instance C (Maybe Int) where ...   -- $df1 :: C (Maybe Int)
+    instance C (Maybe a)   where ...   -- $df2 :: forall a. C (Maybe a)
+
+    f :: C a => blah
+    f = rhs
+
+    g = /\a.  ...(f @(Maybe a) ($df2 a))...
+    h = ...f @(Maybe Int) $df1
+
+  There are two calls to f, but with different evidence.  This patch will
+  combine them into one.  But it's OK: this code will never arise unless you
+  use -XIncoherentInstances.  Even with -XOverlappingInstances, GHC tries hard
+  to keep dictionaries as singleton types.  But that goes out of the window
+  with -XIncoherentInstances -- and that is true even with ordianry type-class
+  specialisation (at least if any inlining has taken place).
+
+  GHC makes very few guarantees when you use -XIncoherentInstances, and its
+  not worth crippling the normal case for the incoherent corner.  (The best
+  thing might be to switch off specialisation altogether if incoherence is
+  involved... but incoherence is a property of an instance, not a class, so
+  it's a hard test to make.)
+
+  But see Note [Specialisation and overlapping instances].
 -}
 
 instance Outputable DictBind where
@@ -2573,8 +2743,9 @@ data CallInfoSet = CIS Id (Bag CallInfo)
 data CallInfo
   = CI { ci_key  :: [SpecArg]   -- All arguments
        , ci_fvs  :: IdSet       -- Free Ids of the ci_key call
-                                -- _not_ including the main id itself, of course
+                                -- /not/ including the main id itself, of course
                                 -- NB: excluding tyvars:
+                                --     See Note [Specialising polymorphic dictionaries]
     }
 
 type DictExpr = CoreExpr
@@ -2620,17 +2791,12 @@ singleCall :: Id -> [SpecArg] -> UsageDetails
 singleCall id args
   = MkUD {ud_binds = emptyFDBs,
           ud_calls = unitDVarEnv id $ CIS id $
-                     unitBag (CI { ci_key  = args -- used to be tys
+                     unitBag (CI { ci_key  = args
                                  , ci_fvs  = call_fvs }) }
   where
-    call_fvs = foldr (unionVarSet . specArgFreeVars) emptyVarSet args
-        -- The type args (tys) are guaranteed to be part of the dictionary
-        -- types, because they are just the constrained types,
-        -- and the dictionary is therefore sure to be bound
-        -- inside the binding for any type variables free in the type;
-        -- hence it's safe to neglect tyvars free in tys when making
-        -- the free-var set for this call
-        -- BUT I don't trust this reasoning; play safe and include tys_fvs
+    call_fvs = foldr (unionVarSet . specArgFreeIds) emptyVarSet args
+        -- specArgFreeIds: we specifically look for free Ids, not TyVars
+        --    see (MP1) in Note [Specialising polymorphic dictionaries]
         --
         -- We don't include the 'id' itself.
 
@@ -2953,15 +3119,15 @@ callsForMe fn uds@MkUD { ud_binds = orig_dbs, ud_calls = orig_calls }
 
 ----------------------
 filterCalls :: CallInfoSet -> FloatedDictBinds -> [CallInfo]
--- Remove dominated calls
+-- Remove dominated calls (Note [Specialising polymorphic dictionaries])
 -- and loopy DFuns (Note [Avoiding loops (DFuns)])
 filterCalls (CIS fn call_bag) (FDB { fdb_binds = dbs })
   | isDFunId fn  -- Note [Avoiding loops (DFuns)] applies only to DFuns
-  = filter ok_call unfiltered_calls
+  = filter ok_call de_dupd_calls
   | otherwise         -- Do not apply it to non-DFuns
-  = unfiltered_calls  -- See Note [Avoiding loops (non-DFuns)]
+  = de_dupd_calls  -- See Note [Avoiding loops (non-DFuns)]
   where
-    unfiltered_calls = bagToList call_bag
+    de_dupd_calls = remove_dups call_bag
 
     dump_set = foldl' go (unitVarSet fn) dbs
       -- This dump-set could also be computed by splitDictBinds
@@ -2975,6 +3141,31 @@ filterCalls (CIS fn call_bag) (FDB { fdb_binds = dbs })
 
     ok_call (CI { ci_fvs = fvs }) = fvs `disjointVarSet` dump_set
 
+remove_dups :: Bag CallInfo -> [CallInfo]
+-- Calls involving more generic instances beat more specific ones.
+-- See (MP3) in Note [Specialising polymorphic dictionaries]
+remove_dups calls = foldr add [] calls
+  where
+    add :: CallInfo -> [CallInfo] -> [CallInfo]
+    add ci [] = [ci]
+    add ci1 (ci2:cis) | ci2 `beats_or_same` ci1 = ci2:cis
+                      | ci1 `beats_or_same` ci2 = ci1:cis
+                      | otherwise               = ci2 : add ci1 cis
+
+beats_or_same :: CallInfo -> CallInfo -> Bool
+beats_or_same (CI { ci_key = args1 }) (CI { ci_key = args2 })
+  = go args1 args2
+  where
+    go [] _ = True
+    go (arg1:args1) (arg2:args2) = go_arg arg1 arg2 && go args1 args2
+    go (_:_)        []           = False
+
+    go_arg (SpecType ty1) (SpecType ty2) = isJust (tcMatchTy ty1 ty2)
+    go_arg UnspecType     UnspecType     = True
+    go_arg (SpecDict {})  (SpecDict {})  = True
+    go_arg UnspecArg      UnspecArg      = True
+    go_arg _              _              = False
+
 ----------------------
 splitDictBinds :: FloatedDictBinds -> IdSet -> (FloatedDictBinds, OrdList DictBind, IdSet)
 -- splitDictBinds dbs bndrs returns
@@ -3005,15 +3196,18 @@ splitDictBinds (FDB { fdb_binds = dbs, fdb_bndrs = bs }) bndr_set
 
 ----------------------
 deleteCallsMentioning :: VarSet -> CallDetails -> CallDetails
--- Remove calls *mentioning* bs in any way
-deleteCallsMentioning bs calls
+-- Remove calls mentioning any Id in bndrs
+-- NB: The call is allowed to mention TyVars in bndrs
+--     Note [Specialising polymorphic dictionaries]
+--     ci_fvs are just the free /Ids/
+deleteCallsMentioning bndrs calls
   = mapDVarEnv (ciSetFilter keep_call) calls
   where
-    keep_call (CI { ci_fvs = fvs }) = fvs `disjointVarSet` bs
+    keep_call (CI { ci_fvs = fvs }) = fvs `disjointVarSet` bndrs
 
 deleteCallsFor :: [Id] -> CallDetails -> CallDetails
--- Remove calls *for* bs
-deleteCallsFor bs calls = delDVarEnvList calls bs
+-- Remove calls *for* bndrs
+deleteCallsFor bndrs calls = delDVarEnvList calls bndrs
 
 {-
 ************************************************************************
@@ -3036,9 +3230,9 @@ mapAndCombineSM f (x:xs) = do (y, uds1) <- f x
                               (ys, uds2) <- mapAndCombineSM f xs
                               return (y:ys, uds1 `thenUDs` uds2)
 
-extendTvSubstList :: SpecEnv -> [(TyVar,Type)] -> SpecEnv
-extendTvSubstList env tv_binds
-  = env { se_subst = Core.extendTvSubstList (se_subst env) tv_binds }
+extendTvSubst :: SpecEnv -> TyVar -> Type -> SpecEnv
+extendTvSubst env tv ty
+  = env { se_subst = Core.extendTvSubst (se_subst env) tv ty }
 
 extendInScope :: SpecEnv -> OutId -> SpecEnv
 extendInScope env@(SE { se_subst = subst }) bndr
diff --git a/compiler/GHC/Core/Subst.hs b/compiler/GHC/Core/Subst.hs
index 9bfca6184e..5d8cd11758 100644
--- a/compiler/GHC/Core/Subst.hs
+++ b/compiler/GHC/Core/Subst.hs
@@ -26,7 +26,8 @@ module GHC.Core.Subst (
         extendIdSubstWithClone,
         extendSubst, extendSubstList, extendSubstWithVar,
         extendSubstInScope, extendSubstInScopeList, extendSubstInScopeSet,
-        isInScope, setInScope, extendTvSubst, extendCvSubst,
+        isInScope, setInScope, getSubstInScope,
+        extendTvSubst, extendCvSubst,
         delBndr, delBndrs, zapSubst,
 
         -- ** Substituting and cloning binders
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 8d41466d30..b6b2dd369c 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -219,7 +219,7 @@ module GHC.Core.Type (
         substTyAddInScope,
         substTyUnchecked, substTysUnchecked, substScaledTyUnchecked, substScaledTysUnchecked,
         substThetaUnchecked, substTyWithUnchecked,
-        substCoUnchecked, substCoWithUnchecked,
+        substCo, substCoUnchecked, substCoWithUnchecked,
         substTyVarBndr, substTyVarBndrs, substTyVar, substTyVars,
         substVarBndr, substVarBndrs,
         substTyCoBndr,
diff --git a/testsuite/tests/numeric/should_compile/T19641.stderr b/testsuite/tests/numeric/should_compile/T19641.stderr
index 7c1cf57b06..ec7e19c946 100644
--- a/testsuite/tests/numeric/should_compile/T19641.stderr
+++ b/testsuite/tests/numeric/should_compile/T19641.stderr
@@ -3,30 +3,30 @@
 Result size of Tidy Core
   = {terms: 22, types: 20, coercions: 0, joins: 0/0}
 
-integer_to_int
+natural_to_word
   = \ eta ->
       case eta of {
-        IS ipv -> Just (I# ipv);
-        IP x1 -> Nothing;
-        IN ds -> Nothing
+        NS x1 -> Just (W# x1);
+        NB ds -> Nothing
       }
 
-natural_to_word
+integer_to_int
   = \ eta ->
       case eta of {
-        NS x1 -> Just (W# x1);
-        NB ds -> Nothing
+        IS ipv -> Just (I# ipv);
+        IP x1 -> Nothing;
+        IN ds -> Nothing
       }
 
 
 ------ Local rules for imported ids --------
-"SPEC/Test toIntegralSized @Natural @Word"
-    forall $dIntegral $dIntegral1 $dBits $dBits1.
-      toIntegralSized $dIntegral $dIntegral1 $dBits $dBits1
-      = natural_to_word
 "SPEC/Test toIntegralSized @Integer @Int"
     forall $dIntegral $dIntegral1 $dBits $dBits1.
       toIntegralSized $dIntegral $dIntegral1 $dBits $dBits1
       = integer_to_int
+"SPEC/Test toIntegralSized @Natural @Word"
+    forall $dIntegral $dIntegral1 $dBits $dBits1.
+      toIntegralSized $dIntegral $dIntegral1 $dBits $dBits1
+      = natural_to_word
 
 
diff --git a/testsuite/tests/simplCore/should_compile/T8331.stderr b/testsuite/tests/simplCore/should_compile/T8331.stderr
index 41bc7de5f4..c940ed26fc 100644
--- a/testsuite/tests/simplCore/should_compile/T8331.stderr
+++ b/testsuite/tests/simplCore/should_compile/T8331.stderr
@@ -1,5 +1,149 @@
 
 ==================== Tidy Core rules ====================
+"SPEC $c*> @(ST s) @_"
+    forall (@s) (@r) ($dApplicative :: Applicative (ST s)).
+      $fApplicativeReaderT_$c*> @(ST s) @r $dApplicative
+      = ($fApplicativeReaderT2 @s @r)
+        `cast` (forall (a :: <*>_N) (b :: <*>_N).
+                <ReaderT r (ST s) a>_R
+                %<'Many>_N ->_R <ReaderT r (ST s) b>_R
+                %<'Many>_N ->_R <r>_R %<'Many>_N ->_R Sym (N:ST[0] <s>_N <b>_R)
+                                ; Sym (N:ReaderT[0] <*>_N <r>_R <ST s>_R <b>_N)
+                :: Coercible
+                     (forall {a} {b}.
+                      ReaderT r (ST s) a -> ReaderT r (ST s) b -> r -> STRep s b)
+                     (forall {a} {b}.
+                      ReaderT r (ST s) a -> ReaderT r (ST s) b -> ReaderT r (ST s) b))
+"SPEC $c<$ @(ST s) @_"
+    forall (@s) (@r) ($dFunctor :: Functor (ST s)).
+      $fFunctorReaderT_$c<$ @(ST s) @r $dFunctor
+      = ($fApplicativeReaderT6 @s @r)
+        `cast` (forall (a :: <*>_N) (b :: <*>_N).
+                <a>_R
+                %<'Many>_N ->_R <ReaderT r (ST s) b>_R
+                %<'Many>_N ->_R <r>_R %<'Many>_N ->_R Sym (N:ST[0] <s>_N <a>_R)
+                                ; Sym (N:ReaderT[0] <*>_N <r>_R <ST s>_R <a>_N)
+                :: Coercible
+                     (forall {a} {b}. a -> ReaderT r (ST s) b -> r -> STRep s a)
+                     (forall {a} {b}. a -> ReaderT r (ST s) b -> ReaderT r (ST s) a))
+"SPEC $c<* @(ST s) @_"
+    forall (@s) (@r) ($dApplicative :: Applicative (ST s)).
+      $fApplicativeReaderT_$c<* @(ST s) @r $dApplicative
+      = ($fApplicativeReaderT1 @s @r)
+        `cast` (forall (a :: <*>_N) (b :: <*>_N).
+                <ReaderT r (ST s) a>_R
+                %<'Many>_N ->_R <ReaderT r (ST s) b>_R
+                %<'Many>_N ->_R <r>_R %<'Many>_N ->_R Sym (N:ST[0] <s>_N <a>_R)
+                                ; Sym (N:ReaderT[0] <*>_N <r>_R <ST s>_R <a>_N)
+                :: Coercible
+                     (forall {a} {b}.
+                      ReaderT r (ST s) a -> ReaderT r (ST s) b -> r -> STRep s a)
+                     (forall {a} {b}.
+                      ReaderT r (ST s) a -> ReaderT r (ST s) b -> ReaderT r (ST s) a))
+"SPEC $c<*> @(ST s) @_"
+    forall (@s) (@r) ($dApplicative :: Applicative (ST s)).
+      $fApplicativeReaderT9 @(ST s) @r $dApplicative
+      = ($fApplicativeReaderT4 @s @r)
+        `cast` (forall (a :: <*>_N) (b :: <*>_N).
+                <ReaderT r (ST s) (a -> b)>_R
+                %<'Many>_N ->_R <ReaderT r (ST s) a>_R
+                %<'Many>_N ->_R <r>_R
+                %<'Many>_N ->_R Sym (N:ST[0] <s>_N <b>_R)
+                :: Coercible
+                     (forall {a} {b}.
+                      ReaderT r (ST s) (a -> b) -> ReaderT r (ST s) a -> r -> STRep s b)
+                     (forall {a} {b}.
+                      ReaderT r (ST s) (a -> b) -> ReaderT r (ST s) a -> r -> ST s b))
+"SPEC $c>> @(ST s) @_"
+    forall (@s) (@r) ($dMonad :: Monad (ST s)).
+      $fMonadReaderT1 @(ST s) @r $dMonad
+      = $fMonadAbstractIOSTReaderT_$s$c>> @s @r
+"SPEC $c>>= @(ST s) @_"
+    forall (@s) (@r) ($dMonad :: Monad (ST s)).
+      $fMonadReaderT2 @(ST s) @r $dMonad
+      = ($fMonadAbstractIOSTReaderT2 @s @r)
+        `cast` (forall (a :: <*>_N) (b :: <*>_N).
+                <ReaderT r (ST s) a>_R
+                %<'Many>_N ->_R <a -> ReaderT r (ST s) b>_R
+                %<'Many>_N ->_R <r>_R
+                %<'Many>_N ->_R Sym (N:ST[0] <s>_N <b>_R)
+                :: Coercible
+                     (forall {a} {b}.
+                      ReaderT r (ST s) a -> (a -> ReaderT r (ST s) b) -> r -> STRep s b)
+                     (forall {a} {b}.
+                      ReaderT r (ST s) a -> (a -> ReaderT r (ST s) b) -> r -> ST s b))
+"SPEC $cfmap @(ST s) @_"
+    forall (@s) (@r) ($dFunctor :: Functor (ST s)).
+      $fFunctorReaderT_$cfmap @(ST s) @r $dFunctor
+      = ($fApplicativeReaderT7 @s @r)
+        `cast` (forall (a :: <*>_N) (b :: <*>_N).
+                <a -> b>_R
+                %<'Many>_N ->_R <ReaderT r (ST s) a>_R
+                %<'Many>_N ->_R <r>_R %<'Many>_N ->_R Sym (N:ST[0] <s>_N <b>_R)
+                                ; Sym (N:ReaderT[0] <*>_N <r>_R <ST s>_R <b>_N)
+                :: Coercible
+                     (forall {a} {b}. (a -> b) -> ReaderT r (ST s) a -> r -> STRep s b)
+                     (forall {a} {b}.
+                      (a -> b) -> ReaderT r (ST s) a -> ReaderT r (ST s) b))
+"SPEC $cliftA2 @(ST s) @_"
+    forall (@s) (@r) ($dApplicative :: Applicative (ST s)).
+      $fApplicativeReaderT_$cliftA2 @(ST s) @r $dApplicative
+      = ($fApplicativeReaderT3 @s @r)
+        `cast` (forall (a :: <*>_N) (b :: <*>_N) (c :: <*>_N).
+                <a -> b -> c>_R
+                %<'Many>_N ->_R <ReaderT r (ST s) a>_R
+                %<'Many>_N ->_R <ReaderT r (ST s) b>_R
+                %<'Many>_N ->_R <r>_R %<'Many>_N ->_R Sym (N:ST[0] <s>_N <c>_R)
+                                ; Sym (N:ReaderT[0] <*>_N <r>_R <ST s>_R <c>_N)
+                :: Coercible
+                     (forall {a} {b} {c}.
+                      (a -> b -> c)
+                      -> ReaderT r (ST s) a -> ReaderT r (ST s) b -> r -> STRep s c)
+                     (forall {a} {b} {c}.
+                      (a -> b -> c)
+                      -> ReaderT r (ST s) a -> ReaderT r (ST s) b -> ReaderT r (ST s) c))
+"SPEC $cp1Applicative @(ST s) @_"
+    forall (@s) (@r) ($dApplicative :: Applicative (ST s)).
+      $fApplicativeReaderT_$cp1Applicative @(ST s) @r $dApplicative
+      = $fApplicativeReaderT_$s$fFunctorReaderT @s @r
+"SPEC $cp1Monad @(ST s) @_"
+    forall (@s) (@r) ($dMonad :: Monad (ST s)).
+      $fMonadReaderT_$cp1Monad @(ST s) @r $dMonad
+      = $fApplicativeReaderT_$s$fApplicativeReaderT @s @r
+"SPEC $cpure @(ST s) @_"
+    forall (@s) (@r) ($dApplicative :: Applicative (ST s)).
+      $fApplicativeReaderT_$cpure @(ST s) @r $dApplicative
+      = ($fApplicativeReaderT5 @s @r)
+        `cast` (forall (a :: <*>_N).
+                <a>_R
+                %<'Many>_N ->_R <r>_R %<'Many>_N ->_R Sym (N:ST[0] <s>_N <a>_R)
+                                ; Sym (N:ReaderT[0] <*>_N <r>_R <ST s>_R <a>_N)
+                :: Coercible
+                     (forall {a}. a -> r -> STRep s a)
+                     (forall {a}. a -> ReaderT r (ST s) a))
+"SPEC $creturn @(ST s) @_"
+    forall (@s) (@r) ($dMonad :: Monad (ST s)).
+      $fMonadReaderT_$creturn @(ST s) @r $dMonad
+      = ($fApplicativeReaderT5 @s @r)
+        `cast` (forall (a :: <*>_N).
+                <a>_R
+                %<'Many>_N ->_R <r>_R %<'Many>_N ->_R Sym (N:ST[0] <s>_N <a>_R)
+                                ; Sym (N:ReaderT[0] <*>_N <r>_R <ST s>_R <a>_N)
+                :: Coercible
+                     (forall {a}. a -> r -> STRep s a)
+                     (forall {a}. a -> ReaderT r (ST s) a))
+"SPEC $fApplicativeReaderT @(ST s) @_"
+    forall (@s) (@r) ($dApplicative :: Applicative (ST s)).
+      $fApplicativeReaderT @(ST s) @r $dApplicative
+      = $fApplicativeReaderT_$s$fApplicativeReaderT @s @r
+"SPEC $fFunctorReaderT @(ST s) @_"
+    forall (@s) (@r) ($dFunctor :: Functor (ST s)).
+      $fFunctorReaderT @(ST s) @r $dFunctor
+      = $fApplicativeReaderT_$s$fFunctorReaderT @s @r
+"SPEC $fMonadReaderT @(ST s) @_"
+    forall (@s) (@r) ($dMonad :: Monad (ST s)).
+      $fMonadReaderT @(ST s) @r $dMonad
+      = $fMonadAbstractIOSTReaderT_$s$fMonadReaderT @s @r
 "USPEC useAbstractMonad @(ReaderT Int (ST s))"
     forall (@s)
            ($dMonadAbstractIOST :: MonadAbstractIOST (ReaderT Int (ST s))).
diff --git a/testsuite/tests/simplCore/should_compile/all.T b/testsuite/tests/simplCore/should_compile/all.T
index 9cbd330d0b..d4ad82e0d9 100644
--- a/testsuite/tests/simplCore/should_compile/all.T
+++ b/testsuite/tests/simplCore/should_compile/all.T
@@ -434,3 +434,6 @@ test('T21148', [grep_errmsg(r'Cpr=') ], compile, ['-O -ddump-simpl'])
 test('T21851', [grep_errmsg(r'case.*w\$sf') ], multimod_compile, ['T21851', '-O -dno-typeable-binds -dsuppress-uniques'])
 # One module, T22097.hs, has OPTIONS_GHC -ddump-simpl
 test('T22097', [grep_errmsg(r'case.*wgoEven') ], multimod_compile, ['T22097', '-O -dno-typeable-binds -dsuppress-uniques'])
+
+test('T13873',  [ grep_errmsg(r'SPEC') ], compile, ['-O -ddump-rules'])
+