Failure of coq.env.add-indt in the presence of non uniform parameters

[ecranceMERCE]

Here is an inductive type:

Inductive t (n : nat) : Type :=
  | K : t O -> t n.

Here is its parametricity translation built in Elpi:

inductive tR tt 
 (parameter n explicit (pglobal (indt «nat») «») c0 \
   parameter n' explicit (pglobal (indt «nat») «») c1 \
	parameter nR explicit (app [pglobal (indt «natR») «», c0, c1]) c2 \
     arity
      (prod `i` (app [pglobal (indt «t») «Test.78», c0]) c3 \
        prod `i'` (app [pglobal (indt «t») «Test.78», c1]) 
         c4 \ sort (typ «Test.78»))) c0 \
 [constructor KR 
   (parameter n explicit (pglobal (indt «nat») «») c1 \
     parameter n' explicit (pglobal (indt «nat») «») c2 \
      parameter nR explicit (app [pglobal (indt «natR») «», c1, c2]) c3 \
       arity
        (prod `_` 
          (app
            [pglobal (indt «t») «Test.78», 
             pglobal (indc «O») «»]) c4 \
          prod `_'` 
           (app
             [pglobal (indt «t») «Test.78», 
              pglobal (indc «O») «»]) c5 \
           prod `_R` 
            (app
              [c0, pglobal (indc «O») «», pglobal (indc «O») «», 
               pglobal (indc «OR») «», c4, c5]) c6 \
            app
             [c0, c1, c2, c3, 
              app [pglobal (indc «K») «Test.78», c1, c4], 
              app [pglobal (indc «K») «Test.78», c2, c5]]))]

Trying to add it to Coq through coq.env.add-indt fails with the following error:

3rd non uniform parameter, named nR, not found in constructor KR

Yet, I declared the corresponding inductive in Coq:

Inductive tR@{u} (n n' : nat) (nR : natR n n') : t@{u} n -> t@{u} n' -> Type :=
  | KR : forall (i i' : t O), tR O O OR i i' -> tR n n' nR (K n i) (K n' i').

and querying its declaration with coq.env.indt-decl gives exactly the same result that the one I wanted to add to Coq through Elpi. There is one universe per declaration which I all renamed to u to do a relevant diff on both versions, and only the naming changes as visible here:

6,7c6,7
<       (prod `i` (app [pglobal (indt «t») «u», c0]) c3 \
<         prod `i'` (app [pglobal (indt «t») «u», c1])
---
>       (prod `_` (app [pglobal (indt «t») «u», c0]) c3 \
>         prod `_` (app [pglobal (indt «t») «u», c1])
14c14
<         (prod `_`
---
>         (prod `i`
18c18
<           prod `_'`
---
>           prod `i'`
22c22
<            prod `_R`
---
>            prod `_`

and naming does not matter as everything is represented with Elpi binders.

[gares]

I guess it is a bug, here the code: https://github.com/LPCIC/coq-elpi/blob/e4bf0b0b3e092b16c89b4e49d64523902fe24d13/src/coq_elpi_HOAS.ml#L2684-L2700

Not sure I'll have to find it soon, but if you could instrument ...

[ecranceMERCE]

The error seems to come from the lift (https://github.com/LPCIC/coq-elpi/pull/388). I haven't added tests, but maybe we should (would just require forging a few indt-decl values by hand).

[gares]

HUM, I have to think about it. Later in the file there is large comment explaining a shift, and this one seems to accommodate for the same issue.

I'll think about it