Java and Scala's type system is unsound -- Lessons for Rust?

(I hope this is not entirely off-topic, please tell me if I’m wrong about this.)

I think this paper is an interesting read for anyone interested in type system design: https://raw.githubusercontent.com/namin/unsound/master/doc/unsound-oopsla16.pdf The Java and Scala type system turned out to be unsound (and I am not talking about the old, well-known issue of covariant array types).

Beyond the general “learn from other people’s mistakes”, I feel like Rust in particular has to be careful not to end up with similar issues. The issue in Java arises from the fact that the type checker assumes that types of in-context variables are well-formed in some sense, and it turns out there is a way to get around that invariant. This reminded me a lot of how Rust treats well-formedness, where e.g. the mere presence of a variable of type &'a &'b T already gives rise to lifetime constraints that the compiler will freely use. We’ve already seen a soundness bug caused by this implicitness, let’s be on the watch for similar issues.

1 Like

At least from my POV, Rust does not assume that the presence of types implies their well-formedness. Instead, the WF of a function’s argument types (and maybe the return type - this is currently implemented in an #25860-unsound way, but the jury is still out on the best way to resolve that) is treated as a predicate on the function (has to be proven by a caller and can be assumed by the callee).

This allows us to get away without having user-visible bounds on functions, but our type-checker is supposed to always be using the “elaborated” version.

Right, that's certainly how I prefer to see it. However, it was my understanding that the actual implementation in the compiler does not work this way; the caller does not check these implicit conditions on the call site -- instead it relies on the fact that since it has a value of the given type, the condition is already guaranteed to hold. Maybe that's outdated information?

The compiler basically has these rules:

Γ, WF(fn(τ) -> σ), x : τ ⊢ EXPR: σ
----------------------------------
Γ ⊢ fn(x) { EXPR } : fn(τ) -> σ

Γ ⊢ WF(fn(τ) -> σ), x : τ, f : fn(τ) -> σ
-----------------------------------------
Γ ⊢ f(x) : σ

Aka when checking a function calls, it adds wf obligations on the function's arguments and

Which (I'm quite sure are) sound by themselves, but are not sound in the presence of subtyping, because the supertype of the WF callee type might be non-WF by itself.

Note that ATM (unless we make the change of replacing the WF(fn(τ) -> σ) assumption with a WF(τ) assumption), no contravariance is required:

static S: &'static &'static u8 = &&0;

fn helper<'a, 'b>(x: &'a u8, _y: &'b u8) -> (&'b &'a u8, &'b u8) {
    (S, x)
}

pub fn coerce_lifetime<'x, 'y>(x: &'x u8) -> &'static u8 {
    let helper: for<'a, 'b> fn(&'a u8, &'b u8) -> (&'b &'a u8, &'b u8)
        = helper;
    let helper: for<'a> fn(&'a u8, &'static u8) -> (&'static &'a u8, &'static u8)
        = helper;
    let helper: for<'a> fn(&'a u8, &'static u8) -> (&'a &'a u8, &'static u8)
        = helper;
    helper(x, *S).1
}

This is the case at least since RFC #1214 landed (the pre-#1214 rules are totally crazy).

Note that typeck also checks WF in tons of random places, both to improve error messages and because trans does not like to see things such as structs with arrays in their middle etc, but the main place WF is required for soundness is because it is used as an assumption at call-sites.

3 Likes

The compiler basically has these rules:

Γ, WF(fn(τ) -> σ), x : τ ⊢ EXPR: σ
Γ ⊢ fn(x) { EXPR } : fn(τ) -> σ

Γ ⊢ WF(fn(τ) -> σ), x : τ, f : fn(τ) -> σ

Γ ⊢ f(x) : σ|

Aka when checking a function calls, it adds wf obligations on the function's arguments and

Which (I'm quite sure are) sound by themselves, but are not sound in the presence of subtyping, because the supertype of the WF callee type might be non-WF by itself.

I agree, these rules make perfect sense. We fix the subtyping problem in our formal development by essentially making the type fn(τ) -> σ syntactic sugar for "fn_internal(τ) -> σ where WF(fn(τ) -> σ)".

So you are saying that the compiler does not have a rule which works like "if I have &'a &'b τ in my context, then I can deduce that 'b : 'a"? Instead, the 'b : 'a is available in the context because it was added to the assumptions by the clause you mentioned above? That would be great.

That's our plan for the future too (aka after we finish unifying type inference and trait checking).

Yup. The compiler generally tries to enforces the converse - that if you have a type T "in your program", then T is well-formed. This is of course not needed for soundness except in the case of function calls, but is required in practice both for user-facing "consistency" and because we need to be able to compute the associated types even of fields that can't be accessed by our program.

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.