From f58afaaa433a877e845c76bd3dcffbba6435709d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 10 May 2022 06:50:53 -0700
Subject: [PATCH] fix: make sure `let _ := val` and `let _ : type := val` are
 treated at `letIdDecl`

closes #1114
---
 src/Lean/Elab/Binders.lean    | 22 ++++++++++++++--------
 tests/lean/run/let_Issue.lean |  7 +++++++
 2 files changed, 21 insertions(+), 8 deletions(-)
 create mode 100644 tests/lean/run/let_Issue.lean

diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 01da7e93c6..c157d456d4 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -666,14 +666,20 @@ def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : B
     let pat     := letDecl[0]
     let optType := letDecl[2]
     let val     := letDecl[4]
-    -- We are currently treating `let_fun` and `let` the same way when patterns are used.
-    let stxNew ←
-      if optType.isNone then
-        `(match $val:term with | $pat => $body)
-      else
-        let type := optType[0][1]
-        `(match ($val:term : $type) with | $pat => $body)
-    withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
+    if pat.getKind == ``Parser.Term.hole then
+      -- `let _ := ...` should not be treated at a `letIdDecl`
+      let id   := mkIdentFrom pat `_
+      let type := expandOptType id optType
+      elabLetDeclAux id #[] type val body expectedType? useLetExpr elabBodyFirst usedLetOnly
+    else
+      -- We are currently treating `let_fun` and `let` the same way when patterns are used.
+      let stxNew ←
+        if optType.isNone then
+          `(match $val:term with | $pat => $body)
+        else
+          let type := optType[0][1]
+          `(match ($val:term : $type) with | $pat => $body)
+      withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
   else if letDecl.getKind == ``Lean.Parser.Term.letEqnsDecl then
     let letDeclIdNew ← liftMacroM <| expandLetEqnsDecl letDecl
     let declNew := stx[1].setArg 0 letDeclIdNew
diff --git a/tests/lean/run/let_Issue.lean b/tests/lean/run/let_Issue.lean
new file mode 100644
index 0000000000..acc0291c6e
--- /dev/null
+++ b/tests/lean/run/let_Issue.lean
@@ -0,0 +1,7 @@
+class C (α : Type)
+
+instance : C (Fin (n+1)) := ⟨⟩
+
+instance : C (Fin UInt64.size) :=
+  let _ : C (Fin UInt64.size) := inferInstanceAs (C (Fin (_+1)))
+  inferInstance