Comment by tauoverpi

Yep, I missed it as I don't often work in haskell anymore but with the correction the rest of the above still stands (haskell syntax is still the most efficient I'm aware of for talking about this). Also, it being unimplementable is also a nice property of having such a type system as you can prove that your specification is impossible to implement (more applicable in Lean, ATS2, Idris, Agda) or make invalid states impossible to even write (consider state transition rules at the type level).