Is Wadler's 'Theorems for Free' as general as Design By Contract for establishing correctness?
"Theorems for free" are so-called because they follow from the type of the program, without looking at the the program code!

"Contracts" are clearly not free theorems, because they depend on the code of the program, not merely the type.

However, the connection you do want to make is between types and specifications.  Specifications are in a way "more detailed" types.  Or, state the other way, types are more basic specifications.  Martin-Lof type theory is precisely about fusing the two ideas into one.