[Veedrac]

Technically that would be something like Haskell's, but I only have surface-level fluency. More to the point would be the most complex stuff I've had reason to do with a type system, which caps at around this generic state machine:

https://play.rust-lang.org/?gist=3fdb20c34d589a2576c6bb137b9...

(TL;DR: A type that encodes a state machine (and is generic over the implementation) that allows you to guarantee reaching a terminating state.)

In practice I rather my types looking much plainer, though:

https://github.com/llogiq/bytecount/blob/master/src/lib.rs