From 35dd2416817de53140970a3776f1fbf1729a9b2f Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 8 Apr 2025 21:34:22 +0200
Subject: [PATCH 01/33] [TC] primitive constructor for fold in instance
 (pre-)compilation

---
 apps/tc/elpi/ho_compile.elpi    | 4 +++-
 apps/tc/elpi/ho_precompile.elpi | 3 ++-
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index fd6b6f599..d56537b51 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/ho_compile.elpi
@@ -23,7 +23,7 @@ namespace tc {
         decompile-term-aux (pglobal _ _ as T) L T' L :- !, copy T T', !.
         decompile-term-aux (sort _ as T) L T' L :- !, copy T T', !.
         decompile-term-aux (uvar as X) L X L :- !.
-        decompile-term-aux (primitive _ as P) L P L :- !.
+        decompile-term-aux (primitive _ as X) L X L :- !.
 
         decompile-term-aux (tc.maybe-eta-tm T S) (pr [X|XS] L1) Y (pr XS' [NL | L2]) :- !,
           name Y X S,
@@ -328,6 +328,8 @@ namespace tc {
         get-uva-pair-arity Y L Z.
 
       pred decompile-problematic-term i:term, i:list prop, o:term, o:list prop.
+      decompile-problematic-term (primitive _ as C) A C A :- !.
+      
       decompile-problematic-term (tc.maybe-eta-tm T S) L V [tc.link.eta V T' | L2] :-
         prune V S, !, fold-map T L T' L2.
 
diff --git a/apps/tc/elpi/ho_precompile.elpi b/apps/tc/elpi/ho_precompile.elpi
index f2bf4a9f4..c6c95043f 100644
--- a/apps/tc/elpi/ho_precompile.elpi
+++ b/apps/tc/elpi/ho_precompile.elpi
@@ -105,6 +105,7 @@ namespace tc {
       precompile-aux _ (global _ as C) A C A :- !.
       precompile-aux _ (pglobal _ _ as C) A C A :- !.
       precompile-aux _ (sort _ as C) A C A :- !.
+      precompile-aux _ (primitive _ as C) A C A :- !.
 
       % Detect maybe-eta term
       % TODO: should I precompile also the type of the fun and put it in the output term
@@ -142,7 +143,6 @@ namespace tc {
       %   precompile-aux IsP Ty A Ty1 A1, pi x\ is-name x => precompile-aux IsP (F x) A1 (F1 x) A2.
       % precompile-aux IsP (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
       %   precompile-aux IsP T A T1 A1, precompile-aux IsP Rty A1 Rty1 A2, std.fold-map B A2 (precompile-aux IsP) B1 A3.
-      precompile-aux _ (primitive _ as C) A C A :- !.
       % precompile-aux IsP (uvar M L as X) A W A1 :- var X, !, std.fold-map L A (precompile-aux IsP) L1 A1, coq.mk-app-uvar M L1 W.
       % % when used in CHR rules
       % precompile-aux IsP (uvar X L) A (uvar X L1) A1 :- std.fold-map L A (precompile-aux IsP) L1 A1.
@@ -226,6 +226,7 @@ namespace tc {
       precompile-aux (global _ as C) A C A :- !.
       precompile-aux (pglobal _ _ as C) A C A :- !.
       precompile-aux (sort _ as C) A C A :- !.
+      precompile-aux (primitive _ as C) A C A :- !.
 
       % Detect maybe-eta term
       precompile-aux (fun Name Ty B as T) N (tc.maybe-eta-tm (fun Name Ty' B') Scope) M :-

From 4f60635141ff4c79efd11495dd045cec36f8bf0e Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 2 Jul 2024 16:54:44 +0200
Subject: [PATCH 02/33] [TC] canonical proj solved with coq.unify-eq

---
 apps/tc/elpi/ho_compile.elpi     |   5 ++
 apps/tc/elpi/ho_precompile.elpi  |   4 +-
 apps/tc/elpi/tc_aux.elpi         |   6 ++
 apps/tc/tests/canonical_struct.v | 102 +++++++++++++++++++++++++++++++
 4 files changed, 116 insertions(+), 1 deletion(-)
 create mode 100644 apps/tc/tests/canonical_struct.v

diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index d56537b51..be75b5aa3 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/ho_compile.elpi
@@ -24,6 +24,11 @@ namespace tc {
         decompile-term-aux (sort _ as T) L T' L :- !, copy T T', !.
         decompile-term-aux (uvar as X) L X L :- !.
         decompile-term-aux (primitive _ as X) L X L :- !.
+        decompile-term-aux (tc.canonical-projection T S _) (pr [X|Xs] L1) Y (pr Xs' L3) :- !,
+          name Y X S,
+          decompile-term-aux T (pr Xs L1) T' (pr Xs' L2),
+          P = coq.unify-eq Y T' ok,
+          L3 = [P | L2].
 
         decompile-term-aux (tc.maybe-eta-tm T S) (pr [X|XS] L1) Y (pr XS' [NL | L2]) :- !,
           name Y X S,
diff --git a/apps/tc/elpi/ho_precompile.elpi b/apps/tc/elpi/ho_precompile.elpi
index c6c95043f..be27e32b5 100644
--- a/apps/tc/elpi/ho_precompile.elpi
+++ b/apps/tc/elpi/ho_precompile.elpi
@@ -106,6 +106,8 @@ namespace tc {
       precompile-aux _ (pglobal _ _ as C) A C A :- !.
       precompile-aux _ (sort _ as C) A C A :- !.
       precompile-aux _ (primitive _ as C) A C A :- !.
+      precompile-aux _ (app [global (const C) | _] as T) A (tc.canonical-projection T Scope N) (s A) :- coq.env.projection? C N, !, free-var Scope.
+      precompile-aux _ (app [primitive (proj P _) | _] as T) A (tc.canonical-projection T Scope 0) (s A) :- coq.env.primitive-projection? P _, !, free-var Scope.
 
       % Detect maybe-eta term
       % TODO: should I precompile also the type of the fun and put it in the output term
@@ -173,7 +175,7 @@ namespace tc {
                 (tc.prod-range (prod _ T Bo) 3)
               since x is applied at most 3 times in Bo
                 ==> This helps charging the right number of `eta-link` for map-deduplication rule
-        N is the number of problematic terms in T
+        N is the number of problematic terms in T + nb of projections
     */
     pred instance i:term, o:term, o:nat, o:list univ, o:list univ-instance.
     instance T T' N UnivConstL UnivInstL :-
diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
index 940c0d442..2d878f53c 100644
--- a/apps/tc/elpi/tc_aux.elpi
+++ b/apps/tc/elpi/tc_aux.elpi
@@ -222,3 +222,9 @@ namespace tc {
     list term ->     % The eta-expanded version of X, from X^{len(PF)} to X^{len(PF)+len(NPF)}
     term.
 }
+
+type tc.canonical-projection
+  term ->       % The current precompiled subterm
+  list term ->  % The list of FV in the precomp subterm
+  int ->
+  term.
\ No newline at end of file
diff --git a/apps/tc/tests/canonical_struct.v b/apps/tc/tests/canonical_struct.v
new file mode 100644
index 000000000..838c10d3d
--- /dev/null
+++ b/apps/tc/tests/canonical_struct.v
@@ -0,0 +1,102 @@
+From elpi.apps Require Import tc.
+
+Module CS1.
+
+  Structure ofe := Ofe {
+    ofe_car :> Type;
+  }.
+  Canonical ofe_nat : ofe := Ofe nat.
+
+  Class C (I : Type).
+
+  Instance c : C (ofe_car ofe_nat). Qed.
+  Goal C (Ofe nat). apply _. Qed. (* No CS search *)
+  Goal exists x, C (Ofe x). eexists. apply _. Qed. (* CS Search to assign x *)
+  Goal C (ofe_car ofe_nat). apply _. Qed.
+
+End CS1.
+
+Module CS2.
+  Structure ofe := Ofe {
+    ofe_car :> Type;
+  }.
+  Canonical ofe_nat : ofe := Ofe nat.
+
+  Class C (I : Type).
+
+  Instance c : C (Ofe nat). Qed.
+  Goal C (Ofe nat). apply _. Qed. (* No CS search *)
+  Goal exists x, C (Ofe x). eexists. apply _. Qed. (* CS Search to assign x *)
+  Goal C (ofe_car ofe_nat). apply _. Qed.
+
+End CS2.
+
+(* With primitive projection *)
+Module CS3.
+  Class C (I : Type).
+
+  #[local] Set Primitive Projections.
+  Structure ofe := Ofe {
+    ofe_car :> Type;
+  }.
+  Canonical ofe_nat : ofe := Ofe nat.
+
+  Instance c : C ofe_nat.(ofe_car). Qed.
+  Goal C (Ofe nat). apply _. Qed. (* No CS search *)
+  Goal exists x, C (Ofe x). eexists. apply _. Qed. (* CS Search to assign x *)
+  Goal C (ofe_car ofe_nat). apply _. Qed.
+
+End CS3.
+
+Module CS4.
+  Class C (I : Type).
+
+  #[local] Set Primitive Projections.
+  Structure ofe := Ofe {
+    ofe_car :> Type;
+  }.
+  Canonical ofe_nat : ofe := Ofe nat.
+
+  Instance c : C (Ofe nat).(ofe_car). Qed.
+  Goal C (Ofe nat). apply _. Qed. (* No CS search *)
+  Goal exists x, C (Ofe x). eexists. apply _. Qed. (* CS Search to assign x *)
+  Goal C (ofe_car ofe_nat). apply _. Qed.
+
+End CS4.
+
+(* With bound variables *)
+Module CS5.
+  Structure ofe := Ofe {
+    ofe_car :> Type;
+  }.
+  Canonical ofe_any x : ofe := Ofe x.
+
+  Class C (I : Type -> Type).
+  Axiom f : ofe -> Type.
+
+  Instance c X : C (fun x => (Ofe (f (X x)))). Qed.
+  Goal C (fun x => (Ofe (f x))). apply _. Qed. (* No CS search *)
+  Goal C (fun (_: Type) => Ofe (f nat)). apply _. Qed. (* CS Search to assign x *)
+  Goal exists X, C (fun y => ofe_car (X y)). eexists.
+    apply _.
+    Unshelve.
+    apply (ofe_any nat).
+  Qed.
+
+  Lemma coq_unif_fail: exists X Y, (fun (y: Type) => ofe_car (X y)) = (fun _ => Y).
+    do 2 eexists.
+    Fail reflexivity.
+  Abort.
+    
+  Goal exists Z, C (fun _ => Z). eexists.
+    (* 
+      Note that here, coq8.20 unification algorithm would fail to unify
+      with error 
+        Unable to unify "?Y" with "ofe_car (?X x)" as "ofe_car (?X x)" 
+        contains local variables.
+    *)
+    apply _.
+    Unshelve.
+    apply (ofe_any nat).
+  Qed.
+End CS5.
\ No newline at end of file

From 30de9b139e4dc1eb046795cad9a94b152fbbb3b0 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 3 Jul 2024 13:17:45 +0200
Subject: [PATCH 03/33] [TC] clean-term also for tc.canonical-projection

---
 apps/tc/elpi/ho_compile.elpi | 1 +
 1 file changed, 1 insertion(+)

diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index be75b5aa3..430b0f017 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/ho_compile.elpi
@@ -121,6 +121,7 @@ namespace tc {
       pred clean-term i:term, o:term.
       clean-term A B :-
         (pi t s r \ copy (tc.maybe-eta-tm  t s) r :- !, copy t r, !) =>
+        (pi t s r \ copy (tc.canonical-projection t s _) r :- !, copy t r, !) =>
         (pi t s r \ copy (tc.prod-range t s) r :- !, copy t r, !) =>
         (pi t s r \ copy (tc.maybe-llam-tm t s) r :- !, copy t r, !) =>
           std.assert!  (copy A B) "[TC] clean-term error".

From caadc9511b75b153f99a5022c44a36f314786a3c Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 10 Jul 2024 14:08:18 +0200
Subject: [PATCH 04/33] [TC] compilation of primitive projections to their
 compatibility constants

---
 apps/tc/elpi/ho_compile.elpi     |  5 +++--
 apps/tc/tests/canonical_struct.v | 21 ++++++++++++++++++++-
 2 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index 430b0f017..786c6d6ae 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/ho_compile.elpi
@@ -23,7 +23,7 @@ namespace tc {
         decompile-term-aux (pglobal _ _ as T) L T' L :- !, copy T T', !.
         decompile-term-aux (sort _ as T) L T' L :- !, copy T T', !.
         decompile-term-aux (uvar as X) L X L :- !.
-        decompile-term-aux (primitive _ as X) L X L :- !.
+        decompile-term-aux (primitive (proj P _)) L (global (const Y)) L :- !, coq.env.primitive-projection? P Y.
         decompile-term-aux (tc.canonical-projection T S _) (pr [X|Xs] L1) Y (pr Xs' L3) :- !,
           name Y X S,
           decompile-term-aux T (pr Xs L1) T' (pr Xs' L2),
@@ -334,7 +334,8 @@ namespace tc {
         get-uva-pair-arity Y L Z.
 
       pred decompile-problematic-term i:term, i:list prop, o:term, o:list prop.
-      decompile-problematic-term (primitive _ as C) A C A :- !.
+      decompile-problematic-term (primitive (proj P _)) A (global (const Y)) A :- !, 
+        coq.env.primitive-projection? P Y.
       
       decompile-problematic-term (tc.maybe-eta-tm T S) L V [tc.link.eta V T' | L2] :-
         prune V S, !, fold-map T L T' L2.
diff --git a/apps/tc/tests/canonical_struct.v b/apps/tc/tests/canonical_struct.v
index 838c10d3d..1a36e4330 100644
--- a/apps/tc/tests/canonical_struct.v
+++ b/apps/tc/tests/canonical_struct.v
@@ -99,4 +99,23 @@ Module CS5.
     Unshelve.
     apply (ofe_any nat).
   Qed.
-End CS5.
\ No newline at end of file
+End CS5.
+
+Module CS6.
+  #[projections(primitive=yes)]
+  Structure ofe := Ofe { ofe_car : Type; }.
+
+  #[projections(primitive=no)] (* TODO: Putting primitive to yes leads to a unification error. Why? *)
+  Structure cmra := { cmra_car :> Type; }.
+  Canonical Structure cmra_ofeO (A : cmra) : ofe := Ofe A.
+
+  Class C (I : Type).
+  Instance c : forall (A : ofe), C ((A).(ofe_car)) := {}.
+
+  Section s.
+    Context {cmra : cmra}.
+    Goal C (cmra_car cmra).
+      apply _.
+    Qed.
+  End s.
+End CS6.

From cdf26f9c6835bb946be311fb9ade0d8e4ba5d742 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 10 Jul 2024 16:26:57 +0200
Subject: [PATCH 05/33] Revert "[TC] compilation of primitive projections to
 their compatibility constants"

This reverts commit 6c639781fd4e3818332fc73fe205e1d52eeb321d.
---
 apps/tc/elpi/ho_compile.elpi     |  5 ++---
 apps/tc/tests/canonical_struct.v | 21 +--------------------
 2 files changed, 3 insertions(+), 23 deletions(-)

diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index 786c6d6ae..430b0f017 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/ho_compile.elpi
@@ -23,7 +23,7 @@ namespace tc {
         decompile-term-aux (pglobal _ _ as T) L T' L :- !, copy T T', !.
         decompile-term-aux (sort _ as T) L T' L :- !, copy T T', !.
         decompile-term-aux (uvar as X) L X L :- !.
-        decompile-term-aux (primitive (proj P _)) L (global (const Y)) L :- !, coq.env.primitive-projection? P Y.
+        decompile-term-aux (primitive _ as X) L X L :- !.
         decompile-term-aux (tc.canonical-projection T S _) (pr [X|Xs] L1) Y (pr Xs' L3) :- !,
           name Y X S,
           decompile-term-aux T (pr Xs L1) T' (pr Xs' L2),
@@ -334,8 +334,7 @@ namespace tc {
         get-uva-pair-arity Y L Z.
 
       pred decompile-problematic-term i:term, i:list prop, o:term, o:list prop.
-      decompile-problematic-term (primitive (proj P _)) A (global (const Y)) A :- !, 
-        coq.env.primitive-projection? P Y.
+      decompile-problematic-term (primitive _ as C) A C A :- !.
       
       decompile-problematic-term (tc.maybe-eta-tm T S) L V [tc.link.eta V T' | L2] :-
         prune V S, !, fold-map T L T' L2.
diff --git a/apps/tc/tests/canonical_struct.v b/apps/tc/tests/canonical_struct.v
index 1a36e4330..838c10d3d 100644
--- a/apps/tc/tests/canonical_struct.v
+++ b/apps/tc/tests/canonical_struct.v
@@ -99,23 +99,4 @@ Module CS5.
     Unshelve.
     apply (ofe_any nat).
   Qed.
-End CS5.
-
-Module CS6.
-  #[projections(primitive=yes)]
-  Structure ofe := Ofe { ofe_car : Type; }.
-
-  #[projections(primitive=no)] (* TODO: Putting primitive to yes leads to a unification error. Why? *)
-  Structure cmra := { cmra_car :> Type; }.
-  Canonical Structure cmra_ofeO (A : cmra) : ofe := Ofe A.
-
-  Class C (I : Type).
-  Instance c : forall (A : ofe), C ((A).(ofe_car)) := {}.
-
-  Section s.
-    Context {cmra : cmra}.
-    Goal C (cmra_car cmra).
-      apply _.
-    Qed.
-  End s.
-End CS6.
+End CS5.
\ No newline at end of file

From de1dac5fe91b8f81b73d3b5681e390414d4fa859 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Fri, 12 Jul 2024 14:16:22 +0200
Subject: [PATCH 06/33] [TC] put cnonical projection in tc namespace

---
 apps/tc/elpi/tc_aux.elpi | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
index 2d878f53c..e6248e450 100644
--- a/apps/tc/elpi/tc_aux.elpi
+++ b/apps/tc/elpi/tc_aux.elpi
@@ -221,10 +221,10 @@ namespace tc {
     term ->          % The current precompiled subterm: shape is app[app[X,PF],NPF]
     list term ->     % The eta-expanded version of X, from X^{len(PF)} to X^{len(PF)+len(NPF)}
     term.
-}
 
-type tc.canonical-projection
-  term ->       % The current precompiled subterm
-  list term ->  % The list of FV in the precomp subterm
-  int ->
-  term.
\ No newline at end of file
+  type canonical-projection
+    term ->       % The current precompiled subterm
+    list term ->  % The list of FV in the precomp subterm
+    int ->
+    term.
+}
\ No newline at end of file

From 0ca09cdd42c13140091af30e1d000a4ba9856039 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 8 Apr 2025 21:35:43 +0200
Subject: [PATCH 07/33] remove reduntant calls to Elpi Typecheck

---
 apps/tc/theories/add_commands.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/apps/tc/theories/add_commands.v b/apps/tc/theories/add_commands.v
index 822436593..d5caaf979 100644
--- a/apps/tc/theories/add_commands.v
+++ b/apps/tc/theories/add_commands.v
@@ -19,6 +19,7 @@ Set Warnings "+elpi".
 Elpi Command TC.AddAllInstances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
+Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
 Elpi Accumulate File ho_precompile.
 Elpi Accumulate File unif.

From 8a5a53ce1820f8a1aed094e77479e8fac29ec4b8 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 8 Apr 2025 21:37:16 +0200
Subject: [PATCH 08/33] [TC] local binders in evar scope during precompile +
 link.cs

---
 apps/tc/elpi/base.elpi           |   5 ++
 apps/tc/elpi/ho_compile.elpi     |  29 +++++--
 apps/tc/elpi/ho_link.elpi        |  62 +++++++++++++++
 apps/tc/elpi/ho_precompile.elpi  |  14 +++-
 apps/tc/elpi/solver.elpi         |   1 +
 apps/tc/elpi/tc_aux.elpi         |   8 ++
 apps/tc/tests/canonical_struct.v | 131 ++++++++++++++++++++++++++++++-
 apps/tc/tests/test.v             |  53 ++++++++++++-
 8 files changed, 290 insertions(+), 13 deletions(-)

diff --git a/apps/tc/elpi/base.elpi b/apps/tc/elpi/base.elpi
index b0df94dca..76dbf04a5 100644
--- a/apps/tc/elpi/base.elpi
+++ b/apps/tc/elpi/base.elpi
@@ -163,3 +163,8 @@ pred close-term-no-prune-ty i:(term -> list prop), i:term, o:list prop.
 close-term-no-prune-ty (x\ []) _ [] :- !.
 close-term-no-prune-ty (x\ [X x | Xs x]) Ty [@pi-decl `x` Ty x\ X x | Xs'] :- !, 
   close-term-no-prune-ty Xs Ty Xs'. 
+
+pred close-term-no-prune-fun i:(term -> list term), i:term, o:list term.
+close-term-no-prune-fun (x\ []) _ [] :- !.
+close-term-no-prune-fun (x\ [X x | Xs x]) Ty [fun _ Ty X | Xs'] :- 
+  close-term-no-prune-fun Xs Ty Xs'.
diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index 430b0f017..fc2cdd2f7 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/ho_compile.elpi
@@ -24,10 +24,15 @@ namespace tc {
         decompile-term-aux (sort _ as T) L T' L :- !, copy T T', !.
         decompile-term-aux (uvar as X) L X L :- !.
         decompile-term-aux (primitive _ as X) L X L :- !.
+        decompile-term-aux (tc.coercion T S) (pr [X|Xs] L1) Y (pr Xs' L3) :- !,
+          name Y X S,
+          decompile-term-aux T (pr Xs L1) T' (pr Xs' L2),
+          P = tc.link.cs Y T',
+          L3 = [P | L2].
         decompile-term-aux (tc.canonical-projection T S _) (pr [X|Xs] L1) Y (pr Xs' L3) :- !,
           name Y X S,
           decompile-term-aux T (pr Xs L1) T' (pr Xs' L2),
-          P = coq.unify-eq Y T' ok,
+          P = tc.link.cs Y T',
           L3 = [P | L2].
 
         decompile-term-aux (tc.maybe-eta-tm T S) (pr [X|XS] L1) Y (pr XS' [NL | L2]) :- !,
@@ -124,6 +129,7 @@ namespace tc {
         (pi t s r \ copy (tc.canonical-projection t s _) r :- !, copy t r, !) =>
         (pi t s r \ copy (tc.prod-range t s) r :- !, copy t r, !) =>
         (pi t s r \ copy (tc.maybe-llam-tm t s) r :- !, copy t r, !) =>
+        (pi t s r \ copy (tc.coercion t s) r :- !, copy t r, !) =>
           std.assert!  (copy A B) "[TC] clean-term error".
 
       pred main 
@@ -316,6 +322,8 @@ namespace tc {
 
       %                    Type     Var    Cnt    uvar-pair-list
       pred make-pairs-aux i:term, i:term, o:list prop.
+      make-pairs-aux Ty (fun _ _ IBo) L' :- !,
+        pi x\ make-pairs-aux Ty (IBo x) (L x), close-prop-no-prune L L'.
       make-pairs-aux (prod _ Ty Bo) V [pi x\ uvar-pair x Ty X' :- x == V, ! | L] :- !,
         pi x\ make-pairs-aux (Bo x) X' L.
       make-pairs-aux _ _ [].
@@ -335,11 +343,18 @@ namespace tc {
 
       pred decompile-problematic-term i:term, i:list prop, o:term, o:list prop.
       decompile-problematic-term (primitive _ as C) A C A :- !.
-      
-      decompile-problematic-term (tc.maybe-eta-tm T S) L V [tc.link.eta V T' | L2] :-
-        prune V S, !, fold-map T L T' L2.
 
-      decompile-problematic-term (tc.prod-range T _) A T' A' :-
+      % there is no need to decompile T since no precompilation is done inside coercions
+      decompile-problematic-term (tc.coercion T S) L1 Y [tc.link.cs Y T|L1] :- !,
+        prune Y S.
+      % there is no need to decompile T since no precompilation is done inside CS
+      decompile-problematic-term (tc.canonical-projection T S _) L1 Y [tc.link.cs Y T|L1] :- !,
+        prune Y S.
+
+      decompile-problematic-term (tc.maybe-eta-tm T S) L V [tc.link.eta V T' | L2] :- !,
+        prune V S, fold-map T L T' L2.
+
+      decompile-problematic-term (tc.prod-range T _) A T' A' :- !,
         fold-map T A T' A'.
 
       decompile-problematic-term (tc.maybe-llam-tm (app [app[H|S] | NPF]) Sc) L Z [NL|L'] :- !,
@@ -399,6 +414,10 @@ namespace tc {
         build-eta-links-of-vars-aux Hd S L',
         build-eta-links-of-vars Vars L'',
         std.append L' L'' L.
+      build-eta-links-of-vars [fun _ Ty Bo|Vars] L :-
+        (pi x\ build-eta-links-of-vars [Bo x] (L' x), close-term-no-prune-ty L' Ty L''),
+        build-eta-links-of-vars Vars L''',
+        std.append L'' L''' L.
     }
     
     %          Goal    Goal'      Links
diff --git a/apps/tc/elpi/ho_link.elpi b/apps/tc/elpi/ho_link.elpi
index fe4105019..6dda51718 100644
--- a/apps/tc/elpi/ho_link.elpi
+++ b/apps/tc/elpi/ho_link.elpi
@@ -130,6 +130,62 @@ namespace tc {
       }
     }
 
+    namespace cs {
+      pred cs i:term, i:term.
+      % TODO: suspend link on vars in T
+      cs V T :- var V, !, get-vars T Vars, declare_constraint (cs V T) [_, V | Vars].
+      cs T1 T2 :- coq.unify-eq T1 T2 ok.
+
+      % pred unify-rebinding-names i:list prop, i:list prop, i:term, i:term.
+      % unify-rebinding-names [] T1 [] T2 (unify-eq T1V T2) :- !, copy T1 T1V.
+      % unify-rebinding-names [N|NS] T1 [V|VS] T2 C :- !, copy N V => unify-rebinding-names NS T1 VS T2 C.
+      % unify-rebinding-names [] T1 VS T2 C :- !, unify-rebinding-names [] {coq.subst-prod VS T1} [] T2 C. % FIXME: reduction
+      % unify-rebinding-names [_|NS] (prod _ _ F) [] T2 C :- !,                      % FIXME: reduction
+      %   assert! (pi x\ F x = F1) "restriction bug", unify-rebinding-names NS F1 [] T2 C.
+
+      pred unify-under-ctx i:list term, i:list term, i:term, i:term, i:term, i:term.
+      unify-under-ctx [] [] A B V1 V2 :- copy A A', copy V1 V1', !, coq.unify-eq A' B ok, !, V1' = V2.
+      unify-under-ctx [X|XS] [Y|YS] A B V1 V2:- (copy X Y :- !) => unify-under-ctx XS YS A B V1 V2.
+
+      % TODO: there could be two same variables suspended on non unifyable
+      % terms, this should be detected and raise a failure.
+      % An example of this is in test/canonical_struct.v
+      constraint cache def decl coq.unify-eq ?- solve-cs cs {
+        rule solve-cs \ (Ctx ?- cs A B) <=> (Ctx => coq.unify-eq A B ok).
+        rule (Ctx1 ?- cs (uvar A L1 as X) T1) \ (Ctx2 ?- cs (uvar A L2 as Y) T2) <=>
+          (Ctx2 => unify-under-ctx L1 L2 T1 T2 X Y).
+        rule \ solve-cs.
+      }
+    }
+
+    namespace cs {
+      pred cs i:term, i:term.
+      % TODO: suspend link on vars in T
+      cs V T :- var V, !, get-vars T Vars, declare_constraint (cs V T) [_, V | Vars].
+      cs T1 T2 :- coq.unify-eq T1 T2 ok.
+
+      % pred unify-rebinding-names i:list prop, i:list prop, i:term, i:term.
+      % unify-rebinding-names [] T1 [] T2 (unify-eq T1V T2) :- !, copy T1 T1V.
+      % unify-rebinding-names [N|NS] T1 [V|VS] T2 C :- !, copy N V => unify-rebinding-names NS T1 VS T2 C.
+      % unify-rebinding-names [] T1 VS T2 C :- !, unify-rebinding-names [] {coq.subst-prod VS T1} [] T2 C. % FIXME: reduction
+      % unify-rebinding-names [_|NS] (prod _ _ F) [] T2 C :- !,                      % FIXME: reduction
+      %   assert! (pi x\ F x = F1) "restriction bug", unify-rebinding-names NS F1 [] T2 C.
+
+      pred unify-under-ctx i:list term, i:list term, i:term, i:term, i:term, i:term.
+      unify-under-ctx [] [] A B V1 V2 :- copy A A', copy V1 V1', !, coq.unify-eq A' B ok, !, V1' = V2.
+      unify-under-ctx [X|XS] [Y|YS] A B V1 V2:- (copy X Y :- !) => unify-under-ctx XS YS A B V1 V2.
+
+      % TODO: there could be two same variables suspended on non unifyable
+      % terms, this should be detected and raise a failure.
+      % An example of this is in test/canonical_struct.v
+      constraint cache def decl coq.unify-eq ?- solve-cs cs {
+        rule solve-cs \ (Ctx ?- cs A B) <=> (Ctx => coq.unify-eq A B ok).
+        rule (Ctx1 ?- cs (uvar A L1 as X) T1) \ (Ctx2 ?- cs (uvar A L2 as Y) T2) <=>
+          (Ctx2 => unify-under-ctx L1 L2 T1 T2 X Y).
+        rule \ solve-cs.
+      }
+    }
+
     pred eta i:term, i:term.
     eta A B :- eta.eta A B.
 
@@ -141,5 +197,11 @@ namespace tc {
 
     pred solve-llam.
     solve-llam :- declare_constraint solve-llam [_].
+
+    pred cs i:term, i:term.
+    cs A B :- cs.cs A B.
+
+    pred solve-cs.
+    solve-cs :- declare_constraint solve-cs [_].
   }
 }
\ No newline at end of file
diff --git a/apps/tc/elpi/ho_precompile.elpi b/apps/tc/elpi/ho_precompile.elpi
index be27e32b5..cf9612988 100644
--- a/apps/tc/elpi/ho_precompile.elpi
+++ b/apps/tc/elpi/ho_precompile.elpi
@@ -106,6 +106,7 @@ namespace tc {
       precompile-aux _ (pglobal _ _ as C) A C A :- !.
       precompile-aux _ (sort _ as C) A C A :- !.
       precompile-aux _ (primitive _ as C) A C A :- !.
+      precompile-aux _ T A (tc.coercion T Scope) (s A) :- coq.safe-dest-app T HD _, tc.coercion-unify HD, !, free-var Scope.
       precompile-aux _ (app [global (const C) | _] as T) A (tc.canonical-projection T Scope N) (s A) :- coq.env.projection? C N, !, free-var Scope.
       precompile-aux _ (app [primitive (proj P _) | _] as T) A (tc.canonical-projection T Scope 0) (s A) :- coq.env.primitive-projection? P _, !, free-var Scope.
 
@@ -229,12 +230,20 @@ namespace tc {
       precompile-aux (pglobal _ _ as C) A C A :- !.
       precompile-aux (sort _ as C) A C A :- !.
       precompile-aux (primitive _ as C) A C A :- !.
+      
+      precompile-aux T A (tc.coercion T Scope) A :- 
+        coq.safe-dest-app T HD _, tc.coercion-unify HD, !, names Scope.
+      precompile-aux (app [global (const C) | _] as T) A (tc.canonical-projection T Scope N) A :- 
+        coq.env.projection? C N, !, names Scope.
+      precompile-aux (app [primitive (proj P _) | _] as T) A (tc.canonical-projection T Scope 0) A :- 
+        coq.env.primitive-projection? P _, !, names Scope.
+
 
       % Detect maybe-eta term
       precompile-aux (fun Name Ty B as T) N (tc.maybe-eta-tm (fun Name Ty' B') Scope) M :-
         maybe-eta T, !,
         names Scope,
-        (pi x\ precompile-aux (B x) N (B' x) M'),
+        std.assert! (pi x\ precompile-aux (B x) N (B' x) (MM x), close-term-no-prune-fun MM Ty M') "[TC] should not fail1",
         precompile-aux Ty M' Ty' M.
 
       % Detect maybe-beta term
@@ -244,10 +253,9 @@ namespace tc {
         names Scope1,
         std.fold-map NPF N precompile-aux NPF1 M. 
 
-      % In the goal there are 
       precompile-aux (prod Name Ty B) N (tc.prod-range (prod Name Ty' B') (r-ar z MaxAr)) P :- !,
         count-prod Ty MaxAr,
-        std.assert! (pi x\ precompile-aux (B x) N (B' x) M) "[TC] should not fail",
+        std.assert! (pi x\ precompile-aux (B x) N (B' x) (MM x), close-term-no-prune-fun MM Ty M) "[TC] should not fail2",
         precompile-aux Ty M Ty' P.
 
       % Working with fun
diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi
index 97596e4ed..7a61aed70 100644
--- a/apps/tc/elpi/solver.elpi
+++ b/apps/tc/elpi/solver.elpi
@@ -32,6 +32,7 @@ namespace tc {
     if-true print-compiled-goal (coq.say "[TC] the compiled goal is" Q), !,
     tc.time-it tc.oTC-time-instance-search (
       do PostProcess, Q,
+      tc.link.solve-cs,
       tc.link.solve-eta, % Trigger eta links
       tc.link.solve-llam % Trigger llam links
     ) "instance search".
diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
index e6248e450..aaee96ffb 100644
--- a/apps/tc/elpi/tc_aux.elpi
+++ b/apps/tc/elpi/tc_aux.elpi
@@ -227,4 +227,12 @@ namespace tc {
     list term ->  % The list of FV in the precomp subterm
     int ->
     term.
+
+  :index (5)
+  pred coercion-unify i:term.
+
+  type coercion
+    term ->
+    list term ->
+    term.
 }
\ No newline at end of file
diff --git a/apps/tc/tests/canonical_struct.v b/apps/tc/tests/canonical_struct.v
index 838c10d3d..8df1b417a 100644
--- a/apps/tc/tests/canonical_struct.v
+++ b/apps/tc/tests/canonical_struct.v
@@ -99,4 +99,133 @@ Module CS5.
     Unshelve.
     apply (ofe_any nat).
   Qed.
-End CS5.
\ No newline at end of file
+End CS5.
+
+Module CS6.
+  Structure ofe := Ofe { ofe_car :> Type; }.
+  Structure cmra := Cmra { cmra_car :> Type; }.
+
+  Coercion cmra_ofeO (A : cmra) := Ofe A.
+
+  Elpi Accumulate tc.db lp:{{
+    tc.coercion-unify {{cmra_ofeO}}.
+  }}.
+
+  Canonical Structure ofe_nat := Ofe nat.
+  Canonical Structure cmra_nat := Cmra nat.
+
+  Class C (i: ofe).
+
+  Instance i: forall (c : cmra), C (cmra_ofeO c) := {}.
+
+  Goal C ofe_nat.
+    apply _.
+  Qed.
+End CS6.
+
+Module CS7.
+  Structure ofe := Ofe { ofe_car :> Type; }.
+  Structure cmra := Cmra { cmra_car :> Type; }.
+
+  Coercion cmra_ofeO (A : cmra) := Ofe A.
+
+  Elpi Accumulate tc.db lp:{{
+    tc.coercion-unify {{cmra_ofeO}}.
+  }}.
+
+  Canonical Structure ofe_bool := Ofe bool.
+  Canonical Structure cmra_bool := Cmra bool.
+
+  Class C (i: ofe).
+
+  Class D (i: Type).
+  Instance d : D bool := {}.
+
+  Instance i: forall (c : cmra), D (cmra_car c) -> C (cmra_ofeO c) := {}.
+  Elpi Print TC.Solver.
+
+  Goal C ofe_bool.
+    apply _.
+  Qed.
+
+  Canonical Structure ofe_nat := Ofe nat.
+  Canonical Structure cmra_nat := Cmra nat.
+
+  Goal exists a, C a.
+    eexists.
+    apply _.
+  Qed.
+End CS7.
+
+Module CS8.
+  Structure ofe := Ofe { ofe_car :> Type; }.
+  Canonical Structure ofe_bool := Ofe bool.
+  Class C (i : Type).
+  Instance i : C ofe_bool := {}.
+
+  (* 
+    Test for constraint activation using tc.link.solve-cs: After
+    tc-instance-search, we have the suspended goal `tc.link.cs X ofe_bool` that
+    must be activated. This activation need to load the context before the 
+    call to unify-eq since we need to load the type of `x`
+  *)
+  Goal forall (x: nat), exists X, C X.
+    eexists. apply _.
+  Qed.
+
+  (* TODO: error in llam link *)
+  (* Goal forall (x: nat), exists X, C (X x).
+    eexists.
+    Elpi Trace Browser.
+    (* Elpi TC Solver Deactivate TC.Solver. *)
+    apply _.
+  Qed *)
+End CS8.
+
+Module CS9.
+  Structure ofe := Ofe { ofe_car :> Type; }.
+  Canonical Structure ofe_bool := Ofe bool.
+  Canonical Structure ofe_nat := Ofe nat.
+
+  Class loop.
+  Instance l : loop -> loop := {}.
+  Class C (i : Type) (i : Type).
+  Instance i : loop -> C ofe_bool ofe_nat := {}.
+
+  (* 
+    Here we have two suspended goal on X with cs links. The same variable
+    is linked with ofe_bool and ofe_nat. Since they don't unfy, the instance
+    `i` cannot be used.
+  *)
+  Goal exists X, C X X.
+    eexists.
+    Fail apply _.
+  Abort.
+End CS9.
+
+Module CS10.
+  Structure ofe := Ofe { ofe_car :> Type; }.
+  Canonical Structure ofe_bool := Ofe bool.
+
+  Class C (i : Type).
+  Instance i : C bool := {}.
+
+  (* Here the projection is in the goal *)
+  Goal C (ofe_car ofe_bool). apply _. Qed.
+End CS10.
+
+Module CS11.
+  Structure ofe := Ofe { ofe_car :> Type; }.
+  Canonical Structure ofe_bool := Ofe bool.
+
+  Class D (i : ofe).
+  Instance d : D (ofe_bool) := {}.
+
+  Class C (i : Type).
+  Instance i X:  D X -> C (ofe_car X) := {}.
+
+  (* Here the projection is in the goal *)
+  Goal exists X, C (ofe_car X). eexists.
+    apply _.
+    Show Proof.
+  Qed.
diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v
index 8ecbe3094..0a6303e41 100644
--- a/apps/tc/tests/test.v
+++ b/apps/tc/tests/test.v
@@ -277,6 +277,54 @@ Module HO_10.
   Qed.
 End HO_10.
 
+Module HO_11.
+  Class Unit (i : Prop).
+  Instance i F : Unit (forall (f : Prop), F f) := {}.
+  Goal Unit (forall x, x).
+    apply _.
+  Qed.
+End HO_11.
+
+Module HO_12.
+  Class Unit (i : Prop).
+  Instance i : Unit (forall x, x) := {}.
+  Set Printing Existential Instances.
+  Goal forall (y: Prop), exists (F: Prop -> Prop), Unit (forall x, F x).
+    intros.
+    eexists ?[F].
+    Unshelve.
+    2: { refine (fun x => _); shelve. }
+    simpl.
+    Set Printing Existential Instances.
+    apply _.
+  Qed.
+End HO_12.
+
+Module HO_13.
+  Class Unit (i : Prop).
+  Class PP (i : Prop -> Prop -> Prop).
+  Axiom f : Prop -> Prop -> Prop.
+  Instance i F : PP (fun x y => F y x) -> Unit (forall (x y: Prop), F y x) := {}.
+  Instance j : PP (fun x y => f y x) := {}.
+  Check _ : (Unit (forall x y, _)).
+
+  Goal exists (X: Prop -> Prop -> Prop), Unit (forall x y, X x y).
+    eexists.
+    Unshelve.
+    2: { refine (fun _ _ => _); shelve. }
+    simpl.
+    apply _.
+  Qed.
+
+  Elpi Query TC.Solver lp:{{
+    std.spy-do![Goal = {{Unit (forall x y, lp:(F x y))}},
+    tc.build-query-from-goal Goal Proof Q PP,
+    do PP, Q,
+    std.assert! (Proof = {{i f j}}) "Error"].
+  }}.
+End HO_13.
+
+
 Module HO_scope_check1.
   Axiom f : Type -> (Type -> Type) -> Type.
   Axiom g : Type -> Type -> Type.
@@ -565,7 +613,4 @@ Module CoqUvar4.
     do 1 eexists.
     apply _.
   Qed.
-End CoqUvar4.
-
-(* TODO: add test with negative premise having a variable with type (M A) where M and A are coq uvar,
-         this is in order to clean-term with llam *)
\ No newline at end of file
+End CoqUvar4.
\ No newline at end of file

From ed1dda58ecde4c254f10363fe7bd2271e9d56a4c Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 8 Apr 2025 21:37:58 +0200
Subject: [PATCH 09/33] [TC] add TC.AddRecordFields command + better chr for
 canon struct

---
 apps/cs/README.md                |  2 +-
 apps/tc/elpi/ho_link.elpi        | 20 +++++++++++++++++---
 apps/tc/elpi/ho_precompile.elpi  | 15 +++++++++++++--
 apps/tc/elpi/solver.elpi         |  2 ++
 apps/tc/tests/canonical_struct.v |  8 ++++++--
 apps/tc/tests/test.v             |  8 ++++++++
 apps/tc/theories/add_commands.v  | 28 ++++++++++++++++++++++++++++
 apps/tc/theories/db.v            |  3 +++
 8 files changed, 78 insertions(+), 8 deletions(-)

diff --git a/apps/cs/README.md b/apps/cs/README.md
index 7c3679444..4693b7d93 100644
--- a/apps/cs/README.md
+++ b/apps/cs/README.md
@@ -16,7 +16,7 @@ The `cs` predicate lives in the database `cs.db`
 pred cs i:goal-ctx, o:term, o:term.
 ```
 
-By addings rules for this predicate one can recover from a CS instance search failure
+By adding rules for this predicate one can recover from a CS instance search failure
 error, that is when `Lhs` and `Rhs` are not unifiable using a canonical structure registered
 by Coq.
 
diff --git a/apps/tc/elpi/ho_link.elpi b/apps/tc/elpi/ho_link.elpi
index 6dda51718..cd85a20a1 100644
--- a/apps/tc/elpi/ho_link.elpi
+++ b/apps/tc/elpi/ho_link.elpi
@@ -131,10 +131,24 @@ namespace tc {
     }
 
     namespace cs {
+      pred reduce-cs i:term, i:term, i:term, i:constant.
+      reduce-cs V (app [ProjT, T]) Record Proj :-
+        coq.unify-eq T Record Err, Err = ok,
+        Q = [coq.redflags.const Proj],
+        coq.redflags.add coq.redflags.nored [coq.redflags.delta, coq.redflags.beta, coq.redflags.match | Q] RF,
+        @redflags! RF => coq.reduction.lazy.whd (app [ProjT, Record]) V',
+        not (V' = match _ _ _), !,
+        cs V V'.
+      reduce-cs V T _ _ :- V = T.
+
       pred cs i:term, i:term.
-      % TODO: suspend link on vars in T
-      cs V T :- var V, !, get-vars T Vars, declare_constraint (cs V T) [_, V | Vars].
-      cs T1 T2 :- coq.unify-eq T1 T2 ok.
+      cs T1 T2 :- not (var T1), !, coq.unify-eq T1 T2 ok.
+      cs (uvar _ as V) (app [_, Arg] as T) :- not (ground_term Arg), !, get-vars T Vars, declare_constraint (cs V T) [_, V | Vars].
+      cs (uvar _ as V) (app [HD | _] as T) :- 
+        if (HD = global (const Proj), tc.proj->record Proj Record)
+          (reduce-cs V T Record Proj)
+          (coq.unify-eq V T ok).
+      cs T1 T2 :- not (T2 = app _), !, coq.unify-eq T1 T2 ok.
 
       % pred unify-rebinding-names i:list prop, i:list prop, i:term, i:term.
       % unify-rebinding-names [] T1 [] T2 (unify-eq T1V T2) :- !, copy T1 T1V.
diff --git a/apps/tc/elpi/ho_precompile.elpi b/apps/tc/elpi/ho_precompile.elpi
index cf9612988..1449eb34b 100644
--- a/apps/tc/elpi/ho_precompile.elpi
+++ b/apps/tc/elpi/ho_precompile.elpi
@@ -224,6 +224,17 @@ namespace tc {
       split-pf [X|Xs] Old [X|Ys] L :- name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
       split-pf Xs _ [] Xs.
 
+      pred used i:term, i:term.
+      used X (uvar _ S) :- std.mem! S X, !.
+      used X (fun _ _ Bo) :- pi x\ used X (Bo x).
+
+      pred close-term-prune-safe-fun i:(term -> list term), i:term, o:list term.
+      close-term-prune-safe-fun (x\ []) _ [] :- !.
+      close-term-prune-safe-fun (x\ [X x | Xs x]) Ty [fun _ _ X | Xs'] :- 
+        pi x\ used x (X x), !, close-term-prune-safe-fun Xs Ty Xs'.
+      close-term-prune-safe-fun (x\ [X | Xs x]) Ty [X | Xs'] :-
+        close-term-prune-safe-fun Xs Ty Xs'.
+
       pred precompile-aux i:term, i:list term, o:term, o:list term.
       precompile-aux X A Y A :- name X, !, X = Y, !. % avoid loading "precompile-aux x A x A" at binders
       precompile-aux (global _ as C) A C A :- !.
@@ -243,7 +254,7 @@ namespace tc {
       precompile-aux (fun Name Ty B as T) N (tc.maybe-eta-tm (fun Name Ty' B') Scope) M :-
         maybe-eta T, !,
         names Scope,
-        std.assert! (pi x\ precompile-aux (B x) N (B' x) (MM x), close-term-no-prune-fun MM Ty M') "[TC] should not fail1",
+        std.assert! (pi x\ precompile-aux (B x) N (B' x) (MM x), close-term-prune-safe-fun MM Ty M') "[TC] should not fail1",
         precompile-aux Ty M' Ty' M.
 
       % Detect maybe-beta term
@@ -255,7 +266,7 @@ namespace tc {
 
       precompile-aux (prod Name Ty B) N (tc.prod-range (prod Name Ty' B') (r-ar z MaxAr)) P :- !,
         count-prod Ty MaxAr,
-        std.assert! (pi x\ precompile-aux (B x) N (B' x) (MM x), close-term-no-prune-fun MM Ty M) "[TC] should not fail2",
+        std.assert! (pi x\ precompile-aux (B x) N (B' x) (MM x), close-term-prune-safe-fun MM Ty M) "[TC] should not fail2",
         precompile-aux Ty M Ty' P.
 
       % Working with fun
diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi
index 7a61aed70..6e4a8b932 100644
--- a/apps/tc/elpi/solver.elpi
+++ b/apps/tc/elpi/solver.elpi
@@ -18,6 +18,7 @@ namespace tc {
   pred refine-proof i:term, i:goal, o:list sealed-goal.
   refine-proof tc.mode_fail G [seal G] :- !.
   refine-proof Proof G GL :-
+    if-true print-goal-after-search (coq.say "[TC] The goal after instance search is <<<" G ">>>"),
     if-true print-solution (coq.say "[TC] The proof is <<<" Proof ">>>"),
     if-true print-solution-pp (coq.say "[TC] The proof is <<<" {coq.term->string Proof} ">>>"),
       
@@ -65,6 +66,7 @@ namespace tc {
   pred print-solution-pp.   % Print the solution in coq pp
   pred print-goal.          % Print the goal in HOAS
   pred print-goal-pp.       % Print the goal with coq pp
+  pred print-goal-after-search.          % Print the goal in HOAS after instance search
   pred print-compiled-goal.
 
 }
\ No newline at end of file
diff --git a/apps/tc/tests/canonical_struct.v b/apps/tc/tests/canonical_struct.v
index 8df1b417a..86783b855 100644
--- a/apps/tc/tests/canonical_struct.v
+++ b/apps/tc/tests/canonical_struct.v
@@ -7,6 +7,8 @@ Module CS1.
   }.
   Canonical ofe_nat : ofe := Ofe nat.
 
+  TC.AddRecordFields (ofe) (Ofe) 1.
+
   Class C (I : Type).
 
   Instance c : C (ofe_car ofe_nat). Qed.
@@ -126,6 +128,8 @@ End CS6.
 Module CS7.
   Structure ofe := Ofe { ofe_car :> Type; }.
   Structure cmra := Cmra { cmra_car :> Type; }.
+  TC.AddRecordFields (ofe) (Ofe) 1.
+  TC.AddRecordFields (cmra) (Cmra) 1.
 
   Coercion cmra_ofeO (A : cmra) := Ofe A.
 
@@ -142,7 +146,6 @@ Module CS7.
   Instance d : D bool := {}.
 
   Instance i: forall (c : cmra), D (cmra_car c) -> C (cmra_ofeO c) := {}.
-  Elpi Print TC.Solver.
 
   Goal C ofe_bool.
     apply _.
@@ -206,6 +209,7 @@ End CS9.
 Module CS10.
   Structure ofe := Ofe { ofe_car :> Type; }.
   Canonical Structure ofe_bool := Ofe bool.
+  TC.AddRecordFields (ofe) (Ofe) 1.
 
   Class C (i : Type).
   Instance i : C bool := {}.
@@ -227,5 +231,5 @@ Module CS11.
   (* Here the projection is in the goal *)
   Goal exists X, C (ofe_car X). eexists.
     apply _.
-    Show Proof.
   Qed.
+End CS11.
\ No newline at end of file
diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v
index 0a6303e41..fae3a5266 100644
--- a/apps/tc/tests/test.v
+++ b/apps/tc/tests/test.v
@@ -289,6 +289,14 @@ Module HO_12.
   Class Unit (i : Prop).
   Instance i : Unit (forall x, x) := {}.
   Set Printing Existential Instances.
+
+  Elpi Accumulate TC.Solver lp:{{
+    % TODO: this rule should be removed if https://github.com/LPCIC/elpi/issues/256
+    % is solved
+    tc-elpi.apps.tc.tests.test.HO_12.tc-Unit {{forall (x:Prop), lp:(X x)}} {{i}} :-
+      X = (x\x).
+  }}.
+
   Goal forall (y: Prop), exists (F: Prop -> Prop), Unit (forall x, F x).
     intros.
     eexists ?[F].
diff --git a/apps/tc/theories/add_commands.v b/apps/tc/theories/add_commands.v
index d5caaf979..7c33b6105 100644
--- a/apps/tc/theories/add_commands.v
+++ b/apps/tc/theories/add_commands.v
@@ -143,8 +143,36 @@ Elpi Accumulate lp:{{
 }}.
 
 
+Elpi Command TC.AddRecordFields.
+Elpi Accumulate Db tc.db.
+Elpi Accumulate Db tc_options.db.
+Elpi Accumulate File base.
+Elpi Accumulate File tc_aux.
+Elpi Accumulate  lp:{{
+  pred tc.add_tc.records_unif.aux i:int, i:term, i:list term, i:constant, o:prop.
+  tc.add_tc.records_unif.aux 0 T Args ProjConstant P :- !,
+    coq.mk-app T Args T',
+    P = tc.proj->record ProjConstant T'.
+  tc.add_tc.records_unif.aux N T Args ProjConstant (pi x\ P x) :- N > 0, !,
+    N1 is N - 1, pi x\ tc.add_tc.records_unif.aux N1 T [x|Args] ProjConstant (P x).
+
+  pred tc.add_tc.records_unif.aux' i:option constant, i:term, i:int.
+  tc.add_tc.records_unif.aux' none _ _.
+  tc.add_tc.records_unif.aux' (some ProjConstant) RecordConstr N :-
+    tc.add_tc.records_unif.aux N RecordConstr [] ProjConstant P, tc.add-tc-db _ _ P.
+
+  pred tc.add_tc.records_unif i:term, o:term, i:int.
+  tc.add_tc.records_unif (global (indt K)) RecordConstr N :-
+    coq.env.projections K Projs,
+    std.forall Projs (x\ tc.add_tc.records_unif.aux' x RecordConstr N).
+
+  main [trm T1, trm T2, int N] :- !, tc.add_tc.records_unif T1 T2 N.
+  main L :- coq.error L.
+}}.
+Elpi Typecheck.
 
 Elpi Export TC.AddAllClasses.
+Elpi Export TC.AddRecordFields.
 Elpi Export TC.AddAllInstances.
 Elpi Export TC.AddClasses.
 Elpi Export TC.AddInstances.
diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
index b8571dd2b..451abe763 100644
--- a/apps/tc/theories/db.v
+++ b/apps/tc/theories/db.v
@@ -102,6 +102,9 @@ Elpi Db tc.db lp:{{
     pred link.eta i:term, i:term.
     pred link.llam i:term, i:term.
 
+
+    % relates a projection to the its record
+    pred proj->record i:constant, o:term.
   }
 }}.
 From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.

From b5ff427d753329b07ef89ceef8085bc6cdac3ba7 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Thu, 8 Aug 2024 12:25:23 +0200
Subject: [PATCH 10/33] [TC] mode ground with ground_term check + tc.link for
 coercions

---
 apps/tc/elpi/ho_link.elpi         | 4 ++++
 apps/tc/elpi/modes.elpi           | 2 ++
 apps/tc/tests/test_pending_mode.v | 8 ++++----
 3 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/apps/tc/elpi/ho_link.elpi b/apps/tc/elpi/ho_link.elpi
index cd85a20a1..da6e2a018 100644
--- a/apps/tc/elpi/ho_link.elpi
+++ b/apps/tc/elpi/ho_link.elpi
@@ -144,6 +144,10 @@ namespace tc {
       pred cs i:term, i:term.
       cs T1 T2 :- not (var T1), !, coq.unify-eq T1 T2 ok.
       cs (uvar _ as V) (app [_, Arg] as T) :- not (ground_term Arg), !, get-vars T Vars, declare_constraint (cs V T) [_, V | Vars].
+      cs (uvar _ as V) (app [HD, _Arg] as T) :- 
+        tc.coercion-unify HD, !, 
+        get-vars T Vars, declare_constraint (cs V T) [_, V | Vars].
+
       cs (uvar _ as V) (app [HD | _] as T) :- 
         if (HD = global (const Proj), tc.proj->record Proj Record)
           (reduce-cs V T Record Proj)
diff --git a/apps/tc/elpi/modes.elpi b/apps/tc/elpi/modes.elpi
index d3e72aaec..c72313d9d 100644
--- a/apps/tc/elpi/modes.elpi
+++ b/apps/tc/elpi/modes.elpi
@@ -97,8 +97,10 @@ namespace tc {
   action-to-accumulate _ _ [].
 
   pred mode-check i:string, i:term.
+  mode-check "+" T :- !, ground_term T.
   % heuristic: if we are in "+" mode, then all evars in T should only be 
   %            in that argument
+  % note: this rule is never applied, the previous having a cut.
   mode-check "+" T :- !, 
     std.findall-unary evars L,
     get-evars T EV,
diff --git a/apps/tc/tests/test_pending_mode.v b/apps/tc/tests/test_pending_mode.v
index 527f15ac0..50f0c2474 100644
--- a/apps/tc/tests/test_pending_mode.v
+++ b/apps/tc/tests/test_pending_mode.v
@@ -35,7 +35,7 @@ Module ground1.
 
   Goal exists (x : Type), C (list x). 
     eexists.
-    apply _.
+    Fail apply _.
   Abort.
 End ground1.
 
@@ -46,7 +46,7 @@ Module ground2.
 
   Goal exists (x : Type), C (list x). 
     eexists. 
-    apply _.
+    Fail apply _.
   Abort.
 End ground2.
 
@@ -63,14 +63,14 @@ Module ground3.
 End ground3.
 
 Module ground4.
-  Elpi TC.Pending_mode - +.
+  Elpi TC.Pending_mode ! !.
   Class C {i : Type} (f : i -> i -> Prop).
   Instance i {X : Type}: C (@eq X). Qed.
   Hint Mode C ! ! : typeclass_instances.
 
   Goal exists (X : Type), @C (list X) eq. 
     eexists.
-     apply _.
+    apply _.
   Abort.
 End ground4.
 

From 18eb74c8058b0fcbd84515800b252088a9c6395c Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Thu, 8 Aug 2024 12:28:15 +0200
Subject: [PATCH 11/33] [TC] clean term in decompilation of goal

---
 apps/tc/elpi/ho_compile.elpi | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index fc2cdd2f7..5a1e9860f 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/ho_compile.elpi
@@ -375,13 +375,13 @@ namespace tc {
 
       decompile-problematic-term (fun N Ty Bo) L (fun N Ty' Bo') L3 :-
         (pi x\ fold-map (Bo x) [] (Bo' x) (Lx x)),
-        close-term-no-prune-ty Lx Ty L1,
+        close-term-no-prune-ty Lx {tc.compile.instance.clean-term Ty} L1,
         fold-map Ty L Ty' L2,
         std.append L2 L1 L3.
 
       decompile-problematic-term (prod N Ty Bo) L (prod N Ty' Bo') L3 :-
         (pi x\ fold-map (Bo x) [] (Bo' x) (Lx x)),
-        close-term-no-prune-ty Lx Ty L1,
+        close-term-no-prune-ty Lx {tc.compile.instance.clean-term Ty} L1,
         fold-map Ty L Ty' L2,
         std.append L2 L1 L3.
 

From 1d67703accac7f99a905c38fa9e07b138b84cb3f Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Thu, 8 Aug 2024 12:35:00 +0200
Subject: [PATCH 12/33] [TC] add file deps in
 tests/importOrder/sameOrderCommand.v

---
 apps/tc/tests/importOrder/sameOrderCommand.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/apps/tc/tests/importOrder/sameOrderCommand.v b/apps/tc/tests/importOrder/sameOrderCommand.v
index 7a0b8e185..caa7cba3f 100644
--- a/apps/tc/tests/importOrder/sameOrderCommand.v
+++ b/apps/tc/tests/importOrder/sameOrderCommand.v
@@ -1,5 +1,7 @@
 From elpi.apps Require Export tc.
 
+From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.
+From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc.elpi Extra Dependency "ho_link.elpi" as ho_link.
 From elpi.apps.tc.elpi Extra Dependency "tc_same_order.elpi" as tc_same_order.
 From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
@@ -7,6 +9,9 @@ From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
 Set Warnings "+elpi".
 Elpi Command SameOrderImport.
 Elpi Accumulate Db tc.db.
+Elpi Accumulate Db tc_options.db.
+Elpi Accumulate File base.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate File unif.
 Elpi Accumulate File ho_link.
 Elpi Accumulate File tc_same_order.

From f350695c5aec4f99c1940e5b6e88cf1659257c1e Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Thu, 8 Aug 2024 14:57:28 +0200
Subject: [PATCH 13/33] [TC] perf: fold-map fully implemented in precompile
 goal

---
 apps/tc/elpi/ho_compile.elpi    | 41 +++++++++++++++++++--------------
 apps/tc/elpi/ho_precompile.elpi | 11 ++++-----
 2 files changed, 29 insertions(+), 23 deletions(-)

diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index 5a1e9860f..d04f76e49 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/ho_compile.elpi
@@ -342,8 +342,6 @@ namespace tc {
         get-uva-pair-arity Y L Z.
 
       pred decompile-problematic-term i:term, i:list prop, o:term, o:list prop.
-      decompile-problematic-term (primitive _ as C) A C A :- !.
-
       % there is no need to decompile T since no precompilation is done inside coercions
       decompile-problematic-term (tc.coercion T S) L1 Y [tc.link.cs Y T|L1] :- !,
         prune Y S.
@@ -352,18 +350,17 @@ namespace tc {
         prune Y S.
 
       decompile-problematic-term (tc.maybe-eta-tm T S) L V [tc.link.eta V T' | L2] :- !,
-        prune V S, fold-map T L T' L2.
+        prune V S, decompile-problematic-term T L T' L2.
 
       decompile-problematic-term (tc.prod-range T _) A T' A' :- !,
-        fold-map T A T' A'.
+        decompile-problematic-term T A T' A'.
 
       decompile-problematic-term (tc.maybe-llam-tm (app [app[H|S] | NPF]) Sc) L Z [NL|L'] :- !,
         prune Z Sc,
         get-uva-pair-arity H S Y,
-        std.fold-map NPF L fold-map Tl L',
+        std.fold-map NPF L decompile-problematic-term Tl L',
         NL = tc.link.llam Z (app[Y | Tl]).
 
-      % TODO: complete this fold
       decompile-problematic-term (app[X|S]) L Z L :-
         var X _ Scope, 
         std.append Scope S Scope',
@@ -371,24 +368,34 @@ namespace tc {
         get-uva-pair-arity X S Y,
         prune Z Scope', var Z Y Scope'.
       
-      decompile-problematic-term A L A L :- var A, !.
-
-      decompile-problematic-term (fun N Ty Bo) L (fun N Ty' Bo') L3 :-
-        (pi x\ fold-map (Bo x) [] (Bo' x) (Lx x)),
+      decompile-problematic-term (fun N Ty Bo) L (fun N Ty' Bo') L3 :- !,
+        (pi x\ decompile-problematic-term (Bo x) [] (Bo' x) (Lx x)),
         close-term-no-prune-ty Lx {tc.compile.instance.clean-term Ty} L1,
-        fold-map Ty L Ty' L2,
+        decompile-problematic-term Ty L Ty' L2,
         std.append L2 L1 L3.
 
-      decompile-problematic-term (prod N Ty Bo) L (prod N Ty' Bo') L3 :-
-        (pi x\ fold-map (Bo x) [] (Bo' x) (Lx x)),
+      decompile-problematic-term (prod N Ty Bo) L (prod N Ty' Bo') L3 :- !,
+        (pi x\ decompile-problematic-term (Bo x) [] (Bo' x) (Lx x)),
         close-term-no-prune-ty Lx {tc.compile.instance.clean-term Ty} L1,
-        fold-map Ty L Ty' L2,
+        decompile-problematic-term Ty L Ty' L2,
         std.append L2 L1 L3.
 
+      decompile-problematic-term (global _ as C) A C A :- !.
+      decompile-problematic-term (pglobal _ _ as C) A C A :- !.
+      decompile-problematic-term (sort _ as C) A C A :- !.
+      decompile-problematic-term (let N T B F) A (let N T1 B1 F1) A3 :- !,
+        decompile-problematic-term T A T1 A1, decompile-problematic-term B A1 B1 A2, pi x\ decompile-problematic-term (F x) A2 (F1 x) A3.
+      decompile-problematic-term (app L) A (app L1) A1 :- !, std.fold-map L A decompile-problematic-term L1 A1.
+      decompile-problematic-term (fix N Rno Ty F) A (fix N Rno Ty1 F1) A2 :- !,
+        decompile-problematic-term Ty A Ty1 A1, pi x\ decompile-problematic-term (F x) A1 (F1 x) A2.
+      decompile-problematic-term (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
+        decompile-problematic-term T A T1 A1, decompile-problematic-term Rty A1 Rty1 A2, std.fold-map B A2 decompile-problematic-term B1 A3.
+      decompile-problematic-term (primitive _ as C) A C A :- !.
+      decompile-problematic-term (uvar _ _ as V) A V A :- !.
+      decompile-problematic-term X A Y A :- name X, !, X = Y, !.
+
       pred compile i:term, i:list prop, o:term, o:list prop.
-      compile T L T' L' :-
-        (pi t l t' l'\ fold-map t l t' l' :- decompile-problematic-term t l t' l', !) =>
-          fold-map T L T' L'.
+      compile T L T' L' :- decompile-problematic-term T L T' L'.
 
       %                                  Uva      Binders      LinkEta 
       pred build-eta-links-of-vars-aux i:term, i:list term, o:list prop.
diff --git a/apps/tc/elpi/ho_precompile.elpi b/apps/tc/elpi/ho_precompile.elpi
index 1449eb34b..e41d316e7 100644
--- a/apps/tc/elpi/ho_precompile.elpi
+++ b/apps/tc/elpi/ho_precompile.elpi
@@ -236,20 +236,18 @@ namespace tc {
         close-term-prune-safe-fun Xs Ty Xs'.
 
       pred precompile-aux i:term, i:list term, o:term, o:list term.
-      precompile-aux X A Y A :- name X, !, X = Y, !. % avoid loading "precompile-aux x A x A" at binders
       precompile-aux (global _ as C) A C A :- !.
       precompile-aux (pglobal _ _ as C) A C A :- !.
       precompile-aux (sort _ as C) A C A :- !.
       precompile-aux (primitive _ as C) A C A :- !.
       
-      precompile-aux T A (tc.coercion T Scope) A :- 
-        coq.safe-dest-app T HD _, tc.coercion-unify HD, !, names Scope.
+      precompile-aux (app [HD | _] as T) A (tc.coercion T Scope) A :- 
+        tc.coercion-unify HD, !, names Scope.
       precompile-aux (app [global (const C) | _] as T) A (tc.canonical-projection T Scope N) A :- 
         coq.env.projection? C N, !, names Scope.
       precompile-aux (app [primitive (proj P _) | _] as T) A (tc.canonical-projection T Scope 0) A :- 
         coq.env.primitive-projection? P _, !, names Scope.
 
-
       % Detect maybe-eta term
       precompile-aux (fun Name Ty B as T) N (tc.maybe-eta-tm (fun Name Ty' B') Scope) M :-
         maybe-eta T, !,
@@ -257,7 +255,7 @@ namespace tc {
         std.assert! (pi x\ precompile-aux (B x) N (B' x) (MM x), close-term-prune-safe-fun MM Ty M') "[TC] should not fail1",
         precompile-aux Ty M' Ty' M.
 
-      % Detect maybe-beta term
+      % Detect maybe-llam term
       precompile-aux (app [X|XS]) N (tc.maybe-llam-tm (app [app[X | PF] | NPF1]) Scope1) [X|M] :-
         var X _ Scope, split-pf XS Scope PF NPF, 
         not (NPF = []), !, % else XS is a list of distinct names, i.e. `app [X|XS]` is in PF
@@ -281,7 +279,8 @@ namespace tc {
       precompile-aux (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
         precompile-aux T A T1 A1, precompile-aux Rty A1 Rty1 A2, std.fold-map B A2 precompile-aux B1 A3.
       precompile-aux (primitive _ as C) A C A :- !.
-      precompile-aux X A X [X|A] :- var X, !.
+      precompile-aux (uvar _ _ as X) A X [X|A] :- !.
+      precompile-aux X A Y A :- name X, !, X = Y, !. % avoid loading "precompile-aux x A x A" at binders
     }
 
     pred goal i:term, o:term, o:list term.

From ce0d03dbf78429bc6b3277701e80f0fcd77ea611 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Sat, 10 Aug 2024 12:43:24 +0200
Subject: [PATCH 14/33] [TC] improve perf of goal compilation

---
 apps/tc/elpi/base.elpi         |  17 +++-
 apps/tc/elpi/compile_goal.elpi | 178 +++++++++++++++++++++++++++++++++
 apps/tc/elpi/ho_link.elpi      |  50 ++++-----
 apps/tc/elpi/solver.elpi       |  14 ++-
 apps/tc/tests-stdlib/bigTest.v |   2 +
 apps/tc/tests/test.v           |   7 +-
 apps/tc/theories/tc.v          |   2 +
 7 files changed, 228 insertions(+), 42 deletions(-)
 create mode 100644 apps/tc/elpi/compile_goal.elpi

diff --git a/apps/tc/elpi/base.elpi b/apps/tc/elpi/base.elpi
index 76dbf04a5..b819c0cf1 100644
--- a/apps/tc/elpi/base.elpi
+++ b/apps/tc/elpi/base.elpi
@@ -90,10 +90,13 @@ split-at-not-fatal N [X|XS] [X|LN] LM :- !, N1 is N - 1,
 
 pred undup-same i:list A, o:list A.
 undup-same [] [].
-undup-same [X|Xs] [X|Ys] :-
-  std.forall Xs (x\ not (x == X)), !,
-  undup-same Xs Ys.
-undup-same [_|Xs] Ys :- undup-same Xs Ys.
+undup-same [X|Xs] Ys :- std.exists Xs (x\ x == X), !, undup-same Xs Ys.
+undup-same [X|Xs] [X|Ys] :- undup-same Xs Ys.
+
+pred undup i:list A, o:list A.
+undup [] [].
+undup [X|Xs] Ys :- std.mem! Xs X, !, undup Xs Ys.
+undup [X|Xs] [X|Ys] :- undup Xs Ys.
 
 :index (1)
 pred is-coq-term i:any.
@@ -168,3 +171,9 @@ pred close-term-no-prune-fun i:(term -> list term), i:term, o:list term.
 close-term-no-prune-fun (x\ []) _ [] :- !.
 close-term-no-prune-fun (x\ [X x | Xs x]) Ty [fun _ Ty X | Xs'] :- 
   close-term-no-prune-fun Xs Ty Xs'.
+
+pred free-names i:term, o:list term.
+free-names T L :-
+  names N,
+  (pi T L\ fold-map T L T [T|L] :- name T, std.mem! N T, !) => fold-map T [] _ L',
+  undup {std.rev L'} L.
\ No newline at end of file
diff --git a/apps/tc/elpi/compile_goal.elpi b/apps/tc/elpi/compile_goal.elpi
new file mode 100644
index 000000000..bea5e93a5
--- /dev/null
+++ b/apps/tc/elpi/compile_goal.elpi
@@ -0,0 +1,178 @@
+namespace tc {
+  shorten tc.{r-ar, range-arity}.
+
+  namespace compile {
+    namespace goall {
+      :index (_ _ 1)
+      pred may-contract-to i:list term, i:term, i:term.
+      may-contract-to _ N N :- !.
+      % TODO: here we should do var V _ Scope and use scope: N can be in Scope but not in S
+      may-contract-to L N (app [V|S]) :- var V, !,
+        std.forall [N|L] (x\ exists! S (may-contract-to [] x)).
+      may-contract-to L N (app [N|A]) :-
+        std.length A {std.length L},
+        std.forall2 {std.rev L} A (may-contract-to []).
+      may-contract-to L N (fun _ _ B) :-
+        pi x\ may-contract-to [x|L] N (B x).
+
+      :index (_ 1)
+      pred occurs-rigidly i:term, i:term.
+      occurs-rigidly N N :- name N, !.
+      occurs-rigidly _ (app [N|_]) :- var N, !, fail.
+      occurs-rigidly N (app A) :- exists! A (occurs-rigidly N).
+      occurs-rigidly N (fun _ _ B) :- pi x\ occurs-rigidly N (B x).
+
+      pred maybe-eta-aux i:term, i:list term.
+      % TODO: here we should do var V _ Scope and use Scope: an elt in L can appear in Scope
+      maybe-eta-aux (app[V|S]) L :- var V, !,
+        std.forall L (x\ exists! S (y\ may-contract-to [] x y)).
+      maybe-eta-aux (app [_|A]) L :-
+        SplitLen is {std.length A} - {std.length L},
+        split-at-not-fatal SplitLen A HD TL,
+        std.forall L (x\ not (exists! HD (occurs-rigidly x))),
+        std.forall2 {std.rev L} TL (may-contract-to []). 
+      maybe-eta-aux (fun _ _ B) L :-
+        pi x\ maybe-eta-aux (B x) [x|L].
+
+      pred maybe-eta i:term.
+      maybe-eta (fun _ _ B) :- pi x\ maybe-eta-aux (B x) [x].
+
+      pred split-pf i:list term, i:list term, o:list term, o:list term.
+      split-pf [] _ [] [] :- !.
+      split-pf [X|Xs] Old [X|Ys] L :- name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
+      split-pf Xs _ [] Xs.
+
+      pred used i:term, i:term.
+      used X (uvar _ S) :- std.mem! S X, !.
+      used X (fun _ _ Bo) :- pi x\ used X (Bo x).
+
+      pred close-term-prune-safe-fun i:(term -> list term), i:term, o:list term.
+      close-term-prune-safe-fun (x\ []) _ [] :- !.
+      close-term-prune-safe-fun (x\ [X x | Xs x]) Ty [fun _ _ X | Xs'] :-
+        pi x\ used x (X x), !, close-term-prune-safe-fun Xs Ty Xs'.
+      close-term-prune-safe-fun (x\ [X | Xs x]) Ty [X | Xs'] :-
+        close-term-prune-safe-fun Xs Ty Xs'.
+
+      pred compile-full-aux-close i:(term -> term), i:term, i:list prop, o:(term -> term), o:list prop.
+      compile-full-aux-close Bo Ty L Bo' L' :-
+        (pi x\ compile-full-aux (Bo x) [] (Bo' x) (BoL x)),
+      % TODO: maybe attach to the links the list of used binders, to simply make this check?
+      % Maybe L' is a pair list links and list binders per link, this way we can easily prune
+        close-term-no-prune-ty BoL Ty BoL',
+        std.append L BoL' L'.
+
+      pred compile-full-aux i:term, i:list prop, o:term, o:list prop.
+      compile-full-aux (global _ as G) L G L :- !.
+      compile-full-aux (pglobal _ _ as G) L G L :- !.
+      compile-full-aux (sort _ as G) L G L :- !.
+
+      % Link for coercion
+      compile-full-aux (app [HD|_] as G) L G' [tc.link.cs G' G | L] :- tc.coercion-unify HD, !.
+      
+      % Link for canonical structure
+      compile-full-aux (app [global (const C) | _] as G) L G' [tc.link.cs G' G | L] :- coq.env.projection? C _, !.
+      
+      % Link for primitive projection
+      compile-full-aux (app [primitive (proj P _) | _] as G) L G' [tc.link.cs G' G | L] :- coq.env.primitive-projection? P _, !.
+
+      % Link for eta-redex
+      compile-full-aux (fun Name Ty Bo as G) L G' [tc.link.eta G' (fun Name Ty' Bo') | L'] :- maybe-eta G, !,
+        compile-full-aux Ty L Ty' LTy,
+        compile-full-aux-close Bo Ty LTy Bo' L'.
+
+      compile-full-aux (fun Name Ty Bo) L (fun Name Ty' Bo') L' :- !,
+        compile-full-aux Ty L Ty' LTy,
+        compile-full-aux-close Bo Ty LTy Bo' L'.
+
+      compile-full-aux (prod Name Ty Bo) L (prod Name Ty' Bo') L' :- !,
+        compile-full-aux Ty L Ty' LTy,
+        compile-full-aux-close Bo Ty LTy Bo' L'.
+
+      % NOTE: when compiling t = (app [X, x, y]) and [x,y] are distinct_names,
+      %       then the coq variable has not [x,y] in scope, it is applied to
+      %       them. Note also that t is a problematic term that cannot be
+      %       exposed to the else unification algorithm.  
+      %       The solution is to build the following links:  
+      %       X =η (λa.Y a)
+      %       a |- Y a =η (λb.Z a b)
+      %       and expose a variable W at toplevel having Z has head and [x, y]
+      %       as scope
+
+      % NOTE: when compiling t = (app [X, a, x]) where a is a constant and x a
+      %       name, we build a llam link.  
+      %       The link will be: T x =L X a x  
+      %       the exposed variable in the term will be T x
+
+      % NOTE: here a combination of eta and llam:  
+      %       let t = (app [X x y, z, c, w, d]) where X is a coq var with x and
+      %       y in scope, z and w are names and c, d are constants.  
+      %       In this case, the links should be:  
+      %       X x y =η (λa.Y x y a)  
+      %       a |- Z x y a w =L (app[Y x y a, c w d])  
+      %       The returned variable is Z x y a w
+
+      pred free-names i:term, o:list term.
+      free-names T L :-
+        names N,
+        (pi T L\ fold-map T L T [T|L] :- name T, std.mem! N T, !) => fold-map T [] _ L',
+        undup {std.rev L'} L.
+
+      :index(_ _ _ _ 3)
+      % TODO: the argument Ty is unused, i.e. the binders of the eta links have no type...
+      %                           LHS      Scope      Ty          Names        PF         NPF        OLDLINKS    NEW_VAR
+      pred build-eta-llam-links i:term, i:list term, o:term, i:list term, i:list term, i:list term, i:list prop, o:term, o:list prop.
+      build-eta-llam-links LHS _ _       Names []  NPF OL HD [tc.link.llam T (app [LHS | NPF]) | OL] :- !,
+        std.assert! (not (NPF = [])) "[TC] NPF List should not be empty",
+        prune T Names,
+        var T HD _. 
+      build-eta-llam-links LHS SC _Ty       _    [X] []  OL HD [tc.link.eta LHS (fun _ _ (x\ V x)) | OL] :- !,
+        prune V SC, var (V X) HD _. % TODO...
+      build-eta-llam-links LHS SC _Ty Names [X|XS] NPF OL HD [tc.link.eta LHS (fun _ _ (x\ LHS' x)) | L] :- !,
+      % TODO: unfold Ty if needed...
+        std.append SC [X] SC',
+        prune LHS' SC, build-eta-llam-links (LHS' X) SC' _ Names XS NPF OL HD L.
+
+      % Link for beta-redex (Uvar in PF)
+      % BUILD CHAIN OF LINKS-ETA from X to V...
+      % TODO: to avoid too many chain for the same var, maybe pass a list into the fold
+      compile-full-aux (app [(uvar _ Scope as V) | S] as T) L G' L'' :- !,
+        % By construction the scope of a uvar is a list of distinct name
+        std.fold-map S L compile-full-aux S' L', % LS = Links built for S
+        % std.assert-ok! (coq.typecheck V Ty) "Not typecheckable variable",
+        split-pf S' Scope PF NPF,
+        free-names T Names,
+        build-eta-llam-links V Scope _ Names PF NPF L' G'' L'',
+        prune G' Names,
+        var G' G'' Names.
+
+      compile-full-aux (app L) A (app L1) A1 :- !, std.fold-map L A compile-full-aux L1 A1.
+
+      compile-full-aux (let N T B F) A (let N T1 B1 F1) A3 :- !,
+        compile-full-aux T A T1 A1, compile-full-aux B A1 B1 A2,
+        compile-full-aux-close F T A2 F1 A3.
+      
+      compile-full-aux (fix N Rno Ty F) A (fix N Rno Ty1 F1) A2 :- !,
+        compile-full-aux Ty A Ty1 A1, 
+        compile-full-aux-close F Ty A1 F1 A2.
+      
+      compile-full-aux (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
+        compile-full-aux T A T1 A1,
+        compile-full-aux Rty A1 Rty1 A2,
+        std.fold-map B A2 compile-full-aux B1 A3.
+      
+      compile-full-aux (uvar _ _ as X) A X A :- !.
+      compile-full-aux X A X A :- name X, !.
+
+      compile-full-aux A B _ _ :- coq.error "Fail to compile-full-aux" A B.
+
+      % takes a term t and returns a term t' and a list of links.
+      pred compile-full i:term, o:term, o:list prop.
+      compile-full Goal Goal' Links :- compile-full-aux Goal [] Goal' Links.
+    }
+
+    pred goal' i:term, o:term, o:list prop.
+    :name "compile-goal'"
+    goal' Goal Goal' Links :- 
+      goall.compile-full-aux Goal [] Goal' Links.
+  }
+}
diff --git a/apps/tc/elpi/ho_link.elpi b/apps/tc/elpi/ho_link.elpi
index da6e2a018..5d8e3269f 100644
--- a/apps/tc/elpi/ho_link.elpi
+++ b/apps/tc/elpi/ho_link.elpi
@@ -1,5 +1,9 @@
 namespace tc {
   namespace link {
+    pred relocate i:list term, i:list term, i:term, o:term.
+    relocate [] [] T T' :- copy T T'.
+    relocate [X|Xs] [Y|Ys] T T' :- (copy Y X :- !) => relocate Xs Ys T T'.
+
     pred get-vars i:term, o:list term.
     get-vars T R :-
       (pi X H L Ign\ fold-map X L X [H|L] :- var X H Ign, !) => 
@@ -61,12 +65,6 @@ namespace tc {
       pred scope-check i:term, i:term.
       scope-check (uvar _ L) T :- prune A L, A = T, !.
 
-      pred relocate i:list term, i:list term, i:term, o:term.
-      relocate [] [] T T' :- copy T T', coq.say "Copy result is" T T'.
-      relocate [X|Xs] [Y|Ys] T T' :-
-        coq.say "Charging" (copy Y X),
-        (copy Y X :- !) => relocate Xs Ys T T'.
-
       pred collect-store o:list prop.
       pred collect-store-aux i:list prop, o:list prop.
 
@@ -80,24 +78,14 @@ namespace tc {
       unify-eta A (fun _ _ _ as B) :- !, eta-expand A A', unify-eta A' B.
       unify-eta A B :- A = B.
 
-      constraint eta uvar relocate fun collect-store-aux solve-eta {
+      constraint eta solve-eta {
         rule solve-eta \ (eta A B) <=> (unify-eta A B).
         rule \ solve-eta.
-        % rule (N1 : G1 ?- eta (uvar X L1) (fun _ T1 B1)) 
-        %     \ (N2 : G2 ?- eta (uvar X L2) (fun _ T2 B2)) 
-        %     | (
-        %       pi x\ relocate L1 L2 (B2 x) (B2' x)
-        %       % coq.say "Deduplicating" 
-        %       %   (eta (uvar X L1) (fun _ T1 B1)) 
-        %       %   (eta (uvar X L2) (fun _ T2 B2))
-        %       %   "B2' is" (B2')
-        %     )  
-        % <=> (N1 : G1 ?- B1 = B2').
-
-        % TODO: link collect do not work since it closes links and 
-        %       therefore variables are prune
-        % rule \ (tc.link.eta A B) (collect-store-aux L R) | (coq.say A B {names}) <=> (collect-store-aux [tc.link.eta A B|L] R).
-        % rule \ (collect-store-aux L R) <=> (R = L).
+        % If two eta links have same lhs they rhs should unify
+        rule (N1 : G1 ?- eta (uvar X L1) (fun _ T1 B1)) 
+            \ (N2 : G2 ?- eta (uvar X L2) (fun _ T2 B2)) 
+            | (pi x\ relocate L1 L2 (B2 x) (B2' x))  
+        <=> (N1 : G1 ?- B1 = B2').
       }
 
       pred eta i:term, i:term.
@@ -114,7 +102,9 @@ namespace tc {
     namespace llam {
       pred llam i:term, i:term.
       llam A (uvar _ S as T) :- distinct_names S, !, A = T.
-      llam A (app [H|L] as T) :- var A, var H, !, get-vars T Vars, declare_constraint (llam A (app [H|L])) [_,A|Vars].
+      llam A (app [H|L] as T) :- var A, var H, !, get-vars T Vars, 
+        coq.say "Declaring constraint" (llam A (app [H|L])) [_,A|Vars],
+        declare_constraint (llam A (app [H|L])) [_,A|Vars].
       llam (fun _ _ _ as F) (app [H | TL]) :- 
         var H _ Scope, !, 
           std.drop-last 1 TL TL', 
@@ -124,9 +114,14 @@ namespace tc {
           pi x\ llam F Bo'.
       llam A B :- !, tc.unify-eq A B.
 
-      constraint solve-llam solve-llam-t llam {
+      constraint solve-llam llam {
         rule solve-llam \ (llam A B) <=> (A = B).
         rule \ solve-llam.
+        % If two llam links have same lhs they rhs should unify
+        rule (N1 : G1 ?- llam (uvar X L1) T1) 
+            \ (N2 : G2 ?- llam (uvar X L2) T2) 
+            | (pi x\ relocate L1 L2 T2 T2')  
+        <=> (N1 : G1 ?- T1 = T2'). % TODO: instead of elpi unif, should use heuristics...
       }
     }
 
@@ -154,13 +149,6 @@ namespace tc {
           (coq.unify-eq V T ok).
       cs T1 T2 :- not (T2 = app _), !, coq.unify-eq T1 T2 ok.
 
-      % pred unify-rebinding-names i:list prop, i:list prop, i:term, i:term.
-      % unify-rebinding-names [] T1 [] T2 (unify-eq T1V T2) :- !, copy T1 T1V.
-      % unify-rebinding-names [N|NS] T1 [V|VS] T2 C :- !, copy N V => unify-rebinding-names NS T1 VS T2 C.
-      % unify-rebinding-names [] T1 VS T2 C :- !, unify-rebinding-names [] {coq.subst-prod VS T1} [] T2 C. % FIXME: reduction
-      % unify-rebinding-names [_|NS] (prod _ _ F) [] T2 C :- !,                      % FIXME: reduction
-      %   assert! (pi x\ F x = F1) "restriction bug", unify-rebinding-names NS F1 [] T2 C.
-
       pred unify-under-ctx i:list term, i:list term, i:term, i:term, i:term, i:term.
       unify-under-ctx [] [] A B V1 V2 :- copy A A', copy V1 V1', !, coq.unify-eq A' B ok, !, V1' = V2.
       unify-under-ctx [X|XS] [Y|YS] A B V1 V2:- (copy X Y :- !) => unify-under-ctx XS YS A B V1 V2.
diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi
index 6e4a8b932..160e91ab9 100644
--- a/apps/tc/elpi/solver.elpi
+++ b/apps/tc/elpi/solver.elpi
@@ -7,8 +7,8 @@ msolve L _ :- coq.ltac.fail _ "[TC] fail to solve" L.
 
 namespace tc {
   pred build-query-from-goal i:term, i:term, o:prop, o:list prop.
-  build-query-from-goal Goal Proof Q PostProcess :-
-    tc.compile.goal Goal Goal' PostProcess, !,
+  build-query-from-goal Goal Proof Q Links :-
+    tc.compile.goal' Goal Goal' Links, !,
     coq.safe-dest-app Goal' (global TC) TL',
     std.append TL' [Proof] TL, !,
     coq.elpi.predicate {tc.gref->pred-name TC} TL Q.
@@ -29,10 +29,11 @@ namespace tc {
 
   pred solve-under-context i:term, o:term.
   solve-under-context Ty Proof :-
-    tc.time-it tc.oTC-time-compile-goal (build-query-from-goal Ty Proof Q PostProcess) "build query", !,
-    if-true print-compiled-goal (coq.say "[TC] the compiled goal is" Q), !,
+    tc.time-it tc.oTC-time-compile-goal (build-query-from-goal Ty Proof Q Links) "build query", !,
+    if-true print-compiled-goal (coq.say "[TC] the compiled goal is" Q),
+    if-true print-links (coq.say "[TC] the links are" Links),
     tc.time-it tc.oTC-time-instance-search (
-      do PostProcess, Q,
+      do Links, Q,
       tc.link.solve-cs,
       tc.link.solve-eta, % Trigger eta links
       tc.link.solve-llam % Trigger llam links
@@ -59,6 +60,7 @@ namespace tc {
     if-true print-goal-pp (coq.say "The goal is <<<" {coq.term->string Ty} ">>>"),
     tc.time-it tc.oTC-time-mode-check (tc.modes-check Ty) "mode check", !,
     tc.time-it _ (tc.compile.context Ctx CtxClause) "compile context", !,
+    if-true print-ctx (coq.say "The context is" CtxClause),
     CtxClause => solve-under-context Ty Proof.
   solve-aux1 _ _ tc.mode_fail :- if-true (print-solution; print-solution-pp) (coq.say "Invalid mode call").
 
@@ -68,5 +70,7 @@ namespace tc {
   pred print-goal-pp.       % Print the goal with coq pp
   pred print-goal-after-search.          % Print the goal in HOAS after instance search
   pred print-compiled-goal.
+  pred print-links.
+  pred print-ctx.
 
 }
\ No newline at end of file
diff --git a/apps/tc/tests-stdlib/bigTest.v b/apps/tc/tests-stdlib/bigTest.v
index 89de2c8b3..42825e83f 100644
--- a/apps/tc/tests-stdlib/bigTest.v
+++ b/apps/tc/tests-stdlib/bigTest.v
@@ -1,3 +1,5 @@
+Set Warnings "-elpi.TC.hints".
+
 From elpi.apps Require Import tc.
 Elpi TC Solver Override TC.Solver All.
 
diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v
index fae3a5266..b2d1b46be 100644
--- a/apps/tc/tests/test.v
+++ b/apps/tc/tests/test.v
@@ -1,4 +1,5 @@
 From elpi Require Import tc.
+Set Warnings "+elpi".
 
 Section test_max_arity.
   Elpi Query TC.Solver lp:{{
@@ -222,8 +223,10 @@ Module HO_81.
     (* Failure is good, since here we simply check that the number of 
       uvar-pair built by tc.precomp is zero. This is because the type
       of ?X is Type (i.e. it has `arity` zero) *)
-    Fail apply _.
-  Abort.
+    apply _.
+    Unshelve.
+    apply nat.
+  Qed.
 End HO_81.
 
 Module HO_8.
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index a9cd831b8..bbc102b45 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -7,6 +7,7 @@ From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
 (* From elpi.apps.tc.elpi Extra Dependency "compiler.elpi" as compiler. *)
 From elpi.apps.tc.elpi Extra Dependency "ho_precompile.elpi" as ho_precompile.
 From elpi.apps.tc.elpi Extra Dependency "ho_compile.elpi" as ho_compile.
+From elpi.apps.tc.elpi Extra Dependency "compile_goal.elpi" as compile_goal.
 From elpi.apps.tc.elpi Extra Dependency "compiler1.elpi" as compiler1.
 From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes.
 From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
@@ -55,6 +56,7 @@ Elpi Accumulate File ho_precompile.
 Elpi Accumulate File ho_compile.
 Elpi Accumulate File compiler1.
 Elpi Accumulate File create_tc_predicate.
+Elpi Accumulate File compile_goal.
 Elpi Accumulate File modes.
 Elpi Accumulate File solver.
 Elpi Query lp:{{

From 03f100f4fed00e53765781bb4fe6a8cb48cfb001 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 8 Apr 2025 21:45:39 +0200
Subject: [PATCH 15/33] [TC] remove goal precomp and goal compile (all is done
 in ycompile_goal.elpi)

---
 apps/tc/elpi/compile_goal.elpi  |  29 +-----
 apps/tc/elpi/ho_compile.elpi    | 172 ++++----------------------------
 apps/tc/elpi/ho_link.elpi       |  26 ++++-
 apps/tc/elpi/ho_precompile.elpi | 102 -------------------
 apps/tc/elpi/solver.elpi        |   2 +-
 apps/tc/tests/test.v            |  12 +--
 6 files changed, 49 insertions(+), 294 deletions(-)

diff --git a/apps/tc/elpi/compile_goal.elpi b/apps/tc/elpi/compile_goal.elpi
index bea5e93a5..33ec8eef8 100644
--- a/apps/tc/elpi/compile_goal.elpi
+++ b/apps/tc/elpi/compile_goal.elpi
@@ -1,6 +1,4 @@
 namespace tc {
-  shorten tc.{r-ar, range-arity}.
-
   namespace compile {
     namespace goall {
       :index (_ _ 1)
@@ -76,7 +74,7 @@ namespace tc {
       compile-full-aux (app [primitive (proj P _) | _] as G) L G' [tc.link.cs G' G | L] :- coq.env.primitive-projection? P _, !.
 
       % Link for eta-redex
-      compile-full-aux (fun Name Ty Bo as G) L G' [tc.link.eta G' (fun Name Ty' Bo') | L'] :- maybe-eta G, !,
+      compile-full-aux (fun Name_ Ty Bo as G) L G' [tc.link.eta G' (fun `_` Ty' Bo') | L'] :- maybe-eta G, !,
         compile-full-aux Ty L Ty' LTy,
         compile-full-aux-close Bo Ty LTy Bo' L'.
 
@@ -111,37 +109,16 @@ namespace tc {
       %       a |- Z x y a w =L (app[Y x y a, c w d])  
       %       The returned variable is Z x y a w
 
-      pred free-names i:term, o:list term.
-      free-names T L :-
-        names N,
-        (pi T L\ fold-map T L T [T|L] :- name T, std.mem! N T, !) => fold-map T [] _ L',
-        undup {std.rev L'} L.
-
-      :index(_ _ _ _ 3)
-      % TODO: the argument Ty is unused, i.e. the binders of the eta links have no type...
-      %                           LHS      Scope      Ty          Names        PF         NPF        OLDLINKS    NEW_VAR
-      pred build-eta-llam-links i:term, i:list term, o:term, i:list term, i:list term, i:list term, i:list prop, o:term, o:list prop.
-      build-eta-llam-links LHS _ _       Names []  NPF OL HD [tc.link.llam T (app [LHS | NPF]) | OL] :- !,
-        std.assert! (not (NPF = [])) "[TC] NPF List should not be empty",
-        prune T Names,
-        var T HD _. 
-      build-eta-llam-links LHS SC _Ty       _    [X] []  OL HD [tc.link.eta LHS (fun _ _ (x\ V x)) | OL] :- !,
-        prune V SC, var (V X) HD _. % TODO...
-      build-eta-llam-links LHS SC _Ty Names [X|XS] NPF OL HD [tc.link.eta LHS (fun _ _ (x\ LHS' x)) | L] :- !,
-      % TODO: unfold Ty if needed...
-        std.append SC [X] SC',
-        prune LHS' SC, build-eta-llam-links (LHS' X) SC' _ Names XS NPF OL HD L.
-
       % Link for beta-redex (Uvar in PF)
       % BUILD CHAIN OF LINKS-ETA from X to V...
       % TODO: to avoid too many chain for the same var, maybe pass a list into the fold
       compile-full-aux (app [(uvar _ Scope as V) | S] as T) L G' L'' :- !,
         % By construction the scope of a uvar is a list of distinct name
         std.fold-map S L compile-full-aux S' L', % LS = Links built for S
-        % std.assert-ok! (coq.typecheck V Ty) "Not typecheckable variable",
+        coq.typecheck V Ty ok,
         split-pf S' Scope PF NPF,
         free-names T Names,
-        build-eta-llam-links V Scope _ Names PF NPF L' G'' L'',
+        tc.link.build-eta-llam-links V Scope Ty Names PF NPF L' G'' L'',
         prune G' Names,
         var G' G'' Names.
 
diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index d04f76e49..f0f473a0d 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/ho_compile.elpi
@@ -59,18 +59,23 @@ namespace tc {
         % This happens when the instance to be compiled comes from the context
         % Example: Goal exists (X : T1 -> T2), forall a, c (X a) -> ...
         %            intros; eexists. (* In the context we have the instance `H: c (?X a)` *)
-        decompile-term-aux (tc.maybe-llam-tm (app[app[H | PF] | NPF]) S) A Z (pr XS' [NL | L3]) :-  !,
-          var H _ Scope, !,
-          std.append Scope S S',
-          prune Z S',
-          tc.compile.goal.make-pairs [T] Pairs,
-          % We build on the fly the eta-links for T
-          (Pairs =>
-            (tc.compile.goal.build-eta-links-of-vars [T] P,
-              tc.compile.goal.get-uva-pair-arity T PF Y)),
-          std.fold-map NPF A decompile-term-aux Tl (pr XS' L2), 
-          std.append P L2 L3,
-          NL = tc.link.llam Z (app [Y|Tl]).
+        decompile-term-aux (tc.maybe-llam-tm (app[app[V | PF] | NPF] as T) S_) L G'' (pr XS' L'') :-  !,
+          var V _ Scope, !,
+          std.fold-map NPF L decompile-term-aux NPF' (pr XS' L'),
+          free-names T Names,
+          coq.typecheck V Ty ok,
+          tc.link.build-eta-llam-links V Scope Ty Names PF NPF' L' G' L'',
+          prune G'' Names,
+          var G'' G' Names.
+
+        % HO var when H is a hole appearing in the shelved goals
+        decompile-term-aux (app [V|PF] as T) (pr XS' L') G'' (pr XS' L'') :-
+          var V _ Scope, !,
+          free-names T Names,
+          coq.typecheck V Ty ok,
+          tc.link.build-eta-llam-links V Scope Ty Names PF [] L' G' L'',
+          prune G'' Names,
+          var G'' G' Names.
 
         decompile-term-aux (fun Name Ty Bo) (pr XS L) (fun Name Ty' Bo') (pr XS2 L3) :- !,
           (pi x\ is-name x => decompile-term-aux (Bo x) (pr XS []) (Bo' x) (pr XS1 (L1x x))),
@@ -96,21 +101,6 @@ namespace tc {
           std.assert! (name-pair H V Len) "[TC] name-pair not found",
           name R V L.
 
-        % HO var when H is a hole appearing in the shelved goals
-        decompile-term-aux (app [T|L]) (pr A B) Z (pr A B') :-
-          var T _ Scope,
-          std.forall L is-name,     % Not needed, since decompile for llam leaves only PF
-          distinct_names L, !,      % Not needed, since decompile for llam leaves only PF
-          std.append Scope L Scope',
-          prune Z Scope',
-          tc.compile.goal.make-pairs [T] Pairs,
-          % We build on the fly the eta-links for `T`
-          (Pairs =>
-            (tc.compile.goal.build-eta-links-of-vars [T] P,
-              tc.compile.goal.get-uva-pair-arity T L Y)),
-          var Z Y Scope',
-          std.append P B B'.
-
         decompile-term-aux (app L) PR (app L') PR' :- !,
           std.fold-map L PR decompile-term-aux L' PR'.
 
@@ -174,10 +164,10 @@ namespace tc {
         o:prop,            % Link         : The new eta-link
         o:term,            % Ty'          : The cleaned version of the binder in Ty
         o:(term -> term).  % Bo           : the body of the type of A
-      make-eta-link-aux A (prod _ Ty Bo) (pr B Name) L Link Ty' Bo :- !,
+      make-eta-link-aux A (prod _ Ty Bo) (pr B Name_) L Link Ty' Bo :- !,
         clean-term Ty Ty',
         name A' A {std.rev L},
-        Link = tc.link.eta A' (fun Name Ty' B'),
+        Link = tc.link.eta A' (fun `_` Ty' B'),
         pi x\ sigma L'\ std.rev [x|L] L', name (B' x) B L'.
       % Going under prod-range
       make-eta-link-aux A (tc.prod-range Prod _) BN L Link Ty' Bo :- !,
@@ -313,129 +303,5 @@ namespace tc {
     instance-gr InstGR Clause :-
       coq.env.typeof InstGR Ty,
       tc.compile.instance Ty (global InstGR) Clause.
-    
-    namespace goal {
-      % [uvar-pair V1 Ty V2] List of uvar for link-eta-dedup
-      %                      V1 has arity n and V2 has arity n+1
-      %                      If V1 has type A -> B, then A = Ty
-      pred uvar-pair i:term, o:term, o:term.
-
-      %                    Type     Var    Cnt    uvar-pair-list
-      pred make-pairs-aux i:term, i:term, o:list prop.
-      make-pairs-aux Ty (fun _ _ IBo) L' :- !,
-        pi x\ make-pairs-aux Ty (IBo x) (L x), close-prop-no-prune L L'.
-      make-pairs-aux (prod _ Ty Bo) V [pi x\ uvar-pair x Ty X' :- x == V, ! | L] :- !,
-        pi x\ make-pairs-aux (Bo x) X' L.
-      make-pairs-aux _ _ [].
-
-      pred make-pairs i:list term, o:list prop.
-      make-pairs [] [] :- !.
-      make-pairs [X|Xs] L :- !,
-        coq.typecheck X Ty ok,
-        make-pairs-aux Ty X L',
-        make-pairs Xs L'',
-        std.append L' L'' L.
-
-      pred get-uva-pair-arity i:term, i:list term, o:term.
-      get-uva-pair-arity X [] X :- !.
-      get-uva-pair-arity X [_|L] Z :- uvar-pair X _ Y, !, 
-        get-uva-pair-arity Y L Z.
-
-      pred decompile-problematic-term i:term, i:list prop, o:term, o:list prop.
-      % there is no need to decompile T since no precompilation is done inside coercions
-      decompile-problematic-term (tc.coercion T S) L1 Y [tc.link.cs Y T|L1] :- !,
-        prune Y S.
-      % there is no need to decompile T since no precompilation is done inside CS
-      decompile-problematic-term (tc.canonical-projection T S _) L1 Y [tc.link.cs Y T|L1] :- !,
-        prune Y S.
-
-      decompile-problematic-term (tc.maybe-eta-tm T S) L V [tc.link.eta V T' | L2] :- !,
-        prune V S, decompile-problematic-term T L T' L2.
-
-      decompile-problematic-term (tc.prod-range T _) A T' A' :- !,
-        decompile-problematic-term T A T' A'.
-
-      decompile-problematic-term (tc.maybe-llam-tm (app [app[H|S] | NPF]) Sc) L Z [NL|L'] :- !,
-        prune Z Sc,
-        get-uva-pair-arity H S Y,
-        std.fold-map NPF L decompile-problematic-term Tl L',
-        NL = tc.link.llam Z (app[Y | Tl]).
-
-      decompile-problematic-term (app[X|S]) L Z L :-
-        var X _ Scope, 
-        std.append Scope S Scope',
-        distinct_names Scope', !,
-        get-uva-pair-arity X S Y,
-        prune Z Scope', var Z Y Scope'.
-      
-      decompile-problematic-term (fun N Ty Bo) L (fun N Ty' Bo') L3 :- !,
-        (pi x\ decompile-problematic-term (Bo x) [] (Bo' x) (Lx x)),
-        close-term-no-prune-ty Lx {tc.compile.instance.clean-term Ty} L1,
-        decompile-problematic-term Ty L Ty' L2,
-        std.append L2 L1 L3.
-
-      decompile-problematic-term (prod N Ty Bo) L (prod N Ty' Bo') L3 :- !,
-        (pi x\ decompile-problematic-term (Bo x) [] (Bo' x) (Lx x)),
-        close-term-no-prune-ty Lx {tc.compile.instance.clean-term Ty} L1,
-        decompile-problematic-term Ty L Ty' L2,
-        std.append L2 L1 L3.
-
-      decompile-problematic-term (global _ as C) A C A :- !.
-      decompile-problematic-term (pglobal _ _ as C) A C A :- !.
-      decompile-problematic-term (sort _ as C) A C A :- !.
-      decompile-problematic-term (let N T B F) A (let N T1 B1 F1) A3 :- !,
-        decompile-problematic-term T A T1 A1, decompile-problematic-term B A1 B1 A2, pi x\ decompile-problematic-term (F x) A2 (F1 x) A3.
-      decompile-problematic-term (app L) A (app L1) A1 :- !, std.fold-map L A decompile-problematic-term L1 A1.
-      decompile-problematic-term (fix N Rno Ty F) A (fix N Rno Ty1 F1) A2 :- !,
-        decompile-problematic-term Ty A Ty1 A1, pi x\ decompile-problematic-term (F x) A1 (F1 x) A2.
-      decompile-problematic-term (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
-        decompile-problematic-term T A T1 A1, decompile-problematic-term Rty A1 Rty1 A2, std.fold-map B A2 decompile-problematic-term B1 A3.
-      decompile-problematic-term (primitive _ as C) A C A :- !.
-      decompile-problematic-term (uvar _ _ as V) A V A :- !.
-      decompile-problematic-term X A Y A :- name X, !, X = Y, !.
-
-      pred compile i:term, i:list prop, o:term, o:list prop.
-      compile T L T' L' :- decompile-problematic-term T L T' L'.
-
-      %                                  Uva      Binders      LinkEta 
-      pred build-eta-links-of-vars-aux i:term, i:list term, o:list prop.
-      build-eta-links-of-vars-aux Old L [Hd | Xs] :- 
-        uvar-pair Old Ty Next, !,
-        prune OldScope L,
-        prune Name L,
-        var OldScope Old L,
-        Hd = tc.link.eta OldScope (fun Name Ty (x\ NextScope x)),
-        pi x\ sigma L'\
-          std.append L [x] L',
-          prune (NextScope x) L',
-          var (NextScope x) Next L',
-          build-eta-links-of-vars-aux Next L' (Ys x), !,
-        sigma Closed\ (close-term-no-prune-ty Ys Ty Closed),
-        Xs = Closed.
-      build-eta-links-of-vars-aux _ _ [].
-
-      pred build-eta-links-of-vars i:list term, o:list prop.
-      build-eta-links-of-vars [] [].
-      build-eta-links-of-vars [V|Vars] L :-
-        var V Hd S,
-        build-eta-links-of-vars-aux Hd S L',
-        build-eta-links-of-vars Vars L'',
-        std.append L' L'' L.
-      build-eta-links-of-vars [fun _ Ty Bo|Vars] L :-
-        (pi x\ build-eta-links-of-vars [Bo x] (L' x), close-term-no-prune-ty L' Ty L''),
-        build-eta-links-of-vars Vars L''',
-        std.append L'' L''' L.
-    }
-    
-    %          Goal    Goal'      Links
-    pred goal i:term, o:term, o:list prop.
-    :name "compile-goal"
-    goal Goal Goal' Links :-
-      tc.precomp.goal Goal GoalPrecomp Vars, !,
-      goal.make-pairs Vars Pairs,
-      Pairs => (
-        std.assert!(goal.build-eta-links-of-vars Vars EtaLinks) "[TC] cannot build eta-links",
-        std.assert!(goal.compile GoalPrecomp EtaLinks Goal' Links) "[TC] cannot compile goal"
-      ).
   }
 }
\ No newline at end of file
diff --git a/apps/tc/elpi/ho_link.elpi b/apps/tc/elpi/ho_link.elpi
index 5d8e3269f..84158c6ac 100644
--- a/apps/tc/elpi/ho_link.elpi
+++ b/apps/tc/elpi/ho_link.elpi
@@ -9,6 +9,29 @@ namespace tc {
       (pi X H L Ign\ fold-map X L X [H|L] :- var X H Ign, !) => 
         fold-map T [] _ R.
 
+    % [build-eta-llam-links LHS Scope Ty Names PF NPF OldLinks NewVar NewLinks]
+    % Builds the eta/llam links at runtime for a term having the shape 
+    % `app[(uvar X Scope as V) | L]`.
+    % LHS should be V, Scope the scope of V, TODO: finish to document this...
+    :index(_ _ _ _ 3)
+    % TODO: the argument Ty is unused, i.e. the binders of the eta links have no type...
+    %                           LHS      Scope      Ty          Names        PF         NPF        OldLinks    NewVar
+    pred build-eta-llam-links i:term, i:list term, o:term, i:list term, i:list term, i:list term, i:list prop, o:term, o:list prop.
+    build-eta-llam-links LHS _ _       Names []  NPF OL HD [tc.link.llam T (app [LHS | NPF]) | OL] :- !,
+      std.assert! (not (NPF = [])) "[TC] NPF List should not be empty",
+      prune T Names,
+      var T HD _. 
+    build-eta-llam-links LHS SC (prod _ Ty _)       _    [X] []  OL HD [tc.link.eta LHS (fun `_` Ty (x\ V x)) | OL] :- !,
+      prune V SC, var (V X) HD _.
+    build-eta-llam-links LHS SC (prod _ Ty Bo) Names [X|XS] NPF OL HD [tc.link.eta LHS (fun `_` Ty (x\ LHS' x)) | L] :- !,
+    % TODO: unfold Ty if needed...
+      std.append SC [X] SC',
+      prune LHS' SC, build-eta-llam-links (LHS' X) SC' (Bo X) Names XS NPF OL HD L.
+    build-eta-llam-links LHS SC Ty Names ([_|_] as PF) NPF OL HD L :-
+      Ty' = prod _ _ _, coq.unify-eq Ty Ty' ok, !,
+      build-eta-llam-links LHS SC Ty' Names PF NPF OL HD L.
+
+
     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     % ETA LINK                                                                 %
     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -73,7 +96,7 @@ namespace tc {
 
       pred unify-eta i:term, i:term.
       % unify-eta A B :- coq.say "Unify-eta" "A"A"B"B, fail.
-      unify-eta A B :- var A, !, A = B, !.
+      unify-eta (uvar _ _ as A) B :- !, A = B, !.
       unify-eta (fun _ _ A) (fun _ _ B) :- !, pi x\ unify-eta (A x) (B x).
       unify-eta A (fun _ _ _ as B) :- !, eta-expand A A', unify-eta A' B.
       unify-eta A B :- A = B.
@@ -103,7 +126,6 @@ namespace tc {
       pred llam i:term, i:term.
       llam A (uvar _ S as T) :- distinct_names S, !, A = T.
       llam A (app [H|L] as T) :- var A, var H, !, get-vars T Vars, 
-        coq.say "Declaring constraint" (llam A (app [H|L])) [_,A|Vars],
         declare_constraint (llam A (app [H|L])) [_,A|Vars].
       llam (fun _ _ _ as F) (app [H | TL]) :- 
         var H _ Scope, !, 
diff --git a/apps/tc/elpi/ho_precompile.elpi b/apps/tc/elpi/ho_precompile.elpi
index e41d316e7..353a5deca 100644
--- a/apps/tc/elpi/ho_precompile.elpi
+++ b/apps/tc/elpi/ho_precompile.elpi
@@ -183,107 +183,5 @@ namespace tc {
       tc.precomp.instance.get-univ T UnivConstL,
       tc.precomp.instance.get-univ-instances T UnivInstL,
       std.assert!(instance.precompile-aux instance.is_pos T z T' N) "[TC] cannot precompile instance".
-
-    namespace goal {
-      :index (_ _ 1)
-      pred may-contract-to i:list term, i:term, i:term.
-      may-contract-to _ N N :- !.
-      % TODO: here we should do var V _ Scope and use scope: N can be in Scope but not in S
-      may-contract-to L N (app [V|S]) :- var V, !,
-        std.forall [N|L] (x\ exists! S (may-contract-to [] x)).
-      may-contract-to L N (app [N|A]) :-
-        std.length A {std.length L},
-        std.forall2 {std.rev L} A (may-contract-to []).
-      may-contract-to L N (fun _ _ B) :-
-        pi x\ may-contract-to [x|L] N (B x).
-
-      :index (_ 1)
-      pred occurs-rigidly i:term, i:term.
-      occurs-rigidly N N :- name N, !.
-      occurs-rigidly _ (app [N|_]) :- var N, !, fail.
-      occurs-rigidly N (app A) :- exists! A (occurs-rigidly N).
-      occurs-rigidly N (fun _ _ B) :- pi x\ occurs-rigidly N (B x).
-
-      pred maybe-eta-aux i:term, i:list term.
-      % TODO: here we should do var V _ Scope and use Scope: an elt in L can appear in Scope
-      maybe-eta-aux (app[V|S]) L :- var V, !,
-        std.forall L (x\ exists! S (y\ may-contract-to [] x y)).
-      maybe-eta-aux (app [_|A]) L :-
-        SplitLen is {std.length A} - {std.length L},
-        split-at-not-fatal SplitLen A HD TL,
-        std.forall L (x\ not (exists! HD (occurs-rigidly x))),
-        std.forall2 {std.rev L} TL (may-contract-to []). 
-      maybe-eta-aux (fun _ _ B) L :-
-        pi x\ maybe-eta-aux (B x) [x|L].
-
-      pred maybe-eta i:term.
-      maybe-eta (fun _ _ B) :- pi x\ maybe-eta-aux (B x) [x].
-
-      pred split-pf i:list term, i:list term, o:list term, o:list term.
-      split-pf [] _ [] [] :- !.
-      split-pf [X|Xs] Old [X|Ys] L :- name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
-      split-pf Xs _ [] Xs.
-
-      pred used i:term, i:term.
-      used X (uvar _ S) :- std.mem! S X, !.
-      used X (fun _ _ Bo) :- pi x\ used X (Bo x).
-
-      pred close-term-prune-safe-fun i:(term -> list term), i:term, o:list term.
-      close-term-prune-safe-fun (x\ []) _ [] :- !.
-      close-term-prune-safe-fun (x\ [X x | Xs x]) Ty [fun _ _ X | Xs'] :- 
-        pi x\ used x (X x), !, close-term-prune-safe-fun Xs Ty Xs'.
-      close-term-prune-safe-fun (x\ [X | Xs x]) Ty [X | Xs'] :-
-        close-term-prune-safe-fun Xs Ty Xs'.
-
-      pred precompile-aux i:term, i:list term, o:term, o:list term.
-      precompile-aux (global _ as C) A C A :- !.
-      precompile-aux (pglobal _ _ as C) A C A :- !.
-      precompile-aux (sort _ as C) A C A :- !.
-      precompile-aux (primitive _ as C) A C A :- !.
-      
-      precompile-aux (app [HD | _] as T) A (tc.coercion T Scope) A :- 
-        tc.coercion-unify HD, !, names Scope.
-      precompile-aux (app [global (const C) | _] as T) A (tc.canonical-projection T Scope N) A :- 
-        coq.env.projection? C N, !, names Scope.
-      precompile-aux (app [primitive (proj P _) | _] as T) A (tc.canonical-projection T Scope 0) A :- 
-        coq.env.primitive-projection? P _, !, names Scope.
-
-      % Detect maybe-eta term
-      precompile-aux (fun Name Ty B as T) N (tc.maybe-eta-tm (fun Name Ty' B') Scope) M :-
-        maybe-eta T, !,
-        names Scope,
-        std.assert! (pi x\ precompile-aux (B x) N (B' x) (MM x), close-term-prune-safe-fun MM Ty M') "[TC] should not fail1",
-        precompile-aux Ty M' Ty' M.
-
-      % Detect maybe-llam term
-      precompile-aux (app [X|XS]) N (tc.maybe-llam-tm (app [app[X | PF] | NPF1]) Scope1) [X|M] :-
-        var X _ Scope, split-pf XS Scope PF NPF, 
-        not (NPF = []), !, % else XS is a list of distinct names, i.e. `app [X|XS]` is in PF
-        names Scope1,
-        std.fold-map NPF N precompile-aux NPF1 M. 
-
-      precompile-aux (prod Name Ty B) N (tc.prod-range (prod Name Ty' B') (r-ar z MaxAr)) P :- !,
-        count-prod Ty MaxAr,
-        std.assert! (pi x\ precompile-aux (B x) N (B' x) (MM x), close-term-prune-safe-fun MM Ty M) "[TC] should not fail2",
-        precompile-aux Ty M Ty' P.
-
-      % Working with fun
-      precompile-aux (fun N T F) A (fun N T F1) A2 :- !, A = A1,
-        /*precompile-aux IsP T A T1 A1,*/ pi x\ precompile-aux (F x) A1 (F1 x) A2.
-      
-      precompile-aux (app L) A (app L1) A1 :- !, std.fold-map L A precompile-aux L1 A1.
-      precompile-aux (let N T B F) A (let N T1 B1 F1) A3 :- !,
-        precompile-aux T A T1 A1, precompile-aux B A1 B1 A2, pi x\ precompile-aux (F x) A2 (F1 x) A3.
-      precompile-aux (fix N Rno Ty F) A (fix N Rno Ty1 F1) A2 :- !,
-        precompile-aux Ty A Ty1 A1, pi x\ precompile-aux (F x) A1 (F1 x) A2.
-      precompile-aux (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
-        precompile-aux T A T1 A1, precompile-aux Rty A1 Rty1 A2, std.fold-map B A2 precompile-aux B1 A3.
-      precompile-aux (primitive _ as C) A C A :- !.
-      precompile-aux (uvar _ _ as X) A X [X|A] :- !.
-      precompile-aux X A Y A :- name X, !, X = Y, !. % avoid loading "precompile-aux x A x A" at binders
-    }
-
-    pred goal i:term, o:term, o:list term.
-    goal T T' Vars' :- std.assert!(goal.precompile-aux T [] T' Vars) "[TC] cannot precompile goal", undup-same Vars Vars'. 
   }
 }
\ No newline at end of file
diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi
index 160e91ab9..4e19a490c 100644
--- a/apps/tc/elpi/solver.elpi
+++ b/apps/tc/elpi/solver.elpi
@@ -34,7 +34,7 @@ namespace tc {
     if-true print-links (coq.say "[TC] the links are" Links),
     tc.time-it tc.oTC-time-instance-search (
       do Links, Q,
-      tc.link.solve-cs,
+      tc.link.solve-cs,  % Trigger cs links (coercions + canonical structures)
       tc.link.solve-eta, % Trigger eta links
       tc.link.solve-llam % Trigger llam links
     ) "instance search".
diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v
index b2d1b46be..cecff5b79 100644
--- a/apps/tc/tests/test.v
+++ b/apps/tc/tests/test.v
@@ -237,7 +237,7 @@ Module HO_8.
     eexists.
     apply _.
     Unshelve.
-    apply nat.
+    auto.
   Qed.
 End HO_8.
 
@@ -569,14 +569,6 @@ Module CoqUvar3.
 
   Class c1 (T : Type -> Type -> Type).
   Instance i1 A: c1 (fun x y => f (A x y) (A x y)). Qed.
-  
-  Elpi Query TC.Solver lp:{{
-    tc.precomp.goal {{c1 (fun x y => lp:X (lp:A x y) y)}} C _,
-    Expected = app [{{c1}}, tc.maybe-eta-tm (fun _ _ Body1) _],
-    Body1 = (x\ tc.maybe-eta-tm (fun _ _ (Body2 x)) [x]),
-    Body2 = (x\y\ tc.maybe-llam-tm (app [app [X], (Y x y), y]) [x,y]),
-    std.assert! (C = Expected) "[TC] invalid compilation".
-  }}.
 
   (* Note: here interesting link-dedup *)
   Goal exists X (A: Type -> Type -> Type), c1 (fun x y => X (A x y) y).
@@ -618,7 +610,7 @@ Module CoqUvar4.
     std.assert! (C = Expected) "[TC] invalid compilation".
   }}.
 
-  (* Note: here interesting failtc-c1ing link-dedup *)
+  (* Note: here interesting fail link-dedup *)
   Goal forall f, exists X, c1 (X nat) -> 
     c1 (f nat nat).
     do 1 eexists.

From bbb7fbb68baba90e63619654f1e4d8844603cef0 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Sat, 10 Aug 2024 17:10:19 +0200
Subject: [PATCH 16/33] [TC] refactor filenames + reorder import

---
 apps/tc/elpi/WIP/force_llam.elpi              | 131 ------------
 apps/tc/elpi/WIP/modes.elpi                   |  44 ----
 apps/tc/elpi/base.elpi                        |  30 +--
 apps/tc/elpi/compile_goal.elpi                |  12 +-
 ...{ho_compile.elpi => compile_instance.elpi} | 190 +++++++++++++++++-
 .../tc/elpi/{compiler1.elpi => compiler.elpi} |   0
 apps/tc/elpi/ho_precompile.elpi               | 187 -----------------
 apps/tc/elpi/{ho_link.elpi => link.elpi}      |   0
 apps/tc/elpi/solver.elpi                      |   2 +-
 apps/tc/src/rocq_elpi_tc_register.ml          |   6 +-
 apps/tc/tests/importOrder/sameOrderCommand.v  |   4 +-
 apps/tc/theories/add_commands.v               |  45 ++---
 apps/tc/theories/tc.v                         |  49 ++---
 apps/tc/theories/wip.v                        |  21 +-
 14 files changed, 244 insertions(+), 477 deletions(-)
 delete mode 100644 apps/tc/elpi/WIP/force_llam.elpi
 delete mode 100644 apps/tc/elpi/WIP/modes.elpi
 rename apps/tc/elpi/{ho_compile.elpi => compile_instance.elpi} (61%)
 rename apps/tc/elpi/{compiler1.elpi => compiler.elpi} (100%)
 delete mode 100644 apps/tc/elpi/ho_precompile.elpi
 rename apps/tc/elpi/{ho_link.elpi => link.elpi} (100%)

diff --git a/apps/tc/elpi/WIP/force_llam.elpi b/apps/tc/elpi/WIP/force_llam.elpi
deleted file mode 100644
index d89f2a239..000000000
--- a/apps/tc/elpi/WIP/force_llam.elpi
+++ /dev/null
@@ -1,131 +0,0 @@
-% This is an effort for forcing llam links when used as input variables
-% in a premise call. However, this brings several issues to find
-% the right variable to activate the right link.s
-namespace force-llam {
-  pred is-uvar-destruct i:term, o:term.
-  is-uvar-destruct T R :- name T Hd _, name-pair R Hd _, !.
-  is-uvar-destruct T T :- is-uvar T.
-
-  % At compile time, given a premise p with a flexible argument X.
-  % If X is expected to be in input mode, we add the auxiliary clause 
-  % `solve-llam-t X`, so that, if any suspended
-  % llam link on X exists, then it is forced before solving p 
-  pred modes i:list string, i:list term, o:list prop.
-  modes ["o"] [] [] :- !.
-  modes ["+" | Ms] [X | Xs] [P | Ps] :- is-uvar-destruct X R, !, 
-    P = tc.link.solve-llam-t R, modes Ms Xs Ps.
-  modes ["!" | Ms] [X | Xs] [P | Ps] :- is-uvar-destruct X R, !, 
-    P = tc.link.solve-llam-t R, modes Ms Xs Ps.
-  modes [_ | Ms] [_ | Xs] Ps :- 
-    modes Ms Xs Ps.
-
-  % The following rule represents a try to force llam links when input of
-  % of other premises. 
-  compile-conclusion ff Goal Proof HOPremisesIn HOPremisesOut Premises Clause :-
-    coq.safe-dest-app Goal Class Args,
-    tc.get-mode {tc.get-TC-of-inst-type Class} Modes,
-    force-llam.modes Modes Args ForceLlam,
-    tc.make-tc Goal Proof Premises ff Clause1, 
-    Prems = [HOPremisesIn, ForceLlam, [Clause1], HOPremisesOut],
-    std.flatten Prems AllPremises,
-    Clause = do AllPremises.
-
-  %                            Scope        Var     Args       Rhs
-  pred progress-llam-refine i:list term, i:term, i:list term, o:term.
-  progress-llam-refine S V [A|As] R :- name A, not (std.mem! S A), !,
-    % prune (V' A) [A|S],
-    eta V (fun _ _ (x\ V' x)),
-    progress-llam-refine [A|S] (V' A) As R.
-  progress-llam-refine _ V [] V.
-  progress-llam-refine _ V As (app [V|As]).
-
-  pred split-pf i:list term, i:list term, o:list term, o:list term.
-  split-pf [] _ [] [] :- !.
-  split-pf [X|Xs] Old [X|Ys] L :- name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
-  split-pf Xs _ [] Xs.
-
-  pred lam->fun i:term, i:list term, i:any.
-  lam->fun T [] R :- !, std.unsafe-cast R R', copy T T', R' = T'.
-  lam->fun Hd [H|L] R :- !,
-    pi x\ (copy H x :- !) => lam->fun Hd L (R' x),
-    std.unsafe-cast R Rx, Rx = R'.
-
-  pred unify-align i:term, i:term, i:list term, i:list term.
-  unify-align (app L) Hd PF NPF :-
-    Len is {std.length L} - {std.length NPF}, Len >= 0,
-    std.split-at Len L L' NPF,
-    Z = app L',
-    coq.mk-app Z NPF TT,
-    lam->fun TT {std.append PF NPF} Hd.
-
-  pred unify-const i:term, i:term, i:list term.
-  unify-const N R [] :- !, copy N X, R = X.
-  unify-const N R [A|As] :- not found.aux, A == N, !,
-    pi x\ found.aux => (copy N x :- !) => unify-const N (R' x) As,
-    std.unsafe-cast R Rx, Rx = R'.
-  unify-const N R [_|As] :- 
-    pi x\ unify-const N (R' x) As,
-    std.unsafe-cast R Rx, Rx = R'.
-
-  pred unify-heuristics i:term, i:term.
-  unify-heuristics A T :- tc.unify-eq A T.
-  % unify-heuristics (app _ as A) (fun _ _ B) :- !,
-  %   coq.error "A",
-  %   eta-expand A (fun _ _ A'), pi x\ unify-heuristics (A' x) (B x).
-  % unify-heuristics (app _ as A) B :- var B Hd Tl, !,
-  %   split-pf Tl [] PF NPF, 
-  %   unify-align A Hd PF NPF.
-  % unify-heuristics A B :- name A, var B Hd Tl, !, % TODO: also const
-  %   unify-const A Hd Tl.
-  % unify-heuristics (app L) (app[X|L']) :-
-  %   var X, !,
-  %   Len is {std.length L} - {std.length L'}, Len > 0,
-  %   std.split-at Len L Hd L',
-  %   if (Hd = [X]) true (X = app Hd).
-  % unify-heuristics (app L) (app L') :-
-  %   std.forall2 L L' unify-heuristics. 
-  % % The following rule leaves elpi uvars outside PF in coq
-  % % unify-heuristics A B :- A = B.
-  % % The following seems to solve the problem of the previous rule
-  % % TODO: I don't understand why the following rule cant be written as:
-  % % unify-heuristics A B :- var B Hb Lb, A = app[Hb|Lb] 
-  % % without breaking test CoqUvar2
-  % unify-heuristics (uvar Ha []) (uvar Hb Lb) :- !,
-  %     Ha = app[Hb|Lb].
-  % unify-heuristics (fun _ _ Bo) (uvar Hb_ Lb1) :- not (distinct_names Lb1), !,
-  %   Lb1 = [_ | Lb],
-  %   std.spy-do![prune Z Lb,
-  %   % std.unsafe-cast Hb Hb1,
-  %   (pi x\ unify-heuristics (Bo x) Z),
-  %   Hb_ = 
-  %   coq.error "TODO" Z].
-  % unify-heuristics A B :- A = B.
-
-  pred llam-aux i:term, i:term.
-  llam-aux A (uvar _ S as T) :- distinct_names S, !, A = T. % Here, both A and T are in PF
-  llam-aux A (uvar _ _ as T) :- !, A = T.
-  llam-aux A (app [H|L] as T) :- var A, var H, !, get-vars T Vars, declare_constraint (llam A (app [H|L])) [_,A|Vars].
-  llam-aux A (app [H|L] as T) :- var H, !, get-vars T Vars, declare_constraint (llam A (app [H|L])) [_|Vars].
-  llam-aux A (app [H|L]) :- coq.mk-app H L T, !, unify-heuristics A T.
-
-  llam L (app [H|As]) :- var H _ S, !,
-    progress-llam-refine S H As Rhs,
-    llam-aux L Rhs.
-  llam L Rhs :- llam-aux L Rhs.
-
-  pred solve-llam-t-cond i:term, i:term.
-  :name "solve-llam-t-cond"
-  solve-llam-t-cond (uvar A _) (app [uvar B _ | _]) :- A = B.
-
-  % Aims to force a llam link suspended on the given variable
-  pred solve-llam-t o:term.
-  solve-llam-t X :- var X, !, declare_constraint (solve-llam-t X) [X].
-  solve-llam-t _.
-
-  constraint solve-llam solve-llam-t llam {
-    rule \ (solve-llam-t X) (llam A B) | (solve-llam-t-cond X B) <=> (unify-heuristics A B).
-    rule solve-llam \ (llam A B) <=> (unify-heuristics A B).
-    rule \ solve-llam.
-  }
-}
-
diff --git a/apps/tc/elpi/WIP/modes.elpi b/apps/tc/elpi/WIP/modes.elpi
deleted file mode 100644
index a7f1d58fc..000000000
--- a/apps/tc/elpi/WIP/modes.elpi
+++ /dev/null
@@ -1,44 +0,0 @@
-/* license: GNU Lesser General Public License Version 2.1 or later           */
-/* ------------------------------------------------------------------------- */
-
-% pred make-modes-cl i:gref, i:list term, i:term, i:list (list hint-mode), i:list (list term), o:prop.
-% make-modes-cl T V (prod _ _ X) HintModes L (pi x\ C x):-
-%   std.map HintModes (x\r\ [r|_] = x) FST,
-%   std.map HintModes (x\r\ [_|r] = x) LAST,
-%   pi x\ sigma NewL\
-%     std.map2 L FST (l\m\r\ if (m = mode-input) (r = [x | l]) (r = l)) NewL,
-%     make-modes-cl T [x | V] (X x) LAST NewL (C x).
-% make-modes-cl T V _ _ L Clause :-
-%   Ty = {coq.mk-app (global T) {std.rev V}},
-%   Clause = (pi s\ tc T Ty s :- std.forall L (x\ std.exists x var), !, coq.error "Invalid mode for" Ty).
-
-% takes the type of a class and build a list
-% of hint mode where the last element is mandatory
-pred make-last-hint-mode-input i:term, o:list hint-mode.
-make-last-hint-mode-input (prod _ _ (x\ (prod _ _ _) as T)) [mode-output | L] :-
-  pi x\ make-last-hint-mode-input (T x) L. 
-make-last-hint-mode-input (prod _ _ _) [mode-input].
-make-last-hint-mode-input (sort _) [].
-
-% build a list of the seme langht as the the passed one
-% where all the elements are []
-pred build-empty-list i:list B, o:list (list A).
-build-empty-list [] [].
-build-empty-list [_ | TL] [[] | L] :- 
-  build-empty-list TL L.
-
-% add the hint modes of a Class to the database.
-% note that if the Class has not specified hint mode
-% then we assume the hint mode to be - - - ... !
-pred add-modes i:gref.
-:if "add-modes"
-add-modes GR :-
-  % the hint mode is added only if not exists
-  if (not (tc.class GR _ _)) (
-    coq.env.typeof GR Ty,
-    coq.hints.modes GR "typeclass_instances" ModesProv,
-    if (ModesProv = []) (Modes = [{make-last-hint-mode-input Ty}]) (Modes = ModesProv),
-    % make-modes-cl GR [] Ty Modes {build-empty-list Modes} Cl,
-    % add-tc-db _ (after "firstHook") Cl,
-  ) true.
-add-modes _.
\ No newline at end of file
diff --git a/apps/tc/elpi/base.elpi b/apps/tc/elpi/base.elpi
index b819c0cf1..85a1c6047 100644
--- a/apps/tc/elpi/base.elpi
+++ b/apps/tc/elpi/base.elpi
@@ -145,32 +145,10 @@ pred count-prod i:term , o:nat.
 count-prod (prod _ _ B) (s N) :- !, pi x\ count-prod (B x) N.
 count-prod _ z.
 
-pred close-prop i:(A -> list prop), o:list prop.
-close-prop (x\ []) [] :- !.
-close-prop (x\ [X | Xs x]) [X| Xs'] :- !, close-prop Xs Xs'.
-close-prop (x\ [X x | Xs x]) [pi x\ X x | Xs'] :- !, close-prop Xs Xs'. 
-
-pred close-prop-no-prune i:(A -> list prop), o:list prop.
-close-prop-no-prune (x\ []) [] :- !.
-close-prop-no-prune (x\ [X x | Xs x]) [pi x\ X x | Xs'] :- !, 
-  close-prop-no-prune Xs Xs'. 
-
-% [close-term-ty (x\ L) Ty R] Ty is the type of x
-pred close-term-ty i:(term -> list prop), i:term, o:list prop.
-close-term-ty (x\ []) _ [] :- !.
-close-term-ty (x\ [X | Xs x]) Ty [X| Xs'] :- !, close-term-ty Xs Ty Xs'.
-close-term-ty (x\ [X x | Xs x]) Ty [@pi-decl `x` Ty x\ X x | Xs'] :- !, 
-  close-term-ty Xs Ty Xs'. 
-
-pred close-term-no-prune-ty i:(term -> list prop), i:term, o:list prop.
-close-term-no-prune-ty (x\ []) _ [] :- !.
-close-term-no-prune-ty (x\ [X x | Xs x]) Ty [@pi-decl `x` Ty x\ X x | Xs'] :- !, 
-  close-term-no-prune-ty Xs Ty Xs'. 
-
-pred close-term-no-prune-fun i:(term -> list term), i:term, o:list term.
-close-term-no-prune-fun (x\ []) _ [] :- !.
-close-term-no-prune-fun (x\ [X x | Xs x]) Ty [fun _ Ty X | Xs'] :- 
-  close-term-no-prune-fun Xs Ty Xs'.
+pred close-prop-no-prune-pi-decl i:(term -> list prop), i:term, o:list prop.
+close-prop-no-prune-pi-decl (x\ []) _ [] :- !.
+close-prop-no-prune-pi-decl (x\ [X x | Xs x]) Ty [@pi-decl `x` Ty x\ X x | Xs'] :- !, 
+  close-prop-no-prune-pi-decl Xs Ty Xs'. 
 
 pred free-names i:term, o:list term.
 free-names T L :-
diff --git a/apps/tc/elpi/compile_goal.elpi b/apps/tc/elpi/compile_goal.elpi
index 33ec8eef8..5e9e8bf94 100644
--- a/apps/tc/elpi/compile_goal.elpi
+++ b/apps/tc/elpi/compile_goal.elpi
@@ -1,6 +1,6 @@
 namespace tc {
   namespace compile {
-    namespace goall {
+    namespace goal {
       :index (_ _ 1)
       pred may-contract-to i:list term, i:term, i:term.
       may-contract-to _ N N :- !.
@@ -56,7 +56,7 @@ namespace tc {
         (pi x\ compile-full-aux (Bo x) [] (Bo' x) (BoL x)),
       % TODO: maybe attach to the links the list of used binders, to simply make this check?
       % Maybe L' is a pair list links and list binders per link, this way we can easily prune
-        close-term-no-prune-ty BoL Ty BoL',
+        close-prop-no-prune-pi-decl BoL Ty BoL',
         std.append L BoL' L'.
 
       pred compile-full-aux i:term, i:list prop, o:term, o:list prop.
@@ -147,9 +147,9 @@ namespace tc {
       compile-full Goal Goal' Links :- compile-full-aux Goal [] Goal' Links.
     }
 
-    pred goal' i:term, o:term, o:list prop.
-    :name "compile-goal'"
-    goal' Goal Goal' Links :- 
-      goall.compile-full-aux Goal [] Goal' Links.
+    pred goal i:term, o:term, o:list prop.
+    :name "compile-goal"
+    goal Goal Goal' Links :- 
+      goal.compile-full-aux Goal [] Goal' Links.
   }
 }
diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/compile_instance.elpi
similarity index 61%
rename from apps/tc/elpi/ho_compile.elpi
rename to apps/tc/elpi/compile_instance.elpi
index f0f473a0d..fd83ccb6d 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/compile_instance.elpi
@@ -1,6 +1,190 @@
 namespace tc {
   shorten tc.{r-ar, range-arity}.
 
+  namespace precomp {
+
+    namespace instance {
+      % Tells if the current name is a bound variables
+      pred is-name o:term.
+      % Tells if the current name stands for a uvar
+      pred is-uvar o:term.
+
+      :index (_ _ 1)
+      pred may-contract-to i:list term, i:term, i:term.
+      may-contract-to _ N N :- !.
+      may-contract-to L N (app [V|S]) :- var V, !,
+        std.forall [N|L] (x\ exists! S (may-contract-to [] x)).
+      may-contract-to L N (app [V|S]) :- is-uvar V, !,
+        std.forall [N|L] (x\ exists! S (may-contract-to [] x)).
+      may-contract-to L N (app [N|A]) :-
+        std.length A {std.length L},
+        std.forall2 {std.rev L} A (may-contract-to []).
+      may-contract-to L N (fun _ _ B) :-
+        pi x\ may-contract-to [x|L] N (B x).
+
+      :index (_ 1)
+      pred occurs-rigidly i:term, i:term.
+      occurs-rigidly N N :- name N, !.
+      occurs-rigidly _ (app [N|_]) :- is-uvar N, !, fail.
+      occurs-rigidly _ (app [N|_]) :- var N, !, fail.
+      occurs-rigidly N (app A) :- exists! A (occurs-rigidly N).
+      occurs-rigidly N (fun _ _ B) :- pi x\ occurs-rigidly N (B x).
+
+      pred maybe-eta-aux i:term, i:list term.
+      maybe-eta-aux (app[V|S]) L :- is-uvar V, !,
+        std.forall L (x\ exists! S (y\ may-contract-to [] x y)).
+      maybe-eta-aux (app[V|S]) L :- var V, !,
+        std.forall L (x\ exists! S (y\ may-contract-to [] x y)).
+      maybe-eta-aux (app [_|A]) L :-
+        SplitLen is {std.length A} - {std.length L},
+        split-at-not-fatal SplitLen A HD TL,
+        std.forall L (x\ not (exists! HD (occurs-rigidly x))),
+        std.forall2 {std.rev L} TL (may-contract-to []). 
+      maybe-eta-aux (fun _ _ B) L :-
+        pi x\ maybe-eta-aux (B x) [x|L].
+
+      pred maybe-eta i:term.
+      maybe-eta (fun _ _ B) :- pi x\ maybe-eta-aux (B x) [x].
+
+      pred free-var o:list term.
+      free-var L :-
+        std.findall (is-name _) T,
+        std.map T (x\y\ x = is-name y) L.
+
+      pred split-pf i:list term, i:list term, o:list term, o:list term.
+      split-pf [] _ [] [] :- !.
+      split-pf [X|Xs] Old [X|Ys] L :- is-name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
+      split-pf Xs _ [] Xs.
+
+      kind positivity type.
+      type is_pos positivity.
+      type is_neg positivity.
+      type is_neg_fix positivity.
+
+      :index (1 _)
+      pred neg i:positivity, o:positivity.
+      neg is_pos is_neg :- !.
+      neg is_neg is_pos :- !.
+      neg is_neg_fix is_neg_fix :- !.
+
+      macro @max-min :- r-ar inf z.
+
+      pred min-max-nat i:range-arity, i:range-arity, o:range-arity.
+      min-max-nat (r-ar A B) (r-ar A' B') (r-ar A'' B'') :- !,
+        min-nat A A' A'', max-nat B B' B''.
+
+      % TODO: this is incomplete: it lacks of some term constructors
+      pred get-range-arity-aux i:term, i:term, o:range-arity.
+      get-range-arity-aux N N (r-ar z z) :- !.
+      get-range-arity-aux _ N @max-min :- name N, !.
+      get-range-arity-aux T (app [T|L]) R :- !,
+        length-nat L Len,
+        std.fold L (r-ar Len Len) (x\y\w\ sigma M\ get-range-arity-aux T x M, min-max-nat y M w) R.
+      get-range-arity-aux T (app [_|L]) R :- !,
+        std.fold L @max-min (x\y\w\ sigma M\ get-range-arity-aux T x M, min-max-nat y M w) R.
+      get-range-arity-aux T (fun _ Ty B) R2 :- !,
+        get-range-arity-aux T Ty R,
+        (pi x\ get-range-arity-aux T (B x) R1),
+        min-max-nat R R1 R2.
+      get-range-arity-aux T (prod _ Ty B) R2 :- !,
+        get-range-arity-aux T Ty R,
+        (pi x\ get-range-arity-aux T (B x) R1),
+        min-max-nat R R1 R2.
+      get-range-arity-aux _ (global _) @max-min :- !.
+      get-range-arity-aux _ (uvar _) @max-min :- !.
+      get-range-arity-aux _ (sort _) @max-min :- !.
+      get-range-arity-aux _ (pglobal _ _) @max-min :- !.
+      get-range-arity-aux A B _ :- coq.error "Count maximal arity failure" A B.
+
+      pred get-range-arity i:term, i:term, i:term, o:range-arity.
+      get-range-arity _ Ty _ (r-ar z N) :- tc.get-TC-of-inst-type Ty _, !, count-prod Ty N.
+      get-range-arity B _ T N :- !, get-range-arity-aux B T N. 
+
+      pred precompile-aux i:positivity, i:term, i:nat, o:term, o:nat.
+      precompile-aux _ X A Y A :- name X, !, X = Y, !. % avoid loading "precompile-aux x A x A" at binders
+      precompile-aux _ (global _ as C) A C A :- !.
+      precompile-aux _ (pglobal _ _ as C) A C A :- !.
+      precompile-aux _ (sort _ as C) A C A :- !.
+      precompile-aux _ (primitive _ as C) A C A :- !.
+      precompile-aux _ T A (tc.coercion T Scope) (s A) :- coq.safe-dest-app T HD _, tc.coercion-unify HD, !, free-var Scope.
+      precompile-aux _ (app [global (const C) | _] as T) A (tc.canonical-projection T Scope N) (s A) :- coq.env.projection? C N, !, free-var Scope.
+      precompile-aux _ (app [primitive (proj P _) | _] as T) A (tc.canonical-projection T Scope 0) (s A) :- coq.env.primitive-projection? P _, !, free-var Scope.
+
+      % Detect maybe-eta term
+      % TODO: should I precompile also the type of the fun and put it in the output term
+      precompile-aux _ (fun Name Ty B as T) N (tc.maybe-eta-tm (fun Name Ty B') Scope) (s M) :-
+        maybe-eta T, !,
+        free-var Scope,
+        precompile-aux is_neg_fix Ty N _ N',
+        (pi x\ is-name x => precompile-aux is_neg_fix (B x) N' (B' x) M).
+
+      precompile-aux _ (app [X|XS]) N (tc.maybe-llam-tm (app [app[X | PF] | NPF1]) Scope) (s M) :-
+        if (is-uvar X) (Sc = []) (var X _ Sc), split-pf XS Sc PF NPF, 
+        not (NPF = []), !, % else XS is a list of distinct names, i.e. `app [X|XS]` is in PF
+        free-var Scope,
+        std.fold-map NPF N (precompile-aux is_neg_fix) NPF1 M. 
+
+      % Charge if we work with unification variable or local name
+      % And returns the subterms is a prod-range
+      precompile-aux IsP (prod Name Ty B) N (tc.prod-range (prod Name Ty' B') MaxAr) P :- !,
+        std.assert! (pi x\ get-range-arity x Ty (B x) MaxAr) "[TC] get-range-arity should not fail",
+        if (IsP = is_pos) (C = x\ is-uvar x) (C = x\ is-name x),
+        std.assert! (pi x\ C x => precompile-aux IsP (B x) N (B' x) M) "[TC] should not fail",
+        precompile-aux {neg IsP} Ty M Ty' P.
+
+      % Working with fun
+      precompile-aux _ (fun N T F) A (fun N T1 F1) A2 :- !,
+        precompile-aux _ T A T1 A1, pi x\ is-name x => precompile-aux is_neg_fix (F x) A1 (F1 x) A2.
+      
+      precompile-aux _ (app L) A (app L1) A1 :- !, std.fold-map L A (precompile-aux is_neg_fix) L1 A1.
+      precompile-aux _ X A X A :- var X, !.
+
+      % TODO: what about the following constructors?
+      % precompile-aux IsP (let N T B F) A (let N T1 B1 F1) A3 :- !,
+      %   precompile-aux IsP T A T1 A1, precompile-aux IsP B A1 B1 A2, pi x\ is-name x => precompile-aux IsP (F x) A2 (F1 x) A3.
+      % precompile-aux IsP (fix N Rno Ty F) A (fix N Rno Ty1 F1) A2 :- !,
+      %   precompile-aux IsP Ty A Ty1 A1, pi x\ is-name x => precompile-aux IsP (F x) A1 (F1 x) A2.
+      % precompile-aux IsP (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
+      %   precompile-aux IsP T A T1 A1, precompile-aux IsP Rty A1 Rty1 A2, std.fold-map B A2 (precompile-aux IsP) B1 A3.
+      % precompile-aux IsP (uvar M L as X) A W A1 :- var X, !, std.fold-map L A (precompile-aux IsP) L1 A1, coq.mk-app-uvar M L1 W.
+      % % when used in CHR rules
+      % precompile-aux IsP (uvar X L) A (uvar X L1) A1 :- std.fold-map L A (precompile-aux IsP) L1 A1.
+
+      pred get-univ-instances i:term, o:list univ-instance.
+      get-univ-instances T L :-
+        (pi x L\ fold-map (pglobal _ x) L _ [x | L] :- !) => fold-map T [] _ L, !.
+
+      pred get-univ i:term, o:list univ.
+      get-univ T L :-
+        coq.univ.variable.set.elements {coq.univ.variable.of-term T} Vars,
+        std.map Vars (x\r\ coq.univ.variable r x) L.
+
+    }
+
+    /*
+      [tc.precomp.instance T T' N] 
+      Returns T' N from T, where: 
+        T' is obtained by the replacement of
+          - all maybe-eta term `t1` with (tc.maybe-eta-tm `t1` `s`) where `s` = FV(`t1`)
+              ==> This helps knowing if a subterm should be replaced with a `eta-link`
+          - all `prod _ Ty (x\ Bo x)` with (tc.prod-range (prod _ Ty (x\ Bo x)) N), 
+            where N is represent the "maximal" application of `x` in `Bo`
+              for example:
+                let Ty = {{Type -> Type -> Type -> Type -> Type}},
+                and Bo = x\ c1 (x nat bool) (x nat) (x nat nat bool)
+              the term `prod _ Ty Bo` is replaced with
+                (tc.prod-range (prod _ T Bo) 3)
+              since x is applied at most 3 times in Bo
+                ==> This helps charging the right number of `eta-link` for map-deduplication rule
+        N is the number of problematic terms in T + nb of projections
+    */
+    pred instance i:term, o:term, o:nat, o:list univ, o:list univ-instance.
+    instance T T' N UnivConstL UnivInstL :-
+      tc.precomp.instance.get-univ T UnivConstL,
+      tc.precomp.instance.get-univ-instances T UnivInstL,
+      std.assert!(instance.precompile-aux instance.is_pos T z T' N) "[TC] cannot precompile instance".
+  }
+
   namespace compile {
 
     namespace instance {
@@ -12,8 +196,6 @@ namespace tc {
       % applied Ar times.
       pred name-pair o:term, o:term, o:nat.
 
-      pred force-llam-mem i:term, o:term.
-
       namespace decompile {
 
         pred decompile-term-aux i:term, i:pair (list term) (list prop), o:term, o:pair (list term) (list prop).
@@ -79,13 +261,13 @@ namespace tc {
 
         decompile-term-aux (fun Name Ty Bo) (pr XS L) (fun Name Ty' Bo') (pr XS2 L3) :- !,
           (pi x\ is-name x => decompile-term-aux (Bo x) (pr XS []) (Bo' x) (pr XS1 (L1x x))),
-          close-term-no-prune-ty L1x Ty L1,
+          close-prop-no-prune-pi-decl L1x Ty L1,
           decompile-term-aux Ty (pr XS1 L) Ty' (pr XS2 L2),
           std.append L1 L2 L3.
 
         decompile-term-aux (prod Name Ty Bo) (pr XS L) (prod Name Ty' Bo') (pr XS2 L3) :- !,
           (pi x\ is-name x => decompile-term-aux (Bo x) (pr XS []) (Bo' x) (pr XS1 (L1x x))),
-          close-term-no-prune-ty L1x Ty L1,
+          close-prop-no-prune-pi-decl L1x Ty L1,
           decompile-term-aux Ty (pr XS1 L) Ty' (pr XS2 L2),
           std.append L1 L2 L3.
 
diff --git a/apps/tc/elpi/compiler1.elpi b/apps/tc/elpi/compiler.elpi
similarity index 100%
rename from apps/tc/elpi/compiler1.elpi
rename to apps/tc/elpi/compiler.elpi
diff --git a/apps/tc/elpi/ho_precompile.elpi b/apps/tc/elpi/ho_precompile.elpi
deleted file mode 100644
index 353a5deca..000000000
--- a/apps/tc/elpi/ho_precompile.elpi
+++ /dev/null
@@ -1,187 +0,0 @@
-namespace tc {
-  shorten tc.{r-ar, range-arity}.
-
-  namespace precomp {
-
-    namespace instance {
-      % Tells if the current name is a bound variables
-      pred is-name o:term.
-      % Tells if the current name stands for a uvar
-      pred is-uvar o:term.
-
-      :index (_ _ 1)
-      pred may-contract-to i:list term, i:term, i:term.
-      may-contract-to _ N N :- !.
-      may-contract-to L N (app [V|S]) :- var V, !,
-        std.forall [N|L] (x\ exists! S (may-contract-to [] x)).
-      may-contract-to L N (app [V|S]) :- is-uvar V, !,
-        std.forall [N|L] (x\ exists! S (may-contract-to [] x)).
-      may-contract-to L N (app [N|A]) :-
-        std.length A {std.length L},
-        std.forall2 {std.rev L} A (may-contract-to []).
-      may-contract-to L N (fun _ _ B) :-
-        pi x\ may-contract-to [x|L] N (B x).
-
-      :index (_ 1)
-      pred occurs-rigidly i:term, i:term.
-      occurs-rigidly N N :- name N, !.
-      occurs-rigidly _ (app [N|_]) :- is-uvar N, !, fail.
-      occurs-rigidly _ (app [N|_]) :- var N, !, fail.
-      occurs-rigidly N (app A) :- exists! A (occurs-rigidly N).
-      occurs-rigidly N (fun _ _ B) :- pi x\ occurs-rigidly N (B x).
-
-      pred maybe-eta-aux i:term, i:list term.
-      maybe-eta-aux (app[V|S]) L :- is-uvar V, !,
-        std.forall L (x\ exists! S (y\ may-contract-to [] x y)).
-      maybe-eta-aux (app[V|S]) L :- var V, !,
-        std.forall L (x\ exists! S (y\ may-contract-to [] x y)).
-      maybe-eta-aux (app [_|A]) L :-
-        SplitLen is {std.length A} - {std.length L},
-        split-at-not-fatal SplitLen A HD TL,
-        std.forall L (x\ not (exists! HD (occurs-rigidly x))),
-        std.forall2 {std.rev L} TL (may-contract-to []). 
-      maybe-eta-aux (fun _ _ B) L :-
-        pi x\ maybe-eta-aux (B x) [x|L].
-
-      pred maybe-eta i:term.
-      maybe-eta (fun _ _ B) :- pi x\ maybe-eta-aux (B x) [x].
-
-      pred free-var o:list term.
-      free-var L :-
-        std.findall (is-name _) T,
-        std.map T (x\y\ x = is-name y) L.
-
-      pred split-pf i:list term, i:list term, o:list term, o:list term.
-      split-pf [] _ [] [] :- !.
-      split-pf [X|Xs] Old [X|Ys] L :- is-name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
-      split-pf Xs _ [] Xs.
-
-      kind positivity type.
-      type is_pos positivity.
-      type is_neg positivity.
-      type is_neg_fix positivity.
-
-      :index (1 _)
-      pred neg i:positivity, o:positivity.
-      neg is_pos is_neg :- !.
-      neg is_neg is_pos :- !.
-      neg is_neg_fix is_neg_fix :- !.
-
-      macro @max-min :- r-ar inf z.
-
-      pred min-max-nat i:range-arity, i:range-arity, o:range-arity.
-      min-max-nat (r-ar A B) (r-ar A' B') (r-ar A'' B'') :- !,
-        min-nat A A' A'', max-nat B B' B''.
-
-      % TODO: this is incomplete: it lacks of some term constructors
-      pred get-range-arity-aux i:term, i:term, o:range-arity.
-      get-range-arity-aux N N (r-ar z z) :- !.
-      get-range-arity-aux _ N @max-min :- name N, !.
-      get-range-arity-aux T (app [T|L]) R :- !,
-        length-nat L Len,
-        std.fold L (r-ar Len Len) (x\y\w\ sigma M\ get-range-arity-aux T x M, min-max-nat y M w) R.
-      get-range-arity-aux T (app [_|L]) R :- !,
-        std.fold L @max-min (x\y\w\ sigma M\ get-range-arity-aux T x M, min-max-nat y M w) R.
-      get-range-arity-aux T (fun _ Ty B) R2 :- !,
-        get-range-arity-aux T Ty R,
-        (pi x\ get-range-arity-aux T (B x) R1),
-        min-max-nat R R1 R2.
-      get-range-arity-aux T (prod _ Ty B) R2 :- !,
-        get-range-arity-aux T Ty R,
-        (pi x\ get-range-arity-aux T (B x) R1),
-        min-max-nat R R1 R2.
-      get-range-arity-aux _ (global _) @max-min :- !.
-      get-range-arity-aux _ uvar @max-min :- !.
-      get-range-arity-aux _ (sort _) @max-min :- !.
-      get-range-arity-aux _ (pglobal _ _) @max-min :- !.
-      get-range-arity-aux A B _ :- coq.error "Count maximal arity failure" A B.
-
-      pred get-range-arity i:term, i:term, i:term, o:range-arity.
-      get-range-arity _ Ty _ (r-ar z N) :- tc.get-TC-of-inst-type Ty _, !, count-prod Ty N.
-      get-range-arity B _ T N :- !, get-range-arity-aux B T N. 
-
-      pred precompile-aux i:positivity, i:term, i:nat, o:term, o:nat.
-      precompile-aux _ X A Y A :- name X, !, X = Y, !. % avoid loading "precompile-aux x A x A" at binders
-      precompile-aux _ (global _ as C) A C A :- !.
-      precompile-aux _ (pglobal _ _ as C) A C A :- !.
-      precompile-aux _ (sort _ as C) A C A :- !.
-      precompile-aux _ (primitive _ as C) A C A :- !.
-      precompile-aux _ T A (tc.coercion T Scope) (s A) :- coq.safe-dest-app T HD _, tc.coercion-unify HD, !, free-var Scope.
-      precompile-aux _ (app [global (const C) | _] as T) A (tc.canonical-projection T Scope N) (s A) :- coq.env.projection? C N, !, free-var Scope.
-      precompile-aux _ (app [primitive (proj P _) | _] as T) A (tc.canonical-projection T Scope 0) (s A) :- coq.env.primitive-projection? P _, !, free-var Scope.
-
-      % Detect maybe-eta term
-      % TODO: should I precompile also the type of the fun and put it in the output term
-      precompile-aux _ (fun Name Ty B as T) N (tc.maybe-eta-tm (fun Name Ty B') Scope) (s M) :-
-        maybe-eta T, !,
-        free-var Scope,
-        precompile-aux is_neg_fix Ty N _ N',
-        (pi x\ is-name x => precompile-aux is_neg_fix (B x) N' (B' x) M).
-
-      precompile-aux _ (app [X|XS]) N (tc.maybe-llam-tm (app [app[X | PF] | NPF1]) Scope) (s M) :-
-        if (is-uvar X) (Sc = []) (var X _ Sc), split-pf XS Sc PF NPF, 
-        not (NPF = []), !, % else XS is a list of distinct names, i.e. `app [X|XS]` is in PF
-        free-var Scope,
-        std.fold-map NPF N (precompile-aux is_neg_fix) NPF1 M. 
-
-      % Charge if we work with unification variable or local name
-      % And returns the subterms is a prod-range
-      precompile-aux IsP (prod Name Ty B) N (tc.prod-range (prod Name Ty' B') MaxAr) P :- !,
-        std.assert! (pi x\ get-range-arity x Ty (B x) MaxAr) "[TC] get-range-arity should not fail",
-        if (IsP = is_pos) (C = x\ is-uvar x) (C = x\ is-name x),
-        std.assert! (pi x\ C x => precompile-aux IsP (B x) N (B' x) M) "[TC] should not fail",
-        precompile-aux {neg IsP} Ty M Ty' P.
-
-      % Working with fun
-      precompile-aux _ (fun N T F) A (fun N T1 F1) A2 :- !,
-        precompile-aux _ T A T1 A1, pi x\ is-name x => precompile-aux is_neg_fix (F x) A1 (F1 x) A2.
-      
-      precompile-aux _ (app L) A (app L1) A1 :- !, std.fold-map L A (precompile-aux is_neg_fix) L1 A1.
-      precompile-aux _ X A X A :- var X, !.
-
-      % TODO: what about the following constructors?
-      % precompile-aux IsP (let N T B F) A (let N T1 B1 F1) A3 :- !,
-      %   precompile-aux IsP T A T1 A1, precompile-aux IsP B A1 B1 A2, pi x\ is-name x => precompile-aux IsP (F x) A2 (F1 x) A3.
-      % precompile-aux IsP (fix N Rno Ty F) A (fix N Rno Ty1 F1) A2 :- !,
-      %   precompile-aux IsP Ty A Ty1 A1, pi x\ is-name x => precompile-aux IsP (F x) A1 (F1 x) A2.
-      % precompile-aux IsP (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
-      %   precompile-aux IsP T A T1 A1, precompile-aux IsP Rty A1 Rty1 A2, std.fold-map B A2 (precompile-aux IsP) B1 A3.
-      % precompile-aux IsP (uvar M L as X) A W A1 :- var X, !, std.fold-map L A (precompile-aux IsP) L1 A1, coq.mk-app-uvar M L1 W.
-      % % when used in CHR rules
-      % precompile-aux IsP (uvar X L) A (uvar X L1) A1 :- std.fold-map L A (precompile-aux IsP) L1 A1.
-
-      pred get-univ-instances i:term, o:list univ-instance.
-      get-univ-instances T L :-
-        (pi x L\ fold-map (pglobal _ x) L _ [x | L] :- !) => fold-map T [] _ L, !.
-
-      pred get-univ i:term, o:list univ.
-      get-univ T L :-
-        coq.univ.variable.set.elements {coq.univ.variable.of-term T} Vars,
-        std.map Vars (x\r\ coq.univ.variable r x) L.
-
-    }
-
-    /*
-      [tc.precomp.instance T T' N] 
-      Returns T' N from T, where: 
-        T' is obtained by the replacement of
-          - all maybe-eta term `t1` with (tc.maybe-eta-tm `t1` `s`) where `s` = FV(`t1`)
-              ==> This helps knowing if a subterm should be replaced with a `eta-link`
-          - all `prod _ Ty (x\ Bo x)` with (tc.prod-range (prod _ Ty (x\ Bo x)) N), 
-            where N is represent the "maximal" application of `x` in `Bo`
-              for example:
-                let Ty = {{Type -> Type -> Type -> Type -> Type}},
-                and Bo = x\ c1 (x nat bool) (x nat) (x nat nat bool)
-              the term `prod _ Ty Bo` is replaced with
-                (tc.prod-range (prod _ T Bo) 3)
-              since x is applied at most 3 times in Bo
-                ==> This helps charging the right number of `eta-link` for map-deduplication rule
-        N is the number of problematic terms in T + nb of projections
-    */
-    pred instance i:term, o:term, o:nat, o:list univ, o:list univ-instance.
-    instance T T' N UnivConstL UnivInstL :-
-      tc.precomp.instance.get-univ T UnivConstL,
-      tc.precomp.instance.get-univ-instances T UnivInstL,
-      std.assert!(instance.precompile-aux instance.is_pos T z T' N) "[TC] cannot precompile instance".
-  }
-}
\ No newline at end of file
diff --git a/apps/tc/elpi/ho_link.elpi b/apps/tc/elpi/link.elpi
similarity index 100%
rename from apps/tc/elpi/ho_link.elpi
rename to apps/tc/elpi/link.elpi
diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi
index 4e19a490c..9163960ff 100644
--- a/apps/tc/elpi/solver.elpi
+++ b/apps/tc/elpi/solver.elpi
@@ -8,7 +8,7 @@ msolve L _ :- coq.ltac.fail _ "[TC] fail to solve" L.
 namespace tc {
   pred build-query-from-goal i:term, i:term, o:prop, o:list prop.
   build-query-from-goal Goal Proof Q Links :-
-    tc.compile.goal' Goal Goal' Links, !,
+    tc.compile.goal Goal Goal' Links, !,
     coq.safe-dest-app Goal' (global TC) TL',
     std.append TL' [Proof] TL, !,
     coq.elpi.predicate {tc.gref->pred-name TC} TL Q.
diff --git a/apps/tc/src/rocq_elpi_tc_register.ml b/apps/tc/src/rocq_elpi_tc_register.ml
index a952b9416..dd3800111 100644
--- a/apps/tc/src/rocq_elpi_tc_register.ml
+++ b/apps/tc/src/rocq_elpi_tc_register.ml
@@ -23,10 +23,7 @@ let gref2elpi_term (gref: GlobRef.t) : Cmd.raw =
 let observer_class (x : Typeclasses.typeclass) : Rocq_elpi_arg_HOAS.Cmd.raw list = 
   [Cmd.String "new_class"; gref2elpi_term x.cl_impl]
 
-let observer_default_instance (x : Typeclasses.typeclass) : Rocq_elpi_arg_HOAS.Cmd.raw list = 
-  [Cmd.String "default_instance";gref2elpi_term x.cl_impl]
-
-let observer_coercion add (x : Typeclasses.typeclass) : Rocq_elpi_arg_HOAS.Cmd.raw list = 
+let observer_coercion add (x : Typeclasses.typeclass) : Coq_elpi_arg_HOAS.Cmd.raw list = 
   let name2str x = Cmd.String (Names.Name.print x |> Pp.string_of_ppcmds) in
   let proj = x.cl_projs |> List.map (fun (x: Typeclasses.class_method) -> x.meth_name) in
   let mode = if add then "add_coercions" else "remove_coercions" in
@@ -63,7 +60,6 @@ let class_runner f cl =
     observer_coercion false; 
     observer_class; 
     observer_coercion true; 
-    (* observer_default_instance *)
   ] in
   List.iter (fun obs -> f (obs cl)) actions
 
diff --git a/apps/tc/tests/importOrder/sameOrderCommand.v b/apps/tc/tests/importOrder/sameOrderCommand.v
index caa7cba3f..41d7d6a09 100644
--- a/apps/tc/tests/importOrder/sameOrderCommand.v
+++ b/apps/tc/tests/importOrder/sameOrderCommand.v
@@ -2,7 +2,7 @@ From elpi.apps Require Export tc.
 
 From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.
 From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
-From elpi.apps.tc.elpi Extra Dependency "ho_link.elpi" as ho_link.
+From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
 From elpi.apps.tc.elpi Extra Dependency "tc_same_order.elpi" as tc_same_order.
 From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
 
@@ -13,7 +13,7 @@ Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
 Elpi Accumulate File unif.
-Elpi Accumulate File ho_link.
+Elpi Accumulate File link.
 Elpi Accumulate File tc_same_order.
 
 
diff --git a/apps/tc/theories/add_commands.v b/apps/tc/theories/add_commands.v
index 7c33b6105..939334e52 100644
--- a/apps/tc/theories/add_commands.v
+++ b/apps/tc/theories/add_commands.v
@@ -4,12 +4,11 @@
 From elpi.apps.tc Require Import db.
 
 From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
-From elpi.apps.tc.elpi Extra Dependency "ho_precompile.elpi" as ho_precompile.
-From elpi.apps.tc.elpi Extra Dependency "ho_compile.elpi" as ho_compile.
-From elpi.apps.tc.elpi Extra Dependency "compiler1.elpi" as compiler1.
+From elpi.apps.tc.elpi Extra Dependency "compile_instance.elpi" as compile_instance.
+From elpi.apps.tc.elpi Extra Dependency "compiler.elpi" as compiler.
 From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
 From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes.
-From elpi.apps.tc.elpi Extra Dependency "ho_link.elpi" as ho_link.
+From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
 From elpi.apps.tc.elpi Extra Dependency "parser_addInstances.elpi" as parser_addInstances.
 From elpi.apps.tc.elpi Extra Dependency "solver.elpi" as solver.
 From elpi.apps.tc.elpi Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
@@ -19,14 +18,9 @@ Set Warnings "+elpi".
 Elpi Command TC.AddAllInstances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
-Elpi Accumulate File ho_precompile.
-Elpi Accumulate File unif.
-Elpi Accumulate File ho_link.
-Elpi Accumulate File ho_compile.
-Elpi Accumulate File compiler1.
-Elpi Accumulate File modes.
+Elpi Accumulate File base tc_aux.
+Elpi Accumulate File unif modes link.
+Elpi Accumulate File compile_instance compiler.
 Elpi Accumulate lp:{{  
   main L :- 
     args->str-list L L1,
@@ -37,13 +31,9 @@ Elpi Accumulate lp:{{
 Elpi Command TC.AddInstances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File tc_aux.
-Elpi Accumulate File ho_precompile.
-Elpi Accumulate File ho_compile.
-Elpi Accumulate File unif.
-Elpi Accumulate File ho_link.
-Elpi Accumulate File compiler1.
-Elpi Accumulate File modes.
+Elpi Accumulate File base tc_aux.
+Elpi Accumulate File unif modes link.
+Elpi Accumulate File compile_instance compiler.
 Elpi Accumulate File parser_addInstances.
 Elpi Accumulate lp:{{
   main Arguments :- 
@@ -54,8 +44,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.AddAllClasses.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File tc_aux.
-Elpi Accumulate File modes.
+Elpi Accumulate File base tc_aux modes.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   % Ignore is the list of classes we do not want to add
@@ -68,8 +57,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.AddClasses.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File tc_aux.
-Elpi Accumulate File modes.
+Elpi Accumulate File base tc_aux modes.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   pred tc.add-all-classes i:list argument , i:tc.search-mode.
@@ -87,7 +75,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.AddHook.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File tc_aux.
+Elpi Accumulate File base tc_aux.
 Elpi Accumulate lp:{{
   pred tc.addHook i:grafting, i:string. 
   tc.addHook Grafting NewName :- 
@@ -117,8 +105,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.Declare.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File tc_aux.
-Elpi Accumulate File modes.
+Elpi Accumulate File base tc_aux modes.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   main _ :- coq.warning "TC.Declare" {tc.warning-name} 
@@ -132,8 +119,7 @@ with implicit arguments (those implicits will be neglected)", fail.
 Elpi Command TC.Pending_mode.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File tc_aux.
-Elpi Accumulate File modes.
+Elpi Accumulate File base tc_aux modes.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   main M :- 
@@ -146,8 +132,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.AddRecordFields.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
+Elpi Accumulate File base tc_aux.
 Elpi Accumulate  lp:{{
   pred tc.add_tc.records_unif.aux i:int, i:term, i:list term, i:constant, o:prop.
   tc.add_tc.records_unif.aux 0 T Args ProjConstant P :- !,
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index bbc102b45..0e911cd0f 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -4,14 +4,15 @@
 Declare ML Module "rocq-elpi.tc".
 
 From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
-(* From elpi.apps.tc.elpi Extra Dependency "compiler.elpi" as compiler. *)
-From elpi.apps.tc.elpi Extra Dependency "ho_precompile.elpi" as ho_precompile.
-From elpi.apps.tc.elpi Extra Dependency "ho_compile.elpi" as ho_compile.
-From elpi.apps.tc.elpi Extra Dependency "compile_goal.elpi" as compile_goal.
-From elpi.apps.tc.elpi Extra Dependency "compiler1.elpi" as compiler1.
+
 From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes.
 From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
-From elpi.apps.tc.elpi Extra Dependency "ho_link.elpi" as ho_link.
+
+From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
+From elpi.apps.tc.elpi Extra Dependency "compiler.elpi" as compiler.
+From elpi.apps.tc.elpi Extra Dependency "compile_goal.elpi" as compile_goal.
+From elpi.apps.tc.elpi Extra Dependency "compile_instance.elpi" as compile_instance.
+
 From elpi.apps.tc.elpi Extra Dependency "solver.elpi" as solver.
 From elpi.apps.tc.elpi Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
 
@@ -48,16 +49,9 @@ Elpi Accumulate lp:{{
 Elpi Tactic TC.Solver.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File tc_aux.
-Elpi Accumulate File unif.
-Elpi Accumulate File ho_link.
-(* Elpi Accumulate File compiler. *)
-Elpi Accumulate File ho_precompile.
-Elpi Accumulate File ho_compile.
-Elpi Accumulate File compiler1.
-Elpi Accumulate File create_tc_predicate.
-Elpi Accumulate File compile_goal.
-Elpi Accumulate File modes.
+Elpi Accumulate File base tc_aux.
+Elpi Accumulate File unif modes link.
+Elpi Accumulate File compile_instance compile_goal.
 Elpi Accumulate File solver.
 Elpi Query lp:{{
   sigma Options\ 
@@ -80,14 +74,10 @@ Elpi Query lp:{{
 Elpi Command TC.Compiler.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File tc_aux.
+Elpi Accumulate File base tc_aux.
+Elpi Accumulate File unif modes link.
+Elpi Accumulate File compile_instance compiler.
 Elpi Accumulate File create_tc_predicate.
-Elpi Accumulate File ho_precompile.
-Elpi Accumulate File ho_compile.
-Elpi Accumulate File unif.
-Elpi Accumulate File ho_link.
-Elpi Accumulate File compiler1.
-Elpi Accumulate File modes.
 Elpi Accumulate lp:{{
 
   /* 
@@ -123,11 +113,6 @@ Elpi Accumulate lp:{{
       coq.locate Cl GR, tc.add-class-gr tc.classic GR
     ) "Compiler for Class".
 
-  % used to build ad-hoc instance for eta-reduction on the argument of 
-  % Cl that have function type
-  main [str "default_instance", str Cl] :- !,
-    tc.eta-reduction-aux.main Cl.
-
   main A :- coq.error "Fail in TC.Compiler: not a valid input entry" A.
 }}.
 
@@ -136,7 +121,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.Set_deterministic.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File tc_aux.
+Elpi Accumulate File base tc_aux.
 Elpi Accumulate lp:{{
   main [str ClassStr] :- 
     coq.locate ClassStr ClassGR, 
@@ -150,7 +135,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.Get_class_info.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File tc_aux.
+Elpi Accumulate File base tc_aux.
 Elpi Accumulate lp:{{
   main [str ClassStr] :- 
     coq.locate ClassStr ClassGR, 
@@ -170,7 +155,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.Unfold.
 Elpi Accumulate Db tc_options.db.
 Elpi Accumulate Db tc.db.
-Elpi Accumulate File tc_aux.
+Elpi Accumulate File base tc_aux.
 Elpi Accumulate lp:{{
   pred tc.add-unfold i:gref.
   tc.add-unfold (const C) :-
@@ -185,6 +170,8 @@ Elpi Accumulate lp:{{
 }}.
 
 
+(* Registering, activating the new tactic TC.Solver for TC resolution
+   + overriding all TC resolution *)
 Elpi TC Solver Register TC.Solver.
 Elpi TC Solver Activate TC.Solver.
 Elpi TC Solver Override TC.Solver All.
diff --git a/apps/tc/theories/wip.v b/apps/tc/theories/wip.v
index d7060d727..6b88f79d2 100644
--- a/apps/tc/theories/wip.v
+++ b/apps/tc/theories/wip.v
@@ -1,20 +1,21 @@
 (* license: GNU Lesser General Public License Version 2.1 or later           *)
 (* --------------------------------------------------------------------------*)
 
-Declare ML Module "rocq-elpi.tc".
+(* Declare ML Module "coq-elpi.tc".
 From elpi Require Import elpi.
 
 From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes.
-From elpi.apps.tc.elpi Extra Dependency "ho_precompile.elpi" as ho_precompile.
-From elpi.apps.tc.elpi Extra Dependency "ho_compile.elpi" as ho_compile.
-From elpi.apps.tc.elpi Extra Dependency "compiler1.elpi" as compiler1.
-From elpi.apps.tc.elpi Extra Dependency "ho_link.elpi" as ho_link.
+
+From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
+From elpi.apps.tc.elpi Extra Dependency "compiler.elpi" as compiler.
+From elpi.apps.tc.elpi Extra Dependency "compile_instance.elpi" as compile_instance.
+
 From elpi.apps.tc.elpi Extra Dependency "parser_addInstances.elpi" as parser_addInstances.
 From elpi.apps.tc.elpi Extra Dependency "alias.elpi" as alias.
 From elpi.apps.tc.elpi Extra Dependency "solver.elpi" as solver.
 From elpi.apps.tc.elpi Extra Dependency "rewrite_forward.elpi" as rforward.
 From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
-From elpi.apps.tc.elpi Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
+From elpi.apps.tc.elpi Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate. *)
 
 (* From elpi.apps Require Import tc.
 Set Warnings "+elpi".
@@ -24,10 +25,10 @@ Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
-Elpi Accumulate File ho_link.
+Elpi Accumulate File link.
 Elpi Accumulate File modes.
-Elpi Accumulate File ho_precompile.
-Elpi Accumulate File compiler1.
+Elpi Accumulate File compile_instance.
+Elpi Accumulate File compiler.
 Elpi Accumulate File ho_compile.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate File solver.
@@ -48,7 +49,7 @@ Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
-Elpi Accumulate File ho_link.
+Elpi Accumulate File link.
 Elpi Accumulate File alias.
 Elpi Accumulate lp:{{
   main [trm New, trm Old] :-

From 1b73a9aa97c5ada5fc72aa3a2016fb040e51fe96 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Sat, 10 Aug 2024 18:04:40 +0200
Subject: [PATCH 17/33] [TC] refactor of build-eta-llam-links

---
 apps/tc/elpi/compile_goal.elpi     | 42 ++--------------------
 apps/tc/elpi/compile_instance.elpi | 28 ++++-----------
 apps/tc/elpi/link.elpi             | 58 ++++++++++++++++++++++--------
 apps/tc/tests/test.v               |  2 +-
 4 files changed, 54 insertions(+), 76 deletions(-)

diff --git a/apps/tc/elpi/compile_goal.elpi b/apps/tc/elpi/compile_goal.elpi
index 5e9e8bf94..340c76f60 100644
--- a/apps/tc/elpi/compile_goal.elpi
+++ b/apps/tc/elpi/compile_goal.elpi
@@ -35,11 +35,6 @@ namespace tc {
       pred maybe-eta i:term.
       maybe-eta (fun _ _ B) :- pi x\ maybe-eta-aux (B x) [x].
 
-      pred split-pf i:list term, i:list term, o:list term, o:list term.
-      split-pf [] _ [] [] :- !.
-      split-pf [X|Xs] Old [X|Ys] L :- name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
-      split-pf Xs _ [] Xs.
-
       pred used i:term, i:term.
       used X (uvar _ S) :- std.mem! S X, !.
       used X (fun _ _ Bo) :- pi x\ used X (Bo x).
@@ -86,41 +81,10 @@ namespace tc {
         compile-full-aux Ty L Ty' LTy,
         compile-full-aux-close Bo Ty LTy Bo' L'.
 
-      % NOTE: when compiling t = (app [X, x, y]) and [x,y] are distinct_names,
-      %       then the coq variable has not [x,y] in scope, it is applied to
-      %       them. Note also that t is a problematic term that cannot be
-      %       exposed to the else unification algorithm.  
-      %       The solution is to build the following links:  
-      %       X =η (λa.Y a)
-      %       a |- Y a =η (λb.Z a b)
-      %       and expose a variable W at toplevel having Z has head and [x, y]
-      %       as scope
-
-      % NOTE: when compiling t = (app [X, a, x]) where a is a constant and x a
-      %       name, we build a llam link.  
-      %       The link will be: T x =L X a x  
-      %       the exposed variable in the term will be T x
-
-      % NOTE: here a combination of eta and llam:  
-      %       let t = (app [X x y, z, c, w, d]) where X is a coq var with x and
-      %       y in scope, z and w are names and c, d are constants.  
-      %       In this case, the links should be:  
-      %       X x y =η (λa.Y x y a)  
-      %       a |- Z x y a w =L (app[Y x y a, c w d])  
-      %       The returned variable is Z x y a w
-
-      % Link for beta-redex (Uvar in PF)
-      % BUILD CHAIN OF LINKS-ETA from X to V...
       % TODO: to avoid too many chain for the same var, maybe pass a list into the fold
-      compile-full-aux (app [(uvar _ Scope as V) | S] as T) L G' L'' :- !,
-        % By construction the scope of a uvar is a list of distinct name
-        std.fold-map S L compile-full-aux S' L', % LS = Links built for S
-        coq.typecheck V Ty ok,
-        split-pf S' Scope PF NPF,
-        free-names T Names,
-        tc.link.build-eta-llam-links V Scope Ty Names PF NPF L' G'' L'',
-        prune G' Names,
-        var G' G'' Names.
+      compile-full-aux (app [(uvar _ _ as V) | S]) L G' L'' :- !,
+        std.fold-map S L compile-full-aux S' L', % L' = Links built for S
+        tc.link.build-eta-llam-links (app [V|S']) L' G' L''.
 
       compile-full-aux (app L) A (app L1) A1 :- !, std.fold-map L A compile-full-aux L1 A1.
 
diff --git a/apps/tc/elpi/compile_instance.elpi b/apps/tc/elpi/compile_instance.elpi
index fd83ccb6d..1921c9ee4 100644
--- a/apps/tc/elpi/compile_instance.elpi
+++ b/apps/tc/elpi/compile_instance.elpi
@@ -119,7 +119,7 @@ namespace tc {
         (pi x\ is-name x => precompile-aux is_neg_fix (B x) N' (B' x) M).
 
       precompile-aux _ (app [X|XS]) N (tc.maybe-llam-tm (app [app[X | PF] | NPF1]) Scope) (s M) :-
-        if (is-uvar X) (Sc = []) (var X _ Sc), split-pf XS Sc PF NPF, 
+        is-uvar X, split-pf XS [] PF NPF, 
         not (NPF = []), !, % else XS is a list of distinct names, i.e. `app [X|XS]` is in PF
         free-var Scope,
         std.fold-map NPF N (precompile-aux is_neg_fix) NPF1 M. 
@@ -237,27 +237,11 @@ namespace tc {
           std.fold-map NPF (pr XS L1) decompile-term-aux Tl (pr XS' L2), 
           NL = tc.link.llam Y (app [Hd|Tl]).
 
-        % Maybe-llam when H is a hole appearing in the shelved goals
-        % This happens when the instance to be compiled comes from the context
-        % Example: Goal exists (X : T1 -> T2), forall a, c (X a) -> ...
-        %            intros; eexists. (* In the context we have the instance `H: c (?X a)` *)
-        decompile-term-aux (tc.maybe-llam-tm (app[app[V | PF] | NPF] as T) S_) L G'' (pr XS' L'') :-  !,
-          var V _ Scope, !,
-          std.fold-map NPF L decompile-term-aux NPF' (pr XS' L'),
-          free-names T Names,
-          coq.typecheck V Ty ok,
-          tc.link.build-eta-llam-links V Scope Ty Names PF NPF' L' G' L'',
-          prune G'' Names,
-          var G'' G' Names.
-
-        % HO var when H is a hole appearing in the shelved goals
-        decompile-term-aux (app [V|PF] as T) (pr XS' L') G'' (pr XS' L'') :-
-          var V _ Scope, !,
-          free-names T Names,
-          coq.typecheck V Ty ok,
-          tc.link.build-eta-llam-links V Scope Ty Names PF [] L' G' L'',
-          prune G'' Names,
-          var G'' G' Names.
+        % Here we have a coq evar applied to some terms. In this case, we build
+        % eta-llam links after the decompilation of S.
+        decompile-term-aux (app [(uvar _ _ as V)|S]) PR H (pr XS L') :- !,
+          std.fold-map S PR decompile-term-aux S' (pr XS L),
+          tc.link.build-eta-llam-links (app [V|S']) L H L'.
 
         decompile-term-aux (fun Name Ty Bo) (pr XS L) (fun Name Ty' Bo') (pr XS2 L3) :- !,
           (pi x\ is-name x => decompile-term-aux (Bo x) (pr XS []) (Bo' x) (pr XS1 (L1x x))),
diff --git a/apps/tc/elpi/link.elpi b/apps/tc/elpi/link.elpi
index 84158c6ac..52eb9ad80 100644
--- a/apps/tc/elpi/link.elpi
+++ b/apps/tc/elpi/link.elpi
@@ -9,28 +9,58 @@ namespace tc {
       (pi X H L Ign\ fold-map X L X [H|L] :- var X H Ign, !) => 
         fold-map T [] _ R.
 
-    % [build-eta-llam-links LHS Scope Ty Names PF NPF OldLinks NewVar NewLinks]
-    % Builds the eta/llam links at runtime for a term having the shape 
-    % `app[(uvar X Scope as V) | L]`.
-    % LHS should be V, Scope the scope of V, TODO: finish to document this...
+    pred split-pf i:list term, i:list term, o:list term, o:list term.
+    split-pf [] _ [] [] :- !.
+    split-pf [X|Xs] Old [X|Ys] L :- name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
+    split-pf Xs _ [] Xs.
+
+    % [build-eta-llam-links.aux LHS Scope Ty Names PF NPF OldLinks NewVar NewLinks]
     :index(_ _ _ _ 3)
-    % TODO: the argument Ty is unused, i.e. the binders of the eta links have no type...
-    %                           LHS      Scope      Ty          Names        PF         NPF        OldLinks    NewVar
-    pred build-eta-llam-links i:term, i:list term, o:term, i:list term, i:list term, i:list term, i:list prop, o:term, o:list prop.
-    build-eta-llam-links LHS _ _       Names []  NPF OL HD [tc.link.llam T (app [LHS | NPF]) | OL] :- !,
+    pred build-eta-llam-links.aux i:term, i:list term, o:term, i:list term, i:list term, i:list term, i:list prop, o:term, o:list prop.
+    build-eta-llam-links.aux LHS _ _       Names []  NPF OL HD [llam T (app [LHS | NPF]) | OL] :- !,
       std.assert! (not (NPF = [])) "[TC] NPF List should not be empty",
       prune T Names,
       var T HD _. 
-    build-eta-llam-links LHS SC (prod _ Ty _)       _    [X] []  OL HD [tc.link.eta LHS (fun `_` Ty (x\ V x)) | OL] :- !,
+    build-eta-llam-links.aux LHS SC (prod _ Ty _)       _    [X] []  OL HD [eta LHS (fun `_` Ty (x\ V x)) | OL] :- !,
       prune V SC, var (V X) HD _.
-    build-eta-llam-links LHS SC (prod _ Ty Bo) Names [X|XS] NPF OL HD [tc.link.eta LHS (fun `_` Ty (x\ LHS' x)) | L] :- !,
+    build-eta-llam-links.aux LHS SC (prod _ Ty Bo) Names [X|XS] NPF OL HD [eta LHS (fun `_` Ty (x\ LHS' x)) | L] :- !,
     % TODO: unfold Ty if needed...
       std.append SC [X] SC',
-      prune LHS' SC, build-eta-llam-links (LHS' X) SC' (Bo X) Names XS NPF OL HD L.
-    build-eta-llam-links LHS SC Ty Names ([_|_] as PF) NPF OL HD L :-
+      prune LHS' SC, build-eta-llam-links.aux (LHS' X) SC' (Bo X) Names XS NPF OL HD L.
+    build-eta-llam-links.aux LHS SC Ty Names ([_|_] as PF) NPF OL HD L :-
       Ty' = prod _ _ _, coq.unify-eq Ty Ty' ok, !,
-      build-eta-llam-links LHS SC Ty' Names PF NPF OL HD L.
-
+      build-eta-llam-links.aux LHS SC Ty' Names PF NPF OL HD L.
+    
+    % [build-eta-llam-links T OldLinks X NewLinks]  
+    % T = app[(uvar _ Scope) | S] this term is problematic and asks for the
+    % creation of eta- and/or llam-links. Below some examples:
+
+    % eta: when compiling t = (app [X, x, y]) and [x,y] are distinct_names, then
+    %     the coq variable has not [x,y] in scope: it is applied to them.  
+    %     The solution is to build the following links:  
+    %     NewLinks = [X =η (λa.Y a),     a |- Y a =η (λb.Z a b)]
+    %     and the exposed variable is G, given by `var G Z [x, y]`
+
+    % llam: when compiling t = (app [X, a, x]) where a is a constant and x a
+    %       name, we build a llam link.  
+    %       The link will be: NewLinks ] = [T x =L X a x]  
+    %       and the exposed variable is G, given by `var G T [x]`
+
+    % eta-llam: here a combination of eta and llam:  
+    %       let t = (app [X x y, z, c, w, d]) where X is a coq var with x and y
+    %       in scope, z and w are names and c, d are constants.  
+    %       In this case, the links should be:  
+    %       NewLinks = [X x y =η (λa.Y x y a),   a |- Z x y a w =L (app[Y x y a, c w d])]  
+    %       and the exposed variable is G, given by `var Z T [x, y, z, w]`  
+    pred build-eta-llam-links i:term, i:list prop, o:term, o:list prop.
+    build-eta-llam-links (app[(uvar _ Scope as V) | S] as T) Links G NewLinks :- !,
+      coq.typecheck V Ty ok,
+      split-pf S Scope PF NPF,
+      free-names T Names,
+      build-eta-llam-links.aux V Scope Ty Names PF NPF Links LhsHd NewLinks,
+      prune G Names,
+      var G LhsHd Names.
+    build-eta-llam-links T _ _ _ :- coq.error "[TC] invalid call to build-eta-llam-links:" T.
 
     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     % ETA LINK                                                                 %
diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v
index cecff5b79..75b48030b 100644
--- a/apps/tc/tests/test.v
+++ b/apps/tc/tests/test.v
@@ -606,7 +606,7 @@ Module CoqUvar4.
     tc.precomp.instance {{c1 (fun x y => lp:X (lp:A x y) y)}} C _ _ _,
     Expected = app [{{c1}}, tc.maybe-eta-tm (fun _ _ Body1) _],
     Body1 = (x\ tc.maybe-eta-tm (fun _ _ (Body2 x)) [x]),
-    Body2 = (x\y\ tc.maybe-llam-tm (app [app [X], (Y x y), y]) [y,x]),
+    Body2 = (x\y\ app [X, (Y x y), y]),
     std.assert! (C = Expected) "[TC] invalid compilation".
   }}.
 

From 9f4894e067c8bb2d6387093f7c64ba1308cca456 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 20 Aug 2024 11:07:16 +0200
Subject: [PATCH 18/33] [TC] avoid a backtrack

---
 apps/tc/elpi/link.elpi | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/apps/tc/elpi/link.elpi b/apps/tc/elpi/link.elpi
index 52eb9ad80..45f69a179 100644
--- a/apps/tc/elpi/link.elpi
+++ b/apps/tc/elpi/link.elpi
@@ -198,7 +198,7 @@ namespace tc {
       cs (uvar _ as V) (app [HD | _] as T) :- 
         if (HD = global (const Proj), tc.proj->record Proj Record)
           (reduce-cs V T Record Proj)
-          (coq.unify-eq V T ok).
+          (coq.unify-eq V T ok), !.
       cs T1 T2 :- not (T2 = app _), !, coq.unify-eq T1 T2 ok.
 
       pred unify-under-ctx i:list term, i:list term, i:term, i:term, i:term, i:term.

From cbb7be18d3abf08f1400ce4c058ab01817fe11bc Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Thu, 19 Sep 2024 16:04:54 +0200
Subject: [PATCH 19/33] [TC] clean compile-conclusion predicate

---
 _opam                                        |  1 +
 apps/tc/elpi/compile_instance.elpi           | 51 ++++++++++----------
 apps/tc/tests/test.v                         |  4 +-
 apps/tc/tests/test_HO.v                      |  4 +-
 apps/tc/tests/test_backtrack_several_goals.v |  4 +-
 apps/tc/tests/test_scope.v                   |  1 -
 apps/tc/tests/test_tc.v                      |  2 -
 7 files changed, 33 insertions(+), 34 deletions(-)
 create mode 120000 _opam

diff --git a/_opam b/_opam
new file mode 120000
index 000000000..343b677d2
--- /dev/null
+++ b/_opam
@@ -0,0 +1 @@
+/home/dfissore/Documents/github/COQ_ELPI_DEV/_opam
\ No newline at end of file
diff --git a/apps/tc/elpi/compile_instance.elpi b/apps/tc/elpi/compile_instance.elpi
index 1921c9ee4..186561538 100644
--- a/apps/tc/elpi/compile_instance.elpi
+++ b/apps/tc/elpi/compile_instance.elpi
@@ -371,6 +371,10 @@ namespace tc {
         pi x y\ name-pair P x (s N) => is-uvar x => add-link-eta-dedup F (r-ar M N) P PTy [pr x y|Acc] PremR (Clause x y).
       add-link-eta-dedup _ Ar P PTy _ _ _ :- coq.error "[TC] add-link-eta-dedup error" Ar P PTy. 
 
+      pred deterministic-prem i:gref, i:prop, o:prop.
+      deterministic-prem TC P (do-once P) :- tc.class TC _ tc.deterministic _, !.
+      deterministic-prem _ P P.
+
       pred compile-premise
         i:list term,
         o:list term,
@@ -382,16 +386,14 @@ namespace tc {
         i:list term,
         i:list prop,
         o:prop.
-      compile-premise L L2 P PTy ProofHd IsPositive ITy ProofTlR PremR Clause :-
-        ((pi a b c\ tc.get-TC-of-inst-type (tc.prod-range a c) b :- tc.get-TC-of-inst-type a b) => 
-          tc.get-TC-of-inst-type PTy TC), !,
+      compile-premise L L2 P PTy ProofHd IsPositive ITy ProofArgsR PremR Clause :-
+        (pi a b c\ tc.get-TC-of-inst-type (tc.prod-range a c) b :- tc.get-TC-of-inst-type a b) => 
+          tc.get-TC-of-inst-type PTy TC, !,
         compile-ty L L1 P {neg IsPositive} PTy [] [] NewPrem,
-        if (tc.class TC _ tc.deterministic _)
-          (NewPrem' = do-once NewPrem)
-          (NewPrem' = NewPrem),
-        compile-ty L1 L2 ProofHd IsPositive ITy ProofTlR [NewPrem' | PremR] Clause.
-      compile-premise L L1 _ _ ProofHd IsPositive ITy ProofTlR PremR Clause :-
-        compile-ty L L1 ProofHd IsPositive ITy ProofTlR PremR Clause. 
+        deterministic-prem TC NewPrem NewPrem',
+        compile-ty L1 L2 ProofHd IsPositive ITy ProofArgsR [NewPrem' | PremR] Clause.
+      compile-premise L L1 _ _ ProofHd IsPositive ITy ProofArgsR PremR Clause :-
+        compile-ty L L1 ProofHd IsPositive ITy ProofArgsR PremR Clause. 
 
       pred compile-ty 
         i:list term,
@@ -402,39 +404,38 @@ namespace tc {
         i:list term,
         i:list prop,
         o:prop.
-      compile-ty L L1 ProofHd IsPositive (tc.prod-range (prod N Ty Bo) Arity) ProofTlR PremR Clause :- !,
+      compile-ty L L1 ProofHd IsPositive (tc.prod-range (prod N Ty Bo) Arity) ProofArgsR PremR Clause :- !,
         std.do![
           if (IsPositive = tt) 
             (Clause = (pi x\ C x), E = is-uvar) 
             (clean-term Ty Ty', Clause = (pi x\ decl x N Ty' => C x), E = is-name),
           pi p\ sigma F\
-            F = compile-premise L L1 p Ty ProofHd IsPositive (Bo p) [p|ProofTlR],
+            F = compile-premise L L1 p Ty ProofHd IsPositive (Bo p) [p|ProofArgsR],
             decl p N Ty' =>
             name-pair p p z => E p => add-link-eta-dedup F Arity p Ty [] PremR (C p)
         ].
-      compile-ty L L2 ProofHd IsPositive Goal ProofTlR PremR Clause :-
+      compile-ty L L2 ProofHd IsPositive Goal ProofArgsR PremR Clause :-
         std.do![    
-          coq.mk-app ProofHd {std.rev ProofTlR} Proof,
-          decompile.decompile-term L L1 Proof Proof' Prem1,
-          decompile.decompile-term L1 L2 Goal Goal' Prem2,
-          compile-conclusion IsPositive Goal' Proof' Prem2 Prem1 {std.rev PremR} Clause
+          coq.mk-app ProofHd {std.rev ProofArgsR} Proof,
+          decompile.decompile-term L L1 Proof Proof' EmptyLinks,
+          std.assert! (EmptyLinks = []) "[TC] should be empty", 
+          decompile.decompile-term L1 L2 Goal Goal' Links,
+          compile-conclusion IsPositive Goal' Proof' Links {std.rev PremR} Clause
         ].
 
       pred compile-conclusion 
         i:bool,             % tt if the term is in positive position
         i:term,             % the goal (invariant: it is a constant or a application)
         i:term,             % the proof
-        i:list prop,        % the list of HOPremises in input mode
-        i:list prop,        % the list of HOPremises in output mode
+        i:list prop,        % the list of links
         i:list prop,        % the premises
         o:prop.             % the compiled clause for the instance
 
-      compile-conclusion tt Goal Proof HOPremisesIn HOPremisesOut Premises Clause :-
-        std.append {std.append HOPremisesIn Premises} HOPremisesOut AllPremises,
+      compile-conclusion tt Goal Proof Links Premises Clause :-
+        std.append Links Premises AllPremises,
         tc.make-tc Goal Proof AllPremises tt Clause.
-      compile-conclusion ff Goal Proof HOPremisesIn HOPremisesOut Premises Clause :-
-        tc.make-tc Goal Proof Premises ff Clause1, 
-        Clause = (do HOPremisesIn, Clause1, do HOPremisesOut).
+      compile-conclusion ff Goal Proof Links Premises (do Links, Clause) :-
+        tc.make-tc Goal Proof Premises ff Clause.
 
       pred context i:goal-ctx, o:list prop.
       context [] [].
@@ -465,9 +466,9 @@ namespace tc {
     % If the instance is polymorphic, we wrap its gref into the pglobal constructor
     instance-gr InstGR (pi x\ Clause x) :- coq.env.univpoly? InstGR _, !,
       coq.env.typeof InstGR Ty,
-      pi x\ tc.compile.instance Ty (pglobal InstGR x) (Clause x).
+      pi x\ instance Ty (pglobal InstGR x) (Clause x).
     instance-gr InstGR Clause :-
       coq.env.typeof InstGR Ty,
-      tc.compile.instance Ty (global InstGR) Clause.
+      instance Ty (global InstGR) Clause.
   }
 }
\ No newline at end of file
diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v
index 75b48030b..e3e847afc 100644
--- a/apps/tc/tests/test.v
+++ b/apps/tc/tests/test.v
@@ -17,7 +17,7 @@ Module test_link_eta_generation.
   Class d (T : Type) (T : Type -> Type -> Type -> Type).
   Elpi Accumulate TC.Solver lp:{{
     :after "0" 
-    tc.compile.instance.compile-conclusion _ (app [H|_]) _ _ _ Premises _ :-
+    tc.compile.instance.compile-conclusion _ (app [H|_]) _ _ Premises _ :-
       H = {{test_link_eta_generation.c}}, !,
       std.assert! (Premises = [do [tc.link.eta _ _] | _]) "[TC] Wrong number of eta links",
       coq.say "Good padding from here",
@@ -25,7 +25,7 @@ Module test_link_eta_generation.
   }}.
   Elpi Query TC.Solver lp:{{
     ToCompile = {{forall (T : Type -> Type -> Type -> Type), (forall (a: Type), d a T) -> c T}},
-    not (tc.compile.instance ToCompile _ _).
+    pi x\ not (tc.compile.instance ToCompile x _).
   }}.
 End test_link_eta_generation.
 
diff --git a/apps/tc/tests/test_HO.v b/apps/tc/tests/test_HO.v
index ac52081a7..408b92332 100644
--- a/apps/tc/tests/test_HO.v
+++ b/apps/tc/tests/test_HO.v
@@ -200,7 +200,7 @@ Module HO_PF1.
     Proof.
       eexists; intros.
       Elpi Bound Steps 30000.
-      Set Typeclasses Debug.
+      (* Set Typeclasses Debug. *)
       apply _.
       Unshelve.
       auto.
@@ -321,7 +321,7 @@ Module F.
 
   Goal forall (T : Type -> Type) (H : forall x, T x), C1 T H -> D.
     intros.
-    Set Typeclasses Debug.
+    (* Set Typeclasses Debug. *)
     Set Debug "tactic-unification".
     Elpi TC Solver Override TC.Solver None.
     Fail apply _. (* Here coq's unfication algorithm fails: 
diff --git a/apps/tc/tests/test_backtrack_several_goals.v b/apps/tc/tests/test_backtrack_several_goals.v
index 06e5280f9..3981bcca2 100644
--- a/apps/tc/tests/test_backtrack_several_goals.v
+++ b/apps/tc/tests/test_backtrack_several_goals.v
@@ -12,7 +12,7 @@ Module M.
 
   Goal exists i, C i.
     eexists.
-    Set Typeclasses Debug.
+    (* Set Typeclasses Debug. *)
     (* Here backtracking is done *)
     apply m.
   Qed.
@@ -32,7 +32,7 @@ Module M1.
 
   Goal exists i, C i.
     eexists.
-    Set Typeclasses Debug.
+    (* Set Typeclasses Debug. *)
     apply m.
     (* 
       Note: in coq the following command fails since apply is a single entry
diff --git a/apps/tc/tests/test_scope.v b/apps/tc/tests/test_scope.v
index 5c4d00b35..e651d1325 100644
--- a/apps/tc/tests/test_scope.v
+++ b/apps/tc/tests/test_scope.v
@@ -10,7 +10,6 @@ Goal C Q ->  exists (T : Type -> Type), forall R, C R -> C (T).
   intros.
   Set Printing Existential Instances.
   assert (C Q) by auto.
-  Elpi Trace Browser.
   apply _.
   Show Proof.
 Abort.
diff --git a/apps/tc/tests/test_tc.v b/apps/tc/tests/test_tc.v
index 79556281a..b2b3280d0 100644
--- a/apps/tc/tests/test_tc.v
+++ b/apps/tc/tests/test_tc.v
@@ -1,7 +1,5 @@
 From elpi.apps Require Import tc.
 
-Elpi TC Solver Override TC.Solver All.
-
 Class a (N: nat).
 Instance b : a 3. Qed.
 Instance c : a 4. Qed.

From 9ed4495b9729ad0208addc0c64a7974d2038c5b2 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Thu, 22 Aug 2024 11:19:36 +0200
Subject: [PATCH 20/33] [TC] link small refactor

---
 apps/tc/elpi/link.elpi | 94 +++++++++++++++++-------------------------
 1 file changed, 37 insertions(+), 57 deletions(-)

diff --git a/apps/tc/elpi/link.elpi b/apps/tc/elpi/link.elpi
index 45f69a179..24e52f636 100644
--- a/apps/tc/elpi/link.elpi
+++ b/apps/tc/elpi/link.elpi
@@ -17,17 +17,17 @@ namespace tc {
     % [build-eta-llam-links.aux LHS Scope Ty Names PF NPF OldLinks NewVar NewLinks]
     :index(_ _ _ _ 3)
     pred build-eta-llam-links.aux i:term, i:list term, o:term, i:list term, i:list term, i:list term, i:list prop, o:term, o:list prop.
+    build-eta-llam-links.aux _   _ _       _     []  []  _  _  _ :-coq.error "MH?".
     build-eta-llam-links.aux LHS _ _       Names []  NPF OL HD [llam T (app [LHS | NPF]) | OL] :- !,
-      std.assert! (not (NPF = [])) "[TC] NPF List should not be empty",
-      prune T Names,
-      var T HD _. 
+      prune T Names, var T HD _. 
     build-eta-llam-links.aux LHS SC (prod _ Ty _)       _    [X] []  OL HD [eta LHS (fun `_` Ty (x\ V x)) | OL] :- !,
       prune V SC, var (V X) HD _.
     build-eta-llam-links.aux LHS SC (prod _ Ty Bo) Names [X|XS] NPF OL HD [eta LHS (fun `_` Ty (x\ LHS' x)) | L] :- !,
-    % TODO: unfold Ty if needed...
       std.append SC [X] SC',
       prune LHS' SC, build-eta-llam-links.aux (LHS' X) SC' (Bo X) Names XS NPF OL HD L.
     build-eta-llam-links.aux LHS SC Ty Names ([_|_] as PF) NPF OL HD L :-
+      % Ty is expected to be of (forall x, ...), however, this can be hidden 
+      % under a definition to be unfolded. The unify-eq below is to perform the unfold
       Ty' = prod _ _ _, coq.unify-eq Ty Ty' ok, !,
       build-eta-llam-links.aux LHS SC Ty' Names PF NPF OL HD L.
     
@@ -73,7 +73,7 @@ namespace tc {
       :index (_ _ 1)
       pred may-contract-to i:list term, i:term, i:term.
       may-contract-to _ N N :- name N, !.
-      may-contract-to L N V :- var V _ S, !,
+      may-contract-to L N (uvar _ S) :- !,
           std.forall [N|L] (x\ exists! S (may-contract-to [] x)).
       may-contract-to L N (app [N|A]) :-
         std.length A {std.length L},
@@ -81,14 +81,15 @@ namespace tc {
       may-contract-to L N (fun _ _ B) :-
         pi x\ may-contract-to [x|L] N (B x).
 
+      :index (_ 1)
       pred occurs-rigidly i:term, i:term.
       occurs-rigidly N N :- name N, !.
-      occurs-rigidly _ V :- var V, !, fail.
+      occurs-rigidly _ (uvar _) :- !, fail.
       occurs-rigidly N (app A) :- exists! A (occurs-rigidly N).
       occurs-rigidly N (fun _ _ B) :- pi x\ occurs-rigidly N (B x).
 
       pred maybe-eta-aux i:term, i:list term.
-      maybe-eta-aux V L :- var V _ S, std.forall L (std.mem! S).
+      maybe-eta-aux (uvar _ S) L :- std.forall L (std.mem! S).
       maybe-eta-aux (app [_|A]) L :-
         SplitLen is {std.length A} - {std.length L},
         split-at-not-fatal SplitLen A HD TL,
@@ -106,7 +107,7 @@ namespace tc {
       unify-left-right A A' :- A = A'.
 
       pred progress-eta-left i:term, o:term.
-      progress-eta-left A _ :- var A, !, fail.
+      progress-eta-left (uvar _) _ :- !, fail.
       progress-eta-left (fun _ _ A) (fun _ _ A).
       progress-eta-left A A' :- (name A; is-coq-term A), !, eta-expand A A'.
 
@@ -118,12 +119,6 @@ namespace tc {
       pred scope-check i:term, i:term.
       scope-check (uvar _ L) T :- prune A L, A = T, !.
 
-      pred collect-store o:list prop.
-      pred collect-store-aux i:list prop, o:list prop.
-
-      collect-store L :- collect-store-aux [] L.
-      collect-store-aux X L :- declare_constraint (collect-store-aux X L) [_].
-
       pred unify-eta i:term, i:term.
       % unify-eta A B :- coq.say "Unify-eta" "A"A"B"B, fail.
       unify-eta (uvar _ _ as A) B :- !, A = B, !.
@@ -132,33 +127,39 @@ namespace tc {
       unify-eta A B :- A = B.
 
       constraint eta solve-eta {
-        rule solve-eta \ (eta A B) <=> (unify-eta A B).
+        rule solve-eta \ (eta A B _) <=> (unify-eta A B).
         rule \ solve-eta.
         % If two eta links have same lhs they rhs should unify
-        rule (N1 : G1 ?- eta (uvar X L1) (fun _ T1 B1)) 
-            \ (N2 : G2 ?- eta (uvar X L2) (fun _ T2 B2)) 
-            | (pi x\ relocate L1 L2 (B2 x) (B2' x))  
+        rule (N1 : G1 ?- eta (uvar X L1) (fun _ T1 B1) _) 
+            \ (N2 : G2 ?- eta (uvar X L2) (fun _ T2 B2) _) 
+            | (pi x\ relocate L1 L2 (B2 x) (B2' x))
         <=> (N1 : G1 ?- B1 = B2').
       }
 
-      pred eta i:term, i:term.
-      eta _ B :- var B, coq.error "[TC] link.eta error, flexible rhs".
-      eta A (fun _ _ B as T) :- not (var A), not (var B), !, unify-left-right A T. 
-      eta A B :- progress-eta-right B B', !, A = B'. 
-      eta A B :- progress-eta-left A A', !, A' = B.
-      eta A B :- scope-check A B, get-vars B Vars, declare_constraint (eta A B) [_,A|Vars].
+      :index (0 1)
+      pred eta i:term, i:term, i:list term.
+      eta _ uvar _ :- coq.error "[TC] link.eta error, flexible rhs".
+      eta A (fun _ _ B as T) _ :- not (var A), not (var B), !, unify-left-right A T.
+      eta A B _ :- progress-eta-right B B', !, A = B'. 
+      eta A B _ :- progress-eta-left A A', !, A' = B.
+      eta (uvar _ as A) B Vars :- 
+        scope-check A B, std.filter Vars (x\ var x) Vars', 
+        declare_constraint (eta A B Vars') [_,A|Vars'].
     }
 
     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     % LLAM LINK                                                                %
     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     namespace llam {
+      % A llam link is suspended on its lhs and the head of its rhs
+      % Note: to avoid not pf elpi variable, the coq term `app[A, x, t]` where
+      % A is a uvar, x a name and t a term, is represented with the llam rhs:
+      % app[A' x, t] instead of (A' x t).
       pred llam i:term, i:term.
       llam A (uvar _ S as T) :- distinct_names S, !, A = T.
-      llam A (app [H|L] as T) :- var A, var H, !, get-vars T Vars, 
-        declare_constraint (llam A (app [H|L])) [_,A|Vars].
-      llam (fun _ _ _ as F) (app [H | TL]) :- 
-        var H _ Scope, !, 
+      llam (uvar _ as A) (app [(uvar HD _)|_] as T) :- !, 
+        declare_constraint (llam A T) [_,A,HD].
+      llam (fun _ _ _ as F) (app [(uvar _ Scope as H) | TL]) :- !, 
           std.drop-last 1 TL TL', 
           H = fun _ _Ty (x\ Bo'),  % TODO give a valid _Ty: should be: (Ty of dropped -> Ty of F)
           prune H' Scope,
@@ -177,6 +178,9 @@ namespace tc {
       }
     }
 
+    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+    % CS LINK                                                                  %
+    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     namespace cs {
       pred reduce-cs i:term, i:term, i:term, i:constant.
       reduce-cs V (app [ProjT, T]) Record Proj :-
@@ -216,36 +220,12 @@ namespace tc {
       }
     }
 
-    namespace cs {
-      pred cs i:term, i:term.
-      % TODO: suspend link on vars in T
-      cs V T :- var V, !, get-vars T Vars, declare_constraint (cs V T) [_, V | Vars].
-      cs T1 T2 :- coq.unify-eq T1 T2 ok.
-
-      % pred unify-rebinding-names i:list prop, i:list prop, i:term, i:term.
-      % unify-rebinding-names [] T1 [] T2 (unify-eq T1V T2) :- !, copy T1 T1V.
-      % unify-rebinding-names [N|NS] T1 [V|VS] T2 C :- !, copy N V => unify-rebinding-names NS T1 VS T2 C.
-      % unify-rebinding-names [] T1 VS T2 C :- !, unify-rebinding-names [] {coq.subst-prod VS T1} [] T2 C. % FIXME: reduction
-      % unify-rebinding-names [_|NS] (prod _ _ F) [] T2 C :- !,                      % FIXME: reduction
-      %   assert! (pi x\ F x = F1) "restriction bug", unify-rebinding-names NS F1 [] T2 C.
-
-      pred unify-under-ctx i:list term, i:list term, i:term, i:term, i:term, i:term.
-      unify-under-ctx [] [] A B V1 V2 :- copy A A', copy V1 V1', !, coq.unify-eq A' B ok, !, V1' = V2.
-      unify-under-ctx [X|XS] [Y|YS] A B V1 V2:- (copy X Y :- !) => unify-under-ctx XS YS A B V1 V2.
-
-      % TODO: there could be two same variables suspended on non unifyable
-      % terms, this should be detected and raise a failure.
-      % An example of this is in test/canonical_struct.v
-      constraint cache def decl coq.unify-eq ?- solve-cs cs {
-        rule solve-cs \ (Ctx ?- cs A B) <=> (Ctx => coq.unify-eq A B ok).
-        rule (Ctx1 ?- cs (uvar A L1 as X) T1) \ (Ctx2 ?- cs (uvar A L2 as Y) T2) <=>
-          (Ctx2 => unify-under-ctx L1 L2 T1 T2 X Y).
-        rule \ solve-cs.
-      }
-    }
-
+    % The last argument contain the list of vars on which the link is
+    % suspended. In order to avoid a call to get-vars if the link is to be 
+    % re-suspended, we explicetely pass this list once when the link is 
+    % created
     pred eta i:term, i:term.
-    eta A B :- eta.eta A B.
+    eta A B :- !, get-vars B V, eta.eta A B [A|V].
 
     pred solve-eta.
     solve-eta :- declare_constraint solve-eta [_].

From 26e439d1ce1f8bcaa358a77726993968b301385a Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Mon, 2 Sep 2024 11:14:17 +0200
Subject: [PATCH 21/33] [TC] clean link code + unification with cs links only
 after a call to tc.compile.

---
 apps/tc/elpi/link.elpi                       | 27 ++++++++++----------
 apps/tc/tests/importOrder/sameOrderCommand.v |  2 ++
 apps/tc/theories/add_commands.v              |  5 ++--
 apps/tc/theories/tc.v                        |  2 +-
 4 files changed, 20 insertions(+), 16 deletions(-)

diff --git a/apps/tc/elpi/link.elpi b/apps/tc/elpi/link.elpi
index 24e52f636..a1dc97138 100644
--- a/apps/tc/elpi/link.elpi
+++ b/apps/tc/elpi/link.elpi
@@ -67,8 +67,7 @@ namespace tc {
     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     namespace eta {
       pred eta-expand i:term, o:term.  
-      eta-expand T1 (fun _ _ B) :- (name T1; is-coq-term T1), !, pi x\ coq.mk-app T1 [x] (B x). 
-      eta-expand T1 (fun _ _ R) :- pi x\ name (R x) T1 [x].
+      eta-expand T1 (fun _ _ B) :- pi x\ coq.mk-app T1 [x] (B x). 
 
       :index (_ _ 1)
       pred may-contract-to i:list term, i:term, i:term.
@@ -107,14 +106,12 @@ namespace tc {
       unify-left-right A A' :- A = A'.
 
       pred progress-eta-left i:term, o:term.
-      progress-eta-left (uvar _) _ :- !, fail.
-      progress-eta-left (fun _ _ A) (fun _ _ A).
-      progress-eta-left A A' :- (name A; is-coq-term A), !, eta-expand A A'.
+      progress-eta-left (fun _ _ _ as A) B :- !, A = B.
+      progress-eta-left A B :- eta-expand A A', !, A' = B.
 
-      pred progress-eta-right i:term, o:term.
-      progress-eta-right (fun _ _ B as T) T :- pi x\ var (B x), !, fail.
-      progress-eta-right A A' :- coq.reduction.eta-contract A A', not (A = A'), !.
-      progress-eta-right A A :- not (maybe-eta A), !.
+      pred progress-eta-right? i:term, o:term.
+      progress-eta-right? A A' :- coq.reduction.eta-contract A A', not (A = A'), !.
+      progress-eta-right? A A :- not (maybe-eta A), !.
 
       pred scope-check i:term, i:term.
       scope-check (uvar _ L) T :- prune A L, A = T, !.
@@ -140,8 +137,8 @@ namespace tc {
       pred eta i:term, i:term, i:list term.
       eta _ uvar _ :- coq.error "[TC] link.eta error, flexible rhs".
       eta A (fun _ _ B as T) _ :- not (var A), not (var B), !, unify-left-right A T.
-      eta A B _ :- progress-eta-right B B', !, A = B'. 
-      eta A B _ :- progress-eta-left A A', !, A' = B.
+      eta A (fun _ _ B as T) _ :- not (var (B _)), progress-eta-right? T T', !, A = T'. 
+      eta A B                _ :- not (var A), !, progress-eta-left A B.
       eta (uvar _ as A) B Vars :- 
         scope-check A B, std.filter Vars (x\ var x) Vars', 
         declare_constraint (eta A B Vars') [_,A|Vars'].
@@ -199,10 +196,14 @@ namespace tc {
         tc.coercion-unify HD, !, 
         get-vars T Vars, declare_constraint (cs V T) [_, V | Vars].
 
-      cs (uvar _ as V) (app [HD | _] as T) :- 
+      cs (uvar _ as V) (app [HD | TL] as T) :- 
         if (HD = global (const Proj), tc.proj->record Proj Record)
           (reduce-cs V T Record Proj)
-          (coq.unify-eq V T ok), !.
+          % Note: Below we cannot unify V and T since T may contain
+          %       deep projections which must be considered as problematic terms
+          %       To avoid the problem, we compile all subterms in TL, the probl
+          %       subterms are replaced with variables put into links
+          (tc.compile.goal (app TL) (app TL') Links, do Links, V = app [HD|TL']), !.
       cs T1 T2 :- not (T2 = app _), !, coq.unify-eq T1 T2 ok.
 
       pred unify-under-ctx i:list term, i:list term, i:term, i:term, i:term, i:term.
diff --git a/apps/tc/tests/importOrder/sameOrderCommand.v b/apps/tc/tests/importOrder/sameOrderCommand.v
index 41d7d6a09..9c412908e 100644
--- a/apps/tc/tests/importOrder/sameOrderCommand.v
+++ b/apps/tc/tests/importOrder/sameOrderCommand.v
@@ -5,6 +5,7 @@ From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
 From elpi.apps.tc.elpi Extra Dependency "tc_same_order.elpi" as tc_same_order.
 From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
+From elpi.apps.tc.elpi Extra Dependency "compile_goal.elpi" as compile_goal.
 
 Set Warnings "+elpi".
 Elpi Command SameOrderImport.
@@ -14,6 +15,7 @@ Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
 Elpi Accumulate File unif.
 Elpi Accumulate File link.
+Elpi Accumulate File compile_goal.
 Elpi Accumulate File tc_same_order.
 
 
diff --git a/apps/tc/theories/add_commands.v b/apps/tc/theories/add_commands.v
index 939334e52..5e171d40c 100644
--- a/apps/tc/theories/add_commands.v
+++ b/apps/tc/theories/add_commands.v
@@ -6,6 +6,7 @@ From elpi.apps.tc Require Import db.
 From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc.elpi Extra Dependency "compile_instance.elpi" as compile_instance.
 From elpi.apps.tc.elpi Extra Dependency "compiler.elpi" as compiler.
+From elpi.apps.tc.elpi Extra Dependency "compile_goal.elpi" as compile_goal.
 From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
 From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes.
 From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
@@ -20,7 +21,7 @@ Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base tc_aux.
 Elpi Accumulate File unif modes link.
-Elpi Accumulate File compile_instance compiler.
+Elpi Accumulate File compile_instance compiler compile_goal.
 Elpi Accumulate lp:{{  
   main L :- 
     args->str-list L L1,
@@ -33,7 +34,7 @@ Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base tc_aux.
 Elpi Accumulate File unif modes link.
-Elpi Accumulate File compile_instance compiler.
+Elpi Accumulate File compile_instance compiler compile_goal.
 Elpi Accumulate File parser_addInstances.
 Elpi Accumulate lp:{{
   main Arguments :- 
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index 0e911cd0f..1c632a54c 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -76,7 +76,7 @@ Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base tc_aux.
 Elpi Accumulate File unif modes link.
-Elpi Accumulate File compile_instance compiler.
+Elpi Accumulate File compile_instance compiler compile_goal.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
 

From 44c2565b023081b650840f9a155638e40ac62945 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 3 Sep 2024 11:34:10 +0200
Subject: [PATCH 22/33] add _opam to .gitignore

---
 .gitignore | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.gitignore b/.gitignore
index 1a1d6e358..44b205805 100644
--- a/.gitignore
+++ b/.gitignore
@@ -57,5 +57,7 @@ rocq-elpi-tests.opam
 rocq-elpi-tests.install
 rocq-elpi.install
 coq-elpi.install
+_opam
+
 
 theories-stdlib/dune

From dc2c9156fefbfca2702e88b3fd3cd9cb9b2bb739 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 3 Sep 2024 11:35:17 +0200
Subject: [PATCH 23/33] [TC] clearn-term on pi-decl in decompile-term-aux

---
 apps/tc/elpi/compile_instance.elpi | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/apps/tc/elpi/compile_instance.elpi b/apps/tc/elpi/compile_instance.elpi
index 186561538..faf002871 100644
--- a/apps/tc/elpi/compile_instance.elpi
+++ b/apps/tc/elpi/compile_instance.elpi
@@ -1,6 +1,16 @@
 namespace tc {
   shorten tc.{r-ar, range-arity}.
 
+  % TODO: also replace (sort (typ X)) and (pglobal _ X) with holes in the place of X
+  pred clean-term i:term, o:term.
+  clean-term A B :-
+    (pi t s r \ copy (tc.maybe-eta-tm  t s) r :- !, copy t r, !) =>
+    (pi t s r \ copy (tc.canonical-projection t s _) r :- !, copy t r, !) =>
+    (pi t s r \ copy (tc.prod-range t s) r :- !, copy t r, !) =>
+    (pi t s r \ copy (tc.maybe-llam-tm t s) r :- !, copy t r, !) =>
+    (pi t s r \ copy (tc.coercion t s) r :- !, copy t r, !) =>
+      std.assert!  (copy A B) "[TC] clean-term error".
+
   namespace precomp {
 
     namespace instance {
@@ -245,13 +255,13 @@ namespace tc {
 
         decompile-term-aux (fun Name Ty Bo) (pr XS L) (fun Name Ty' Bo') (pr XS2 L3) :- !,
           (pi x\ is-name x => decompile-term-aux (Bo x) (pr XS []) (Bo' x) (pr XS1 (L1x x))),
-          close-prop-no-prune-pi-decl L1x Ty L1,
+          close-prop-no-prune-pi-decl L1x {clean-term Ty} L1,
           decompile-term-aux Ty (pr XS1 L) Ty' (pr XS2 L2),
           std.append L1 L2 L3.
 
         decompile-term-aux (prod Name Ty Bo) (pr XS L) (prod Name Ty' Bo') (pr XS2 L3) :- !,
           (pi x\ is-name x => decompile-term-aux (Bo x) (pr XS []) (Bo' x) (pr XS1 (L1x x))),
-          close-prop-no-prune-pi-decl L1x Ty L1,
+          close-prop-no-prune-pi-decl L1x {clean-term Ty} L1,
           decompile-term-aux Ty (pr XS1 L) Ty' (pr XS2 L2),
           std.append L1 L2 L3.
 
@@ -278,16 +288,6 @@ namespace tc {
 
       }
 
-      % TODO: also replace (sort (typ X)) and (pglobal _ X) with holes in the place of X
-      pred clean-term i:term, o:term.
-      clean-term A B :-
-        (pi t s r \ copy (tc.maybe-eta-tm  t s) r :- !, copy t r, !) =>
-        (pi t s r \ copy (tc.canonical-projection t s _) r :- !, copy t r, !) =>
-        (pi t s r \ copy (tc.prod-range t s) r :- !, copy t r, !) =>
-        (pi t s r \ copy (tc.maybe-llam-tm t s) r :- !, copy t r, !) =>
-        (pi t s r \ copy (tc.coercion t s) r :- !, copy t r, !) =>
-          std.assert!  (copy A B) "[TC] clean-term error".
-
       pred main 
         i:nat,                % the number of problematic terms
         i:term,               % the type of the instance

From a491a71cc86db4e1ad13e2b27b054fee415f86bc Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Thu, 19 Sep 2024 16:05:46 +0200
Subject: [PATCH 24/33] [TC] dummy clauses are local to sections

This aims to solve the compilation error produced by the compilation of

```
Module foo.
  Class B (i : nat).

  Section s.
    (* Class with coercion depending on section parameters *)
    Context (A : Type).
    Class C (i : A) : Set := {
      x (x : A) :: B 3
    }.
  End s.
End foo.
```
---
 apps/tc/theories/tc.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index 1c632a54c..16080ad11 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -88,10 +88,11 @@ Elpi Accumulate lp:{{
       Class Bird := IsAnimal :> Animal.
     ```
     The instance IsAnimal of type Bird -> Animal, is compiled before the
-    predicate for Bird; hence, Bird is not recognize as a premise of IsAnimal.
+    predicate for Bird; hence, it is not possible to add the premise
+    tc-Bird for the IsAnimal instance...
     This problem is due to the order in which the registers for Instance and
     Class creation are run.
-    The solution is to do the following two jobs when a class C is created:
+    The solution is to do the following jobs when a class C is created:
       1: for every projection P of C, if P is a coercion, the wrongly 
         compiled instance is replaced with a `dummy` clause.
       2: the predicate for the class is created

From 9891625eee82beae4fa92f523bd72d047801c4af Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 25 Sep 2024 16:12:59 +0200
Subject: [PATCH 25/33] [TC] add comment

---
 apps/tc/elpi/compile_goal.elpi | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/apps/tc/elpi/compile_goal.elpi b/apps/tc/elpi/compile_goal.elpi
index 340c76f60..0abf16517 100644
--- a/apps/tc/elpi/compile_goal.elpi
+++ b/apps/tc/elpi/compile_goal.elpi
@@ -111,6 +111,9 @@ namespace tc {
       compile-full Goal Goal' Links :- compile-full-aux Goal [] Goal' Links.
     }
 
+    % [goal T T' L] takes a term T and returns a new term T' where problematic
+    % subterms (see this: https://dl.acm.org/doi/10.1145/3678232.3678233)
+    % are replaced with fresh variables. The list of links is L
     pred goal i:term, o:term, o:list prop.
     :name "compile-goal"
     goal Goal Goal' Links :- 

From 79c7251da56ec048a30e92d8148ac559b17a5b99 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 25 Sep 2024 16:13:34 +0200
Subject: [PATCH 26/33] [TC] move time-is-active and coercion-unify in db.v

---
 apps/tc/elpi/tc_aux.elpi | 4 ----
 apps/tc/theories/db.v    | 5 +++++
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
index aaee96ffb..f165afb14 100644
--- a/apps/tc/elpi/tc_aux.elpi
+++ b/apps/tc/elpi/tc_aux.elpi
@@ -181,7 +181,6 @@ namespace tc {
   section-var->decl L :-
     section-var->decl.aux {coq.env.section} L.
 
-  pred time-is-active i:(list string -> prop).
   :name "time-is-active"
   time-is-active _ :- coq.option.get ["Time", "TC", "Bench"] (coq.option.bool tt), !.
   time-is-active Opt :- tc.is-option-active Opt. 
@@ -228,9 +227,6 @@ namespace tc {
     int ->
     term.
 
-  :index (5)
-  pred coercion-unify i:term.
-
   type coercion
     term ->
     list term ->
diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
index 451abe763..1c7591db1 100644
--- a/apps/tc/theories/db.v
+++ b/apps/tc/theories/db.v
@@ -105,6 +105,11 @@ Elpi Db tc.db lp:{{
 
     % relates a projection to the its record
     pred proj->record i:constant, o:term.
+    
+    :index (5)
+    pred coercion-unify i:term.
+
+    pred time-is-active i:(list string -> prop).
   }
 }}.
 From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.

From 79ded6ce65289e9733fee69ebd3e1043b0db6a2d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 2 Oct 2024 13:05:50 +0200
Subject: [PATCH 27/33] cleanup

---
 _opam | 1 -
 1 file changed, 1 deletion(-)
 delete mode 120000 _opam

diff --git a/_opam b/_opam
deleted file mode 120000
index 343b677d2..000000000
--- a/_opam
+++ /dev/null
@@ -1 +0,0 @@
-/home/dfissore/Documents/github/COQ_ELPI_DEV/_opam
\ No newline at end of file

From 17eb2bc53a314e69910a11599a0073059ab0c562 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 2 Oct 2024 13:14:13 +0200
Subject: [PATCH 28/33] cleanup

---
 apps/tc/theories/db.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
index 1c7591db1..c9f0be4ee 100644
--- a/apps/tc/theories/db.v
+++ b/apps/tc/theories/db.v
@@ -103,7 +103,8 @@ Elpi Db tc.db lp:{{
     pred link.llam i:term, i:term.
 
 
-    % relates a projection to the its record
+    % relates a projection to the its record type fully applied to fresh
+    % variables, eg, rules have the shape: (pi P1 ... PN\ proj->record {{p}} {{r P1 .. PN}})
     pred proj->record i:constant, o:term.
     
     :index (5)

From 37fd717df9f98cdaf635620b000bca49a1d45488 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 2 Oct 2024 13:16:47 +0200
Subject: [PATCH 29/33] cleanup

---
 apps/tc/theories/db.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
index c9f0be4ee..c48898c82 100644
--- a/apps/tc/theories/db.v
+++ b/apps/tc/theories/db.v
@@ -105,11 +105,15 @@ Elpi Db tc.db lp:{{
 
     % relates a projection to the its record type fully applied to fresh
     % variables, eg, rules have the shape: (pi P1 ... PN\ proj->record {{p}} {{r P1 .. PN}})
+    % MANUALLY INSERTED by TC.AddRecordFields
     pred proj->record i:constant, o:term.
     
+    % tells if a term is a coercion
+    % MANUALLY INSERTED by Elpi Accumulate
     :index (5)
     pred coercion-unify i:term.
 
+    % Used to print bench infos
     pred time-is-active i:(list string -> prop).
   }
 }}.

From 5e191201cb05ae019f51e17ac3c62f8a231f9ade Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 2 Oct 2024 13:28:50 +0200
Subject: [PATCH 30/33] ci

---
 .github/workflows/doc.yml     | 4 +++-
 .github/workflows/release.yml | 4 +++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/doc.yml b/.github/workflows/doc.yml
index e80a9b629..6c54098d2 100644
--- a/.github/workflows/doc.yml
+++ b/.github/workflows/doc.yml
@@ -9,7 +9,9 @@ on:
     branches: [ master ]
   pull_request:
     branches: [ master ]
-
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
 jobs:
   build:
     name: Build doc
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index c212889c0..52d84898f 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -22,7 +22,9 @@ on:
         options:
         - released
         - extra-dev
-
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
 env:
   OPAM_SUITE: ${{ inputs.suite }}
 

From cd6da58a47e53bd9a7cbfd03e68c45ff2140dea0 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 8 Apr 2025 22:29:42 +0200
Subject: [PATCH 31/33] [TC] fix

---
 apps/tc/elpi/compile_goal.elpi               |  2 +-
 apps/tc/elpi/compile_instance.elpi           |  8 ++---
 apps/tc/elpi/link.elpi                       | 26 +++++++--------
 apps/tc/src/rocq_elpi_tc_register.ml         |  2 +-
 apps/tc/tests/importOrder/sameOrderCommand.v |  2 +-
 apps/tc/tests/test.v                         | 35 ++++++++------------
 apps/tc/theories/add_commands.v              |  6 ++--
 apps/tc/theories/db.v                        |  3 +-
 apps/tc/theories/tc.v                        |  1 +
 builtin-doc/coq-builtin.elpi                 | 19 +++++------
 10 files changed, 48 insertions(+), 56 deletions(-)

diff --git a/apps/tc/elpi/compile_goal.elpi b/apps/tc/elpi/compile_goal.elpi
index 0abf16517..0053d84c0 100644
--- a/apps/tc/elpi/compile_goal.elpi
+++ b/apps/tc/elpi/compile_goal.elpi
@@ -66,7 +66,7 @@ namespace tc {
       compile-full-aux (app [global (const C) | _] as G) L G' [tc.link.cs G' G | L] :- coq.env.projection? C _, !.
       
       % Link for primitive projection
-      compile-full-aux (app [primitive (proj P _) | _] as G) L G' [tc.link.cs G' G | L] :- coq.env.primitive-projection? P _, !.
+      compile-full-aux (app [primitive (proj P _) | _] as G) L G' [tc.link.cs G' G | L] :- coq.env.primitive-projection? P _ _, !.
 
       % Link for eta-redex
       compile-full-aux (fun Name_ Ty Bo as G) L G' [tc.link.eta G' (fun `_` Ty' Bo') | L'] :- maybe-eta G, !,
diff --git a/apps/tc/elpi/compile_instance.elpi b/apps/tc/elpi/compile_instance.elpi
index faf002871..c9bae6e49 100644
--- a/apps/tc/elpi/compile_instance.elpi
+++ b/apps/tc/elpi/compile_instance.elpi
@@ -101,7 +101,7 @@ namespace tc {
         (pi x\ get-range-arity-aux T (B x) R1),
         min-max-nat R R1 R2.
       get-range-arity-aux _ (global _) @max-min :- !.
-      get-range-arity-aux _ (uvar _) @max-min :- !.
+      get-range-arity-aux _ uvar @max-min :- !.
       get-range-arity-aux _ (sort _) @max-min :- !.
       get-range-arity-aux _ (pglobal _ _) @max-min :- !.
       get-range-arity-aux A B _ :- coq.error "Count maximal arity failure" A B.
@@ -118,7 +118,7 @@ namespace tc {
       precompile-aux _ (primitive _ as C) A C A :- !.
       precompile-aux _ T A (tc.coercion T Scope) (s A) :- coq.safe-dest-app T HD _, tc.coercion-unify HD, !, free-var Scope.
       precompile-aux _ (app [global (const C) | _] as T) A (tc.canonical-projection T Scope N) (s A) :- coq.env.projection? C N, !, free-var Scope.
-      precompile-aux _ (app [primitive (proj P _) | _] as T) A (tc.canonical-projection T Scope 0) (s A) :- coq.env.primitive-projection? P _, !, free-var Scope.
+      precompile-aux _ (app [primitive (proj P _) | _] as T) A (tc.canonical-projection T Scope 0) (s A) :- coq.env.primitive-projection? P _ _, !, free-var Scope.
 
       % Detect maybe-eta term
       % TODO: should I precompile also the type of the fun and put it in the output term
@@ -387,8 +387,8 @@ namespace tc {
         i:list prop,
         o:prop.
       compile-premise L L2 P PTy ProofHd IsPositive ITy ProofArgsR PremR Clause :-
-        (pi a b c\ tc.get-TC-of-inst-type (tc.prod-range a c) b :- tc.get-TC-of-inst-type a b) => 
-          tc.get-TC-of-inst-type PTy TC, !,
+        ((pi a b c\ tc.get-TC-of-inst-type (tc.prod-range a c) b :- tc.get-TC-of-inst-type a b) => 
+          tc.get-TC-of-inst-type PTy TC), !,
         compile-ty L L1 P {neg IsPositive} PTy [] [] NewPrem,
         deterministic-prem TC NewPrem NewPrem',
         compile-ty L1 L2 ProofHd IsPositive ITy ProofArgsR [NewPrem' | PremR] Clause.
diff --git a/apps/tc/elpi/link.elpi b/apps/tc/elpi/link.elpi
index a1dc97138..a041dd868 100644
--- a/apps/tc/elpi/link.elpi
+++ b/apps/tc/elpi/link.elpi
@@ -83,7 +83,7 @@ namespace tc {
       :index (_ 1)
       pred occurs-rigidly i:term, i:term.
       occurs-rigidly N N :- name N, !.
-      occurs-rigidly _ (uvar _) :- !, fail.
+      occurs-rigidly _ uvar :- !, fail.
       occurs-rigidly N (app A) :- exists! A (occurs-rigidly N).
       occurs-rigidly N (fun _ _ B) :- pi x\ occurs-rigidly N (B x).
 
@@ -127,10 +127,10 @@ namespace tc {
         rule solve-eta \ (eta A B _) <=> (unify-eta A B).
         rule \ solve-eta.
         % If two eta links have same lhs they rhs should unify
-        rule (N1 : G1 ?- eta (uvar X L1) (fun _ T1 B1) _) 
-            \ (N2 : G2 ?- eta (uvar X L2) (fun _ T2 B2) _) 
+        rule (N1 :> G1 ?- eta (uvar X L1) (fun _ T1 B1) _) 
+            \ (N2 :> G2 ?- eta (uvar X L2) (fun _ T2 B2) _) 
             | (pi x\ relocate L1 L2 (B2 x) (B2' x))
-        <=> (N1 : G1 ?- B1 = B2').
+        <=> (N1 :> G1 ?- B1 = B2').
       }
 
       :index (0 1)
@@ -139,7 +139,7 @@ namespace tc {
       eta A (fun _ _ B as T) _ :- not (var A), not (var B), !, unify-left-right A T.
       eta A (fun _ _ B as T) _ :- not (var (B _)), progress-eta-right? T T', !, A = T'. 
       eta A B                _ :- not (var A), !, progress-eta-left A B.
-      eta (uvar _ as A) B Vars :- 
+      eta (uvar as A) B Vars :- 
         scope-check A B, std.filter Vars (x\ var x) Vars', 
         declare_constraint (eta A B Vars') [_,A|Vars'].
     }
@@ -154,7 +154,7 @@ namespace tc {
       % app[A' x, t] instead of (A' x t).
       pred llam i:term, i:term.
       llam A (uvar _ S as T) :- distinct_names S, !, A = T.
-      llam (uvar _ as A) (app [(uvar HD _)|_] as T) :- !, 
+      llam (uvar as A) (app [(uvar as HD)|_] as T) :- !, 
         declare_constraint (llam A T) [_,A,HD].
       llam (fun _ _ _ as F) (app [(uvar _ Scope as H) | TL]) :- !, 
           std.drop-last 1 TL TL', 
@@ -168,10 +168,10 @@ namespace tc {
         rule solve-llam \ (llam A B) <=> (A = B).
         rule \ solve-llam.
         % If two llam links have same lhs they rhs should unify
-        rule (N1 : G1 ?- llam (uvar X L1) T1) 
-            \ (N2 : G2 ?- llam (uvar X L2) T2) 
+        rule (N1 :> G1 ?- llam (uvar X L1) T1) 
+            \ (N2 :> G2 ?- llam (uvar X L2) T2) 
             | (pi x\ relocate L1 L2 T2 T2')  
-        <=> (N1 : G1 ?- T1 = T2'). % TODO: instead of elpi unif, should use heuristics...
+        <=> (N1 :> G1 ?- T1 = T2'). % TODO: instead of elpi unif, should use heuristics...
       }
     }
 
@@ -184,19 +184,19 @@ namespace tc {
         coq.unify-eq T Record Err, Err = ok,
         Q = [coq.redflags.const Proj],
         coq.redflags.add coq.redflags.nored [coq.redflags.delta, coq.redflags.beta, coq.redflags.match | Q] RF,
-        @redflags! RF => coq.reduction.lazy.whd (app [ProjT, Record]) V',
+        (@redflags! RF => coq.reduction.lazy.whd (app [ProjT, Record]) V'),
         not (V' = match _ _ _), !,
         cs V V'.
       reduce-cs V T _ _ :- V = T.
 
       pred cs i:term, i:term.
       cs T1 T2 :- not (var T1), !, coq.unify-eq T1 T2 ok.
-      cs (uvar _ as V) (app [_, Arg] as T) :- not (ground_term Arg), !, get-vars T Vars, declare_constraint (cs V T) [_, V | Vars].
-      cs (uvar _ as V) (app [HD, _Arg] as T) :- 
+      cs (uvar as V) (app [_, Arg] as T) :- not (ground_term Arg), !, get-vars T Vars, declare_constraint (cs V T) [_, V | Vars].
+      cs (uvar as V) (app [HD, _Arg] as T) :- 
         tc.coercion-unify HD, !, 
         get-vars T Vars, declare_constraint (cs V T) [_, V | Vars].
 
-      cs (uvar _ as V) (app [HD | TL] as T) :- 
+      cs (uvar as V) (app [HD | TL] as T) :- 
         if (HD = global (const Proj), tc.proj->record Proj Record)
           (reduce-cs V T Record Proj)
           % Note: Below we cannot unify V and T since T may contain
diff --git a/apps/tc/src/rocq_elpi_tc_register.ml b/apps/tc/src/rocq_elpi_tc_register.ml
index dd3800111..22f94ab62 100644
--- a/apps/tc/src/rocq_elpi_tc_register.ml
+++ b/apps/tc/src/rocq_elpi_tc_register.ml
@@ -23,7 +23,7 @@ let gref2elpi_term (gref: GlobRef.t) : Cmd.raw =
 let observer_class (x : Typeclasses.typeclass) : Rocq_elpi_arg_HOAS.Cmd.raw list = 
   [Cmd.String "new_class"; gref2elpi_term x.cl_impl]
 
-let observer_coercion add (x : Typeclasses.typeclass) : Coq_elpi_arg_HOAS.Cmd.raw list = 
+let observer_coercion add (x : Typeclasses.typeclass) : Rocq_elpi_arg_HOAS.Cmd.raw list = 
   let name2str x = Cmd.String (Names.Name.print x |> Pp.string_of_ppcmds) in
   let proj = x.cl_projs |> List.map (fun (x: Typeclasses.class_method) -> x.meth_name) in
   let mode = if add then "add_coercions" else "remove_coercions" in
diff --git a/apps/tc/tests/importOrder/sameOrderCommand.v b/apps/tc/tests/importOrder/sameOrderCommand.v
index 9c412908e..07e994c4e 100644
--- a/apps/tc/tests/importOrder/sameOrderCommand.v
+++ b/apps/tc/tests/importOrder/sameOrderCommand.v
@@ -14,8 +14,8 @@ Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
 Elpi Accumulate File unif.
-Elpi Accumulate File link.
 Elpi Accumulate File compile_goal.
+Elpi Accumulate File link.
 Elpi Accumulate File tc_same_order.
 
 
diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v
index e3e847afc..37cf891db 100644
--- a/apps/tc/tests/test.v
+++ b/apps/tc/tests/test.v
@@ -119,7 +119,7 @@ Module HO_swap.
   Axiom (f : Type -> Type -> Type).
   Elpi Query TC.Solver lp:{{
     tc.link.eta.maybe-eta (fun `x` _ c0 \ fun `y` _ c1 \ A2 c1 c0),
-    tc.link.eta.maybe-eta (fun `x` _ c0 \ fun `y` _ c1 \ A2 (A c1) c0),
+    tc.link.eta.maybe-eta (fun `x` _ c0 \ fun `y` _ c1 \ A2 (A_ c1) c0),
     tc.link.eta.maybe-eta {{fun x y => f x y}}.
   }}.
 
@@ -129,7 +129,7 @@ Module HO_swap.
   Elpi Query TC.Solver lp:{{
     @pi-decl `x` {{Type -> Type}} f\ tc.precomp.instance.is-uvar f => 
       sigma T\
-        tc.precomp.instance {{c1 (fun x y => lp:f y x)}} T N _ _,
+        tc.precomp.instance {{c1 (fun x y => lp:f y x)}} T N_ _ _,
         std.assert! (T = app[{{c1}}, tc.maybe-eta-tm _ _]) "[TC] invalid precomp".
   }}.
 
@@ -204,7 +204,7 @@ Module HO_7.
   Qed.
 End HO_7.
 
-Module HO_81.
+(* Module HO_81.
   Class c1 (T : Type).
   Instance i1 F : c1 F. Qed.
 
@@ -223,11 +223,9 @@ Module HO_81.
     (* Failure is good, since here we simply check that the number of 
       uvar-pair built by tc.precomp is zero. This is because the type
       of ?X is Type (i.e. it has `arity` zero) *)
-    apply _.
-    Unshelve.
-    apply nat.
-  Qed.
-End HO_81.
+    Fail apply _.
+  Abort.
+End HO_81. *)
 
 Module HO_8.
   Class c1 (T : Type -> Type -> Type).
@@ -249,7 +247,7 @@ Module HO_9.
 
   Elpi Query TC.Solver lp:{{
     pi F\ sigma T\ decl F `x` {{Type -> Type}} ==> tc.precomp.instance.is-uvar F ==> 
-      tc.precomp.instance {{c1 (fun x => f (lp:F x) (lp:F x))}} T N _ _,
+      tc.precomp.instance {{c1 (fun x => f (lp:F x) (lp:F x))}} T _N _ _,
       std.assert! (T = app [{{c1}}, tc.maybe-eta-tm _ _]) "Invalid precompilation".
   }}.
 
@@ -293,13 +291,6 @@ Module HO_12.
   Instance i : Unit (forall x, x) := {}.
   Set Printing Existential Instances.
 
-  Elpi Accumulate TC.Solver lp:{{
-    % TODO: this rule should be removed if https://github.com/LPCIC/elpi/issues/256
-    % is solved
-    tc-elpi.apps.tc.tests.test.HO_12.tc-Unit {{forall (x:Prop), lp:(X x)}} {{i}} :-
-      X = (x\x).
-  }}.
-
   Goal forall (y: Prop), exists (F: Prop -> Prop), Unit (forall x, F x).
     intros.
     eexists ?[F].
@@ -328,7 +319,7 @@ Module HO_13.
   Qed.
 
   Elpi Query TC.Solver lp:{{
-    std.spy-do![Goal = {{Unit (forall x y, lp:(F x y))}},
+    std.spy-do![Goal = {{Unit (forall x y, lp:(F_ x y))}},
     tc.build-query-from-goal Goal Proof Q PP,
     do PP, Q,
     std.assert! (Proof = {{i f j}}) "Error"].
@@ -396,7 +387,7 @@ Module Llam_1.
     @pi-decl `x` {{Type -> Type}} f\ tc.precomp.instance.is-uvar f => 
       @pi-decl `x` {{Type -> Type}} g\ tc.precomp.instance.is-uvar g => 
         sigma T\
-          tc.precomp.instance {{A (fun x => lp:f (lp:g x))}} T N _ _,
+          tc.precomp.instance {{A (fun x => lp:f (lp:g x))}} T _N _ _,
           std.assert! (T = app[{{A}}, tc.maybe-eta-tm (fun _ _ (x\ tc.maybe-llam-tm _ _)) _]) "[TC] invalid precomp".
   }}.
 
@@ -512,12 +503,12 @@ Module CoqUvar.
   Class c1 (i:Type -> Type -> Type).
 
   Elpi Query TC.Solver lp:{{
-    tc.precomp.instance {{c1 (fun x y => lp:F y x)}} T _ _ _,
+    tc.precomp.instance {{c1 (fun x y => lp:F_ y x)}} T _ _ _,
     coq.say T,
     Expected = app[{{c1}}, tc.maybe-eta-tm (fun _ _ Inn) []],
     std.assert! (T = Expected) "[TC] invalid precompile1",
     pi x\ sigma ExpectedInn\
-      ExpectedInn = tc.maybe-eta-tm (A x) [x],
+      ExpectedInn = tc.maybe-eta-tm (A_ x) [x],
       std.assert! ((Inn x) = ExpectedInn) "[TC] invalid precompile2".
   }}.
 
@@ -603,10 +594,10 @@ Module CoqUvar4.
   Class c1 (T : Type -> Type -> Type).
   
   Elpi Query TC.Solver lp:{{
-    tc.precomp.instance {{c1 (fun x y => lp:X (lp:A x y) y)}} C _ _ _,
+    tc.precomp.instance {{c1 (fun x y => lp:X (lp:A_ x y) y)}} C _ _ _,
     Expected = app [{{c1}}, tc.maybe-eta-tm (fun _ _ Body1) _],
     Body1 = (x\ tc.maybe-eta-tm (fun _ _ (Body2 x)) [x]),
-    Body2 = (x\y\ app [X, (Y x y), y]),
+    Body2 = (x\y\ app [X, (Y_ x y), y]),
     std.assert! (C = Expected) "[TC] invalid compilation".
   }}.
 
diff --git a/apps/tc/theories/add_commands.v b/apps/tc/theories/add_commands.v
index 5e171d40c..1a24efa3a 100644
--- a/apps/tc/theories/add_commands.v
+++ b/apps/tc/theories/add_commands.v
@@ -10,6 +10,7 @@ From elpi.apps.tc.elpi Extra Dependency "compile_goal.elpi" as compile_goal.
 From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
 From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes.
 From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
+From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.
 From elpi.apps.tc.elpi Extra Dependency "parser_addInstances.elpi" as parser_addInstances.
 From elpi.apps.tc.elpi Extra Dependency "solver.elpi" as solver.
 From elpi.apps.tc.elpi Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
@@ -20,8 +21,8 @@ Elpi Command TC.AddAllInstances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base tc_aux.
-Elpi Accumulate File unif modes link.
 Elpi Accumulate File compile_instance compiler compile_goal.
+Elpi Accumulate File unif modes link.
 Elpi Accumulate lp:{{  
   main L :- 
     args->str-list L L1,
@@ -33,8 +34,8 @@ Elpi Command TC.AddInstances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base tc_aux.
-Elpi Accumulate File unif modes link.
 Elpi Accumulate File compile_instance compiler compile_goal.
+Elpi Accumulate File unif modes link.
 Elpi Accumulate File parser_addInstances.
 Elpi Accumulate lp:{{
   main Arguments :- 
@@ -155,7 +156,6 @@ Elpi Accumulate  lp:{{
   main [trm T1, trm T2, int N] :- !, tc.add_tc.records_unif T1 T2 N.
   main L :- coq.error L.
 }}.
-Elpi Typecheck.
 
 Elpi Export TC.AddAllClasses.
 Elpi Export TC.AddRecordFields.
diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
index c48898c82..9ab27f703 100644
--- a/apps/tc/theories/db.v
+++ b/apps/tc/theories/db.v
@@ -101,7 +101,8 @@ Elpi Db tc.db lp:{{
     pred ho-link o:term, i:term, o:A.
     pred link.eta i:term, i:term.
     pred link.llam i:term, i:term.
-
+    pred link.cs i:term, i:term.
+    pred link.build-eta-llam-links i:term, i:list prop, o:term, o:list prop.
 
     % relates a projection to the its record type fully applied to fresh
     % variables, eg, rules have the shape: (pi P1 ... PN\ proj->record {{p}} {{r P1 .. PN}})
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index 16080ad11..b54d82cae 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -9,6 +9,7 @@ From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes.
 From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
 
 From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
+From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.
 From elpi.apps.tc.elpi Extra Dependency "compiler.elpi" as compiler.
 From elpi.apps.tc.elpi Extra Dependency "compile_goal.elpi" as compile_goal.
 From elpi.apps.tc.elpi Extra Dependency "compile_instance.elpi" as compile_instance.
diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi
index 7f1af9eb9..0900983f4 100644
--- a/builtin-doc/coq-builtin.elpi
+++ b/builtin-doc/coq-builtin.elpi
@@ -934,9 +934,11 @@ external pred coq.env.projection? i:constant, o:int.
 external pred coq.env.primitive-projections i:inductive, 
                                             o:list (option (pair projection int)).
 
-% [coq.env.primitive-projection? Projection Compatibility constant] relates
-% a projection to its compatibility constant.
-external pred coq.env.primitive-projection? i:projection, o:constant.
+% [coq.env.primitive-projection? Projection Compatibility constant Index]
+% Relates a primitive projection to its compatibility constant. Index is set
+% to the constructor argument extracted by the projection (starting from 0).
+external pred coq.env.primitive-projection? o:projection, o:constant, 
+                                            o:int.
 
 % -- Sorts (and their universe level, if applicable) ----------------
 
@@ -1178,6 +1180,10 @@ external pred coq.CS.db o:list cs-instance.
 % or canonical Value, or both
 external pred coq.CS.db-for i:gref, i:cs-pattern, o:list cs-instance.
 
+% [coq.CS.canonical-projection? Projection] Tells if the projection can be
+% used for CS inference.
+external pred coq.CS.canonical-projection? i:constant.
+
 % [coq.TC.declare-class GR] Declare GR as a type class
 external pred coq.TC.declare-class i:gref.
 
@@ -1372,13 +1378,6 @@ external pred coq.arguments.simplification i:gref,
 external pred coq.arguments.set-simplification i:gref, 
                                                i:simplification_strategy.
 
-% [coq.arguments.reset-simplification GR] resets the behavior of the
-% simplification tactics.
-% Also resets the ! and / modifiers for the Arguments command.
-% Supported attributes:
-% - @global! (default: false)
-external pred coq.arguments.reset-simplification i:gref.
-
 % [coq.locate-abbreviation Name Abbreviation] locates an abbreviation.  It's
 % a fatal error if Name cannot be located.
 external pred coq.locate-abbreviation i:id, o:abbreviation.

From 363765fdcadb94c268467da53d8c28486522df13 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 8 Apr 2025 22:43:01 +0200
Subject: [PATCH 32/33] [TC] base file loaded once

---
 apps/tc/tests/importOrder/sameOrderCommand.v |  2 --
 apps/tc/theories/add_commands.v              | 17 ++++++++---------
 apps/tc/theories/tc.v                        | 11 +++++------
 3 files changed, 13 insertions(+), 17 deletions(-)

diff --git a/apps/tc/tests/importOrder/sameOrderCommand.v b/apps/tc/tests/importOrder/sameOrderCommand.v
index 07e994c4e..631b08620 100644
--- a/apps/tc/tests/importOrder/sameOrderCommand.v
+++ b/apps/tc/tests/importOrder/sameOrderCommand.v
@@ -1,6 +1,5 @@
 From elpi.apps Require Export tc.
 
-From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.
 From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
 From elpi.apps.tc.elpi Extra Dependency "tc_same_order.elpi" as tc_same_order.
@@ -11,7 +10,6 @@ Set Warnings "+elpi".
 Elpi Command SameOrderImport.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
 Elpi Accumulate File unif.
 Elpi Accumulate File compile_goal.
diff --git a/apps/tc/theories/add_commands.v b/apps/tc/theories/add_commands.v
index 1a24efa3a..91df74131 100644
--- a/apps/tc/theories/add_commands.v
+++ b/apps/tc/theories/add_commands.v
@@ -10,7 +10,6 @@ From elpi.apps.tc.elpi Extra Dependency "compile_goal.elpi" as compile_goal.
 From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
 From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes.
 From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
-From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.
 From elpi.apps.tc.elpi Extra Dependency "parser_addInstances.elpi" as parser_addInstances.
 From elpi.apps.tc.elpi Extra Dependency "solver.elpi" as solver.
 From elpi.apps.tc.elpi Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
@@ -20,7 +19,7 @@ Set Warnings "+elpi".
 Elpi Command TC.AddAllInstances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate File compile_instance compiler compile_goal.
 Elpi Accumulate File unif modes link.
 Elpi Accumulate lp:{{  
@@ -33,7 +32,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.AddInstances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate File compile_instance compiler compile_goal.
 Elpi Accumulate File unif modes link.
 Elpi Accumulate File parser_addInstances.
@@ -46,7 +45,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.AddAllClasses.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux modes.
+Elpi Accumulate File tc_aux modes.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   % Ignore is the list of classes we do not want to add
@@ -59,7 +58,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.AddClasses.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux modes.
+Elpi Accumulate File tc_aux modes.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   pred tc.add-all-classes i:list argument , i:tc.search-mode.
@@ -77,7 +76,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.AddHook.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate lp:{{
   pred tc.addHook i:grafting, i:string. 
   tc.addHook Grafting NewName :- 
@@ -107,7 +106,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.Declare.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux modes.
+Elpi Accumulate File tc_aux modes.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   main _ :- coq.warning "TC.Declare" {tc.warning-name} 
@@ -121,7 +120,7 @@ with implicit arguments (those implicits will be neglected)", fail.
 Elpi Command TC.Pending_mode.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux modes.
+Elpi Accumulate File tc_aux modes.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   main M :- 
@@ -134,7 +133,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.AddRecordFields.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate  lp:{{
   pred tc.add_tc.records_unif.aux i:int, i:term, i:list term, i:constant, o:prop.
   tc.add_tc.records_unif.aux 0 T Args ProjConstant P :- !,
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index b54d82cae..350331dd6 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -9,7 +9,6 @@ From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes.
 From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
 
 From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
-From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.
 From elpi.apps.tc.elpi Extra Dependency "compiler.elpi" as compiler.
 From elpi.apps.tc.elpi Extra Dependency "compile_goal.elpi" as compile_goal.
 From elpi.apps.tc.elpi Extra Dependency "compile_instance.elpi" as compile_instance.
@@ -50,7 +49,7 @@ Elpi Accumulate lp:{{
 Elpi Tactic TC.Solver.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate File unif modes link.
 Elpi Accumulate File compile_instance compile_goal.
 Elpi Accumulate File solver.
@@ -75,7 +74,7 @@ Elpi Query lp:{{
 Elpi Command TC.Compiler.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate File unif modes link.
 Elpi Accumulate File compile_instance compiler compile_goal.
 Elpi Accumulate File create_tc_predicate.
@@ -123,7 +122,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.Set_deterministic.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate lp:{{
   main [str ClassStr] :- 
     coq.locate ClassStr ClassGR, 
@@ -137,7 +136,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.Get_class_info.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate lp:{{
   main [str ClassStr] :- 
     coq.locate ClassStr ClassGR, 
@@ -157,7 +156,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.Unfold.
 Elpi Accumulate Db tc_options.db.
 Elpi Accumulate Db tc.db.
-Elpi Accumulate File base tc_aux.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate lp:{{
   pred tc.add-unfold i:gref.
   tc.add-unfold (const C) :-

From 733f3a21dc0c1d3e8195811af266f0cf04db53f3 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 9 Apr 2025 09:04:33 +0200
Subject: [PATCH 33/33] [TC] add some doc to predicates

---
 apps/tc/elpi/compile_instance.elpi | 43 +++++++++++++++++-------------
 1 file changed, 24 insertions(+), 19 deletions(-)

diff --git a/apps/tc/elpi/compile_instance.elpi b/apps/tc/elpi/compile_instance.elpi
index c9bae6e49..1d4448345 100644
--- a/apps/tc/elpi/compile_instance.elpi
+++ b/apps/tc/elpi/compile_instance.elpi
@@ -110,7 +110,12 @@ namespace tc {
       get-range-arity _ Ty _ (r-ar z N) :- tc.get-TC-of-inst-type Ty _, !, count-prod Ty N.
       get-range-arity B _ T N :- !, get-range-arity-aux B T N. 
 
-      pred precompile-aux i:positivity, i:term, i:nat, o:term, o:nat.
+      pred precompile-aux 
+        i:positivity, % Positive or negaive position of the term being pre-compiled
+        i:term,       % Term being explored
+        i:nat,        % Number of pi to quantified accumulated
+        o:term,       % Precompiled term: problematic sub-terms are tagged with custom constructors
+        o:nat.        % Final number of pi to quantify
       precompile-aux _ X A Y A :- name X, !, X = Y, !. % avoid loading "precompile-aux x A x A" at binders
       precompile-aux _ (global _ as C) A C A :- !.
       precompile-aux _ (pglobal _ _ as C) A C A :- !.
@@ -376,16 +381,16 @@ namespace tc {
       deterministic-prem _ P P.
 
       pred compile-premise
-        i:list term,
-        o:list term,
-        i:term,
-        i:term,
-        i:term,
-        i:bool,
-        i:term,
-        i:list term,
-        i:list prop,
-        o:prop.
+        i:list term,       % List of pi-quantified vars to consume
+        o:list term,       % List of remaining pi-quantified variables
+        i:term,            % (Local) Name of the proof of the premise
+        i:term,            % Type of the local premise being consumed by compile-ty
+        i:term,            % Name of the instance being compiled (global {{:gref InstName}})
+        i:bool,            % Positive or negative position of the term
+        i:term,            % Type of InstName to compile
+        i:list term,       % List of the name of all local proofs
+        i:list prop,       % List of premises to add to the fianal clause
+        o:prop.            % The final clause
       compile-premise L L2 P PTy ProofHd IsPositive ITy ProofArgsR PremR Clause :-
         ((pi a b c\ tc.get-TC-of-inst-type (tc.prod-range a c) b :- tc.get-TC-of-inst-type a b) => 
           tc.get-TC-of-inst-type PTy TC), !,
@@ -396,14 +401,14 @@ namespace tc {
         compile-ty L L1 ProofHd IsPositive ITy ProofArgsR PremR Clause. 
 
       pred compile-ty 
-        i:list term,
-        i:list term,
-        i:term,
-        i:bool,
-        i:term,
-        i:list term,
-        i:list prop,
-        o:prop.
+        i:list term,       % List of pi-quantified vars to consume
+        o:list term,       % List of remaining pi-quantified variables
+        i:term,            % Name of the instance being compiled (global {{:gref InstName}}) 
+        i:bool,            % Positive or negative position of the term
+        i:term,            % Type of InstName to compile
+        i:list term,       % List of the name of all local proofs
+        i:list prop,       % List of premises to add to the fianal clause
+        o:prop.            % The final clause
       compile-ty L L1 ProofHd IsPositive (tc.prod-range (prod N Ty Bo) Arity) ProofArgsR PremR Clause :- !,
         std.do![
           if (IsPositive = tt)