pglobals: add hole for universe level

apps/tc/elpi/ho_compile.elpi

@@ -380,6 +380,12 @@ namespace tc {
         fold-map Ty L Ty' L2,
         std.append L2 L1 L3.
 
+      pred unif-univ-constraint term, term.
+      unif-univ-constraint T1 T2 :- declare_constraint (tc.link.univ-poly T1 T2) [_].
+
+      decompile-problematic-term (pglobal P Q as T) L (pglobal P Q' as T') L' :-
+        L' = [unif-univ-constraint T T' | L].
+
       func compile term, list prop -> term, 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', !) =>

apps/tc/elpi/ho_link.elpi

@@ -133,6 +133,13 @@ namespace tc {
       }
     }
 
+    namespace univ-poly {
+      constraint solve-poly univ-poly {
+        rule solve-poly \ (univ-poly A B) <=> (coq.unify-eq T1 T2 ok).
+        rule \ solve-poly.
+      }
+    }
+
     namespace unif-eq {
       func unif-eq term, term.
       unif-eq T1 (uvar as T2) :- !, declare_constraint (unif-eq T1 T2) [_,T2].
@@ -154,5 +161,11 @@ namespace tc {
 
     func solve-llam.
     solve-llam :- declare_constraint solve-llam [_].
+
+    func univ-poly term, term ->.
+
+    func solve-poly.
+    solve-poly :- declare_constraint solve-poly [_].
+
   }
 }

apps/tc/elpi/solver.elpi

@@ -30,10 +30,12 @@ namespace tc {
   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), !,
+    if-true print-post-process-goal (coq.say "[TC] the post-process goal list is" PostProcess), !,
     tc.time-it tc.oTC-time-instance-search (
       do PostProcess, Q,
-      tc.link.solve-eta, % Trigger eta links
-      tc.link.solve-llam % Trigger llam links
+      tc.link.solve-eta,  % Trigger eta links
+      tc.link.solve-llam, % Trigger llam links
+      tc.link.solve-poly % Trigger univ links
     ) "instance search".
 
   pred solve-aux i:goal, o:list sealed-goal.
@@ -65,5 +67,6 @@ namespace tc {
   pred print-goal.          % Print the goal in HOAS
   pred print-goal-pp.       % Print the goal with coq pp
   pred print-compiled-goal.
+  pred print-post-process-goal.
 
 }

apps/tc/tests-stdlib/polyUniv.v

@@ -0,0 +1,24 @@
+From elpi.apps Require Import tc.
+Elpi TC Solver Override TC.Solver All.
+
+Polymorphic Definition pidentity {A : Type} (a : A) := a.
+Polymorphic Definition selfpid := pidentity (@pidentity).
+
+Class C A (H : A -> A) (Z : forall A, A -> A)  := {}.
+
+Set Printing Universes.
+About C.
+
+Elpi Accumulate TC.Solver lp:{{
+  tc.print-goal.
+  tc.print-compiled-goal.
+  tc.print-post-process-goal.
+}}.
+
+Instance I A : C A pidentity selfpid. Qed.
+
+Goal forall A, C A pidentity selfpid.
+  intro H.
+  apply _.
+Qed.
+