Inferred type of a variable not propagated to earlier usages

[mik-jozef]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

In the following code

structure PairNat where
  a: Nat
  b: Nat

def forceType (c: PairNat → Prop) := c

def foo :=
  let bar := fun ⟨a, b⟩ => a = b

  let ftBefore := forceType bar
  let inBarToEq a b: bar ⟨a, b⟩ → a = b := id
  let ftAfter := forceType bar

  0

Lean is able to infer the type of bar from its usage by the function forceType.
Lean also uses this inferred type to make sense of the pattern matching in the definition
of bar – if the block of three variables is commented out, we get this error:

invalid constructor ⟨...⟩, expected type must be an inductive type 
  ?m.339

Even though the inferred type is used where bar is defined, it is not used where
bar is used – if the declaration of ftBefore is commented out, we get the above
error at the definition of inBarToEq (while the definition of bar itself is still error-free).

Strangely, when one hovers the mouse over the bar in the type of inBarToEq,
the type is still displayed correctly:

Also, when the caret is over the usage of bar, the context contains the correct type:

bar: PairNat → Prop := fun x =>
  match x with
  | { a := a, b := b } => a = b
ab: ?m.416
⊢ Prop

Explicitly typing the variable is an abvious and quick workaround. I realize this is
a very minor issue once one knows what's happening, but from the usage perspective,
it was very confusing before I did 😅

Steps to Reproduce

0. Paste the above code to https://live.lean-lang.org/
1. Comment out the line defining the variable ftBefore
2. Observe the error on the line below.

Expected behavior: There is no error.

Versions

Lean version: 4.11.0-rc2 and 4.12.0-nightly-2024-08-14
OS: Ubuntu 22.04.4 LTS;

Impact

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

[Kha]

This unfortunately is a consequence of another desirable change, #4096. While we would love to make Lean as independent from elaboration ordering as possible, in practice this is unfortunately not always achievable.