Mmmh thanks for the link and the paper about generative types. Seems very interesting!

I'm wondering if using type predicates or type invariants (+ proof for static verification, otherwise the check will mostly be at runtime) would help here.

Look up https://blog.adacore.com/spark-2014-rationale-type-predicate... if interested.