First class support for type parameters in VIR

[fpoli]

Currently, the vir module in which statements and expressions are defined has no notion of type parameters. To support Rust code that uses type parameters, Prusti uses a fragile regexp-based approach implemented in prusti-common/src/vir/ast/typaram.rs, plus a variety of hacks that can be found by searching for one of the following comments.

• // FIXME; hideous monstrosity...
• // FIXME oh dear...
• // FIXME: the following fields serve a grotesque hack.
• // FIXME: A hack. Replaces all generic types with their instantiations

To avoid the regular expressions and the hacks, we could extend vir::Expr and vir::Type to make them aware of type parameters and type substitutions.

[vakaras]

I think we should check whether it would be cleaner to have two layers of VIR: a generic VIR and monomorphic VIR that can be directly translated into Viper.

[Aurel300]

Can you see other issues that can be addressed by having the poly-/monomorphic variants?

[Aurel300]

I'll close this. We no longer have the fragile regexp-base hack in the codebase (since #899 and a bunch of work by @vl0w), so generics are much more robust, although associated types might still take some more work (possible changes in #980). I also think having "first-class type parameters" in the VIR is the wrong decision: this is the job of the compiler. VIR poly thus should (and does not) have type parameters. @vakaras might be using them in the unsafe core proof VIR layers for dealing with lifetimes.