Rule typing failure

[gabrielhdt]

The following signature

Set : Type.
injective El : (Set -> Type).

N : Type.
s : N -> N.
z : N.

T : (N -> Type).
cons! : (n : N -> (Set -> ((T n) -> (T (s n))))).
nil! : (T z).
code : (n : N -> ((T n) -> Set)).
nil : (El (code z nil!)).
cons : (n : N -> (X : Set -> (Q : (T n) -> ((El X) -> ((El (code n Q)) -> (El (code (s n) (cons! n X Q)))))))).
def car! : (n : N -> ((T n) -> Set)).
[v0, v1, v2_X, v3] car! v0 (cons! v1 v2_X v3) --> v2_X.
def cdr! : (n : N -> (tt : (T (s n)) -> ((El (code (s n) tt)) -> (T n)))).
[v0, v1, v2, v3_Q, v4] cdr! v0 (cons! v1 v2 v3_Q) v4 --> v3_Q.

def car : (n : N -> (tt : (T n) -> ((El (code n tt)) -> (El (car! n tt))))).
[v0, v1, v2, v3, v4, v5_x, v6] car v0 v1 (cons v2 v3 v4 v5_x v6) --> v5_x.

fails to type check with Error 207 [...] [line:21 column:31] Feature not implemented using dk check with the master branch.

[GuillaumeGen]

The issue is that when trying to to type check your last rule, Dedukti infers the substitution

[Rule] Inferred typing substitution:
  v1[5](0 args) -> Issue.cons! v2[4] v3[3] v4[2]
  v0[6](0 args) -> Issue.s v2[4]

(obtained with -d u)

The issue here is that when one tries to apply this substitution in the type, then the type of v1 : T (s v2) and this is impossible to express since v2 occurs after v1.

A very simple, but not very satisfactory, fix, is to states that v0 is a successor

[v0, v1, v2, v3, v4, v5_x, v6] car (s v2) v1 (cons _ v3 v4 v5_x v6) --> v5_x.

Then the substitution inferred is

Inferred typing substitution:
  ?_1[4](0 args) -> v2[6]
  v1[5](0 args) -> Issue.dk.v.cons! v2[6] v3[3] v4[2]

and there is no circularity issue anymore with the types of the variables.
(But it requires to reduce to (weak) head normal form the first argument of car to apply the rule).

[GuillaumeGen]

Well, things are more subtle than that, because this file is accepted, whereas it happens exactly what I described in the previous comment.

Nat : Type.
0 : Nat.
s : Nat -> Nat.

A : Type.

Vec : Nat -> Type.
nil : Vec 0.
cons : (n : Nat) -> A -> Vec n -> Vec (s n).

def length : (n : Nat) -> Vec n -> Nat.
[] length _ nil --> 0.
[m, n, tl] length m (cons n _ tl) --> s (length n tl).

where the substitution inferred is

Inferred typing substitution:
  m[3](0 args) -> test.s n[2]

EDIT:
Well I was completely wrong about this example, the type of the second argument of length indeed depends of the first argument, but this is the case of no variable, hence applying this substitution does not lead to an invalid context.

[gabrielhdt]

How should m[3](0 args) be read?

[GuillaumeGen]

m[3](0 args) means that it is the variable with identifier "m", with de Bruijn index 3 (last to be declared variable has index 0, and then it increases) and is a pattern variable which does not take any argument (with Miller's pattern, under binders it happens to have pattern variable with arguments).

[GuillaumeGen]

I realize that my week-end messages only expressed a diagnosis without any action plan.
First, my opinionated version of the diagnosis is that refusing this file is quite legitimate, but the error message is really shitty.
I see 3 possible actions, depending of how much work one wants to invest in it:

1. One could simply replace the error message by something like "Applying the typing constraints lead to an invalid context". (15 minutes of work).
2. One could forget the part of the substitution leading to an invalid context and try to type-check the rhs only with this safe "sub-substitution" (a short afternoon of work).
3. I am quite rusty, but I have the feeling that applying the substitution inferred while type-checking the lhs to the context does not serve any purpose. If it is possible to have a theoretical justification for simply not modifying the context with this substitution, then one can completely drop it. (15 minutes of implementing, but some research to do before. It does not look very hard to me, but the devil hides in details, I am rusty and it does not look to be on anyone plate now, hence I will not try to estimate this).