This tradeoff sounds similar to the choice to use "tagged types" versus "variant records" in Ada. Ada has provided variant records since 1983 and tagged types since 1995 (and both with a very nice syntax).
https://learn.adacore.com/courses/intro-to-ada/chapters/more...
I believe the SPARK subset can (through static analysis) ensure that only valid fields are accessed for the current discriminant.