[pufuwozu]

That checking is by definition, not type safety.

What you're talking about now is totality. Both Haskell and Clojure allow non-total functions (functions which may not return a result) - the checking that they do are to stop undefined results. Agda is an example of a language that only allows total functions.

[rprospero]

Adding the fromJust Haskell argument seems to have confused the argument I was trying to make. I had two points. The first one was better expressed by Evbn and I don't really have anything to add to that.

The second was that Clojure arguably has a type system. There is exactly one type, Stuff. Every function takes Stuff and returns Stuff. Of course, functions themselves are a kind of Stuff. Now, it lacks totality, but otherwise every compiled Clojure program has passed the type checker. It's just that type checking is a no-op, since there's no way for anything to have the wrong type.

[Evbn]

Totality is different. In C you can (using a pointed cast cast) add a float to an intended and get gobbledygook (by interpreting the bits in memory incorrectly) and keep going. In Closure you can't, it will throw an exception, but you won't get warned about that until runtime.