From 32dd3c6b29254d05697c85cbc54a05546c1a4f14 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 12 Feb 2022 07:54:48 -0800
Subject: [PATCH] feat: use at least default transparency at `toCtorWhenK`

Improves the effectiveness of `simp` when reducing `match`-expr.
---
 src/Lean/Meta/WHNF.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 966ca2c47a..a8c23bec3e 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -99,7 +99,10 @@ private def toCtorWhenK (recVal : RecursorVal) (major : Expr) : MetaM Expr := do
   else do
     let (some newCtorApp) ← mkNullaryCtor majorType recVal.numParams | pure major
     let newType ← inferType newCtorApp
-    if (← isDefEq majorType newType) then
+    /- TODO: check whether changing reducibility to default hurts performance here.
+       We do that to make sure auxiliary `Eq.rec` introduced by the `match`-compiler
+       are reduced even when `TransparencyMode.reducible` (like in `simp`) -/
+    if (← withAtLeastTransparency TransparencyMode.default <| isDefEq majorType newType) then
       return newCtorApp
     else
       return major