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 s

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-predicates https://blog.adacore.com/spark-2014-rationale-type-predicate... if interested.