Skip to content

Implied bounds / well-formedness of references treats contravariant lifetimes the same as covariant #106431

Open
@Manishearth

Description

@Manishearth

Potentially related to #25860 . The issues seem related but the examples are pretty different so I figured I'd file this as separate.

I'm not yet sure if I can craft an actual self-contained soundness bug out of this, but it does cause a soundness bug in Yoke which relies on for<'a> working correctly: unicode-org/icu4x#2926. I have multiple potential fixes for the yoke issue, but it's worth at least noting.

TLDR: Rust currently correctly implies a 'inner: 'outer bound when you have &'outer &'inner _. It is also incorrectly implying this for &'outer fn(&'inner _)

The reduced example is as follows:

// A function that forces the closure to work for ALL lifetimes
// ... or does it?  };-)
fn attach<C, F>(cart: Box<C>, transform: F) where F: for<'all> FnOnce(&'all C) -> &'all str {
    // could call f(&cart);, etc
}

type Contra<'a> = fn(&'a ());

fn contra_shorter<'contra, 's: 'contra>(param_contra: Contra<'contra>, param_s: &'s str) {
    let contravariant_cart = Box::new(param_contra);
    attach(contravariant_cart, |_| param_s);
    
}

(playpen)

This should not compile. F requires the returned string to be valid for ALL lifetimes 'all, whereas we're returning a string of lifetime 's

This code is behaving the same as this code:

fn co_shorter<'co, 's: 'co>(param_co: &'co u8, param_s: &'s str) {
    let covariant_cart = Box::new(param_co);
    attach(covariant_cart, |_| param_s);
}

where the concrete type of F is for<'all> FnOnce(&'all &'co u8) -> &'all str, and well-formedness implies that 'all must be shorter than 'co, so you end up getting a 'co: 'all bound, and 's: 'co ends up giving us 's: 'all, so even though there is a for<'all>, the 'all is actually artificially restricted to being "for all shorter than 'co" and returning data of lifetime 's is valid there.

(the 's: 'co is actually not necessary for co_shorter() to compile, but it's easier to explain that way)


Basically, for &'outer Foo<'inner>, the implied bound probably should be:

  • For covariant Foo: 'inner: 'outer
  • For contravariant Foo: Nothing
  • For invariant Foo: 'inner: 'outer, or nothing

Basically the implied bound is safe when things are guaranteed to not be contravariant. It's actually fine to have the implied bound for e.g. the invariant case of &'outer Cell<'inner _>, because a cell is logically a tuple of a covariant getter and contravariant setter, and the setter implies no bounds but the getter can imply bounds.

This does give me some pause since typically we tend to believe that code that works on invariant types will also work on contravariant types, and here's a situation where it won't; so perhaps it's safer to also opt invariant lifetimes out of this. Idk.

Contravariant types could imply the bound 'outer: 'inner because function parameters can't live for less than the function does, but I'm not sure this implied bound is ever useful. Does lead to a nice symmetry though.

The Yoke bug (unicode-org/icu4x#2926) only shows up for contravariance due to how Yoke is structured. It's not clear to me that there's a way to write an unsafe abstraction that relies on for<'a> being truly universal where an implied bound coming from an invariant type may cause unsoundness. But I could be wrong.


A further exploration can be found in this code (playpen):

Show code
// A function that forces the closure to work for ALL lifetimes
// ... or does it?  };-)
fn attach<C, F>(cart: Box<C>, transform: F) where F: for<'all> FnOnce(&'all C) -> &'all str {
    // could call f(&cart);, etc
}

type Contra<'a> = fn(&'a ());


fn main() {
    // create a Box<&'a _> with a longer lifetime than s ('a_longer; where `'a_longer: 's`)
    let local_longer = vec![1,2,3,4];
    let covariant_cart_longer: Box<&'_ [u32]> = Box::new(&*local_longer);
    
    // let's say this has lifetime 's
    let s = String::from("hello");
    
    
    // Create a Box<Contra<'contra>>, contravariant over 'contra
    let contravariant_cart: Box<Contra<'_>> = Box::new((|_| ()) as Contra);
    
    
    // Create a Box<_> that is fully owned
    let owned = vec![1,2,3,4];
    let owned_cart = Box::new(owned);
    
    // create a Box<&'a _> with a shorter lifetime than s ('a_shorter, where `'s: 'a_shorter`)
    let local_shorter = vec![1,2,3,4];
    let covariant_cart_shorter: Box<&'_ [u32]> = Box::new(&*local_shorter);  
    


    // does not compile, &s cannot produce &'all str for ALL 'all
    //
    // attach(owned_cart, |_| &s); 



    // This does compile, because in the bounds for F, `&'all C` is `&'all &'a_longer [u32]`, which forces
    // 'all to be shorter than 'a_shorter due to well-formedness / implied bounds (`'a_shorter: 'all`), reducing the for<'all> in scope
    // which works just fine for &s since 's is longer than 'a_shorter (`'s: 'a_shorter`) implying that `'s: 'all`
    attach(covariant_cart_shorter, |_| &s);
    
    
    
    // Seems like it shouldn't work, because the reason from before doesn't seem apply: even if 'all is forced to be shorter than 'a_longer,
    // there is still a period of time where 'a_longer is valid but 's is not, so the closure shouldn't compile.
    //
    // However, rustc is smart! It knows that it can make it work by squeezing 'a_longer *until* it is shorter than 's (`'s: 'a_longer`), and then WF rules force
    // us back into 'all being short (`'a_longer: 'all`), which brings us back to the previous situation; `'s: 'all`
    attach(covariant_cart_longer, |_| &s);
    

    // works, but shouldn't. 'contra is being selected to be *something*, and that somehow impacts WFness enough to
    // restrict the range of the for<'all>
    //
    // Without knowing WF rules for functions for sure, the clear answer is that *if* there are WF rules for functions, they would apply outside-in, not inside-out,
    // i.e. &'all fn(&'contra) would restrict 'contra to live at least as long as 'all, not vice versa.
    // This is unhelpful for us since we still have compiling code where &'s str is somehow a valid `for<'all> &'all str`; we MUST restrict 'all somehow
    //
    // To poke at this further without the problem of rustc picking some lifetime for 'contra, let's give it a named lifetime in two methods below:
    attach(contravariant_cart, |_| &s);
    
}

// First let's just give it a named lifetime
fn contra_longer<'a>(param_contra: Contra<'a>) {
    let contravariant_cart = Box::new(param_contra);
    let s = String::from("hello");
    // doesn't work, &s cannot produce &'all str for ALL 'all
    // huzzah!
    // attach(contravariant_cart, |_| &s);
    
}

// Now let's give it *and* s named lifetimes, and say that 's lives at least as long as 'contra
fn contra_shorter<'contra, 's: 'contra>(param_contra: Contra<'contra>, param_s: &'s str) {
    let contravariant_cart = Box::new(param_contra);
    // ... does work, but shouldn't
    // this is the same behavior as that for covariant lifetimes, clearly
    // the WF rules are assuming covariance somehow;
    //
    // the previous function fails to compile because 's lives 
    // less than 'contra, so we have a case similar to that of `covariant_cart_shorter` but this time the
    // covariance cannot come to the rescue
    attach(contravariant_cart, |_| param_s);
    
}

The line attach(contravariant_cart, |_| &s); should not compile, nor should the function contra_shorter(). contra_longer() happens to correctly fail to compile because the same variance trick that saves covariant_cart_shorter does not apply here.

cc @pnkfelix @lcnr

Thanks to @workingjubilee for rubberducking this with me.

Metadata

Metadata

Assignees

No one assigned

    Labels

    A-docsArea: Documentation for any part of the project, including the compiler, standard library, and toolsA-type-systemArea: Type systemA-varianceArea: Variance (https://doc.rust-lang.org/nomicon/subtyping.html)T-compilerRelevant to the compiler team, which will review and decide on the PR/issue.T-typesRelevant to the types team, which will review and decide on the PR/issue.

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions