Debug implementation causes Creusot ICE

[xldenis]

thread 'rustc' panicked at creusot/src/backend/ty_inv.rs:69:18:
not implemented: dyn [Binder { value: Trait(std::fmt::Write), bound_vars: [] }] + '?24
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

error: the compiler unexpectedly panicked. this is a bug.

note: we would appreciate a bug report: https://github.com/creusot-rs/creusot/issues/new

note: please make sure that you have updated to the latest nightly

note: rustc 1.82.0-nightly (c1a6199e9 2024-07-24) running on aarch64-apple-darwin

note: compiler flags: -Z unstable-options --crate-type bin -C embed-bitcode=no -C debuginfo=2 -C split-debuginfo=unpacked

note: some of the compiler flags provided by cargo are hidden

query stack during panic:

[jhjourdan]

What's the source ?

[xldenis]

I added a derive(Debug) on a simple type.

[jhjourdan]

Wow. That is using dyn ?

[xldenis]

yes of course, the write! macros are expressed in terms of trait objects to make them easily generic over the specific writers without tons of monomorhpization.