[spilling] Anomaly from compiler.ml in v2.0.6

[kyagrd]

Got this assertion failure anomaly while I was using coq-elpi.

Anomaly "File "src/compiler/compiler.ml", line 1712, characters 52-58: Assertion failed."

This is the code.

Elpi Accumulate LamTri lp:{{
    % iterate until failure 
    pred iterate    i:(pred i:A, o:A), i:A, o:(list A).
    iterate F X [X|XS] :- iterate F {F X} XS ; XS = [].

    %%% no Anomaly without spilling like below
    % iterate F X [X|XS] :- F X Y, iterate F Y XS ; XS = [].
}}.

Elpi Query LamTri lp:{{
    iterate (x\ y\ if (x < 10) (y is (x + 1)) fail) 1 L,
    coq.say "L = " L
}}.

[gares]

Thanks for reporting, the bug is that this line

elpi/src/compiler/compiler.ml

Line 1710 in 1992fb3

| Var _

should really be doing Var l -> Var (l @ args) instead of failing.

[kyagrd]

Yay! thanks for the quick fix!!!