Extend MIR with type assertions

[nikomatsakis]

Real MIR carries "user type assertions" that correspond to pattern annotations and the like. We need to add that to a-mir-formality.

@lcnr has recently been fixing bugs in those and is probably well-equipped to advise here.