From 06ad52575a93a0c488bceffb5e6c39aa677bc36e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 8 Dec 2020 06:00:01 -0800
Subject: [PATCH] feat: force users to use `discard` when action result is not
 being bound and it is not `PUnit`

After this commit, we have to use an explicit `discard` in code such as
```
def g (x : Nat) : IO Nat := ...
def f (x : Nat) : IO Unit := do
  discard <| g x   -- type error without the `discard`
  IO.println x
```

Motivation: prevent users from making mistakes such as
```
def f (xs : Array Nat) : IO Unit := do
  xs.set! 0 1
  IO.println xs
```
when they meant to write
```
def f (xs : Array Nat) : IO Unit := do
  let xs := xs.set! 0 1
  IO.println xs
```
---
 src/Lean/Elab/Do.lean                     |  4 +--
 tests/compiler/t2.lean                    |  6 ++---
 tests/compiler/t4.lean                    |  2 +-
 tests/lean/PPRoundtrip.lean               |  2 +-
 tests/lean/PPRoundtrip.lean.expected.out  |  2 +-
 tests/lean/Process.lean                   |  8 +++---
 tests/lean/doIssue.lean                   | 23 +++++++++++++++++
 tests/lean/doIssue.lean.expected.out      | 30 +++++++++++++++++++++++
 tests/lean/pureCoeIssue.lean.expected.out |  4 +--
 tests/lean/ref1.lean                      |  4 +--
 tests/lean/run/deriv.lean                 |  2 +-
 tests/lean/run/doNotation1.lean           |  4 +--
 tests/lean/run/doNotation2.lean           |  6 ++---
 tests/lean/run/finally.lean               |  4 +--
 tests/lean/run/meta3.lean                 |  2 +-
 tests/lean/run/parsePrelude.lean          |  2 +-
 tests/lean/run/task_test_io.lean          |  2 +-
 17 files changed, 80 insertions(+), 27 deletions(-)
 create mode 100644 tests/lean/doIssue.lean
 create mode 100644 tests/lean/doIssue.lean.expected.out

diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index b0ce8f9de6..821432ae42 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -887,11 +887,11 @@ def seqToTermCore (action : Syntax) (k : Syntax) : MacroM Syntax := withFreshMac
     let cond := action[1]
     `(assert! $cond; $k)
   else
-    `(Bind.bind $action (fun _ => $k))
+    `(Bind.bind $action (fun (_ : PUnit) => $k))
 
 def seqToTerm (action : Syntax) (k : Syntax) : MacroM Syntax := do
   let r ← seqToTermCore action k
-  pure $ r.copyInfo action
+  return r.copyInfo action
 
 def declToTermCore (decl : Syntax) (k : Syntax) : M Syntax := withFreshMacroScope do
   let kind := decl.getKind
diff --git a/tests/compiler/t2.lean b/tests/compiler/t2.lean
index 5ed5fc4445..f2cb76c560 100644
--- a/tests/compiler/t2.lean
+++ b/tests/compiler/t2.lean
@@ -93,9 +93,9 @@ do
 end Expr
 
 def main (xs : List String) : IO UInt32 :=
-do let x := Expr.Var "x";
-   let f := Expr.pow x x;
-   Expr.nest Expr.deriv 7 f;
+do let x := Expr.Var "x"
+   let f := Expr.pow x x
+   discard <| Expr.nest Expr.deriv 7 f
    pure 0
 
 -- setOption profiler True
diff --git a/tests/compiler/t4.lean b/tests/compiler/t4.lean
index 7b9885a928..548dbfe996 100644
--- a/tests/compiler/t4.lean
+++ b/tests/compiler/t4.lean
@@ -110,7 +110,7 @@ def main (xs : List String) : IO UInt32 :=
 do let x := Expr.Var "x";
    let f := Expr.add x (Expr.mul x (Expr.mul x (Expr.add x x)));
    IO.println f;
-   Expr.nest Expr.deriv 3 f;
+   discard <| Expr.nest Expr.deriv 3 f;
    pure 0
 
 -- setOption profiler True
diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean
index 41ee5e69f9..711ff0f83e 100644
--- a/tests/lean/PPRoundtrip.lean
+++ b/tests/lean/PPRoundtrip.lean
@@ -94,6 +94,6 @@ set_option pp.structure_instance_type true in
 
 #eval checkM `(typeAs Nat (do
   let x ← pure 1
-  pure 2
+  discard <| pure 2
   let y := 3
   return x + y))
diff --git a/tests/lean/PPRoundtrip.lean.expected.out b/tests/lean/PPRoundtrip.lean.expected.out
index e06c5d0e7b..fb74e5547e 100644
--- a/tests/lean/PPRoundtrip.lean.expected.out
+++ b/tests/lean/PPRoundtrip.lean.expected.out
@@ -57,6 +57,6 @@ id
 typeAs Nat
   (do 
     let x ← pure 1
-    pure 2
+    discard (pure 2)
     let y : Nat := 3
     pure (x + y))
diff --git a/tests/lean/Process.lean b/tests/lean/Process.lean
index 07cdca30ce..6591d72261 100644
--- a/tests/lean/Process.lean
+++ b/tests/lean/Process.lean
@@ -1,4 +1,4 @@
-
+--
 open IO.Process
 
 def usingIO {α} (x : IO α) : IO α := x
@@ -13,19 +13,19 @@ def usingIO {α} (x : IO α) : IO α := x
 
 #eval usingIO do
   let child ← spawn { cmd := "sh", args := #["-c", "echo ho!"], stdout := Stdio.piped };
-  child.wait;
+  discard $ child.wait;
   child.stdout.readToEnd
 
 #eval usingIO do
   let child ← spawn { cmd := "head", args := #["-n1"], stdin := Stdio.piped, stdout := Stdio.piped };
   child.stdin.putStrLn "hu!";
   child.stdin.flush;
-  child.wait;
+  discard $ child.wait;
   child.stdout.readToEnd
 
 #eval usingIO do
   let child ← spawn { cmd := "true", stdin := Stdio.piped };
-  child.wait;
+  discard $ child.wait;
   child.stdin.putStrLn "ha!";
   child.stdin.flush <|> IO.println "flush of broken pipe failed"
 
diff --git a/tests/lean/doIssue.lean b/tests/lean/doIssue.lean
new file mode 100644
index 0000000000..52e1513688
--- /dev/null
+++ b/tests/lean/doIssue.lean
@@ -0,0 +1,23 @@
+def f (x : Nat) : IO Unit := do
+  x -- Error
+  IO.println x
+
+def f' (x : Nat) : IO Unit := do
+  discard x
+  IO.println x
+
+def g (xs : Array Nat) : IO Unit := do
+  xs.set! 0 1 -- Error
+  IO.println xs
+
+def g' (xs : Array Nat) : IO Unit := do
+  discard <| xs.set! 0 1 -- Error
+  IO.println xs
+
+def h (xs : Array Nat) : IO Unit := do
+  pure (xs.set! 0 1) -- Error
+  IO.println xs
+
+def h' (xs : Array Nat) : IO Unit := do
+  discard <| pure (xs.set! 0 1) -- Error
+  IO.println xs
diff --git a/tests/lean/doIssue.lean.expected.out b/tests/lean/doIssue.lean.expected.out
new file mode 100644
index 0000000000..938b920489
--- /dev/null
+++ b/tests/lean/doIssue.lean.expected.out
@@ -0,0 +1,30 @@
+doIssue.lean:2:2: error: application type mismatch
+  do 
+    pure x 
+    IO.println x
+argument
+  fun (x_1 : PUnit) => IO.println x
+has type
+  PUnit → IO Unit
+but is expected to have type
+  Nat → IO Unit
+doIssue.lean:10:2: error: application type mismatch
+  do 
+    pure (Array.set! xs 0 1)
+    IO.println xs
+argument
+  fun (x : PUnit) => IO.println xs
+has type
+  PUnit → IO Unit
+but is expected to have type
+  Array Nat → IO Unit
+doIssue.lean:18:2: error: application type mismatch
+  do 
+    pure (Array.set! xs 0 1)
+    IO.println xs
+argument
+  fun (x : PUnit) => IO.println xs
+has type
+  PUnit → IO Unit
+but is expected to have type
+  Array Nat → IO Unit
diff --git a/tests/lean/pureCoeIssue.lean.expected.out b/tests/lean/pureCoeIssue.lean.expected.out
index 0c53623b00..c832d04f70 100644
--- a/tests/lean/pureCoeIssue.lean.expected.out
+++ b/tests/lean/pureCoeIssue.lean.expected.out
@@ -5,7 +5,7 @@ argument
 has type
   Nat → IO Unit
 but is expected to have type
-  IO ?m
+  IO PUnit
 pureCoeIssue.lean:14:2: error: application type mismatch
   bind (f2 10)
 argument
@@ -13,4 +13,4 @@ argument
 has type
   Nat → IO Unit
 but is expected to have type
-  IO ?m
+  IO PUnit
diff --git a/tests/lean/ref1.lean b/tests/lean/ref1.lean
index 10035aced5..7e5718a5a2 100644
--- a/tests/lean/ref1.lean
+++ b/tests/lean/ref1.lean
@@ -1,4 +1,4 @@
-
+--
 def inc (r : IO.Ref Nat) : IO Unit := do
 let v ← r.get;
 r.set (v+1);
@@ -11,7 +11,7 @@ n.forM $ fun i => do
 def showArrayRef (r : IO.Ref (Array Nat)) : IO Unit := do
 let a ← r.swap ∅;
 a.size.forM (fun i => IO.println ("[" ++ toString i ++ "]: " ++ toString (a.get! i)));
-r.swap a;
+discard $ r.swap a;
 pure ()
 
 def tst (n : Nat) : IO Unit := do
diff --git a/tests/lean/run/deriv.lean b/tests/lean/run/deriv.lean
index 322960cf4e..ac9c2c6a3b 100644
--- a/tests/lean/run/deriv.lean
+++ b/tests/lean/run/deriv.lean
@@ -95,5 +95,5 @@ end Expr
 unsafe def main : IO Unit :=
 do let x := Expr.Var "x";
    let f := Expr.pow x x;
-   Expr.nest Expr.deriv 9 f;
+   discard $ Expr.nest Expr.deriv 9 f;
    pure ()
diff --git a/tests/lean/run/doNotation1.lean b/tests/lean/run/doNotation1.lean
index be0877b7e4..467d50c559 100644
--- a/tests/lean/run/doNotation1.lean
+++ b/tests/lean/run/doNotation1.lean
@@ -35,10 +35,10 @@ pure (a + 1)
 
 def h₃ (x : Nat) : StateT Nat IO Nat := do
 let m1 := do    -- Type inferred from application below
-  g x           -- liftM inserted here
+  discard <| g x           -- liftM inserted here
   IO.println 1
 let m2 (y : Nat) := do   -- Type inferred from application below
-  h (x+y)       -- liftM inserted here
+  discard <| h (x+y)       -- liftM inserted here
   myPrint y     -- liftM inserted here
 let a ← h 1        -- liftM inserted here
 IO.println x
diff --git a/tests/lean/run/doNotation2.lean b/tests/lean/run/doNotation2.lean
index 3892a6e87d..639c209b3e 100644
--- a/tests/lean/run/doNotation2.lean
+++ b/tests/lean/run/doNotation2.lean
@@ -4,11 +4,11 @@ let aux (y : Nat) (z : Nat) : IO Nat := do
   IO.println "aux started"
   IO.println s!"y: {y}, z: {z}"
   pure (x+y)
-aux x
+discard <| aux x
   (x + 1) -- It is part of the application since it is indented
-aux x (x -- parentheses use `withoutPosition`
+discard <| aux x (x -- parentheses use `withoutPosition`
 -1)
-aux x x;
+discard <| aux x x;
   aux x
  x
 
diff --git a/tests/lean/run/finally.lean b/tests/lean/run/finally.lean
index 19f6580c41..b46ffef2d1 100644
--- a/tests/lean/run/finally.lean
+++ b/tests/lean/run/finally.lean
@@ -37,7 +37,7 @@ tryCatchThe IO.Error
 def tst3 : M Nat :=
 tryCatchThe IO.Error
   (tryFinally
-    (tryFinally f1 (do set 100; IO.println "inner finisher executed"; f2; pure ()))
+    (tryFinally f1 (do set 100; IO.println "inner finisher executed"; discard $ f2; pure ()))
     (do modify Nat.succ; IO.println "outer finisher executed"))
   (fun _ => get)
 
@@ -67,6 +67,6 @@ let (a, _) ← tryFinally' f2 (fun a? => do IO.println ("finalizer received: " +
 pure a
 
 def tst7 : IO Unit :=
-tryCatchThe IO.Error (do (tst6.run).run' 0; pure ()) (fun _ => IO.println "failed as expected")
+tryCatchThe IO.Error (do discard $ (tst6.run).run' 0; pure ()) (fun _ => IO.println "failed as expected")
 
 #eval tst7
diff --git a/tests/lean/run/meta3.lean b/tests/lean/run/meta3.lean
index 55ba4dec8a..eea22a6a9b 100644
--- a/tests/lean/run/meta3.lean
+++ b/tests/lean/run/meta3.lean
@@ -24,7 +24,7 @@ do let v? ← getExprMVarAssignment? m.mvarId!;
 unsafe def run (mods : List Name) (x : MetaM Unit) (opts : Options := dbgOpt) : IO Unit :=
 withImportModules (mods.map $ fun m => {module := m}) {} 0 fun env => do
    let x : MetaM Unit := do { x; printTraces };
-   x.toIO { options := opts } { env := env };
+   discard $ x.toIO { options := opts } { env := env };
    pure ()
 
 def nat  := mkConst `Nat
diff --git a/tests/lean/run/parsePrelude.lean b/tests/lean/run/parsePrelude.lean
index 6cc7066877..4fb3588542 100644
--- a/tests/lean/run/parsePrelude.lean
+++ b/tests/lean/run/parsePrelude.lean
@@ -5,7 +5,7 @@ if System.Platform.isWindows then
   pure () -- TODO investigate why the following doesn't work on Windows
 else do
   let env ← Lean.mkEmptyEnvironment;
-  Lean.Parser.testParseFile env (System.mkFilePath ["..", "..", "..", "src", "Init", "Prelude.lean"]);
+  discard <| Lean.Parser.testParseFile env (System.mkFilePath ["..", "..", "..", "src", "Init", "Prelude.lean"]);
   IO.println "done"
 
 #eval test
diff --git a/tests/lean/run/task_test_io.lean b/tests/lean/run/task_test_io.lean
index f567c33083..3a7bd2775c 100644
--- a/tests/lean/run/task_test_io.lean
+++ b/tests/lean/run/task_test_io.lean
@@ -26,7 +26,7 @@
     IO.println (if c then "canceled! 2" else "done! 2")
   };
   IO.cancel t1;
-  IO.wait t1;
+  discard $ IO.wait t1;
   pure ()
 
 #eval IO.waitAny [