Stefan, the way you described the case composed of separate product and raw (untagged) sum certainly reminds me of the low-level languages we used to work in, but the types and proofs certainly become low-level is well. Macros can hide some of it, but I'm not sure I'd like macros doing the work that should 'rightfully' belong to the compiler... and I don't think ultra-low-level primitives is what you're aiming for with Typer.
Actually, I do want to move as much of the compilers's work to libraries (sometimes via macros), and I'd be happy if that gives access to very low-level operations.
I think the problem is whether it will be workable in practice (the cost of constructing/manipulating all those extra proofs could be prohibitive).
So as you concluded here, I think a tagged sum as a primitive could work, but then the rest of the record/product is unspecified, in the style of row(ρ) polymorphism. We know field zero is an int, and the rest is a dependent type based on type-level discrimination of the singleton int type... or is that piece getting back to the low-level stuff?
Indeed, maybe a middle point where we hard code the "switch on field-0 which is an int". That still allows funny things such as take a tuple from one union type and use it as-is in another union type.
Stefan