From 37450d47e2cee9b81c352ff4a4090c0be945ba17 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 4 Mar 2024 15:56:00 -0800
Subject: [PATCH] fix: bug at `elimOptParam` (#3595)

`let_expr` uses `cleanupAnnotations` which consumes `optParam` type
annotations.

cc @nomeata
---
 src/Lean/Meta/Injective.lean     |  6 ++++--
 tests/lean/run/elimOptParam.lean | 14 ++++++++++++++
 2 files changed, 18 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/elimOptParam.lean

diff --git a/src/Lean/Meta/Injective.lean b/src/Lean/Meta/Injective.lean
index c1d1aaa82f..95e4dad4b7 100644
--- a/src/Lean/Meta/Injective.lean
+++ b/src/Lean/Meta/Injective.lean
@@ -26,8 +26,10 @@ private def mkAnd? (args : Array Expr) : Option Expr := Id.run do
 
 def elimOptParam (type : Expr) : CoreM Expr := do
   Core.transform type fun e =>
-    let_expr optParam _ a := e | return .continue
-    return TransformStep.visit a
+    if e.isAppOfArity ``optParam 2 then
+      return TransformStep.visit (e.getArg! 0)
+    else
+      return .continue
 
 private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useEq : Bool) : MetaM (Option Expr) := do
   let us := ctorVal.levelParams.map mkLevelParam
diff --git a/tests/lean/run/elimOptParam.lean b/tests/lean/run/elimOptParam.lean
new file mode 100644
index 0000000000..b0a99ae657
--- /dev/null
+++ b/tests/lean/run/elimOptParam.lean
@@ -0,0 +1,14 @@
+import Lean
+
+def f (x := 0) (y := 1) : Nat :=
+  x + y
+
+open Lean Meta
+
+/--
+info: Nat → Nat → Nat
+-/
+#guard_msgs in
+run_meta do
+  let info ← getConstInfo ``f
+  logInfo (← elimOptParam info.type)