fix: have #eval save the info context (#10008)

This PR fixes a bug in `#eval` where clicking on the evaluated
expression could show errors in the Infoview. This was caused by `#eval`
not saving the temporary environment that is used when elaborating the
expression.

src/Lean/Elab/BuiltinEvalCommand.lean

@@ -217,15 +217,16 @@ unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax) (expectedType? :
       -- Generate an action without executing it. We use `withoutModifyingEnv` to ensure
       -- we don't pollute the environment with auxiliary declarations.
       let act : EvalAction ← liftTermElabM do Term.withDeclName declName do withoutModifyingEnv do
-        let e ← elabTermForEval term expectedType?
-        -- If there is an elaboration error, don't evaluate!
-        if e.hasSyntheticSorry then throwAbortTerm
-        -- We want `#eval` to work even in the core library, so if `ofFormat` isn't available,
-        -- we fall back on a `Format`-based approach.
-        if (← getEnv).contains ``Lean.MessageData.ofFormat then
-          mkAct id (mkMessageData ·) e
-        else
-          mkAct Lean.MessageData.ofFormat (mkFormat ·) e
+        withSaveInfoContext do -- save the environment post-elaboration (for matchers, let rec, etc.)
+          let e ← elabTermForEval term expectedType?
+          -- If there is an elaboration error, don't evaluate!
+          if e.hasSyntheticSorry then throwAbortTerm
+          -- We want `#eval` to work even in the core library, so if `ofFormat` isn't available,
+          -- we fall back on a `Format`-based approach.
+          if (← getEnv).contains ``Lean.MessageData.ofFormat then
+            mkAct id (mkMessageData ·) e
+          else
+            mkAct Lean.MessageData.ofFormat (mkFormat ·) e
       let res ← act.eval
       return Sum.inr (res, act.printVal)
     catch ex =>

tests/lean/interactive/hover.lean

@@ -299,3 +299,10 @@ open List renaming zip → zip'
                  --^ textDocument/hover
 
 end Foo
+
+/-!
+`#eval` needs to save info context for this hover to give the inferred type,
+since it needs the environment with the generated `_eval.match_1` matcher.
+-/
+#eval (default : Nat) matches .succ ..
+                      --^ textDocument/hover

tests/lean/interactive/hover.lean.expected.out

@@ -650,3 +650,9 @@
  {"value":
   "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} : List α → List β → List (α × β)\n```\n***\nCombines two lists into a list of pairs in which the first and second components are the\ncorresponding elements of each list. The resulting list is the length of the shorter of the input\nlists.\n\n`O(min |xs| |ys|)`.\n\nExamples:\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2, 3] = [(\"Mon\", 1), (\"Tue\", 2), (\"Wed\", 3)]`\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2] = [(\"Mon\", 1), (\"Tue\", 2)]`\n* `[x₁, x₂, x₃].zip [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*",
   "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hover.lean"},
+ "position": {"line": 306, "character": 24}}
+{"range":
+ {"start": {"line": 306, "character": 6},
+  "end": {"line": 306, "character": 38}},
+ "contents": {"value": "```lean\nBool\n```", "kind": "markdown"}}