How to work with outParams

Stream: new members

[Luna]

This question stemmed from here. I have the an Equal type class whose second argument is an outParam. I want to create the equivalent version of Eq.symm, so for all instances Equal a b I want to create the instance Equal b a. Is this possible given the outParam as the second argument?

Below is my code:

variable {α : Type _}

class Equal (a : α) (b : outParam α) where
    equal : a = b

instance {a b : α} : Coe (Equal a b) (Eq a b) where
    coe eq := eq.equal

/-
ERROR:
cannot find synthesization order for instance @symm_inst with type
    {α : Type u_1} → {a b : α} → [a_eq_b : Equal a b] → Equal b a
all remaining arguments have metavariables:
    @Equal α ?a b
-/
instance Equal.symm_inst {a b : α} [a_eq_b : Equal a b] : Equal b a where
    equal := Eq.symm a_eq_b

[Edward van de Meent]

The short answer is no, you can't. If you want this, you have to get rid of the outParam