From ec39de8caed5f86604cec2b4b788d917aaebbe34 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Tue, 23 Jan 2024 09:02:05 +0000
Subject: [PATCH] fix: allow generalization in let (#3060)

As suggested by @kmill, removing an unnecessary `let` (possibly only
there in the first place for copy/paste reasons) seems to fix the
included test.

This makes `~q()` matching in quote4 noticeably more useful in things
like `norm_num` (as it fixes
https://github.com/leanprover-community/quote4/issues/29)

It also makes a quote4 bug slightly more visible
(https://github.com/leanprover-community/quote4/issues/30), but the bug
there already existed anyway, and isn't caused by this patch.

Fixes #3065
---
 src/Lean/Elab/Do.lean         |  2 +-
 tests/lean/run/doLetElse.lean | 20 ++++++++++++++++----
 2 files changed, 17 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 85392b5d38d8..a81dd14afb5c 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -1368,7 +1368,7 @@ mutual
     else
       pure doElems.toArray
     let contSeq := mkDoSeq contSeq
-    let auxDo ← `(do let __discr := $val; match __discr with | $pattern:term => $contSeq | _ => $elseSeq)
+    let auxDo ← `(do match $val:term with | $pattern:term => $contSeq | _ => $elseSeq)
     doSeqToCode <| getDoSeqElems (getDoSeq auxDo)
 
   /-- Generate `CodeBlock` for `doReassignArrow; doElems`
diff --git a/tests/lean/run/doLetElse.lean b/tests/lean/run/doLetElse.lean
index 24435474c14e..e65b084f99ae 100644
--- a/tests/lean/run/doLetElse.lean
+++ b/tests/lean/run/doLetElse.lean
@@ -3,10 +3,22 @@ def foo (x? : Option Nat) : IO Nat := do
   IO.println s!"x: {x}"
   return x
 
-def test (input : Option Nat) (expected : Nat) : IO Unit := do
+def testFoo (input : Option Nat) (expected : Nat) : IO Unit := do
   assert! (← foo input) == expected
 
+#eval testFoo (some 10) 10
+#eval testFoo none 0
+#eval testFoo (some 1) 1
 
-#eval test (some 10) 10
-#eval test none 0
-#eval test (some 1) 1
+def bar (x : Nat) : IO (Fin (x + 1)) := do
+  let 2 := x | return 0
+  -- the pattern match performed a substitution
+  let y : Fin 3 := ⟨1, by decide⟩
+  return y
+
+def testBar (x : Nat) (expected : Fin (x + 1)) : IO Unit := do
+  assert! (← bar x) == expected
+
+#eval testBar 1 0
+#eval testBar 2 1
+#eval testBar 3 0