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 inserted print-env yields:
And the full stack trace:
Example not minimal, unclear if `match` is the problem
Comment made by: zerokarmaleft
Sorry, forgot JIRA eats formatting.