alias bound candidates for opaques allow cyclic reasoning #109387
Comments
lcnr
added
A-typesystem
|
it's probably possible to get a segfault at runtime from this instead, but thinking about circular reasoning like this is hard so I am satisfied with an ICE for now. |
Noratrieb
added
the
T-compiler
|
A proposed solution was to recheck the opaque for well-formedness with |
This is surprisingly hard: taking the known issue for projections in the new solver lcnr/solver-woes#9 (comment), we instead overflow because instantiating // compile-flags: -Ztrait-solver=next
#![feature(type_alias_impl_trait)]
mod define {
pub type Tait where Tait: Copy = impl Copy;
fn define() -> Tait
where
Tait: Copy
{
String::new()
}
}
fn copy(x: &define::Tait) -> define::Tait {
*x
}using a coinductive trait currently also doesn't compile though I am unsure why https://rust.godbolt.org/z/xncdcecWY // compile-flags: -Ztrait-solver=next
#![feature(rustc_attrs, type_alias_impl_trait)]
#[rustc_coinductive]
trait Trait {
fn mk() -> Self;
}
mod define {
use super::*;
pub type Tait where Tait: Trait = impl Trait;
fn define() -> Tait
where
Tait: Trait
{}
}
fn make() -> define::Tait {
Trait::mk()
} |
lcnr
added
the
A-impl-trait
lcnr
changed the title
passes cargo check and results in an ICE
This has the same underlying reason as the unsoundness for super traits with coinduction and alias bound for projections. To my knowledge none of these issues are exploitable on stable right now though.
This relies on the following unsound circular reasoning:
Trait<T> for Trelies on the item boundTy<T>: Trait<T>Ty<T>(T) uses the implThe text was updated successfully, but these errors were encountered: