Redundent typeclasses

[Alizter]

We have redundant typeclasses littered through out the library. Dan Christensen has observed the following:

I did a test, and it definitely causes Coq to duplicate its search through the sub-tree. If you think about it, there's no efficient way for Coq to avoid this. It would have to cache every state it has been in through the search, and then compare each new state to the states in the cache up to definitional equality, which is an expensive test in general. Moreover, each redundant path multiplies the slow down. So we definitely want to avoid redundant typeclass instances. My test code is below.

Require Import HoTT.

Class Class1 := { dummy1 : nat }.

Class Class2 := { dummy2 : Empty }.

Class Class3 := { dummy3 : Type }.

Axiom ax12 : Class1 -> Class2.

Axiom ax23 : Class2 -> Class3.

Global Existing Instance ax12.

Global Existing Instance ax23.

Set Typeclasses Debug.

Definition test1 : Class1 -> Class3 := _.
(* 11 lines of output. *)

Definition test2 : Unit -> Class3.
Proof.
  refine _.
  (* 10 lines of output *)
Abort.

Global Instance ax12' : Class1 -> Class2 := _.

Definition test2 : Unit -> Class3.
Proof.
  refine _.
  (* 21 lines of output *)
Abort.

Global Instance ax23' : Class2 -> Class3 := _.

Definition test2 : Unit -> Class3.
Proof.
  refine _.
  (* 32 lines of output, 2^2 cases tried. *)
Abort.

Originally posted by @jdchristensen in https://github.com/HoTT/HoTT/pull/1312

[Alizter]

We should try to clean up some of these instances as they could be causing speed issues in various places.

[spitters]

I believe this is a problem that lean4 is trying to solve. @mattam82 This may be a good test case.