feat: improve #eval command

Now, if it fails to synthesize the TC instance, it applies `whnf` and
tries again.

src/Lean/Elab/BuiltinCommand.lean

@@ -277,7 +277,11 @@ private def mkEvalInstCore (evalClassName : Name) (e : Expr) : MetaM Expr := do
   try
     synthInstance inst
   catch _ =>
-    throwError "expression{indentExpr e}\nhas type{indentExpr α}\nbut instance{indentExpr inst}\nfailed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `{evalClassName}` class"
+    -- Reduce `α` and try again
+    try
+      synthInstance (mkApp (Lean.mkConst evalClassName [u]) (← whnf α))
+    catch _ =>
+      throwError "expression{indentExpr e}\nhas type{indentExpr α}\nbut instance{indentExpr inst}\nfailed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `{evalClassName}` class"
 
 private def mkRunMetaEval (e : Expr) : MetaM Expr :=
   withLocalDeclD `env (mkConst ``Lean.Environment) fun env =>

tests/lean/defInst.lean

@@ -3,7 +3,7 @@ def Foo := List Nat
 def test (x : Nat) : Foo :=
   [x, x+1, x+2]
 
-#eval test 4 -- Error
+#eval test 4
 
 #check fun (x y : Foo) => x == y -- Error
 

tests/lean/defInst.lean.expected.out

@@ -1,10 +1,4 @@
-defInst.lean:6:0-6:12: error: expression
-  test 4
-has type
-  Foo
-but instance
-  Lean.Eval Foo
-failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.Eval` class
+[4, 5, 6]
 defInst.lean:8:26-8:32: error: failed to synthesize instance
   BEq Foo
 fun x y => sorryAx (?m x y) : (x y : Foo) → ?m x y

tests/lean/run/hlistOverload.lean

@@ -31,18 +31,6 @@ example : [10, true, 20.1].nth #0 = (10:Nat) := rfl
 example : [10, true, 20.1].nth #1 = true     := rfl
 example : [10, true, 20.1].nth #2 = 20.1     := rfl
 
-#eval id (α := Nat) ([10, true, 20.1].nth #0)
-
-def the (α : Type u) (a : α) := a
-
-#eval the Nat ([10, true, 20.1].nth #0)
-#eval the Bool ([10, true, 20.1].nth #1)
-#eval the Float ([10, true, 20.1].nth #2)
-
--- If we mark `List.nth` as `[reducible]`, typeclass resolution will reduce it,
--- when trying to synthesize a `Repr` instance in the following examples.
-attribute [reducible] List.nth
-
 #eval [10, true, 20.1].nth #0
 #eval [10, true, 20.1].nth #1
 #eval [10, true, 20.1].nth #2