Let's interpret a type as a "partial specification" of a value.  If we can express this "partial specification" completely enough so that one (and only one, at least ignoring values like bottom) value is a member of the type, then any expression of that value must be formally correct.

There are a couple of issues:  the type system is strong, but it still has limitations.  There are types we might like to express, but can't.  We might be able to express "supersets" of the type we really want, and the type inference engine will ensure that a value in the type meets at least this partial specification, but it cannot check to see if it is the "right" value in the type.  That is up to us.  Some of Haskell's properties, like referential transparency, equational reasoning, etc. make this easier than in other languages.

A related difficulty is that encoding specifications is a programming task in itself.  Even if you correctly compile requirements, and are able to completely encode them in the type system, you might still introduce a logic mistake in this encoding.  A similar issue is that logic mistakes can creep into the requirements compiling phase of a project.  In either of these cases, your values would dutifully and correctly compute the wrong things.