coercion/inference pitfall

Stream: lean4

[Mac]

What is going on with coercion and type inference that makes the below fail? Is this a bug? If not, why?

structure Foo (A : Sort _) := (foo : A)
structure Bar (A : Sort _) extends Foo A := (bar : A)
instance {A} : Coe (Bar A) (Foo A) := {coe := Bar.toFoo}
def getFoo {A} (F : Foo A) := F.foo
def bar : Bar Nat := {foo := 0, bar := 1}
#check getFoo (A := Nat) bar -- okay
#check getFoo bar -- fails, see below
/-
application type mismatch
  getFoo bar
argument
  bar
has type
  Bar Nat
but is expected to have type
  Foo (Bar Nat)
-/

P.S. I am using Lean 4.0.0-m2.

[Daniel Selsam]

I wouldn't have expected this to work, since the expected type is not known, and a TC query Coe (Bar Nat) (Foo ?m) would not be allowed to assign the ?m metavariable. However, I wouldn't have expected it to try to synthesize CoeT (Bar Nat) bar (Foo (Bar Nat)), and I do not immediately see why it unifies the argument to Foo with Bar Nat in the first place. I don't understand what is happening well enough to assess if it is a bug or not though. The current tracing system is pretty good but debugging this kind of thing can still be tricky. Pragmatic note: you don't need to pass A := Nat if the expected type is known, i.e. the following works: #check (getFoo bar : Nat)

[Mac]

Is there any way to inform lean that it should fill in the metavariable? (i.e. that Bar A only coerces to Foo A and not to some other Foo B?)