Change Global instances to #[export]

[patrick-nicodemus]

Suggests a different approach to managing typeclass instances now that the "export" locality attribute is available

[jdchristensen]

I'm tentatively in favour of this, but would first like to see that it works in practice, by removing Global (almost?) everywhere in the library, and checking that only a small number of Imports need to be added. Maybe the best approach is to try it in a few waves. E.g. try it for one folder first, then another, then more if things are going well?

BTW, based on https://coq.inria.fr/doc/V8.20.0/refman/language/core/sections.html#section-mechanism, I think that instances within a section can not be declared Global, so we shouldn't have any Global Instance declarations within a section. If I'm right, that means that when testing this, we can simply change all Global Instance to Instance.

We have about 2000 global instances in total, broken up by top-level folder like this:

./Algebra: 461
./Analysis: 0
./Axioms: 0
./Basics: 53
./Categories: 100
./Classes: 406
./Colimits: 22
./Cubical: 3
./Diagrams: 12
./Equiv: 5
./HIT: 8
./Homotopy: 133
./Limits: 4
./Metatheory: 4
./Misc: 1
./Modalities: 110
./Pointed: 57
./PropResizing: 0
./Sets: 21
./Spaces: 165
./Spectra: 0
./Tactics: 20
./Truncations: 17
./Types: 104
./Universes: 59
./WildCat: 250

[patrick-nicodemus]

In this series of commits I remove all the global instances from some of the folders to see how much maintenance is required.

I think the documentation you're citing is either incorrect or we are misinterpreting it. There are many Global Instances inside sections, and for me on Coq 8.20 if I remove the "Global" keyword for these I have to add the #[export] annotation to get it to compile. So one can do a global search and replace of Instance by #[export] Instance but it will look a bit nicer if we use the more concise syntax where it is permissible to do so.

The kind of maintenance I had to do was:

1. Adding new explicit import statements
2. Fixing breakages which I believe are due to changes in the order of hints in the typeclass database.

To elaborate on (2.), if A imports B at the top of the file, A declares a hint Hint_A and B declares a global hint Hint_B, then if C imports A and then B, then Hint_B will occur in the hint database before Hint_A because Hint_B was added first (at the time that B was first loaded, at the beginning of A). But if you now make Hint_B a module-scoped hint, then Hint_A gets added before Hint_B, because C imports A before B.

So you have typeclass searches which were quick before but now take a very long time, or go down a dead end. Most of these can be fixed by setting the typeclass search depth to something lower or annotating terms with more explicit detail.

[jdchristensen]

@patrick-nicodemus Thanks for tackling this! I haven't looked closely yet, but have a few comments/questions.

In this series of commits I remove all the global instances from some of the folders to see how much maintenance is required.

Does the library build after each commit? For example, the first new commit removes global instances from Basics, and only two other changes are made. If the library builds with just those two changes, that's great news.

I think the documentation you're citing is either incorrect or we are misinterpreting it. There are many Global Instances inside sections, and for me on Coq 8.20 if I remove the "Global" keyword for these I have to add the #[export] annotation to get it to compile.

Oh, that's annoying. It's hard to see how to handle that automatically. I guess you could try to do it based on indentation. Replace Global Instance with #[export] Instance and then replace the remaining occurences of Global Instance with Instance. I agree that it's better to not have #[export] for the ones that don't need it.

1. Adding new explicit import statements

That's to be expected. Another possible solution is to change Require Import to Require Export very selectively, if there is a file that you found you needed to add lots of imports for.

2. Fixing breakages which I believe are due to changes in the order of hints in the typeclass database.

To elaborate on (2.), if A imports B at the top of the file, A declares a hint Hint_A and B declares a global hint Hint_B, then if C imports A and then B, then Hint_B will occur in the hint database before Hint_A because Hint_B was added first (at the time that B was first loaded, at the beginning of A). But if you now make Hint_B a module-scoped hint, then Hint_A gets added before Hint_B, because C imports A before B.

Couldn't you just change C to import B before A to fix this? (But see below.)

So you have typeclass searches which were quick before but now take a very long time, or go down a dead end. Most of these can be fixed by setting the typeclass search depth to something lower or annotating terms with more explicit detail.

It would be good if not many such changes were needed. If a quick fix involving the import order (or using Require Export) can fix this, I think that would be better.

But longer-term, we should try to avoid situations where the order of imports affects typeclass search in a meaningful way. I think the real solution is to adjust the priorities of the instances so the more useful ones are tried first. This might be a bit hard to figure out, but is the most robust solution to this issue. So if there are cases in which you can easily tell what instance is being missed, you could give it higher priority. But if it's not easy, a quick fix involving import order (or export) would be fine.

[patrick-nicodemus]

The library builds after each commit, each one is self contained. Perhaps I should have put the "fixes" in separate commits for readability.

[patrick-nicodemus]

I guess you could try to do it based on indentation. Replace Global Instance with #[export] Instance and then replace the remaining occurences of Global Instance with Instance

I have been doing the manual equivalent of this but indenting style is not consistent throughout the library, so this is a very noisy signal for guessing whether you are in a file.

[jdchristensen]

Yes, it would have been easier to see the fixes if they were in separate commits. (I do like to have the library build after each commit, but that could be achieved by pairwise squashing before merge.) In any case, no need to redo things now.

[jdchristensen]

I have just skimmed through the commits. Here's my summary of the changes besides removing Global:

• Basics: only two lines, in V.v, getting rid of simpl in both cases. Fine.
• Wildcat: only five files changed outside of WildCat/*, and I think there were no changes within WildCat. Not bad, but the changes needed were a bit ugly, so hopefully by reordering imports, changing priorities, or using Export, this can be improved.
• Types: none!
• Algebra: This commit included removing Global from two files in Basics. There are no other changes outside of the Algebra folder. Within Algebra, there are two or three additional imports, a few type annotations : AbGroup, a couple of changes of GroupHomomorphism to Hom (A:=AbGroup), and the coercion from GroupIsomorphim to Hom. (Those last few seem to be the same as what was done in the Hint Mode IsGraph PR, so I'm not sure if it's intentional that they are here too. Maybe the same issue arises, so the same changes help here?) This is all fine.
• rest of library (except Classes): none!
• Classes: none!

(There's also a merge commit, but github seems to just show me the combination of the previous commits, so I'm assuming nothing substantial changed there. I also might have missed one or two things in my skimming, but if so, the diff was small enough to not catch my eye.)

So the upshot is that this change affected almost nothing. It's pretty amazing to me that we didn't seem to be relying on the transitive behaviour of Global except in a couple of spots.

The only commit I'm not completely happy with is the WildCat commit, but since only five files were affected, it shouldn't be hard to find a way to get rid of the changes made to those files. We should also check that the build time has not gone up.

[patrick-nicodemus]

I looked into this to see if it could be fixed by rearranging the typeclass database and I would prefer to just be more explicit in some parts. It is an unguided typeclass search where it is looking for a bifunctor structure on an unknown function A -> A -> A so I think it is better to just supply the underlying function explicitly. (Although granted we at least know the type here, so it is at least partially guided.)

Dan pointed out that the changes in this section are a bit ugly. I have rewritten a lot of this section in the latest commit on the philosophy that more changes to keep things pretty is better than a few ugly changes.

[patrick-nicodemus]

I have done a timing test and on my machine the time increased by ~1% on this PR. I assume this is considered negligible/within the realm of noise. I was hoping this PR would improve performance somewhat, but mostly I was hoping it would help to debug long loops of rapply because I don't have to worry about transitively imported hints that are difficult to find. I think that the PR can be justified on grounds of modularity even though it doesn't appear to improve performance.

[jdchristensen]

I have done a timing test and on my machine the time increased by ~1% on this PR. I assume this is considered negligible/within the realm of noise.

Yes.

I was hoping this PR would improve performance somewhat, but mostly I was hoping it would help to debug long loops of rapply because I don't have to worry about transitively imported hints that are difficult to find. I think that the PR can be justified on grounds of modularity even though it doesn't appear to improve performance.

I was hoping for an improvement as well, but like you, I still agree with this PR on principle.

[jdchristensen]

To me, this is essentially done, except for the minor issue about the * notation. With the recent commits, all of the awkward workarounds are gone, so there are only minor changes besides all of the removals of Global. So I have marked this as Ready for review.

[Alizter]

Can you hardwrap the paragraph in STYLE.md at 70 chars? I had a look through all of the changes and they look good. Thanks for tacking this! This is something we should have done a while back.

I have the same comment as Dan on the changes in MonoidObject. Let me know if you need any help.

[jdchristensen]

This looks good. I'll merge when the CI is done, unless someone speaks up before then.

[Alizter]

Again @patrick-nicodemus, thanks a lot for tackling this. It's really appreciated.

[patrick-nicodemus]

@jdchristensen
The commit you merged does not remove all Global Instances, only the Global Instances from the handful of sub-libraries which contain the majority of them (I followed your suggestion up above: remove everything from one library, change what needs to be changed, and go onto another.)

The merged commit removed some 2500 Global Instances. I have gone through and removed the remaining ~1000. There are only two changes:

1. isO_contr was changed to have priority 2 rather than 1
2. An import of the Pointed library in an AbSES file was moved to the top of the file so that group instances take priority over ptype instances in that file

[jdchristensen]

Ah, I misread this commit message: "Removed all 'Global Existing Instances' from the entire library."

[patrick-nicodemus]

@jdchristensen Yes, that is a silly distinction to make but since I was going by textual search and replace, I removed Global Existing Instances in a separate commit from Global Instances

[jdchristensen]

Oh, no worries, the commit message was fine and I just misread it.