Help with instance search and (semi)OutParam

Stream: mathlib4

[Robert Maxton]

Consider the class

import Mathlib.Init.Data.Quot

/--A class representing antisymmetry "up to" some equivalence relation
  `eqv`. That is, if `rel x y` and `rel y x`, then `eqv x y`.

  As with `Quot`, `eqv` need not actually be an equivalence relation, in which
case `AntiSymmUpTo eqv r` is equivalent to `AntisymmUpTo (EqvGen eqv) r`-/
class AntisymmUpTo (eqv: α → α → Prop) (r: semiOutParam (α → α → Prop))  where
  antisymm : ∀ {x y}, r x y → r y x → EqvGen eqv x y

Clearly, as multiple relations r might 'close into' a given eqv, it would be inappropriate to mark r as an outParam. But with only a semiOutParam, simp_all and aesop can't seem to find the right instance even when there's one right there in the declaration:

  @[simp] -- or @[aesop safe apply]
  theorem antisymm_upto_eqv {r : α → α → Prop} [AntisymmUpTo ε r] {x y : α}
      (h₁ : r x y) (h₂ : r y x) : EqvGen ε x y :=
    AntisymmUpTo.antisymm h₁ h₂

  theorem foo {r : α → α → Prop} [AntisymmUpTo ε r] {x y : α}
      (h₁ : r x y) (h₂ : r y x) : EqvGen ε x y := by
    -- At this point, the infoview includes the line
    --`inst✝ : AntisymmUpTo ε r`.
    aesop -- makes no progress

[Robert Maxton]

Changing it to an outParam "fixes" the issue, but from what I understand that is not the correct use of outParams here. What else can I do to fix this?