Field notation in `where` decl complains about metavariable when omitting an autoParam in main declaration

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 my situation, field notation complains about the base type being a metavariable even though Lean seems to be perfectly able to show me its fully determined type in the Lean Infoview. This is somehow related to an autoParam I'm using.

Steps to Reproduce

Lean Web:

structure X (m : Type u → Type w) (β : Type v) where
  val : β

def f {α : Type u} (l : List α) (m : Type u → Type w := by exact Id) [Pure m] :
    X m α := sorry

/--
error: invalid field notation, type is not of the form (C ...) where C is a constant
  it
has type
  ?m.425
-/
#guard_msgs in
def mwe (l : List Nat) : Nat :=
  go (f l) 0 -- Try explicitly passing `Id`
where
  go it acc := it.val -- fails here

Expected behavior: [Clear and concise description of what you expect to happen]

Lean should be able to infer that it is of type X Id Nat and use this information in go to successfully elaborate the do notation.

Actual behavior: [Clear and concise description of what actually happens]

If I put my cursor right before it in the last line, the environment seems right:

l : List Nat
it : X Id Nat
acc : Nat
⊢ Nat

However, as seen in the #guard_msgs comment above, the field notation elaborator seems not to know about it's type (yet?).

I don't know a lot about the elaborator's internals but this looks as if the field notation elaborator should have deferred itself so that it's type can be determined first.

If we explicitly pass the autoParam m := Id to `f``, the problem disappears.

Versions

Lean 4.20.0-nightly-2025-04-14
Target: x86_64-unknown-linux-gnu

Impact

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

Start by running the minimal reproducer in Lean Web or against the reported nightly version, comparing the failing call with the variant that explicitly passes m := Id. Inspect the field-notation elaborator and its interaction with the omitted autoParam; done means the where declaration accepts it.val without requiring the explicit parameter.