Thoughts on pattern types and subtyping

language design
18

Some thoughts on type inference with subtyping coercion.

In current Rust:

trait Trait {}
impl Trait for fn(&'static u8) {}

fn takes_concrete_supertype(_: fn(&'static u8)) {}
fn takes_impl_trait(_: impl Trait) {}

fn to_ptr<'a>(_: &'a u8) {}

fn main() {
   let fn_ptr: for<'a> fn(&'a u8) = to_ptr;

   // This works fine. Rust realizes it needs to convert `fn_ptr`
   // from a `for<'a> fn(&'a u8)` to the supertype `fn(&'static u8)`.
   takes_concrete_supertype(fn_ptr);

   // This doesn't compile today :(
   // Rust doesn't manage to coerce `fn_ptr` to supertype.
   takes_impl_trait(fn_ptr);
}

If a u32 in 1.. is to be as useful as a u32, code like the last line in the above example needs to compile. For Rust to be able to infer what to do, there needs to be a unique "best" supertype to coerce to to satisfy trait bounds. I would propose something like the following rules:

For any type T and trait Trait, one of the following two cases must hold:

  1. T implements Trait. In this case, if any of T's supertypes or subtypes also implement Trait, those impls must come from the same impl block as the impl of Trait for T. Additionally, if U is a supertype of T, and U does not implement Trait, then none of U's supertypes may implement Trait. If any of these rules is violated, it's a coherence error.

  2. T does not implement Trait. In this case, consider the set {U} of all supertypes of T that do implement Trait. One of the following must hold (otherwise, it's a coherence error):

    a) The described set {U} is empty

    b) All of the elements of {U} share a common subtype S, that itself implements Trait, and is a member of {U}.

In case 2b, when a value of type T is provided but a value of a type implementing Trait is expected, the value of type T is coerced to S.

I don't believe it's possible to write impls that would conflict with these rules in Rust today, without triggering the coherence_leak_check future-compat lint. But maybe I am wrong about that, please tell me if so!