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

@@ -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

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

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

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))

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))

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"
 

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

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

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

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

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 ()

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

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
 

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

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

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

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 [