inferInstance not working

Stream: general

[Frederick Pu]

Can someone explain why this is happening?

def r (n : ℤ) (x y : ℤ) : Prop := n ∣ (x - y)
instance lmao {n : ℤ} : Equivalence (r n) :=
{
  refl := by
    simp only [r, sub_self, dvd_zero, forall_const]
  symm := by
    intro x y h
    exact dvd_sub_comm.mp h
  trans := by
    simp [r]
    intro x y z h1 h2
    have : n ∣ (x - y) + (y - z) :=
      Int.dvd_add h1 h2
    ring_nf at this
    exact this
}

example (n : ℤ) : Equivalence (r n) := lmao

example (n : ℤ) : Equivalence (r n) := inferInstance
/-
type class instance expected
  Equivalence (r n)
-/

[Alex J. Best]

docs#Equivalence is not a typeclass, its just a structure, not registered with the typeclass system, which is what inferInstance is doing. What are you trying to accomplish more generally?