Clojure's spec basically provides that, but it does so at run-time while in development mode. I think Idris may have some similar capability there at compile-ti

Clojure's spec basically provides that, but it does so at run-time while in development mode. I think Idris may have some similar capability there at compile-time. I suspect the wrangling involved to get a static type checker to precisely describe this would probably not often be worth the effort.