fix(library/compiler/erase_irrelevant): make sure io monad actions are not erased by dead code elimination optimization

src/library/compiler/erase_irrelevant.cpp

@@ -325,18 +325,16 @@ class erase_irrelevant_fn : public compiler_step_visitor {
               So, in this version, we have a simpler (monad.bind v b)
 
                bind v b :=
-               fun s, let a := v unit in
+               fun s, let a := v s in
                       b a a
 
-              We use (b a a) instead of (b a unit) to make sure the let-declaration
-              is not erased by the elim_unused_lets step. This is ok because
-              the second argument is not used during runtime.
-
-              We use a let-expression to make sure that `v unit` is not erased.
+              We use (b a a) instead of (b a unit), and (v s) instead of (v unit)
+              to make sure the let-declaration is not erased by the elim_unused_lets step.
+              For (b a a), this hack is ok because the second argument is not used during runtime.
             */
             expr v    = visit(args[4]);
             expr u    = mk_neutral_expr();
-            expr vu   = mk_app(v, u);
+            expr vu   = mk_app(v, mk_var(0));
             expr b    = visit(args[5]);
             expr bau  = beta_reduce(mk_app(b, mk_var(0), mk_var(0)));
             expr let  = mk_let("a", u, vu, bau);

tests/lean/io_bug1.lean

@@ -0,0 +1,22 @@
+import system.io
+
+def bar : io unit :=
+do put_str "one", put_str "two", put_str "three"
+
+vm_eval bar
+
+print "---------"
+
+def foo : ℕ → io unit
+| 0     := put_str "at zero\n"
+| (n+1) := do put_str "in\n", foo n, put_str "out\n"
+
+vm_eval foo 3
+
+print "---------"
+
+def foo2 : ℕ → io unit
+| 0     := put_str "at zero\n"
+| (n+1) := do put_str "in\n", foo2 n, put_str "out\n", put_str "out2\n"
+
+vm_eval foo2 3

tests/lean/io_bug1.lean.expected.out

@@ -0,0 +1,22 @@
+onetwothree
+---------
+in
+in
+in
+at zero
+out
+out
+out
+
+---------
+in
+in
+in
+at zero
+out
+out2
+out
+out2
+out
+out2
+