> In an ideal world, tests would be subsumed by types

It would be literally impossible for this to happen in a Turing-complete language, though, because a hypothetical 'perfect' type system would be able to solve the halting problem.

The Haskell 'Bottom' type alludes to this in its documentation, actually: http://www.haskell.org/haskellwiki/Bottom

(Essentially, Bottom is a member of every type, or else the compiler would need to distinguish between a halting program and a non-halting program before accepting the input program).