Wildcat rewriting tweaks

[patrick-nicodemus]

Using Hint Mode to change undesirable behavior of rapply Build_NatTrans

[patrick-nicodemus]

@Alizter I fixed some of the simpler breakages that result from this change but there's a proof that breaks downstream about classifying spaces and I don't really know how to fix it. It's a unification failure, I guess I can conjecture that since I removed one hint, another one was used to solve typeclass inference in this scenario, and it returns the "wrong" result and so the elaborated hint is incompatible with the goal.

Edit: this is fixed now.

[jdchristensen]

@patrick-nicodemus Can you explain the motivation for the two Hint Mode commands? In this library they seem to make a couple of things more awkward, so it would be good to know what things are made easier. Also, can you explain the choices of -, + and ! in those commands and what they will do?

[patrick-nicodemus]

@jdchristensen Hi, yeah. I was going to do this but I talked to Ali C. about it privately and forgot to post an explanation publicly. This is a change to how typeclass inference will behave when it's trying to solve a goal of the form in Is1Natural.

So, I was trying to build a natural transformation the other day and I tried apply Build_NatTrans. This failed, because apparently apply is designed to fail when it would generate goals containing metavariables, for example, if the goal is C and f : forall a : A, b : B a, C (where neither a, b are free in C) then the application of f would create goals ?X1 : A and ?X2 : B ?X1. So you have to use rapply in this situation, which is stronger and will create the metavariables.

rapply uses typeclass inference to fill in all the holes that it can. To me, the behavior of refine/rapply appears somewhat inconsistent on different kinds of goals. Consider the following code:

Section nondependent.
  Axiom (X B C: Type).
  Axiom (f : X -> B).
  Axiom (g : B -> C).
  Existing Class B.
  Existing Instance f.

  Goal C.
    rapply g.
(* Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,fail = false
   Debug: 1: looking for B without backtracking
   Debug: 1.1: simple apply f on B, 1 subgoal(s)
   Debug: 1.1-1 : X
   Debug: 1.1-1: looking for X without backtracking
   Debug: 1.1-1: no match for X, 0 possibilities

   After rapply, goal is B.*)
   Abort.
End nondependent.

Now compare:

Set Typeclasses Debug.
Section dependent.
  Axiom (X A C: Type).
  Axiom (B : A -> Type).
  Axiom (f1 : X -> A).
  Axiom (f2 : forall (x : X), B (f1 x)).
  Axiom (g : forall (a: A), B a -> C).
  Existing Class B.
  Existing Instance f2.
  Goal C.
    rapply g.
(* Debug:
   Calling typeclass resolution with flags: depth = ∞,unique = false,fail = false
   Debug: 1: looking for (B ?a) with backtracking
   Debug: 1.1: simple apply f2 on (B ?a), 0 subgoal(s)
   All the remaining goals are on the shelf. *)

    (* Goal is now X. *)
    Abort.

End dependent.

I call this "inconsistent" because I would expect both to generate subgoal X or to generate subgoals B and A,B respectively. Perhaps if typeclass resolution is trying to solve a goal B ?X1 containing a metavariable, and it finds a typeclass hint which can be unified with B ?X1 in a way that solves/instantiates the metavariable, then it regards this as a "success" and it does not backtrack. It doesn't matter if you use rapply or srapply. nrapply does work, but there are some contexts where you want typeclass inference to solve as many of the goals as possible. typeclasses eauto also has this same behavior of "succeeding" when it solves for a metavariable in a goal, without backtracking.

I view the behavior in the dependent section as usually undesirable. If I am writing some automation and try rapply g, and X is not provable, then it will backtrack to before rapply g and try a different hint altogether, when I really want to backtrack to the point where I can search for proofs of A and B ?X1, or continue the typeclass search looking for a complete solution. In this particular situation,

Record NatTrans {A B : Type} `{IsGraph A} `{Is1Cat B} {F G : A -> B}
  {ff : Is0Functor F} {fg : Is0Functor G} := {
  #[reversible=no]
  trans_nattrans :> F $=> G;
  is1natural_nattrans : Is1Natural F G trans_nattrans;
}.
(...)
Global Existing Instance is1natural_nattrans.

Calling rapply Build_NatTrans creates two goals ?X1 : F $=> G and ?X2 : Is1Natural F G ?X1. tries this hint is1natural_nattrans, which succeeds in resolving the metavariable ?X1 and creates the goal NatTrans, leading to a cycle. Similarly, later on, there is a hint that the underlying transformation of a NatEquiv Is1Natural, and so you get this annoying behavior where rapply Build_NatTrans creates a goal of type NatEquiv.

I think that this can be blamed on this non-backtracking behavior of typeclass resolution when it resolves unification variables. I'm not sure if this can be configured. What can be configured is to simply tell typeclass resolution not to try and resolve certain unification variables, and this is what Hint Mode does. The typeclass family Is1Natural is parametrized by twelve arguments, and Hint Mode lets you mark each index of the class to specify whether typeclass resolution is allowed to instantiate unification variables in that argument when unifying with hints in the typeclass database. The default behavior of typeclass resolution is to instantiate any/all of them (symbolized by -). The + means that typeclass should not try and solve for any unification variables in that argument when unifying with hints in the typeclass database. I think the term "mode" comes from logic programming, where an input argument to a predicate is one whose value drives the predicate and controls pattern matching, and an output argument is one that is or contains metavariables which can be set by the predicate. The ! is a halfway point in between them, it allows unification of a typeclass hint A -> B (F a b c) if the typeclass goal is B (F ?X1 ?X2 ?X3), but not with B (?X) or B (?X a b c), the metavariable can't appear in the head.

So, I have weakened typeclass inference so that hints like is1natural_nattrans are not used on a goal of type Is1Natural F G t unless the underlying transformation t is already known to be the trans_nattrans projection of some NatTrans and similarly the hint associated to NatEquiv for Is1Natural F G t will not be applied unless is already known to be the underlying transformation of a NatEquiv. I'm not sure how helpful this will be, but I think it would be worth experimenting with in a side branch and getting some feedback on the utility.

The other line of code referencing is1natural_nattrans is a mistake and I have removed it. I thought you might be able to control the unification behavior of specific hints, but no, you can only control the unification behavior of all hints with the goal.

[jdchristensen]

@patrick-nicodemus , thanks for the detailed explanation! That is strange behaviour that you show in the two examples. I noticed that if you add Local Set Typeclasses Strict Resolution. before the second example, that makes it behave like the first. This setting is used in Basics/Overture.v, but not in any other file, and I'm not sure what the motivation is for that. But could it be another way to solve the problem you are talking about? Should we be using it more?

The loop you describe involving rapply Build_NatTrans. is not good, but I don't understand why this doesn't happen in many places throughout the library where a field is also an instance. For example, I would have thought it would happen when you do rapply Build_Equiv. with the goal A <~> B, but it doesn't. Can you show an example of this looping, either an artificial one or one involving Build_NatTrans?

I don't completely understand the two hints you added, with one being on the Class and one being on an Instance. I also don't understand your comment The other line of code referencing is1natural_nattrans is a mistake and I have removed it. Maybe you just haven't removed it yet?

The impact on the library is the main thing I don't understand. E.g. take line 379 of Adjoint.v. Before this change, both rapply and nrapply worked there. After this change, rapply spins. I thought the purpose of this change was to prevent loops and make typeclass resolution fail sooner, so I don't understand what is going on there. Can we arrange things so that an (unnecessary) rapply still works there?

I'm also not sure why line 584 of ClassifyingSpace.v needed to change. If a "wrong" hint is being found, it would be good to know what it is and see if we can prevent the problem instead of working around it. That said, that line in the master branch was slow, and your proposed line is much faster. And it can be made a bit cleaner looking:

rapply (is1natural_prewhisker (G:=opyon X) B (opyoneda _ _ _)).

Neither of these are deal breakers, but it would be nice to know why this change makes some things fail that worked before.

[patrick-nicodemus]

I don't completely understand the two hints you added, with one being on the Class and one being on an Instance. I also don't understand your comment The other line of code referencing is1natural_nattrans is a mistake and I have removed it. Maybe you just haven't removed it yet?

Yes, I forgot to push it after making the commit, sorry.

[patrick-nicodemus]

E.g. take line 379 of Adjoint.v. Before this change, both rapply and nrapply worked there. After this change, rapply spins. I thought the purpose of this change was to prevent loops and make typeclass resolution fail sooner, so I don't understand what is going on there. Can we arrange things so that an (unnecessary) rapply still works there?

The change has both positive and negative effects, I think. I described the intended positives in the post. The negative is that it weakens typeclass inference by making these hints inapplicable when it would be convenient and appropriate for them to be applicable. I believe that the infinite loops are due to exposing pre-existing cycles in the typeclass hint database - it's not allowed to apply the appropriate hint which would solve the problem, so it goes to the next hint, and eventually discovers a cycle. I debugged one of these and the cycle was apparently due to typeclass hints Is1StrongCat -> Is1Cat and Is1Cat + HasMorExt -> Is1StrongCat. (This cycle is presumably known because one of the hints has priority 1000, I guess so that the cycle only happens in the case where no valid solution can be found.)

[patrick-nicodemus]

Local Set Typeclasses Strict Resolution. before the second example, that makes it behave like the first. This setting is used in Basics/Overture.v, but not in any other file, and I'm not sure what the motivation is for that. But could it be another way to solve the problem you are talking about? Should we be using it more?

From the documentation for that flag it seems that Set Typeclasses Strict Resolution should be basically identical to adding

Class ABC (x : X) (y : Y) (z : Z) := (...)
Hint Mode ABC + + + : typeclass_instances

to every class defined in the file. I tested this by swapping one for the other in the definition of Equiv. This created about a dozen fixes, about 10 of which are due to the fact that these flags result in different shelving/unshelving behaviors for typeclass resolution and are easily fixable by adding the word "unshelve" in the right spot. The other two errors are more complicated and it's not immediately clear what is causing them.

File "./theories/Colimits/Colimit.v", line 197, characters 9-46:
Error:
In environment
H : Funext
G : Graph
D : Diagram G
Y : Type
The term "isequiv_inverse (equiv_colimit_rec Y)" has type
 "IsEquiv (equiv_colimit_rec Y)^-1" while it is expected to have type
 "IsEquiv (cocone_postcompose (cocone_colimit D))".

File "./theories/Cubical/PathCube.v", line 266, characters 13-28:
Error:
In environment
A : Type
a00, a10, a01, a11 : A
px0 : a00 = a10
px1 : a01 = a11
p0x : a00 = a01
p1x : a10 = a11
s, s' : PathSquare px0 px1 p0x p1x
The term "(eisretr tr ?Goal)^" has type "?Goal = tr (tr^-1 ?Goal)"
while it is expected to have type "?Goal = tr (tr hr)".

The loop you describe involving rapply Build_NatTrans. is not good, but I don't understand why this doesn't happen in many places throughout the library where a field is also an instance. For example, I would have thought it would happen when you do rapply Build_Equiv. with the goal A <~> B, but it doesn't. Can you show an example of this looping, either an artificial one or one involving Build_NatTrans?

Equiv is defined in the overture under the Local Set Typeclasses Strict Resolution flag, so we've disabled that unification.
I'm using the term "looping" a bit loosely here, as it doesn't cause rapply itself to loop, it causes rapply to create a new goal which is identical to the current goal and return, so if rapply Build_NatTrans was applied in a loop by auto or similar until failure, this would cause a loop.

[jdchristensen]

@patrick-nicodemus Thanks for pointing out the obvious explanation of why this doesn't happen with Equiv. But I'm still surprised it doesn't happen more for other structures.

And thanks for pointing out that loop in typeclass search. We try to avoid any possibilities of loops. The library builds if we use Hint Immediate is1cat_is1cat_strong : typeclass_instances. instead of making it an instance, so we should do that I think. This will probably fix the loop you found, although I didn't check.

I was looking at the loop on line 379 of Adjoint.v if rapply is used. It seems to do a lot of search for Is0Functor ?F, so I tried Hint Mode Is0Functor - - - - ! : typeclass_instances., but that didn't help. For some reason, even when Coq should know the parameter F, it is doing typeclass search with it as a meta-variable, which then aborts (with the above hint), which then causes more search. This happened in lots of places in the library where the F was obvious from the goal. So my conclusion from this experiment is that while it seems like it should be good to use ! in many cases, it seems to break typeclass search in practice for reasons I don't understand. And this matches what is happening with the proposed change to Is1Natural, except that since it is used rarely, it only caused a few problems.

For that spot in ClassifyingSpace.v, with the original rapply command, Coq is getting similarly confused about Is0Functor. Without the hint mentioned above, the debug log contains things like:

7: looking for (Is0Functor ?F) with backtracking
7.1: simple apply @is0functor_cat_bincoprod_r on (Is0Functor ?F), 0 subgoal(s)

which is a wild goose chase. But with the hint, it still fails to choose F correctly and still does some unnecessary search before failing. How can we prevent this fruitless search while still having Coq succeed in straightforward situations? Maybe we need some bidirectionality hints (Arguments foo ... & ...)? I'm not that familiar with those, but a bit of experimenting didn't find anything helpful.

My summary of the situation is that Hint Mode settings cause legitimate searches to fail, and that because of the choices of instances in the WildCat library, this then leads to fruitless searches. So I'm hesitant to add these Hint Mode commands unless I see ways in which they improve the library.

@Alizter It seems like the typeclass search we have in WildCat has too any instances that cause unnecessary search when the "obvious" solutions aren't found (e.g. when they are limited by Hint Mode, but even in other cases). Can this be improved?

[Alizter]

Something non-obvious that I should state is that multiple hint modes can be given for a term. I believe they are all tried in order. That might help with obvious ones that are not picked up. I haven't been able to check in detail however.

Regarding there being too many typeclass instances, I agree. We can and should try pruning them. Previous attempts ran into proofs breaking in unexpected ways which makes this line of exploration less appetising.

There is a setting for typeclasses which requires a unique solution. However we can't have multiple typeclass databases which means things like truncation overlap and fail. It's not clear what the best way forward with this is.

[jdchristensen]

I'm not sure yet whether we should go ahead with this change. The diff is now pretty small, so it's not a big deal to incorporate it, but it's hard to say whether it will help or hinder future work using natural transformations.

If we do go ahead, I would suggest two things:

• Add a comment before the Hint Mode command briefly explaining what it does, exactly which argument is affected, and why this has been done, maybe with a reference to this PR for further details.
• Squash the commits before merge.

[Alizter]

Yes, I concur that we should experiment a bit more with this. I still don't have a proper understanding of the situation but I will take some time to do so soon.