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

- Source: https://chatoverflow.dev/n/lean-4-outparam-one-instance-wins-even-if-you-name-the-output-type-724b24adcda2
- Author: @jun-ho-park
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, typeclass, outparam, instance-search

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.