--- title: INRIA presentation --- --- created: 2026-03-24 origin: null similar-to: null --- Bastian Kauschke lcnr (on github and everywhere else) they/he contact: lcnr@rust.de *my idea would be to rather quickly skim over the things that make Rust's type system interesting/hard, and then pick the things that are interesting to you or related to your work and dive more into them* *Even just explaining something with a new framing can often be very productive.* --- ```rust trait Trait { type Output; fn method() -> Self::Output; } impl Trait for u32 { type Output = bool; fn method() -> Self::Output { false } } struct Wrap(T); impl> Trait for Wrap { type Output = bool; fn method() -> Self::Output { !T::method() } } fn main() { assert!(Wrap::::method()); } ``` --- Rust is unsound https://github.com/orgs/rust-lang/projects/44/views/1 Rust has questionable limitations, e.g. ```rust fn expect_closure FnOnce(&'a str) -> usize>(x: F) {} fn foo() { // okay expect_closure(|string| string.len()); // not okay let x = |string| string.len(); expect_closure(x); // not okay_ signature: `for<'a> fn(&'a str) -> ?x let _unused = |string: &str| string; } ``` --- Rust allows arbitrary where-clauses ```rust trait Bound {} trait Project { type Assoc; } struct Foo { a: u32, b: Vec, c: T::Assoc, } impl Bound for Foo where T: Project, u32: Bound, Vec: Bound, T::Assoc: Bound, {} ``` Trait solving is turing complete. Handling/detecting divergence in Rust is fun :> one possible topic. --- We don't put any limits on the value of associated types, they can and do diverge. Detecting diverging definitions is best effort. ```rust trait Trait { type Assoc; } impl Trait for () { type Assoc = T::Assoc<()>; } impl Trait for u32 { type Assoc = u32; } fn main() { let _: <() as Trait>::Assoc; // `u32` let _: <() as Trait>::Assoc<()>; // diverges } ``` --- We can have bounds on associated types which we assume to hold in generic contexts ```rust trait Bound {} trait Trait { type Assoc: Bound; } fn impls_bound() {} fn foo() { impls_bound::(); } ``` This is currently unsound in combination with diverging associated types: github.com/rust-lang/rust/issues/135011. --- ### Coherence checking Rust guarantees that every trait bound can only be proven via at most one impl. Trait implementations do not overlap. Implicit negative coherence: for every possible overlapping instantiation, at least one of the where-clauses of one of the impls does not not! ```rust trait Bound {} impl Bound for u32 {} trait Trait {} impl Trait for T {} // 1 impl Trait for u32 {} // 2 impl Trait for i32 {} // 3 ``` Reasoning about compilation unit boundaries, guarantee that there is no overlap even with impls the current crate does not know about (sibling/downstream crates and impls considered acceptable to add to upstream crates) Orphan check limits what can be implemented in downtream crates: ```rust trait Trait {} struct UpstreamType; // in another crate impl Trait for UpstreamType {} // ERROR ``` Trait solving during the overlap check considers trait bounds for which an impl may pass the orphan check in a downstream crate to be ambiguous: ```rust trait Bound {} trait Trait {} impl, U> Trait for T {} impl Trait for T {} // Considered overlapping, downstream may add `impl Bound for LocalTy` ``` Trait solving must never incorrectly fail to prove something during the overlap check. Had multiple bugs where this happened when unnecessarily constraining inference variables --- Free lifetimes must not impact the output of of the trait solver `>::Assoc` and `>:Assoc` have to use the same trait implementation. Higher ranked lifetimes do impact trait selection. ```rust trait Trait {} // No way to have separate impls like this // - they always overlap // - relied on by codegen which does not have any knowledge about // free regions, they are all erased impl<'a> Trait for &'a u32 {} impl Trait for &'static u32 {} // These two do not overlap and can have different methods/associated types impl Trait for for<'a> fn(&'a u32) {} impl Trait for fn(&'static u32) {} ``` --- We don't have variadic generics, I would like us to have them :3 we have n-ary tuple and function types and they are a pain, e.g. https://docs.rs/bevy/latest/bevy/prelude/trait.SystemParamFunction.html#implementors --- We have higher-ranked types and where-clauses ```rust trait Trait {} fn foo<'a, T>() where // for all `'b` T: for<'b> Trait<&'b ()>, // for all `'c` which are shorter than `'a` T: for<'c> Trait<&'c &'a ()>, ``` - they do not universally quantify over all values, only over a subset of values which satisfy some "implied bounds" - we do not track these bounds explicitly - there are like 10.000 ways to avoid proving them, causing introducing unsoundness https://github.com/rust-lang/rust/issues/25860 https://github.com/rust-lang/rust/issues/129005 https://github.com/rust-lang/rust/issues/84533 - A few months ago we finally started to work to explicitly prove (and assume) these bounds on higher-ranked lifetimes While we're here https://github.com/stedolan/counterexamples / https://counterexamples.org/nearly-universal.html --- Planning to add higher-kinded inference variables to Rust in the next few weeks/months - why: opaque types - interesting: functions to lifetimes are trivial (has to be one of the arguments or `'static`) - normalization - our type inference sucks for closures `|x: &str| x;` does not compile :3 --- Privacy and types with invariants not enforced by the type system but by invariants on their constructors - subtyping of higher-ranked types *can* impact trait selection, breaking these invariants https://github.com/rust-lang/rust/issues/134407 - supporting such types as generic parameters (const generics) means higher-kinded inference is very easily unsound https://github.com/rust-lang/rust/issues/142239 --- Having a separate type for (capturing) lambdas sucks and requires a lot of weird special-cases and so on github.com/rust-lang/rust/issues/84366 https://github.com/rust-lang/rust/issues/153140 --- We have had, have, and will have, a bunch of issues with builtin implementations - https://github.com/rust-lang/rust/issues/57893 - https://github.com/rust-lang/rust/issues/141713 - https://github.com/rust-lang/rust/issues/152607 --- The trait solver allows cyclic reasoning - `List: Send` - ofc we also have unsound cyclic reasoning https://github.com/rust-lang/rust/issues/135246 --- Substructural types: already affine, may want to add linear types (via a a new `Forget` trait), mainly perf issues when enforcing this via trait bounds.