Bug: error on dereferencing a `Copy` type inside a closure

[maximebuyse]

Code snippet to reproduce the bug:

fn f<T: Copy>(x: &T) {
    let _c = || *x;
}

Charon version: ed22146

Charon command: charon cargo --preset=aeneas

Charon output:

error: Type error after transformations:
       Found incorrect clause var: Bound(1, 0)
       Visitor stack:
         charon_lib::ast::types::TraitRef
         charon_lib::ids::index_vec::IndexVec<charon_lib::ast::types::vars::TraitClauseId, charon_lib::ast::types::TraitRef>
         charon_lib::ast::types::GenericArgs
         alloc::boxed::Box<charon_lib::ast::types::GenericArgs>
         charon_lib::ast::types::TraitImplRef
         charon_lib::ast::types::RegionBinder<charon_lib::ast::types::TraitImplRef>
         charon_lib::ast::types::ClosureInfo
         charon_lib::ast::gast::ItemSource
         charon_lib::ast::types::TypeDecl
       Binding stack (depth 2):
         0: 
         1: <'_0, T>
 --> src/main.rs:4:14
  |
4 |     let _c = || *x;
  |              ^^^^^

[maximebuyse]

If this can help, I debugged using claude, and here is what it says (I can PR if this looks like a good explanation):

Root cause: The --remove-adt-clauses transform (used by --preset=aeneas) clears all trait clauses from type declarations. For closure ADTs, however, the ItemSource::Closure { info } field carries RegionBinder<TraitImplRef> references to the closure's Fn/FnMut/FnOnce impls, and those references contain Clause(Bound(1, 0)) vars that point to the closure ADT's clauses. Stripping the closure ADT's clauses leaves those references dangling, which the type checker reports as Found incorrect clause var: Bound(1, 0).

For the repro:

• f<T: Copy> → closure inherits T and the T: Copy clause from f.
• The closure's FnOnce/FnMut/Fn impls have where T: Copy. The ClosureInfo references those impls and passes Clause(Bound(1, 0)) for the Copy<T> slot.
• remove_adt_clauses clears the closure ADT's Copy<T> clause but leaves the ClosureInfo references untouched → invalid var.

Fix: charon/src/transform/simplify_output/remove_adt_clauses.rs — collect closure ADT IDs up front (those with ItemSource::Closure { .. }) and skip them when clearing trait clauses on TypeDecls, and skip clearing trait refs on TypeDeclRefs pointing at those ADTs. Closure ADTs keep their parent-inherited clauses; non-closure ADTs are unaffected.

[Nadrieril]

Oh, yep the analysis sounds right. The truth is that --remove-adt-clauses is fundamentally an ugly hack. We can't skip closure ADTs tho, these are the exact case for which @sonmarcho requested the --remove-adt-clauses flag.

I propose the following fix instead: instead of just removing the clauses, we also replace any reference to them with TraitRefKind::BuiltinOrAuto (and adjust documentation of BuiltinOrAuto accordingly, as well as add a BuiltinImplData::RemovedAdtClause variant).