lcnr
commented
1 year ago 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.
Open lcnr opened 1 year ago
lcnr
commented
1 year ago 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.
lcnr
commented
1 year ago A proposed solution was to recheck the opaque for well-formedness with Reveal::All. This check probably still needs to handle region obligations as we can otherwise end up with unproven outlives bounds.
lcnr
commented
1 year ago 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.
This is surprisingly hard: taking the known issue for projections in the new solver https://github.com/lcnr/solver-woes/issues/9#issuecomment-1483510789, we instead overflow because instantiating Tait with String requires a nested String: Copy bound which we again prove using the alias bound on Tait, resulting in a cycle https://rust.godbolt.org/z/41cM1snx5
// 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()
}
passes cargo check and results in an ICE
``` error: internal compiler error: compiler/rustc_middle/src/ty/normalize_erasing_regions.rs:195:90: Failed to normalize fn() ->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 impl