I am using Racket v8.5, with the packages for minikanren and
minikanren/numbers required. Why does introducing the numbero
constraint cause previously valid unifications to fail?
> (run 1 (q) (<lo '(1) q))
'((_.0 _.1 . _.2))
> (run 1 (q) (<lo '(1) q) (numbero q))
'()
> (run 1 (q) (numbero q) (<lo '(1) q))
'()
> (run 1 (q) (<lo q '(1)))
'(())
> (run 1 (q) (<lo q '(1)) (numbero q))
'()
> (run 1 (q) (numbero q) (<lo q '(1)))
'()
Because the numbero constraint enforces that a term is consistent with a number in the host language (Racket in this case). Think of numbero as the constraint equivalent of Racket's number? predicate: (numbero 5) succeeds. However, you are using Kisleyov's relational arithmetic system, in which numerals are represented as little-endian lists of binary digits: (numbero '(1 0 1)) fails, just as (number? '(1 0 1)) returns #f in Racket.