How is a type checker different from a proof checker?

A type checker can be a proof checker. Theoretically, a full proof that the program meets some arbitrary specification could be encoded in type annotations.