Reject move from struct that implements drop

[kirloo]

What does this PR do?

Resolves #422

How does it work, what questions do you have?

I reused the logic from prove_ty_is_copy for a function prove_ty_is_drop and added a predicate that prove_ty_is_drop should fail for the TypedPlaceExpressionData::Field branch of prove_place_is_movable.

prove_ty_is_copy and prove_ty_is_drop are nearly the same function, so maybe I could have refactored into a function like "prove_ty_is_trait".

AI disclosure

• I used an AI tool for research, autocomplete, or in other minimal ways

[rustbot]

Thanks for contributing to formality! :)
A reviewer will take a look at your PR within a week or two. If not, come talk to us on https://rust-lang.zulipchat.com/#narrow/channel/402470-t-types.2Fformality

[nikomatsakis]

See comments on Zulip. Let's restructure this like so:

• extend TypedPlaceExpressionData::Field with the AdtId and variant info
• write a helper on Program to search for an impl of Drop for a given adt, taking advantage that we don't care about where-clauses etc
• then in the rule we can just check like (if let None = program.find_drop_impl(adt_id))

View changes since this review

[kirloo]

@nikomatsakis I'm curious about what you think now. I had to split the TypedPlaceExpressionData::Field variant into two variants, Field and TupleField, since tuples don't have an AdtId.

[rustbot]

This PR was rebased onto a different main commit. Here's a range-diff highlighting what actually changed.

Rebasing is a normal part of keeping PRs up to date, so no action is needed—this note is just to help reviewers.

[nikomatsakis]

This looks great @kirloo !

View changes since this review