[TC] premise not run if rigid solution

Author: FissoreD

apps/tc/elpi/tc_aux.elpi

@@ -111,23 +111,24 @@ namespace tc {
   get-mode ClassGR M :- tc.class ClassGR _ _ M, !.
   get-mode ClassGR _ :- coq.error "[TC]" ClassGR "is an unknown class".
 
-  pred make-tc.aux i:bool, i:prop, i:list prop, o:prop.
-  make-tc.aux _ Head [] Head.
-  make-tc.aux tt Head Body (Head :- Body).
-  make-tc.aux ff Head Body (Body => Head).
+  pred make-tc.aux i:bool, i:term, i:prop, i:list prop, o:prop.
+  make-tc.aux tt _ Head [] Head :- !.
+  make-tc.aux ff Sol Head [] P :- !, P = if (var Sol) Head true.
+  make-tc.aux tt _ Head Body (Head :- Body) :- !.
+  make-tc.aux ff Sol Head Body P :- !, P = if (var Sol) (Body => Head) true.
 
   pred make-tc i:term, i:term, i:list prop, i:bool, o:prop.
-  make-tc Ty Inst Body IsPositive Clause :-
-    coq.safe-dest-app Ty HD TL,
-    get-TC-of-inst-type HD ClassGR,
+  make-tc Goal Sol RuleBody IsPositive Rule :-
+    coq.safe-dest-app Goal Class Args,
+    get-TC-of-inst-type Class ClassGR,
     gref->pred-name ClassGR ClassStr,
-    std.append TL [Inst] Args, 
-    coq.elpi.predicate ClassStr Args Head,
-    make-tc.aux IsPositive Head Body Clause.
+    std.append Args [Sol] ArgsSol, 
+    coq.elpi.predicate ClassStr ArgsSol RuleHead,
+    make-tc.aux IsPositive Sol RuleHead RuleBody Rule.
 
-  pred unwrap-prio i:tc-priority, o:int.
-  unwrap-prio (tc-priority-given Prio) Prio.
-  unwrap-prio (tc-priority-computed Prio) Prio.
+    pred unwrap-prio i:tc-priority, o:int.
+    unwrap-prio (tc-priority-given Prio) Prio.
+    unwrap-prio (tc-priority-computed Prio) Prio.
 
   % returns the priority of an instance from the gref of an instance
   pred get-inst-prio i:gref, o:int.

apps/tc/tests/hyp_in_conl.v

@@ -0,0 +1,65 @@
+From elpi.apps Require Import tc.
+
+(* 
+  Here we want to test that if the solution of a premise is rigid
+  then the premise is not run
+*)
+
+Module M1.
+  Structure ofe := Ofe { ofe_car : Type; }.
+
+  Class D (I : ofe).
+
+  Class C (X : ofe) (I : D X).
+
+  Definition ofe_nat : ofe := Ofe nat.
+
+  Instance c : forall (H : D (Ofe nat)), C ofe_nat H := {}.
+
+  Goal forall (H : D (Ofe nat)), True -> exists H, C (ofe_nat) H.
+    intros.
+    notypeclasses refine (ex_intro _ _ _ ).
+    apply _.
+  Qed.
+End M1.
+
+Module M2.
+
+  Class A.
+  Class B (I : A).
+  Class C (A : A) (I : B A).
+
+  Instance c : forall (A : A) (B : B A), C A B := {}.
+
+  Goal forall (A : A) (B : B A), exists A B, C A B.
+    intros.
+    do 2 notypeclasses refine (ex_intro _ _ _ ).
+    apply _.
+  Qed.
+
+End M2.
+
+Module M3.
+
+  Class A.
+  Class B (I : A).
+  Class C (A : A) (I : B A).
+
+  Instance c : forall (A : A) (B : B A), C A B := {}.
+
+  Set Warnings "+elpi".
+
+  Elpi Accumulate TC.Solver lp:{{
+    :after "0"
+    tc-elpi.apps.tc.tests.hyp_in_conl.M3.tc-A _ :- !, coq.error "Should not check for tc-A".
+    tc-elpi.apps.tc.tests.hyp_in_conl.M3.tc-B _ _ :- !, coq.error "Should not check for tc-B".
+  }}.
+  Elpi Typecheck TC.Solver.
+
+  Section s.
+    Context (A : A) (B : B A).
+
+    Definition d : C A B := _.
+  End s.
+
+End M3.