Remove some Global Instances

[jdchristensen]

I was noticing some slow typeclass search, and saw that a few things were being tried that were either futile (because Coq would have to guess something) or caused a loop (which Coq seemed to at least notice and cut short). This PR removes them from the global database, without needing to change any proofs. I was hoping the build would be faster, but there is no noticeable change. Still, this might let us use rapply in places where we were forced to use nrapply combined with some specific exact _ lines.

I also have a question. Consider the following:

Require Import HoTT.

Definition lem (k : trunc_index) (X : pType) `{IsConnected k X} (Y : Type) : Contr (X -> Y).
Admitted.  (* Not a true statement.  Just an example. *)

Definition test (m : nat) (X : pType) `{Univalence} (Y : Type) : Contr (X -> Y).
Proof.
  Typeclasses eauto := debug.
  try refine (lem m.+1 _).

On the last line, Coq does typeclass inference, and the part that was slow before this PR involves:

Debug: 1: looking for (IsConnected (Tr m.+1) ?X) with backtracking

Is there a way to tell Coq to not bother doing typeclass search if we don't know what X is? Coq ends up on a bit of a wild goose chase trying to find various modalities, etc. Because X is pointed, it explores things involving the unit_name map.

I also wonder why Coq is even attempting typeclass search. Note that the type of refine (lem m.+1 X) is forall Y, Contr (X -> Y), which does not match the type of the goal. Is there a reason that Coq does typeclass inference rather than just immediately noticing the problem and giving up? (This is not a silly thing to try, since our rapply tactic does exactly this before trying two underscores, which works.)

[CohenCyril]

not bother doing typeclass search if we don't know what X is?

Hint Mode IsConnected - !. will guarantee typeclass search only activates if the head symbol is not an evar.

[SkySkimmer]

I also wonder why Coq is even attempting typeclass search. Note that the type of refine (lem m.+1 X) is forall Y, Contr (X -> Y), which does not match the type of the goal. Is there a reason that Coq does typeclass inference rather than just immediately noticing the problem and giving up? (This is not a silly thing to try, since our rapply tactic does exactly this before trying two underscores, which works.)

Probably https://coq.inria.fr/doc/master/refman/addendum/type-classes.html#coq:flag.Typeclass-Resolution-For-Conversion
In general TC resolution may instantiate evars which can make a problem solvable.

[jdchristensen]

Hint Mode IsConnected - !. will guarantee typeclass search only activates if the head symbol is not an evar.

I tried both ! and + in the second position, and I still get

Debug: 1: looking for (IsConnected (Tr m.+1) ?X) with backtracking

with a full search after that.

[CohenCyril]

you may need: to add : typeclass_instances at the end:
Hint Mode IsConnected - ! : typeclass_instances.

[jdchristensen]

Hint Mode IsConnected - ! : typeclass_instances.

Thanks, it does the trick with +. I'm investigating whether this would work with the library.

[jdchristensen]

Probably https://coq.inria.fr/doc/master/refman/addendum/type-classes.html#coq:flag.Typeclass-Resolution-For-Conversion
In general TC resolution may instantiate evars which can make a problem solvable.

Thanks! With Unset Typeclass Resolution For Conversion. Coq completely avoids typeclass search in my example. Basics/* all build fine, but Types/Sigma.v has a problem, and I can't see why that particular line fails when other similar lines worked. So I'm not sure if we can have this unset for the whole library. I do expect it would make rapply a lot faster, by having it give up quickly until the right number of underscores have been inserted. Maybe someone else wants to give it a shot, adding that Unset to Overture.v.

[jdchristensen]

Hint Mode IsConnected - ! : typeclass_instances.

Thanks, it does the trick with +. I'm investigating whether this would work with the library.

It was easy to get the library to build with this change. I think I had to change four spots and in three of them I just filled in some underscores, which also made the proofs more readable. There was one spot in BlakersMassey where I couldn't see how to fix it, so I just temporarily switched back to -. The build time of the library doesn't change, though, so probably there's no point adding this hint.

[jdchristensen]

To get Hint Mode IsConnected - + : typeclass_instances. to work, there were five changes, and three were backwards compatible and clarified the proof, so I've just pushed those three changes. This will make it easier in case someone wants to explore this in the future. (The same hint might be good for IsTrunc and other things.)

[Alizter]

As it happens, I was trying to set up hint mode for wildcat. It's great to see it is useful elsewhere.

[jdchristensen]

As it happens, I was trying to set up hint mode for wildcat. It's great to see it is useful elsewhere.

Well, my summary of the situation is that it didn't speed anything up, and in a few cases it made typeclass search fail, so I was planning to not add this hint. (It does speed things up for the example I posted, but the changes in the first commit here also improve the example enough that it's not an issue anymore.)

[Alizter]

@jdchristensen I will continue to play with it for WildCat since it ought to be useful when resolving functoriality lemmas. There we do a lot of useless searches and need to prioritise what should be searched.

Other changes here however look good. FTR, how did you diagnose the original issue? With Typeclasses Debug?

[jdchristensen]

FTR, how did you diagnose the original issue? With Typeclasses Debug?

@Alizter I used Typeclasses eauto := debug <n>. for various n so I could see what was happening without getting overwhelmed. I also put a try in front of the failing refine because otherwise proof general would hide the debug output from me.