Using new syntax for projection instance declarations

[patrick-nicodemus]

This commit replaces all Existing Instance proj1 occurrences in the library with the new :: syntax.

I have opted not to replace the occurrences of Coercion as I didn't realize the :> makes it reversible.

[Alizter]

This is funny. Back when the syntax was :> for an existing instance in a Class we had these priorities. When they were removed the parser still accepted and ignored them. Now that we are adding them back in, the priority is back to the original one.

[patrick-nicodemus]

I was pleasantly surprised that this notation was accepted by the parser.

[jdchristensen]

Does that mean that this change is also a semantic one? Why should we set the cost of this instance to something other than the default? (And since this wasn't just a rote change, it should have been highlighted in the PR.)

[Alizter]

The original intention is for the reflexivity instance coming from here to be lower priority than the rest. This was broken some time when we removed the legacy :> syntax.

We have two choices: Either we remove the | 2s or we keep them the way they are. The secondary option seems better as I think I see the reason for choosing a lower priority. During typeclass search, you don't want to try the reflexivity proof from the preorder class of R rather than just choosing a direct reflexivity proof if one is available.

[patrick-nicodemus]

I thought that the original hint had a custom priority of 2. If there was no custom priority in the original hint than this is a mistake and I'll look at it again to see what happened. Maybe I mixed it up with another hint

[jdchristensen]

As Ali explained, I think historically it had a custom priority of 2, but when the old :> notation for an instance was replaced with an explicit Existing Instance line, that priority was lost (but the | 2 was still in the record field, doing nothing). Then your change caused the priority to go back to 2. Ali suggests that this is probably a good thing, so there is no need to change this PR. I was just pointing out that this is a semantic change, which should have been mentioned, but of course it was the kind of thing that would be easy to miss.

[Alizter]

I had an initial look and it mostly looks good. Thanks for taking this on. I will do a more thorough review once my previous comments have been addressed.

[jdchristensen]

Thanks for doing this. It looks good to me.

Can you also update Section 3.7 of STYLE.md? It should say that we prefer "::" to "Existing Instance" and that we do not want to use ":>" for coercions, in part because it makes them reversible, and in part because we like being explicit about Coercions. It also has out-of-date info about what ":>" means.

(And another task would be to replace the current uses of ":>" with an explicit Coercion command. They were done without realizing that it made the coercions reversible.)

[jdchristensen]

This looks good to me, modulo one tweak to STYLE.md.

(And, just to be clear, my comment about removing :> was meant as a task for another PR.)