Odd behaviour with inferring instances.

Stream: mathlib4

[Wrenna Robson]

I am getting an odd behaviour with instances.

import Mathlib.Tactic
instance foobar {α : Type u} {β : Type v}  : Mul (β → Function.End α) := by infer_instance
--- This doesn't work: instance barfoo : Mul (Bool → Function.End (Fin 2)) := by infer_instance

Something is getting imported here that is breaking the latter case, and I have no idea what it is. This is causing me an issue, because suddenly some code that was working, that used the multiplication on Bool → Function.End (Fin (2^m)), is no longer doing so

[Wrenna Robson]

This was previously working - and I have no idea when it broke.

[Wrenna Robson]

This also works:
instance foobar {α : Type} {β : Type} : Mul (β → Function.End α) := by infer_instance

[Matthew Ballard]

This works again in #12037. I didn’t try to dig into the actual problem.

[Wrenna Robson]

Huh. How odd. How did you find it?

[Matthew Ballard]

set_option trace.Meta.synthInstance and looked at what it was trying. That was at the top of the list. It elaborated fine in foobar but didn’t in barfoo. Didn’t really try to figure out why since the instance itself seemed not so useful. There is probably some underlying issue still

[Wrenna Robson]

Interesting. Was it added recently?

[Wrenna Robson]

What does an instance being private do?

[Matthew Ballard]

Wrenna Robson said:

What does an instance being private do?

Doesn’t keep it very private :)

[Matthew Ballard]

Wrenna Robson said:

Interesting. Was it added recently?

I also didn’t check the git blame

[Junyan Xu]

I added the private instance in #7169; it was only used to prove two instances ((Two)UniqueProds (G × H)) by transferring results proved for indexed products to binary products. I couldn't inline it due to to_additive not working, or elaboration problem related to inferred universe parameters, maybe a combination of both. Since the proofs now work without the private instance, I'm all for removing it.

Thanks for the diagnosis and PR!

[Wrenna Robson]

How odd. Can we remove anything else while we're there?

[Wrenna Robson]

I don't want to create scope creep but obviously if we can remove future footguns or whatnot that seems good

[Matthew Ballard]

Thanks the :eagle: eye @Junyan Xu !

I think locating such future footguns is currently not a well-posed problem. I think it’s fair to say that user questions about typeclass synthesis are a top, if not the the top, issue. There have been many discussions but really the only concrete procedure we have is

1. Run into issue
2. Change priorities or remove instances to fix it
3. Repeat

[Wrenna Robson]

Well, I was really thinking about the other private instances in the same file.

[Wrenna Robson]

But yes in general it does not seem well-posed.

[Matthew Ballard]

Oh ok. Yes, private instance is not something I can assign a value to over instance. I think it is common to read it as “hidden instance” but since it is exposed to the typeclass synthesis it doesn’t really do a good job of hiding.

[Matthew Ballard]

If someone wants to attempt a cull of the private instances I would be interested in seeing how much breakage results

[Jireh Loreaux]

Why do we have private instances at all? Shouldn't they just be local?

[Junyan Xu]

These instances that I added should be okay globally, but they are auxiliary to two particular proofs and not intended to be otherwise used, which is a usual use case of private. If we intend them to be otherwise used, they should be moved to a more basic file. local instance is mainly used because it conflicts with a global instance (making them instances allows stating lemmas about them more conveniently), or for performance reasons (?).

However one of these instances is now indeed causing trouble globally. Does changing private instance to local instance solve Wrenna's original problem? Changing to instance probably doesn't? If instance works, we'll know to avoid private instance in the future, and it would be a good idea to remove the remaining private from instances in this file.