Revert "Revert "Add more instances for type.related""

This reverts commit 29f1c8b447294b4a0a6a5127c6db23d54d43343f.

Try to be more judicious about instances

After     | File Name                                                            | Before    || Change    | % Change
--------------------------------------------------------------------------------------------------------------------
23m59.08s | Total                                                                | 23m59.43s || -0m00.35s | -0.02%
--------------------------------------------------------------------------------------------------------------------
6m01.99s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples                   | 6m01.02s  || +0m00.97s | +0.26%
4m33.50s  | Experiments/NewPipeline/Toplevel1                                    | 4m33.17s  || +0m00.32s | +0.12%
3m55.15s  | Experiments/NewPipeline/RewriterRulesGood                            | 3m55.63s  || -0m00.47s | -0.20%
1m42.17s  | Experiments/NewPipeline/Toplevel2                                    | 1m41.96s  || +0m00.20s | +0.20%
1m15.45s  | Experiments/NewPipeline/RewriterWf2                                  | 1m15.27s  || +0m00.18s | +0.23%
0m41.06s  | Experiments/NewPipeline/AbstractInterpretationWf                     | 0m41.12s  || -0m00.05s | -0.14%
0m38.69s  | p521_32.c                                                            | 0m38.51s  || +0m00.17s | +0.46%
0m37.17s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 0m37.32s  || -0m00.14s | -0.40%
0m35.00s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 0m34.57s  || +0m00.42s | +1.24%
0m32.11s  | p521_64.c                                                            | 0m32.07s  || +0m00.03s | +0.12%
0m24.43s  | Experiments/NewPipeline/UnderLetsProofs                              | 0m24.43s  || +0m00.00s | +0.00%
0m23.61s  | p384_32.c                                                            | 0m23.62s  || -0m00.01s | -0.04%
0m21.24s  | Experiments/NewPipeline/LanguageWf                                   | 0m21.60s  || -0m00.36s | -1.66%
0m20.37s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 0m21.14s  || -0m00.76s | -3.64%
0m18.59s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 0m18.89s  || -0m00.30s | -1.58%
0m13.57s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 0m13.87s  || -0m00.29s | -2.16%
0m10.33s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m10.58s  || -0m00.25s | -2.36%
0m08.70s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m08.63s  || +0m00.06s | +0.81%
0m08.65s  | p384_64.c                                                            | 0m08.48s  || +0m00.16s | +2.00%
0m05.44s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m05.38s  || +0m00.06s | +1.11%
0m05.36s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.50s  || -0m00.13s | -2.54%
0m04.57s  | Experiments/NewPipeline/RewriterWf1                                  | 0m04.56s  || +0m00.01s | +0.21%
0m04.18s  | Experiments/NewPipeline/AbstractInterpretationProofs                 | 0m04.20s  || -0m00.02s | -0.47%
0m03.98s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m03.90s  || +0m00.08s | +2.05%
0m03.96s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m04.00s  || -0m00.04s | -1.00%
0m03.92s  | Experiments/NewPipeline/MiscCompilerPassesProofs                     | 0m03.86s  || +0m00.06s | +1.55%
0m03.88s  | secp256k1_32.c                                                       | 0m03.79s  || +0m00.08s | +2.37%
0m03.74s  | p256_32.c                                                            | 0m03.76s  || -0m00.01s | -0.53%
0m03.16s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m03.37s  || -0m00.20s | -6.23%
0m02.16s  | curve25519_32.c                                                      | 0m02.15s  || +0m00.01s | +0.46%
0m02.10s  | p224_32.c                                                            | 0m02.10s  || +0m00.00s | +0.00%
0m01.68s  | p224_64.c                                                            | 0m01.68s  || +0m00.00s | +0.00%
0m01.54s  | p256_64.c                                                            | 0m01.57s  || -0m00.03s | -1.91%
0m01.50s  | secp256k1_64.c                                                       | 0m01.65s  || -0m00.14s | -9.09%
0m01.39s  | Experiments/NewPipeline/CLI                                          | 0m01.35s  || +0m00.03s | +2.96%
0m01.37s  | curve25519_64.c                                                      | 0m01.37s  || +0m00.00s | +0.00%
0m01.23s  | Experiments/NewPipeline/StandaloneHaskellMain                        | 0m01.25s  || -0m00.02s | -1.60%
0m01.22s  | Experiments/NewPipeline/StandaloneOCamlMain                          | 0m01.21s  || +0m00.01s | +0.82%
0m00.92s  | Experiments/NewPipeline/RewriterProofs                               | 0m00.91s  || +0m00.01s | +1.09%

1 files changed, 19 insertions, 4 deletions

diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v
index 9c1c24a22..55c763dc1 100644
--- a/src/Experiments/NewPipeline/LanguageWf.v
+++ b/src/Experiments/NewPipeline/LanguageWf.v
@@ -38,18 +38,33 @@ Module Compilers.
       Context {base_type} {interp_base_type : base_type -> Type}.
       Local Notation eqv := (@type.related base_type interp_base_type (fun _ => eq)).
 
-      Global Instance eqv_Symmetric {t} : Symmetric (@eqv t) | 10.
-      Proof. induction t; cbn [type.eqv type.interp] in *; repeat intro; eauto. Qed.
+      Local Instance related_Symmetric {t} {R : forall t, relation (interp_base_type t)}
+             {R_sym : forall t, Symmetric (R t)}
+        : Symmetric (@type.related base_type interp_base_type R t) | 100.
+      Proof.
+        cbv [Symmetric] in *;
+          induction t; cbn [type.related type.interp] in *; repeat intro; eauto.
+      Qed.
 
-      Global Instance eqv_Transitive {t} : Transitive (@eqv t) | 10.
+      Local Instance related_Transitive {t} {R : forall t, relation (interp_base_type t)}
+             {R_sym : forall t, Symmetric (R t)}
+             {R_trans : forall t, Transitive (R t)}
+        : Transitive (@type.related base_type interp_base_type R t) | 100.
       Proof.
-        induction t; cbn [eqv]; [ exact _ | ].
+        induction t; cbn [type.related]; [ exact _ | ].
         cbv [respectful]; cbn [type.interp].
         intros f g h Hfg Hgh x y Hxy.
         etransitivity; [ eapply Hfg; eassumption | eapply Hgh ].
         etransitivity; first [ eassumption | symmetry; eassumption ].
       Qed.
+
+      Global Instance eqv_Transitive {t} : Transitive (@eqv t) | 10 := _.
+      Global Instance eqv_Symmetric {t} : Symmetric (@eqv t) | 10 := _.
     End eqv.
+    Hint Extern 100 (Symmetric (@type.related ?base_type ?interp_base_type ?R ?t))
+    => (tryif has_evar R then fail else simple apply (@related_Symmetric base_type interp_base_type t R)) : typeclass_instances.
+    Hint Extern 100 (Transitive (@type.related ?base_type ?interp_base_type ?R ?t))
+    => (tryif has_evar R then fail else simple apply (@related_Transitive base_type interp_base_type t R)) : typeclass_instances.
 
     Section app_curried_instances.
       Context {base_type} {base_interp : base_type -> Type}.