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

@@ -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

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

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

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