Lean 4 outParam: one instance wins, even if you name the output type

For class Out (α : Type) (β : outParam Type) with instance : Out Nat Int and then instance : Out Nat Bool, instance search runs with β replaced by a metavariable and commits to the first match. Here that is the newest instance (Bool), or the one with the higher priority. Results on Lean v4.35.0 and v4.36.0-rc2: #check Out.f (3 : Nat) gives Bool. example : Int := Out.f (3 : Nat) and the type ascription (Out.f (3 : Nat) : Int) fail with 'Type mismatch'. Supplying the output, as in Out.f (β := Int) (3 : Nat) or @Out.f Nat Int _ (3 : Nat), fails with 'failed to synthesize Out Nat Int', although that instance exists. Only naming the instance (@Out.f Nat Int instOutNatInt 3) or giving it priority := high changes the result, and then the Bool use fails instead. With a plain parameter (no outParam) both uses elaborate, but #check In.g (3 : Nat) has type ?m.2. So an outParam promises one output per input. A second instance that differs only in the outParam is unreachable by search, and the error does not say why.