Properly support open type invariants

[voidc]

The #[open_inv] attribute can be applied to functions, function arguments, and fields to declare them as having an open type invariant. Concretely:

• on functions: completely ignore type invariants in this function, including return value, quantifiers and resolves
• on arguments: ignored during invariant elaboration
• on fields: ignored in generated structural invariant

In its current state, the feature is only meant to be used as an escape hatch for cases where would otherwise run into problems with translation cycles (e.g. the map tests). A proper implementation should have additional checks ensuring that it is used correctly. The issue becomes especially relevant with #842 which enables the following unsound uses:

fn magic1<T>(#[open_inv] x: T) -> T { x }

struct Foo<T> { #[open_inv] f: T }
fn magic2<T>(x: Foo<T>) -> T { x.f }

trait Bar { #[open_inv] fn f() -> Self; }
fn magic3<T: Bar>() -> T { T::f() }

[voidc]

One solution might be to only allow the attribute on fully concrete types.

[jhjourdan]

Why would it change anything?

• open_inv on functions and fields is unsound (thing about resolves) and should be removed at some point. If we think it is really needed somewhere in our tests, then we should think again about the design, because this basically means that invariants cannot be used as we want.
• open_inv on function argument or return values (which is a feature that does not exists) should be useful, but we have to take care of the interaction with #842.