synthesize metavariables of function type

Stream: new members

[nnarek]

I see that lean able to synthesize metavariables inside this term
#check ∀ (x : Nat) (f : Nat → ?B), f x = 1

but unable for this one
#check ∀ (x : Nat) (f : ?A → ?B), f x = 1
it throws the following error, from which I can conclude that Lean successfully unified ?A with Nat, but instead of synthsizing ?A, it throws error

Application type mismatch: The argument
  x
has type
  Nat
but is expected to have type
  ?A
in the application
  f x

I do not understand why it happens and are there an option which will allow to do such synthesis

[Aaron Liu]

?A generates a synthetic opaque metavariable which is usually not allowed to be assigned by unification

[Kyle Miller]

#check ∀ (x : Nat) (f : _ → ?B), f x = 1

The ? metavariables cannot be assigned by unification (except by tactics).