synthesis failure along non-preferred parent

Stream: lean4

[Matthew Ballard]

I stopped by office hours with a simplified version of the following. Thanks for @Sebastian Ullrich for indulging me. The following makes things more clear I believe

-- stand in for Setoid
class Setoid' (R : Type _) where

-- stand in for some construction of quotient
def Setoid'.Quotient {R : Type _} (_ : Setoid' R) : Type _ := Unit

-- in mathlib, we would require a proof that relation preserves multiplication
structure Con (R : Type _) [Mul R] extends Setoid' R

-- in mathlib, we would require a proof that relation preserves addition
structure AddCon (R : Type _) [Add R] extends Setoid' R

structure RingCon (R : Type _) [Add R] [Mul R] extends Con R, AddCon R

-- @[reducible] -- uncomment me to break the last #synth
def RingCon.toAddCon' {R : Type _} [Add R] [Mul R] (c : RingCon R) : AddCon R :=
  {toSetoid' := c.toSetoid'}

-- the underlying quotient for an AddCon
abbrev AddCon.Quotient {R : Type _} [Add R] (c : AddCon R) := c.toSetoid'.Quotient

-- we can un-sorry this if we have a proof that the relation preserves addition
instance AddCon.instaAdd {R : Type _} [Add R] (c : AddCon R) : Add (c.Quotient) := sorry

-- the underlying quotient for a Con
abbrev Con.Quotient {R: Type _} [Mul R] (c : Con R) := c.toSetoid'.Quotient

-- we can un-sorry this if we have a proof that the relation preserves multiplication
instance Con.instaMul {R : Type _} [Mul R] (c : Con R) : Mul (c.Quotient) := sorry

-- the underlying quotient for a RingCon
abbrev RingCon.Quotient {R : Type _} [Mul R] [Add R] (c : RingCon R) := c.toSetoid'.Quotient

variable {R : Type _} [Mul R] [Add R] (c : RingCon R) (c' : AddCon R)

-- set_option trace.Meta.DiscrTree true in
-- set_option trace.Meta.synthInstance true in
#synth Mul (c.Quotient) -- ok

-- set_option trace.Meta.DiscrTree true in
-- set_option trace.Meta.synthInstance true in
#synth Add (c.Quotient) -- fails

-- set_option trace.Meta.DiscrTree true in
-- set_option trace.Meta.synthInstance true in
#synth Add (c.toAddCon'.Quotient) -- ok for now but make `toAddCon'` reducible and it breaks

[Matthew Ballard]

This is a continuation of #mathlib4 > synthesis failure on non-preferred parent

The cause is that the discrimination tree indexes c.Quotient for (c : RingCon R) as c.toCon.toSetoid' and then cannot find an instance of Add for this.

Lowering the transparency with RingCon.toAddCon' blocks this reduction so things work.

[Matthew Ballard]

In mathlib, there seems (from memory right now) to be multiple bug reports that involve "losing" instances along non-preferred parent projections. This might be related but is speculative at this point.

[Matthew Ballard]

I guess I can also use no_index here

instance AddCon.instaAdd {R : Type _} [Add R] (c : AddCon R) : Add no_index (c.Quotient) := sorry

but that seems less than ideal