Borrow checking without lifetimes and specialization soundness

compiler traits working group
1

After reading a blog post borrow checking without lifetimes it made me wonder whether this could be a solution to the specialization unsoundness issue.

For example in shipping specialization: a story of soundness the author describes the classical example of why specialization is unsound:

trait Bomb {
    type Assoc: Default;
}

impl<T> Bomb for T {
    default type Assoc = ();
}

impl Bomb for &'static str {
    type Assoc = String;
}

fn build<T: Bomb>(t: T) -> T::Assoc {
    T::Assoc::default()
}

fn main() {
    let s: String = build("Uh oh");
    drop(s) // typeck and trans disagree about the type of `s`
}

The core of the issue is that different parts of the compiler disagree on which impl to use because of the ambiguity of lifetimes.

  1. The Conflict: When you call build("Uh oh"), the compiler sees the input has the type &'static str. It has two potential impls of Bomb it could use:
  • The generic impl<T> Bomb for T, where T would be &'static str.
  • The specialized impl Bomb for &'static str.
  1. The Ambiguity: The rules of specialization say to pick the most specific implementation. The compiler's type checker can see that impl Bomb for &'static str is more specific and correctly deduces that T::Assoc should be String.
  2. The Disagreement (The Bug): However, the code generation part of the compiler gets confused. It sees the generic function build<T: Bomb> and has trouble proving that the specialization is always the right choice for the erased lifetime that a &'erased str has. The blanket impl covers &'a str for any 'a, while the specialized one is only for 'static. This lifetime erasure creates a soundness minefield. Unsure if it can safely commit to the specialization, it falls back to the most general, "safest" option: the blanket impl.

The proposed origin system solves this by making the borrow information a concrete and unambiguous part of the type itself, eliminating the abstract lifetime 'a that causes so much trouble.

Let's re-imagine the types using origins:

  • A string literal like "Uh oh" doesn't have an abstract 'static lifetime. It has a concrete origin pointing to the program's static data segment. Let's call this origin {'static_data}.
  • The type of "Uh oh" is now &{'static_data} str.

Now, let's look at the impls in this new lifetime system:

  1. Blanket impl: impl<T> Bomb for T (This remains the same).
  2. Specialized impl: impl Bomb for &{'static_data} str

When the compiler sees the call build("Uh oh"), the type of the input is unambiguously &{'static_data} str.

The trait solver now has a much simpler decision:

  • Does impl<T> Bomb for T match? Yes, T can be &{'static_data} str.
  • Does impl Bomb for &{'static_data} str match? Yes, it's an exact match.

Because &{'static_data} str is a specific, concrete type, it is undeniably more specific than the generic parameter T. There is no lifetime erasure to create confusion. Every part of the compiler, from the type checker to the code generator, agrees on the type. There is no ambiguity to cause a disagreement. The compiler can confidently select the specialized impl and know that T::Assoc is String throughout the entire compilation pipeline.

It seems that the mojo language has learnt its lesson from Rust and they are using origins concept for handling lifetimes as well.

I would appreciate if anyone can point out the flaw in the reasoning and explain why borrow checking with origins will not fix the unsoundness issue of specialization.

2

Currently Rust can be compiled without any borrow checker at all. The borrow checker is just a checker, like debug_assert, and doesn't affect semantics of the program. This is used by mrustc, and temporarily by GCC front-end project that don't support borrow checking. It's a nice property of the language. Apart from specialisation, it makes later code generation stages simpler.

It gives assurance that changing implementation details of the borrow checker can't break working programs. I'm not sure if this would still be possible if the lifetimes were part of the type system during monomorphisation.

Would having just 'static as a special case be enough? Or could there be ambiguities from 'a: 'b vs 'b: 'c somewhere?

3

well, you could try to specialize based on S<'a, 'b> with the specialized case being S<'c, 'c>, which means lifetime comparison with things other than 'static, so yes there are other ambiguities.

2 Likes