feat: #eval: auto-hide () output for m Unit chained instances

src/Init/Lean/Elab/Term.lean

@@ -1152,7 +1152,7 @@ fun stx _ =>
   | none     => throwError stx "ill-formed syntax"
 
 instance MetaHasEval {α} [MetaHasEval α] : MetaHasEval (TermElabM α) :=
-⟨fun env opts x => do
+⟨fun env opts x _ => do
   let ctx : Context := {
     config        := { opts := opts },
     fileName      := "<TermElabM>",
@@ -1177,7 +1177,7 @@ instance MetaHasEval {α} [MetaHasEval α] : MetaHasEval (TermElabM α) :=
     throw (IO.userError "error: unsupported syntax")
   | EStateM.Result.error Exception.postpone s => do
     showMessages s;
-    throw (IO.userError "error: elaborator posponed")⟩
+    throw (IO.userError "error: elaborator postponed")⟩
 
 end Term
 

src/Init/Lean/Eval.lean

@@ -16,10 +16,10 @@ universe u
     The basic `HasEval` class is in the prelude and should not depend on these
     types. -/
 class MetaHasEval (α : Type u) :=
-(eval : Environment → Options → α → IO Unit)
+(eval : Environment → Options → α → forall (hideUnit : optParam Bool true), IO Unit)
 
-instance MetaHasEvalOfHasEval {α : Type u} [HasEval α] : MetaHasEval α :=
-⟨fun env opts a => HasEval.eval a⟩
+instance metaHasEvalOfHasEval {α : Type u} [HasEval α] : MetaHasEval α :=
+⟨fun env opts a hideUnit => HasEval.eval a hideUnit⟩
 
 abbrev MetaIO := ReaderT (Environment × Options) IO
 
@@ -29,8 +29,8 @@ ctx ← read; pure ctx.1
 def MetaIO.getOptions : MetaIO Options := do
 ctx ← read; pure ctx.2
 
-instance MetaIO.metaHasEval : MetaHasEval (MetaIO Unit) :=
-⟨fun env opts x => x (env, opts)⟩
+instance MetaIO.metaHasEval {α} [MetaHasEval α] : MetaHasEval (MetaIO α) :=
+⟨fun env opts x _ => x (env, opts) >>= MetaHasEval.eval env opts⟩
 
 instance MetaIO.monadIO : MonadIO MetaIO :=
 ⟨fun _ x _ => x⟩

src/Init/Lean/Meta/Message.lean

@@ -85,7 +85,7 @@ def toMessageData : Exception → MessageData
 end Exception
 
 instance MetaHasEval {α} [MetaHasEval α] : MetaHasEval (MetaM α) :=
-⟨fun env opts x => do
+⟨fun env opts x _ => do
    match x { config := { opts := opts }, currRecDepth := 0, maxRecDepth := getMaxRecDepth opts } { env := env } with
    | EStateM.Result.ok a s    => do
      s.traceState.traces.forM $ fun m => IO.println $ format m;

src/Init/System/IO.lean

@@ -308,16 +308,17 @@ namespace Lean
 
 /-- Typeclass used for presenting the output of an `#eval` command. -/
 class HasEval (α : Type u) :=
-(eval : α → IO Unit)
+-- We default `hideUnit` to `true`, but set it to `false` in the direct call from `#eval`
+-- so that `()` output is hidden in chained instances such as for some `m Unit`.
+(eval : α → forall (hideUnit : optParam Bool true), IO Unit)
 
-instance HasRepr.HasEval {α : Type u} [HasRepr α] : HasEval α :=
-⟨fun a => IO.println (repr a)⟩
+instance HasRepr.hasEval {α : Type u} [HasRepr α] : HasEval α :=
+⟨fun a _ => IO.println (repr a)⟩
+
+instance Unit.hasEval : HasEval Unit :=
+⟨fun u hideUnit => if hideUnit then pure () else IO.println (repr u)⟩
 
 instance IO.HasEval {α : Type} [HasEval α] : HasEval (IO α) :=
-⟨fun x => do a ← x; HasEval.eval a⟩
-
--- special case: do not print `()`
-instance IOUnit.HasEval : HasEval (IO Unit) :=
-⟨fun x => x⟩
+⟨fun x _ => do a ← x; HasEval.eval a⟩
 
 end Lean

src/frontends/lean/builtin_cmds.cpp

@@ -349,12 +349,12 @@ static environment eval_cmd(parser & p) {
     } catch (exception &) {}
 
     if (meta_eval_instance) {
-        /* Modify the 'program' to (fun env opts => MetaHasEval.eval env opts e) */
+        /* Modify the 'program' to (fun env opts => MetaHasEval.eval (hideUnit := false) env opts e) */
         expr env = tc.push_local("env", mk_const({"Lean", "Environment"}));
         expr opts = tc.push_local("opts", mk_const({"Lean", "Options"}));
         e = tc.mk_lambda(env, tc.mk_lambda(opts,
-                                           mk_app(tc, {"Lean", "MetaHasEval", "eval"}, 5,
-                                                  {type, *meta_eval_instance, env, opts, e})));
+                                           mk_app(tc, {"Lean", "MetaHasEval", "eval"}, 6,
+                                                  {type, *meta_eval_instance, env, opts, e, mk_bool_false()})));
         // run `Environment -> Options -> IO Unit`
         args = { p.env().to_obj_arg(), p.get_options().to_obj_arg(), io_mk_world() };
     } else {
@@ -365,8 +365,8 @@ static environment eval_cmd(parser & p) {
         } catch (exception &) {}
 
         if (eval_instance) {
-            /* Modify the 'program' to (HasEval.eval e) */
-            e = mk_app(tc, {"Lean", "HasEval", "eval"}, 3, type, *eval_instance, e);
+            /* Modify the 'program' to (HasEval.eval (hideUnit := false) e) */
+            e = mk_app(tc, {"Lean", "HasEval", "eval"}, 4, {type, *eval_instance, e, mk_bool_false()});
             // run `IO Unit`
             args = { io_mk_world() };
         } else {