Using new syntax for typeclass instance declarations #2262

patrick-nicodemus · 2025-03-20T07:03:04Z

In Coq 8.17, concise syntax was added to make a record projection into a typeclass instance, rather than writing "Existing Instance" after the record definition. This PR systematically replaces Existing Instance proj1 with proj1 :: ClassType throughout the library.

I also replaced Coercion proj1 : Record >-> FieldType with the syntax proj1 :> FieldType where I noticed it.

While going through the classes I found two classes with a single field. I replaced these classes with "unboxed" classes which do not define a record type, they are definitionally equivalent to their field. This reduces term size because you do not need a constructor, it also shortens the proofs because you don't need to rapply constructor.

There was one breakage in ClassifyingSpace.v due to the coercion Coercion equiv_fun : Equiv >-> Funclass being marked as reversible, but I'm not sure the mechanics of this infinite search during unification.

At several points there is a comment saying

Use :> and remove the two following lines (declaring a record projection as both an instance and a coercion) once Coq 8.16 is the minimum required version

I didn't understand this comment, as AFAIK there is no way to declare a record field as an instance and as a coercion at once, one can use :> or :: but not both, one still needs to add a line declaring the field as a Coercion or Existing Instance.

By the way, by default when you write proj1 :: ClassType, it declares proj1 with the #[export] attribute, but one can put other attributes like #[global] or #[local] directly inline in the record definition as well, also hint priorities can be written inline. The syntax is flexible.

Alizter · 2025-03-20T07:12:41Z

Be aware that :> makes the coercion reversible which can have some surprising behaviour if you are not aware of it.

Alizter · 2025-03-20T07:13:51Z

To do both, there is ::>.

Alizter · 2025-03-20T07:16:33Z

Regarding the boxed type classes, let's make those opaque to type class search, which is probably the original motivation.

patrick-nicodemus · 2025-03-20T07:17:43Z

Thanks, I didn't realize the coercions were reversible, so these changes have more semantic consequences than I realized. Luckily there was only one breakage (in ClassifyingSpace.v). I guess we should discuss whether the changes are positive or negative, the manual is not super clear on how this "synthesizing" of arguments works.

Alizter · 2025-03-20T07:19:44Z

Our current lower bound is 8.19 so you should check that we aren't introducing many warnings. The :> syntax for Classes went through a deprecation phase due to a change of semantics, so it might spit out some warnings.

Another comment would be to separate each kind of change so that we can better bisect the issue when there are future issues. Making the commits more atomic can help with review and future debugging pain.

patrick-nicodemus · 2025-03-20T07:22:31Z

@Alizter That warning is still in place, so I just didn't use :> at all in any Classes, only in Records.

patrick-nicodemus · 2025-03-20T07:29:56Z

Changing the typeclasses to opaque didn't fix the breakage in ClassifyingSpace.v. Hm.

patrick-nicodemus · 2025-03-20T08:02:35Z

I have determined that the breakage in ClassifyingSpace.v is a result of making equiv_fun : Equiv >-> Funclass a reversible coercion. The goal is (Pi 1 X $-> G) <~> (X $-> B G), which is an Equiv. The proof is by rapply natequiv_bg_pi1_adjoint, which tries refine @natequiv_bg_pi1_adjoint, refine (natequiv_bg_pi1_adjoint _) and so on. (natequiv_bg_pi1_adjoint _) does not unify with the goal, so unification tries to find some term r of type Equiv such that equiv_fun r = (natequiv_bg_pi1_adjoint _). Somehow this causes unification to loop, but I am not sure why.

If one writes exact (natequiv_bg_pi1_adjoint _ _) then there is no problem, it finds the correct solution immediately.

This is a bit surprising to me because I'm not sure what the search could be doing. Equiv isn't a canonical structure or a typeclass, so what is leading to this long search?

Alizter · 2025-03-20T08:04:24Z

You can mark a :> as non reversible using an attribute. See the definition of Natural transformation for an example.

patrick-nicodemus · 2025-03-20T08:10:51Z

Why do you think they chose to make reversible coercions the default for record projections? Do you think that is a sensible default for record projections?

jdchristensen

It's great to get this cleaned up.

But again I have to point out that you combined many different things into one commit, which made it much harder to review than necessary. Any time you are doing a bunch of rote changes, any change that does not follow the pattern should be put in a separate commit. And if you are doing more than one kind of rote change, each kind should be in a separate commit. This makes it very easy for us to focus on the changes that are more important to review. In addition, as Ali pointed out, it allows us in the future to determine which kind of change broke something or caused a slow down.

So you should break this up into multiple commits. From memory, I can recall at least five categories of changes: ::, :>, unboxing Classes, changing Lemma + Existing Instance to Instance, and whitespace. There may have been one or two more changes that would also deserve their own commits. Oh, right, there is the new Class in the Categories library, and however that ends up being done should be in its own commit.

jdchristensen · 2025-03-20T14:08:22Z

theories/Categories/Structure/Core.v

-
-    When we move to polyproj, it won't anymore. *)
-
+Existing Class is_structure_homomorphism.


This wasn't a class before, so this is a change to semantics. Presumably it has no instances, since it wasn't a class, so this should have no effect, but then it seems misleading to declare it a class.

It looks to me like the next part of this file is making a separate database to work around that issue preventing it from being made a class? If so, maybe the right thing to do for now is to not make this a class, but to change the comment to something like "It now works to make [is_structure_homomorphism] a class using [display the line], but taking advantage of that would require some other changes to the library." @JasonGross Is that a fair summary?

I need to go back and look at this more carefully, I don't remember what istrunc_is_structure_homomorphism was before the class declaration. I guess it would have been best to create an issue pointing out that this code now works in recent versions of Coq and ask how we can take advantage of this.

jdchristensen · 2025-03-20T14:10:29Z

theories/Classes/orders/orders.v

@@ -558,6 +558,6 @@ Section pseudo.
    - destruct (pseudo_order_antisym y z (ltyz , ltzy)).
  Qed.

-  Existing Instance lt_transitive.
+  #[export] Existing Instance lt_transitive.


I'll comment more generally on this, but this change should be in a separate commit.

jdchristensen · 2025-03-20T14:12:28Z

theories/Classes/theory/premetric.v

@@ -358,13 +350,12 @@ rewrite <-(pos_unconjugate L e),<-Qpos_mult_assoc.
 apply (lipschitz f L),xi.
 Qed.

-Lemma uniform_continuous@{} mu `{!Uniform@{UA UB} f mu} : Continuous f.
+Instance uniform_continuous@{} mu `{!Uniform@{UA UB} f mu} : Continuous f | 5.


Is this missing an #[export] like the previous result? Also, this is a different kind of change and should be in a different commit.

jdchristensen · 2025-03-20T14:13:38Z

theories/Diagrams/DDiagram.v

+Definition diagram_sigma {G : Graph} {D : Diagram G} (E : DDiagram D)
+  : Diagram G.
+Proof.
+  srapply Build_Diagram.
+  - intro i.
+    exact {x : D i & E (i; x)}.
+  - intros i j g x. simpl in *.
+    exists (D _f g x.1).
+    exact (@arr _ E (i; x.1) (j; D _f g x.1) (g; idpath) x.2).
+Defined.
+
+(** A dependent diagram is said equifibered if all its fibers are equivalences. *)
+
+Class Equifibered {G : Graph} {D : Diagram G} (E : DDiagram D) := {


Please don't mix whitespace changes in.

jdchristensen · 2025-03-20T14:16:26Z

theories/WildCat/Core.v


-Existing Instance isequiv_Htpy_path.
+Typeclasses Opaque HasMorExt.


This generates a warning, but I can't see the full message in the diff view.

jdchristensen · 2025-03-20T14:17:03Z

theories/WildCat/Equiv.v

-Existing Instance isequiv_cat_equiv_path.
+  := isequiv_cat_equiv_path :: forall a b, IsEquiv (@cat_equiv_path A _ _ _ _ _ a b).
+
+Typeclasses Opaque IsUnivalent1Cat.


Another warning.

patrick-nicodemus · 2025-03-20T14:34:50Z

It's great to get this cleaned up.

But again I have to point out that you combined many different things into one commit, which made it much harder to review than necessary. Any time you are doing a bunch of rote changes, any change that does not follow the pattern should be put in a separate commit. And if you are doing more than one kind of rote change, each kind should be in a separate commit. This makes it very easy for us to focus on the changes that are more important to review. In addition, as Ali pointed out, it allows us in the future to determine which kind of change broke something or caused a slow down.

So you should break this up into multiple commits. From memory, I can recall at least five categories of changes: ::, :>, unboxing Classes, changing Lemma + Existing Instance to Instance, and whitespace. There may have been one or two more changes that would also deserve their own commits. Oh, right, there is the new Class in the Categories library, and however that ends up being done should be in its own commit.

Yes, that's fair. I apologize and I will redo the commit. When I am going through lots of small changes like this where I end up reading through hundreds of files, inevitably I see other some changes that I think would be a good idea. I don't want to forget about them and lose track of them so I put them into same commit so they don't get lost. I guess I should keep track of the changes a better way, I could create multiple small branches or create an issue with a checklist of the changes I want to make. I will do my best to keep the material more organized.

jdchristensen · 2025-03-20T16:27:33Z

I guess I should keep track of the changes a better way

I tend to just make the changes, but in the UI I use when creating a commit, I scan through the changes and select which ones to add to the commit. In this case, I would scan through for the ones that don't match the rote pattern and apply their to their own commit(s). After a few iterations, what's left is the bulk, which I can easily put into the main commit. By manually choosing what to put into each commit, I also would notice if I unintentionally changed whitespace or other things, and could revert those then.

If some of the changes conflict, then this doesn't work so easily, so I would just make notes to come back to line XX of file YY later.

patrick-nicodemus · 2025-03-20T21:05:42Z

Is this magit? I sometimes use magit but I forgot it has that ability to work with sub file sized chunks in git

jdchristensen · 2025-03-21T16:12:25Z

Is this magit? I sometimes use magit but I forgot it has that ability to work with sub file sized chunks in git

Yes, it's magit. I think just about any git UI will let you select which chunks to commit, but magit even lets you select regions within a chunk.

Using new syntax for typeclass instance declarations

b1da402

Made unboxed classes opaque to typeclass search.

be3bec1

Marked Equiv as non-reversible.

a0f595b

jdchristensen reviewed Mar 20, 2025

View reviewed changes

patrick-nicodemus closed this Mar 21, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Using new syntax for typeclass instance declarations #2262

Using new syntax for typeclass instance declarations #2262

patrick-nicodemus commented Mar 20, 2025 •

edited

Loading

Alizter commented Mar 20, 2025

Alizter commented Mar 20, 2025

Alizter commented Mar 20, 2025

patrick-nicodemus commented Mar 20, 2025

Alizter commented Mar 20, 2025

patrick-nicodemus commented Mar 20, 2025

patrick-nicodemus commented Mar 20, 2025

patrick-nicodemus commented Mar 20, 2025 •

edited

Loading

Alizter commented Mar 20, 2025

patrick-nicodemus commented Mar 20, 2025

jdchristensen left a comment

jdchristensen Mar 20, 2025 •

edited

Loading

patrick-nicodemus Mar 20, 2025

jdchristensen Mar 20, 2025

jdchristensen Mar 20, 2025

jdchristensen Mar 20, 2025

jdchristensen Mar 20, 2025

jdchristensen Mar 20, 2025

patrick-nicodemus commented Mar 20, 2025 •

edited

Loading

jdchristensen commented Mar 20, 2025

patrick-nicodemus commented Mar 20, 2025

jdchristensen commented Mar 21, 2025


		When we move to polyproj, it won't anymore. *)

		Existing Class is_structure_homomorphism.


		Existing Instance isequiv_Htpy_path.
		Typeclasses Opaque HasMorExt.

Using new syntax for typeclass instance declarations #2262

Using new syntax for typeclass instance declarations #2262

Conversation

patrick-nicodemus commented Mar 20, 2025 • edited Loading

Alizter commented Mar 20, 2025

Alizter commented Mar 20, 2025

Alizter commented Mar 20, 2025

patrick-nicodemus commented Mar 20, 2025

Alizter commented Mar 20, 2025

patrick-nicodemus commented Mar 20, 2025

patrick-nicodemus commented Mar 20, 2025

patrick-nicodemus commented Mar 20, 2025 • edited Loading

Alizter commented Mar 20, 2025

patrick-nicodemus commented Mar 20, 2025

jdchristensen left a comment

Choose a reason for hiding this comment

jdchristensen Mar 20, 2025 • edited Loading

Choose a reason for hiding this comment

patrick-nicodemus Mar 20, 2025

Choose a reason for hiding this comment

jdchristensen Mar 20, 2025

Choose a reason for hiding this comment

jdchristensen Mar 20, 2025

Choose a reason for hiding this comment

jdchristensen Mar 20, 2025

Choose a reason for hiding this comment

jdchristensen Mar 20, 2025

Choose a reason for hiding this comment

jdchristensen Mar 20, 2025

Choose a reason for hiding this comment

patrick-nicodemus commented Mar 20, 2025 • edited Loading

jdchristensen commented Mar 20, 2025

patrick-nicodemus commented Mar 20, 2025

jdchristensen commented Mar 21, 2025

patrick-nicodemus commented Mar 20, 2025 •

edited

Loading

patrick-nicodemus commented Mar 20, 2025 •

edited

Loading

jdchristensen Mar 20, 2025 •

edited

Loading

patrick-nicodemus commented Mar 20, 2025 •

edited

Loading