+
+%************************************************************************
+
+ Static Argument Transformation Monad
+
+%************************************************************************
+
+To do the transformation, the game plan is to:
+
+1. Create a small nonrecursive RHS that takes the
+ original arguments to the function but discards
+ the ones that are static and makes a call to the
+ SATed version with the remainder. We intend that
+ this will be inlined later, removing the overhead
+
+2. Bind this nonrecursive RHS over the original body
+ WITH THE SAME UNIQUE as the original body so that
+ any recursive calls to the original now go via
+ the small wrapper
+
+3. Rebind the original function to a new one which contains
+ our SATed function and just makes a call to it:
+ we call the thing making this call the local body
+
+Example: transform this
+
+ map :: forall a b. (a->b) -> [a] -> [b]
+ map = /\ab. \(f:a->b) (as:[a]) -> body[map]
+to
+ map :: forall a b. (a->b) -> [a] -> [b]
+ map = /\ab. \(f:a->b) (as:[a]) ->
+ letrec map' :: [a] -> [b]
+ -- The "worker function
+ map' = \(as:[a]) ->
+ let map :: forall a' b'. (a -> b) -> [a] -> [b]
+ -- The "shadow function
+ map = /\a'b'. \(f':(a->b) (as:[a]).
+ map' as
+ in body[map]
+ in map' as
+
+Note [Shadow binding]
+~~~~~~~~~~~~~~~~~~~~~
+The calls to the inner map inside body[map] should get inlined
+by the local re-binding of 'map'. We call this the "shadow binding".
+
+But we can't use the original binder 'map' unchanged, because
+it might be exported, in which case the shadow binding won't be
+discarded as dead code after it is inlined.
+
+So we use a hack: we make a new SysLocal binder with the *same* unique
+as binder. (Another alternative would be to reset the export flag.)
+
+Note [Binder type capture]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Notice that in the inner map (the "shadow function"), the static arguments
+are discarded -- it's as if they were underscores. Instead, mentions
+of these arguments (notably in the types of dynamic arguments) are bound
+by the *outer* lambdas of the main function. So we must make up fresh
+names for the static arguments so that they do not capture variables
+mentioned in the types of dynamic args.
+
+In the map example, the shadow function must clone the static type
+argument a,b, giving a',b', to ensure that in the \(as:[a]), the 'a'
+is bound by the outer forall. We clone f' too for consistency, but
+that doesn't matter either way because static Id arguments aren't
+mentioned in the shadow binding at all.
+
+If we don't we get something like this:
+
+[Exported]
+[Arity 3]
+GHC.Base.until =
+ \ (@ a_aiK)
+ (p_a6T :: a_aiK -> GHC.Bool.Bool)
+ (f_a6V :: a_aiK -> a_aiK)
+ (x_a6X :: a_aiK) ->
+ letrec {
+ sat_worker_s1aU :: a_aiK -> a_aiK
+ []
+ sat_worker_s1aU =
+ \ (x_a6X :: a_aiK) ->
+ let {
+ sat_shadow_r17 :: forall a_a3O.
+ (a_a3O -> GHC.Bool.Bool) -> (a_a3O -> a_a3O) -> a_a3O -> a_a3O
+ []
+ sat_shadow_r17 =
+ \ (@ a_aiK)
+ (p_a6T :: a_aiK -> GHC.Bool.Bool)
+ (f_a6V :: a_aiK -> a_aiK)
+ (x_a6X :: a_aiK) ->
+ sat_worker_s1aU x_a6X } in
+ case p_a6T x_a6X of wild_X3y [ALWAYS Dead Nothing] {
+ GHC.Bool.False -> GHC.Base.until @ a_aiK p_a6T f_a6V (f_a6V x_a6X);
+ GHC.Bool.True -> x_a6X
+ }; } in
+ sat_worker_s1aU x_a6X
+
+Where sat_shadow has captured the type variables of x_a6X etc as it has a a_aiK
+type argument. This is bad because it means the application sat_worker_s1aU x_a6X
+is not well typed.
+