Inversion fails in type inference

[fblanqui]

symbol N:TYPE;
symbol 0:N;
symbol Set:TYPE;
symbol nat:Set;
symbol arr:Set → Set → Set;
symbol El:Set → TYPE;
rule El(arr $x $y) ↪ El $x → El $y;
rule El nat ↪ N;
symbol I[a]:N → El a;
debug +u;
symbol f:N → N ≔ I 0;

Checking "/home/blanqui/src/lambdapi/tmp/inj.lp" ...
debug +u
[unif] solve El ?0 ≡ N → N
[unif] whnf
[unif] solve El ?0 ≡ N → N
[unif] try inverse El
[unif] failed
[unif] check unif_rules
[unif] found no unif_rule
[unif] move to unsolved
[unif] solve El ?0 ≡ N → N
[unif] whnf
[unif] solve El ?0 ≡ N → N
[unif] try inverse El
[unif] failed
[unif] check unif_rules
[unif] found no unif_rule
[unif] move to unsolved
[/home/blanqui/src/lambdapi/tmp/inj.lp:11:0-21]
Some metavariables could not be solved: a proof must be given
[/home/blanqui/src/lambdapi/tmp/inj.lp:11:21] The proof is not finished:
0. El ?0 ≡ N → N
1. El ?0 ≡ N → N
2. ?0: Set
3. ?0: Set

[NotBad4U]

If you set the symbol El injective it works:

symbol N:TYPE;
symbol 0:N;
symbol Set:TYPE;
symbol nat:Set;
symbol arr:Set → Set → Set;
injective symbol El:Set → TYPE;  //<----- add modifier
rule El(arr $x $y) ↪ El $x → El $y;
rule El nat ↪ N;
symbol I[a]:N → El a;
debug +u;
symbol f:N → N ≔ I 0;

[unif] solve El ?138 ≡ N → N
[unif] whnf
[unif] solve El ?138 ≡ N → N
[unif] try inverse El                         <----- does not fail anymore
[unif] add ?138 ≡ arr nat nat
[unif] solve ?138 ≡ arr nat nat
[unif] try instantiate
[unif] check typing
[unif] ?138 ≔ arr nat nat
[unif] solve El (arr nat nat) ≡ N → N
[unif] whnf
[unif] solve El nat → El nat ≡ N → N
[unif] decompose
[unif] add El nat ≡ N
[unif] add El nat ≡ N
[unif] solve El nat ≡ N
[unif] whnf
[unif] solve N ≡ N
[unif] equivalent terms
[unif] solve El nat ≡ N
[unif] whnf
[unif] solve N ≡ N
[unif] equivalent terms

I think we just forgot to set El injective during our test :).