fix: to do unfold matcher applications that cannot be reduced when smartUnfolding is true

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/How.20to.20WHNF.20without.20exposing.20recursors.3F

src/Lean/Meta/WHNF.lean

@@ -429,8 +429,7 @@ mutual
             else
               return none
           if smartUnfolding.get (← getOptions) then
-            let fAuxInfo? ← getConstNoEx? (mkSmartUnfoldingNameFor fInfo.name)
-            match fAuxInfo? with
+            match (← getConstNoEx? (mkSmartUnfoldingNameFor fInfo.name)) with
             | some fAuxInfo@(ConstantInfo.defnInfo _) =>
               deltaBetaDefinition fAuxInfo fLvls e.getAppRevArgs (fun _ => pure none) fun e₁ => do
                 let e₂ ← whnfUntilIdRhs e₁
@@ -438,7 +437,12 @@ mutual
                   return some (extractIdRhs e₂)
                 else
                   return none
-            | _ => unfoldDefault ()
+            | _ =>
+              if (← getMatcherInfo? fInfo.name).isSome then
+                -- Recall that `whnfCore` tries to reduce "matcher" applications.
+                return none
+              else
+                unfoldDefault ()
           else
             unfoldDefault ()
     | Expr.const declName lvls _ => do

tests/lean/run/match1.lean

@@ -6,16 +6,18 @@ def checkWithMkMatcherInput (matcher : Lean.Name) : Lean.MetaM Unit :=
   let origMatcher ← Lean.getConstInfo matcher
   if not <| input.matcherName == matcher then
     throwError "matcher name not reconstructed correctly: {matcher} ≟ {input.matcherName}"
-  
+
   let lCtx ← Lean.getLCtx
   let fvars ← Lean.collectFVars {} res.matcher
   let closure ← Lean.Meta.Closure.mkLambda (fvars.fvarSet.toList.toArray.map lCtx.get!) res.matcher
 
-  let origTy := origMatcher.value! 
+  let origTy := origMatcher.value!
   let newTy ← closure
   if not <| ←Lean.Meta.isDefEq origTy newTy then
     throwError "matcher {matcher} does not round-trip correctly:\n{origTy} ≟ {newTy}"
-  
+
+set_option smartUnfolding false
+
 def f (xs : List Nat) : List Bool :=
 xs.map fun
   | 0 => true

tests/lean/smartUnfoldingMatch.lean

@@ -0,0 +1,12 @@
+import Lean
+
+open Lean Meta Elab Term in
+elab "whnf%" t:term : term <= expectedType => do
+  let r ← whnf (← elabTerm t expectedType)
+  trace[Meta.debug] "r: {r}"
+  return r
+
+constant x : Option Nat := some 42
+
+set_option trace.Meta.debug true
+#eval whnf% x.getD 0

tests/lean/smartUnfoldingMatch.lean.expected.out

@@ -0,0 +1,4 @@
+42
+[Meta.debug] r: match x, 0 with 
+  | some x, x_1 => x
+  | none, e => e