Conv pattern and typeclasses problem

Stream: lean4

[Tomas Skrivan]

I having a problem using pattern (foo _) in conv mode when the function foo depends on a somewhat complicated tangle of type classes.

Here is MWE:

class Trait (X : Type) where
  R : Type

class One (R : Type) where
  one : R

attribute [reducible] Trait.R

def add_one {X} [Trait X] [One (Trait.R X)] [HAdd X (Trait.R X) X] (x : X) : X := x + (One.one : (Trait.R X))
def foo {X} [Trait X] (x : X) : X := x

@[reducible] instance : Trait Int := ⟨Nat⟩
instance : One Nat := ⟨1⟩
instance : HAdd Int Nat Int := ⟨λ x y => x + y⟩

def add_one_to_one : add_one (1 : Int) = (2 : Int) :=
by
  conv =>
    pattern (add_one _)            -- Error: One (Trait.R ?m.532)
    pattern (@add_one Int _ _ _ _) -- works

I really do not understand why is there a meta variable when trying to synthesize One (Trait.R ?m.532). The ?m.532 should clearly be Int, I do not even understand why is it trying to synthesize an instance, an instance is already in the expression add_one (1 : Int) I'm trying to match on.

I'm suspecting that there is a bug of missing instantiateMVars or something along those lines.