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 #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.)