diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 348f608cb5..22ec0674c0 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -74,7 +74,7 @@ if h : 0 < prevHeaders.size then
 else
   pure ()
 
-private def elabFunType (xs : Array Expr) (view : DefView) : TermElabM Expr :=
+private def elabFunType (ref : Syntax) (xs : Array Expr) (view : DefView) : TermElabM Expr :=
 match view.type? with
 | some typeStx => do
   type ← elabType typeStx;
@@ -82,7 +82,8 @@ match view.type? with
   type ← instantiateMVars type;
   mkForallFVars xs type
 | none => do
-  type ← withRef view.binders $ mkFreshTypeMVar;
+  let hole := mkHole ref;
+  type ← elabType hole;
   mkForallFVars xs type
 
 private def elabHeaders (views : Array DefView) : TermElabM (Array DefViewElabHeader) :=
@@ -93,7 +94,8 @@ views.foldlM
     ⟨shortDeclName, declName, levelNames⟩ ← expandDeclId currNamespace currLevelNames view.declId view.modifiers;
     applyAttributes declName view.modifiers.attrs AttributeApplicationTime.beforeElaboration;
     withLevelNames levelNames $ elabBinders view.binders.getArgs fun xs => do
-      type ← elabFunType xs view;
+      let refForElabFunType := view.value;
+      type ← elabFunType refForElabFunType xs view;
       let newHeader : DefViewElabHeader := {
         ref           := view.ref,
         modifiers     := view.modifiers,
diff --git a/tests/lean/holes.lean b/tests/lean/holes.lean
index d444874af2..5fe9a4e6be 100644
--- a/tests/lean/holes.lean
+++ b/tests/lean/holes.lean
@@ -17,3 +17,6 @@ def f5 {α} {β : _} (a : α) := a
 def f6 (a : Nat) :=
 let f {α β} (a : α) := a;
 f a
+
+partial def f7 (x : Nat) :=
+f7 x
diff --git a/tests/lean/holes.lean.expected.out b/tests/lean/holes.lean.expected.out
index 8fe88a080d..9b0cc34dfa 100644
--- a/tests/lean/holes.lean.expected.out
+++ b/tests/lean/holes.lean.expected.out
@@ -45,3 +45,7 @@ f6 : Nat → Nat
 a : Nat
 α : Type
 ⊢ Sort ?
+holes.lean:21:25: error: don't know how to synthesize placeholder
+context:
+x : Nat
+⊢ Sort ?