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.