From 02b206af9b857a2bbc796394aec14fe192ab59d7 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 18 Apr 2025 11:23:51 +0200
Subject: [PATCH] fix: mkAppM to typecheck at .default transparency (#7957)

This PR ensures that `mkAppM` can be used to construct terms that are
only type-correct at at default transparency, even if we are in
`withReducible` (e.g. in simp), so that simp does not stumble over
simplifying `let` expression with simplifiable type.reliable.

Here is a reproducer of the issue this solves:
```
example (a b : Nat) (h : a = b):
  (let _ : id Bool := true; a) = (let _ : Bool := true; b) := by
  simp -zeta -zetaDelta [h]
```

This fixes #7826.
---
 src/Lean/Meta/AppBuilder.lean  |  2 +-
 tests/lean/run/issue7826.lean  | 39 ++++++++++++++++++++++++++++++++++
 tests/lean/run/issue7826a.lean |  3 +++
 3 files changed, 43 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/issue7826.lean
 create mode 100644 tests/lean/run/issue7826a.lean

diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index bb88990bfe..aacbe84ad1 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -304,7 +304,7 @@ private partial def mkAppMArgs (f : Expr) (fType : Expr) (xs : Array Expr) : Met
         | _ =>
           let x := xs[i]
           let xType ← inferType x
-          if (← isDefEq d xType) then
+          if (← withAtLeastTransparency .default (isDefEq d xType)) then
             loop b (i+1) j (args.push x) instMVars
           else
             throwAppTypeMismatch (mkAppN f args) x
diff --git a/tests/lean/run/issue7826.lean b/tests/lean/run/issue7826.lean
new file mode 100644
index 0000000000..2e149237ea
--- /dev/null
+++ b/tests/lean/run/issue7826.lean
@@ -0,0 +1,39 @@
+axiom SparseSet : Nat → Type
+
+def SparseSet.insert {n} (set : SparseSet n) (v : Fin n) : SparseSet n := sorry
+
+inductive Node where
+  | epsilon (next : Nat)
+
+structure NFA where
+  nodes : Array Node
+
+def NFA.get (nfa : NFA) (i : Nat) (h : i < nfa.nodes.size) : Node :=
+  nfa.nodes[i]
+
+structure Strategy' where
+  T : Type
+
+-- set_option trace.Meta.appBuilder true
+-- set_option trace.Meta.isDefEq true
+
+def εClosure (σ : Strategy') (nfa : NFA) (states : SparseSet nfa.nodes.size) (stack : List (Fin nfa.nodes.size)) :
+  -- REPRO: using `σ.T` is necessary to reproduce.
+  Option σ.T :=
+  match stack with
+  | [] => .none
+  | state :: stack' =>
+    -- REPRO: removing this `if` fixes the error.
+    if true then
+      εClosure σ nfa states stack'
+    else
+      -- REPRO: this insert is necessary to reproduce.
+      let states' := states.insert state
+      match nfa.get state state.isLt with
+      | .epsilon state' =>
+        -- REPRO: this line is also necessary to reproduce.
+        have isLt : state' < nfa.nodes.size := sorry
+        sorry
+-- REPRO: using well-founded recursion is necessary to reproduce.
+-- NOTE: the original code uses well-founded recursion to take visited states (`states`) into account.
+termination_by /-structural-/ stack
diff --git a/tests/lean/run/issue7826a.lean b/tests/lean/run/issue7826a.lean
new file mode 100644
index 0000000000..935a7b71ba
--- /dev/null
+++ b/tests/lean/run/issue7826a.lean
@@ -0,0 +1,3 @@
+example (a b : Nat) (h : a = b):
+  (let _ : id Bool := true; a) = (let _ : Bool := true; b) := by
+  simp -zeta -zetaDelta [h]