feat: improve @[ext] error message when ext_iff generation fails (#4762)

Now it suggests using `@[ext (iff := false)]` to disable generating the
`ext_iff` lemma.

This PR also adjusts error messages and attribute documentation.
Additionally, to simplify the code now the `x` and `y` arguments can't
come in reverse order (this feature was was added in the refactor
#4543).

Closes #4758

src/Init/Ext.lean

@@ -24,15 +24,16 @@ syntax extFlat := atomic("(" &"flat" " := " &"false" ")")
 /--
 Registers an extensionality theorem.
 
-* When `@[ext]` is applied to a structure, it generates `.ext` and `.ext_iff` theorems and registers
-  them for the `ext` tactic.
-
-* When `@[ext]` is applied to a theorem, the theorem is registered for the `ext` tactic, and it generates an `ext_iff` theorem.
+* When `@[ext]` is applied to a theorem, the theorem is registered for the `ext` tactic, and it generates an "`ext_iff`" theorem.
   The name of the theorem is from adding the suffix `_iff` to the theorem name.
 
-* An optional natural number argument, e.g. `@[ext 9000]`, specifies a priority for the lemma. Higher-priority lemmas are chosen first, and the default is `1000`.
+* When `@[ext]` is applied to a structure, it generates an `.ext` theorem and applies the `@[ext]` attribute to it.
+  The result is an `.ext` and an `.ext_iff` theorem with the `.ext` theorem registered for the `ext` tactic.
 
-* The flag `@[ext (iff := false)]` prevents it from generating an `ext_iff` theorem.
+* An optional natural number argument, e.g. `@[ext 9000]`, specifies a priority for the `ext` lemma.
+  Higher-priority lemmas are chosen first, and the default is `1000`.
+
+* The flag `@[ext (iff := false)]` disables generating an `ext_iff` theorem.
 
 * The flag `@[ext (flat := false)]` causes generated structure extensionality theorems to show inherited fields based on their representation,
   rather than flattening the parents' fields into the lemma's equality hypotheses.

src/Lean/Elab/Tactic/Ext.lean

@@ -74,16 +74,16 @@ def mkExtIffType (extThmName : Name) : MetaM Expr := withLCtx {} {} do
     let some (_, x, y) := ty.eq? | failNotEq
     let some xIdx := args.findIdx? (· == x) | failNotEq
     let some yIdx := args.findIdx? (· == y) | failNotEq
-    unless xIdx == yIdx + 1 || xIdx + 1 == yIdx do
+    unless xIdx + 1 == yIdx do
       throwError "expecting {x} and {y} to be consecutive arguments"
-    let startIdx := max xIdx yIdx + 1
+    let startIdx := yIdx + 1
     let toRevert := args[startIdx:].toArray
     let fvars ← toRevert.foldlM (init := {}) (fun st e => return collectFVars st (← inferType e))
     for fvar in toRevert do
       unless ← Meta.isProof fvar do
-        throwError "argument {fvar} is not a proof, which is not supported"
+        throwError "argument {fvar} is not a proof, which is not supported for arguments after {x} and {y}"
       if fvars.fvarSet.contains fvar.fvarId! then
-        throwError "argument {fvar} is depended upon, which is not supported"
+        throwError "argument {fvar} is depended upon, which is not supported for arguments after {x} and {y}"
     let conj := mkAndN (← toRevert.mapM (inferType ·)).toList
     -- Make everything implicit except for inst implicits
     let mut newBis := #[]
@@ -104,27 +104,31 @@ def realizeExtTheorem (structName : Name) (flat : Bool) : Elab.Command.CommandEl
     throwError "'{structName}' is not a structure"
   let extName := structName.mkStr "ext"
   unless (← getEnv).contains extName do
-    Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extName do
-      let type ← mkExtType structName flat
-      let pf ← withSynthesize do
-        let indVal ← getConstInfoInduct structName
-        let params := Array.mkArray indVal.numParams (← `(_))
-        Elab.Term.elabTermEnsuringType (expectedType? := type) (implicitLambda := false)
-          -- introduce the params, do cases on 'x' and 'y', and then substitute each equation
-          (← `(by intro $params* {..} {..}; intros; subst_eqs; rfl))
-      let pf ← instantiateMVars pf
-      if pf.hasMVar then throwError "(internal error) synthesized ext proof contains metavariables{indentD pf}"
-      let info ← getConstInfo structName
-      addDecl <| Declaration.thmDecl {
-        name := extName
-        type
-        value := pf
-        levelParams := info.levelParams
-      }
-      modifyEnv fun env => addProtected env extName
-      Lean.addDeclarationRanges extName {
-        range := ← getDeclarationRange (← getRef)
-        selectionRange := ← getDeclarationRange (← getRef) }
+    try
+      Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extName do
+        let type ← mkExtType structName flat
+        let pf ← withSynthesize do
+          let indVal ← getConstInfoInduct structName
+          let params := Array.mkArray indVal.numParams (← `(_))
+          Elab.Term.elabTermEnsuringType (expectedType? := type) (implicitLambda := false)
+            -- introduce the params, do cases on 'x' and 'y', and then substitute each equation
+            (← `(by intro $params* {..} {..}; intros; subst_eqs; rfl))
+        let pf ← instantiateMVars pf
+        if pf.hasMVar then throwError "(internal error) synthesized ext proof contains metavariables{indentD pf}"
+        let info ← getConstInfo structName
+        addDecl <| Declaration.thmDecl {
+          name := extName
+          type
+          value := pf
+          levelParams := info.levelParams
+        }
+        modifyEnv fun env => addProtected env extName
+        Lean.addDeclarationRanges extName {
+          range := ← getDeclarationRange (← getRef)
+          selectionRange := ← getDeclarationRange (← getRef) }
+    catch e =>
+      throwError m!"\
+        Failed to generate an 'ext' theorem for '{MessageData.ofConstName structName}': {e.toMessageData}"
   return extName
 
 /--
@@ -138,29 +142,35 @@ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do
     | .str n s => .str n (s ++ "_iff")
     | _ => .str extName "ext_iff"
   unless (← getEnv).contains extIffName do
-    let info ← getConstInfo extName
-    Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extIffName do
-      let type ← mkExtIffType extName
-      let pf ← withSynthesize do
-        Elab.Term.elabTermEnsuringType (expectedType? := type) <| ← `(by
-          intros
-          refine ⟨?_, ?_⟩
-          · intro h; cases h; and_intros <;> (intros; first | rfl | simp | fail "Failed to prove converse of ext theorem")
-          · intro; (repeat cases ‹_ ∧ _›); apply $(mkCIdent extName) <;> assumption)
-      let pf ← instantiateMVars pf
-      if pf.hasMVar then throwError "(internal error) synthesized ext_iff proof contains metavariables{indentD pf}"
-      addDecl <| Declaration.thmDecl {
-        name := extIffName
-        type
-        value := pf
-        levelParams := info.levelParams
-      }
-      -- Only declarations in a namespace can be protected:
-      unless extIffName.isAtomic do
-        modifyEnv fun env => addProtected env extIffName
-      Lean.addDeclarationRanges extIffName {
-        range := ← getDeclarationRange (← getRef)
-        selectionRange := ← getDeclarationRange (← getRef) }
+    try
+      let info ← getConstInfo extName
+      Elab.Command.liftTermElabM <| withoutErrToSorry <| withDeclName extIffName do
+        let type ← mkExtIffType extName
+        let pf ← withSynthesize do
+          Elab.Term.elabTermEnsuringType (expectedType? := type) <| ← `(by
+            intros
+            refine ⟨?_, ?_⟩
+            · intro h; cases h; and_intros <;> (intros; first | rfl | simp | fail "Failed to prove converse of ext theorem")
+            · intro; (repeat cases ‹_ ∧ _›); apply $(mkCIdent extName) <;> assumption)
+        let pf ← instantiateMVars pf
+        if pf.hasMVar then throwError "(internal error) synthesized ext_iff proof contains metavariables{indentD pf}"
+        addDecl <| Declaration.thmDecl {
+          name := extIffName
+          type
+          value := pf
+          levelParams := info.levelParams
+        }
+        -- Only declarations in a namespace can be protected:
+        unless extIffName.isAtomic do
+          modifyEnv fun env => addProtected env extIffName
+        Lean.addDeclarationRanges extIffName {
+          range := ← getDeclarationRange (← getRef)
+          selectionRange := ← getDeclarationRange (← getRef) }
+    catch e =>
+      throwError m!"\
+        Failed to generate an 'ext_iff' theorem from '{MessageData.ofConstName extName}': {e.toMessageData}\n\
+        \n\
+        Try '@[ext (iff := false)]' to prevent generating an 'ext_iff' theorem."
   return extIffName
 
 

tests/lean/run/ext.lean

@@ -138,3 +138,35 @@ attribute [local ext] Subsingleton.elim
 /-- info: Subsingleton.elim_iff.{u} {α : Sort u} [h : Subsingleton α] {a b : α} : a = b ↔ True -/
 #guard_msgs in #check Subsingleton.elim_iff
 end
+
+
+/-!
+More informative error (issue #4758)
+-/
+
+/--
+warning: declaration uses 'sorry'
+---
+error: Failed to generate an 'ext_iff' theorem from 'weird_prod_ext': argument f is not a proof, which is not supported for arguments after p and q
+
+Try '@[ext (iff := false)]' to prevent generating an 'ext_iff' theorem.
+-/
+#guard_msgs in
+@[ext]
+theorem weird_prod_ext (p q : α × β)
+    (f : α → α') (g : β → β') -- (hf : Function.Injective f) (hg : Function.Injective g)
+    (h : f p.1 = f q.1) (h' : g p.2 = g q.2) :
+  p = q := sorry
+
+/--
+error: Failed to generate an 'ext_iff' theorem from 'ext'': argument h1 is depended upon, which is not supported for arguments after p and q
+
+Try '@[ext (iff := false)]' to prevent generating an 'ext_iff' theorem.
+-/
+#guard_msgs in
+@[ext]
+theorem Sigma.ext' {β : α → Type _} (p q : (i : α) × β i)
+    (h1 : p.1 = q.1)
+    (h2 : h1 ▸ p.2 = q.2) :
+    p = q := by
+  cases p; cases q; cases h1; cases h2; rfl