feat(Tactic/InferInstanceAsPercent): error on unification failure, guard getAppFn

Throw an error when source and expected types fail to unify, and
check that the class heads match before comparing arguments pairwise (#1).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: kim-em

Mathlib/Tactic/InferInstanceAsPercent.lean

@@ -180,11 +180,17 @@ noncomputable instance : Field (FiniteResidueField K) :=
 elab "inferInstanceAs% " source:term : term <= expectedType => do
   let sourceType ← elabType source
   -- Unify source with expected type to resolve metavariables (e.g., _ placeholders)
-  discard <| withDefault <| isDefEq sourceType expectedType
+  unless ← withDefault <| isDefEq sourceType expectedType do
+    throwError "inferInstanceAs%: source type{indentExpr sourceType}\n\
+      is not defeq to expected type{indentExpr expectedType}"
   let sourceType ← instantiateMVars sourceType
   let inst ← synthInstance sourceType
   let inst ← instantiateMVars inst
   let expectedType ← instantiateMVars expectedType
+  -- Check that the class heads match before comparing arguments pairwise
+  unless sourceType.getAppFn == expectedType.getAppFn do
+    throwError "inferInstanceAs%: source type head{indentExpr sourceType.getAppFn}\n\
+      does not match expected type head{indentExpr expectedType.getAppFn}"
   -- Build replacement table from differing carrier type arguments
   let replacements ← buildReplacements sourceType expectedType
   if replacements.isEmpty then return inst