fix: remove incorrect test

It had two problems:
- It was preventing coercions from being applied.
- It was compromising error recovery. The body of the lambda was not
being elaborated when the exception was thrown.

The new error message is more verbose and potentially confusing, but
it is better than the one produced this morning.

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

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

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