Bug: Compiler panic with `--precise-drops`

[Nadrieril]

After #912,

//@ charon-args=--precise-drops
struct KeccakState;

struct PortableHash<const K: usize> {
    shake128_state: [KeccakState; K],
    make_non_trivial: Box<u32>,
}

fn foo(_: PortableHash<42>) {}

causes

error: internal compiler error: compiler/rustc_middle/src/ty/sty.rs:373:13: cannot find `K/#0` in param-env: ParamEnv {
                                    caller_bounds: [
                                        Binder { value: HostEffectPredicate { trait_ref: <T as std::marker::Destruct>, constness: Maybe }, bound_vars: [] },
                                        Binder { value: TraitPredicate(<T as std::marker::Destruct>, polarity:Positive), bound_vars: [] },
                                    ],
                                }


thread 'rustc' panicked at compiler/rustc_middle/src/ty/sty.rs:373:13:
Box<dyn Any>
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
error: rustc panicked while retrieving drop glue. This is known to happen ith `--precise-drops`; to silence this warning, pass `--opaque '{impl core::marker::Destruct for test_crate::PortableHash}'` to charon
 --> tests/ui/simple/drop-glue-with-const-generic.rs:5:1
  |
5 | / struct PortableHash<const K: usize> {
6 | |     shake128_state: [KeccakState; K],
7 | |     make_non_trivial: Box<u32>,
8 | | }
  | |_^

error: Item `test_crate::PortableHash` caused errors; ignoring.
 --> tests/ui/simple/drop-glue-with-const-generic.rs:5:1
  |
5 | struct PortableHash<const K: usize> {
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This is a known consequence of rustc's drop elaboration not being written to handle generics properly. I have documented this in the --precise-drops option and will leave things like that for now. But ideally we'd write a PR to rustc to make drop elaboration generics-friendly.