compiler/parser/Lexer.x

@@ -475,6 +475,7 @@ data Token
   | ITinline_prag InlineSpec RuleMatchInfo
   | ITspec_prag                 -- SPECIALISE
   | ITspec_inline_prag Bool     -- SPECIALISE INLINE (or NOINLINE)
+  | ITsupercompile_prag         -- SUPERCOMPILE
   | ITsource_prag
   | ITrules_prag
   | ITwarning_prag
@@ -2310,11 +2311,15 @@ ignoredPrags = Map.fromList (map ignored pragmas)
 
 oneWordPrags = Map.fromList([("rules", rulePrag),
                            ("inline", token (ITinline_prag Inline FunLike)),
-                           ("inlinable", token (ITinline_prag Inlinable FunLike)),
-                           ("inlineable", token (ITinline_prag Inlinable FunLike)),
+                           ("inlinable", token (ITinline_prag (Inlinable False) FunLike)),
+                           ("inlineable", token (ITinline_prag (Inlinable False) FunLike)),
+                                          -- Spelling variant
+                           ("superinlinable", token (ITinline_prag (Inlinable True) FunLike)),
+                           ("superinlineable", token (ITinline_prag (Inlinable True) FunLike)),
                                           -- Spelling variant
                            ("notinline", token (ITinline_prag NoInline FunLike)),
                            ("specialize", token ITspec_prag),
+                           ("supercompile", token ITsupercompile_prag),
                            ("source", token ITsource_prag),
                            ("warning", token ITwarning_prag),
                            ("deprecated", token ITdeprecated_prag),

compiler/parser/Parser.y.pp

@@ -254,6 +254,7 @@ incorrect.
  '{-# INLINE'             { L _ (ITinline_prag _ _) }
  '{-# SPECIALISE'         { L _ ITspec_prag }
  '{-# SPECIALISE_INLINE'  { L _ (ITspec_inline_prag _) }
+ '{-# SUPERCOMPILE'       { L _ ITsupercompile_prag }
  '{-# SOURCE'                                   { L _ ITsource_prag }
  '{-# RULES'                                    { L _ ITrules_prag }
  '{-# CORE'                                     { L _ ITcore_prag }              -- hdaume: annotated core
@@ -594,6 +595,8 @@ topdecl :: { OrdList (LHsDecl RdrName) }
         | '{-# VECTORISE' 'class' gtycon '#-}'  { unitOL $ LL $ VectD (HsVectClassIn $3) }
         | '{-# VECTORISE_SCALAR' 'instance' type '#-}'     
                                                 { unitOL $ LL $ VectD (HsVectInstIn $3) }
+        | '{-# INLINE' activation 'module' '#-}'        
+                                                { unitOL (LL $ SigD (InlineSig Nothing (mkInlinePragma (getINLINE $1) $2))) }
         | annotation { unitOL $1 }
         | decl                                  { unLoc $1 }
 
@@ -1346,7 +1349,7 @@ sigdecl :: { Located (OrdList (LHsDecl RdrName)) }
         | infix prec ops        { LL $ toOL [ LL $ SigD (FixSig (FixitySig n (Fixity $2 (unLoc $1))))
                                              | n <- unLoc $3 ] }
         | '{-# INLINE' activation qvar '#-}'        
-                { LL $ unitOL (LL $ SigD (InlineSig $3 (mkInlinePragma (getINLINE $1) $2))) }
+                { LL $ unitOL (LL $ SigD (InlineSig (Just $3) (mkInlinePragma (getINLINE $1) $2))) }
         | '{-# SPECIALISE' activation qvar '::' sigtypes1 '#-}'
                 { let inl_prag = mkInlinePragma (EmptyInlineSpec, FunLike) $2
                   in LL $ toOL [ LL $ SigD (SpecSig $3 t inl_prag) 
@@ -1356,6 +1359,8 @@ sigdecl :: { Located (OrdList (LHsDecl RdrName)) }
                             | t <- $5] }
         | '{-# SPECIALISE' 'instance' inst_type '#-}'
                 { LL $ unitOL (LL $ SigD (SpecInstSig $3)) }
+        | '{-# SUPERCOMPILE' qvar '#-}'
+                { LL $ unitOL (LL $ SigD (SupercompileSig $2)) }
 
 -----------------------------------------------------------------------------
 -- Expressions

compiler/rename/RnBinds.lhs

@@ -53,6 +53,7 @@ import FastString
 import Data.List	( partition )
 import Maybes		( orElse )
 import Control.Monad
+import Data.Traversable ( traverse )
 \end{code}
 
 -- ToDo: Put the annotations into the monad, so that they arrive in the proper
@@ -701,9 +702,13 @@ renameSig ctxt sig@(SpecSig v ty inl)
 	; (new_ty, fvs) <- rnHsSigType (quotes (ppr v)) ty
 	; return (SpecSig new_v new_ty inl, fvs) }
 
-renameSig ctxt sig@(InlineSig v s)
-  = do	{ new_v <- lookupSigOccRn ctxt sig v
-	; return (InlineSig new_v s, emptyFVs) }
+renameSig ctxt sig@(InlineSig mb_v s)
+  = do	{ new_mb_v <- traverse (lookupSigOccRn ctxt sig) mb_v
+	; return (InlineSig new_mb_v s, emptyFVs) }
+
+renameSig ctxt sig@(SupercompileSig v)
+  = do  { new_v <- lookupSigOccRn ctxt sig v
+        ; return (SupercompileSig new_v, emptyFVs) }
 
 renameSig ctxt sig@(FixSig (FixitySig v f))
   = do	{ new_v <- lookupSigOccRn ctxt sig v
@@ -737,6 +742,9 @@ okHsSig ctxt (L _ sig)
 
      (SpecInstSig {}, InstDeclCtxt {}) -> True
      (SpecInstSig {}, _)               -> False
+
+     (SupercompileSig {}, HsBootCtxt) -> False
+     (SupercompileSig {}, _)          -> True
 \end{code}
 
 

compiler/simplCore/CoreMonad.lhs

@@ -245,6 +245,7 @@ data CoreToDo           -- These are diff core-to-core passes,
   | CoreDoWorkerWrapper
   | CoreDoSpecialising
   | CoreDoSpecConstr
+  | CoreDoSupercomp
   | CoreCSE
   | CoreDoRuleCheck CompilerPhase String   -- Check for non-application of rules
                                            -- matching this string
@@ -273,6 +274,7 @@ coreDumpFlag CoreDoStrictness 	      = Just Opt_D_dump_stranal
 coreDumpFlag CoreDoWorkerWrapper      = Just Opt_D_dump_worker_wrapper
 coreDumpFlag CoreDoSpecialising       = Just Opt_D_dump_spec
 coreDumpFlag CoreDoSpecConstr         = Just Opt_D_dump_spec
+coreDumpFlag CoreDoSupercomp          = Just Opt_D_dump_supercomp
 coreDumpFlag CoreCSE                  = Just Opt_D_dump_cse 
 coreDumpFlag CoreDoVectorisation      = Just Opt_D_dump_vect
 coreDumpFlag CoreDesugar              = Just Opt_D_dump_ds 
@@ -296,6 +298,7 @@ instance Outputable CoreToDo where
   ppr CoreDoWorkerWrapper      = ptext (sLit "Worker Wrapper binds")
   ppr CoreDoSpecialising       = ptext (sLit "Specialise")
   ppr CoreDoSpecConstr         = ptext (sLit "SpecConstr")
+  ppr CoreDoSupercomp          = ptext (sLit "Supercompilation")
   ppr CoreCSE                  = ptext (sLit "Common sub-expression")
   ppr CoreDoVectorisation      = ptext (sLit "Vectorisation")
   ppr CoreDesugar              = ptext (sLit "Desugar (before optimization)")

compiler/simplCore/SimplCore.lhs

@@ -36,13 +36,14 @@ import FloatIn          ( floatInwards )
 import FloatOut         ( floatOutwards )
 import FamInstEnv
 import Id
-import BasicTypes       ( CompilerPhase(..), isDefaultInlinePragma )
+import BasicTypes       ( CompilerPhase(..) )
 import VarSet
 import VarEnv
 import LiberateCase     ( liberateCase )
 import SAT              ( doStaticArgs )
 import Specialise       ( specProgram)
 import SpecConstr       ( specConstrProgram)
+import Supercompile     ( supercompileProgram )
 import DmdAnal          ( dmdAnalPgm )
 import WorkWrap         ( wwTopBinds )
 import Vectorise        ( vectorise )
@@ -125,6 +126,7 @@ getCoreToDo dflags
     do_float_in   = dopt Opt_FloatIn                      dflags
     cse           = dopt Opt_CSE                          dflags
     spec_constr   = dopt Opt_SpecConstr                   dflags
+    supercomp     = dopt Opt_Supercompilation             dflags
     liberate_case = dopt Opt_LiberateCase                 dflags
     static_args   = dopt Opt_StaticArgumentTransformation dflags
     rules_on      = dopt Opt_EnableRewriteRules           dflags
@@ -205,6 +207,8 @@ getCoreToDo dflags
     -- after this before anything else
         runWhen static_args (CoreDoPasses [ simpl_gently, CoreDoStaticArgs ]),
 
+        runWhen supercomp CoreDoSupercomp,
+
         -- We run vectorisation here for now, but we might also try to run
         -- it later
         vectorisation,
@@ -397,6 +401,9 @@ doCorePass CoreDoSpecialising        = {-# SCC "Specialise" #-}
 doCorePass CoreDoSpecConstr          = {-# SCC "SpecConstr" #-}
                                        specConstrProgram
 
+doCorePass CoreDoSupercomp           = {-# SCC "Supercomp" #-}
+                                       doPassDM (\_ -> supercompileProgram)
+
 doCorePass CoreDoVectorisation       = {-# SCC "Vectorise" #-}
                                        vectorise
 
@@ -882,12 +889,7 @@ hasShortableIdInfo :: Id -> Bool
 -- True if there is no user-attached IdInfo on exported_id,
 -- so we can safely discard it
 -- See Note [Messing up the exported Id's IdInfo]
-hasShortableIdInfo id
-  =  isEmptySpecInfo (specInfo info)
-  && isDefaultInlinePragma (inlinePragInfo info)
-  && not (isStableUnfolding (unfoldingInfo info))
-  where
-     info = idInfo id
+hasShortableIdInfo = isShortableIdInfo . idInfo
 
 -----------------
 transferIdInfo :: Id -> Id -> Id

compiler/simplCore/SimplUtils.lhs

@@ -13,7 +13,7 @@
 
 module SimplUtils (
 	-- Rebuilding
-	mkLam, mkCase, prepareAlts, tryEtaExpand,
+	mkLam, mkCase, prepareAlts, filterAlts, tryEtaExpand,
 
 	-- Inlining,
 	preInlineUnconditionally, postInlineUnconditionally, 
@@ -52,6 +52,7 @@ import CoreUnfold
 import Name
 import Id
 import Var
+import DataCon          ( dataConWorkId )
 import Demand
 import SimplMonad
 import Type	hiding( substTy )

compiler/simplCore/Simplify.lhs

@@ -760,7 +760,7 @@ simplUnfolding env top_lvl id _
        }
   where
     act      = idInlineActivation id
-    rule_env = updMode (updModeForInlineRules act) env
+    rule_env = updMode (\mode -> let mode' = updModeForInlineRules act mode in case src of InlineStable -> mode' { sm_rules = False }; _ -> mode') env
        	       -- See Note [Simplifying inside InlineRules] in SimplUtils
 
 simplUnfolding _ top_lvl id new_rhs _

compiler/specialise/Specialise.lhs

@@ -1157,15 +1157,15 @@ specCalls subst rules_for_me calls_for_me fn rhs
                   = neverInlinePragma	-- See Note [Specialising imported functions] in OccurAnal
                   | otherwise	
 		  = case inl_prag of
-                       InlinePragma { inl_inline = Inlinable } 
+                       InlinePragma { inl_inline = Inlinable _ } 
                           -> inl_prag { inl_inline = EmptyInlineSpec }
 		       _  -> inl_prag
 
 		spec_unf
                   = case inlinePragmaSpec spec_inl_prag of
-                      Inline    -> mkInlineUnfolding (Just spec_arity) spec_rhs
-                      Inlinable -> mkInlinableUnfolding spec_rhs
-                      _         -> NoUnfolding
+                      Inline      -> mkInlineUnfolding (Just spec_arity) spec_rhs
+                      Inlinable _ -> mkInlinableUnfolding spec_rhs
+                      _           -> NoUnfolding
 
 		--------------------------------------
 		-- Adding arity information just propagates it a bit faster

compiler/supercompile/.gitignore

+# Ignore directory created by install-plugin-inplace
+dist/

compiler/supercompile/CHSC.hs

+module CHSC (Supercompile(..), plugin) where
+
+import Supercompile
+import GhcPlugins
+
+import Data.Data     (Data)
+import Data.Typeable (Typeable)
+import Data.List     (nub)
+
+
+-- The supercomplier behaves as follows:
+--  1. If the command line contains -fplugin-opt=CHSC:supercompile or the module is annotated
+--     with Supercompile then we supercompile the whole module
+--  2. Otherwise, we supercompile any individual definitions annoted with Supercompile
+
+data Supercompile = Supercompile deriving (Data, Typeable)
+
+
+plugin :: Plugin
+plugin = defaultPlugin {
+    installCoreToDos = install
+  }
+
+install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]
+install options todos = do
+    unconditional <- case nub options of
+        []               -> return False
+        ["supercompile"] -> return True
+        _                -> fail "CHSC: the only recognised command line option is -fplugin-opt=CHSC:supercompile"
+    return $ CoreDoPluginPass "Supercompile (CHSC)" (pass unconditional) : todos
+
+pass :: Bool -> ModGuts -> CoreM ModGuts
+pass unconditional guts = do
+    -- Determine which top-level binders should be supercompiled
+    should_sc <- case unconditional of
+        True  -> return (const True)
+        False -> do
+            anns :: UniqFM Supercompile <- getFirstAnnotations deserializeWithData guts
+            mod <- getModule
+            return $ if mod `elemUFM` anns
+                      then const True
+                      else (`elemUFM` anns)
+    -- Do the deed
+    bindsOnlyPass (return . supercompileProgramSelective should_sc) guts

compiler/supercompile/Supercompile.hs

+module Supercompile (supercompileProgram, supercompileProgramSelective) where
+
+#include "HsVersions.h"
+
+-- FIXME: I need to document the basis on which I push down unlifted heap bindings (they are all values, IIRC)
+-- TODO:
+--  * Why does the supercompiler not match as much as it should? (e.g. Interpreter, UInterpreter)
+--  * We should probably claimStep when supercompiling the RHS of an explicit lambda bound by a recursive "let".
+--    Reason: it is tantamount to inlining the body one time. Note that we don't care about non-lambdas (we don't
+--    pay for inlining them) or non-values (we don't put a copy of a non-value in the heap along with the RHS).
+--
+--    If there isn't enough left, what do we do?? Obvious answer: lambda abstract over the function name.
+--    Better(?) answer: add it as a let-bound Nothing to the heap, so the resulting h-function is trapped by the residual letrec...
+
+-- TODO: pre-transforming (case e1 of y { C z -> e2[z] }) to case (case e1 of y { C z -> z }) of z -> e2[z]
+-- might help us replace CPR more because even if we generalise away the e2[z] we potentially keep the unboxing.
+-- Probably can't/shouldn't do this if the wildcard binder y is used in the RHS.
+
+import Supercompile.GHC
+import Supercompile.StaticFlags
+import Supercompile.Utilities
+import qualified Supercompile.Core.Syntax as S
+import qualified Supercompile.Core.FreeVars as S
+import qualified Supercompile.Evaluator.Evaluate as S (shouldExposeUnfolding)
+import qualified Supercompile.Drive.Process1 as S ()
+import qualified Supercompile.Drive.Process2 as S ()
+import qualified Supercompile.Drive.Process3 as S
+
+import BasicTypes
+import CoreSyn
+import CoreFVs    (exprFreeVars)
+import CoreUtils  (exprType)
+import MkCore     (mkWildValBinder)
+import Coercion   (isCoVar, mkCoVarCo, mkAxInstCo, mkSymCo)
+import DataCon    (dataConAllTyVars, dataConRepArgTys, dataConTyCon, dataConWorkId)
+import VarSet
+import Var        (tyVarKind)
+import Id
+import MkId       (realWorldPrimId)
+import FastString (fsLit)
+import PrimOp     (primOpSig)
+import TcType     (tcSplitDFunTy)
+import Type       (mkTyVarTy, mkTyConApp)
+import TysPrim    (realWorldStatePrimTy)
+import TysWiredIn (tupleTyCon, tupleCon)
+import TyCon      (newTyConCo_maybe)
+
+import qualified Data.Map as M
+
+type FlatCoreBinds = [(Id, CoreExpr)]
+
+-- Split input bindings into two lists:
+--  1) CoreBinds binding variables with at least one binder marked by the predicate,
+--     and any CoreBinds that those CoreBinds transitively refer to
+--  2) The remaining CoreBinds. These may refer to those CoreBinds but are not referred
+--     to *by* them
+--
+-- NB: assumes no-shadowing at the top level. I don't want to have to rename stuff to
+-- commute CoreBinds...
+partitionBinds :: (Id -> Bool) -> FlatCoreBinds -> (FlatCoreBinds, FlatCoreBinds)
+partitionBinds should_sc initial_binds = go initial_inside initial_undecided
+  where
+    (initial_inside, initial_undecided) = partition (should_sc . fst) initial_binds
+    
+    go :: FlatCoreBinds -> FlatCoreBinds -> (FlatCoreBinds, FlatCoreBinds)
+    go inside undecided
+        | null inside' = (inside, undecided)
+        | otherwise    = first (inside ++) $ go inside' undecided'
+      where
+        -- Move anything inside that is referred to by a binding that was moved inside last round
+        inside_fvs = coreBindsFVs inside
+        (inside', undecided') = partition (\(x, _) -> x `elemVarSet` inside_fvs) undecided
+
+coreBindsFVs :: FlatCoreBinds -> S.FreeVars
+coreBindsFVs bs = unionVarSets [S.idBndrFreeVars x `unionVarSet` exprFreeVars e | (x, e) <- bs]
+
+coreBindsToCoreTerm :: (Id -> Bool) -> FlatCoreBinds -> (CoreExpr, Var -> FlatCoreBinds)
+coreBindsToCoreTerm should_sc binds
+  = pprTrace "coreBindsToCoreTerm" (hang (text "Supercompiling")     2 (ppr (map fst sc_binds)) $$
+                                    hang (text "Not supercompiling") 2 (ppr (map fst dont_sc_binds))) $
+    (Let (Rec internal_sc_binds) (mkLiftedVarTup sc_internal_xs),
+     \y -> [(x, mkLiftedTupleSelector sc_internal_xs internal_x (Var y)) | (x, internal_x) <- sc_xs_internal_xs] ++ dont_sc_binds)
+  where
+    -- We put all the sc_binds into a local let, and use unboxed tuples to bind back to the top level the names of
+    -- any of those sc_binds that are either exported *or* in the free variables of something from dont_sc_binds.
+    -- Making that list as small as possible allows the supercompiler to determine that more things are used linearly.
+    --
+    -- We used to use a standard "big tuple" to do the binding-back, but this breaks down if we need to include
+    -- some variables of unlifted type (of kind #) or a dictionary (of kind Constraint) since the type arguments of
+    -- the (,..,) tycon must be of kind *. The unlifted case isn't important (they can't occur at top level), but
+    -- the Constraint case is a killer.
+    --
+    -- Then I tried to use a church-encoded tuple to do that, where the tuple (x, y, z) is encoded as
+    -- /\(a :: ArgTypeKind). \(k :: x_ty -> y_ty -> z_ty -> a). k x y z
+    -- And selected from by applying an appropriate type argument and continuation. Unfortunately, this type polymorphism,
+    -- while permitted by the type system, is an illusion: abstraction over types of kinds other than * only works
+    -- if the type abstractions all are beta-reduced away before code generation.
+    --
+    -- Another problem with this second approach is that GHC's inlining heuristics didn't tend to inline very
+    -- large encoded tuples even with explicit continutaion args, because the contination binder didn't get a
+    -- large enough discount.
+    --
+    -- My third attempt just encodes it as an unboxed tuple, which we contrive to buind at the top level by abstracting
+    -- it over a useless arg of void representation.
+    (sc_binds, dont_sc_binds) = partitionBinds should_sc binds -- FIXME: experiment with just taking annotated binds, and relying on unfoldings for the rest (problematic for non-values, though!)
+    dont_sc_binds_fvs = coreBindsFVs dont_sc_binds
+    
+    -- We should zap fragile information on the Ids' we use within the tuple selector. The reasons are:
+    --  1. They may be mutually inter-referring, and the binders of a "case" are not simultaneously brought into scope
+    --  2. For some reason, GHC seems to have trouble optimising (let x = y in x) to (y) if x has an unfolding.
+    zappedBindersOfBinds = map (zapFragileIdInfo . fst)
+
+    -- This is a sweet hack. Most of the top-level binders will be External names. It is a Bad Idea to locally-bind
+    -- an External name, because several Externals with the same name but different uniques will generate clashing
+    -- C labels at code-generation time (the unique is not included in the label).
+    --
+    -- To work around this, we deexternalise the variables at the *local binding sites* we are about to create.
+    -- Note that we leave the *use sites* totally intact: we rely on the fact that a) variables are compared only by
+    -- unique and b) the internality of these names will be carried down on the next simplifier run, so this works.
+    -- The ice is thin, though!
+    sc_xs = zappedBindersOfBinds sc_binds
+    -- NB: if we don't mark these Ids as not exported then we get lots of residual top-level bindings of the form x = y
+    internal_sc_binds = map (first localiseId) sc_binds
+    -- Decide which things we should export from the supercompiled term using a Church tuple.
+    -- We need to export to the top level of the module those bindings that are *any* of:
+    --   1. Are exported by the module itself
+    --   2. Are free variables of the non-supercompiled bindings
+    --   3. Are free variables of the var binder for another top-level-exported thing
+    go exported exported' undecided
+       | null exported' = exported
+       | otherwise      = go (exported' ++ exported) exported'' undecided'
+      where (exported'', undecided') = partition (\(x, _) -> x `elemVarSet` exported_xs') undecided
+            exported_xs' = unionVarSets (map (S.idBndrFreeVars . fst) exported')
+    sc_xs_internal_xs = uncurry (go []) (partition (\(x, _) -> isExportedId x || x `elemVarSet` dont_sc_binds_fvs) (sc_xs `zip` zappedBindersOfBinds internal_sc_binds))
+    sc_internal_xs = map snd sc_xs_internal_xs
+
+
+-- NB: I can't see any GHC code that prevents nullary unboxed tuples, but I'm not actually sure they work
+-- (note that in particular they get the same OccName as the unary versions).
+mkLiftedVarTup :: [Id] -> CoreExpr
+mkLiftedVarTup xs = Lam (mkWildValBinder realWorldStatePrimTy) $ Var (dataConWorkId (tupleCon UnboxedTuple (length xs))) `mkTyApps` map idType xs `mkVarApps` xs
+
+mkLiftedTupleSelector :: [Id] -> Id -> CoreExpr -> CoreExpr
+mkLiftedTupleSelector xs want_x tup_e
+  = Case (tup_e `App` Var realWorldPrimId) (mkWildValBinder (mkTyConApp (tupleTyCon UnboxedTuple n) (map idType xs))) (idType want_x)
+         [(DataAlt (tupleCon UnboxedTuple n), xs, Var want_x)]
+  where n = length xs
+
+termUnfoldings :: {-(Module -> ModIface) ->-} S.Term -> [(Var, S.Term)]
+termUnfoldings {-mod_finder-} e = go (S.termFreeVars e) emptyVarSet [] []
+  where
+    go new_fvs all_fvs all_xwhy_nots all_xes
+      | isEmptyVarSet added_fvs = pprTrace "termUnfoldings" (vcat [hang (text why_not <> text ":") 2 (vcat (map ppr xs)) | (why_not, xs) <- groups snd fst all_xwhy_nots]) $
+                                  all_xes
+      | otherwise               = go (unionVarSets (map (\(x, e) -> S.idBndrFreeVars x `unionVarSet` S.termFreeVars e) added_xes)) (all_fvs `unionVarSet` added_fvs)
+                                     (added_xwhy_nots ++ all_xwhy_nots) (added_xes ++ all_xes)
+      where added_fvs = new_fvs `minusVarSet` all_fvs
+            (added_xwhy_nots, added_xes)
+              = foldVarSet (\x (xwhy_nots, xes) -> case varUnfolding x of
+                                                     Left why_not | isPrimOpId x || isJust (isFCallId_maybe x)
+                                                                  -> (             xwhy_nots,        xes) -- Suppress noisy errors
+                                                                  | otherwise
+                                                                  -> ((x, why_not):xwhy_nots,        xes)
+                                                     Right e      -> (             xwhy_nots, (x, e):xes))
+                           ([], []) added_fvs
+
+    {-
+    -- Returns true for function name like workers which are not typed by the user but tend to be exported into interface files
+    x `probablyWorkerFor` y
+      | Just mod_x <- nameModule_maybe (varName x)
+      , Just mod_y <- nameModule_maybe (varName y)
+      , mod_x == mod_y
+      -- Both names in the same module! Now just check that x was not actually originally exported by that module.
+      -- FIXME: this doesn't work because we might have a user-written but non-exported helper, we don't want
+      -- to ignore the SUPERINLINABLE pragma on that!!
+      , let iface = mod_finder mod_x
+            mod_exports_set = availsToNameSet (mi_exports iface)
+      = not $ varName x `elemNameSet` mod_exports_set
+      | otherwise
+      = False
+    -}
+
+    -- NB: at this point we have already done prepareTerm, so used local bindings will be pushed into "e"
+    -- already. Thus all this code basically only affects imported functions. In this way, we exactly match
+    -- the behaviour of GHC's current Specialise pass, which:
+    --  * Exhaustively specialises *locally defined* functions on their dictionary arguments
+    --  * Specialises those *imported* functions that are marked Inlineable
+    --
+    -- NB: it is not sufficient to only check shouldExposeUnfolding here, because a non-recursive function
+    -- might have a *nested* recursive function, and we may want to prevent inlining of that one as well.
+    -- We still do check shouldExposeUnfolding here because we can avoid parsing+tagging those unfoldings
+    -- which can literall never be used.
+    varUnfolding x
+      -- NB: probably want to ensure these are all considered superinlinable by shouldExposeUnfolding for the evaluator
+      | Just pop <- isPrimOpId_maybe x     = Right $ primOpUnfolding pop
+      | Just dc <- isDataConWorkId_maybe x = dataUnfolding dc
+      | otherwise                          = case S.shouldExposeUnfolding x of
+        Left why_not -> Left why_not
+        Right super  -> case realIdUnfolding x of
+          NoUnfolding                   -> Left "no unfolding"
+          OtherCon _                    -> Left "no positive unfolding"
+          DFunUnfolding _ dc es         -> Right $ runParseM us2 $ coreExprToTerm $ mkLams as $ mkLams xs $ Var (dataConWorkId dc) `mkTyApps` cls_tys `mkApps` [(e `mkTyApps` map mkTyVarTy as) `mkVarApps` xs | e <- es]
+           where (as, theta, _cls, cls_tys) = tcSplitDFunTy (idType x)
+                 xs = zipWith (mkSysLocal (fsLit "x")) bv_uniques theta
+          CoreUnfolding { uf_tmpl = e } -> Right $ superinlinableLexically super $ runParseM us2 $ coreExprToTerm e
+           -- NB: it's OK if the unfolding is a non-value, as the evaluator won't inline LetBound non-values
+    
+    primOpUnfolding pop = S.tyLambdas as $ S.lambdas xs $ S.primOp pop (map mkTyVarTy as) (map S.var xs)
+      where (as, arg_tys, _res_ty, _arity, _strictness) = primOpSig pop
+            xs = zipWith (mkSysLocal (fsLit "x")) bv_uniques arg_tys
+    
+    dataUnfolding dc
+      | Just co_axiom <- newTyConCo_maybe (dataConTyCon dc)
+      , let [x] = xs
+      = Right $ S.tyLambdas as $ S.lambdas [x] $ S.var x `S.cast` mkSymCo (mkAxInstCo co_axiom (map mkTyVarTy as)) -- Axiom LHS = TyCon, RHS = Rep Type
+      | any (not . S.canAbstractOverTyVarOfKind . tyVarKind) as
+      = Left "some type variable which we cannot abstract over"
+      | otherwise
+      = Right $ S.tyLambdas as $ S.lambdas xs $ S.value (S.Data dc (map mkTyVarTy as) (map mkCoVarCo qs) ys)
+      where as = dataConAllTyVars dc
+            arg_tys = dataConRepArgTys dc
+            xs = zipWith (mkSysLocal (fsLit "x")) bv_uniques arg_tys
+            (qs, ys) = span isCoVar xs
+
+    -- We need a UniqSupply so we can generate Uniques for datacon/primop/user unfoldings. It doesn't really matter
+    -- that the binders we generate here may shadow things above, but we have to be careful with our use of anfUniqSupply'
+    -- when we call runParseM to deal with user unfoldings. The reason is that coreExprToTerm assumes that no free variables
+    -- of the CoreExpr have Uniques generated by the unique supply it is passed.
+    --
+    -- This meant that when runParseM used to unconditionally use anfUniqSupply' for Uniques we had a stupid bug, because
+    -- we were also using the uniques from anfUniqueSupply to generate lambda-binders in the DFunUnfolding case.
+    -- All we needed to do to fix this was to make sure we split off a seperate UniqSupply for generating the lambda-bindings
+    -- than we pass down to runParseM. 
+    (us1, us2) = splitUniqSupply anfUniqSupply'
+    bv_uniques = uniqsFromSupply us1
+
+-- NB: this is used to deal with SUPERINLINABLE bindings which have locally bound loops which
+-- are *not* marked SUPERINLINABLE
+--
+-- NB: for this to work properly, coreExprToTerm must not float
+-- stuff that was lexically within a binding out of that binding!
+--
+-- TODO: this is actually useless if we just say that all InternallyBound things are SUPERINLINABLE
+superinlinableLexically :: Superinlinable -> S.Term -> S.Term
+--superinlinableLexically = id
+{--}
+superinlinableLexically ctxt = term
+  where
+    term e = flip fmap e $ \e -> case e of
+      S.Var x -> S.Var x
+      S.Value v -> S.Value $ case v of
+        S.Lambda   x e -> S.Lambda   x (term e)
+        S.TyLambda a e -> S.TyLambda a (term e)
+        _              -> v
+      S.TyApp e ty -> S.TyApp (term e) ty
+      S.CoApp e co -> S.CoApp (term e) co
+      S.App   e x  -> S.App   (term e) x
+      S.PrimOp pop tys es -> S.PrimOp pop tys (map term es)
+      S.Case e x ty alts  -> uncurry (flip S.Case) (pair (x, e)) ty (map (second term) alts)
+      S.Let x e1 e2       -> uncurry S.Let (pair (x, e1)) (term e2)
+      S.LetRec xes e      -> S.LetRec (map pair xes) (term e)
+      S.Cast e co         -> S.Cast (term e) co
+
+    pair (x, e) | not ctxt  = case S.shouldExposeUnfolding x of Right True -> (x, superinlinableLexically True e)
+                                                                _          -> (x, term e)
+                | otherwise = (x', term e)
+      where x' = x `setInlinePragma` (idInlinePragma x) { inl_inline = case inl_inline (idInlinePragma x) of
+                                                                          Inline          -> Inline
+                                                                          Inlinable _     -> Inlinable True
+                                                                          NoInline        -> NoInline
+                                                                          EmptyInlineSpec -> Inlinable True }
+{--}
+
+
+
+supercompile :: {-(Module -> ModIface) -> -} CoreExpr -> IO CoreExpr
+supercompile {-mod_finder-} e = -- liftM (termToCoreExpr . snd) $
+                 return $ termToCoreExpr $
+                 S.supercompile (M.fromList unfs) e'
+  where unfs = termUnfoldings {-mod_finder-} e'
+        -- NB: ensure we mark any child bindings of bindings marked SUPERINLINABLE in *this module* as SUPERINLINABLE,
+        -- just like we would if we imported a SUPERINLINABLE binding
+        e' = superinlinableLexically mODULE_SUPERINLINABLE $ runParseM anfUniqSupply' $ coreExprToTerm e
+
+supercompileProgram :: [CoreBind] -> IO [CoreBind]
+supercompileProgram binds = do
+    {-mod_finder <- mkModuleFinder-}
+    supercompileProgramSelective {-mod_finder-} selector binds
+  where selector | any idSupercompilePragma (bindersOfBinds binds) = idSupercompilePragma
+                 | otherwise                                       = const True
+
+{-
+mkModuleFinder :: CoreM (Module -> ModIface)
+mkModuleFinder = do
+    hsc_env <- getHscEnv
+    eps <- liftIO $ hscEPS hsc_env
+    let hpt = hsc_HPT hsc_env
+        dflags = hsc_dflags hsc_env
+    -- All referenced modules should be loaded by this point, so this should always succeed:
+    return $ \mod -> case lookupIfaceByModule dflags hpt (eps_PIT eps) mod of
+      Nothing    -> panic "mkModuleFinder"
+      Just iface -> iface
+-}
+
+supercompileProgramSelective :: {-(Module -> ModIface) ->-} (Id -> Bool) -> [CoreBind] -> IO [CoreBind]
+supercompileProgramSelective {-mod_finder-} should_sc binds = liftM (\e' -> [Rec $ (x, e') : rebuild x]) (supercompile {-mod_finder-} e)
+  where x = mkSysLocal (fsLit "sc") topUnique (exprType e)
+        -- NB: we assume no-shadowing at top level, which is probably reasonable
+        flat_binds = flattenBinds binds
+        (e, rebuild) = ASSERT(length (nub (map fst flat_binds)) == length flat_binds)
+                       coreBindsToCoreTerm should_sc flat_binds

compiler/supercompile/Supercompile/Core/FreeVars.hs

+{-# LANGUAGE Rank2Types #-}
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+module Supercompile.Core.FreeVars (
+    module Supercompile.Core.FreeVars,
+    module VarSet,
+    tyVarsOfType, tyVarsOfTypes, tyCoVarsOfCo
+  ) where
+
+import Supercompile.Core.Syntax
+
+import Supercompile.Utilities
+
+import CoreFVs
+import CoreSyn  (CoreRule(..))
+import VarSet
+import Coercion (tyCoVarsOfCo)
+import Var      (Id, TyVar)
+import Id       (isId, idSpecialisation, realIdUnfolding)
+import IdInfo   (specInfoRules)
+import Type     (tyVarsOfType, tyVarsOfTypes)
+
+
+type FreeVars = VarSet
+type BoundVars = VarSet
+
+
+varBndrFreeVars :: Var -> FreeVars
+varBndrFreeVars x | isId x    = idBndrFreeVars x
+                  | otherwise = tyVarBndrFreeVars x
+
+-- We have our own version of idFreeVars so we can treat global variables as free
+idBndrFreeVars :: Id -> FreeVars
+idBndrFreeVars x = varTypeTyVars x `unionVarSet` -- No global tyvars, so no problem
+                   rulesFreeVars (specInfoRules (idSpecialisation x)) `unionVarSet`
+                   (stableUnfoldingVars (const True) (realIdUnfolding x) `orElse` emptyVarSet)
+  where
+    rulesFreeVars :: [CoreRule] -> VarSet
+    rulesFreeVars rules = foldr (unionVarSet . ruleFreeVars) emptyVarSet rules
+
+    ruleFreeVars :: CoreRule -> VarSet
+    ruleFreeVars (BuiltinRule {}) = emptyVarSet
+    ruleFreeVars (Rule { ru_fn = _, ru_bndrs = bndrs, ru_rhs = rhs, ru_args = args })
+      = nonRecBindersFreeVars bndrs (exprsSomeFreeVars (const True) (rhs:args))
+
+tyVarBndrFreeVars :: TyVar -> FreeVars
+tyVarBndrFreeVars = varTypeTyVars -- No global tyvars, so no problem
+
+
+(varFreeVars',                termFreeVars,                termFreeVars',                altsFreeVars,                valueFreeVars,                valueFreeVars')                = mkFreeVars (\f (I e) -> f e)
+(fvedVarFreeVars',            fvedTermFreeVars,            fvedTermFreeVars',            fvedAltsFreeVars,            fvedValueFreeVars,            fvedValueFreeVars')            = mkFreeVars (\_ (FVed fvs _) -> fvs)
+(sizedFVedVarFreeVars',       sizedFVedTermFreeVars,       sizedFVedTermFreeVars',       sizedFVedAltsFreeVars,       sizedFVedValueFreeVars,       sizedFVedValueFreeVars')       = mkFreeVars (\_ (Comp (Sized _ (FVed fvs _))) -> fvs)
+(taggedVarFreeVars',          taggedTermFreeVars,          taggedTermFreeVars',          taggedAltsFreeVars,          taggedValueFreeVars,          taggedValueFreeVars')          = mkFreeVars (\f (Tagged _ e) -> f e)
+(taggedSizedFVedVarFreeVars', taggedSizedFVedTermFreeVars, taggedSizedFVedTermFreeVars', taggedSizedFVedAltsFreeVars, taggedSizedFVedValueFreeVars, taggedSizedFVedValueFreeVars') = mkFreeVars (\_ (Comp (Tagged _ (Comp (Sized _ (FVed fvs _))))) -> fvs)
+
+{-# INLINE mkFreeVars #-}
+mkFreeVars :: (forall a. (a -> FreeVars) -> ann a -> FreeVars)
+           -> (Var              -> FreeVars,
+               ann (TermF ann)  -> FreeVars,
+               TermF ann        -> FreeVars,
+               [AltF ann]       -> FreeVars,
+               ann (ValueF ann) -> FreeVars,
+               ValueF ann       -> FreeVars)
+mkFreeVars rec = (unitVarSet, term, term', alternatives, value, value')
+  where
+    term = rec term'
+    term' (Var x)            = unitVarSet x
+    term' (Value v)          = value' v
+    term' (TyApp e ty)       = tyVarsOfType ty `unionVarSet` term e
+    term' (CoApp e co)       = term e `unionVarSet` tyCoVarsOfCo co
+    term' (App e x)          = term e `extendVarSet` x
+    term' (PrimOp _ tys es)  = unionVarSets (map tyVarsOfType tys) `unionVarSet` unionVarSets (map term es)
+    term' (Case e x ty alts) = tyVarsOfType ty `unionVarSet` term e `unionVarSet` nonRecBinderFreeVars x (alternatives alts)
+    term' (Let x e1 e2)      = term e1 `unionVarSet` nonRecBinderFreeVars x (term e2)
+    term' (LetRec xes e)     = (unionVarSets (map term es) `unionVarSet` term e `unionVarSet` unionVarSets (map idBndrFreeVars xs)) `delVarSetList` xs
+      where (xs, es) = unzip xes
+    term' (Cast e co)        = term e `unionVarSet` tyCoVarsOfCo co
+    
+    value = rec value'
+    value' = valueGFreeVars' term
+    
+    alternatives = unionVarSets . map alternative
+    
+    alternative (altcon, e) = altConFreeVars altcon $ term e
+
+valueGFreeVars' :: (a -> FreeVars) -> ValueG a -> FreeVars
+valueGFreeVars' term (TyLambda x e)      = nonRecBinderFreeVars x (term e)
+valueGFreeVars' term (Lambda x e)        = nonRecBinderFreeVars x (term e)
+valueGFreeVars' _    (Data _ tys cos xs) = unionVarSets (map tyVarsOfType tys) `unionVarSet` unionVarSets (map tyCoVarsOfCo cos) `unionVarSet` mkVarSet xs
+valueGFreeVars' _    (Literal _)         = emptyVarSet
+valueGFreeVars' _    (Coercion co)       = tyCoVarsOfCo co
+
+nonRecBinderFreeVars :: Var -> FreeVars -> FreeVars
+nonRecBinderFreeVars x fvs = (fvs `delVarSet` x) `unionVarSet` varBndrFreeVars x
+
+nonRecBindersFreeVars :: [Var] -> FreeVars -> FreeVars
+nonRecBindersFreeVars xs = flip (foldr nonRecBinderFreeVars) xs
+
+-- Returns the most tightly binding variable last
+altConBoundVars :: AltCon -> [Var]
+altConBoundVars (DataAlt _ as qs xs) = as ++ qs ++ xs
+altConBoundVars (LiteralAlt _)       = []
+altConBoundVars _                    = []
+
+altConFreeVars :: AltCon -> FreeVars -> FreeVars
+altConFreeVars (DataAlt _ as qs xs) = (`delVarSetList` as) . nonRecBindersFreeVars (qs ++ xs)
+altConFreeVars (LiteralAlt _)       = id
+altConFreeVars DefaultAlt           = id
+
+
+coercedFreeVars :: (a -> FreeVars) -> Coerced a -> FreeVars
+coercedFreeVars f (cast_by, x) = f x `unionVarSet` castByFreeVars cast_by
+
+castByFreeVars :: CastBy -> FreeVars
+castByFreeVars Uncast        = emptyVarSet
+castByFreeVars (CastBy co _) = tyCoVarsOfCo co
+
+
+data FVed a = FVed { freeVars :: !FreeVars, fvee :: !a }
+
+instance Copointed FVed where
+    extract = fvee
+
+instance Functor FVed where
+    fmap f (FVed fvs x) = FVed fvs (f x)
+
+instance Foldable FVed where
+    foldMap f (FVed _ x) = f x
+
+instance Traversable FVed where
+    traverse f (FVed fvs x) = pure (FVed fvs) <*> f x
+
+instance Show1 FVed where
+    showsPrec1 prec (FVed fvs x) = showParen (prec >= appPrec) (showString "FVed" . showsPrec appPrec (varSetElems fvs) . showsPrec appPrec x)
+
+instance Eq1 FVed where
+    eq1 (FVed fvs1 x1) (FVed fvs2 x2) = varSetElems fvs1 == varSetElems fvs2 && x1 == x2
+
+instance Ord1 FVed where
+    compare1 (FVed fvs1 x1) (FVed fvs2 x2) = (x1, varSetElems fvs1) `compare` (x2, varSetElems fvs2)
+
+instance Outputable1 FVed where
+    pprPrec1 prec (FVed _ x) = pprPrec prec x
+
+instance OutputableLambdas1 FVed where
+    pprPrecLam1 (FVed _ x) = pprPrecLam x
+
+instance Show a => Show (FVed a) where
+    showsPrec = showsPrec1
+
+instance Eq a => Eq (FVed a) where
+    (==) = eq1
+
+instance Ord a => Ord (FVed a) where
+    compare = compare1
+
+instance Outputable a => Outputable (FVed a) where
+    pprPrec = pprPrec1
+
+
+type FVedTerm = FVed (TermF FVed)
+type FVedAlt = AltF FVed
+type FVedValue = ValueF FVed
+
+
+instance Symantics FVed where
+    var = fvedTerm . Var
+    value = fmap Value . fvedValue
+    tyApp e = fvedTerm . TyApp e
+    coApp e = fvedTerm . CoApp e
+    app e = fvedTerm . App e
+    primOp pop tys = fvedTerm . PrimOp pop tys
+    case_ e x ty = fvedTerm . Case e x ty
+    let_ x e1 = fvedTerm . Let x e1
+    letRec xes = fvedTerm . LetRec xes
+    cast e = fvedTerm . Cast e
+
+fvedVar :: Var -> FVed Var
+fvedVar x = FVed (taggedVarFreeVars' x) x
+
+fvedValue :: ValueF FVed -> FVed FVedValue
+fvedValue v = FVed (fvedValueFreeVars' v) v
+
+fvedTerm :: TermF FVed -> FVedTerm
+fvedTerm e = FVed (fvedTermFreeVars' e) e

compiler/supercompile/Supercompile/Core/Renaming.hs

+{-# LANGUAGE Rank2Types #-}
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+module Supercompile.Core.Renaming (
+    -- | Renamings
+    Renaming, emptyRenaming,
+    mkInScopeIdentityRenaming, mkIdentityRenaming, mkTyVarRenaming, mkRenaming,
+    InScopeSet, emptyInScopeSet, mkInScopeSet,
+    
+    -- | PreRenamings
+    PreRenaming, invertRenaming, composeRenamings,
+    restrictRenaming,
+
+    -- | Extending the renaming
+    insertVarRenaming,
+    insertIdRenaming, insertIdRenamings,
+    insertTypeSubst, insertTypeSubsts,
+    insertCoercionSubst, insertCoercionSubsts,
+    
+    -- | Querying the renaming
+    renameId, lookupTyVarSubst, lookupCoVarSubst,
+    
+    -- | Things with associated renamings
+    In, Out,
+
+    -- | Renaming variables occurrences and binding sites
+    inFreeVars, renameFreeVars, renameIn,
+    renameType, renameCoercion,
+    renameBinders, renameNonRecBinder, renameNonRecBinders,
+    renameBounds, renameNonRecBound,
+    
+    -- | Renaming actual bits of syntax
+    renameValueG, renameAltCon,
+    renameTerm,                renameAlts,                renameValue,                renameValue',
+    renameFVedTerm,            renameFVedAlts,            renameFVedValue,            renameFVedValue',
+    renameTaggedTerm,          renameTaggedAlts,          renameTaggedValue,          renameTaggedValue',
+    renameTaggedSizedFVedTerm, renameTaggedSizedFVedAlts, renameTaggedSizedFVedValue, renameTaggedSizedFVedValue'
+  ) where
+
+import Supercompile.Core.FreeVars
+import Supercompile.Core.Syntax
+
+import Supercompile.Utilities
+
+import CoreSubst
+import OptCoercion (optCoercion)
+import Coercion    (CvSubst(..), CvSubstEnv, isCoVar, mkCoVarCo, getCoVar_maybe)
+import qualified CoreSyn as CoreSyn (CoreExpr, Expr(Var))
+import Type        (mkTyVarTy, getTyVar_maybe)
+import Id          (mkSysLocal)
+import Var         (Id, TyVar, CoVar, isTyVar, mkTyVar, varType, isGlobalId, varUnique)
+import OccName     (occNameFS)
+import Name        (getOccName, mkSysTvName)
+import FastString  (FastString)
+import UniqFM      (ufmToList)
+import VarEnv
+
+import Control.Monad.Fix (mfix)
+
+import qualified Data.Map as M
+
+
+-- We are going to use GHC's substitution type in a rather stylised way, and only
+-- ever substitute variables for variables. The reasons for this are twofold:
+--
+--  1. Particularly since we are in ANF, doing any other sort of substitution is unnecessary
+--
+--  2. We have our own syntax data type, and we don't want to build a GHC syntax tree just
+--     for insertion into the Subst if we can help it!
+--
+-- Unfortunately, in order to make this work with the coercionful operational semantics
+-- we will sometimes need to substitute coerced variables for variables. An example would be
+-- when reducing:
+--
+--  (\x. e) |> gam y
+--
+-- Where
+--
+--  gam = (F Int -> F Int ~ Bool -> Bool)
+--
+-- We need to reduce to something like:
+--
+--  e[(y |> sym (nth 1 gam))/x] |> (nth 2 gam)
+--
+-- We deal with this problem in the evaluator by introducing an intermediate let binding for
+-- such redexes.
+
+type Renaming = (IdSubstEnv, TvSubstEnv, CvSubstEnv)
+
+joinSubst :: InScopeSet -> Renaming -> Subst
+joinSubst iss (id_subst, tv_subst, co_subst) = mkSubst iss tv_subst co_subst id_subst
+
+-- GHC's binder-renaming stuff does this awful thing where a var->var renaming
+-- will always be added to the InScopeSet (which is really an InScopeMap) but
+-- will only be added to the IdSubstEnv *if the unique changes*.
+--
+-- This is a problem for us because we only store the Renaming with each In thing,
+-- not the full Subst. So we might lose some renamings recorded only in the InScopeSet.
+--
+-- The solution is either:
+--  1) Rewrite the rest of the supercompiler so it stores a Subst with each binding.
+--     Given the behaviour of GHCs binder-renamer, this is probably cleaner (and matches
+--     what the GHC does), but I'm not really interested in doing that work right now.
+--
+--     It also means you have te be very careful to join together InScopeSets if you
+--     pull one of those Subst-paired things down into a strictly deeper context. This
+--     is easy to get wrong.
+--
+--  2) Ensure that we always extend the IdSubstEnv, regardless of whether the unique changed.
+--     This is the solution I've adopted, and it is implemented here in splitSubst:
+splitSubst :: Subst -> [(Var, Var)] -> (InScopeSet, Renaming)
+splitSubst (Subst iss id_subst tv_subst co_subst) extend
+  = (iss, foldVarlikes (\f -> foldr (\x_x' -> f (fst x_x') x_x')) extend
+                       (\(x, x') -> first3  (\id_subst -> extendVarEnv id_subst x (mkIdExpr x')))
+                       (\(a, a') -> second3 (\tv_subst -> extendVarEnv tv_subst a (mkTyVarTy a')))
+                       (\(q, q') -> third3  (\co_subst -> extendVarEnv co_subst q (mkCoVarCo q')))
+                       (id_subst, tv_subst, co_subst))
+
+-- NB: this used to return a triple of lists, but I introduced this version due to profiling
+-- results that indicated a caller (renameFreeVars) was causing 2% of all allocations. It turns
+-- out that I managed to achieve deforestation in all of the callers by rewriting them to use this
+-- version instead.
+{-# INLINE foldVarlikes #-}
+foldVarlikes :: ((Var -> a -> b -> b) -> b -> f_a -> b)
+             -> f_a
+             -> (a -> b -> b) -- Id continuation
+             -> (a -> b -> b) -- TyVar continuation
+             -> (a -> b -> b) -- CoVar continuation
+             -> b -> b
+foldVarlikes fold as id tv co acc = fold go acc as
+  where go x a res | isTyVar x = tv a res
+                   | isCoVar x = co a res
+                   | otherwise = id a res
+
+emptyRenaming :: Renaming
+emptyRenaming = (emptyVarEnv, emptyVarEnv, emptyVarEnv)
+
+mkIdentityRenaming :: FreeVars -> Renaming
+mkIdentityRenaming fvs = foldVarlikes (\f -> foldVarSet (\x -> f x x)) fvs
+                                      (\x -> first3  (\id_subst -> extendVarEnv id_subst x (mkIdExpr x)))
+                                      (\a -> second3 (\tv_subst -> extendVarEnv tv_subst a (mkTyVarTy a)))
+                                      (\q -> third3  (\co_subst -> extendVarEnv co_subst q (mkCoVarCo q)))
+                                      (emptyVarEnv, emptyVarEnv, emptyVarEnv)
+
+mkInScopeIdentityRenaming :: InScopeSet -> Renaming
+mkInScopeIdentityRenaming = mkIdentityRenaming . getInScopeVars
+
+mkTyVarRenaming :: [(TyVar, Type)] -> Renaming
+mkTyVarRenaming aas = (emptyVarEnv, mkVarEnv aas, emptyVarEnv)
+
+mkRenaming :: M.Map Var Var -> Renaming
+mkRenaming rn = foldVarlikes (\f -> M.foldWithKey (\x x' -> f x (x, x'))) rn
+                             (\(x, x') -> first3  (\id_subst -> extendVarEnv id_subst x (mkIdExpr x')))
+                             (\(a, a') -> second3 (\tv_subst -> extendVarEnv tv_subst a (mkTyVarTy a')))
+                             (\(q, q') -> third3  (\co_subst -> extendVarEnv co_subst q (mkCoVarCo q')))
+                             (emptyVarEnv, emptyVarEnv, emptyVarEnv)
+
+type PreRenaming = (VarEnv Id, VarEnv TyVar, VarEnv CoVar)
+
+-- NB: the output Vars in the range of the mappings are dodgy and should really only be used for
+-- their Uniques. I turn them into full Ids mostly for convenience.
+--
+-- NB: the InScopeSet should be that of the *domain* of the renaming (I think!)
+--
+-- NB: I used to return a real *Renaming* as the result, but that wasn't very convenient for the MSG caller:
+--  1. It hides the fact that looking up a CoVar/TyVar always yields a variable
+--  2. It doesn't let us easily test if a variable is actually present in the domain of the inverted renaming
+invertRenaming :: InScopeSet -> Renaming -> Maybe PreRenaming
+invertRenaming ids (id_subst, tv_subst, co_subst)
+  = mfix $ \rn -> let -- FIXME: this inversion relies on something of a hack because the domain of the mapping is not stored (only its Unique)
+                      -- Furthermore, we want to carefully rename the *types* (and extra info, if we actually preserved any) as well when doing
+                      -- this inversion so that the renaming {a |-> b, y |-> x :: b} is inverted to {b |-> a, x |-> y :: a}
+                      invertVarEnv :: (FastString -> Unique -> Type -> Var)
+                                   -> VarEnv Var -> Maybe (VarEnv Var)
+                      invertVarEnv mk env
+                        | distinct (varEnvElts env) = Just (mkVarEnv [ (x, if isGlobalId x && u == varUnique x
+                                                                            then x -- So we don't replace global Ids with new local Ids!
+                                                                            else mk (occNameFS (getOccName x)) u (renameType ids (mkRenaming' rn) (varType x)))
+                                                                     | (u, x) <- ufmToList env])
+                        | otherwise                 = Nothing
+                  in liftM3 (,,) (traverse getId_maybe    id_subst >>= invertVarEnv  mkSysLocal)
+                                 (traverse getTyVar_maybe tv_subst >>= invertVarEnv (\fs uniq -> mkTyVar (mkSysTvName uniq fs)))
+                                 (traverse getCoVar_maybe co_subst >>= invertVarEnv mkSysLocal)
+  where
+    mkRenaming' :: PreRenaming -> Renaming
+    mkRenaming' (xxs, aas, qqs) = (mapVarEnv mkIdExpr  xxs,
+                                   mapVarEnv mkTyVarTy aas,
+                                   mapVarEnv mkCoVarCo qqs)
+
+composeRenamings :: PreRenaming -> Renaming -> Renaming
+composeRenamings (id_subst1, tv_subst1, co_subst1) rn2
+  = (mapVarEnv (mkIdExpr . renameId rn2) id_subst1,
+     mapVarEnv (lookupTyVarSubst    rn2) tv_subst1,
+     mapVarEnv (lookupCoVarSubst    rn2) co_subst1)
+
+restrictRenaming :: Renaming -> VarSet -> Renaming
+restrictRenaming (id_subst, tv_subst, co_subst) fvs = (id_subst `restrictVarEnv` fvs, tv_subst `restrictVarEnv` fvs, co_subst `restrictVarEnv` fvs)
+
+mkIdExpr :: Id -> CoreSyn.CoreExpr
+mkIdExpr = CoreSyn.Var
+
+getId_maybe :: CoreSyn.CoreExpr -> Maybe Id
+getId_maybe (CoreSyn.Var x') = Just x'
+getId_maybe _                = Nothing
+
+coreSynToVar :: CoreSyn.CoreExpr -> Var
+coreSynToVar = fromMaybe (panic "renameId" empty) . getId_maybe
+
+insertVarRenaming :: Renaming -> Var -> Out Var -> Renaming
+insertVarRenaming rn x y
+  | isTyVar x = insertTypeSubst     rn x (mkTyVarTy y)
+  | isCoVar x = insertCoercionSubst rn x (mkCoVarCo y)
+  | otherwise = insertIdRenaming    rn x y
+
+insertIdRenaming :: Renaming -> Id -> Out Id -> Renaming
+insertIdRenaming (id_subst, tv_subst, co_subst) x x'
+  = (extendVarEnv id_subst x (mkIdExpr x'), tv_subst, co_subst)
+
+insertIdRenamings :: Renaming -> [(Id, Out Id)] -> Renaming
+insertIdRenamings = foldr (\(x, x') rn -> insertIdRenaming rn x x')
+
+insertTypeSubst :: Renaming -> TyVar -> Out Type -> Renaming
+insertTypeSubst (id_subst, tv_subst, co_subst) x ty' = (id_subst, extendVarEnv tv_subst x ty', co_subst)
+
+insertTypeSubsts :: Renaming -> [(TyVar, Out Type)] -> Renaming
+insertTypeSubsts (id_subst, tv_subst, co_subst) xtys = (id_subst, extendVarEnvList tv_subst xtys, co_subst)
+
+insertCoercionSubst :: Renaming -> CoVar -> Out Coercion -> Renaming
+insertCoercionSubst (id_subst, tv_subst, co_subst) x co' = (id_subst, tv_subst, extendVarEnv co_subst x co')
+
+insertCoercionSubsts :: Renaming -> [(CoVar, Out Coercion)] -> Renaming
+insertCoercionSubsts (id_subst, tv_subst, co_subst) xcos = (id_subst, tv_subst, extendVarEnvList co_subst xcos)
+
+-- NB: these three function can supply emptyInScopeSet because of what I do in splitSubst
+
+renameId :: Renaming -> Id -> Out Id
+renameId rn = coreSynToVar . lookupIdSubst (text "renameId") (joinSubst emptyInScopeSet rn)
+
+lookupTyVarSubst :: Renaming -> TyVar -> Out Type
+lookupTyVarSubst rn = lookupTvSubst (joinSubst emptyInScopeSet rn)
+
+lookupCoVarSubst :: Renaming -> CoVar -> Out Coercion
+lookupCoVarSubst rn = lookupCvSubst (joinSubst emptyInScopeSet rn)
+
+
+type In a = (Renaming, a)
+type Out a = a
+
+
+inFreeVars :: (a -> FreeVars) -> In a -> FreeVars
+inFreeVars thing_fvs (rn, thing) = renameFreeVars rn (thing_fvs thing)
+
+renameFreeVars :: Renaming -> FreeVars -> FreeVars
+renameFreeVars rn fvs = foldVarlikes (\f -> foldVarSet (\x -> f x x)) fvs
+                                     (\x -> flip extendVarSet (renameId rn x))
+                                     (\a -> unionVarSet (tyVarsOfType (lookupTyVarSubst rn a)))
+                                     (\q -> unionVarSet (tyCoVarsOfCo (lookupCoVarSubst rn q)))
+                                     emptyVarSet
+
+renameType :: InScopeSet -> Renaming -> Type -> Type
+renameType iss rn = substTy (joinSubst iss rn)
+
+renameCoercion :: InScopeSet -> Renaming -> Coercion -> NormalCo
+renameCoercion iss (_, tv_subst, co_subst) = optCoercion (CvSubst iss tv_subst co_subst)
+
+
+renameIn :: (Renaming -> a -> a) -> In a -> a
+renameIn f (rn, x) = f rn x
+
+
+renameBinders :: InScopeSet -> Renaming -> [Var] -> (InScopeSet, Renaming, [Var])
+renameBinders iss rn xs = (iss', rn', xs')
+  where (subst', xs') = substRecBndrs (joinSubst iss rn) xs
+        (iss', rn') = splitSubst subst' (xs `zip` xs')
+
+renameNonRecBinder :: InScopeSet -> Renaming -> Var -> (InScopeSet, Renaming, Var)
+renameNonRecBinder iss rn x = (iss', rn', x')
+  where (subst', x') = substBndr (joinSubst iss rn) x
+        (iss', rn') = splitSubst subst' [(x, x')]
+
+renameNonRecBinders :: InScopeSet -> Renaming -> [Var] -> (InScopeSet, Renaming, [Var])
+renameNonRecBinders iss rn xs = (iss', rn', xs')
+  where (subst', xs') = substBndrs (joinSubst iss rn) xs
+        (iss', rn') = splitSubst subst' (xs `zip` xs')
+
+
+renameBounds :: InScopeSet -> Renaming -> [(Var, a)] -> (InScopeSet, Renaming, [(Var, In a)])
+renameBounds iss rn xes = (iss', rn', xs' `zip` map ((,) rn') es)
+  where (xs, es) = unzip xes
+        (iss', rn', xs') = renameBinders iss rn xs
+
+renameNonRecBound :: InScopeSet -> Renaming -> (Var, a) -> (InScopeSet, Renaming, (Var, In a))
+renameNonRecBound iss rn (x, e) = (iss', rn', (x', (rn, e)))
+  where (iss', rn', x') = renameNonRecBinder iss rn x
+
+
+(renameTerm,                renameAlts,                renameValue,                renameValue')                = mkRename (\f rn (I e) -> I (f rn e))
+(renameFVedTerm,            renameFVedAlts,            renameFVedValue,            renameFVedValue')            = mkRename (\f rn (FVed fvs e) -> FVed (renameFreeVars rn fvs) (f rn e))
+(renameTaggedTerm,          renameTaggedAlts,          renameTaggedValue,          renameTaggedValue')          = mkRename (\f rn (Tagged tg e) -> Tagged tg (f rn e))
+(renameTaggedSizedFVedTerm, renameTaggedSizedFVedAlts, renameTaggedSizedFVedValue, renameTaggedSizedFVedValue') = mkRename (\f rn (Comp (Tagged tg (Comp (Sized sz (FVed fvs e))))) -> Comp (Tagged tg (Comp (Sized sz (FVed (renameFreeVars rn fvs) (f rn e))))))
+
+{-# INLINE mkRename #-}
+mkRename :: (forall a. (Renaming -> a -> a) -> Renaming -> ann a -> ann a)
+         -> (InScopeSet -> Renaming -> ann (TermF ann)  -> ann (TermF ann),
+             InScopeSet -> Renaming -> [AltF ann]       -> [AltF ann],
+             InScopeSet -> Renaming -> ann (ValueF ann) -> ann (ValueF ann),
+             InScopeSet -> Renaming -> ValueF ann       -> ValueF ann)
+mkRename rec = (term, alternatives, value, value')
+  where
+    term ids rn = rec (term' ids) rn
+    term' ids rn e = case e of
+      Var x -> Var (renameId rn x)
+      Value v -> Value (value' ids rn v)
+      TyApp e ty -> TyApp (term ids rn e) (renameType ids rn ty)
+      CoApp e co -> CoApp (term ids rn e) (renameCoercion ids rn co)
+      App e x -> App (term ids rn e) (renameId rn x)
+      PrimOp pop tys es -> PrimOp pop (map (renameType ids rn) tys) (map (term ids rn) es)
+      Case e x ty alts -> Case (term ids rn e) x' (renameType ids rn ty) (alternatives ids' rn' alts)
+        where (ids', rn', x') = renameNonRecBinder ids rn x
+      Let x e1 e2 -> Let x' (renameIn (term ids) in_e1) (term ids' rn' e2)
+        where (ids', rn', (x', in_e1)) = renameNonRecBound ids rn (x, e1)
+      LetRec xes e -> LetRec (map (second (renameIn (term ids'))) xes') (term ids' rn' e)
+        where (ids', rn', xes') = renameBounds ids rn xes
+      Cast e co -> Cast (term ids rn e) (renameCoercion ids rn co)
+    
+    value ids rn = rec (value' ids) rn
+    value' ids rn v = renameValueG term ids rn v
+    
+    alternatives ids rn = map (alternative ids rn)
+    
+    alternative ids rn (alt_con, alt_e) = (alt_con', term ids' rn' alt_e)
+        where (ids', rn', alt_con') = renameAltCon ids rn alt_con
+
+renameValueG :: (InScopeSet -> Renaming -> a -> b)
+             -> InScopeSet -> Renaming -> ValueG a -> ValueG b
+renameValueG term ids rn v = case v of
+      TyLambda x e -> TyLambda x' (term ids' rn' e)
+        where (ids', rn', x') = renameNonRecBinder ids rn x
+      Lambda x e -> Lambda x' (term ids' rn' e)
+        where (ids', rn', x') = renameNonRecBinder ids rn x
+      Data dc tys cos xs -> Data dc (map (renameType ids rn) tys) (map (renameCoercion ids rn) cos) (map (renameId rn) xs)
+      Literal l -> Literal l
+      Coercion co -> Coercion (renameCoercion ids rn co)
+
+renameAltCon :: InScopeSet -> Renaming -> AltCon -> (InScopeSet, Renaming, AltCon)
+renameAltCon ids rn_alt alt_con = case alt_con of
+    DataAlt alt_dc alt_as alt_qs alt_xs -> third3 (DataAlt alt_dc alt_as' alt_qs') $ renameNonRecBinders ids1 rn_alt1 alt_xs
+      where (ids0, rn_alt0, alt_as') = renameNonRecBinders ids rn_alt alt_as
+            (ids1, rn_alt1, alt_qs') = renameNonRecBinders ids0 rn_alt0 alt_qs
+    LiteralAlt _                        -> (ids, rn_alt, alt_con)
+    DefaultAlt                          -> (ids, rn_alt, alt_con)

compiler/supercompile/Supercompile/Core/Size.hs

+{-# LANGUAGE Rank2Types #-}
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+module Supercompile.Core.Size where
+
+import Supercompile.Core.FreeVars
+import Supercompile.Core.Syntax
+
+import Supercompile.Utilities
+
+
+type SizedTerm = Sized (TermF Sized)
+
+type SizedFVedTerm = (O Sized FVed) (TermF (O Sized FVed))
+type SizedFVedAlt = AltF (O Sized FVed)
+type SizedFVedValue = ValueF (O Sized FVed)
+
+type TaggedSizedFVedTerm = (O Tagged (O Sized FVed)) (TermF (O Tagged (O Sized FVed)))
+type TaggedSizedFVedAlt = AltF (O Tagged (O Sized FVed))
+type TaggedSizedFVedValue = ValueF (O Tagged (O Sized FVed))
+
+(termSize,                termSize',                altsSize,                valueSize,                valueSize')                = mkSize (\f (I e) -> f e)
+(fvedTermSize,            fvedTermSize',            fvedAltsSize,            fvedValueSize,            fvedValueSize')            = mkSize (\f (FVed _ e) -> f e)
+(sizedTermSize,           sizedTermSize',           sizedAltsSize,           sizedValueSize,           sizedValueSize')           = mkSize (\_ (Sized sz _) -> sz)
+(sizedFVedTermSize,       sizedFVedTermSize',       sizedFVedAltsSize,       sizedFVedValueSize,       sizedFVedValueSize')       = mkSize (\_ (Comp (Sized sz (FVed _ _))) -> sz)
+(taggedSizedFVedTermSize, taggedSizedFVedTermSize', taggedSizedFVedAltsSize, taggedSizedFVedValueSize, taggedSizedFVedValueSize') = mkSize (\_ (Comp (Tagged _ (Comp (Sized sz (FVed _ _))))) -> sz)
+
+{-# INLINE mkSize #-}
+mkSize :: (forall a. (a -> Size) -> ann a -> Size)
+       -> (ann (TermF ann)  -> Size,
+           TermF ann        -> Size,
+           [AltF ann]       -> Size,
+           ann (ValueF ann) -> Size,
+           ValueF ann       -> Size)
+mkSize rec = (term, term', alternatives, value, value')
+  where
+    term = rec term'
+    term' e = 1 + case e of
+        Var _           -> 0
+        Value v         -> value' v - 1 -- Slight hack here so that we don't get +2 size on values
+        TyApp e _       -> term e
+        CoApp e _       -> term e
+        App e _         -> term e
+        PrimOp _ _ es   -> sum (map term es)
+        Case e _ _ alts -> term e + alternatives alts
+        Let _ e1 e2     -> term e1 + term e2
+        LetRec xes e    -> sum (map (term . snd) xes) + term e
+        Cast e _        -> term e
+    
+    value = rec value'
+    value' v = 1 + case v of
+        TyLambda _ e -> term e
+        Lambda _ e   -> term e
+        Data _ _ _ _ -> 0
+        Literal _    -> 0
+        Coercion _   -> 0
+    
+    alternatives = sum . map alternative
+    
+    alternative = term . snd
+
+
+instance Symantics (O Sized FVed) where
+    var = sizedFVedTerm . Var
+    value = fmap Value . sizedFVedValue
+    tyApp e = sizedFVedTerm . TyApp e
+    coApp e = sizedFVedTerm . CoApp e
+    app e = sizedFVedTerm . App e
+    primOp pop tys = sizedFVedTerm . PrimOp pop tys
+    case_ e x ty = sizedFVedTerm . Case e x ty
+    let_ x e1 = sizedFVedTerm . Let x e1
+    letRec xes = sizedFVedTerm . LetRec xes
+    cast e = sizedFVedTerm . Cast e
+
+sizedFVedValue :: SizedFVedValue -> (O Sized FVed) SizedFVedValue
+sizedFVedValue v = Comp (Sized (sizedFVedValueSize' v) (FVed (sizedFVedValueFreeVars' v) v))
+
+sizedFVedTerm :: TermF (O Sized FVed) -> SizedFVedTerm
+sizedFVedTerm e = Comp (Sized (sizedFVedTermSize' e) (FVed (sizedFVedTermFreeVars' e) e))
+
+
+castBySize :: CastBy -> Size
+castBySize (CastBy _ _) = 1
+castBySize Uncast       = 0
+
+coercedSize :: (a -> Size) -> Coerced a -> Size
+coercedSize sz (cast_by, e) = castBySize cast_by + sz e

compiler/supercompile/Supercompile/Core/Syntax.hs

+{-# LANGUAGE Rank2Types #-}
+module Supercompile.Core.Syntax (
+    module Supercompile.Core.Syntax,
+    Coercion, NormalCo, mkAxInstCo, mkReflCo,
+    DataCon, Var, Literal, Type, PrimOp
+  ) where
+
+#include "HsVersions.h"
+
+import Supercompile.Utilities
+import Supercompile.StaticFlags
+
+import OptCoercion
+import VarEnv   (InScopeSet)
+import DataCon  (DataCon, dataConWorkId)
+import Var      (TyVar, Var, varName, isTyVar, varType)
+import Name     (Name, nameOccName)
+import OccName  (occNameString)
+import Id       (Id, isId, idType, idInlinePragma)
+import PrimOp   (primOpType)
+import Literal  (Literal, literalType)
+import Type     (Type, mkTyVarTy, applyTy, applyTys, mkForAllTy, mkFunTy, splitFunTy_maybe, eqType)
+import TypeRep  (Type(..))
+import Kind
+import Coercion (CoVar, Coercion, coercionType, coercionKind, mkCvSubst, mkAxInstCo, mkReflCo, isReflCo)
+import qualified Coercion as Coercion
+import PrimOp   (PrimOp)
+import Pair     (pSnd)
+import PprCore  ()
+
+import qualified Data.Traversable as Traversable
+
+
+mkSymCo :: InScopeSet -> NormalCo -> NormalCo
+mkSymCo iss co = optCoercion (mkCvSubst iss []) (Coercion.mkSymCo co)
+
+mkTransCo :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
+mkTransCo = opt_trans
+
+mkNthCo :: Int -> NormalCo -> NormalCo
+mkNthCo = opt_nth
+
+mkInstCo :: InScopeSet -> NormalCo -> Type -> NormalCo
+mkInstCo = opt_inst
+
+decomposeCo :: Int -> NormalCo -> [NormalCo]
+decomposeCo arity co = [mkNthCo n co | n <- [0..(arity-1)] ]
+
+
+class Outputable a => OutputableLambdas a where
+    pprPrecLam :: a -> ([Var], Rational -> SDoc)
+
+class Outputable1 f => OutputableLambdas1 f where
+    pprPrecLam1 :: OutputableLambdas a => f a -> ([Var], Rational -> SDoc)
+
+instance (OutputableLambdas1 f, OutputableLambdas a) => OutputableLambdas (Wrapper1 f a) where
+    pprPrecLam = pprPrecLam1 . unWrapper1
+
+instance OutputableLambdas1 Identity where
+    pprPrecLam1 (I x) = pprPrecLam x
+
+instance (Functor f, OutputableLambdas1 f, OutputableLambdas1 g) => OutputableLambdas1 (O f g) where
+    pprPrecLam1 (Comp x) = pprPrecLam1 (fmap Wrapper1 x)
+
+instance OutputableLambdas1 Tagged where
+    pprPrecLam1 (Tagged tg x) = second ((braces (ppr tg) <+>) .) (pprPrecLam x)
+
+instance OutputableLambdas1 Sized where
+    pprPrecLam1 (Sized sz x) = second ((bananas (text (show sz)) <>) .) (pprPrecLam x)
+
+pprPrecDefault :: OutputableLambdas a => Rational -> a -> SDoc
+pprPrecDefault prec e = pPrintPrecLam prec xs (PrettyFunction ppr_prec)
+  where (xs, ppr_prec) = pprPrecLam e
+
+
+-- NB: don't use GHC's pprBndr because its way too noisy, printing unfoldings etc
+pPrintBndr :: BindingSite -> Var -> SDoc
+pPrintBndr bs x = prettyParen needs_parens $ ppr x <+> superinlinable <+> text "::" <+> ppr (varType x)
+  where needs_parens = case bs of LambdaBind -> True
+                                  CaseBind   -> True
+                                  LetBind    -> False
+        superinlinable = if isId x then ppr (idInlinePragma x) else empty
+
+data AltCon = DataAlt DataCon [TyVar] [CoVar] [Id] | LiteralAlt Literal | DefaultAlt
+            deriving (Eq, Show)
+
+-- Note [Case wildcards]
+-- ~~~~~~~~~~~~~~~~~~~~~
+--
+-- Simon thought that I should use the variable in the DefaultAlt to agressively rewrite occurences of a scrutinised variable.
+-- The motivation is that this lets us do more inlining above the case. For example, take this code fragment from foldl':
+--
+--   let n' = c n y
+--   in case n' of wild -> foldl' c n' ys
+--
+-- If we rewrite, n' becomes linear:
+--
+--   let n' = c n y
+--   in case n' of wild -> foldl c wild ys
+--
+-- This lets us potentially inline n' directly into the scrutinee position (operationally, this prevent creation of a thunk for n').
+-- However, I don't think that this particular form of improving linearity helps the supercompiler. We only want to inline n' in
+-- somewhere if it meets some interesting context, with which it can cancel. But if we are creating an update frame for n' at all,
+-- it is *probably* because we had no information about what it evaluated to.
+--
+-- An interesting exception is when n' binds a case expression:
+--
+--   let n' = case unk of T -> F; F -> T
+--   in case (case n' of T -> F; F -> T) of
+--        wild -> e[n']
+--
+-- You might think that we want n' to be linear so we can inline it into the case on it. However, the splitter will save us and produce:
+--
+--   case unk of
+--     T -> let n' = F
+--          in case (case n' of T -> F; F -> T) of wild -> e[n']
+--     F -> let n' = T
+--          in case (case n' of T -> F; F -> T) of wild -> e[n']
+--
+-- Since we now know the form of n', everything works out nicely.
+--
+-- Conclusion: I don't think rewriting to use the case wildcard buys us anything at all.
+
+-- Note [CoApp]
+-- ~~~~~~~~~~~~
+-- CoApp might seem redundant because we almost never substitute CoVars for Coercions, so we you might think we could get away
+-- with just reusing the App constructor but having the Var be either an Id or a CoVar. Unfortunately mkCoVarCo sometimes returns Refl so
+-- we can't guarantee that all CoVar substitutions will be variable-for-variable. We add CoApp to work around this fragility.
+
+type Term = Identity (TermF Identity)
+type TaggedTerm = Tagged (TermF Tagged)
+data TermF ann = Var Id
+               | Value (ValueF ann)
+               | TyApp (ann (TermF ann)) Type
+               | CoApp (ann (TermF ann)) Coercion
+               | App (ann (TermF ann)) Id
+               | PrimOp PrimOp [Type] [ann (TermF ann)]
+               | Case (ann (TermF ann)) Id Type [AltF ann]  -- NB: unlike GHC, for convenience we allow the list of alternatives to be empty
+               | Let Id (ann (TermF ann)) (ann (TermF ann)) -- NB: might bind an unlifted thing, in which case evaluation changes. Unlike GHC, we do NOT assume the RHSes of unlifted bindings are ok-for-speculation.
+               | LetRec [(Id, ann (TermF ann))] (ann (TermF ann))
+               | Cast (ann (TermF ann)) Coercion
+
+-- FIXME: arguably we have just Vars as arguments in PrimOp for better Tag behaviour
+-- (otherwise improving the arguments is hidden by the Tag on the whole PrimOp stack frames).
+--
+-- FIXME: in fact, we need to change this because *NOT ALL PRIMOP ARGUMENTS ARE STRICT* (e.g.
+-- the lazy polymorphic arguments to newMutVar#, newArray#).
+--
+-- FIXME: the reason I haven't done this is because it means I should remove the PrimApply frame,
+-- which breaks the "question or answer" evaluator normalisation property. Probably what I should
+-- do is just remove PrimOp and stop generating wrappers for PrimOps, so they are treated as normal Vars.
+-- We can then special case them in the evaluator's "force", using rules to pretend like they have a RHS.
+-- The only problem with this is that if there are no wrappers there is no guarantee of saturation,
+-- but we can probably ignore that.
+--
+-- FIXME: the way I'm splitting PrimApply isn't right. If we have
+--  case ((case [x] of I# x# -> x#) +# (case y of I# y# -> y#)) of
+--    0 -> ...; _ -> e[x, y]
+-- Then I want to eventually split to e[I# x#, I# y#]. At the moment we will only split to e[I# x, y]!
+-- This could be achieved in the current framework by splitting to
+--  case (x# +# (case [y] of I# y# -> y#)) of ...
+-- (Where the focus is now on y rather than x, and we put x# in the first set of arguments to PrimApply
+-- as if x# were an answer.) If we just removed the PrimApply frame then we wouldn't need to worry about this though.
+
+type Alt = AltF Identity
+type TaggedAlt = AltF Tagged
+type AltF ann = AltG (ann (TermF ann))
+type AltG term = (AltCon, term)
+
+-- FIXME: I should probably implement a correct operational semantics for TyLambdas!
+type Value = ValueF Identity
+type TaggedValue = ValueF Tagged
+type ValueF ann = ValueG (ann (TermF ann))
+data ValueG term = Literal Literal | Coercion Coercion
+                 | TyLambda TyVar term | Lambda Id term -- NB: might bind a CoVar
+                 | Data DataCon [Type] [Coercion] [Id] -- NB: includes universal and existential type arguments, in that order
+                                                       -- NB: not a newtype DataCon
+
+instance Functor ValueG where
+    fmap = Traversable.fmapDefault
+
+instance Foldable ValueG where
+    foldMap = Traversable.foldMapDefault
+
+instance Traversable ValueG where
+    traverse f e = case e of
+      Literal l          -> pure $ Literal l
+      Coercion co        -> pure $ Coercion co
+      TyLambda a e       -> fmap (TyLambda a) $ f e
+      Lambda   x e       -> fmap (Lambda   x) $ f e
+      Data dc tys cos xs -> pure $ Data dc tys cos xs
+
+instance Outputable AltCon where
+    pprPrec prec altcon = case altcon of
+        DataAlt dc as qs xs -> prettyParen (prec >= appPrec) $ ppr dc <+> hsep (map (pPrintBndr CaseBind) as ++ map (pPrintBndr CaseBind) qs ++ map (pPrintBndr CaseBind) xs)
+        LiteralAlt l        -> pPrint l
+        DefaultAlt          -> text "_"
+
+instance (Functor ann, OutputableLambdas1 ann) => Outputable (TermF ann) where
+    pprPrec = pprPrecDefault
+
+instance (Functor ann, OutputableLambdas1 ann) => OutputableLambdas (TermF ann) where
+    pprPrecLam e = case e of
+        Let x e1 e2       -> ([], \prec -> pPrintPrecLet prec x (asPrettyFunction1 e1) (asPrettyFunction1 e2))
+        LetRec xes e      -> ([], \prec -> pPrintPrecLetRec prec (map (second asPrettyFunction1) xes) (asPrettyFunction1 e))
+        Var x             -> ([], \prec -> pPrintPrec prec x)
+        Value v           -> pprPrecLam v
+        TyApp e ty        -> ([], \prec -> pPrintPrecApp prec (asPrettyFunction1 e) ty)
+        CoApp e co        -> ([], \prec -> pPrintPrecApp prec (asPrettyFunction1 e) co)
+        App e x           -> ([], \prec -> pPrintPrecApp prec (asPrettyFunction1 e) x)
+        PrimOp pop tys es -> ([], \prec -> pPrintPrecPrimOp prec pop (map asPrettyFunction tys) (map asPrettyFunction1 es))
+        Case e x _ty alts -> ([], \prec -> pPrintPrecCase prec (asPrettyFunction1 e) x (map (second asPrettyFunction1) alts))
+        Cast e co         -> ([], \prec -> pPrintPrecCast prec (asPrettyFunction1 e) co)
+
+pPrintPrecCast :: Outputable a => Rational -> a -> Coercion -> SDoc
+pPrintPrecCast prec e co = prettyParen (prec > noPrec) $ pPrintPrec opPrec e <+> text "|>" <+> pPrintPrec appPrec co
+
+pPrintPrecCoerced :: Outputable a => Rational -> Coerced a -> SDoc
+pPrintPrecCoerced prec (CastBy co _, e) = pPrintPrecCast prec e co
+pPrintPrecCoerced prec (Uncast,      e) = pPrintPrec prec e
+
+pPrintPrecApp :: (Outputable a, Outputable b) => Rational -> a -> b -> SDoc
+pPrintPrecApp prec e1 e2 = prettyParen (prec >= appPrec) $ pPrintPrec opPrec e1 <+> pPrintPrec appPrec e2
+
+pPrintPrecPrimOp :: (Outputable a, Outputable b, Outputable c) => Rational -> a -> [b] -> [c] -> SDoc
+pPrintPrecPrimOp prec pop as xs = pPrintPrecApps prec (PrettyFunction (\prec -> pPrintPrecApps prec pop as)) xs
+
+pPrintPrecCase :: (Outputable a, Outputable b, Outputable c) => Rational -> a -> Var -> [(b, c)] -> SDoc
+pPrintPrecCase prec e x alts = prettyParen (prec > noPrec) $ hang (text "case" <+> pPrintPrec noPrec e <+> text "of" <+> pPrintBndr CaseBind x) 2 $ vcat (map (pPrintPrecAlt noPrec) alts)
+
+pPrintPrecAlt :: (Outputable a, Outputable b) => Rational -> (a, b) -> SDoc
+pPrintPrecAlt _ (alt_con, alt_e) = hang (pPrintPrec noPrec alt_con <+> text "->") 2 (pPrintPrec noPrec alt_e)
+
+pPrintPrecLet :: (Outputable a, Outputable b) => Rational -> Var -> a -> b -> SDoc
+pPrintPrecLet prec x e e_body = prettyParen (prec > noPrec) $ hang (text "let") 2 (pPrintBndr LetBind x <+> text "=" <+> pPrintPrec noPrec e) $$ text "in" <+> pPrintPrec noPrec e_body
+
+pPrintPrecLetRec, pPrintPrecWhere :: (Outputable a, Outputable b) => Rational -> [(Var, a)] -> b -> SDoc
+pPrintPrecLetRec prec xes e_body
+  | [] <- xes = pPrintPrec prec e_body
+  | otherwise = prettyParen (prec > noPrec) $ hang (text "letrec") 2 (vcat [hang (pPrintBndr LetBind x) 2 (text "=" <+> pPrintPrec noPrec e) | (x, e) <- xes]) $$ text "in" <+> pPrintPrec noPrec e_body
+
+pPrintPrecWhere prec xes e_body
+  | [] <- xes = pPrintPrec prec e_body
+  | otherwise = prettyParen (prec > noPrec) $ hang (pPrintPrec noPrec e_body) 1 $ hang (text "where") 1 $ vcat [hang (pPrintBndr LetBind x) 2 (text "=" <+> pPrintPrec noPrec e) | (x, e) <- xes]
+
+instance (Functor ann, OutputableLambdas1 ann) => Outputable (ValueF ann) where
+    pprPrec = pprPrecDefault
+
+instance (Functor ann, OutputableLambdas1 ann) => OutputableLambdas (ValueF ann) where
+    pprPrecLam v = case v of
+        TyLambda x e       -> (x:xs, ppr_prec)
+          where (xs, ppr_prec) = pprPrecLam1 e
+        Lambda x e         -> (x:xs, ppr_prec)
+          where (xs, ppr_prec) = pprPrecLam1 e
+        Data dc tys cos xs -> ([], \prec -> pPrintPrecApps prec dc ([asPrettyFunction ty | ty <- tys] ++ [asPrettyFunction co | co <- cos] ++ [asPrettyFunction x | x <- xs]))
+        Literal l          -> ([], flip pPrintPrec l)
+        Coercion co        -> ([], flip pPrintPrec co)
+
+pPrintPrecLam :: Outputable a => Rational -> [Var] -> a -> SDoc
+pPrintPrecLam prec [] e = pPrintPrec prec e
+pPrintPrecLam prec xs e = prettyParen (prec > noPrec) $ text "\\" <> (vcat [pPrintBndr LambdaBind y | y <- xs] $$ text "->" <+> pPrintPrec noPrec e)
+
+pPrintPrecApps :: (Outputable a, Outputable b) => Rational -> a -> [b] -> SDoc
+pPrintPrecApps prec e1 es2 = prettyParen (not (null es2) && prec >= appPrec) $ pPrintPrec opPrec e1 <+> hsep (map (pPrintPrec appPrec) es2)
+
+
+-- Find those things that are Values and cannot be further evaluated. Primarily used to prevent the
+-- speculator from re-speculating values, but also as an approximation for what GHC considers a value.
+termIsValue :: Copointed ann => ann (TermF ann) -> Bool
+termIsValue = isValue . extract
+  where
+    isValue (Value _)                         = True
+    isValue (Cast e _) | Value _ <- extract e = True
+    isValue _                                 = False
+
+-- Find those things that we are willing to duplicate.
+termIsCheap :: Copointed ann => ann (TermF ann) -> Bool
+termIsCheap = termIsCheap' . extract
+
+termIsCheap' :: Copointed ann => TermF ann -> Bool
+termIsCheap' _ | cALL_BY_NAME = True -- A cunning hack. I think this is all that should be required... (TODO: not for stack bound things..)
+termIsCheap' (Var _)         = True
+termIsCheap' (Value _)       = True
+termIsCheap' (Cast e _)      = termIsCheap e
+termIsCheap' (Case e _ _ []) = termIsCheap e -- NB: important for pushing down let-bound applications of ``error''
+termIsCheap' _               = False
+
+varString :: Var -> String
+varString = nameString . varName
+
+nameString :: Name -> String
+nameString = occNameString . nameOccName
+
+
+data CastBy = Uncast | CastBy NormalCo Tag -- INVARIANT: NormalCo is not Refl
+type Coerced a = (CastBy, a)
+
+castBy :: NormalCo -> Tag -> CastBy
+castBy co tg | isReflCo co = Uncast -- TODO: this throws away a tag (and hence a deed). But do I care any longer?
+             | otherwise   = CastBy co tg
+
+castByCo :: CastBy -> Maybe NormalCo
+castByCo Uncast        = Nothing
+castByCo (CastBy co _) = Just co
+
+mkSymCastBy :: InScopeSet -> CastBy -> CastBy
+mkSymCastBy _   Uncast         = Uncast
+mkSymCastBy ids (CastBy co tg) = CastBy (mkSymCo ids co) tg
+
+mkTransCastBy :: InScopeSet -> CastBy -> CastBy -> CastBy
+mkTransCastBy _   Uncast            cast_by2         = cast_by2
+mkTransCastBy _   cast_by1          Uncast           = cast_by1
+mkTransCastBy ids (CastBy co1 _tg1) (CastBy co2 tg2) = castBy (mkTransCo ids co1 co2) tg2
+
+
+canAbstractOverTyVarOfKind :: Kind -> Bool
+canAbstractOverTyVarOfKind = ok
+  where
+    -- TODO: I'm not 100% sure of the correctness of this check
+    -- In particular, I don't think we need to check for non-conforming
+    -- kinds in "negative" positions since they would only appear if the
+    -- definition site had erroneously abstracted over a non-conforming
+    -- kind. For example, this *should* never be allowed:
+    --   data Foo (a :: * -> #) = Bar (a Int)
+    --   Foo :: (* -> #) -> *
+    --   Bar :: forall (a :: * -> #). a Int -> Foo a
+    ok k | isOpenTypeKind k || isUbxTupleKind k || isArgTypeKind k || isUnliftedTypeKind k = False
+    ok (TyVarTy _)     = True -- This is OK because kinds dont get generalised, and we assume all incoming kind instantiations satisfy the kind invariant
+    ok (AppTy k1 k2)   = ok k1 && ok k2
+    ok (TyConApp _ ks) = all ok ks
+    ok (FunTy k1 k2)   = ok k1 && ok k2
+    ok (ForAllTy _ k)  = ok k
+    ok (LitTy _)       = True
+
+
+valueType :: Copointed ann => ValueF ann -> Type
+valueType (TyLambda a e)      = mkForAllTy a (termType e)
+valueType (Lambda x e)        = idType x `mkFunTy` termType e
+valueType (Data dc as cos xs) = ((idType (dataConWorkId dc) `applyTys` as) `applyFunTys` map coercionType cos) `applyFunTys` map idType xs
+valueType (Literal l)         = literalType l
+valueType (Coercion co)       = coercionType co
+
+termType :: Copointed ann => ann (TermF ann) -> Type
+termType = termType' . extract
+
+termType' :: Copointed ann => TermF ann -> Type
+termType' e = case e of
+    Var x             -> idType x
+    Value v           -> valueType v
+    TyApp e a         -> termType e `applyTy` a
+    CoApp e co        -> termType e `applyFunTy` coercionType co
+    App e x           -> termType e `applyFunTy` idType x
+    PrimOp pop tys es -> (primOpType pop `applyTys` tys) `applyFunTys` map termType es
+    Case _ _ ty _     -> ty
+    Let _ _ e         -> termType e
+    LetRec _ e        -> termType e
+    Cast _ co         -> pSnd (coercionKind co)
+
+applyFunTy :: Type -> Type -> Type
+applyFunTy fun_ty got_arg_ty = case splitFunTy_maybe fun_ty of
+    Just (expected_arg_ty, res_ty) -> ASSERT2(got_arg_ty `eqType` expected_arg_ty, text "applyFunTy:" <+> ppr got_arg_ty <+> ppr expected_arg_ty) res_ty
+    Nothing                        -> pprPanic "applyFunTy" (ppr fun_ty $$ ppr got_arg_ty)
+
+applyFunTys :: Type -> [Type] -> Type
+applyFunTys = foldl' applyFunTy
+
+
+class Functor ann => Symantics ann where
+    var    :: Var -> ann (TermF ann)
+    value  :: ValueF ann -> ann (TermF ann)
+    app    :: ann (TermF ann) -> Var -> ann (TermF ann)
+    coApp  :: ann (TermF ann) -> Coercion -> ann (TermF ann)
+    tyApp  :: ann (TermF ann) -> Type -> ann (TermF ann)
+    primOp :: PrimOp -> [Type] -> [ann (TermF ann)] -> ann (TermF ann)
+    case_  :: ann (TermF ann) -> Var -> Type -> [AltF ann] -> ann (TermF ann)
+    let_   :: Var -> ann (TermF ann) -> ann (TermF ann) -> ann (TermF ann)
+    letRec :: [(Var, ann (TermF ann))] -> ann (TermF ann) -> ann (TermF ann)
+    cast   :: ann (TermF ann) -> Coercion -> ann (TermF ann)
+
+instance Symantics Identity where
+    var = I . Var
+    value = I . Value
+    tyApp e = I . TyApp e
+    coApp e = I . CoApp e
+    app e = I . App e
+    primOp pop tys = I . PrimOp pop tys
+    case_ e x ty = I . Case e x ty
+    let_ x e1 = I . Let x e1
+    letRec xes = I . LetRec xes
+    cast e = I . Cast e
+
+
+reify :: (forall ann. Symantics ann => ann (TermF ann)) -> Term
+reify x = x
+
+reflect :: Term -> (forall ann. Symantics ann => ann (TermF ann))
+reflect (I e) = case e of
+    Var x             -> var x
+    Value v           -> value (reflectValue v)
+    TyApp e ty        -> tyApp (reflect e) ty
+    App e x           -> app (reflect e) x
+    CoApp e co        -> coApp (reflect e) co
+    PrimOp pop tys es -> primOp pop tys (map reflect es)
+    Case e x ty alts  -> case_ (reflect e) x ty (map (second reflect) alts)
+    Let x e1 e2       -> let_ x (reflect e1) (reflect e2)
+    LetRec xes e      -> letRec (map (second reflect) xes) (reflect e)
+    Cast e co         -> cast (reflect e) co
+  where
+    reflectValue :: Value -> (forall ann. Symantics ann => ValueF ann)
+    reflectValue v = case v of
+        TyLambda x e       -> TyLambda x (reflect e)
+        Lambda x e         -> Lambda x (reflect e)
+        Data dc tys cos xs -> Data dc tys cos xs
+        Literal l          -> Literal l
+        Coercion co        -> Coercion co
+
+
+literal :: Symantics ann => Literal -> ann (TermF ann)
+literal = value . Literal
+
+coercion :: Symantics ann => Coercion -> ann (TermF ann)
+coercion = value . Coercion
+
+{-
+lambda :: Symantics ann => Var -> ann (TermF ann) -> ann (TermF ann)
+lambda x = value . Lambda x
+
+data_ :: Symantics ann => DataCon -> [Var] -> ann (TermF ann)
+data_ dc = value . Data dc
+-}
+
+tyLambdas :: Symantics ann => [TyVar] -> ann (TermF ann) -> ann (TermF ann)
+tyLambdas = flip $ foldr (\x -> value . TyLambda x)
+
+lambdas :: Symantics ann => [Id] -> ann (TermF ann) -> ann (TermF ann)
+lambdas = flip $ foldr (\x -> value . Lambda x)
+
+tyVarIdLambdas :: Symantics ann => [Var] -> ann (TermF ann) -> ann (TermF ann)
+tyVarIdLambdas = flip $ foldr tyVarIdLambda
+
+tyVarIdLambda :: Symantics ann => Var -> ann (TermF ann) -> ann (TermF ann)
+tyVarIdLambda x e | isTyVar x = value $ TyLambda x e
+                  | otherwise = value $ Lambda   x e
+
+tyApps :: Symantics ann => ann (TermF ann) -> [Type] -> ann (TermF ann)
+tyApps = foldl tyApp
+
+coApps :: Symantics ann => ann (TermF ann) -> [Coercion] -> ann (TermF ann)
+coApps = foldl coApp
+
+apps :: Symantics ann => ann (TermF ann) -> [Id] -> ann (TermF ann)
+apps = foldl app
+
+tyVarIdApps :: Symantics ann => ann (TermF ann) -> [Var] -> ann (TermF ann)
+tyVarIdApps = foldl tyVarIdApp
+
+tyVarIdApp :: Symantics ann => ann (TermF ann) -> Var -> ann (TermF ann)
+tyVarIdApp e x | isTyVar x = e `tyApp` mkTyVarTy x
+               | otherwise = e `app` x
+
+{-
+strictLet :: Symantics ann => Var -> ann (TermF ann) -> ann (TermF ann) -> ann (TermF ann)
+strictLet x e1 e2 = case_ e1 [(DefaultAlt (Just x), e2)]
+
+collectLambdas :: Term -> ([Var], Term)
+collectLambdas (I (Value (Lambda x e))) = first (x:) $ collectLambdas e
+collectLambdas e                        = ([], e)
+
+freshFloatVar :: IdSupply -> String -> Term -> (IdSupply, Maybe (Var, Term), Var)
+freshFloatVar ids _ (I (Var x)) = (ids,  Nothing,     x)
+freshFloatVar ids s e           = (ids', Just (y, e), y)
+  where (ids', y) = freshName ids s
+
+freshFloatVars :: IdSupply -> String -> [Term] -> (IdSupply, [(Var, Term)], [Var])
+freshFloatVars ids s es = reassociate $ mapAccumL (\ids -> associate . freshFloatVar ids s) ids es
+  where reassociate (ids, floats_xs) = let (mb_floats, xs) = unzip floats_xs in (ids, catMaybes mb_floats, xs)
+        associate (ids, mb_float, x) = (ids, (mb_float, x))
+-}

compiler/supercompile/Supercompile/Core/Tag.hs

+{-# LANGUAGE RankNTypes #-}
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+module Supercompile.Core.Tag where
+
+import Supercompile.Utilities
+
+import Supercompile.Core.FreeVars
+import Supercompile.Core.Size
+import Supercompile.Core.Syntax
+
+import Literal (hashLiteral)
+import Unique  (mkPrimOpIdUnique)
+import qualified PrimOp as PrimOp (primOpTag)
+
+
+tagTerm :: UniqSupply -> Term -> TaggedTerm
+tagTerm = mkTagger (\tg (I e) -> Tagged tg e)
+
+tagFVedTerm :: UniqSupply -> SizedFVedTerm -> TaggedSizedFVedTerm
+tagFVedTerm = mkTagger (\tg e -> Comp (Tagged tg e))
+
+
+-- The guiding principle behind these two functions is that ideally there should only
+-- be one tag for a particular value. If we give every occurrence of (:) in the input
+-- program a different tag we can get weird situations (like gen_regexps) where programs
+-- are specialised on very long repititions of the same constructor.
+--
+-- The special treatment of PrimOp has a similar reason, and is necessary because I started
+-- treating PrimOp specially and unfolding it without going through the wrapper if it is
+-- saturated. This saves us from ANFing the arguments to a primop, which is cool!
+
+uniqueToTag :: Unique -> Tag
+uniqueToTag = mkTag . negate . abs . getKey -- Works well because (hashLiteral l) is always positive
+
+dataConTag :: DataCon -> Tag
+dataConTag = uniqueToTag . getUnique -- Don't use dataConTag because tags are shared between DC families, and [], True and all dictionary all get the same tag!!
+
+literalTag :: Literal -> Tag
+literalTag = mkTag . hashLiteral
+
+primOpTag :: PrimOp -> Tag
+primOpTag = uniqueToTag . mkPrimOpIdUnique . PrimOp.primOpTag
+
+
+{-# INLINE mkTagger #-}
+mkTagger :: (Copointed ann, Functor ann')
+         => (forall a. Tag -> ann a -> ann' a)
+         -> UniqSupply -> ann (TermF ann) -> ann' (TermF ann')
+mkTagger rec = term
+  where
+    tag_rec ids orig f = rec (mkTag (getKey i)) (replace orig (f ids'))
+      where (i, ids') = takeUniqFromSupply ids
+
+    replace orig hole = fmap (const hole) orig
+
+    term ids e = case extract e of
+        Var x             -> tag $ \_ -> Var x
+        Value v           -> value ids e v
+        TyApp e ty        -> tag $ \ids -> TyApp (term ids e) ty
+        CoApp e co        -> tag $ \ids -> CoApp (term ids e) co
+        App e x           -> tag $ \ids -> App (term ids e) x
+        PrimOp pop tys es -> rec (primOpTag pop) $ replace e $ let idss' = listSplitUniqSupply ids
+                                                               in PrimOp pop tys (zipWith term idss' es)
+        Case e x ty alts  -> tag $ \ids -> let (ids0', ids1') = splitUniqSupply ids
+                                           in Case (term ids0' e) x ty (alternatives ids1' alts)
+        Let x e1 e2       -> tag $ \ids -> let (ids0', ids1') = splitUniqSupply ids
+                                           in Let x (term ids0' e1) (term ids1' e2)
+        LetRec xes e      -> tag $ \ids -> let (ids0', ids1') = splitUniqSupply ids
+                                               idss' = listSplitUniqSupply ids0'
+                                           in LetRec (zipWith (\ids'' (x, e) -> (x, term ids'' e)) idss' xes) (term ids1' e)
+        Cast e co         -> tag $ \ids -> Cast (term ids e) co
+      where tag = tag_rec ids e
+
+    value ids e v = fmap Value $ case v of
+        TyLambda x e       -> tag $ \ids -> TyLambda x (term ids e)
+        Lambda x e         -> tag $ \ids -> Lambda x (term ids e)
+        Data dc tys cos xs -> rec (dataConTag dc) $ replace e (Data dc tys cos xs)
+        Literal l          -> rec (literalTag l)  $ replace e (Literal l)
+        Coercion co        -> tag $ \_ -> Coercion co
+      where tag = tag_rec ids e
+
+    alternatives = zipWith alternative . listSplitUniqSupply
+    
+    alternative ids (con, e) = (con, term ids e)
+
+
+(taggedTermToTerm,              taggedTermToTerm',              taggedAltsToAlts,              taggedValueToValue,              taggedValue'ToValue')              = mkDetag (\f e -> I (f (tagee e)))
+(fVedTermToTerm,                fVedTermToTerm',                fVedAltsToAlts,                fVedValueToValue,                fVedValue'ToValue')                = mkDetag (\f e -> I (f (fvee e)))
+(taggedSizedFVedTermToTerm,     taggedSizedFVedTermToTerm',     taggedSizedFVedAltsToAlts,     taggedSizedFVedValueToValue,     taggedSizedFVedValue'ToValue')     = mkDetag (\f e -> I (f (fvee (sizee (unComp (tagee (unComp e)))))))
+(taggedSizedFVedTermToFVedTerm, taggedSizedFVedTermToFVedTerm', taggedSizedFVedAltsToFVedAlts, taggedSizedFVedValueToFVedValue, taggedSizedFVedValue'ToFVedValue') = mkDetag (\f e -> FVed (freeVars (sizee (unComp (tagee (unComp e))))) (f (extract e)))
+
+
+{-# INLINE mkDetag #-}
+mkDetag :: (forall a b. (a -> b) -> ann a -> ann' b)
+        -> (ann (TermF ann)  -> ann' (TermF ann'),
+            TermF ann        -> TermF ann',
+            [AltF ann]       -> [AltF ann'],
+            ann (ValueF ann) -> ann' (ValueF ann'),
+            ValueF ann       -> ValueF ann')
+mkDetag rec = (term, term', alternatives, value, value')
+  where
+    term = rec term'
+    term' e = case e of
+        Var x             -> Var x
+        Value v           -> Value (value' v)
+        TyApp e ty        -> TyApp (term e) ty
+        CoApp e co        -> CoApp (term e) co
+        App e x           -> App (term e) x
+        PrimOp pop tys es -> PrimOp pop tys (map term es)
+        Case e x ty alts  -> Case (term e) x ty (alternatives alts)
+        Let x e1 e2       -> Let x (term e1) (term e2)
+        LetRec xes e      -> LetRec (map (second term) xes) (term e)
+        Cast e co         -> Cast (term e) co
+
+    value = rec value'
+    value' (TyLambda a e)       = TyLambda a (term e)
+    value' (Lambda x e)         = Lambda x (term e)
+    value' (Data dc tys cos xs) = Data dc tys cos xs
+    value' (Literal l)          = Literal l
+    value' (Coercion co)        = Coercion co
+
+    alternatives = map (second term)

compiler/supercompile/Supercompile/Drive/Match.hs

+module Supercompile.Drive.Match (
+    MatchMode(..), InstanceMatching(..),
+    match, match',
+    Match, unMatch, matchWithReason, matchWithReason'
+  ) where
+
+#include "HsVersions.h"
+
+import Supercompile.Core.Renaming
+import Supercompile.Core.Syntax
+
+import Supercompile.Evaluator.FreeVars
+import Supercompile.Evaluator.Syntax
+
+import Supercompile.StaticFlags
+import Supercompile.Utilities hiding (guard)
+
+import qualified CoreSyn as Core
+
+import Util
+import Coercion
+import Var        (TyVar, isTyVar, isId, tyVarKind, setVarType)
+import Id         (Id, idType, realIdUnfolding, idSpecialisation, zapFragileIdInfo)
+import IdInfo     (SpecInfo(..), emptySpecInfo)
+import VarEnv
+import TypeRep    (Kind, Type(..), isKindVar)
+
+import qualified Control.Monad
+import Control.Monad.Fix
+
+import qualified Data.Map as M
+
+
+pprTraceSC :: String -> SDoc -> a -> a
+--pprTraceSC _ _ = id
+--pprTraceSC = pprTrace
+pprTraceSC msg doc a = traceSC (msg ++ ": " ++ showSDoc doc) a
+
+traceSC :: String -> a -> a
+traceSC _ = id
+--traceSC = trace
+
+
+-- Note [Instance matching]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~
+--
+-- Instance matching is very, very dangerous from a correctness standpoint. If we start with:
+--
+--  let x = v[x] in x
+--
+-- Then reducing and splitting causes us to drive:
+--
+--  let x = v[x] in v
+--
+-- Note that the new term matches against the previous one ([v/x]) if we can do instance matching, so
+-- if we are not careful we immediately build a loop. This really sucks.
+
+
+newtype Match a = Match { unMatch :: Either String a }
+--newtype Match a = Match { unMatch :: Maybe a }
+
+instance Functor Match where
+    fmap = liftM
+
+instance Monad Match where
+    return = Match . return
+    mx >>= fxmy = Match $ unMatch mx >>= (unMatch . fxmy)
+    fail s = Match $ Left s
+    --fail s = Match $ fail s
+
+instance MonadFix Match where
+    mfix xmy = Match (mfix (unMatch . xmy))
+
+guard :: String -> Bool -> Match ()
+guard _   True  = return ()
+guard msg False = fail msg
+
+runMatch :: Match a -> Maybe a
+runMatch (Match (Right x))   = Just x
+runMatch (Match (Left _msg)) = {- trace ("match " ++ _msg) -} Nothing
+--runMatch = unMatch
+
+matchRnEnv2 :: (a -> FreeVars) -> a -> a -> RnEnv2
+matchRnEnv2 f x y = mkRnEnv2 (mkInScopeSet (f x `unionVarSet` f y))
+
+-- instance MonadPlus Match where
+--     mzero = fail "mzero"
+--     mx1 `mplus` mx2 = Match $ unMatch mx1 `mplus` unMatch mx2
+
+
+data MatchMode = MatchMode {
+    matchInstanceMatching :: InstanceMatching,
+    matchCommonHeapVars :: InScopeSet
+  }
+
+
+type MatchRenaming = M.Map Var Var
+
+-- INVARIANTs:
+--   1. All the Vars are *not* rigidly bound (i.e. they are bound by a "let")
+--   2. The terms *may* contain free variables of any kind, rigidly bound or not
+--   3. The Vars in VarL/VarR are always CoVars/Ids, NEVER TyVars (might change this in the future)
+data MatchLR = VarL Var (Out AnnedTerm) -- NB: we should not let these two float out of lambdas because they
+             | VarR (Out AnnedTerm) Var -- might match against top-level bindings and hence change work sharing
+             | VarLR Var Var
+
+-- Need exact equality for matchPureHeap loop
+instance Eq MatchLR where
+    VarL x1 e1      == VarL x2 e2      = x1 == x2            && e1 `eqAnnedTerm` e2
+    VarR e1 x1      == VarR e2 x2      = e1 `eqAnnedTerm` e2 && x1 == x2
+    VarLR x_l1 x_r1 == VarLR x_l2 x_r2 = x_l1 == x_l2        && x_r1 == x_r2
+    _ == _ = False
+
+eqAnnedTerm :: AnnedTerm -> AnnedTerm -> Bool
+eqAnnedTerm e1 e2  = case runMatch (matchTerm (matchRnEnv2 annedTermFreeVars e1 e2) e1 e2) of
+    Nothing  -> False
+    Just lrs -> all (\lr -> case lr of VarLR x_l x_r | x_l == x_r -> True; _ -> False) lrs
+
+instance Outputable MatchLR where
+    pprPrec _ (VarL x _e')  = ppr x                   <+> text "<->" <+> text "..." {- ppr e' -}
+    pprPrec _ (VarR _e' x)  = text "..." {- ppr e' -} <+> text "<->" <+> ppr x
+    pprPrec _ (VarLR x1 x2) = ppr x1                  <+> text "<->" <+> ppr x2
+
+match :: State -- ^ Tieback semantics
+      -> State -- ^ This semantics
+      -> Maybe MatchRenaming -- ^ Renaming from left to right
+match s_l s_r = runMatch (matchWithReason s_l s_r)
+
+match' :: MatchMode -> State -> State -> Maybe (Heap, Stack, MatchRenaming)
+match' mm s_l s_r = runMatch (matchWithReason' mm s_l s_r)
+
+matchWithReason :: State -> State -> Match MatchRenaming
+matchWithReason s_l s_r = fmap thirdOf3 $ matchWithReason' (MatchMode { matchInstanceMatching = NoInstances, matchCommonHeapVars = emptyInScopeSet }) s_l s_r
+
+matchWithReason' :: MatchMode -> State -> State -> Match (Heap, Stack, MatchRenaming)
+matchWithReason' mm (_deeds_l, Heap h_l ids_l, k_l, qa_l) (_deeds_r, Heap h_r ids_r, k_r, qa_r) = -- (\res -> traceRender ("match", M.keysSet h_l, residualiseDriveState (Heap h_l prettyIdSupply, k_l, in_e_l), M.keysSet h_r, residualiseDriveState (Heap h_r prettyIdSupply, k_r, in_e_r), res) res) $
+  {-# SCC "matchWithReason'" #-} do
+    -- It's very important that we don't just use the state free variables from both sides to construct the initial in scope set,
+    -- because we use it to match the stack and QA on each side *without* first extending it with variables bound by the PureHeap!
+    --
+    -- The InScopeSets from the Heap are guaranteed to take these into account (along with the stuff bound by the stack, but that
+    -- doesn't matter too much) so we just use those instead.
+    --
+    -- This was the source of a very confusing bug :-(
+    let init_rn2 = mkRnEnv2 (ids_l `unionInScope` ids_r)
+    (rn2, k_inst, mfree_eqs2) <- matchEC mm init_rn2 k_l k_r
+    free_eqs1 <- pprTraceSC "match0" (rn2 `seq` empty) $ matchAnned (matchQA rn2) qa_l qa_r
+    free_eqs2 <- pprTraceSC "match1" empty $ mfree_eqs2 rn2
+    (heap_inst, mr) <- pprTraceSC "match2" (ppr free_eqs1) $ matchPureHeap mm rn2 k_inst (free_eqs1 ++ free_eqs2) h_l (Heap h_r ids_r)
+    return (heap_inst, k_inst, mr)
+
+matchAnned :: (Tag -> a -> Tag -> a -> b)
+            -> Anned a -> Anned a -> b
+matchAnned f a_l a_r = f (annedTag a_l) (annee a_l) (annedTag a_r) (annee a_r)
+
+matchQA :: RnEnv2 -> Tag -> QA -> Tag -> QA -> Match [MatchLR]
+matchQA rn2 _    (Question x_l') _    (Question x_r') = matchVar rn2 x_l' x_r'
+matchQA rn2 _    (Question x_l') tg_r (Answer in_v_r) = matchVarL rn2 x_l' (annedTerm tg_r (answerToAnnedTerm' (rnInScopeSet rn2) in_v_r)) -- NB: these rely on the RnEnv2
+matchQA rn2 tg_l (Answer in_v_l) _    (Question x_r') = matchVarR rn2 (annedTerm tg_l (answerToAnnedTerm' (rnInScopeSet rn2) in_v_l)) x_r' -- InScopeSet just like matchIn does
+matchQA rn2 tg_l (Answer in_v_l) tg_r (Answer in_v_r) = matchAnswer rn2 tg_l in_v_l tg_r in_v_r
+
+matchAnswer :: RnEnv2 -> Tag -> Answer -> Tag -> Answer -> Match [MatchLR]
+matchAnswer rn2 tg_l in_v_l tg_r in_v_r = matchIn renameAnnedValue' (\rn2 v_l v_r -> matchValue rn2 tg_l v_l tg_r v_r) rn2 in_v_l in_v_r
+
+matchCoerced :: (RnEnv2 -> Tag -> a -> Tag -> a -> Match [MatchLR])
+             -> RnEnv2 -> Tag -> Coerced a -> Tag -> Coerced a -> Match [MatchLR]
+matchCoerced f rn2 tg_l (Uncast,           x_l) tg_r (Uncast,           x_r) = f rn2 tg_l x_l tg_r x_r
+matchCoerced f rn2 _    (CastBy co_l tg_l, x_l) _    (CastBy co_r tg_r, x_r) = liftM2 (++) (matchCoercion rn2 co_l co_r) (f rn2 tg_l x_l tg_r x_r)
+matchCoerced _ _ _ _ _ _ = fail "matchCoerced"
+
+-- TODO: I don't know how complete support for polykinds actually *is* in the supercompiler, so this is a bit speculative:
+matchKind :: RnEnv2 -> Kind -> Kind -> Match [MatchLR]
+matchKind = matchType
+
+-- TODO: match type instantiation?
+matchType :: RnEnv2 -> Type -> Type -> Match [MatchLR]
+matchType rn2 (TyVarTy x_l)         (TyVarTy x_r)         = matchVar rn2 x_l x_r
+matchType rn2 (AppTy ty1_l ty2_l)   (AppTy ty1_r ty2_r)   = liftM2 (++) (matchType rn2 ty1_l ty1_r) (matchType rn2 ty2_l ty2_r)
+matchType rn2 (TyConApp tc_l tys_l) (TyConApp tc_r tys_r) = guard "matchType: TyConApp" (tc_l == tc_r) >> matchList (matchType rn2) tys_l tys_r
+matchType rn2 (FunTy ty1_l ty2_l)   (FunTy ty1_r ty2_r)   = liftM2 (++) (matchType rn2 ty1_l ty1_r) (matchType rn2 ty2_l ty2_r)
+matchType rn2 (ForAllTy a_l ty_l)   (ForAllTy a_r ty_r)   = matchTyVarBndr rn2 a_l a_r $ \rn2 -> matchType rn2 ty_l ty_r
+matchType _   (LitTy l_l)           (LitTy l_r)           = guard "matchType: LitTy" (l_l == l_r) >> return []
+matchType _ _ _ = fail "matchType"
+
+-- TODO: match coercion instantiation?
+matchCoercion :: RnEnv2 -> Coercion -> Coercion -> Match [MatchLR]
+matchCoercion rn2 (Refl ty_l)              (Refl ty_r)              = matchType rn2 (ty_l) (ty_r)
+matchCoercion rn2 (TyConAppCo tc_l cos_l)  (TyConAppCo tc_r cos_r)  = guard "matchCoercion: TyConAppCo" (tc_l == tc_r) >> matchList (matchCoercion rn2) (cos_l) (cos_r)
+matchCoercion rn2 (AppCo co1_l co2_l)      (AppCo co1_r co2_r)      = liftM2 (++) (matchCoercion rn2 (co1_l) (co1_r)) (matchCoercion rn2 (co2_l) (co2_r))
+matchCoercion rn2 (ForAllCo a_l co_l)      (ForAllCo a_r co_r)      = matchTyVarBndr rn2 a_l a_r $ \rn2 -> matchCoercion rn2 co_l co_r
+matchCoercion rn2 (CoVarCo a_l)            (CoVarCo a_r)            = matchVar rn2 a_l a_r
+matchCoercion rn2 (AxiomInstCo ax_l cos_l) (AxiomInstCo ax_r cos_r) = guard "matchCoercion: AxiomInstCo" (ax_l == ax_r) >> matchList (matchCoercion rn2) (cos_l) (cos_r)
+matchCoercion rn2 (UnsafeCo ty1_l ty2_l)   (UnsafeCo ty1_r ty2_r)   = liftM2 (++) (matchType rn2 (ty1_l) (ty1_r)) (matchType rn2 (ty2_l) (ty2_r))
+matchCoercion rn2 (SymCo co_l)             (SymCo co_r)             = matchCoercion rn2 (co_l) (co_r)
+matchCoercion rn2 (TransCo co1_l co2_l)    (TransCo co1_r co2_r)    = liftM2 (++) (matchCoercion rn2 (co1_l) (co1_r)) (matchCoercion rn2 (co2_l) (co2_r))
+matchCoercion rn2 (NthCo i_l co_l)         (NthCo i_r co_r)         = guard "matchCoercion: NthCo" (i_l == i_r) >> matchCoercion rn2 (co_l) (co_r)
+matchCoercion rn2 (InstCo co_l ty_l)       (InstCo co_r ty_r)       = liftM2 (++) (matchCoercion rn2 (co_l) (co_r)) (matchType rn2 (ty_l) (ty_r))
+matchCoercion _ _ _ = fail "matchCoercion"
+
+matchTerm :: RnEnv2 -> AnnedTerm -> AnnedTerm -> Match [MatchLR]
+matchTerm rn2 = matchAnned (matchTerm' rn2)
+
+-- TODO: allow lets on only one side? Useful for matching e.g. (let x = 2 in y + x) with (z + 2)
+matchTerm' :: RnEnv2 -> Tag -> TermF Anned -> Tag -> TermF Anned -> Match [MatchLR]
+matchTerm' rn2 _    (Var x_l)                  _    (Var x_r)                  = matchVar rn2 x_l x_r
+matchTerm' rn2 _    (Var x_l)                  tg_r e_r                        = matchVarL rn2 x_l (annedTerm tg_r e_r)
+matchTerm' rn2 tg_l e_l                        _    (Var x_r)                  = matchVarR rn2 (annedTerm tg_l e_l) x_r
+matchTerm' rn2 tg_l (Value v_l)                tg_r (Value v_r)                = matchValue rn2 tg_l v_l tg_r v_r
+matchTerm' rn2 _    (TyApp e_l ty_l)           _    (TyApp e_r ty_r)           = liftM2 (++) (matchTerm rn2 e_l e_r) (matchType rn2 ty_l ty_r)
+matchTerm' rn2 _    (App e_l x_l)              _    (App e_r x_r)              = liftM2 (++) (matchTerm rn2 e_l e_r) (matchVar   rn2 x_l x_r)
+matchTerm' rn2 _    (PrimOp pop_l tys_l es_l)  _    (PrimOp pop_r tys_r es_r)  = guard "matchTerm: primop" (pop_l == pop_r) >> liftM2 (++) (matchList (matchType rn2) tys_l tys_r) (matchList (matchTerm rn2) es_l es_r)
+matchTerm' rn2 _    (Case e_l x_l ty_l alts_l) _    (Case e_r x_r ty_r alts_r) = liftM3 app3 (matchTerm rn2 e_l e_r) (matchType rn2 ty_l ty_r) (matchIdCoVarBndr False rn2 x_l x_r $ \rn2 -> matchAlts rn2 alts_l alts_r)
+matchTerm' rn2 _    (Let x_l e1_l e2_l)        _    (Let x_r e1_r e2_r)        = liftM2 (++) (matchTerm rn2 e1_l e1_r) $ matchIdCoVarBndr False rn2 x_l x_r $ \rn2 -> matchTerm rn2 e2_l e2_r
+matchTerm' rn2 _    (LetRec xes_l e_l)         _    (LetRec xes_r e_r)         = matchIdCoVarBndrsRec rn2 xs_l xs_r $ \rn2 -> liftM2 (++) (matchList (matchTerm rn2) es_l es_r) (matchTerm rn2 e_l e_r)
+  where (xs_l, es_l) = unzip xes_l
+        (xs_r, es_r) = unzip xes_r
+matchTerm' rn2 _    (Cast e_l co_l)            _    (Cast e_r co_r)            = liftM2 (++) (matchTerm rn2 (e_l) (e_r)) (matchCoercion rn2 (co_l) (co_r))
+matchTerm' _ _ _ _ _ = fail "matchTerm"
+
+matchValue :: RnEnv2 -> Tag -> AnnedValue -> Tag -> AnnedValue -> Match [MatchLR]
+-- TODO: value instance matching (need to check for a solitary update at stack top..)
+--matchValue rn2 _    (Indirect x_l)               _    (Indirect x_r)               = matchVar rn2 x_l x_r
+--matchValue rn2 _    (Indirect x_l)               tg_r v_r                          = matchVarL rn2 x_l (annedTerm tg_r (Value v_r))
+--matchValue rn2 tg_l v_l                          _    (Indirect x_r)               = matchVarR rn2 (annedTerm tg_l (Value v_l)) x_r
+matchValue rn2 _    (TyLambda a_l e_l)           _    (TyLambda a_r e_r)           = matchTyVarBndr rn2 a_l a_r $ \rn2 -> matchTerm rn2 e_l e_r
+matchValue rn2 _    (Lambda x_l e_l)             _    (Lambda x_r e_r)             = matchIdCoVarBndr True rn2 x_l x_r $ \rn2 -> matchTerm rn2 e_l e_r
+matchValue rn2 _    (Data dc_l tys_l cos_l xs_l) _    (Data dc_r tys_r cos_r xs_r) = guard "matchValue: datacon" (dc_l == dc_r) >> liftM3 app3 (matchList (matchType rn2) tys_l tys_r) (matchList (matchCoercion rn2) cos_l cos_r) (matchList (matchVar rn2) xs_l xs_r)
+matchValue _   _    (Literal l_l)                _    (Literal l_r)                = guard "matchValue: literal" (l_l == l_r) >> return []
+matchValue rn2 _    (Coercion co_l)              _    (Coercion co_r)              = matchCoercion rn2 (co_l) (co_r)
+matchValue _ _ _ _ _ = fail "matchValue"
+
+matchAlts :: RnEnv2 -> [AnnedAlt] -> [AnnedAlt] -> Match [MatchLR]
+matchAlts rn2 = matchList (matchAlt rn2)
+
+matchAlt :: RnEnv2 -> AnnedAlt -> AnnedAlt -> Match [MatchLR]
+matchAlt rn2 (alt_con_l, alt_e_l) (alt_con_r, alt_e_r) = matchAltCon rn2 alt_con_l alt_con_r $ \rn2 -> matchTerm rn2 alt_e_l alt_e_r
+
+matchAltCon :: RnEnv2 -> AltCon -> AltCon -> (RnEnv2 -> Match [MatchLR]) -> Match [MatchLR]
+matchAltCon rn2 (DataAlt dc_l as_l qs_l xs_l) (DataAlt dc_r as_r qs_r xs_r) k = guard "matchAltCon: datacon" (dc_l == dc_r) >> (matchTyVarBndrs rn2 as_l as_r $ \rn2 -> matchIdCoVarBndrs False rn2 qs_l qs_r $ \rn2 -> matchIdCoVarBndrs False rn2 xs_l xs_r k)
+matchAltCon rn2 (LiteralAlt l_l)              (LiteralAlt l_r)              k = guard "matchAltCon: literal" (l_l == l_r) >> k rn2
+matchAltCon rn2 DefaultAlt                    DefaultAlt                    k = k rn2
+matchAltCon _ _ _ _ = fail "matchAltCon"
+
+matchVarBndr :: Bool -> RnEnv2 -> Var -> Var -> (RnEnv2 -> Match [MatchLR]) -> Match [MatchLR]
+matchVarBndr lambdaish rn2 v_l v_r k | isId      v_l = guard "matchVarBndr: Id"      (isId      v_r) >> matchIdCoVarBndr lambdaish rn2 v_l v_r k
+                                     | isKindVar v_l = guard "matchVarBndr: KindVar" (isKindVar v_r) >> matchTyVarBndr             rn2 v_l v_r k -- Type variable binders never
+                                     | isTyVar   v_l = guard "matchVarBndr: TyVar"   (isTyVar   v_r) >> matchTyVarBndr             rn2 v_l v_r k -- lose work sharing
+                                     | otherwise     = panic "matchVarBndr"
+
+matchTyVarBndr :: RnEnv2 -> TyVar -> TyVar -> (RnEnv2 -> Match [MatchLR]) -> Match [MatchLR]
+matchTyVarBndr rn2 a_l a_r k = liftM2 (++) (matchKind rn2 (tyVarKind a_l) (tyVarKind a_r)) (k (rnBndr2 rn2 a_l a_r))
+
+matchIdCoVarBndr :: Bool -> RnEnv2 -> Id -> Id -> (RnEnv2 -> Match [MatchLR]) -> Match [MatchLR]
+matchIdCoVarBndr lambdaish rn2 x_l x_r k = liftM (\((), eqs) -> eqs) $ matchIdCoVarBndrFlexible lambdaish rn2 x_l x_r $ \rn2 -> liftM ((,,) rn2 ()) $ k rn2
+
+matchIdCoVarBndrFlexible :: Bool -> RnEnv2 -> Id -> Id -> (RnEnv2 -> Match (RnEnv2, a, [MatchLR])) -> Match (a, [MatchLR])
+matchIdCoVarBndrFlexible lambdaish rn2 x_l x_r k = do
+    (rn2, a, eqs1) <- k rn2'
+    eqs1 <- (if fLOAT_TO_MATCH then mapM (checkMatchLR lambdaish x_l x_r) else return) eqs1
+    eqs2 <- mk_match_x rn2
+    return (a, eqs1 ++ eqs2)
+  where (rn2', mk_match_x) = matchIdCoVarBndr' rn2 x_l x_r
+
+checkMatchLR :: Bool -> Id -> Id -> MatchLR -> Match MatchLR
+checkMatchLR lambdaish x_l x_r lr = case lr of
+    VarL _ e_r | x_r `elemVarSet` annedTermFreeVars e_r -> fail "checkMatchLR: deferred term mentioned rigid right variable"
+               | lambdaish, not (termIsCheap e_r)       -> fail "checkMatchLR: expensive deferred (right) term escaping lambda"
+    VarR e_l _ | x_l `elemVarSet` annedTermFreeVars e_l -> fail "checkMatchLR: deferred term mentioned rigid left variable"
+               | lambdaish, not (termIsCheap e_l)       -> fail "checkMatchLR: expensive deferred (left) term escaping lambda"
+    _ -> return lr
+
+-- We have to be careful to match the "fragile" IdInfo for binders as well as the obvious type information
+-- (idSpecialisation :: Id -> SpecInfo, realIdUnfolding :: Id -> Unfolding)
+matchIdCoVarBndr' :: RnEnv2 -> Id -> Id -> (RnEnv2, RnEnv2 -> Match [MatchLR])
+matchIdCoVarBndr' init_rn2 x_l x_r = (pprTraceSC "matchIdCoVarBndr'" (ppr (x_l, x_r)) $ rnBndr2 init_rn2 x_l x_r, \rn2 -> matchIdCoVarBndrExtras rn2 x_l x_r)
+
+matchBndrExtras :: RnEnv2 -> Var -> Var -> Match [MatchLR]
+matchBndrExtras rn2 v_l v_r
+  | isId      v_l = guard "matchBndrExtras: Id"      (isId      v_r) >> matchIdCoVarBndrExtras rn2 v_l v_r
+  | isKindVar v_l = guard "matchBndrExtras: KindVar" (isKindVar v_r) >> matchTyVarBndrExtras   rn2 v_l v_r
+  | isTyVar   v_l = guard "matchBndrExtras: TyVar"   (isTyVar   v_r) >> matchTyVarBndrExtras   rn2 v_l v_r
+  | otherwise     = panic "matchBndrExtras"
+
+matchTyVarBndrExtras :: RnEnv2 -> TyVar -> TyVar -> Match [MatchLR]
+matchTyVarBndrExtras rn2 a_l a_r = matchKind rn2 (tyVarKind a_l) (tyVarKind a_r)
+
+matchIdCoVarBndrExtras :: RnEnv2 -> Id -> Id -> Match [MatchLR]
+matchIdCoVarBndrExtras rn2 x_l x_r = liftM3 app3 (matchUnfolding rn2 (realIdUnfolding x_l) (realIdUnfolding x_r)) (matchSpecInfo rn2 (idSpecialisation x_l) (idSpecialisation x_r)) (matchType rn2 (idType x_l) (idType x_r))
+
+-- TODO: currently insists that the LHS has no unfolding/RULES. (This is not as bad as it seems since unstable unfoldings match). Can we do better?
+matchIdCoVarBndrExtrasL :: RnEnv2 -> Id -> AnnedTerm -> Match [MatchLR]
+matchIdCoVarBndrExtrasL rn2 x_l e_r = liftM3 app3 (matchUnfolding rn2 (realIdUnfolding x_l) Core.noUnfolding) (matchSpecInfo rn2 (idSpecialisation x_l) emptySpecInfo) (matchType rn2 (idType x_l) (termType e_r))
+
+-- TODO: currently insists that the LHS has no unfolding/RULES. (This is not as bad as it seems since unstable unfoldings match). Can we do better?
+matchIdCoVarBndrExtrasR :: RnEnv2 -> AnnedTerm -> Id -> Match [MatchLR]
+matchIdCoVarBndrExtrasR rn2 e_l x_r = liftM3 app3 (matchUnfolding rn2 Core.noUnfolding (realIdUnfolding x_r)) (matchSpecInfo rn2 emptySpecInfo (idSpecialisation x_r)) (matchType rn2 (termType e_l) (idType x_r))
+
+matchSpecInfo :: RnEnv2 -> SpecInfo -> SpecInfo -> Match [MatchLR]
+matchSpecInfo rn2 (SpecInfo rules_l _) (SpecInfo rules_r _) = matchList (matchRule rn2) rules_l rules_r
+
+matchRule :: RnEnv2 -> Core.CoreRule -> Core.CoreRule -> Match [MatchLR]
+matchRule _   (Core.BuiltinRule { Core.ru_name = name1 }) (Core.BuiltinRule { Core.ru_name = name2 }) = guard "matchRule: BuiltinRule" (name1 == name2) >> return [] -- NB: assume builtin rules generate RHSes without any free vars!
+matchRule rn2 (Core.Rule { Core.ru_bndrs = vs_l, Core.ru_args = args_l, Core.ru_rhs = rhs_l }) (Core.Rule { Core.ru_bndrs = vs_r, Core.ru_args = args_r, Core.ru_rhs = rhs_r }) = matchMany (matchVarBndr True) rn2 vs_l vs_r $ \rn2 -> liftM2 (++) (matchList (matchCore rn2) args_l args_r) (matchCore rn2 rhs_l rhs_r)
+matchRule _ _ _ = fail "matchRule"
+
+matchUnfolding :: RnEnv2 -> Core.Unfolding -> Core.Unfolding -> Match [MatchLR]
+matchUnfolding rn2 (Core.CoreUnfolding { Core.uf_tmpl = rhs1, Core.uf_src = src1 }) (Core.CoreUnfolding { Core.uf_tmpl = rhs2, Core.uf_src = src2 })
+  | Core.isStableSource src1, Core.isStableSource src2 = matchCore rn2 rhs1 rhs2
+matchUnfolding rn2 (Core.DFunUnfolding _ _ args1) (Core.DFunUnfolding _ _ args2) = matchList (matchCore rn2) args1 args2
+-- It is OK to match any *unstable* unfolding against any other one
+matchUnfolding _ unf1 unf2 | not (Core.isStableUnfolding unf1), not (Core.isStableUnfolding unf2) = return []
+matchUnfolding _ _ _ = fail "matchUnfolding"
+
+matchTickish :: RnEnv2 -> Core.Tickish Id -> Core.Tickish Id -> Match [MatchLR]
+matchTickish rn2 (Core.Breakpoint { Core.breakpointId = id_l, Core.breakpointFVs = fvs_l }) (Core.Breakpoint { Core.breakpointId = id_r, Core.breakpointFVs = fvs_r })
+  = guard "matchTickish: Breakpoint" (id_l == id_r) >> matchList (matchVar rn2) fvs_l fvs_r
+matchTickish _ (Core.Breakpoint {}) _ = fail "matchTickish: Breakpoint vs ?"
+matchTickish _ _ (Core.Breakpoint {}) = fail "matchTickish: ? vs Breakpoint"
+matchTickish _ ti_l ti_r = guard "matchTickish: non-Breakpoint not exacttly equal" (ti_l == ti_r) >> return []
+
+-- TODO: match instantiation within Core?
+matchCore :: RnEnv2 -> Core.CoreExpr -> Core.CoreExpr -> Match [MatchLR]
+matchCore rn2 (Core.Var x_l)       (Core.Var x_r)       = matchVar rn2 x_l x_r
+matchCore _   (Core.Lit l_l)       (Core.Lit l_r)       = guard "matchCore: Lit" (l_l == l_r) >> return []
+matchCore rn2 (Core.App e1_l e2_l) (Core.App e1_r e2_r) = liftM2 (++) (matchCore rn2 e1_l e1_r) (matchCore rn2 e2_l e2_r)
+matchCore rn2 (Core.Lam x_l e_l)   (Core.Lam x_r e_r)   = matchVarBndr True rn2 x_l x_r $ \rn2 -> matchCore rn2 e_l e_r
+matchCore rn2 (Core.Let (Core.NonRec x_l e1_l) e2_l) (Core.Let (Core.NonRec x_r e1_r) e2_r)
+  = liftM2 (++) (matchCore rn2 e1_l e1_r) $ matchVarBndr False rn2 x_l x_r $ \rn2 -> matchCore rn2 e2_l e2_r
+matchCore rn2 (Core.Let (Core.Rec xes_l) e_l) (Core.Let (Core.Rec xes_r) e_r)
+  = matchIdCoVarBndrsRec rn2 xs_l xs_r $ \rn2 -> liftM2 (++) (matchList (matchCore rn2) es_l es_r) (matchCore rn2 e_l e_r)
+      where (xs_l, es_l) = unzip xes_l
+            (xs_r, es_r) = unzip xes_r
+matchCore rn2 (Core.Case e_l x_l ty_l alts_l) (Core.Case e_r x_r ty_r alts_r) = liftM3 app3 (matchCore rn2 e_l e_r) (matchType rn2 ty_l ty_r) (matchIdCoVarBndr False rn2 x_l x_r $ \rn2 -> matchCoreAlts rn2 alts_l alts_r)
+matchCore rn2 (Core.Cast e_l co_l)            (Core.Cast e_r co_r)            = liftM2 (++) (matchCore rn2 e_l e_r) (matchCoercion rn2 co_l co_r)
+matchCore rn2 (Core.Tick ti_l e_l)            (Core.Tick ti_r e_r)            = liftM2 (++) (matchTickish rn2 ti_l ti_r) (matchCore rn2 e_l e_r)
+matchCore rn2 (Core.Type ty_l)                (Core.Type ty_r)                = matchType rn2 ty_l ty_r
+matchCore rn2 (Core.Coercion co_l)            (Core.Coercion co_r)            = matchCoercion rn2 co_l co_r
+matchCore _ _ _ = fail "matchCore"
+
+matchCoreAlts :: RnEnv2 -> [Core.CoreAlt] -> [Core.CoreAlt] -> Match [MatchLR]
+matchCoreAlts rn2 = matchList (matchCoreAlt rn2)
+
+matchCoreAlt :: RnEnv2 -> Core.CoreAlt -> Core.CoreAlt -> Match [MatchLR]
+matchCoreAlt rn2 (alt_con_l, vs_l, alt_e_l) (alt_con_r, vs_r, alt_e_r) = guard "matchCoreAlt" (alt_con_l == alt_con_r) >> matchMany (matchVarBndr False) rn2 vs_l vs_r (\rn2 -> matchCore rn2 alt_e_l alt_e_r)
+
+matchTyVarBndrs :: RnEnv2 -> [TyVar] -> [TyVar] -> (RnEnv2 -> Match [MatchLR]) -> Match [MatchLR]
+matchTyVarBndrs = matchMany matchTyVarBndr
+
+matchIdCoVarBndrs :: Bool -> RnEnv2 -> [Id] -> [Id] -> (RnEnv2 -> Match [MatchLR]) -> Match [MatchLR]
+matchIdCoVarBndrs lambdaish = matchMany (matchIdCoVarBndr lambdaish)
+
+matchIdCoVarBndrsRec :: RnEnv2 -> [Id] -> [Id] -> (RnEnv2 -> Match [MatchLR]) -> Match [MatchLR]
+matchIdCoVarBndrsRec = matchManyRec (matchIdCoVarBndrFlexible False)
+
+matchMany :: (RnEnv2 -> v -> v -> (RnEnv2 -> Match b) -> Match b)
+          -> RnEnv2 -> [v] -> [v] -> (RnEnv2 -> Match b) -> Match b
+matchMany mtch init_rn2 init_xs_l init_xs_r k = go init_rn2 init_xs_l init_xs_r
+  where
+    go rn2 []         []         = k rn2
+    go rn2 (x_l:xs_l) (x_r:xs_r) = mtch rn2 x_l x_r $ \rn2 -> go rn2 xs_l xs_r
+    go _ _ _ = fail "matchMany"
+
+matchManyRec :: forall b v.
+                (forall a. RnEnv2 -> v -> v -> (RnEnv2 -> Match (RnEnv2, a, b)) -> Match (a, b))
+             -> RnEnv2 -> [v] -> [v] -> (RnEnv2 -> Match b) -> Match b
+matchManyRec mtch init_rn2 init_xs_l init_xs_r k = liftM snd $ go init_rn2 init_xs_l init_xs_r
+  where
+    go :: RnEnv2 -> [v] -> [v] -> Match (RnEnv2, b)
+    go rn2 []         []         = liftM ((,) rn2) $ k rn2
+    go rn2 (x_l:xs_l) (x_r:xs_r) = mtch rn2 x_l x_r $ \rn2 -> liftM (\(rn2, b) -> (rn2, rn2, b)) $ go rn2 xs_l xs_r
+    go _ _ _ = fail "matchManyRec"
+
+matchVar :: RnEnv2 -> Out Id -> Out Id -> Match [MatchLR]
+matchVar rn2 x_l x_r = fmap maybeToList (matchVar_maybe rn2 x_l x_r)
+
+matchVar_maybe :: RnEnv2 -> Out Id -> Out Id -> Match (Maybe MatchLR)
+matchVar_maybe rn2 x_l x_r = case (rnOccL_maybe rn2 x_l, rnOccR_maybe rn2 x_r) of
+     -- Both rigidly bound: match iff they rename to the same thing
+    (Just x_l', Just x_r') -> pprTraceSC "matchVar_maybe(rigid)" (ppr (x_l, x_r)) $ guard "matchVar: rigid" (x_l' == x_r') >> return Nothing
+     -- Both bound by let: defer decision about matching
+    (Nothing, Nothing)     -> pprTraceSC "matchVar_maybe(flexi)" (ppr (x_l, x_r)) $ return (Just (VarLR x_l x_r))
+     -- One bound by let and one bound rigidly: don't match
+    _                      -> fail "matchVar: mismatch"
+
+matchVarL :: RnEnv2 -> Out Id -> Out AnnedTerm -> Match [MatchLR]
+matchVarL rn2 x_l e_r = fmap maybeToList (matchVarL_maybe rn2 x_l e_r)
+
+matchVarL_maybe :: RnEnv2 -> Out Id -> Out AnnedTerm -> Match (Maybe MatchLR)
+matchVarL_maybe rn2 x_l e_r = guard "matchVarL_maybe: no float-to-match"  fLOAT_TO_MATCH >> case rnOccL_maybe rn2 x_l of
+     -- Left rigidly bound: matching is impossible (assume we already tried matchVar_maybe)
+    Just _  -> fail "matchVar: rigid"
+     -- Both bound by let: defer decision about matching
+    Nothing -> return (Just (VarL x_l e_r))
+
+matchVarR :: RnEnv2 -> Out AnnedTerm -> Out Id -> Match [MatchLR]
+matchVarR rn2 e_l x_r = fmap maybeToList (matchVarR_maybe rn2 e_l x_r)
+
+matchVarR_maybe :: RnEnv2 -> Out AnnedTerm -> Out Id -> Match (Maybe MatchLR)
+matchVarR_maybe rn2 e_l x_r = guard "matchVarR_maybe: no float-to-match" fLOAT_TO_MATCH >> case rnOccR_maybe rn2 x_r of
+     -- Right rigidly bound: matching is impossible (assume we already tried matchVar_maybe)
+    Just _  -> fail "matchVar: rigid"
+     -- Both bound by let: defer decision about matching
+    Nothing -> return (Just (VarR e_l x_r))
+
+matchList :: (a -> a -> Match [MatchLR])
+          -> [a] -> [a] -> Match [MatchLR]
+matchList mtch xs_l xs_r = fmap concat (zipWithEqualM mtch xs_l xs_r)
+
+matchIn :: (InScopeSet -> Renaming -> a -> a)
+        -> (RnEnv2 -> a -> a -> Match b)
+        -> RnEnv2 -> In a -> In a -> Match b
+matchIn rnm mtch rn2 (rn_l, x_l) (rn_r, x_r) = mtch rn2 (rnm iss rn_l x_l) (rnm iss rn_r x_r)
+  where iss = rnInScopeSet rn2 -- NB: this line is one of the few things that relies on the RnEnv2 InScopeSet being correct
+
+matchEC :: MatchMode -> RnEnv2 -> Stack -> Stack -> Match (RnEnv2, Stack, RnEnv2 -> Match [MatchLR])
+matchEC mm init_rn2 = go (init_rn2, \_ -> return [])
+  where
+    go (rn2', meqs) (Loco gen_l)   k_r            = guard "matchEC: instance match disallowed" (nullTrain k_r || mayInstantiate (matchInstanceMatching mm) gen_l) >> return (rn2', k_r, meqs)
+    go _            _              (Loco _)       = fail "matchEC: instantiation on left"
+    go (rn2', meqs) (Car kf_l k_l) (Car kf_r k_r) = do
+      (rn2'', meqs') <- matchECFrame rn2' kf_l kf_r
+      go (rn2'', \rn2 -> liftM2 (++) (meqs rn2) (meqs' rn2)) k_l k_r
+
+matchECFrame :: RnEnv2 -> Tagged StackFrame -> Tagged StackFrame -> Match (RnEnv2, RnEnv2 -> Match [MatchLR])
+matchECFrame init_rn2 kf_l kf_r = go (tagee kf_l) (tagee kf_r)
+  where
+    go :: StackFrame -> StackFrame -> Match (RnEnv2, RnEnv2 -> Match [MatchLR])
+    go (Apply x_l')                          (Apply x_r')                          = return (init_rn2, \rn2 -> matchVar rn2 x_l' x_r')
+    go (TyApply ty_l')                       (TyApply ty_r')                       = return (init_rn2, \rn2 -> matchType rn2 ty_l' ty_r')
+    go (Scrutinise x_l' ty_l' in_alts_l)     (Scrutinise x_r' ty_r' in_alts_r)     = return (init_rn2, \rn2 -> liftM2 (++) (matchType rn2 ty_l' ty_r') (matchIdCoVarBndr False rn2 x_l' x_r' $ \rn2 -> matchIn renameAnnedAlts matchAlts rn2 in_alts_l in_alts_r))
+    go (PrimApply pop_l tys_l' as_l in_es_l) (PrimApply pop_r tys_r' as_r in_es_r) = return (init_rn2, \rn2 -> guard "matchECFrame: primop" (pop_l == pop_r) >> liftM3 (\x y z -> x ++ y ++ z) (matchList (matchType rn2) tys_l' tys_r') (matchList (matchAnned (matchCoerced matchAnswer rn2)) as_l as_r) (matchList (matchIn renameAnnedTerm matchTerm rn2) in_es_l in_es_r))
+    go (StrictLet x_l' in_e_l)               (StrictLet x_r' in_e_r)               = return (init_rn2, \rn2 -> matchIdCoVarBndr False rn2 x_l' x_r' $ \rn2 -> matchIn renameAnnedTerm matchTerm rn2 in_e_l in_e_r)
+    go (CastIt co_l')                        (CastIt co_r')                        = return (init_rn2, \rn2 -> matchCoercion rn2 co_l' co_r')
+    go (Update x_l')                         (Update x_r')                         = return (matchIdCoVarBndr' init_rn2 x_l' x_r')
+    go _ _ = fail "matchECFrame"
+
+--- Returns a renaming from the list only if the list maps a "left" variable to a unique "right" variable
+-- If the left side var was free, we might have assumed two different corresponding rights for it. This is not necessarily a problem:
+--      a |-> True; ()<(a, a)> `match` c |-> True; d |-> True; ()<(c, d)>
+--      a |-> True; ()<(a, a)> `match` c |-> True; d |-> c; ()<(c, d)>
+-- However, I'm going to reject this for now (simpler).
+--
+-- TODO: arguably I should check that this is actually a true *bijection* not just a *function* because a renaming like
+-- {x |-> a, y |-> a} means that if we carrried on supercompiling here we could exploit more equalities (via positive information
+-- propagation - imagine we scrutinise x and later scrutinise y) and potentially get better code that at the tieback site. I need to
+-- check how important this is in practice.
+safeMkMatchRenaming :: [(Var, Var)] -> Match MatchRenaming
+safeMkMatchRenaming eqs = guard "safeMkMatchRenaming" (all (\(x_l, x_r) -> M.lookup x_l eqs_map == Just x_r) eqs) >> return eqs_map
+  where eqs_map = M.fromList eqs
+
+
+matchPureHeap :: MatchMode -> RnEnv2 -> Stack -> [MatchLR] -> PureHeap -> Heap -> Match (Heap, MatchRenaming)
+matchPureHeap mm rn2 k_inst init_free_eqs h_l (Heap h_r ids_r)
+  = do (h_inst, used_r) <- fvsInstLoop M.empty emptyVarSet k_inst_fvs
+       (heap_inst, xys) <- matchLoop [] (Heap h_inst ids_r) [] init_free_eqs emptyVarSet used_r
+       liftM ((,) heap_inst) (safeMkMatchRenaming xys)
+    -- NB: if there are dead bindings in the left PureHeap then the output Renaming will not contain a renaming for their binders.
+    --
+    -- NB: The resulting equalities must only relate local vars to local vars (in which case we can discard them, because
+    -- matchLoop would have ensured that they were fulfilled) or free vars to free vars (in which case we propagate them upward).
+    --
+    -- NB: We already know there are no eqs that relate update-frame bound (rigid) variables.
+  where
+    (k_inst_bvs, k_inst_fvs) = stackOpenFreeVars k_inst
+
+    -- NB: must respect work-sharing for non-values
+    --  x |-> e1, y |-> e1; (x, y) `match` x |-> e1; (x, x) == Nothing
+    --  x |-> e1; (x, x) `match` x |-> e1; y |-> e1; (x, y) == Nothing (though this is more questionable, it seems a consistent choice)
+    -- NB: treat equal values as equal regardless of duplication
+    --  x |-> v, y |-> v; (x, y) `match` x |-> v; (x, x) /= Nothing
+    -- TODO: look through variables on both sides
+    --  x |-> e1; (x, x) `match` x |-> e1; y |-> x `match` (x, y) /= Nothing
+    --  x |-> e1, y |-> x; (x, y) `match` x |-> e1 `match` (x, x) /= Nothing
+    --
+    -- It used to be important to allow instantiatation of a dynamic variable with a static *variable*.
+    -- This was so because if we didn't tie back to a situation where all that had changed was that one more
+    -- variable was static, we would immediately whistle because the tagbags would be the same.
+    --
+    -- In the new world, we record staticness as phantom heap bindings, so this just doesn't figure in at all.
+    -- We can account for staticness using the standard generalisation mechanism, and there is no need for the
+    -- matcher to have hacks like that (though we still have to be careful about how we match phantoms).
+    
+    matchLoop _     heap_inst xys [] _ _ = return (heap_inst, xys)
+    matchLoop known (Heap h_inst ids_r) xys (lr:free_eqs) used_l used_r
+       -- Perhaps we have already assumed this equality is true?
+       -- NB: it is OK to do exact syntactic equality on VarL/VarR here because we always rename new equalities generated in
+       -- this loop using the same InScopeSet (that from rn2) so only a finite number of distinct binders will be generated.
+      | lr `elem` known = matchLoop known (Heap h_inst ids_r) xys free_eqs used_l used_r
+      | otherwise = pprTraceSC "matchLoop" (ppr lr) $
+                    -- See Note [Non-terminating instance matches] in MSG.hs for the story on the guards here
+                    case (case lr of VarLR x_l x_r -> (go_template (Just [(x_l, x_r)]) (matchBndrExtras rn2 x_l x_r),         ids_r,                        x_l == x_r && x_l `elemInScopeSet` matchCommonHeapVars mm, lookupUsed used_l x_l h_l,                                                       x_r, lookupUsed used_r x_r h_r)
+                                     VarL  x_l e_r -> (go_template (Just [(x_l, x_r)]) (matchIdCoVarBndrExtrasL rn2 x_l e_r), ids_r `extendInScopeSet` x_r, False,                                                     lookupUsed used_l x_l h_l,                                                       x_r, Control.Monad.guard False >> Just (InternallyBound, Right (Just (used_r, e_r))))
+                                       where x_r = uniqAway ids_r (zapFragileIdInfo (x_l `setVarType` termType e_r))
+                                     VarR  e_l x_r -> (go_template Nothing             (matchIdCoVarBndrExtrasR rn2 e_l x_r), ids_r,                        False,                                                     Control.Monad.guard False >> Just (InternallyBound, Right (Just (used_l, e_l))), x_r, lookupUsed used_r x_r h_r)) of
+           -- If matching an internal let, it is possible that variables occur free. Insist that free-ness matches:
+           -- TODO: actually I'm pretty sure that the heap binds *everything* now. These cases could probably be removed,
+           -- though they don't do any particular harm.
+          (go, ids_r, _, Nothing, _, Nothing) -> go False (Heap h_inst ids_r) [] used_l used_r
+          (_,  _,     _, Just _,  _, Nothing) -> failLoop "matching binding on left not present in the right"
+          (_,  _,     _, Nothing, _, Just _)  -> failLoop "matching binding on right not present in the left"
+          (go, ids_r, certain_match, Just hb_l, ei_x_l_x_r, Just hb_r) -> case (hb_l, hb_r) of
+               -- If the template provably doesn't use this heap binding, we can match it against anything at all
+              ((InternallyBound, Left _), _) -> go True (Heap h_inst ids_r) [] used_l used_r
+               -- If the template internalises a binding of this form, check that the matchable semantics is the same.
+               -- If the matchable doesn't have a corresponding binding tieback is impossible because we have less info this time.
+              ((InternallyBound, Right (Just (used_l', e_l'))), (how_r, mb_e_r')) -> case mb_e_r' of
+                  Right (Just (used_r', e_r')) -> match_term certain_match rn2 e_l' e_r' >>= \extra_free_eqs -> go True (Heap h_inst ids_r) extra_free_eqs used_l' used_r'
+                  Right Nothing                -> failLoop "right side of InternallyBound already used"
+                  Left _                       -> failLoop $ "can only match a termful InternallyBound on left against an actual term, not a termless " ++ show how_r ++ " binding"
+               -- If the template has no information but exposes a lambda, we can rename to tie back.
+               -- If there is a corresponding binding in the matchable we can't tieback because we have more info this time.
+               --
+               -- NB: this may cause us to instantiate a lambda-bound var with one that is presently let-bound. The alternative
+               -- (almost certainly an sc-stop) is worse, though... Doing this really matters; see for example the Bernouilli benchmark.
+               --
+               -- TODO: give let-bound nothings tags and generalise to get the same effect?
+              ((LambdaBound, Left stuff_l), (how_r, mb_e_r')) -> case mb_e_r' of
+                  Left _       -> (if how_r == LetBound then pprTraceSC "Downgrading" empty else id) $
+                                  go False (Heap h_inst ids_r) [] used_l used_r
+                  Right mb_er' | Left gen_l <- stuff_l
+                               , mayInstantiate (matchInstanceMatching mm) gen_l
+                               -> instLoop h_inst ei_x_l_x_r how_r used_r (Right mb_er') >>= \(h_inst, used_r') -> go False (Heap h_inst ids_r) [] used_l used_r'
+                               | otherwise
+                               -> failLoop "instance match disallowed"
+               -- If the template has an unfolding, we must do lookthrough
+              ((LambdaBound, Right (Just (used_l', e_l'))), (_how_r, mb_e_r')) -> case mb_e_r' of
+                  Right (Just (used_r', e_r')) -> match_term certain_match rn2 e_l' e_r' >>= \extra_free_eqs -> go False (Heap h_inst ids_r) extra_free_eqs used_l' used_r'
+                  Right Nothing                -> failLoop "right side of LambdaBound already used"
+                  Left _                       -> failLoop "can only match a termful LambdaBound on left against an actual term"
+               -- We assume the supercompiler gives us no-shadowing for let-bound names, so if two names are the same they must refer to the same thing
+               -- NB: because I include this case, we may not include a renaming for some lambda-bound variables in the final knowns (if they are bound
+               -- above the let-bound thing)
+               --
+               -- Interestingly, doing this matching here also improves matching in the case where a previous state had a more-or-less
+               -- evaluated version of this heap binding in place. We "know" that we can match them since they originated from the same
+               -- heap binding, even though evaluation may have changed their shape.
+               --
+               -- Of course, we still need to match the FVs on both sides. For example, the LHS could be {x |-> Just y} with the RHS
+               -- {x |-> Just y, y |-> True} -- better not tie back in this situation, so we validate that the y bindings still match.
+               -- This also ensures that the outgoing knowns can be used to build a renaming that includes the RHS of these bindings.
+               --
+               -- OK, I don't think this is safe in the case where either side is not LetBound. The reason is that we might have:
+               --     D[(let x = e1 in x, let x = e2 in x)]
+               -- ==> (D[let x = e1 in x], D[let x = e2 in x])
+               --
+               -- Which floats to:
+               --     let h0 = D[let x = e1 in x]
+               --     in in (h0, D[let x = e2 in x])
+               --
+               -- We better not tieback the second tuple component to h0 on the basis that the two x binders match!
+               -- They are only guaranteed to match if the are **Let bound**, because in that case those binders must have been
+               -- created by a common ancestor and hence we can just match the uniques to determine whether the binders are the "same".
+               -- It is NOT safe to do this is both/either sides are LambdaBound, because we have no guarantee of a common ancestor in that case.
+              ((LetBound, mb_e_l'), (_how_r, mb_e_r'))
+                | VarLR x_l x_r <- lr, x_l == x_r -> case (mb_e_l', mb_e_r') of -- TODO: even match LetBounds against non-VarLR
+                  (Left _ ,                      Left _)                       -> go True (Heap h_inst ids_r) [] used_l used_r
+                  (Right (Just (used_l', e_l')), Right (Just (used_r', e_r'))) -> ASSERT2(annedTermFreeVars e_r' `subVarSet` annedTermFreeVars e_l', text "match" <+> ppr (x_l, e_l', x_r, _how_r, e_r'))
+                                                                                  go True (Heap h_inst ids_r) [VarLR x x | x <- varSetElems (annedTermFreeVars e_l')] used_l' used_r'
+                  _                                                            -> failLoop "insane LetBounds"
+               -- If the template doesn't lambda abstract, we can't rename. Only tieback if we have an exact *name* match.
+               --
+               -- You might think that we could do better than this if both the LHS and RHS had unfoldings, by matching them.
+               -- However, this is very dangerous because we don't want to match the template {x |-> let {Just y}, y |-> lam {}}
+               -- against the matchable {x' |-> let {Just y'}, y' |-> lam {}}, since the template may still be able to reach y via the binding
+               -- for x (we renamed the lambda-abstracted y to y' so there is nothing to fear from there).
+               --
+               -- NB: we can treat this *almost* exactly like the LambdaBound+unfolding case now since we have the invariant that LetBound things never
+               -- refer to LambdaBound things. *However* we anticipate that doing so would almost always fail to tieback, so we elect to just stick with
+               -- the "cheap-but-inaccurate" name-matching heuristic.
+                | otherwise -> failLoop "LetBound"
+              _ -> failLoop "left side of InternallyBound/LambdaBound already used"
+      where -- If the two RHSs have a common name then they certainly started off having the same meaning (modulo FVs), so we
+            -- can almost certainly match them together. But there is a wrinkle: we might have started off with the heap
+            --   x |-> case y of A -> B; B -> A
+            --
+            -- And now later on we have:
+            --   x |-> B; y |-> A
+            --
+            -- We don't want to blindly just match x against x and call it a day, ignoring y. Instead, we recursively ask for the
+            -- free variables of both RHSs to match exactly, which ensures that in the example we ask that (y == y) which fails
+            -- since y == A in the later term but is unbound in the earlier one.
+            --
+            -- Matching the free variables recursively also ensures that the final renaming will include entries for each of the
+            -- free variables of the certainly-matching RHS.
+            match_term certain_match rn2 e_l' e_r'
+              | certain_match = return [VarLR x x | x <- varSetElems (annedTermFreeVars e_l' `unionVarSet` annedTermFreeVars e_r')]
+              | otherwise     = matchTerm rn2 e_l' e_r'
+            go_template mb_extra_xys mextras lhs_var_doesnt_need_rn heap_inst extra_free_eqs used_l' used_r' = do
+                -- Don't forget to match types/unfoldings of binders as well:
+                bndr_free_eqs <- mextras
+                extra_xys <- case mb_extra_xys of
+                  _ | lhs_var_doesnt_need_rn -> return []
+                  Just extra_xys             -> return extra_xys
+                  Nothing                    -> failLoop "cannot match VarR non-internally"
+                matchLoop (lr : known) heap_inst (extra_xys ++ xys) (bndr_free_eqs ++ extra_free_eqs ++ free_eqs) used_l' used_r'
+            failLoop rest = fail $ "matchLoop: " ++ showPpr lr ++ ": " ++ rest
+    
+    -- First Maybe: whether or not the var is bound in the heap
+    -- Second Maybe: whether or not the HeapBinding actually has a term
+    -- Third Maybe: whether it is safe for work duplication to make use of that term
+    lookupUsed :: VarSet -> Var -> PureHeap -> Maybe (HowBound, Either (Either Generalised Tag) (Maybe (VarSet, Out AnnedTerm)))
+    lookupUsed used x h = case M.lookup x h of
+      Nothing -> Nothing
+      Just hb -> Just (howBound hb, flip (either Left) (heapBindingMeaning hb) $ \in_e -> let e' = renameIn (renameAnnedTerm (rnInScopeSet rn2)) in_e
+                                                                                          in Right $ case () of () | termIsCheap e'      -> Just (used, e')
+                                                                                                                   | x `elemVarSet` used -> Nothing
+                                                                                                                   | otherwise           -> Just (used `extendVarSet` x, e'))
+    -- The key idea behind the "instantiation loop" is that to construct the heap that instantiates
+    -- the left hand side to obtain the right hand side, we have to copy some bindings from the right
+    -- into the instantiating heap. In particular, we must copy:
+    --  * Any binding for a variable which is unbound on the left
+    --  * Any binding which is referred to by any other copied binding
+    --
+    -- At the same time, we must avoid copying expensive bindings more than once (because of work duplication).
+    instLoop :: PureHeap  -- ^ Instantiation heap to extend
+             -> Var       -- ^ Binder for the term on the RHS (newly manufactured if coming from MatchR)
+             -> HowBound  -- ^ How the term on the RHS was bound
+             -> VarSet    -- ^ Things on the right that have already been used, BEFORE the copy
+             -> Either (Either Generalised Tag) (Maybe (VarSet, Out AnnedTerm)) -- ^ Meaning. Contains a nested Nothing if we cannot take another copy of the term for work duplication reasons
+             -> Match (PureHeap, VarSet) -- Returns final instantiation heap and things on the right that were used
+    instLoop h_inst x_r how_r used_r mb_er'
+      -- If we know the name of the thing on the RHS and it is already in the instantiating heap, we need do no work at all
+      | x_r `M.member` h_inst
+      = return (h_inst, used_r)
+      -- Otherwise we have to insert some bindings
+      | otherwise = do
+        (hb_meaning, used_r, fvs_r) <- case mb_er' of
+          Left mb_tg                   -> return (Left mb_tg,               used_r,  emptyVarSet)
+          Right (Just (used_r', e_r')) -> return (Right (renamedTerm e_r'), used_r', annedTermFreeVars e_r')
+          Right Nothing                -> fail $ "instLoop(" ++ showPpr x_r ++ "): right side already used in instance match"
+        
+        -- Transitively add the free variables of the copied bindings
+        fvsInstLoop (M.insert x_r (HB how_r hb_meaning) h_inst) used_r (fvs_r `unionVarSet` varBndrFreeVars x_r)
+
+    fvsInstLoop :: PureHeap -> VarSet -> FreeVars -> Match (PureHeap, VarSet)
+    fvsInstLoop h_inst used_r fvs
+      = foldM (\(h_inst, used_r) y_r -> case rnOccR_maybe rn2 y_r of
+                                          Just _ 
+                                            | y_r `elemVarSet` k_inst_bvs -> return (h_inst, used_r) -- In the instantiating stack: no heap copying required
+                                            | otherwise                   -> fail $ "fvsInstLoop(" ++ showPpr y_r ++ "): heap instance reference to non-instantiating stack"
+                                          Nothing -> case lookupUsed used_r y_r h_r of -- Bound by the heap: must copy something
+                                            Just (how_r, mb_er') -> instLoop h_inst y_r how_r used_r mb_er'
+                                            Nothing              -> fail $ "fvsInstLoop(" ++ showPpr y_r ++ "): right heap binding not present")
+              (h_inst, used_r) (varSetElems fvs)
+
+app3 :: [a] -> [a] -> [a] -> [a]
+app3 x y z = x ++ y ++ z

compiler/supercompile/Supercompile/Drive/Process1.hs

+{-# LANGUAGE BangPatterns, RankNTypes, RebindableSyntax #-}
+{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
+module Supercompile.Drive.Process1 (supercompile) where
+
+#include "HsVersions.h"
+
+import Supercompile.Drive.Match
+import Supercompile.Drive.Split
+import Supercompile.Drive.Process
+
+import Supercompile.Core.FreeVars
+import Supercompile.Core.Renaming
+--import Supercompile.Core.Size
+import Supercompile.Core.Syntax
+import Supercompile.Core.Tag
+
+import Supercompile.Evaluator.Deeds
+import Supercompile.Evaluator.FreeVars
+import Supercompile.Evaluator.Residualise
+import Supercompile.Evaluator.Syntax
+
+import Supercompile.Termination.Combinators
+--import Supercompile.Termination.Extras
+--import Supercompile.Termination.TagSet
+--import Supercompile.Termination.TagGraph
+import Supercompile.Termination.Generaliser
+
+import Supercompile.StaticFlags
+import Supercompile.Utilities hiding (Monad(..))
+
+import Id         (mkLocalId)
+import Name       (Name, mkSystemVarName)
+import FastString (mkFastString)
+import qualified State as State
+import State hiding (State, mapAccumLM)
+
+import Text.XHtml hiding (text)
+
+import qualified Control.Monad as Monad
+import Control.Exception (handleJust, AsyncException(UserInterrupt))
+import qualified Data.Foldable as Foldable
+import qualified Data.Traversable as Traversable
+import qualified Data.Map as M
+import Data.Monoid (Monoid(mappend, mempty))
+import Data.Ord
+import qualified Data.Set as S
+
+import Prelude hiding (Monad(..))
+
+
+ifThenElse :: Bool -> a -> a -> a
+ifThenElse True  x _ = x
+ifThenElse False _ y = y
+
+
+supercompile :: M.Map Var Term -> Term -> IO (SCStats, Term)
+supercompile unfoldings e = liftM (second (fVedTermToTerm . bindManyMixedLiftedness fvedTermFreeVars to_bind)) $ runScpM $ fmap snd $ sc (mkLinearHistory (cofmap fst wQO)) S.empty state
+  where (_, (to_bind, _preinit_with, state), _) = prepareTerm unfoldings e
+
+--
+-- == The drive loop ==
+--
+
+data Promise = P {
+    fun        :: Var,      -- Name assigned in output program
+    abstracted :: [AbsVar], -- Abstracted over these variables
+    meaning    :: State,    -- Minimum adequate term
+    embedded   :: Maybe SDoc
+  }
+
+instance MonadStatics ScpBM where
+    bindCapturedFloats = bindFloats
+    monitorFVs mx = ScpM $ \e s k -> unScpM mx e s (\x s' -> let (Right fss_delta, _fss_common) = splitByReverse (pTreeHole s) (pTreeHole s')
+                                                             in k (unionVarSets [fvedTermFreeVars e' | (_, e') <- concatMap fulfilmentTreeFulfilments fss_delta], x) s')
+
+-- Note [Floating h-functions past the let-bound variables to which they refer]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+--
+-- This seems like a reasonable thing to do because some variables will become free after supercompilation.
+-- However, there really isn't much point doing the float because I won't be able to tie back to the floated thing
+-- in any other branch.
+--
+-- Indeed, allowing such tiebacks may be a source of bugs! Consider a term like:
+--
+--  x |-> <10>
+--  x + 5
+--
+-- After supercompilation, we will have:
+--
+--  15
+--
+-- Since we check the *post supercompilation* free variables here, that h function could be floated
+-- upwards, so it is visible to later supercompilations. But what if our context had looked like:
+--
+--   (let x = 10 in x + 5, let x = 11 in x + 5)
+--
+-- Since we only match phantoms by name, we are now in danger of tying back to this h-function when we
+-- supercompile the second component of the pair!
+--
+-- Conclusion: don't bother with this rubbish.
+--
+-- Note [Variables reachable from let-bindings]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+--
+-- TODO: we shouldn't lambda-abstract over any variables reachable via the let-bound thing. Doing so needlessly
+-- passes them around via lambdas when they will always be available in the closure.
+--
+-- Consider this example:
+--
+--   \y -> let x = \z -> .. too big to inline ... y ...
+---        in (... x ..., ... x ...)
+--
+-- When supercompliing each component of the pair we might feel tempted to generate h-functions lambda abstracted over
+-- y, but doing so is pointless (just hides information from GHC) since the result will be trapped under the x binding anyway.
+fulfilmentRefersTo :: FreeVars -> (Promise, FreeVars) -> Maybe (Out Var)
+fulfilmentRefersTo extra_statics (p, fulfilment_fvs)
+  = if Foldable.any (`elemVarSet` extra_statics) (fulfilment_fvs `unionVarSet` extra_fvs)
+     then Just (fun p)
+     else Nothing
+  where
+    -- We bind floats with phantoms bindings where those phantom bindings are bound.
+    --
+    -- For wrappers introduced by --refine-fvs, we still need to use (fvedTermFreeVars e') because that will include
+    -- the wrapped h-function (e.g. the h83' wrapper for h83). This also applies (though more rarely) for non-wrappers
+    -- because looking at the fvedTermFreeVars is the only way we can learn about what h-functions they require.
+    extra_fvs = stateLetBounders (meaning p)
+
+-- Used at the end of supercompilation to extract just those h functions that are actually referred to.
+-- More often than not, this will be *all* the h functions, but if we don't discard h functions on rollback
+-- then this is not necessarily the case!
+fulfilmentReferredTo :: FreeVars -> (Promise, FreeVars) -> Maybe FreeVars
+fulfilmentReferredTo fvs (p, fulfilment_fvs)
+  = if fun p `elemVarSet` fvs
+     then Just fulfilment_fvs
+     else Nothing
+
+-- We do need a fixed point here to identify the full set of h-functions to residualise.
+-- The reason is that even if a static variable is not free in an output h-function, we might
+-- have created (and make reference to) some h-function that *does* actually refer to one
+-- of the static variables.
+-- See also Note [Phantom variables and bindings introduced by scrutinisation]
+partitionFulfilments :: forall t a b. Traversable t
+                     => (a -> (Promise, FreeVars) -> Maybe b)              -- ^ Decide whether a fulfilment should be residualised given our current a, returning a new b if so
+                     -> ([b] -> a)                                         -- ^ Combine bs of those fufilments being residualised into a new a
+                     -> a                                                  -- ^ Used to decide whether the fufilments right here are suitable for residulising
+                     -> t (Promise, Fulfilment)                            -- ^ Fulfilments to partition
+                     -> ([(Promise, Fulfilment)], t (Promise, Fulfilment)) -- ^ Fulfilments that should be bound and those that should continue to float, respectively
+partitionFulfilments check combine = go
+  where
+    go :: a -> t (Promise, Fulfilment) -> ([(Promise, Fulfilment)], t (Promise, Fulfilment))
+    go x fs
+      -- | traceRender ("partitionFulfilments", x, map (fun . fst) fs) False = undefined
+      | null fs_now' = ([], fs)
+      | otherwise    = first (fs_now' ++) $ go (combine xs') fs'
+      where (fs', fs_now_xs') = runState (traverse one_captured fs) []
+            (fs_now', xs') = unzip fs_now_xs'
+
+            one_captured :: (Promise, Fulfilment) -> State.State [((Promise, Fulfilment), b)] (Promise, Fulfilment)
+            one_captured (p, f)
+              | Fulfilled e <- f
+              , Just y <- check x (p, fvedTermFreeVars e)
+              = modify (((p, f), y):) Monad.>> pure (p, Captured)
+              | otherwise
+              = pure (p, f)
+            
+-- Note [Where to residualise fulfilments with FVs]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+--
+-- Be careful of this subtle problem:
+--
+--  let h6 = D[e1]
+--      residual = ...
+--      h7 = D[... let residual = ...
+--                 in Just residual]
+--  in ...
+--
+-- If we first drive e1 and create a fulfilment for the h6 promise, then when driving h7 we will eventually come across a residual binding for the
+-- "residual" variable. If we aren't careful, we will notice that "residual" is a FV of the h6 fulfilment and residualise it deep within h7. But
+-- what if the body of the outermost let drove to something referring to h6? We have a FV - disaster!
+--
+-- The right thing to do is to make sure that fulfilments created in different "branches" of the process tree aren't eligible for early binding in
+-- that manner, but we still want to tie back to them if possible. The bindFloats function achieves this by carefully shuffling information between the
+-- fulfilments and promises parts of the monadic-carried state.
+bindFloats :: FreeVars -> ScpBM a -> ScpBM ([(Var, FVedTerm)], a)
+bindFloats extra_statics mx
+  = ScpM $ \e s k -> unScpM mx (e { pTreeContext = BindCapturedFloats extra_statics (pTreeHole s) : pTreeContext e })
+                               (s { pTreeHole = [] }) (kontinue s k)
+  where
+    kontinue s k x s' = -- traceRender ("bindFloats", [(fun p, fvedTermFreeVars e) | (p, e) <- fs_now], [(fun p, fvedTermFreeVars e) | (p, e) <- fs_later]) $
+                        k (fulfilmentsToBinds fs_now, x) (s' { pTreeHole = unComp fs_later ++ pTreeHole s })
+      where (fs_now, fs_later) = partitionFulfilments fulfilmentRefersTo mkVarSet extra_statics (Comp (pTreeHole s'))
+
+fulfilmentsToBinds :: [(Promise, Fulfilment)] -> Out [(Var, FVedTerm)]
+fulfilmentsToBinds fs = sortBy (comparing ((read :: String -> Int) . dropLastWhile (== '\'') . drop 1 . varString . fst)) [(fun p, e') | (p, Fulfilled e') <- fs]
+
+freshHName :: ScpM f f Name
+freshHName = ScpM $ \_e s k -> k (expectHead "freshHName" (names s)) (s { names = tail (names s) })
+
+
+getPromises :: ScpM () () [Promise]
+getPromises = ScpM $ \e s k -> k (pTreeContextPromises (pTreeContext e)) s
+
+getPromiseNames :: ScpM FulfilmentTree FulfilmentTree [Var]
+getPromiseNames = ScpM $ \e s k -> k (map (fun . fst) (fulfilmentTreeFulfilments (pTreeHole s)) ++ map fun (pTreeContextPromises (pTreeContext e))) s
+
+promise :: Promise -> ScpBM (a, Out FVedTerm) -> ScpPM (a, Out FVedTerm)
+promise p opt = ScpM $ \e s k -> {- traceRender ("promise", fun p, abstracted p) $ -} unScpM (mx p) (e { pTreeContext = Promise p : pTreeContext e, depth = 1 + depth e }) (s { pTreeHole = [] }) k
+  where
+    mx p = do
+      (a, optimised_e) <- opt
+      -- We have a little trick here: we can reduce the number of free variables our "h" functions abstract over if we discover that after supercompilation some
+      -- variables become dead. This lets us get some of the good stuff from absence analysis: we can actually reduce the number of loop-carried vars like this.
+      -- It is particularly important to do this trick when we have unfoldings, because functions get a ton more free variables in that case.
+      --
+      -- If some of the fufilments we have already generated refer to us, we need to fix them up because their application sites will apply more arguments than we
+      -- actually need. We aren't able to do anything about the stuff they spuriously allocate as a result, but we can make generate a little wrapper that just discards
+      -- those arguments. With luck, GHC will inline it and good things will happen.
+      --
+      -- We have to be careful when generating the wrapper: the *type variables* of the optimised_fvs must also be abstracted over!
+      --
+      -- TODO: we can generate the wrappers in a smarter way now that we can always see all possible fulfilments?
+      let optimised_fvs_incomplete = fvedTermFreeVars optimised_e
+          optimised_fvs = optimised_fvs_incomplete `unionVarSet` unionVarSets (map varBndrFreeVars (varSetElems optimised_fvs_incomplete))
+          abstracted'
+            | not rEFINE_FULFILMENT_FVS = abstracted p
+            | otherwise = [x { absVarDead = absVarDead x || not (absVarVar x `elemVarSet` optimised_fvs) }
+                          | x <- abstracted p]
+      pprTrace "promise" (ppr optimised_fvs $$ ppr optimised_e) $
+       ScpM $ \_e s k -> k () (s { pTreeHole = Split False [(p { abstracted = abstracted' },
+                               Fulfilled (absVarLambdas abstracted' optimised_e))] (pTreeHole s) })
+      
+      fmap (((mkVarSet (map absVarVar abstracted') `unionVarSet` stateLetBounders (meaning p) `unionVarSet` extraOutputFvs) `unionVarSet`) . mkVarSet) getPromiseNames >>=
+        \fvs -> ASSERT2(optimised_fvs `subVarSet` fvs, ppr (fun p, optimised_fvs `minusVarSet` fvs, fvs, optimised_e)) return ()
+      
+      return (a, applyAbsVars (fun p) Nothing abstracted')
+
+-- No meaning, term: "legacy" term that can no longer be tied back to
+-- No meaning, no term: rolled back while still a promise
+-- Meaning, term: standard
+-- Meaning, no term: rolled back after being fulfilled for some other reason
+type FulfilmentTree = PTree (Promise, Fulfilment)
+
+data Fulfilment = Captured                           -- ^ Already residualised because captured by a BV or similar
+                | RolledBack (Maybe (Out FVedTerm))  -- ^ Rolled back so will never be residualised, but we might know what it is anyway (FIXME: always Nothing)
+                | Fulfilled (Out FVedTerm)           -- ^ Not yet residualised: floated, eligible for further tiebacks
+
+data PTree a = Tieback Var              -- ^ Didn't promise or drive extra stuff: just tied back
+             | Split Bool [a] [PTree a] -- ^ Made a promise, fulfiling it like so (with 1 or 2 fulfilments..)
+                                        --   and where the children are these
+             | BoundCapturedFloats FreeVars [PTree a]
+                                        -- ^ Produced these children within the context of these BVs
+
+instance Functor PTree where fmap = Traversable.fmapDefault
+instance Foldable PTree where foldMap = Traversable.foldMapDefault
+
+instance Traversable PTree where
+    traverse _ (Tieback n)  = pure (Tieback n)
+    traverse f (Split rb x ts) = Split rb <$> traverse f x <*> traverse (traverse f) ts
+    traverse f (BoundCapturedFloats bvs ts) = BoundCapturedFloats bvs <$> traverse (traverse f) ts
+
+-- Fulfilments at each level and the free variables of bindCapturedFloats that caused them to pushed.
+-- We guarantee that promises for each these are already present in the promises field.
+--
+-- I have to store these in the monad-carried information because catchScpM has to be able to restore
+-- (a subset of) them when rollback is initiated. See also Note [Where to residualise fulfilments with FVs]
+--
+-- I have to store them in their full-blown tree format (rather than just a flat list of Fulfilment at each
+-- level) for nice pretty-printed logging.
+data PTreeContextItem = Promise Promise
+                      | BindCapturedFloats FreeVars [FulfilmentTree]
+type PTreeContext = [PTreeContextItem]
+
+data ScpEnv = ScpEnv {
+    pTreeContext :: PTreeContext, -- Zipper into the process tree "above" us
+    depth        :: Int
+  }
+
+data ScpState f = ScpState {
+    names     :: [Name],
+    pTreeHole :: f, -- Work-in-progress on "this level" of the process tree
+    stats     :: SCStats
+  }
+
+pTreeContextPromises :: PTreeContext -> [Promise]
+pTreeContextPromises = foldMap $ \tci -> case tci of
+    Promise p                -> [p]
+    BindCapturedFloats _ fts -> map fst (concatMap fulfilmentTreeFulfilments fts)
+
+-- Only returns those fulfilments that are still floating and eligible for tieback
+fulfilmentTreeFulfilments :: FulfilmentTree -> [(Promise, Out FVedTerm)]
+fulfilmentTreeFulfilments t = [(p, e') | (p, Fulfilled e') <- Foldable.toList t]
+
+class IMonad m where
+    return :: a -> m s s a
+    (>>=) :: m s0 s1 a -> (a -> m s1 s2 b) -> m s0 s2 b
+    (>>) :: m s0 s1 a -> m s1 s2 b -> m s0 s2 b
+    fail :: String -> m s0 s1 a
+
+    mx >> my = mx >>= \_ -> my
+    fail = error
+
+-- The IO monad is used to catch Ctrl+C for pretty-printing purposes
+newtype ScpM f f' a = ScpM { unScpM :: ScpEnv -> ScpState f -> (a -> ScpState f' -> IO (SCStats, Out FVedTerm)) -> IO (SCStats, Out FVedTerm) }
+
+type ScpPM = ScpM ()                FulfilmentTree
+type ScpBM = ScpM [FulfilmentTree] [FulfilmentTree]
+
+instance Functor (ScpM f f') where
+    fmap f x = x >>= (return . f)
+
+instance Monad.Monad (ScpM f f) where
+    return = return
+    (>>=) = (>>=)
+
+instance IMonad ScpM where
+    return x = ScpM $ \_e s k -> k x s
+    (!mx) >>= fxmy = ScpM $ \e s k -> unScpM mx e s (\x s -> unScpM (fxmy x) e s k)
+
+class Printable f where
+    handlePrint :: ScpM f f' a -> ScpM f f' a
+
+instance Printable FulfilmentTree where
+    handlePrint = handlePrint' pprScpPM
+
+instance Printable [FulfilmentTree] where
+    handlePrint = handlePrint' pprScpBM
+
+instance Printable () where
+    handlePrint = id
+
+handlePrint' :: ScpM f f String -> ScpM f f' a -> ScpM f f' a
+handlePrint' prnt act = ScpM $ \e s k -> handleJust (\e -> case e of UserInterrupt -> Just (); _ -> Nothing) (\() -> unScpM prnt e s (\res _ -> writeFile "sc.htm" res Monad.>> error "Ctrl+C-ed")) (unScpM act e s k)
+
+runScpM :: ScpPM (Out FVedTerm) -> IO (SCStats, Out FVedTerm)
+runScpM me = unScpM (tracePprScpPM me) init_e init_s (\e' s -> Monad.return (stats s, bindManyMixedLiftedness fvedTermFreeVars (fulfilmentsToBinds $ fst $ partitionFulfilments fulfilmentReferredTo unionVarSets (fvedTermFreeVars e') (pTreeHole s)) e'))
+  where
+    init_e = ScpEnv { pTreeContext = [], depth = 0 }
+    init_s = ScpState { names = h_names, pTreeHole = (), stats = mempty }
+    
+    -- We need to create a name supply with *pairs* of Names because if we refine the fulfilment FVs we will create two bindings for each h-function
+    h_names = zipWith (\i uniq -> mkSystemVarName uniq (mkFastString ('h' : show (i :: Int))))
+                      [1..] (uniqsFromSupply hFunctionsUniqSupply)
+
+catchScpM :: ((forall b. c -> ScpBM b) -> ScpBM a) -- ^ Action to try: supplies a function than can be called to "raise an exception". Raising an exception restores the original ScpEnv and ScpState
+          -> (c -> ScpBM a)                        -- ^ Handler deferred to if an exception is raised
+          -> ScpBM a                               -- ^ Result from either the main action or the handler
+catchScpM f_try f_abort = ScpM $ \e s k -> unScpM (f_try (\c -> ScpM $ \e' s' _k' ->
+    unScpM (f_abort c) e (if False -- dISCARD_FULFILMENTS_ON_ROLLBACK
+                          then s
+                          else let (Right fss_candidates, _fss_common) = splitByReverse (pTreeContext e) (pTreeContext e')
+                                   
+                                   -- Since we are rolling back we need to float as many of the fulfilments created in between here and the rollback point
+                                   -- upwards. This means that we don't lose the work that we already did to supercompile those bindings.
+                                   --
+                                   -- The approach is to accumulate a set of floating fulfilments that I try to move past each statics set one at a time,
+                                   -- from inside (deeper in the tree) to the outside (closer to top level).
+                                   go :: (VarSet, [FulfilmentTree]) -> PTreeContextItem -> (VarSet, [FulfilmentTree])
+                                   go (partial_not_completed, fs_floating) (Promise p) = (partial_not_completed `extendVarSet` fun p, [Split True [(p, RolledBack Nothing)] fs_floating])
+                                   go (partial_not_completed, fs_floating) (BindCapturedFloats extra_statics fs_pre_bind) = (partial_not_completed, fs_pre_bind ++ [BoundCapturedFloats extra_statics (unComp fs_ok)])
+                                      where (_fs_discard, fs_ok) = partitionFulfilments fulfilmentRefersTo mkVarSet (not_completed `unionVarSet` extra_statics) (Comp fs_floating)
+
+                                   (not_completed, fs_floating) = foldl' go (emptyVarSet, []) fss_candidates
+                               in s' { pTreeHole = fs_floating ++ pTreeHole s })
+                         k)) e s k
+
+addStats :: SCStats -> ScpM f f ()
+addStats scstats = ScpM $ \_e s k -> k () (let scstats' = stats s `mappend` scstats in scstats' `seqSCStats` s { stats = scstats' })
+
+recordStopped :: State -> ScpBM a -> ScpBM a
+recordStopped state mx = ScpM $ \e s k -> unScpM mx (e { pTreeContext = case pTreeContext e of (Promise p:rest) -> Promise p { embedded = Just (pPrintFullState quietStatePrettiness state) }:rest }) s k
+
+
+type PrettyTree = PTree (Var, SDoc, Maybe SDoc, Maybe SDoc)
+
+tracePprScpPM :: ScpPM a -> ScpPM a
+tracePprScpPM = id
+{-
+tracePprScpPM mx = do
+  x <- mx
+  s <- pprScpPM
+  unsafePerformIO (writeFile "sc.htm" s Monad.>> Monad.return (return x))
+  -- pprTraceSC "tracePprScpM" (text s) $ return x
+-}
+
+pprScpBM :: ScpBM String
+pprScpPM :: ScpM FulfilmentTree FulfilmentTree String
+(pprScpBM, pprScpPM) = (go (map unwindTree), go (\t -> [unwindTree t]))
+  where
+    go :: forall f. (f -> [PrettyTree]) -> ScpM f f String
+    go xtract = ScpM $ \e s k -> k (html (pTreeContext e) (xtract (pTreeHole s))) s
+
+    html ctxt hole = show $ thehtml $ toHtmlFromList
+      [header (toHtmlFromList [thetitle (stringToHtml "Supercompilation"),
+                               script mempty ! [thetype "text/javascript", src "http://www.omega-prime.co.uk/files/chsc/jquery-1.6.3.min.js"],
+                               script mempty ! [thetype "text/javascript", src "http://www.omega-prime.co.uk/files/chsc/jstree_pre1.0_fix_1/jquery.jstree.js"],
+                               script js]),
+       body (toHtmlFromList [thediv htm ! [identifier "tree"],
+                             pre mempty ! [identifier "content-in"],
+                             pre mempty ! [identifier "content-embed"],
+                             pre mempty ! [identifier "content-out"]])]
+      where htm = pprTrees (unwindContext ctxt hole)
+            -- NB: must use primHtml so that entities in the script are not escaped
+            js = primHtml "$(function () { $(\"#tree\").jstree({ \"plugins\" : [\"themes\", \"html_data\"], \"core\" : { \"animation\" : 0 } }).bind(\"loaded.jstree\", function (event, data) { data.inst.open_all(-1, false); }); });"
+
+    unwindTree :: FulfilmentTree -> PrettyTree
+    unwindTree = fmap unwindPromiseFulfilment
+
+    unwindPromiseFulfilment (p, f) = (fun p, pPrintFullState quietStatePrettiness (meaning p), embedded p,
+                                      case f of Captured         -> Nothing
+                                                RolledBack mb_e' -> fmap ppr mb_e'
+                                                Fulfilled e'     -> Just (ppr e'))
+
+    unwindContext :: PTreeContext -> [PrettyTree] -> [PrettyTree]
+    unwindContext = flip $ foldl (flip unwindContextItem)
+
+    unwindContextItem :: PTreeContextItem -> [PrettyTree] -> [PrettyTree]
+    unwindContextItem (Promise p)                  ts = [Split False [(fun p, pPrintFullState quietStatePrettiness (meaning p), embedded p, Nothing)] ts]
+     -- NB: don't put (Split True) here because otherwise it looks like everything on the way back to the root has been rolled back, when it fact it is only "in progress"
+    unwindContextItem (BindCapturedFloats fvs ts') ts = map unwindTree ts' ++ [BoundCapturedFloats fvs ts]
+
+    pprTrees :: [PrettyTree] -> Html
+    pprTrees ts = ulist $ toHtmlFromList $ map pprTree ts
+
+    pprTree :: PrettyTree -> Html
+    pprTree t = li $ case t of
+      Tieback x                  -> anchor (stringToHtml ("Tieback " ++ show x)) ! [href ("#" ++ show x)]
+      Split rb fs ts             -> toHtmlFromList ([thediv (anchor (stringToHtml (show x ++ (if isJust mb_emb_code then " (sc-stop)" else "") ++ if rb then " (rolled back)" else "")) !
+                                                                [strAttr "onclick" $ "document.getElementById(\"content-in\").innerText=" ++ show (showSDoc in_code) ++
+                                                                                    ";document.getElementById(\"content-out\").innerText=" ++ show (maybe "" showSDoc mb_out_code) ++
+                                                                                    ";document.getElementById(\"content-embed\").innerText=" ++ show (maybe "" showSDoc mb_emb_code) ++
+                                                                                    ";return false"]) !
+                                                            [identifier (show x)]
+                                                    | (x, in_code, mb_emb_code, mb_out_code) <- fs] ++ [pprTrees ts])
+      BoundCapturedFloats fvs ts -> toHtmlFromList [stringToHtml ("Capture " ++ showSDoc (ppr fvs)), pprTrees ts]
+
+
+type RollbackScpM = Generaliser -> ScpBM (Deeds, Out FVedTerm)
+type ProcessHistory = LinearHistory (State, RollbackScpM)
+
+liftPB :: ScpPM a -> ScpBM a
+liftPB act = ScpM $ \e s k -> unScpM act e (s { pTreeHole = () }) (\x s' -> k x (s' { pTreeHole = pTreeHole s' : pTreeHole s }))
+
+sc  :: ProcessHistory -> AlreadySpeculated -> State -> ScpPM (Deeds, Out FVedTerm)
+sc' :: ProcessHistory -> AlreadySpeculated -> State -> ScpBM (Deeds, Out FVedTerm)
+sc  hist = rollbackBig (memo (sc' hist))
+sc' hist speculated state = handlePrint $ (\raise -> check raise) `catchScpM` \gen -> stop gen state hist -- TODO: I want to use the original history here, but I think doing so leads to non-term as it contains rollbacks from "below us" (try DigitsOfE2)
+  where
+    check this_rb = case terminate hist (state, this_rb) of
+                      Continue hist' -> continue hist'
+                      Stop (shallower_state, rb) -> recordStopped shallower_state $ maybe (stop gen state hist) ($ gen) $ guard sC_ROLLBACK Monad.>> Just rb
+                        where gen = mK_GENERALISER shallower_state state
+    stop gen state hist = do addStats $ mempty { stat_sc_stops = 1 }
+                             liftM (\(_, deeds, e') -> (deeds, e')) $ maybe (trace "sc-stop: no generalisation" $ split state) (trace "sc-stop: generalisation") (generalise gen state) (liftPB . sc hist speculated) -- Keep the trace exactly here or it gets floated out by GHC
+    continue hist = do traceRenderScpM "reduce end (continue)" (PrettyDoc (pPrintFullState quietStatePrettiness state'))
+                       addStats stats
+                       liftM (\(_, deeds, e') -> (deeds, e')) $ split state' (liftPB . sc hist speculated')
+      where (speculated', (stats, state')) = speculate speculated $ reduceWithStats state -- TODO: experiment with doing admissability-generalisation on reduced terms. My suspicion is that it won't help, though (such terms are already stuck or non-stuck but loopy: throwing stuff away does not necessarily remove loopiness).
+
+memo :: (AlreadySpeculated -> State -> ScpBM (Deeds, Out FVedTerm))
+     ->  AlreadySpeculated -> State -> ScpPM (Deeds, Out FVedTerm)
+memo opt speculated state0 = do
+    let state1 = gc state0 -- Necessary because normalisation might have made some stuff dead
+    
+    ps <- getPromises
+    case [ (p, (releaseStateDeed state0, applyAbsVars (fun p) (Just (mkRenaming rn_lr)) (abstracted p)))
+         | p <- ps
+         , Just rn_lr <- [(\res -> if isNothing res then pprTraceSC "no match:" (ppr (fun p)) res else res) $
+                           match (meaning p) state1]
+          -- NB: because I can trim reduce the set of things abstracted over above, it's OK if the renaming derived from the meanings renames vars that aren't in the abstracted list, but NOT vice-versa
+         -- , let bad_renames = S.fromList (abstracted p) S.\\ M.keysSet (unRenaming rn_lr) in ASSERT2(S.null bad_renames, text "Renaming was inexhaustive:" <+> pPrint bad_renames $$ pPrint (fun p) $$ pPrintFullState (unI (meaning p)) $$ pPrint rn_lr $$ pPrintFullState state3) True
+          -- ("tieback: FVs for " ++ showSDoc (pPrint (fun p) $$ text "Us:" $$ pPrint state3 $$ text "Them:" $$ pPrint (meaning p)))
+         ] of
+      (p, res):_ -> {- traceRender ("tieback", pPrintFullState state3, fst res) $ -} do
+        traceRenderScpM "=sc" (fun p, PrettyDoc (pPrintFullState fullStatePrettiness state1), res)
+        ScpM $ \_ s k -> k res (s { pTreeHole = Tieback (fun p) })
+      [] -> {- traceRender ("new drive", pPrintFullState state3) $ -} do
+        let (vs_list, h_ty) = stateAbsVars Nothing state1
+
+        -- NB: promises are lexically scoped because they may refer to FVs
+        x <- freshHName
+        promise (P { fun = mkLocalId x h_ty, abstracted = vs_list, meaning = state1, embedded = Nothing }) $
+          do
+            traceRenderScpM ">sc" (x, PrettyDoc (pPrintFullState fullStatePrettiness state1))
+            -- FIXME: this is the site of the Dreadful Hack that makes it safe to match on reduced terms yet *drive* unreduced ones
+            -- I only add non-internally bound junk to the input heap because:
+            --  a) Thats the only stuff I *need* to add to make sure the FVs etc match up properly
+            --  b) New InternallyBound stuff might be created by reduction and then swiftly become dead, and I don't want to push that down
+            --     gratutiously. Furthermore, the Ids for that stuff might clash with those still-to-be-allocated in the state0 IdSupply.
+            --
+            -- Note that since the reducer only looks into non-internal *value* bindings doing this does not cause work duplication, only value duplication
+            --
+            -- FIXME: I'm not acquiring deeds for these....
+            res <- opt speculated state1
+            traceRenderScpM "<sc" (x, PrettyDoc (pPrintFullState quietStatePrettiness state1), res)
+            return res
+
+-- Several design choices here:
+--
+--  1. How to account for size of specialisations created during drive? Presumably ones that eventually get shared should be given a discount, but how?
+--
+--  2. How to continue if we do roll back. Currently I throw away any specialisations created in the process, but this seems uncool.
+rollbackBig :: (AlreadySpeculated -> State -> ScpM f f' (Deeds, Out FVedTerm))
+            ->  AlreadySpeculated -> State -> ScpM f f' (Deeds, Out FVedTerm)
+rollbackBig opt speculated state
+  -- | rOLLBACK_BIG = ScpM $ \e s k -> unScpM (opt speculated state) e s $ \(deeds', term') s' -> let too_big = fvedTermSize term' + sum [fvedTermSize term' | (p, term') <- pTreeHoles s', not (fun p `elem` map (fun . fst) (pTreeHoles s))] > bLOAT_FACTOR * stateSize state
+  --                                                                                              in if too_big then k (case residualiseState state of (deeds, _, e') -> (deeds, e')) s else k (deeds', term') s'
+  | otherwise = opt speculated state
+
+traceRenderScpM :: Outputable a => String -> a -> ScpM f f ()
+traceRenderScpM msg x = ScpM (\e s k -> k (depth e) s) >>= \depth -> pprTraceSC msg (nest depth $ pPrint x) $ return ()