Dot notation with typeclass instances issue

[lecopivo]

There seems to be an issue when using dot notation with type class instances.

mwe:

class Approx {α : Type} (a : α) (X : Type) : Type where
  val : X

variable {α β X Y : Type} {f' : α → β} {x' : α} [f : Approx f' (X → Y)] [x : Approx x' X]

-- fails
#check f.val x.val

-- works
#check let f'' := f.val
       let x'' := x.val
       f'' x''

The f.val x.val fails with

application type mismatch
  @Approx.val X (Approx.val x') ?m.70 f
argument
  f
has type
  Approx f' (X → Y) : Type
but is expected to have type
  Approx (Approx.val x') ?m.70 : Type

I would expect f.val x.val to typecheck

Tested on Lean (version 4.0.0-nightly-2022-11-18, commit 7529e86, Release)