I have a project with some custom automation to construct instances for a type class.

The automation uses 'notypeclasses refine' to apply recursive rules.

I've just noticed that in contexts with a large number of variables (around ~120 in scope in one example), the individual calls to 'notypeclasses refine' become slow. Is this expected? I only recent learned of 'autoapply', which does not seem to suffer from this (or at least, much less). My suspicion is that 'notypeclasses refine (some_term _ _ _ _ _)' will have to create and unify a bunch of evars, and that 'autoapply @some_term' is smarter about this?

I will try to replace 'notypeclasses refine' with 'autoapply' and see if this breaks things (old vs new unification..?). Here is a somewhat minimal example.

```
Inductive TCEq_par {A : Type} (x : A) : A -> A -> A -> A -> A -> A -> A -> Prop :=
TCEq_refl y1 y2 y3 y4 y5 y6 : TCEq_par x y1 y2 y3 y4 y5 y6 x.
Lemma TCEq_sym {A : Type} (x x' : A) y1 y2 y3 y4 y5 y6 : TCEq_par x' y1 y2 y3 y4 y5 y6 x -> TCEq_par x y1 y2 y3 y4 y5 y6 x'.
Proof. destruct 1. constructor. Qed.
Existing Class TCEq_par.
#[local] Existing Instance TCEq_refl.
Require Import Vector.
Lemma useless_variable P A :
(forall (n : nat) (v : Vector.t A n), P) ->
P.
Proof.
exact (fun f => f O (Vector.nil _)).
Qed.
Ltac introduce_dep_vars :=
apply (useless_variable _ nat); intros ??.
Lemma test : exists y1 y2 y3 y4 y5 y6, TCEq_par O y1 y2 y3 y4 y5 y6 O.
Proof.
do 6 eexists.
do 100 introduce_dep_vars. (* also try with this line commented out completely *)
time do 30 (notypeclasses refine (TCEq_sym _ _ _ _ _ _ _ _ _)).
time do 30 (autoapply @TCEq_sym with typeclass_instances).
Abort.
```

cc @Janno

Last updated: Jun 23 2024 at 04:03 UTC