charon
charon copied to clipboard
Failure on function returning iterator with lifetime annotation
Charon commit https://github.com/AeneasVerif/charon/commit/e0b2b31542eaf8725757880ec62f27bc00a0007f aborts on the following code with error message Compilation failed: error: Unimplemented: Alias(Alias { kind: Opaque, args: [Lifetime(Region { kind: ReEarlyParam(EarlyParamRegion { index: 0, name: "'a" }) }), Lifetime(Region { kind: ReEarlyParam(EarlyParamRegion { index: 0, name: "'a" }) })], def_id: test_crate::sparse_transitions::{opaque#0} })
fn sparse_transitions<'a>() -> impl Iterator<Item = u8> + 'a {
core::iter::from_fn(move || { None })
}
Note, while this specifc snppet mentions EarlyParamRegion, this does not seem due to a lack of support for them. Other code snippets also fail with args such as Lifetime(Region { kind: ReErased }