From 8a302e6135bc1b0f1f2901702664c56cd424ebc2 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 22 Mar 2023 11:17:19 +0100
Subject: [PATCH] fix: `match` discriminant reduction should not unfold
 irreducible defs

---
 src/Lean/Meta/WHNF.lean           |  6 +++---
 tests/lean/2161.lean              | 22 ++++++++++++++++++++++
 tests/lean/2161.lean.expected.out |  6 ++++++
 3 files changed, 31 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/2161.lean
 create mode 100644 tests/lean/2161.lean.expected.out

diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index e5db1e2e04..d28a9b5f42 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -368,7 +368,7 @@ inductive ReduceMatcherResult where
   should reduce in any transparency mode.
   Thus, we define a custom `canUnfoldAtMatcher` predicate for `whnfMatcher`.
 
-  This solution is not very modular because modications at the `match` compiler require changes here.
+  This solution is not very modular because modifications at the `match` compiler require changes here.
   We claim this is defensible because it is reducing the auxiliary declaration defined by the `match` compiler.
 
   Alternative solution: tactics that use `TransparencyMode.reducible` should rely on the equations we generated for match-expressions.
@@ -378,7 +378,7 @@ inductive ReduceMatcherResult where
 def canUnfoldAtMatcher (cfg : Config) (info : ConstantInfo) : CoreM Bool := do
   match cfg.transparency with
   | TransparencyMode.all     => return true
-  | TransparencyMode.default => return true
+  | TransparencyMode.default => return !(← isIrreducible info.name)
   | _ =>
     if (← isReducible info.name) || isGlobalInstance (← getEnv) info.name then
       return true
@@ -402,7 +402,7 @@ def canUnfoldAtMatcher (cfg : Config) (info : ConstantInfo) : CoreM Bool := do
 
 private def whnfMatcher (e : Expr) : MetaM Expr := do
   /- When reducing `match` expressions, if the reducibility setting is at `TransparencyMode.reducible`,
-     we increase it to `TransparencyMode.instance`. We use the `TransparencyMode.reducible` in many places (e.g., `simp`),
+     we increase it to `TransparencyMode.instances`. We use the `TransparencyMode.reducible` in many places (e.g., `simp`),
      and this setting prevents us from reducing `match` expressions where the discriminants are terms such as `OfNat.ofNat α n inst`.
      For example, `simp [Int.div]` will not unfold the application `Int.div 2 1` occuring in the target.
 
diff --git a/tests/lean/2161.lean b/tests/lean/2161.lean
new file mode 100644
index 0000000000..7330d12a61
--- /dev/null
+++ b/tests/lean/2161.lean
@@ -0,0 +1,22 @@
+structure Foo where num : Nat deriving DecidableEq
+
+namespace Foo
+
+instance : OfNat Foo n := ⟨⟨n⟩⟩
+
+/-! # Example 1 -/
+
+@[irreducible] def mul (a b : Foo) : Foo :=
+  let d := Nat.gcd a.num 1
+  ⟨(a.num.div d) * (b.num.div d)⟩
+
+-- should fail fast; exact heartbeat count at time of writing is 31
+set_option maxHeartbeats 310
+example : ((Foo.mul 4 1).mul 1).mul 1 = 4 := by decide
+
+/-! # Example 2 -/
+
+@[irreducible] def add (a b : Foo) : Foo := ⟨a.num * b.num⟩
+
+-- should not succeed (and fail fast); exact heartbeat count at time of writing is 21
+example : ((Foo.add 4 1).add 1).add 1 = 4 := by decide
diff --git a/tests/lean/2161.lean.expected.out b/tests/lean/2161.lean.expected.out
new file mode 100644
index 0000000000..aa64fd3a49
--- /dev/null
+++ b/tests/lean/2161.lean.expected.out
@@ -0,0 +1,6 @@
+2161.lean:15:48-15:54: error: failed to reduce to 'true'
+  Decidable.rec (fun h => (fun x => false) h) (fun h => (fun x => true) h)
+    (instDecidableEqFoo (mul (mul (mul 4 1) 1) 1) 4)
+2161.lean:22:48-22:54: error: failed to reduce to 'true'
+  Decidable.rec (fun h => (fun x => false) h) (fun h => (fun x => true) h)
+    (instDecidableEqFoo (add (add (add 4 1) 1) 1) 4)