From bbc196eeb79db463b03a884639c72b1c8f76f7de Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 17 Jun 2022 17:36:41 -0700
Subject: [PATCH] fix: make sure `WF/Fix.lean` tolerates `MatcherApp.addArg?`
 failures

see #1228
---
 src/Lean/Elab/PreDefinition/WF/Fix.lean |  5 +--
 src/Lean/Meta/Match/Match.lean          |  7 ++++
 tests/lean/run/1228.lean                | 46 +++++++++++++++++++++++++
 3 files changed, 56 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/1228.lean

diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean
index ac53946a0c..7cb5702ca6 100644
--- a/src/Lean/Elab/PreDefinition/WF/Fix.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean
@@ -83,8 +83,7 @@ where
       | some matcherApp =>
         if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then
           processApp F e
-        else
-          let matcherApp ← mapError (matcherApp.addArg F) (fun msg => "failed to add functional argument to 'matcher' application" ++ indentD msg)
+        else if let some matcherApp ← matcherApp.addArg? F then
           if !(← Structural.refinedArgType matcherApp F) then
             processApp F e
           else
@@ -95,6 +94,8 @@ where
                 let FAlt := xs[numParams - 1]
                 mkLambdaFVars xs (← loop FAlt altBody)
             return { matcherApp with alts := altsNew, discrs := (← matcherApp.discrs.mapM (loop F)) }.toExpr
+        else
+          processApp F e
       | none =>
       match (← toCasesOnApp? e) with
       | some casesOnApp =>
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index 129127f959..f694488a2f 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -982,6 +982,13 @@ def MatcherApp.addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp :=
       remaining     := #[e] ++ matcherApp.remaining
     }
 
+/-- Similar `MatcherApp.addArg?`, but returns `none` on failure. -/
+def MatcherApp.addArg? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option MatcherApp) :=
+  try
+    return some (← matcherApp.addArg e)
+  catch _ =>
+    return none
+
 builtin_initialize
   registerTraceClass `Meta.Match.match
   registerTraceClass `Meta.Match.debug
diff --git a/tests/lean/run/1228.lean b/tests/lean/run/1228.lean
new file mode 100644
index 0000000000..45dd064b49
--- /dev/null
+++ b/tests/lean/run/1228.lean
@@ -0,0 +1,46 @@
+inductive Foo (n : Nat) : Type
+| foo (t: Foo n): Foo n
+
+namespace Foo
+  inductive Bar: Foo n → Prop
+
+  theorem ex₁ {s: Foo n} (H: s.Bar): True := by
+    cases h₁ : s
+    case foo s' =>
+      cases h₂ : n; sorry
+      have: Bar s' := sorry
+      exact ex₁ this
+  termination_by _ => sizeOf s
+
+  theorem ex₂
+    {s: Foo n}
+    (H: s.Bar):
+    True := by
+    generalize hs': s = s'
+    match s' with
+    | foo s' =>
+      have: Bar s' := sorry
+      have hterm: sizeOf s' < sizeOf s := by simp_all_arith
+      exact ex₂ this
+  termination_by _ => sizeOf s
+
+  theorem ex₃ {s: Foo n} (H: s.Bar): True := by
+    cases h₁ : s
+    case foo s' =>
+      match n with
+      | 0 => sorry
+      | _ =>
+        have: Bar s' := sorry
+        exact ex₃ this
+  termination_by _ => sizeOf s
+
+  -- it works
+  theorem ex₄ {s: Foo n} (H: s.Bar): True := by
+    match s with
+    | foo s' =>
+    match n with
+    | 0 => sorry
+    | _ =>
+      have: Bar s' := sorry
+      exact ex₄ this
+  termination_by _ => sizeOf s