Reported by @sonmarcho:
//@ charon-args=--hide-marker-traits
#![feature(const_destruct)]
use std::marker::Destruct;
fn drop<T: Destruct>(_: T) {}
gives
fn drop<T>(@1: T)
{
let @0: (); // return
let @1: T; // arg #1
@0 := ()
@0 := ()
drop[missing(@TraitClauseBound(0, 1))] @1
return
}
Note the missing trait ref, caused by removing the Destruct clause.