This error occurs when translating the Rust standard library with Charon running in monomorphized mode. Below we first describe how the error arises when translating std, and then provide a minimal example (independent of std) to reproduce it.
Reproducing the error in std
The error can be triggered when translating std::env::* with the following commands:
cd charon
echo "fn main() {}" > file.rs
cargo build
./target/debug/charon rustc --monomorphize --start-from="std::env::*" --include=std --no-serialize -- --sysroot=$(rustc --print sysroot) file.rs
Part of the error output (there are other errors, which are omitted here) is:
error: Type error after translation:
Mismatched type generics:
target: Thin
expected: [Self]
got: []
Visitor stack:
charon_lib::ast::types::TraitDeclRef
charon_lib::ast::gast::TraitImpl
Binding stack (depth 1):
0: <[@TraitClause0]: @TraitDecl41<()>, {built_in impl @TraitDecl41 for ()}::Metadata = ()>
--> /rustc/library/core/src/ptr/metadata.rs:85:1
error: Type error after translation:
Mismatched type generics:
target: {impl Thin}::<()>
expected: []
got: [()]
Visitor stack:
charon_lib::ast::types::TraitImplRef
charon_lib::ast::types::TraitRefKind
charon_lib::ast::types::TraitRefContents
charon_lib::ast::hash_cons::HashConsed<charon_lib::ast::types::TraitRefContents>
charon_lib::ast::types::TraitRef
charon_lib::ids::index_map::IndexMap<charon_lib::ast::types::vars::TraitClauseId, charon_lib::ast::types::TraitRef>
charon_lib::ast::types::GenericArgs
charon_lib::ast::types::Binder<charon_lib::ast::types::GenericArgs>
alloc::boxed::Box<charon_lib::ast::types::Binder<charon_lib::ast::types::GenericArgs>>
charon_lib::ast::names::PathElem
alloc::vec::Vec<charon_lib::ast::names::PathElem>
charon_lib::ast::names::Name
charon_lib::ast::meta::ItemMeta
charon_lib::ast::gast::FunDecl
Binding stack (depth 2):
0:
1:
--> /rustc/library/core/src/ptr/mod.rs:862:1
After inspecting /rustc/library/core/src/ptr/metadata.rs:85:1 and /rustc/library/core/src/ptr/mod.rs:862:1 (using rustc version nightly-2026-02-07, which matches the version used to compile Charon), @maltuned and I found that the error is caused by the use of trait alias).
Minimal reproduction
We constructed the following minimal example to reproduce the error:
#![feature(trait_alias)]
trait A {}
trait B = A;
impl A for i32 {
}
fn f<T : B>() {
}
fn main() {
f::<i32>();
}Running:
charon cargo --monomorphize --no-serialize
produces:
error: Type error after translation:
Mismatched type generics:
target: B
expected: [Self]
got: []
Visitor stack:
charon_lib::ast::types::TraitDeclRef
charon_lib::ast::gast::TraitImpl
Binding stack (depth 1):
0: <[@TraitClause0]: @TraitDecl1<i32>, [@TraitClause1]: @TraitDecl0<i32>>
--> src/main.rs:5:1
|
5 | trait B = A;
| ^^^^^^^^^^^^
error: Type error after translation:
Mismatched type generics:
target: {impl B}::<i32>
expected: []
got: [i32]
Visitor stack:
charon_lib::ast::types::TraitImplRef
charon_lib::ast::types::TraitRefKind
charon_lib::ast::types::TraitRefContents
charon_lib::ast::hash_cons::HashConsed<charon_lib::ast::types::TraitRefContents>
charon_lib::ast::types::TraitRef
charon_lib::ids::index_map::IndexMap<charon_lib::ast::types::vars::TraitClauseId, charon_lib::ast::types::TraitRef>
charon_lib::ast::types::GenericArgs
charon_lib::ast::types::Binder<charon_lib::ast::types::GenericArgs>
alloc::boxed::Box<charon_lib::ast::types::Binder<charon_lib::ast::types::GenericArgs>>
charon_lib::ast::names::PathElem
alloc::vec::Vec<charon_lib::ast::names::PathElem>
charon_lib::ast::names::Name
charon_lib::ast::meta::ItemMeta
charon_lib::ast::gast::FunDecl
Binding stack (depth 2):
0:
1:
--> src/main.rs:11:1
|
11 | / fn f<T : B>() {
12 | |
13 | | }
| |_^
error: Type error after transformations:
Mismatched type generics:
target: B
expected: [Self]
got: []
Visitor stack:
charon_lib::ast::types::TraitDeclRef
charon_lib::ast::gast::TraitImpl
Binding stack (depth 1):
0: <[@TraitClause0]: @TraitDecl1<i32>, [@TraitClause1]: @TraitDecl0<i32>>
--> src/main.rs:5:1
|
5 | trait B = A;
| ^^^^^^^^^^^^
error: Type error after transformations:
Mismatched type generics:
target: {impl B}::<i32>
expected: []
got: [i32]
Visitor stack:
charon_lib::ast::types::TraitImplRef
charon_lib::ast::types::TraitRefKind
charon_lib::ast::types::TraitRefContents
charon_lib::ast::hash_cons::HashConsed<charon_lib::ast::types::TraitRefContents>
charon_lib::ast::types::TraitRef
charon_lib::ids::index_map::IndexMap<charon_lib::ast::types::vars::TraitClauseId, charon_lib::ast::types::TraitRef>
charon_lib::ast::types::GenericArgs
charon_lib::ast::types::Binder<charon_lib::ast::types::GenericArgs>
alloc::boxed::Box<charon_lib::ast::types::Binder<charon_lib::ast::types::GenericArgs>>
charon_lib::ast::names::PathElem
alloc::vec::Vec<charon_lib::ast::names::PathElem>
charon_lib::ast::names::Name
charon_lib::ast::meta::ItemMeta
charon_lib::ast::gast::FunDecl
Binding stack (depth 2):
0:
1:
--> src/main.rs:11:1
|
11 | / fn f<T : B>() {
12 | |
13 | | }
| |_^
Charon version: the latest Charon in monomorphized mode (commit 77d5206)
Explain the bug: (why is this behavior incorrect, and what do you think Charon should do instead)
The trait aliases are not correctly translated in monomorphized mode because the PR about supporting dynamic trait object in mono mode only deals with the "normal" (contrary to trait alias) traits by keeping the generic and associative types. This makes the translation of trait aliases inconsistent with the nornal traits, which caused the mismatched type generics error.
To solve this problem, we think the generic types of trait aliases should also be preserved in mono mode, which is consistent with the treatment of normal traits.
This error occurs when translating the Rust standard library with Charon running in monomorphized mode. Below we first describe how the error arises when translating
std, and then provide a minimal example (independent ofstd) to reproduce it.Reproducing the error in
stdThe error can be triggered when translating
std::env::*with the following commands:Part of the error output (there are other errors, which are omitted here) is:
After inspecting
/rustc/library/core/src/ptr/metadata.rs:85:1and/rustc/library/core/src/ptr/mod.rs:862:1(usingrustcversionnightly-2026-02-07, which matches the version used to compile Charon), @maltuned and I found that the error is caused by the use of trait alias).Minimal reproduction
We constructed the following minimal example to reproduce the error:
Running:
produces:
Charon version: the latest Charon in monomorphized mode (commit 77d5206)
Explain the bug: (why is this behavior incorrect, and what do you think Charon should do instead)
The trait aliases are not correctly translated in monomorphized mode because the PR about supporting dynamic trait object in mono mode only deals with the "normal" (contrary to trait alias) traits by keeping the generic and associative types. This makes the translation of trait aliases inconsistent with the nornal traits, which caused the
mismatched type genericserror.To solve this problem, we think the generic types of trait aliases should also be preserved in mono mode, which is consistent with the treatment of normal traits.