Spans of quantified variables

[fpoli]

The Spanned::get_spans method needs a MIR body to obtain the spans of variables stored in the ForAllVars<'tcx> type. Currently, the MIR body is passed as argument and is used to resolve all quantifiers in an assertion, but each quantifier should use its own MIR body: the one in which the quantified variables are declared.

https://github.com/viperproject/prusti-dev/blob/7ac30e86ecd31a8b766c1a50a719dd4302bc4d17/prusti-interface/src/specs/typed.rs#L54-L62

A solution:

1. Add a definition: LocalDefId field to the typed::ForAllVars structure (this probably requires adding one more type parameter to common::ForAllVars`).
2. Remove the mir_body: mir::Body argument from all Spanned::get_spans methods, using the precedently added definition field to resolve local variables in typed::ForAllVars.

[Aurel300]

Spanned no longer exists in the codebase. Errors (parse and type) are reported at the correct location thanks to how the new preparser works. There are two potential problems still:

• unused qvars are not reported (because somewhere there is an allow(unused_vars) to suppress other warnings we would get, I imagine)
• Prusti encoding/internal errors when encoding a qvar type are unwrapped, or reported with the body span in #882

We should get the span of the qvar local from the MIR to report errors (make this change as part of #882).