diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index f01583cc0b..ed92845871 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -313,10 +313,7 @@ private def propagateExpectedType (fvar : Expr) (fvarType : Expr) (s : State) :
       let b := b.instantiate1 fvar
       pure { s with expectedType? := some b }
     | _ =>
-      if expectedType.getAppFn.isMVar then
-        pure { s with expectedType? := none }
-      else
-        throwError "expected type is not a function type{indentExpr expectedType}"
+      pure { s with expectedType? := none }
 
 private partial def elabFunBinderViews (binderViews : Array BinderView) (i : Nat) (s : State) : TermElabM State := do
   if h : i < binderViews.size then
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 3c21d04d64..6984161da3 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -932,20 +932,10 @@ private def postponeElabTerm (stx : Syntax) (expectedType? : Option Expr) : Term
   registerSyntheticMVar stx mvar.mvarId! (SyntheticMVarKind.postponed (← saveContext))
   pure mvar
 
-private def decorateErrorMessageWithLambdaImplicitVars (ref : Syntax) (msg : MessageData) (impFVars : Array Expr) : TermElabM Exception := do
-  if impFVars.isEmpty then
-    return Exception.error ref msg
-  else
-    let mut msg := m!"{msg}\nthe following variables have been introduced by the implicit lamda feature"
-    for impFVar in impFVars do
-      msg := m!"{msg}{indentD m!"{impFVar} : {← inferType impFVar}"}"
-    msg := m!"{msg}\nyou can disable implict lambdas using `@` or writing a lambda expression with `\{}` or `[]` binder annotations."
-    return Exception.error ref msg
-
 /-
   Helper function for `elabTerm` is tries the registered elaboration functions for `stxNode` kind until it finds one that supports the syntax or
   an error is found. -/
-private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone : Bool) (impFVars : Array Expr)
+private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone : Bool)
     : List TermElab → TermElabM Expr
   | []                => do throwError "unexpected syntax{indentD stx}"
   | (elabFn::elabFns) => do
@@ -953,7 +943,6 @@ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? :
       elabFn stx expectedType?
     catch ex => match ex with
       | Exception.error ref msg =>
-        let ex ← decorateErrorMessageWithLambdaImplicitVars ref msg impFVars
         if (← read).errToSorry then
           exceptionToSorry ex expectedType?
         else
@@ -963,7 +952,7 @@ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? :
           exceptionToSorry ex expectedType?
         else if id == unsupportedSyntaxExceptionId then
           s.restore
-          elabUsingElabFnsAux s stx expectedType? catchExPostpone impFVars elabFns
+          elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns
         else if catchExPostpone && id == postponeExceptionId then
           /- If `elab` threw `Exception.postpone`, we reset any state modifications.
              For example, we want to make sure pending synthetic metavariables created by `elab` before
@@ -984,12 +973,12 @@ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? :
           else
             throw ex
 
-private def elabUsingElabFns (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone : Bool) (impFVars : Array Expr): TermElabM Expr := do
+private def elabUsingElabFns (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone : Bool) : TermElabM Expr := do
   let s ← saveState
   let table := termElabAttribute.ext.getState (← getEnv) |>.table
   let k := stx.getKind
   match table.find? k with
-  | some elabFns => elabUsingElabFnsAux s stx expectedType? catchExPostpone impFVars elabFns
+  | some elabFns => elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns
   | none         => throwError "elaboration function for '{k}' has not been implemented{indentD stx}"
 
 instance : MonadMacroAdapter TermElabM where
@@ -1064,12 +1053,30 @@ private def useImplicitLambda? (stx : Syntax) (expectedType? : Option Expr) : Te
         | _                    => pure none
     | _         => pure none
 
+private def decorateErrorMessageWithLambdaImplicitVars (ex : Exception) (impFVars : Array Expr) : TermElabM Exception := do
+  match ex with
+  | Exception.error ref msg =>
+    if impFVars.isEmpty then
+      return Exception.error ref msg
+    else
+      let mut msg := m!"{msg}\nthe following variables have been introduced by the implicit lamda feature"
+      for impFVar in impFVars do
+        let auxMsg := m!"{impFVar} : {← inferType impFVar}"
+        let auxMsg ← addMessageContext auxMsg
+        msg := m!"{msg}{indentD auxMsg}"
+      msg := m!"{msg}\nyou can disable implict lambdas using `@` or writing a lambda expression with `\{}` or `[]` binder annotations."
+      return Exception.error ref msg
+  | _ => return ex
+
 private def elabImplicitLambdaAux (stx : Syntax) (catchExPostpone : Bool) (expectedType : Expr) (impFVars : Array Expr) : TermElabM Expr := do
-  let body ← elabUsingElabFns stx expectedType catchExPostpone impFVars
-  let body ← ensureHasType expectedType body
-  let r ← mkLambdaFVars impFVars body
-  trace[Elab.implicitForall] r
-  pure r
+  let body ← elabUsingElabFns stx expectedType catchExPostpone
+  try
+    let body ← ensureHasType expectedType body
+    let r ← mkLambdaFVars impFVars body
+    trace[Elab.implicitForall] r
+    pure r
+  catch ex =>
+    throw (← decorateErrorMessageWithLambdaImplicitVars ex impFVars)
 
 private partial def elabImplicitLambda (stx : Syntax) (catchExPostpone : Bool) (type : Expr) : TermElabM Expr :=
   loop type #[]
@@ -1103,7 +1110,7 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone :
       let implicit? ← if implicitLambda && (← read).implicitLambda then useImplicitLambda? stx expectedType? else pure none
       match implicit? with
       | some expectedType => elabImplicitLambda stx catchExPostpone expectedType
-      | none              => elabUsingElabFns stx expectedType? catchExPostpone (impFVars := #[])
+      | none              => elabUsingElabFns stx expectedType? catchExPostpone
 
 def addTermInfo (stx : Syntax) (e : Expr) : TermElabM Unit := do
   if (← getInfoState).enabled then
diff --git a/tests/lean/mulcommErrorMessage.lean.expected.out b/tests/lean/mulcommErrorMessage.lean.expected.out
index 83c5363b26..8b3daf9bd3 100644
--- a/tests/lean/mulcommErrorMessage.lean.expected.out
+++ b/tests/lean/mulcommErrorMessage.lean.expected.out
@@ -1,12 +1,34 @@
-mulcommErrorMessage.lean:8:17-8:18: error: expected type is not a function type
-  a✝ * b✝ = b✝ * a✝
+mulcommErrorMessage.lean:8:13-13:25: error: type mismatch
+  fun (a : ?m) (b : ?m a) => ?m a b
+has type
+  (a : ?m) → (b : ?m a) → ?m a b : Sort (imax ?u ?u ?u)
+but is expected to have type
+  a✝ * b✝ = b✝ * a✝ : Prop
 the following variables have been introduced by the implicit lamda feature
   a✝ : Bool
   b✝ : Bool
 you can disable implict lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.
-mulcommErrorMessage.lean:16:5-16:6: error: expected type is not a function type
-  a✝ * b✝ = b✝ * a✝
+mulcommErrorMessage.lean:11:22-11:25: error: type mismatch
+  rfl
+has type
+  true = true : Prop
+but is expected to have type
+  true = false : Prop
+mulcommErrorMessage.lean:16:3-17:47: error: type mismatch
+  fun (a b : Bool) => Bool.casesOn a (?m a b) (?m a b)
+has type
+  (a b : Bool) → ?m a b a : Sort (imax 1 1 ?u)
+but is expected to have type
+  a✝ * b✝ = b✝ * a✝ : Prop
 the following variables have been introduced by the implicit lamda feature
   a✝ : Bool
   b✝ : Bool
 you can disable implict lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.
+mulcommErrorMessage.lean:16:12-17:47: error: application type mismatch
+  Bool.casesOn a ?m (Bool.casesOn b ?m ?m)
+argument
+  Bool.casesOn b ?m ?m
+has type
+  ?m a b b : Sort ?u
+but is expected to have type
+  ?m a b true : Sort ?u