What's different to typical Algebraic-Types/Sum-Types/Nü-Enums in what they showed is that it's Values being OR'd, not types. That is presumably why they are obliquely mentioning it in the comments thread of an Idris release, because Idris is known for "Dependent Types", i.e. types that depend on actual values, not just other types.