Dissimilar lengths of HVecs in a union doesn't type-check

Setting up a simple union type for nats with a vector encoding, where the first element is the tag (:zero or :succ). The :zero constructor is nullary, but the :succ constructor recurses. The type checker doesn't seem to correctly handle union types consisting of HVecs of different lengths

The namespace:

The inserted print-env yields:

And the full stack trace: