typedKanren: help me write a `length` predicate

This is a great response, it is much appreciated. I took a few days to study again how recursive logic programming works to finally understand what you said. But now I see why in both implementations termination is not possible.