Hint mode

[patrick-nicodemus]

This pull request is similar to the previous one, where the Hint Mode of IsGraph is changed to !, meaning that typeclass search will never try to solve IsGraph ?A unless ?A is known.

I've done some more experimenting and debugging and I feel I have a little more to say regarding Coq's unification, elaboration and typeclass inference. Elaboration is a complex beast and there's a lot I really don't understand and I'm early in learning. Still, I learned a lot in the process of working on this so I'd like to document what I learned.

Let me start with the justification for this PR: I claim that the current setup makes the rapply tactic slow and inefficient, and to explain this I will discuss the refine tactic and elaboration in Coq.

In short, the way elaboration works in Coq for an incomplete term t declared to be of type T is:

1. Coq computes a type U = type(t) for t, which may contain holes.
2. Coq tries to unify T with U, solving all holes in the process.

This is very much a "bottom up" process: the declared type T has no effect at all at stage 1. It's possible to change this now using bidirectionality hints, which are not part of this PR, but I'll comment on these later, I think they could be useful.

Actually this process is apparently recursive, in the sense that while traversing the term t from the ground up, both steps are repeated for each subterm. For example, if f a is a small subterm of t, where f is a variable of declared type forall x :A, B x and a is a complex term, then:

1. Coq computes a type U_a = type(a), which may contain holes, and
2. Coq tries to unify U_a with A and if successful reports B a as the type of f a.

Typeclass search seems to be part of step 2; if unification fails, then by default we launch a typeclass search to instantiate the values within terms (if this flag is set to its default value, Typeclass resolution for conversion).

Typeclass search seems to be regarded as a "success" for a given subterm if it successfully instantiates all the typeclass holes in a consistent way, even if these choices cause elaboration of the broader term to fail.

An important thing that can interfere with this process is coercions. In order for coercions x -> f x to work right in partially elaborated terms, we need to know the type that x needs to be in order to apply the coercion. For example, g $o f will fail in general if g needs to be coerced (say, from Iso x y to Hom x y) in order to be of the correct type, because we can't derive the Hom type from g alone.

Some of the downstream changes I made have a simple, obvious explanation. For example, in

Global Instance reflexive_Hom {A} `{Is01Cat A}
  : Reflexive Hom
  := fun a => Id a.

it should be clear that there is no way to "honestly" elaborate the expected type Reflexive Hom or fun a => Id a by deriving it from constraints, because A is not mentioned. Instead, in trying to elaborate Hom ?A ?IsGraph ?Is01Cat,
typeclass search would in theory search through the entire database plugging in all possible values of ?IsGraph, but it starts with the hints prioritized in the context, and since the hints in the context give a valid solution to the typing problem, there's no need to continue the rest of the search. This seems harmless, although I think I have an aesthetic preference for explicit specification when things cannot be uniquely derived.

I think there are a few points in the code base where we are relying on a somewhat surprising elaboration strategy for terms. I will attach a small example, which is a paraphrased version of one of the changes in this commit.

Require Import WildCat.Core.
Require Import Algebra.AbGroups.AbelianGroup.
Axiom inv : forall (A : AbGroup), GroupIsomorphism A A.
Set Printing All.
Set Typeclasses Debug.
Set Debug "unification".
Definition abc1 (A B  : AbGroup) (f : Hom A B) := (inv B) $o f.

From reading the unification debug logs, the first thing that happens (after f : Hom A B is fully elaborated) is that we try to check that the application of cat_comp to inv B is valid by unifying the type of inv B, GroupIsomorphism B B, with Hom ?A ?IsGraph ?Is01Cat ?x ?y This unification fails almost immediately (thank you very much Gaetan Gilbert for helping me understand why!) so we try and elaborate both the type of inv B and Hom ?A ?IsGraph ?Is01Cat ?x ?y independently using typeclass search.
It's important to note here that when we are trying to elaborate this latter term, we are truly starting from scratch and starting to "elaborate" the term Hom _ _ _ _ _ from nothing. The typeclass search is not being driven by the type argument, because there is no type argument, so it is just generating any arbitrary typeclasses of the form Is01Cat and IsGraph, and instantiating the type this way. In this case we get lucky and get the right answer, but only by the coincidence that isgraph_abgroup happened to be the most recent hint in the database - if you change AbGroup to Group in inv and abc1, it will fail because it still finds isgraph_abgroup as the most recent hint in the database and we can't convert a Group to an AbGroup.

So, in my opinion, this is not very robust, we are getting lucky, and I think we shouldn't rely on this elaboration technique, if possible we should try and understand why unification is failing and fix it. This is one argument for using Hint Mode + in some cases.

Now let me return to the discussion of rapply. Something like Build_Is0Bifunctor'' takes, say, a dozen arguments, so we want refine Build_Is0Bifunctor'' || refine Build_Is0Bifunctor'' _ || refine Build_Is0Bifunctor'' _ _ to fail quickly at each case so we quickly reach 12 arguments. The way this works is that we try to unify the type of (Build_Is01Bifunctor'' _ _ _ _ _ _) with the type of the goal, and if this fails, we launch typeclass search to elaborate the term and try again, but this is not guided from the top down, so we are trying every combination of hints in the database for the typeclass holes. This is very expensive. Using Hint Mode ! on the parameter types would make this faster because we basically wouldn't carry out a typeclass search at all unless unification succeeded in instantiating the parameter types.

Now, bidirectionality is complementary to this. If we write

Arguments Build_Is0Bifunctor'' {A B C} & { H H0 H1 _ } F _ _

then whenever we call Build_Is0Bifunctor'', it will first look to the context of the expected type to solve for A, B, C, and then try to elaborate the rest of everything from this. In this situation, as long as Build_Is0Bifunctor is being used in a situation where the correct types can be inferred from the external context then you will not have this unguided typeclass search. And in many cases where we remove typeclass inference with Hint Mode + we could restore the same elaboration behavior with bidirectionality hints, so hopefully not too many more annotations. On the other hand if unification fails completely (as in the first few iterations of rapply) then typeclass search will still start from a blank slate, so bidirectionality will not make as much of an impact there.

I experimented with bidirectionality and I found that in some cases you want to use it and in some you don't. If you have cat_comp _ _ _ g f where g needs to be coerced from Iso x y -> Hom x y or something, then bidirectionality is helping you, because deriving the category structure from Iso x y would give you the wrong answer. But if g, f are (say) group homomorphisms and you have a function application (cat_comp _ _ _ g f) x, then bidirectionality could hurt you here because based on the application it will derive that (cat_comp _ _ _ g f) should be of a function type, and therefore Hom x y should be a function type, and maybe it will now coerce g, f from group homomorphisms to functions before composing them. Or, if this unification fails, it will carry out typeclass search and just find any type with a category structure whose homs are function types.

In some of the commits below, we have to add additional type annotations.
In some, rapply takes too much time to run; I checked that these can be fixed by adding more Hint Mode + types to make rapply fail faster, but I chose a simpler patch.

A complementary fix for rapply would be perhaps to replace refine (f _ _ _ _) with notypeclasses refine (f _ _ _ _); try(typeclasses eauto) which should fail faster if it cannot successfully unify the type of the input with the type of the term at all, making the earlier stages much faster.

[jdchristensen]

Thanks for the very detailed explanation! I don't follow some of the points you made, but I appreciate the effort you took to understand this and explain it.

The changes here aren't too bad, but it's a bit annoying to have to write cat_comp (A:=Foo) in a number of places. Is there a way to tell Coq to try using the second map to determine A? Or any other trick we could use?

If not, some ideas are:

• Make a notation (maybe f $o[A] g?) that specifies the category.
• Make a notation (maybe f oG g) that specifically works with group homomorphisms.

My broader question is about the benefit. The description of the PR talks about making rapply faster. Can you give an example of something that is faster with this PR than without it?

[patrick-nicodemus]

Yes, I will try to construct examples of rapply working faster to move the discussion forward.

I think the $o[A] notation or something like it is a good idea. I can incorporate such a notation into the PR or try the alternative solution of adding a coercion. Still, something like $o[A] makes sense to have around in general.

[Alizter]

I think the $o[A] notation or something like it is a good idea. I can incorporate such a notation into the PR or try the alternative solution of adding a coercion. Still, something like $o[A] makes sense to have around in general.

I like the idea of this notation, but I would prefer a separate PR for it. There are two points to address. Firstly, we need to do some formatting tweaks which I can help with in the PR, and secondly we need to find cat_comp (A:=_) in the library and see if it helps readability when used.

[patrick-nicodemus]

This PR was motivated by downstream breakages in the rapply tactic while I was trying to work on my bicategory development, so I hope it's okay for me to draw examples from that PR rather than trying to find examples in the current master.

In #2215 in theories/WildCat/TwoOneCat.v, at the definition of cat_postwhisker_pp, there was previously an rapply tactic used, but after adding / removing typeclasses above, it takes too long to run. In the PR code we have

Definition cat_postwhisker_pp {A} `{IsBicategory A} {a b c : A}
  {f g h : a $-> b} (k : b $-> c) (p : f $=> g) (q : g $=> h)
  : k $@L (q * p) $== (k $@L q) * (k $@L p).
Proof.
  Set Typeclasses Debug.
  Set Typeclasses Depth 4.
  time rapply fmap_comp.

So, at each iteration before the final one, unification fails (it's the wrong number of holes for fmap_comp to unify with the goal) and this takes 13 seconds before giving up. Typeclass search is looking for 1-category structures on types ?X and ?Y and a 1-functor structure on ?F : ?X -> ?Y (all unknown because unification failed) and there are a lot of possible instantiations of these given a bicategory structure on ?X, so search takes a while.

Adding Hint Mode IsGraph ! : typeclass_instances. before the definition reduces this to 6.7s.
Adding both Hint Mode IsGraph ! and Hint Mode Is2Graph ! - reduces it to 0.08s.

[patrick-nicodemus]

For contrast, without using Hint Mode, time do_with_holes ltac:(fun x => nrefine x; try typeclasses eauto) fmap_comp terminates in 0.01s; for performance it is obviously preferable to avoid typeclass search altogether if you can get away with it!

[Alizter]

Why not do nrapply? We very rarely use rapply in wildcat stuff.

[patrick-nicodemus]

I don't follow your point. The example I gave was not an instance of rapply that I had written, it was an instance of rapply which existed already in the codebase. Changing rapply to nrapply would have been an easy one-line fix. The fix I chose in this scenario was to replace the proof using rapply with a direct definition, which was also an easy one-line fix. But it would have been easier to not have to fix it at all, if rapply was more stable.

But the general scope here is beyond rapply, because this affects the elaboration of all terms.

"Robustness" of Coq code is pretty complex and subjective. That said, if you write a term t : T where type(t) cannot be unified with T , and so the elaboration falls back on totally unguided typeclass search to try and instantiate holes in t, then because of the lack of structure guiding the search, the outcome is going to be dependent on the order of typeclass hints in the database (I give an example in the OP) and so I think this is more likely to break later in response to refactoring.

On the other hand it's definitely a convenient feature that makes the code more concise because typeclass search often hits the right answer quickly and helps the elaborator figure things out where we would otherwise need lots of annotations. So I think there's a tradeoff between concision and robustness here. The opposite extreme here is Unset Typeclass Resolution For Conversion, where typeclass resolution is never used to flesh out two terms in order to help them unify, and I think that would probably be infeasible. I'm not sure what the right balance is, but this PR is a small move from convenience -> robustness.

[jdchristensen]

For contrast, without using Hint Mode, time do_with_holes ltac:(fun x => nrefine x; try typeclasses eauto) fmap_comp terminates in 0.01s; for performance it is obviously preferable to avoid typeclass search altogether if you can get away with it!

Have you looked into how much would need to change if we made rapply behave this way? It does seem like it would get rid of a lot of fruitless search, but I don't know how often we rely on this behaviour working quickly by chance.

[jdchristensen]

Why not do nrapply? We very rarely use rapply in wildcat stuff.

Really? I thought we often needed the wildcat instances to be found. Here's the data for WildCat/*.v:

    247 (s)nrapply
    194 (s)rapply

Anyways, I think this is beside the point. It's a good idea to make rapply behave better, maybe by using Hint Mode more, maybe by changing rapply so it doesn't try fruitless search, or maybe with both.

I'm in favour of moving forward with this PR, but think we should first solve the composition issue.

I think it should be possible to revert these changes just by declaring a coercion GroupHomomorphism >-> Hom or GroupIsomorphism >-> Hom

If that's true, then it could be added to this PR and maybe we'd be done. If it doesn't work, then I think we should have a separate PR that introduces a notation for composition in a wildcat. I proposed f $o[A] g, but another option would be something like f $o g :> A, paralleling x = y :> A to specify the type in which paths are taken.

[jdchristensen]

Have you looked into how much would need to change if we made rapply behave this way? It does seem like it would get rid of a lot of fruitless search, but I don't know how often we rely on this behaviour working quickly by chance.

If we do rely on the current behaviour a lot, we could keep that behaviour and add a third version with the new behaviour. Here's one idea on the naming:

• tapply: what is currently called rapply: eager typeclass search.
• rapply: the new idea: only use typeclass search after unification with the goal.
• napply: what is currently called nrapply: no typeclass search at all. (Renamed just to fit the pattern.)

(Or the first two could be swapped, if we need most current uses of rapply to do eager typeclass search.)

All three would have s versions ("simple") to show all subgoals.

Ideally, we wouldn't need three, so this is only a worthwhile option if many uses of rapply can be converted to the new idea, but many cannot.

[patrick-nicodemus]

For contrast, without using Hint Mode, time do_with_holes ltac:(fun x => nrefine x; try typeclasses eauto) fmap_comp terminates in 0.01s; for performance it is obviously preferable to avoid typeclass search altogether if you can get away with it!

Have you looked into how much would need to change if we made rapply behave this way? It does seem like it would get rid of a lot of fruitless search, but I don't know how often we rely on this behaviour working quickly by chance.

The original tactic I wrote down has slightly different shelving behavior than refine, so it isn't a drop-in replacement.
I did an experiment the other day where I replaced the definition of rapply with the following tactic:

Tactic Notation "rapply" uconstr(term)
  := do_with_holes ltac:(fun x => try (try (nrefine x || fail 2); fail); refine x) term.

If I wrote this correctly, it should try nrefine x, nrefine (x _), ... until it finds a term t such that nrefine t succeeds;
then it fails and applies refine t instead so that the typeclass behavior is the same. I then fixed all the downstream breakages that were relying on rapply instantiating typeclasses in order to unify terms (because this tactic will not succeed if nrefine never succeeds)
https://github.com/patrick-nicodemus/HoTT/blob/rapply_v2/theories/Basics/Tactics.v

If I applied the timing experiment correctly, the results of this change are -1% time difference on average, which seems negligible. But I am not positive I correctly applied the timing script. Here is the result:
patrick-nicodemus@0c73334

Anyway, skimming through that branch rapply_v2 and its diff with master should indicate how big the changes are that would need to be made.

[patrick-nicodemus]

Some minor stylistic changes. Added a coercion GroupIsomorphism >-> Hom which resolves four of the six explicit Group category annotations.

I tried adding a coercion GroupHomomorphism >-> Hom as well and this fixed the remaining two, but this seemed to break more things downstream so I skipped it. Instead I replaced phi: GroupHomomorphism A B with phi : Hom (A:=Group) A B in a few spots and this fixed it. (One could also make GroupHomomorphism a Notation for @Hom Group isgraph_group, as well, and this would solve the problem as well by eliminating the need for coercions to be inserted.)

[jdchristensen]

The original tactic I wrote down has slightly different shelving behavior than refine, so it isn't a drop-in replacement. I did an experiment the other day where I replaced the definition of rapply with the following tactic:

Tactic Notation "rapply" uconstr(term)
  := do_with_holes ltac:(fun x => try (try (nrefine x || fail 2); fail); refine x) term.

If I wrote this correctly, it should try nrefine x, nrefine (x _), ... until it finds a term t such that nrefine t succeeds; then it fails and applies refine t instead so that the typeclass behavior is the same.

I think you are right about how this behaves. I suspect that it could be done more directly, maybe by using unify?

If you instead try your original way, where you just use nrefine and then do typeclasses eauto afterwards, does a lot more break? I ask because I'd prefer an implementation that is more transparent and that doesn't do an extra unification step.

If I applied the timing experiment correctly, the results of this change are -1% time difference on average, which seems negligible.

Interesting, I would have suspected a bigger improvement. But when rapply was slow, we avoided it. With your new version, there are probably places where it was avoided and could now be used.

Anyway, skimming through that branch rapply_v2 and its diff with master should indicate how big the changes are that would need to be made.

Unfortunately, in addition to the 69 lines that changed in an important way, that commit contains 52 lines with whitespace changes. You have to avoid putting such unrelated changes into your commits. Luckily, I found a way to view the changes without showing the whitespace changes:

https://github.com/HoTT/Coq-HoTT/compare/master...patrick-nicodemus:HoTT:rapply_v2?diff=unified&w=1

The library contains around 2000 uses of (s)rapply, so it's great that only 69 of them needed to change. And 4 or 5 of those changes are improvements anyways, where rapply is simply replaced with exact. So I think this is good evidence that replacing rapply with your new definition (or something similar) is sensible. And it's probably worth adding tapply which behaves like the old rapply. Then alphabetical order napply, rapply, tapply would also correspond to "strength of typeclass search" order.

[jdchristensen]

We should move the discussion of rapply out of this PR. Can you make a new PR with your rapply_v2 branch, but with the whitespace changes removed?

Also, can you redo the latest commit to this PR with the whitespace changes removed?

[jdchristensen]

(One could also make GroupHomomorphism a Notation for @Hom Group isgraph_group

This won't work, because GroupHomomorphism is how the graph structure on Group is defined. But glad to see that the other trick helped.

[patrick-nicodemus]

Whitespace changes removed

[jdchristensen]

I approve, but I'll wait to see what @Alizter thinks before merging.

[Alizter]

It will be a couple of days before I can have a closer look. If there is a rush to get this through however, I don't mind @jdchristensen confirming the change and merging.

[jdchristensen]

It will be a couple of days before I can have a closer look. If there is a rush to get this through however, I don't mind @jdchristensen confirming the change and merging.

I don't think there's any rush. The diff is now quite clean, so it should be quick to review when you get a chance.

[jdchristensen]

@Alizter Do you still want more time to look at this one?

[patrick-nicodemus]

I'm just going to comment here with an example of this robustness issue I mentioned above, because I find it pretty complicated and I need a convenient place to write down a simple example that illustrates the problem. @jdchristensen said in response to the original post that he didn't follow everything I said, so I'm trying to make a simpler example.

Require Import Basics.Overture Basics.Tactics. 
Require Import Types.Bool Types.Unit Types.Empty.

Class myType (b : Bool) := { type_of : Type }.
Instance myType_ff : myType false := { type_of := Empty }.
Instance myType_tt : myType true := { type_of := Unit }.

Definition f {b : Bool} {p : myType b} (x : @type_of _ p) : Unit := tt.
Definition abc := f tt.

This definition succeeds, but if you swap the order of the instances, it fails.

What's happening is this.
Expanding the term, you get f _ _ tt. The type signature of f is defined so that the type of the third argument x is @type_of _ _. So, we try to unify @type_of _ _ with the type of tt, which is Unit. This is not a problem that unification knows how to solve, so we fall back on typeclass inference. Typeclass inference is going completely blind here, because unification failed completely, so it has to instantiate myType ?b without knowing ?n. It keeps trying hints until it "succeeds" by instantiating the typeclass. Since @typeof true mytype_tt is unifiable with Unit, it succeeds and we can apply f to tt. But @typeof false mytype_ff is also considered a valid solution from the point of view of typeclass inference, because ?b is a free variable; so typeclass inference succeeds, and then we try to unify Unit with @typeof false mytype_ff, which we obviously cannot do, so we have a failure.

So I consider this a robustness issue, because whether elaboration of a term succeeds or not should not be dependent upon subtle details such as typeclass ordering. Let us now discuss possible solutions to this issue, which are not necessarily mutually exclusive.

1. Reduce the amount of such fragile code that we write, by using Hint Mode myType ! : typeclass_instances. and the weaker version of rapply I have suggested in another PR. This would simply cause both definitions to fail, because typeclass search would fail immediately rather than randomly guessing at a type it couldn't solve. Of course this doesn't solve the problem, it just surfaces instances of the problem in the codebase and prevents us from writing more code that relies on that elaboration behavior.
2. Give a hint to the unification algorithm that @type_of ?b ?mytype ~ Unit can be solved by the instantiation @type_of true mytype_tt ~ Unit, so unification solves the problem directly and we don't have to fall back on typeclass inference. This is exactly what happens when you declare mytype_tt as a Canonical Structure, and we can see that when you replace Instance with Canonical Structure above, it solves the problem.
3. Bidirectionality. Bidirectionality doesn't solve the example above, but it helps with a similar example:

Definition g {b : Bool} {p : myType b} (x : @type_of _ p) : @type_of _ p := x.
Definition f (x : @type_of true _) : Unit := tt.
Arguments g {b} & {p}. (* Succeeds if this line is present, fails otherwise *)
Definition abc := f (g tt).

The point here is that in this situation, the argument b of g can't always be derived from x, so you can tell Coq to ignore x and instead derive the value of b from the surrounding context. Here, the output of g should have type myType true to align with f, so we get the value of b and can solve for p correctly based on that. I don't know yet for what kinds of functions we should use bidirectionality hints, but it seems common to use them for record constructors between the parameters and the arguments.
4. Extend with a coercion. Coercions are inserted during the unification process, so this, like canonical structures, is helping unification to solve the problem.

Definition unit_to_instance (x : Unit) : @type_of _ myType_tt := x.
Coercion unit_to_instance : Unit >-> type_of. 
Definition abc := f tt.

[Alizter]

Suggested change

	Coercion isHom_GroupIsomorphism : GroupIsomorphism >-> Hom.
	Identity Coercion isHom_GroupIsomorphism : GroupIsomorphism >-> Hom.

Documentation on this is terrible:
https://coq.inria.fr/doc/master/refman/addendum/implicit-coercions.html#identity-coercions

Basically its a coercion that doesn't insert a term. This is useful for elaboration. So GroupIsomoprhism will be treated as a Hom and elaboration will work on that, but isHom_GroupIsomorphism won't be inserted.

Also I don't like the name. Something like groupisomorphism_to_hom is better IMO.

[patrick-nicodemus]

This gives me the error message "GroupIsomorphism must be a transparent constant." Do you know a fix for this?

[jdchristensen]

I also had trouble trying something similar. BTW, if this trick works, could it be applied to GroupHomomorphism instead of GroupIsomorphism without leading to cycles? That would help us use WildCat results more often when dealing with group homomorphisms.

[JasonGross]

Identity Coercion only works when both constants are definitions and one (eventually) unfolds to the other.

[jdchristensen]

@patrick-nicodemus Thanks for the great overview.

Let us now discuss possible solutions to this issue, which are not necessarily mutually exclusive.

I'll add a couple of things:

5. Annotate instances with priorities (also called costs). The example involving myType works with the instances in either order if myType_ff is given a higher cost. When we have instances that are not likely to be used or are too generic, we should give them higher costs.
6. Remove some instances that are not likely to be used much in practice. If they are needed in a particular file, they can be added at the top of the file with a simple Existing Instance command. Similarly, some global/export instances could be made local.

I also don't think it's really that serious a problem if the behaviour sometimes depends on the order in which files are imported. We should in general import the most generic things first and the most specific things later, which will often mean that the desired instances are tried first. Even if either order works, this should speed up type class search. (And it's worth noting that many of the suggestions in our lists will not only improve how often typeclass search succeeds, but will likely speed it up as well.)

[jdchristensen]

I've thought a bit more about the idea of using Hint Mode ! and how it will interact with how we use the WildCat library in practice. For example, we often use it to deal with pointed types. Currently, almost nothing about pointed types is expressed in WildCat notation, and yet we use results from the WildCat library freely. This means that Coq has to search through various wild category structures before it finds one that matches the goal. Adding Hint Mode ! to IsGraph doesn't seem to hurt this, but I think that's only because Coq does searches on Is2Graph, etc., which do eventually find the right instance, which then forces the IsGraph instance to be resolved correctly. If we added Hint Mode ! to all of the WildCat structures, I think we'd find that we need to add (A:=pType) to every use of the WildCat library for pointed types, and similarly in other situations (Type, Group, etc).

We could adapt the pointed types library to use WildCat notation (e.g. by making the existing notations like o* and ==* synonyms for WildCat notations), which I think would remedy this. But we'd have to do this not just for pointed types, but throughout the library (even for (A:=Type)), and it would be a lot of work. So I think there's a fundamental conflict between having the WildCat library be useful for things not expressed in WildCat notation and the hope of getting rid of undirected search.

We could add more coercions to WildCat Hom, but I tried this for pointed maps, and didn't get far. Even just adding a type that would be the domain of the coercions caused lots of build failures for reasons I couldn't figure out:

Definition pMap (A B : pType) := pForall A (pfam_const B).
Notation "A ->* B" := (pMap A B) : pointed_scope.

(This also suggests that changing A ->* B to be a synonym for the wildcat Hom is going to lead to lots of build failures.)

So my general summary is: Adding Hint Mode ! to IsGraph doesn't actually reduce typeclass search much in practice, since almost all of the time Coq will still search for Is2Graph, etc. And I don't think it will be feasible to use Hint Mode ! on all wild category structures without a major overhaul. So I feel like this PR is going in a direction that won't be productive in the long run, and so maybe we should decide not to merge it.

BTW, adding

Existing Instance isgraph_ptype | 0.

to the top of pSusp.v makes Coq find the right instance immediately. So I think adding some lines like that to appropriate files is a good way to control typeclass search and make it find what we want quickly.

[patrick-nicodemus]

So my general summary is: Adding Hint Mode ! to IsGraph doesn't actually reduce typeclass search much in practice, since almost all of the time Coq will still search for Is2Graph, etc.

I agree with this. I didn't want to dramatically transform the library in one PR, so I thought it was best to make one small change (to IsGraph) and fix the breakages. But you're right that only removing one of the instances will have no effect as long as typeclass search continues for the other ones.

And I don't think it will be feasible to use Hint Mode ! on all wild category structures without a major overhaul.

This made me curious about how much work it would take. I have created a branch of this PR at patrick-nicodemus/HoTT called "hint_mode_wildcat" where I use Hint Mode for the type parameter of almost all of the wildcat instances. (If there is more than one type parameter, as in the case of functors, then I only make one of the type parameters into a ! to prevent completely blind search.)
So it looks like:

Hint Mode IsGraph ! : typeclass_instances.
Hint Mode Is01Cat ! - : typeclass_instances.
Hint Mode Is0Gpd ! - - : typeclass_instances.
Hint Mode Is0Functor + - - - - : typeclass_instances.
Hint Mode Is2Graph ! - : typeclass_instances.
Hint Mode Is1Cat ! - - - : typeclass_instances.
Hint Mode HasMorExt ! - - - - : typeclass_instances.
Hint Mode Is1Functor + - - - - - - - - - - - : typeclass_instances.
Hint Mode Is1Gpd ! - - - - - : typeclass_instances.
Hint Mode Is1Natural ! - - - - - - - - - - - : typeclass_instances.

Here is the most recent commit if you want to see the overall size of the changes that have to be made. https://github.com/patrick-nicodemus/HoTT/tree/hint_mode_wildcat

Two somewhat big changes to make things work: I redefined <~>* as a notation for CatEquiv in the category of pointed types, and I defined GroupIsomorphism as the Canonical element of HasEquivs Group. The rest are minor local fixes.

I should note that I didn't go through and diagnose the exact reason for each build error, I think this would be valuable information. I figured the first step is to fix it, and then I can go back afterwards and worry about why it broke in the first place.

I ran a timing test and the difference in runtimes was negligible. So apparently it does not affect performance much. I still think that these changes will result in fewer breakages due to refactoring on average. (This was my original motivation, because I kept breaking things when I was trying to refactor (2,1)-categories - rapply spinning, etc)

[jdchristensen]

I have created a branch of this PR at patrick-nicodemus/HoTT called "hint_mode_wildcat" where I use Hint Mode for the type parameter of almost all of the wildcat instances.

Thanks for doing this! I think we have to decide to either go fully in with this approach, using Hint Mode ! or + on all of the classes, or not do it at all, so your new branch is very valuable.

The changes are much less than I expected. But it's still the case that various things become just slightly more awkward. Being able to smoothly apply WildCat lemmas to situations not using WildCat notation is really valuable, and I'm reluctant to impose these "papercuts" on all uses of the WildCat library, especially since there still don't seem to be any concrete benefits. You've mentioned challenges while refactoring, but most of the time people are proving things, and we want that to be as easy as possible.

My suggestion is that we focus on changes that will make the typeclass search more efficient. For example, we can use priorities/costs more. Also, instead of importing all of WildCat, we should be selective, so we don't have the wildcat structures on Unit and Empty in the typeclass database, cluttering up the search. And at the top of a file, we can re-add important instances to the database, so they come first in the search. Etc.

[patrick-nicodemus]

Assuming we decide not to merge this PR, would you be willing to merge many of the "paper cuts" in this PR on the grounds that these are "accidents waiting to happen", i.e. the things changed in this PR identify things that could possibly break later during refactoring? This would have no effect on the end user. Many of the changes are not too ugly, they are little one line fixes, sometimes a single character.

[jdchristensen]

To me, a lot of the changes clutter things up, so I would have a preference to not make them. A few would be fine, e.g. changing {a b} to {a b : A} is perfectly reasonable and probably helps the reader. And changing rapply fmap_comp. to := fmap_comp _ _ _. is an improvement. I think most of the others are better left undone. That's just my opinion, and I'd like to hear what @Alizter thinks.

I've changed my mind, so I'm retracting my approval.

[Alizter]

I have marked the changes we can take from here. Let's open a new PR as to keep the discussion on point. This PR was about proposing Hint Mode and it seems it wasn't successful due to reasons we don't fully understand. Please open a new PR with the changes I marked, since they are a net readability improvement.

[Alizter]

Leave this

[Alizter]

this

[Alizter]

these

[Alizter]

these

[jdchristensen]

This PR was about proposing Hint Mode and it seems it wasn't successful due to reasons we don't fully understand.

I don't agree with this summary. @patrick-nicodemus has shown that it is possible to use Hint Mode for all of the main wildcat classes. But it requires various minor annotations, and I think it's clear why: when a goal doesn't specifically use wildcat definitions, typeclass search has no way of knowing which instances will make the Hom types match the morphism types in the goal. So I think there's a legitimate decision here between reducing undirected type class search vs making it convenient to apply wildcat results to non-wildcat goals. I'm leaning towards keeping the latter convenient.

Either way, we've also learned about how to reduce the amount of typeclass search, and I'll make a PR soon with a few minor changes illustrating this.

I agree that some of the changes in this PR should also be made in a separate PR. Your list seems like a pretty reasonable subset to choose.

[patrick-nicodemus]

I may have said this before but the VSCode Coq plugin does not yet support the very useful feature of interrupting a tactic that is taking a long time to run, so typeclass searches that loop or take exponential time to run require me to kill VSCode and reopen it. This irritation has been in mind when opening these related PR's. I think I'll switch back to ProofGeneral until that feature gets added, because otherwise interactive development with this library becomes quite painful. (Even "Check fmap11" can cause a typeclass loop and halt development since fmap11 has so many maximally inserted implicit arguments.)

[Alizter]

If you use coq-lsp you can just do Restart coq-lsp.

[jdchristensen]

@patrick-nicodemus Thanks again for experimenting with this. It's been very useful. But I think we should close this now. Sound good?

[patrick-nicodemus]

@jdchristensen Sounds good, it's a little disappointing but I understand the criticism expressed. If I continue to run into breakages while refactoring, I might propose another PR in the same spirit, but I'll keep in mind that the policy is not to compromise on the strength of elaboration of newly proved theorems.

[JasonGross]

And I don't think it will be feasible to use Hint Mode ! on all wild category structures without a major overhaul.

One possible way to avoid this issue is that you can stick all the hints in a module, and only import it in files where the hints help, if it is feasible, for example, inside the wildcats library but not outside