Bug for quotients?

Stream: mathlib4

[David Ang]

When making a structure based on quotient groups, sometimes instances are not found? Here is an MWE:

import Mathlib.GroupTheory.QuotientGroup

structure foo := (unfoo : ℕ)
instance fooSetoid : Setoid foo := sorry
def bar := Quotient fooSetoid
instance barNeg : Neg bar := sorry

variable (x : ℕ)
#check (-(⟦⟨x⟩⟧ : bar)) -- no instance of Neg (Quotient fooSetoid)
#check (barNeg.neg (⟦⟨x⟩⟧ : bar)) -- instance found

Not sure if it's a bug in instance resolution or reducibility or something else.

[Sebastien Gouezel]

When you are writing

#check (-(⟦⟨x⟩⟧ : bar))

you are not forcing Lean to consider that ⟦⟨x⟩⟧ is of type bar, you are just helping it to elaborate. Here Lean discards your advice, and considers it as a term of type Quotient fooSetoid. And it can't find a Neg instance on this one, which is normal since you haven't declared one (it's exactly what the error message says).

To force Lean to consider ⟦⟨x⟩⟧of type bar, you can for instance write id ⟦⟨x⟩⟧ : bar.

[Scott Morrison]

Alternatively an explicit bar.mkconstructor to help guide the type.

[Eric Wieser]

Making bar an abbrev here would work too I think

[David Ang]

I see. Thanks for the suggestions!