[TC] mode ground with ground_term check + tc.link for coercions

Author: FissoreD

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)

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,

apps/tc/tests/test_pending_mode.v

@@ -36,7 +36,7 @@ Module ground1.
 
   Goal exists (x : Type), C (list x). 
     eexists.
-    apply _.
+    Fail apply _.
   Abort.
 End ground1.
 
@@ -47,7 +47,7 @@ Module ground2.
 
   Goal exists (x : Type), C (list x). 
     eexists. 
-    apply _.
+    Fail apply _.
   Abort.
 End ground2.
 
@@ -64,14 +64,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.