higher-order rewrite rule with implicit arguments under the binder: uninformative cryptic error message? BUG?

[1337777]

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;

[fblanqui]

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.