`Application type mismatch` when using nested structure projection

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”)

Steps to Reproduce

structure Foo where
  S : Type

structure Foo.Bar (self : Foo) where
  s : self.S

def Foo.Bar.frob {foo : Foo} (bar : foo.Bar) : foo.Bar where
  s := bar.s

Expected behavior: Code succeeds.

Actual behavior:

Application type mismatch: The argument
  bar
has type
  foo.Bar
of sort `Type` but is expected to have type
  Foo
of sort `Type 1` in the application
  @s bar

Renaming the self variable for Foo.Bar avoids the error:

structure Foo.Bar (foo : Foo) where
  s : foo.S

Versions

Lean 4.23.0-nightly-2025-07-26

Impact

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

Start with the minimal Foo, Foo.Bar, and Foo.Bar.frob reproducer against the specified Lean nightly release. Trace the nested structure projection involved in the @s bar application; the issue is done when the original code succeeds without renaming self and the reproducer remains dependency-free.