Never types and inference

language design
24

One problem is that traits that don’t themselves cause paradoxes, like:

trait Innocent {
    type Assoc;
}

…can be referenced by other things that do, such as this:

struct Iffy<T: Innocent> {
    val: <T as Innocent>::Assoc
}

Or, if we change the trait slightly:

trait Funky {
    fn funk(&self);
}
trait Innocent { // still looks innocent
    type Assoc: Default + Funky;
}

…this:

pub fn foo<T: Innocent>() {
    let x: T::Assoc = Default::default();
    x.funk(); // what should this do?
}

You could say, “just don’t allow Iffy<!> or foo<!> to be instantiated”. But it doesn’t have to be a concrete instantiation; it could be buried inside a number of other instantiations.

Well, those examples don’t necessarily show unsoundness, just places the compiler could get stuck and perhaps produce instantiation-time errors. But how about this, using the typemap crate:

// crate A:
trait Innocent: Any {
    type Assoc: Any;
}

pub struct MyKey<T>(T);
impl<T: Innocent> typemap::Key for MyKey<T> {
    type Value = <T as Innocent>::Assoc;
}

// crate B (depends on A):
pub fn set(map: &mut typemap::TypeMap, val: u32) {
    map.insert::<A::MyKey<!>>(val);
}

// crate C (depends on A):
pub fn get(map: &typemap::TypeMap) -> &String {
    map.get::<A::MyKey<!>>().unwrap()
}

// crate D (depends on B, C):
fn huh() {
    let map = typemap::TypeMap::new();
    B::set(&mut map, 42);
    let s: &String = C::get(&map); // ???
}

Finally, there’s an RFC to allow impls to be proven disjoint if they have bounds with disjoint associated types, i.e.

impl<T> Foo for T where T: Innocent<Assoc=i32> {
    // some impl
}
impl<T> Foo for T where T: Innocent<Assoc=i64> {
    // some other impl
}

That RFC was postponed rather than accepted, but only until chalk becomes a thing; it’s definitely a desirable feature to have eventually. But it’s broken if both impls can be selected for T = !.

I believe there actually is a form of reasoning that would soundly allow incoherent impls in general, including the implicit ones you’re proposing. There’s a reason I had to reach out to something weird like typemap to get unsoundness. But… it would be a pretty huge change and would have all sorts of limitations. (I could also just be wrong.) It might be interesting to explore someday in order to allow ‘local impls’… but not just for this.

3 Likes