From 05c9567e4c6f31f0858c705b67b1be77018621b5 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Thu, 19 Sep 2024 16:05:46 +0200 Subject: [PATCH] [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 22e734a90..998db8083 100644 --- a/apps/tc/theories/tc.v +++ b/apps/tc/theories/tc.v @@ -89,10 +89,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