fix(Geometry/Manifold/Notation): better error message if the expected type contains metavariables (#35180)

Author: grunweg

Mathlib/Geometry/Manifold/Notation.lean

@@ -687,9 +687,13 @@ partial def findModel (e : Expr) (baseInfo : Option (Expr × Expr) := none) : Te
   if let some { model .. } ← go e baseInfo then
     return model
   else
-    let hint := if (← isTracingEnabledFor `Elab.DiffGeo.MDiff) then m!"" else
-      .hint' "failures to find a model with corners can be debugged with the \
-        command `set_option trace.Elab.DiffGeo.MDiff true`."
+    let tracing := (← isTracingEnabledFor `Elab.DiffGeo.MDiff)
+    let hint : MessageData := if e.hasExprMVar then
+      .hint' "the expected type contains metavariables, \
+        maybe you need to provide an implicit argument"
+      else if tracing then m!"" else
+        .hint' "failures to find a model with corners can be debugged with the \
+          command `set_option trace.Elab.DiffGeo.MDiff true`."
     throwError "Could not find a model with corners for `{e}`.{hint}"
 where
   go (e : Expr) (baseInfo : Option (Expr × Expr)) : TermElabM (Option FindModelResult) := do

MathlibTest/DifferentialGeometry/NotationAdvanced.lean

@@ -46,11 +46,10 @@ def proj : TangentBundle 𝓘(𝕜, 𝕜) 𝕜 → 𝕜 := fun x ↦ x.2
 
 open ContDiff
 
--- TODO: the error message could be more helpful, by saying "the goal has metavariables; maybe there is an implicit argument missing"
 /--
 error: Could not find a model with corners for `TangentBundle 𝓘(?_, ?_) ?_`.
 
-Hint: failures to find a model with corners can be debugged with the command `set_option trace.Elab.DiffGeo.MDiff true`.
+Hint: the expected type contains metavariables, maybe you need to provide an implicit argument
 -/
 #guard_msgs in
 set_option pp.mvars.anonymous false in