synthesis failure on non-preferred parent

Stream: mathlib4

[Matthew Ballard]

import Mathlib.RingTheory.Congruence

abbrev AddCon.Quotient''' {R : Type*} [Add R] (c : AddCon R) := Quotient c.toSetoid

instance {R : Type*} [Add R] (c : AddCon R) : Add (c.Quotient''') := sorry

abbrev Con.Quotient''' {R: Type*} [Mul R] (c : Con R) := Quotient c.toSetoid

instance {R : Type*} [Mul R] (c : Con R) : Mul (c.Quotient''') := sorry

abbrev RingCon.Quotient'' {R : Type*} [Ring R] (c : RingCon R) := Quotient c.toSetoid

variable {R : Type*} [Ring R] (c : RingCon R)

#synth Mul (c.Quotient'') -- ok, finds the above

#synth Add (c.Quotient'') -- failed

Should I already know the answer as to why this fails?

[Matthew Ballard]

Even more troubling

#synth Add (c.toAddCon.Quotient’’’) — fails

Hopefully this is user error :)

[Matthew Ballard]

Mathlib free is easy

structure Con (R : Type _) [Mul R] extends Setoid R

structure AddCon (R : Type _) [Add R] extends Setoid R

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

abbrev AddCon.Quotient''' {R : Type _} [Add R] (c : AddCon R) := Quotient c.toSetoid

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

abbrev Con.Quotient''' {R: Type _} [Mul R] (c : Con R) := Quotient c.toSetoid

instance {R : Type _} [Mul R] (c : Con R) : Mul (c.Quotient''') := sorry

abbrev RingCon.Quotient'' {R : Type _} [Mul R] [Add R] (c : RingCon R) := Quotient c.toSetoid

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

#synth Mul (c.Quotient'') — ok

#synth Add (c.Quotient'') — fails

#synth Add (c.toAddCon.Quotient''') —  fails

[Matthew Ballard]

I think it is reasonable to expect this to succeed right?

[Matthew Ballard]

Well this works…

def RingCon.toAddCon’ {R : Type _} [Mul R] [Add R] (c : RingCon R) : AddCon R := { toSetoid := c.toSetoid}

#synth Add (c.toAddCon’.Quotient’’’)

[Matthew Ballard]

If I mark it reducible it fails again

[Eric Wieser]

Further minimized:

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

variable {R : Type _}

instance [Add R] (c : AddCon R) : Add (Quotient c.toSetoid) := sorry
instance [Mul R] (c : Con R) : Mul (Quotient c.toSetoid) := sorry

variable [Mul R] [Add R] (c : RingCon R)

#synth Mul (Quotient c.toSetoid) -- ok
#synth Add (Quotient c.toSetoid) -- fails
#synth Add (Quotient c.toAddCon.toSetoid) --  fails

[Eric Wieser]

The problem with the second one is that the expression is c.toMulCon.toSetoid which doesn't match the pattern AddCon.toSetoid ?_ that the first instance expects.

[Matthew Ballard]

You can even remove Setoid

structure Setoid' (R : Type _) where

instance : CoeSort (Setoid' R) (Type _) := sorry

def Setoid'.Quotient {R : Type _} (c : Setoid' R) : Type _ := c

structure Con (R : Type _) [Mul R] extends Setoid' R

structure AddCon (R : Type _) [Add R] extends Setoid' R

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

@[reducible]
def RingCon.toAddCon' {R : Type _} [Add R] [Mul R] (c : RingCon R) : AddCon R :=
  {toSetoid' := c.toSetoid'}

abbrev AddCon.Quotient''' {R : Type _} [Add R] (c : AddCon R) := c.toSetoid'.Quotient

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

abbrev Con.Quotient''' {R: Type _} [Mul R] (c : Con R) := c.toSetoid'.Quotient

instance Con.instMul {R : Type _} [Mul R] (c : Con R) : Mul (c.Quotient''') := sorry

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)

#synth Mul (c.Quotient'')

#synth Add (c.Quotient'')

#synth Add (c'.Quotient''')

#synth Add (c.toAddCon'.Quotient''')

#synth Add (AddCon.Quotient''' c.toAddCon)

[Eric Wieser]

Eric Wieser said:

The problem with the second one is that the expression is c.toMulCon.toSetoid which doesn't match the pattern AddCon.toSetoid ?_ that the first instance expects.

The third one in this example is fixed by making src#Quotient reducible

[Matthew Ballard]

Eric Wieser said:

The problem with the second one is that the expression is c.toMulCon.toSetoid which doesn't match the pattern AddCon.toSetoid ?_ that the first instance expects.

Thanks! It only fails to match with reducible transparency

[Eric Wieser]

Well it doesn't match syntactically either, which I think is the problem

[Matthew Ballard]

Eric Wieser said:

Eric Wieser said:

The problem with the second one is that the expression is c.toMulCon.toSetoid which doesn't match the pattern AddCon.toSetoid ?_ that the first instance expects.

The third one in this example is fixed by making src#Quotient reducible

Third? I get that working always. The fourth you can toggle on/off by toggling reduciblity of RingCon.toAddCon’

[Eric Wieser]

I'm counting in my code sample not yours

[Eric Wieser]

Making the three structures classes in my example, along with reducible Quotient, fixes everything

[Eric Wieser]

Not that it make any sense for them to be classes...

[Matthew Ballard]

Eric Wieser said:

Making the three structures classes in my example, along with reducible Quotient, fixes everything

Do you understand the underlying reason? I haven’t opened the source yet

[Matthew Ballard]

In the last code block I shared, you only need to make AddCon a class

[Matthew Ballard]

For all but the 2nd.

[Matthew Ballard]

And of course if you switch the order of the parents the failures flip

[Eric Wieser]

Can you think of any reason that Quotient shouldn't be reducible?

[Matthew Ballard]

No (edit: assuming benchmarking doesn’t complain)

[Matthew Ballard]

But I think the issue is broader than that

[Matthew Ballard]

Ah ok, there is a discrimination tree involved

[Matthew Ballard]

We don’t match on

[Add, Quotient, *, AddCon.0, *]

but

[Mul, Quotient, *, Con.0, *]

is ok

[Matthew Ballard]

With docs#Lean.Meta.DiscTree.getUnify

[Matthew Ballard]

And trace.Meta.Disctree is not turned on…

[Matthew Ballard]

It looks like that since the custom projection RingCon.toAddCon’ is reducible we end up at c.toSetoid’ which takes (c : Con R) as an argument and goes into the keys for the discrimination tree search. But this doesn’t match the AddCon in the entry from the Add instance so it just gets tossed.

If you don’t make the custom projection RingCon.toAddCon’ reducible, then you get AddCon as the key to match on.

[Matthew Ballard]

Since projections from classes are not reducible, this is another way to block the unfolding and make it work.

[Matthew Ballard]

Should Lean be able to synthesis these instances (really only needs to not cut them here)?

My answer is “obviously, yes” but what do I know. I feel like this might be a contributing factor to other failures coming from passing to non-preferred parents.

[Eric Wieser]

Matthew Ballard said:

It looks like that since the custom projection RingCon.toAddCon’ is reducible we end up at c.toSetoid’ which takes (c : Con R) as an argument and goes into the keys for the discrimination tree search. But this doesn’t match the AddCon in the entry from the Add instance so it just gets tossed.

If you don’t make the custom projection RingCon.toAddCon’ reducible, then you get AddCon as the key to match on.

Sorry, this is what I was trying to say above.

[Eric Wieser]

Matthew Ballard said:

Since projections from classes are not reducible, this is another way to block the unfolding and make it work.

Are they reducible on structures?