Nor do unit tests. The power level when used correctly is similar.

I'm not sure if I agree about the highly subjective "power level" claim, but then who's to say.

More specifically, it's quite certain that types are capable of solidly dispatching some kinds of errors and tests a different kind. In other words, they are orthogonally optimized and combine well.

Just about every unit test suite I've seen includes a reimplementation of a typechecker.

Type checking does not verify behavior

Yes, it does verify behavior... "up to" how well your types describe your program's behavior. That is, you get a free proof that your program does at least what it says it does in its types.

If, for example, I give one of my Haskell functions the type "f: [a] -> a", I know that it a) does not have side effects, and b) must pick some element from the list to hand me back, i.e. it cannot just construct or cast "something" to an 'a' and give me that. (There is a caveat around explicit "unsafeXXX" usage, but that's mostly beside the point.)

Both of those properties constrain behavior and are impossible to prove using unit testing.

How can you tell the function doesn't return a modified 'a', or create a new 'a' based on the values in the list (i.e., an average)?

Or, for that matter, how can you tell the function doesn't return a completely new 'a' from hardcoded values?

It seems my confusion was that 'a' represents a generic in Haskell. Since the parameter is generic the function can't perform any type-specific operations on the value (e.g., creation or modification), and since it doesn't accept a function to apply to the values in the list, the only thing it can do is return one of the values it was given.

Yes, exactly. There's no way to construct a value of an arbitrary type -- outside of non-termination[1] (which doesn't really produce any values) or abuses of unsafeXXX functions. I think I perhaps should have been more explicit in my example. It could also have been specified as

   f: forall a . [a] -> a

which would make it more explicit that the function has to work for any given 'a'.

[1] ... which I think I should have actually specified. The function type given does not preclude non-termination in Haskell. (You can specify such things in Idris/Coq/Agda, but the effort of implementing f can be much higher if you have to prove totality.)

If said a implements the Num typeclass (can kind of think of it like an interface) then you can perform Num specific operations such as adding/subtracting or averaging.

It verifies all the behavior that you tell it to. Consider the simple example used to help teach people to use type systems effectively: tic tac toe. You can write an implementation of tic tac toe in which the behavior of the game is type checked. You can even do so in java, although it is certainly more effort than in a more powerful language.

It verifies types, which most unit test suites I've seen with dynamic languages duplicate.

Most Haskell programmers also write exhaustive tests, the type system is great but it's not there so you can avoid writing tests.