diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 9f4a7e78b4..fafe44b239 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/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 =>
diff --git a/tests/lean/defInst.lean b/tests/lean/defInst.lean
index cd8f0022dd..c614d3528d 100644
--- a/tests/lean/defInst.lean
+++ b/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
 
diff --git a/tests/lean/defInst.lean.expected.out b/tests/lean/defInst.lean.expected.out
index d8ec787a0e..8a93131a95 100644
--- a/tests/lean/defInst.lean.expected.out
+++ b/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
diff --git a/tests/lean/run/hlistOverload.lean b/tests/lean/run/hlistOverload.lean
index 9d9186d337..5fc33715d4 100644
--- a/tests/lean/run/hlistOverload.lean
+++ b/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