unif_rule is unable to bypass the priority of injectivity unification vs rewriting reduction? BUG?

[1337777]

unif_rule is unable to bypass the priority of injectivity unification vs rewriting reduction? BUG?

MINIMAL EXAMPLE (more minimal is possible, without the type dependency)
And why it shows up / matters is contained in the pull request Deducteam/lambdapi-stdlib#25

constant symbol cat : TYPE;
constant symbol func : Π (A B : cat), TYPE;
constant symbol Id_func : Π [A : cat], func A A;

constant symbol catd: Π (X : cat), TYPE;
constant symbol Terminal_catd : Π (A : cat), catd A;

injective symbol Context_cat : Π [X : cat], catd X → cat;
rule Context_cat (Terminal_catd $A) ↪ $A;

// THE PROBLEM: unif_rule UNABLE TO BYPASS THE PRIORITY OF INJECTIVITY UNIFICATION VS REWRITING REDUCTION
// Context_cat $A ≡? (Context_cat (Terminal_catd (Context_cat $A)))

// In the case that injectivity unification happens first:
// $A ≡? (Terminal_catd (Context_cat $A))  which then fails
// In the case that rewriting reduction happens first:
// Context_cat $A ≡? (Context_cat $A)  which then succeds

// LAMBDAPI BUG? this unification rule doesnt work... it seems that it is not really registered
// so finding an alternative explicit coercion rule_Context_cat_Terminal_catd_func
unif_rule Context_cat $B ≡ (Context_cat (Terminal_catd (Context_cat $X))) ↪ [ $B ≡ $X];

symbol rule_Context_cat_Terminal_catd_func [X: cat] (A: catd X) 
: func (Context_cat (Terminal_catd (Context_cat A))) (Context_cat A)
≔ begin assume X A; 
// KO THIS FAILS WITHOUT simplify 
try refine Id_func;
// OK
simplify; refine Id_func; 
end;

// OK
// λ X A, Id_func
compute λ [X: cat] (A: catd X), rule_Context_cat_Terminal_catd_func A;

// KO
// [Terminal_catd (Context_cat A)] and [A] are not unifiable.
// Those two types are not unifiable.
assert [X: cat] (A: catd X) ⊢ rule_Context_cat_Terminal_catd_func A ≡ Id_func ;

[fblanqui]

Hi. The short answer to your first question is: yes, unification rules are applied after decomposition and weak-head normalization. Is it a bug? Not really after the doc: "Given a unification problem t ≡ u, if the engine cannot find a solution, it will try to match the pattern t ≡ u against the defined rules (modulo commutativity of ≡) and rewrite the problem to the right-hand side of the matched rule."

You can follow what the unification algorithm is doing by writing:

debug +u;

You also print implicit arguments by writing:

flag "print_implicits" on;

a) When doing refine Id_func before simplify, you get the following unification problem:

@Context_cat X A ≡ @Context_cat (@Context_cat X A) (Terminal_catd (@Context_cat X A))

You declare Context_cat : Π [X : cat], catd X → cat as injective. This means that Context_cat X x ≡ Context_cat Y y should imply X ≡ Y and x ≡ y, where ≡ is the definitional equality. Are you sure of that? (Lambdapi does not check injectivity.) Partial injectivity is a feature request (#270).

As Context_cat is declared as injective, the above unification is decomposed into:

1. X ≡ @Context_cat X A
2. A ≡ Terminal_catd (@Context_cat X A)

but 2) is not solvable (A is a variable and Terminal_catd is a constant), so the algorithm stops.

b) When doing simplify before refine, you get as goal:

func (@Context_cat X A) (@Context_cat X A)

and refine works as expected.

c) The last assert fails for the same reason as in a)

d) adding the unification rule that you propose doesn't change anything because you never get a potentially solvable unification problem matching the LHS of your unification rule because, indeed, decomposition is done before the application of unification rules.

[1337777]

Here is a preliminary heuristic argument. Let's try to find a counterexample to "Context_cat X x ≡ Context_cat Y y should imply X ≡ Y and x ≡ y".
Most likely such a counterexample would happen via the rule @Context_cat (@Context_cat Y y) (Terminal_catd (@Context_cat Y y)) ↪ (Context_cat Y y); where X is (@Context_cat Y y) and x is (Terminal_catd (@Context_cat Y y)).
Then is it still possible that (@Context_cat Y y) ≡ Y ? Yes when y ≡ Terminal_catd Y
THEREAFTER (i.e. assuming y has been instantiated as y ≡ Terminal_catd Y), is it still possible that (Terminal_catd (@Context_cat Y y)) ≡ y ? Yes both sides compute to Terminal_catd Y

So there would be no obvious counterexamples if the symbol is declared "SEQUENTIALLY INJECTIVE": "Context_cat X x ≡ Context_cat Y y should IMPLY FIRSTLY X ≡ Y and THEREAFTER x ≡ y".

Anyway below is further data for a ?BUG? REPORT which shows none of these questions are clear.

// BUG REPORT:
The implementation of these 3 declarations yield not the same identical effect, regardless of what they mean in theory.

// (1) injective keyword
injective symbol Context_cat : Π [X : cat], catd X → cat;

// (2) injectivity via unification
symbol Context_cat : Π [X : cat], catd X → cat;
unif_rule @Context_cat $X $B ≡ @Context_cat $Y $A ↪ [ $X ≡ $Y; $B ≡ $A];

// (3) "partial" injectivity via unification
symbol Context_cat : Π [X : cat], catd X → cat;
unif_rule @Context_cat $X $B ≡ @Context_cat $X $A ↪ [ $B ≡ $A];

Replacing (1) by (2) instead provokes a problem 1000 lines later down the realistic-application file. The problem is that the lambdapi compiler is slow stuck at a type query to get the type of a term; but this term is somewhat unrelated to the symbol Context_cat where the injectivity problem is arises. And because it is just a type query and not a rule command, this slow stuck would have nothing to do confluences checks (which usually involves unrelated terms)?. Here is the stuck query:

// Fatal error: out of memory
// Aborted (core dumped)
// real    5m23.652s
// user    3m52.808s
// sys     1m29.492s
// type λ [A B I : cat] [R : mod A B] (BB : catd B) [x : func I A] [y : func I B] (r : hom x R y)
//  [J] [x' : func J I] [J0] [F : func J0 A] [x'x] (x'x_ : hom x'x (Unit_mod F x) x')
//  [J'] [x'' : func J' J] [J0'] [F' : func J0' J0] [x''x'] (x''x'_ : hom x''x' (Unit_mod F' x'x) x''),
//   (((Comma_con_homd BB (x'x_ '∘  ((F)_'∘> r)) x''x'_) ) '∘d  (( _ ) _'∘>d  (Comma_con_homd BB r x'x_)))
//        = ((Comma_con_homd BB r (x''x'_ '∘  ((F')_'∘> x'x_ ))) );

Replacing (1) by (3) instead provokes an error: "unable to prove type preservation" later in 2 rules, which are fixed by giving more explicitly the first argument of the symbol Context_cat where injectivity arises. But then the same above problem of slow stuck happens at the same type query 1000 lines later.