Add checking for functions wf / body

[nikomatsakis]

We need to add a "type-check" for functions with the following parts:

Decl layer

• Assuming:
  • function where-clauses hold
  • argument and return types are "valid" (need a term for this, in the absence of full implied bounds, this does not mean we can assume they are completely valid)
• Prove:
  • Where clauses are well-formed
  • Argument, return types are well-formed

Typeck layer

Additionally prove that MIR type checks and produces a valid of the given return type