Deducteam
higher-order rewrite rule with implicit arguments under the binder: uninformative cryptic error message? BUG?
higher-order rewrite rule with implicit arguments under the binder: uninformative cryptic error message? BUG?
MINIMAL EXAMPLE with the solution (could be non-obvious in real-world complex code). Then an alternative solution (optional), specific to the subject matter, in the style of Kosta Dosen.
constant symbol cat : TYPE;
constant symbol Terminal_cat : cat;
constant symbol func : Π (A B : cat), TYPE;
constant symbol Id_func : Π [A : cat], func A A;
symbol ∘> : Π [A B C: cat], func A B → func B C → func A C;
notation ∘> infix left 90; // ∘> is a reducible symbols with rules that compute it
constant symbol Set : TYPE;
injective symbol τ : Set → TYPE;
constant symbol set_cat : Set → cat;
constant symbol set_cat_intro_func : Π [I : Set], τ I → func Terminal_cat (set_cat I);
injective symbol set_cat_elim_func : Π [I : Set] [A : cat], (τ I → func Terminal_cat A ) → func (set_cat I) A;
// usual beta rule
//OK
rule set_cat_elim_func (set_cat_intro_func) ↪ Id_func;
// but the extensional form of above beta rule is often required, it now uses higher-order rewrite rule/unification:
// KO
// "Bug. Introduced symbol [$15227] cannot be removed. Please contact the developers."
rule set_cat_elim_func (λ i, set_cat_intro_func i) ↪ Id_func;
// PROBLEM: THE ERROR MESSAGE HERE IS NOT VERY INFORMATIVE ABOUT WHAT IS THE PROBLEM AND HOW TO SOLVE IT
// SOLUTION:
// OK
rule set_cat_elim_func (λ i, @set_cat_intro_func $I.[] i) ↪ Id_func;
// --------8<------OPTIONAL PART---------->8--------
// ALTERNATIVE SOLUTION:
// avoid higher-order rewrite rule unification and use Kosta Dosen techniques:
// in fact, putting aside the minimal example which demonstrates the "BUG"
// Here is the REAL INTENTION behind all of that:
// The REAL INTENTION MOTIVATION was to have this (too complex) rewrite rule
// which is second-order unifification and it has some inner-and-under-binder reducible symbols `∘>`
// So this assumes that the Lambdapi logical framework has such higher-order rewrite rules,
rule set_cat_elim_func (λ i, (@set_cat_intro_func $I.[] i) ∘> $G.[]) ↪ $G;
// but in case Lambdapi was not that powerful, there would still exists an alternative:
// KOSTA DOSEN ALTERNATIVE SOLUTION
injective symbol set_cat_intro_func_ALT : Π [I : Set] [A : cat], func (set_cat I) A → (τ I → func Terminal_cat A);
// naturality (accumulation), which says that morally : the new (set_cat_intro_func_ALT F i) is the former ((set_cat_intro_func i) ∘> $F).
rule (set_cat_intro_func_ALT $F $i) ∘> $G ↪ set_cat_intro_func_ALT ($F ∘> $G) $i;
//alternative beta rule, fist-order and no inner reducible symbols inside the rule
rule @set_cat_elim_func $I _ (λ i, @∘> $A.[] $B.[] $C.[] (@set_cat_intro_func $I.[] i) $G.[]) ↪ $G; //nasty: second-order unif & inner-and-under-binder reducible symbols
rule set_cat_elim_func (set_cat_intro_func_ALT $F) ↪ $F;
If you print implicit arguments (flag "print_implicits" on) and the rules of set_cat_elim_func (print set_cat_elim_func), you see that the first rule actually is:
rule @set_cat_elim_func $0 $1 (@set_cat_intro_func $2) ↪ @Id_func (set_cat $0);
When adding an abstraction, you can specify how each pattern variable that is below the abstraction depends on it. By default, a pattern depends on all abstracted variables. The user manual indicates: "The unnamed pattern variable _ is always the most general: if x and y are the only variables in scope, then _ is equivalent to $_.[x;y]." This means that the second rule is like:
rule @set_cat_elim_func $0 $1 (λ i, @set_cat_intro_func $2.[i] i) ↪ @Id_func (set_cat $0);
but the type of i then is τ $2.[i], which is problematic (a term t whose type contains t itself).
Indeed, the solution is to enforce $2 to not depend on i and explicitly write $2.[].
We should definitely improve the error message. The code currently contains the following comment: "A symbol may also come from a metavariable that appeared in the type of a metavariable that was replaced by a symbol. We do not have concrete examples of that happening yet." We now have one. Thank you.
Remark: using flag "eta_equality" on doesn't help (eta-conversion is only used when comparing an abstraction with some other term). Lambdapi implements no eta-reduction (or eta-expansion). This could be a feature request. With eta-reduction, the second rule would be useless though.
Comment: it is unusual to define an arrow type constructor as infix left.
The arrow/function type constructor is
constant symbol func : Π (A B : cat), TYPE;
the composition of elements/functions in this arrow type is
symbol ∘> : Π [A B C: cat], func A B → func B C → func A C;
with a rewrite rule
`rule $X ∘> ($G ∘> $H) ↪ ($X ∘> $G) ∘> $H;
so that (x ∘> f ) ∘> g means the usual textbook notation g ∘ (f ∘ x)
so the notation
notation ∘> infix left 90;
is clearly justified by the rewrite rule which associates to the left, which itself is justified by the intended operational meaning of composing/applying inputs to inner functions until the last outer function to get an output