`findall_solutions P` may be inconsistent wrt unification variables in `P`

[swasey]

I ran across what appears to be an inconsistency.

In the following, I invoke findall_solutions with two (deterministic) queries. In the first query the name N in test gets unified with the solution. In the second query, it does not.

Require Import elpi.elpi.

Variant atomic_name : Set := Nanon.
Variant name : Set := Nglobal (c : atomic_name).

Elpi Program test lp:{{ }}.
Elpi Accumulate lp:{{

    namespace cpp {
        kind atomic_name, name type.
        type Nanon atomic_name.
        type Nglobal atomic_name -> name.
    }

    namespace cpp.atomic_name {
        pred of_term i:term, o:cpp.atomic_name.
        of_term T C :-
            ( T = {{ Nanon }}, !, C = cpp.Nanon
            ; coq.error "cpp.atomic_name.of_term" ).
    }

    namespace cpp.name {
        pred of_term i:term, o:cpp.name.
        of_term T N :-
            T = {{ Nglobal lp:CT }},
            N = cpp.Nglobal {cpp.atomic_name.of_term CT}.

        pred gen o:cpp.name.
        gen (cpp.Nglobal cpp.Nanon).
    }

    pred test i:(cpp.name -> prop).
    test Gen :-
        findall_solutions (Gen N) [_],
        ( ground_term N, !, coq.say "name:" N
        ; coq.error "name not ground:" N ).

}}.
Elpi Typecheck.

Succeed Elpi Query lp:{{ test cpp.name.gen }}.  (* name: cpp.Nglobal cpp.Nanon *)
Fail Elpi Query lp:{{ test (cpp.name.of_term {{ Nglobal Nanon }}) }}.   (* name not ground: X0 *)

[gares]

I confirm this is a bug (in elpi). I think the expected behavior is the second one, that is the query term to findall_solutions is not assigned.

[gares]

In any case, you should look for the value of N in the list of results, eg findall_solutions (Gen _) [Gen N] or something like this.

[gares]

The discrepancy comes from the fact that cpp.name.gen has only one clause so I believe Elpi does not even set up the trail to backtrack (this is a little bug IMO). If you add a second clause to gen, then the two tests behave the same.

[gares]

I clarify the doc here https://github.com/LPCIC/elpi/pull/230

[swasey]

Thanks for taking a look, and for adjusting the docs.

My chief concern had been that the discrepancy might be a symptom of a deeper flaw. (I do look to the list to instantiate things.)