feat: better error message in T% elaborator (#36040)

When applying the `T%` elaborator to sections of a fibre bundle, previously in the case of missing typeclass assumptions the elaborator would silently do nothing. Now it errors about this case.

Thanks to Patrick Massot for reporting this bug in person.

Author: grunweg

Mathlib/Geometry/Manifold/Notation.lean

@@ -172,7 +172,14 @@ def totalSpaceMk (e : Expr) : MetaM Expr := do
               some <$> mkLambdaFVars #[x] body
             else return none
           | _ => return none
-        return f?.getD e.headBeta
+        match f? with
+        | some e => return e.headBeta
+        | none =>
+          -- future: special-case `Bundle.TotalSpace` for V;
+          -- if so, say "there is no need to apply T% twice"
+          throwError "could not find a `FiberBundle` instance on `{V}`:\n\
+          `{e}` is a function into `{V}`\n\n\
+          hint: you may be missing suitable typeclass assumptions"
       | tgt =>
         trace[Elab.DiffGeo.TotalSpaceMk] "Section of a trivial bundle as a non-dependent function"
         -- TODO: can `tgt` depend on `x` in a way that is not a function application?

MathlibTest/DifferentialGeometry/Notation/Basic.lean

@@ -139,15 +139,50 @@ example : (fun m ↦ (X m : TangentBundle I M)) = (fun m ↦ TotalSpace.mk' E m
 #guard_msgs in
 #check T% (fun x ↦ X x) x
 
--- Applying the same elaborator twice is fine (and idempotent).
-/-- info: fun m ↦ TotalSpace.mk' E m (X m) : M → TotalSpace E (TangentSpace I) -/
+-- Applying the same elaborator twice errors.
+/--
+error: could not find a `FiberBundle` instance on `TotalSpace E`:
+`fun m ↦ TotalSpace.mk' E m (X m)` is a function into `TotalSpace E`
+
+hint: you may be missing suitable typeclass assumptions
+-/
 #guard_msgs in
 #check (T% (T% X))
 
-/-- info: (fun m ↦ TotalSpace.mk' E m (X m)) x : TotalSpace E (TangentSpace I) -/
+/--
+error: could not find a `FiberBundle` instance on `TotalSpace E`:
+`fun m ↦ TotalSpace.mk' E m (X m)` is a function into `TotalSpace E`
+
+hint: you may be missing suitable typeclass assumptions
+-/
 #guard_msgs in
 #check (T% (T% X)) x
 
+-- Error message when missing typeclass assumptions for sections of a fiber bundle.
+-- This used to silently do nothing; now there is a helpful error.
+section
+
+variable {B F Z : Type*} [TopologicalSpace B] [TopologicalSpace F]
+  {E : B → Type*} [TopologicalSpace (TotalSpace F E)]
+  (e : Trivialization F (π F E)) [(x : B) → Zero (E x)]
+
+variable (σ : (b : B) → E b) in
+/--
+error: could not find a `FiberBundle` instance on `E`:
+`σ` is a function into `E`
+
+hint: you may be missing suitable typeclass assumptions
+-/
+#guard_msgs in
+#check T% σ
+
+/-- info: fun b ↦ TotalSpace.mk' F b (σ b) : B → TotalSpace F E -/
+#guard_msgs in
+variable [(b : B) → TopologicalSpace (E b)] [FiberBundle F E] (σ : (b : B) → E b) in
+#check T% σ
+
+end
+
 end TotalSpace
 
 /-! Tests for the elaborators for `MDifferentiable{WithinAt,At,On}`. -/