Feature request: add `needs_drop` to `TypeDecl` info

[ssyram]

The needs_drop is a natural info in Rustc and it is needed especially when trying to verify memory safety. How about adding a needs_drop: Either<Vec<TypeDbVar>, bool> field to the definition of TypeDecl? The Vec<TypeDbVar> means "whether this generic type needs drop depends on this list of the generic param types, if any of them has needs_drop == Right(true) then this type also needs drop".

[Nadrieril]

Good idea yeah :) One difficulty is that it should work with substitution. We can either make it a Vec<Ty> or add a special case in visit_vars. I'd prefer Vec<Ty> because we'll need a Ty::needs_drop(&self, krate: &TranslatedCrate) method anyway. Something like:

struct TypeDecl {
  ..
  /// Describes whether the type has non-trivial drop glue.
  needs_drop: NeedsDropPredicate,
}
/// Describes whether a type has non-trivial drop glue.
struct NeedsDropPredicate {
  /// A list of types that are `drop`ped in the destructor of the type we care about. The type has
  /// significant drop iff any of these type has. In particular, if this list is empty
  /// then the type we care about has trivial drop glue.
  calls_drop_for: Vec<Ty>,
}

[ssyram]

Cool! But in that case, the inquiry procedure will have to be implemented also in the client codes, e.g., Charon-ML. Will this make the maintenance tougher?

While the results should be a fixed value for mono LLBC, to cache the final results somehow might be more straightforward?

[Nadrieril]

the inquiry procedure will have to be implemented also in the client codes

That's unavoidable: in practice for verification you'll have a Ty for which you want to know if it requires drop.

While the results should be a fixed value for mono LLBC, to cache the final results somehow might be more straightforward?

You may be misunderstanding me: I propose to store the same thing as you do, i.e. just the type variables that are relevant for dropping. I'm only saying they should be represented as a Ty instead of a TypeDbVar. And then when we substitute, we should add a procedure that normalizes the NeedsDropPredicate to once again only mention type vars.

Also to be fully precise type variables aren't enough, we may need associated types too. E.g. Cow will have <T as TOOwned>::Owned in its NeedsDropPredicate list. So we don't have a choice.

[ssyram]

OK, thanks for the in-depth discussion! It makes total sense!