[mcguire]

"If this were true then functions would not need bodies, you would just define their signatures and move on with life."

That's because both addition and multiplication, for example, have the same type signature.

    Prelude> :type (+)
    (+) :: Num a => a -> a -> a
    Prelude> :type (*)
    (*) :: Num a => a -> a -> a

A better rephrasing might well be "If it compiles and you've used the right operations, which is made easier because most of the wrong operations will blow chunks all over the place, it works."

Dependent typing anyone? (I think what you're looking for goes by the name "code extraction" in Coq, but I've never gotten into it as a programming environment.)