diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index c124f55a84..d88923fdeb 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -102,9 +102,14 @@ private def elabHeaders (views : Array DefView) : TermElabM (Array DefViewElabHe
         elabBinders (catchAutoBoundImplicit := true) view.binders.getArgs fun xs => do
           let refForElabFunType := view.value
           elabFunType refForElabFunType xs view fun xs type => do
-            let type ← mkForallFVars (← read).autoBoundImplicits.toArray type
+            let mut type ← mkForallFVars (← read).autoBoundImplicits.toArray type
             let xs ← addAutoBoundImplicits xs
             let levelNames ← getLevelNames
+            if view.type?.isSome then
+              Term.synthesizeSyntheticMVarsNoPostponing
+              type ← instantiateMVars type
+              let pendingMVarIds ← getMVars type
+              discard <| logUnassignedUsingErrorInfos pendingMVarIds
             let newHeader := {
               ref           := view.ref,
               modifiers     := view.modifiers,
diff --git a/tests/bench/binarytrees.lean b/tests/bench/binarytrees.lean
index 5e5e4e6d40..9e48dcb6b0 100644
--- a/tests/bench/binarytrees.lean
+++ b/tests/bench/binarytrees.lean
@@ -21,7 +21,7 @@ def check : Tree → UInt32
 
 def minN := 4
 
-def out (s) (n : Nat) (t : UInt32) : IO Unit :=
+def out (s : String) (n : Nat) (t : UInt32) : IO Unit :=
 IO.println (s ++ " of depth " ++ toString n ++ "\t check: " ++ toString t)
 
 -- allocate and check lots of trees
diff --git a/tests/lean/holeErrors.lean b/tests/lean/holeErrors.lean
index d6be4d7452..5d5e5f2391 100644
--- a/tests/lean/holeErrors.lean
+++ b/tests/lean/holeErrors.lean
@@ -1,4 +1,4 @@
-
+--
 
 def f1 := id
 
diff --git a/tests/lean/holeErrors.lean.expected.out b/tests/lean/holeErrors.lean.expected.out
index 35e8fb158f..b12183de22 100644
--- a/tests/lean/holeErrors.lean.expected.out
+++ b/tests/lean/holeErrors.lean.expected.out
@@ -3,10 +3,6 @@ holeErrors.lean:3:10: error: don't know how to synthesize implicit argument
 context:
 ⊢ Sort u_1
 holeErrors.lean:3:7: error: failed to infer definition type
-holeErrors.lean:5:14: error: don't know how to synthesize implicit argument
-  @id ?m
-context:
-⊢ Sort u_1
 holeErrors.lean:5:9: error: failed to infer definition type
 holeErrors.lean:8:9: error: don't know how to synthesize implicit argument
   @id ?m
diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index ed8a462d3f..5e4c3a1af9 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -419,5 +419,5 @@ def f3 x y :=
 theorem f3eq x y : f3 x y = x + y + 1 :=
   rfl
 
-def f4 x y : String :=
+def f4 (x y : Nat) : String :=
   if x > y + 1 then "hello" else "world"
diff --git a/tests/lean/theoremType.lean b/tests/lean/theoremType.lean
new file mode 100644
index 0000000000..a52a8418f6
--- /dev/null
+++ b/tests/lean/theoremType.lean
@@ -0,0 +1,5 @@
+theorem ex1 : 1 + 1 = _ := -- Error
+  show 1 + 1 = 2 by rfl
+
+def ex2 : 1 + 1 = _ := -- Error
+  show 1 + 1 = 2 by rfl
diff --git a/tests/lean/theoremType.lean.expected.out b/tests/lean/theoremType.lean.expected.out
new file mode 100644
index 0000000000..8c71c1feb4
--- /dev/null
+++ b/tests/lean/theoremType.lean.expected.out
@@ -0,0 +1,6 @@
+theoremType.lean:1:22: error: don't know how to synthesize placeholder
+context:
+⊢ Nat
+theoremType.lean:4:18: error: don't know how to synthesize placeholder
+context:
+⊢ Nat