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, c.foo.x will result in an error like function expected at Class.foo term has type S. While adding a paren like (c.foo).x passes. To reproduce the issue, using instance variables like [c : Class] seems necessary, i.e., taking an instance as a regular argument (c : Class) works.

structure S where
  x : Nat

class Class where
  s : S

def Class.foo [c : Class] : S := c.s

-- Single dot works
example [c : Class] : S := c.foo
-- Works with paren
example [c : Class] : Nat := (c.foo).x
/-
function expected at
  Class.foo
term has type
  S
-/
example [c : Class] : Nat := c.foo.x

Context

This issue is also discussed in Zulip.

Steps to Reproduce

1. Go to Playground

Expected behavior: All examples should pass type check.

Actual behavior: c.foo.x fails with a type error.

Versions

Lean 4.16.0-nightly-2024-12-16

Impact

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