Hover shows resolved type but error shows unresolved metavariable

Prerequisites

• 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

Hover shows resolved type but error message uses unresolved metavariable for outParam with dot-notation.

Steps to Reproduce

live.lean-lang.org link

inductive Foo
| x
| y

-- A typeclass with an `outParam`
class MyClass (T : Type) (U : outParam Type) where
  getType : T → U → Type

-- An instance associating `List Foo` to `Foo`
instance : MyClass (List Foo) Foo where
  getType
    | _, .x => Nat
    | _, .y => String

-- A definition with an `U` `outParam`
def bar {T : Type} {U : outParam Type} [MyClass T U]
  (t : T) (u : U) : MyClass.getType t u := sorry

def test2 (t : List Foo) : Nat :=
  let res := bar t .x  -- dot-notation for the `outParam` argument
  res

Expected behavior:
No error, .x should be resolved to Foo.x, and res should have the type MyClass.getType t Foo.x.

Actual behavior:
Two pieces of information are reported that contradict each other:

• Hover on let res reports res : MyClass.getType t Foo.x
• Error the returning res reports:

Type mismatch
  res
has type
  MyClass.getType t ?m.5
but is expected to have type
  Nat

Workarounds:
These two alternative definitions of res do not expose this error:

• let res := bar t Foo.x -- Foo.x instead of .x
• let res : MyClass.getType t Foo.x := bar t .x -- explicit type annotation

Versions

Tested on 4.31.0-nightly-2026-04-14 and 4.28.0

Impact

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

Start with the linked live.lean-lang.org reproducer and the test2 definition using bar t .x. Compare the hover type with the reported type mismatch, then inspect the elaboration path for outParam dot-notation resolution. Done means the minimal example reports no mismatch and consistently resolves .x as Foo.x, without requiring either workaround.