[ambrosebs]

To type check Clojure idioms we use techniques that resemble light-weight dependent types. No particular attempt is made to go beyond the minimum required for checking certain idioms.

We can express lengths of sequences for example, but they only support explicit lengths: you can't put a type variable in the length position.