Pitfalls

A collection of mistakes that trip up newcomers and veterans alike, each cross-referencing where it is covered in depth.

Misleading precedence of =>

If a hypothesis added with => does not reach the goals you expect, this is almost always why: => binds tighter than ,, so in A, B => C, D the hypothesis B reaches only C, not D. A debug print between the goals, A, B => print C, D, shows where it stops: print C sees B, D does not. The fix is ==>, which binds looser than ,; Elpi also warns where the => precedence bites. The parse rules are given in Inference rules and queries.

Treacherous one-rule anonymous predicates

A variable is a parameter of the whole rule it occurs in, not of an anonymous predicate nested inside it, so a variable used only inside a std.map (or similar) callback is shared by every call the traversal makes, not fresh per call, unless a sigma says otherwise (Binders and HOAS):

../code/anonymous-predicate.elpi:

% A variable is a parameter of the whole rule, not of an anonymous predicate
% nested inside it: A below is shared by every call std.map makes, unless a
% sigma gives each call its own.

pred p int -> int.
p X Y :- Y is X + 1.

pred q int -> int.
q X Y :- Y is X * 10.

pred wrong list int -> list int.
wrong L L1 :- std.map L (x\ r\ p x A, q A r) L1.        % A is the same for every x

pred right list int -> list int.
right L L1 :- std.map L (x\ r\ sigma A\ p x A, q A r) L1. % a fresh A per call

main :-
  (wrong [1, 2, 3] _ ; print "wrong: fails (A can't be both 2 and 3)"),
  right [1, 2, 3] R, print "right:" R.

wrong: fails (A can't be both 2 and 3)
right: [20, 30, 40]

A named, top-level predicate sidesteps the issue entirely: its own variables are fresh at every call by construction, with no sigma to remember.

Scope error as a silent failure

A unification that fails because a term escapes its scope (a hole assigned a value that mentions a name it cannot see) fails with nothing marking it as different from an ordinary logical failure. In practice this is almost always a mistake, not a deliberate use of scoping: most often, a variable used right after a pi/sigma that needed its own, inner sigma (Binders and HOAS) rather than reusing one from further out. If a goal fails for no apparent reason, a scope mismatch is worth checking before anything else.

=!=> and functional predicates

Adding a rule to a func predicate at run time, through ==>, can trip the determinacy checker even when the rule is only ever meant to fire once. =!=> adds the missing cut automatically; see Inference rules and queries.

Unification variables are not imperative variables

X = 1 does not set X; it unifies it, once, for good (until backtracking undoes it). A later X = 2 does not overwrite it: it tries to unify the already-1 X with 2, and fails, since 1 and 2 are not the same term:

../code/logic-variable.elpi:

% A unification variable is not a mutable slot: once assigned, a second
% "assignment" is a unification against the existing value, which fails
% unless it happens to agree.

main :-
  X = 1, print "X is now" X,
  (X = 2, print "reassigned to" X
   ; print "cannot reassign: X is already 1, not 2").

X is now 1
cannot reassign: X is already 1, not 2

Code that needs an evolving value across a computation should thread a fresh variable through each step (Binders and HOAS, sigma for each new one) or use the constraint store as an explicit global (The constraint store), not repeated assignment to the same variable.