Correctly refresh the SAT inner worker

This is a little over-eager, but it's good enough

Cherry-picked from #265 in order to fix #264

Author: SquidDev

src/Core/Optimise/SAT.hs

@@ -60,7 +60,6 @@ import Data.Semigroup
 import Data.Maybe
 import Data.List
 
-
 -- | Do the static argument transformation on a whole program.
 staticArgsPass :: (MonadNamey m, IsVar a) => [Stmt a] -> m [Stmt a]
 staticArgsPass = traverse staticArg_stmt
@@ -174,13 +173,13 @@ doStaticArgs the_func the_type the_body =
     mkShadow worker =
       let go_dynamic args = do
             inside <- mkApps (Ref worker worker_ty) worker_ty args
-            pure $ foldr Lam inside args
+            refresh $ foldr Lam inside args
 
           go (Static (TypeArgument _ k):xs) = do
-            x <- fromVar . mkTyvar <$> genName
+            x <- fresh' TypeVar
             Lam (TypeArgument x k) <$> go xs
           go (Static (TermArgument _ k):xs) = do
-            x <- fromVar . mkVal <$> genName
+            x <- fresh' ValueVar
             Lam (TermArgument x k) <$> go xs
           go [] = go_dynamic non_static_bndrs
           go _ = error "NonStatic binder in static_binders"
@@ -229,11 +228,11 @@ isStatic _ _ = NonStatic
 mkApps :: forall a m. (IsVar a, MonadNamey m) => Atom -> Type -> [Argument a] -> m (Term a)
 mkApps at _ [] = pure $ Atom at
 mkApps at (ForallTy Irrelevant _ t) (TermArgument x tau:xs) = do
-  this_app <- fromVar . mkVal <$> genName
+  this_app <- fresh' ValueVar
   Let (One (this_app, t, App at (Ref (toVar x) tau))) <$>
     mkApps (Ref (toVar this_app) t) t xs
 mkApps at (ForallTy r _ t) (TypeArgument v _:xs) = do
-  this_app <- fromVar . mkVal <$> genName
+  this_app <- fresh' ValueVar
   let t' =
         case r of
           Relevant binder -> substituteInType (VarMap.singleton binder (VarTy (toVar v))) t

tests/lua/opt_sat_inline.lua

@@ -0,0 +1,10 @@
+do
+  local E = { __tag = "E" }
+  local function foldr_sat(zero, x)
+    if x.__tag ~= "T" then return zero end
+    local tmp = x[1]
+    local tmp0 = tmp._2._2
+    return foldr_sat(tmp._1 + foldr_sat(zero, tmp0._2), tmp0._1)
+  end
+  foldr_sat(0, E)
+end

tests/lua/opt_sat_inline.ml

@@ -0,0 +1,11 @@
+external val (+) : int -> int -> int = "function(x, y) return x + y end"
+
+type sz_tree 'a =
+  | E
+  | T of 'a * int * sz_tree 'a * sz_tree 'a
+
+let rec foldr f zero = function
+  | E -> zero
+  | T (x, _, l, r) -> foldr f (f x (foldr f zero r)) l
+
+let _ = foldr (+) 0 E