let/ else pattern matching does not substitute in expected type

[eric-wieser]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

let 3 := n | failure does not substitute n with 3 in the target type, even though equivalent spellings do.

Context

Zulip thread

This impacts leanprover-community/quote4, which transpiles to this type of let statement.

Steps to Reproduce

The following does not work:

example (n : Nat) (i : Fin n) : Option (Fin 3) := do
  let 3 := n | failure
  return i -- fails, pattern match did not substitute in hypothesis

example (n : Nat) (i : Fin 3) : Option (Fin n) := do
  let 3 := n | failure
  return i -- fails, pattern match did not substitute in goal

but the corresponding match does:

example (n : Nat) (i : Fin n) : Option (Fin 3) := do
  match n with
  | 3 => return i -- ok
  | _ => failure

example (n : Nat) (i : Fin 3) : Option (Fin n) := do
  match n with
  | 3 => return i -- ok
  | _ => failure

as does if let

example (n : Nat) (i : Fin n) : Option (Fin 3) := do
  if let 3 := n then
    return i
  else
    failure

example (n : Nat) (i : Fin 3) : Option (Fin n) := do
  if let 3 := n then
    return i
  else
    failure

Expected behavior: All three examples should behave identically

Actual behavior: The first one does not type-check

Versions

leanprover/lean4:v4.4.0-rc1

Additional Information

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.