This is an excellent observation--and indeed, one of the things about implementing (so, so many versions of) microKanren is that I've learned the paper version

This is an excellent observation--and indeed, one of the things about implementing (so, so many versions of) microKanren is that I've learned the paper version relies heavily on magic. It is very easy to get a microKanren that works sometimes, but explodes in some conditions, because of the subtle ways that the paper relies on the behavior of improper lists (raw cons pairs) vs proper lists, and because many recursive cases which would normally be explicitly enumerated (or handled via polymorphic dispatch) just happen to work correctly thanks to the way they encode bindings, substitutions, etc as lists. In particular, there are many places where it looks like a `map` might make things simpler, but will subtly break things, thanks to the need to recurse into improper lists. The mplus/bind control flow graph is also... extremely tricky if you aren't precise about null/empty/car/cdr. If you take a look at the "full" version of this program, which uses more struct types, it involves a good deal more explicit recursion: https://gist.github.com/aphyr/4d41e7655b10a68e753f729bdc1c5a6d#file-minikanren-pl-L522-L542 https://gist.github.com/aphyr/4d41e7655b10a68e753f729bdc1c5a... her kanren can't really solve "inside" of the structs that she asked to be provided. Ahhhh, so this is true, and actually a feature: uKanren exploits scheme vectors as lvars, and initially my language was just lists. I wound up adding structs precisely so that I'd have an analogous non-list compound type!