>So, I'd love a language with a type checker that when ahead-of-time compiling code would refuse to emit libraries/binaries when it couldn't statically prove ty

>So, I'd love a language with a type checker that when ahead-of-time compiling code would refuse to emit libraries/binaries when it couldn't statically prove types were used correctly. In interpreted mode, it would only refuse to load code that it could statically prove contained type errors. Maybe when used within an interactive session, it would still allow (but warn) when code provably has type errors. Haskell can do that. https://downloads.haskell.org/~ghc/7.8.2/docs/html/users_guide/defer-type-errors.html https://downloads.haskell.org/~ghc/7.8.2/docs/html/users_gui...