fix more outputs

Author: Garmelon

Manual/BasicTypes/Range.lean

@@ -332,8 +332,10 @@ Ranges can't be iterated over:
     IO.println s!"It's {repr d}"
 ```
 ```leanOutput noIter
-failed to synthesize instance for 'for_in%' notation
-  ForIn (EIO IO.Error) (Std.Rcc Day) ?m.11
+failed to synthesize instance of type class
+  ForIn IO (Std.Rcc Day) ?α
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 ```
 Nor can they be enumerated, even though the type is finite:
 ```lean +error (name := noEnum)
@@ -508,8 +510,10 @@ It's also possible to create an iterator that can be enumerated, but it can't ye
     IO.println s!"It's {repr d}."
 ```
 ```leanOutput iterForNo
-failed to synthesize instance for 'for_in%' notation
-  ForIn (EIO IO.Error) (Std.Iter Day) ?m.12
+failed to synthesize instance of type class
+  ForIn IO (Std.Iter Day) ?α
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 ```
 
 :::

Manual/Iterators.lean

@@ -401,8 +401,10 @@ Because there are infinitely many {name}`Nat`s, using {name}`Iter.ensureTerminat
     IO.println s!"{x}"
 ```
 ```leanOutput natterm
-failed to synthesize instance for 'for_in%' notation
-  ForIn (EIO IO.Error) (Iter.Total Nat) ?m.12
+failed to synthesize instance of type class
+  ForIn IO (Iter.Total Nat) ?α
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 ```
 :::
 ::::

Manual/Monads/Syntax.lean

@@ -607,8 +607,7 @@ inst✝ : DecidablePred p
 xs : Array α
 out✝ : Array Nat := #[]
 i : Nat
-r✝ : Array Nat
-out : Array Nat := r✝
+out : Array Nat := __s✝
 ⊢ i < xs.size
 -/
 #check_msgs in
@@ -822,7 +821,11 @@ The rules are as follows:
     set 6
     return
 
-/-- error: must be last element in a `do` sequence -/
+/--
+warning: This `do` element and its control-flow region are dead code. Consider removing it.
+---
+info: ((), 6)
+-/
 #check_msgs in
 #eval (·.run 0) <| show StateM Nat Unit from do
   set 5
@@ -875,7 +878,7 @@ end
 set_option pp.all true
 
 /--
-info: @Bind.bind.{0, 0} m (@Monad.toBind.{0, 0} m inst✝) Unit α e1 fun (x : PUnit.{1}) => es : m α
+info: @Bind.bind.{0, 0} m (@Monad.toBind.{0, 0} m inst✝) PUnit.{1} α e1 fun (__r : PUnit.{1}) => es : m α
 -/
 #check_msgs in
 #check do e1; es
@@ -899,7 +902,8 @@ variable {e1 : m β} {e2 : m γ} {f : β → γ → m Unit} {g : γ → α} {h :
 /--
 info: @Bind.bind.{0, 0} m (@Monad.toBind.{0, 0} m inst✝) β α e1 fun (__do_lift : β) =>
   @Bind.bind.{0, 0} m (@Monad.toBind.{0, 0} m inst✝) γ α e2 fun (__do_lift_1 : γ) =>
-    @Bind.bind.{0, 0} m (@Monad.toBind.{0, 0} m inst✝) Unit α (f __do_lift __do_lift_1) fun (x : PUnit.{1}) => es : m α
+    @Bind.bind.{0, 0} m (@Monad.toBind.{0, 0} m inst✝) PUnit.{1} α (f __do_lift __do_lift_1) fun (__r : PUnit.{1}) =>
+      es : m α
 -/
 #check_msgs in
 #check do f (← e1) (← e2); es

Manual/NotationsMacros/DoElab.lean

@@ -208,7 +208,8 @@ This means that mutable variables in the surrounding block cannot be modified:
   return y
 ```
 ```leanOutput noMutFreeze
-`y` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intend to mutate but define `y`, consider using `let y` instead
+Variable `y` cannot be mutated. Only variables declared using `let mut` can be mutated.
+      If you did not intend to mutate but define `y`, consider using `let y` instead
 ```
 Additionally, an early {keywordOf Lean.Parser.Term.doReturn}`return` exits the inner {keywordOf Lean.Parser.Term.do}`do`, rather than the surrounding one, as indicated by the fact that it is expected to return a {lean}`Unit` (in this case, the universe-polymorphic {name}`PUnit`):
 ```lean +error (name := noInnerReturn)
@@ -221,14 +222,12 @@ Additionally, an early {keywordOf Lean.Parser.Term.doReturn}`return` exits the i
   return y
 ```
 ```leanOutput noInnerReturn
-Application type mismatch: The argument
+Type mismatch
   x
 has type
   Nat
 but is expected to have type
   PUnit
-in the application
-  pure x
 ```
 ::::
 

Manual/VCGen.lean

@@ -500,11 +500,8 @@ xs x : List α✝
 h : (rev xs).run = x
 out✝ : List α✝ := []
 ⊢ (wp⟦do
-      let r ←
-        forIn xs out✝ fun x r => do
-            pure PUnit.unit
-            pure (ForInStep.yield (x :: r))
-      pure r⟧
+      let __s ← forIn xs out✝ fun x __s => pure (ForInStep.yield (x :: __s))
+      pure __s⟧
     (PostCond.noThrow fun a => { down := a = xs.reverse })).down
 ```
 When the verification condition is just the original problem, without even any simplification of {name}`bind`, the problem is usually a missing {name}`WPMonad` instance.