fix(*): lower instance priority

[fpvandoorn]

use lower instance priority for instances that always apply
also do this for automatically generated instances using the extend keyword
also add a comment to most places where we short-circuit type-class inference. This can lead to greatly increased search times (see issue #1561), so we might want to delete some/all of them.

This PR will almost certainly break things, although I strongly expect that it will decrease the overall type-class inference search space. I investigated one place where type-class inference was short-circuited. This short-circuiting was necessary before the change, but not afterwards.

[sgouezel]

This looks like a very good idea, but I am afraid people will forget about it constantly, and it adds some boilerplate. Is it impossible to do it by automation, i.e., when an instance or a class is declared, change the priority on the fly depending on the shape of the statement (unless the priority is specified explicitly, and then respect the explicit choice)?

[robertylewis]

@fpvandoorn Thank you for doing this! I tried (briefly) a few weeks ago, and it seemed like it would be hard to do locally -- changing a few priorities broke many things, which required more priority changes to fix, and so on. But it's definitely a worthwhile change.

I am afraid people will forget about it constantly

There's a linting test for it. It's temporarily disabled in CI, but after this PR lands we can enable it, so forgetting about it will be automatically detected. I suppose 3.5c could use the same test to set the priority automatically. But this would be a destructive change (mathlib compiling with 3.5c would no longer compile with 3.4.2).

[sgouezel]

Maybe it's time to switch to 3.5c?

[robertylewis]

Maybe. I think it's a good thing to discuss at Lean Together in January. The list of reasons is growing.

[robertylewis]

It might actually be good to make this change in a branch of 3.5c before continuing on this PR. I suspect it will be a lot less work, and it would show any unexpected consequences (good or bad) of these changes.

[fpvandoorn]

I am afraid people will forget about it constantly

In addition to what Rob said, forgetting it is not worse than the situation we are currently in. It just means that in some cases you're doing unnecessary search before trying the easy instances.

The linter test doesn't apply to all automatically generated instances, since automatically generated instances are currently ignored by the linter. I'll try to fix that later. (If old_structure_cmd is true, then the linter will test the automatically generated instances, because the linter currently doesn't know that those instances are automatically generated)

It would be nice to set the priority automatically in the community fork, but until we adopt the community fork, I still want to finish and merge this PR.

---

As expected, there are some breakages. Some of the changes I had to make strictly improved a proof (e.g. replacing simp, refl by simp, which now closed a goal).
In some cases, a local instance is used, and it is necessary that some global instances are disabled during the proof. In that case I just locally set those global instances to have low priority.

There was also one case where a new construction was marked with @[reducible] and then some (incompatible) new instances were declared. This was fixed by just removing the reducible attribute.

[fpvandoorn]

It might actually be good to make this change in a branch of 3.5c before continuing on this PR. I suspect it will be a lot less work, and it would show any unexpected consequences (good or bad) of these changes.

I have already done all the priority changes. The only thing left to do is to fix resulting errors.

[fpvandoorn]

The library now compiles locally for me.
There are a few places that got worse (in some places where max_depth was increased, I had to increase it a bit more), but I think overall it got significantly better.

[sgouezel]

Do you understand why you had to increase max_depth in some places? Can you tell if there is a bad instance somewhere, or some instance whose priority should be changed?

[sgouezel]

Also, can you say how you determined the instances that needed tweaking (did you rely on the linter, or a clever grep, or did you look at all files one by one)?

And do you have statistics of compile time before/after? (If you have more than a 5% gain, I will merge this right away without letting time for others to complain that it is not automated :)

[fpvandoorn]

Do you understand why you had to increase max_depth in some places?

No, probably just some instances that are a slightly different priority, causing some searches to take longer and some searches to become quicker. Out of the 50+ instances where max_depth is increased, I had to increase 3 further, and probably there is a nonzero amount of them that can be reduced/removed now.

Can you tell if there is a bad instance somewhere, or some instance whose priority should be changed?

There are plenty of bad instances. The comp instances for unbundled morphisms (like is_mul_hom.comp) seem to be the worst, since they are applied using the identity function, and (probably) loop by themselves. Other instances that are suspicious are instances like additive.is_add_subgroup and is_mul_hom.mul, since type-class inference seemed to also apply them in cases where they wouldn't apply.

I'm happy to investigate those further in a future PR.

Also, can you say how you determined the instances that needed tweaking (did you rely on the linter, or a clever grep, or did you look at all files one by one)?

I searched for extend to figure out where to add the default_priority option (which should happen to all classes that extend some other class). I used the linter for all other instances.

And do you have statistics of compile time before/after? (If you have more than a 5% gain, I will merge this right away without letting time for others to complain that it is not automated :)

No. I am strongly trying to minimize the amount of local compilations of mathlib.
Hopefully Travis can give a reasonable estimate. The last commit adds some comments to a low-level file (tactic.lint) so that should recompile 90+% of the library.

[fpvandoorn]

5% reduction of total compile time is probably unreasonable to expect: I expect that less than 10% of the compilation time of mathlib is spend in type class inference: simp, tidy and other tactics probably take much longer.

[sgouezel]

The global strategy is clearly sound. Let me merge this, and then if we want to automate this it will be easy to come back to it with a simple grep as everything is clearly marked in the source code.