From 2832442e7afad582175def1b40d1828342ce3488 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 6 Jun 2022 13:47:00 -0700
Subject: [PATCH] fix: unfold declarations tagged with `[matchPattern]` at
 `reduceMatcher?` even if transparency setting is not the default one

see #1193

It fixes one of the issues exposed at the issue above.
---
 src/Lean/Meta/WHNF.lean              |  7 +++++--
 tests/lean/run/1193a.lean            | 17 +++++++++++++++++
 tests/lean/unfold1.lean              |  3 +--
 tests/lean/unfold1.lean.expected.out |  5 +----
 4 files changed, 24 insertions(+), 8 deletions(-)
 create mode 100644 tests/lean/run/1193a.lean

diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index ee800a0a74..c481b44668 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -11,6 +11,7 @@ import Lean.Util.Recognizers
 import Lean.Meta.Basic
 import Lean.Meta.GetConst
 import Lean.Meta.Match.MatcherInfo
+import Lean.Meta.Match.MatchPatternAttr
 
 namespace Lean.Meta
 
@@ -359,13 +360,15 @@ inductive ReduceMatcherResult where
   This solution is also not perfect because the match-expression above will not reduce during type checking when we are not using
   `TransparencyMode.default` or `TransparencyMode.all`.
 -/
-private def canUnfoldAtMatcher (cfg : Config) (info : ConstantInfo) : CoreM Bool := do
+def canUnfoldAtMatcher (cfg : Config) (info : ConstantInfo) : CoreM Bool := do
   match cfg.transparency with
   | TransparencyMode.all     => return true
   | TransparencyMode.default => return true
-  | m =>
+  | _ =>
     if (← isReducible info.name) || isGlobalInstance (← getEnv) info.name then
       return true
+    else if hasMatchPatternAttribute (← getEnv) info.name then
+      return true
     else
       return info.name == ``ite
        || info.name == ``dite
diff --git a/tests/lean/run/1193a.lean b/tests/lean/run/1193a.lean
new file mode 100644
index 0000000000..4c1171444d
--- /dev/null
+++ b/tests/lean/run/1193a.lean
@@ -0,0 +1,17 @@
+inductive Foo (n : Nat) : Type
+| nil            : Foo n
+| cons (s: Foo n): Foo n
+
+namespace Foo
+
+@[simp] def bar: {n: Nat} → Foo n → Foo n → Bool
+  | n+1, cons a, cons b => bar a b
+  | _, _, _ => true
+
+example: bar (n:=n+1) nil nil = true := by
+  unfold bar
+  simp
+
+example: bar (n:= Nat.succ n) nil nil = true := by
+  unfold bar
+  simp
diff --git a/tests/lean/unfold1.lean b/tests/lean/unfold1.lean
index 8c5d4aa28a..702ee1ee88 100644
--- a/tests/lean/unfold1.lean
+++ b/tests/lean/unfold1.lean
@@ -19,9 +19,8 @@ theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
     simp
     unfold isOdd
     trace_state
-    rw [Nat.add_succ]
     simp
     exact ih
 
 theorem isEven_succ_succ (x : Nat) : isEven (x + 2) = isEven x := by
-  conv => lhs; unfold isEven; rw [Nat.add_succ]; simp; unfold isOdd; rw [Nat.add_succ]; simp
+  conv => lhs; unfold isEven; simp; unfold isOdd; simp
diff --git a/tests/lean/unfold1.lean.expected.out b/tests/lean/unfold1.lean.expected.out
index 64d497d269..5b6b560a4a 100644
--- a/tests/lean/unfold1.lean.expected.out
+++ b/tests/lean/unfold1.lean.expected.out
@@ -8,7 +8,4 @@ ih : isEven (2 * x) = true
 case succ
 x : Nat
 ih : isEven (2 * x) = true
-⊢ (match 2 * x + 1 with
-    | 0 => false
-    | Nat.succ n => isEven n) =
-    true
+⊢ isEven (Nat.add (2 * x) 0) = true