rw fails because `outParam` was not filled correctly

Stream: general

[Yuyang Zhao]

class QuotLike (Q : Type) (α : outParam Type) (r : outParam (α → α → Prop)) where
  mkQ : α → Q

variable {Q α r} [QuotLike Q α r]

def lift {β : Type} (f : α → β) (h : ∀ (a b : α), r a b → f a = f b) : Q → β := sorry

theorem lift_mkQ {β : Type} (f : α → β) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) (a : α) :
    lift f h (QuotLike.mkQ a : Q) = f a :=
  sorry

example (h : ∀ a b, r a b → id a = id b) (a : α) :
    lift id h (QuotLike.mkQ a : Q) = a := by
  rw [lift_mkQ]
  rfl

example (h : ∀ a b, r (id a) (id b) → id a = id b) (a : α) :
    lift id h (QuotLike.mkQ a : Q) = a := by
  rw [lift_mkQ] -- fails because `r := fun a b => r (id a) (id b)` was not filled correctly

Is there a way to ensure that r is always filled correctly?

[Oliver Nash]

Looking quickly, I don't think that outParam is the issue here. Indeed h in your final example does not match the corresponding argument to lift_mkQ unless we commit some minor defeq abuse and use that id a = a. The rw tactic will not commit this sin; the erw will but is usually a sign something you be doing things differently earlier on.

[Yuyang Zhao]

Yes, but I was wondering if there is a way to force Lean to fill r via outParam? The context was that I was refactoring Quotient APIs, and then found out that this would make rw fail. I wondered if this could be completely avoided in the future.