--- title: "T-types roadmap 2024" tags: T-types, 2023-meetup-BRU, minutes date: 2023-10-10 / 2023-10-11 url: https://hackmd.io/hqjun2xuRQmtBcCps-bAnA --- # types team 2024 roadmap ```mermaid flowchart LR subgraph Edition2024 RPITLifetimeCaptureRules[" \n\nowner: TC/errs"] WeakTypeAliases["Changing type aliases to be weak\n\nowner: (lang)"] end subgraph EOY2024 NewSolverEverywhere["Use the new trait solver in all the places\n\nowner: lcnr"] NegativeImpls["Support negative impls in coherence\n\nowner: niko"] PoloniusStable["Location-sensitive polonius\n\nowner: lqd"] end subgraph HeatDeath UnlimiTAITed Coinduction Fix25860 ImpliedBounds BeautifulGat PerfectDerive FixOrSettle41756["Address how reordering where clauses can change behavior"] ExistentialLifetimes["more usable RPIT via existential lifetimes"] end subgraph Early2024 ModelCoherenceInFormality["Model coherence in formality\n\nowner: nikomatsakis"] NormalizeInOrphanCheck["Normalize in orphan check\n\nowner: lcnr"] NewSolverInCoherence["New solver in coherence\n\nowner: lcnr"] ImprovedOutlivesWithOpaqueBounds["`-> impl Trait + 'static` is ok even if it captures\n\nowner: errs"] MinTAITs["Minimal version of TAITs\n\nowner: oli, TC for prose, fallback to errs"] PoloniusPrototype["Prototype of Polonius\n\nowner: lqd"] DynUpcasting["Dyn upcasting\n\nowner: lcnr"] end Early2024 -.- Edition2024 Edition2024 -.- EOY2024 EOY2024 -.- HeatDeath NewSolverInCoherence --> NewSolverEverywhere NormalizeInOrphanCheck --> WeakTypeAliases MinTAITs --> RPITLifetimeCaptureRules MinTAITs --> UnlimiTAITed PoloniusPrototype --> PoloniusStable ImprovedOutlivesWithOpaqueBounds --> ExistentialLifetimes NewSolverEverywhere --> Coinduction NewSolverEverywhere --> UnlimiTAITed ModelCoherenceInFormality --> NewSolverInCoherence Coinduction --> ImpliedBounds ImpliedBounds --> BeautifulGat Coinduction --> Fix25860 linkStyle 0 stroke-width:0px linkStyle 1 stroke-width:0px linkStyle 2 stroke-width:0px ``` * New solver * coherence (early 2024) * possible additional partial stabilizations (by EOY 2024) * MIR! validation and/or MIR typeck * `fn codegen_select_candidate` * replace evaluate * item WF check * all but HIR typeck seems feasible * "Minimal version of TAITs" -- no edition interaction * Open question: what are the use cases we really want? * What are the restrictions we have to enforce to feel comfortable? * [Weak type aliases for Edition 2024](https://hackmd.io/hnJkp_ZdT6aVUu-7piUdsQ) * need to be done mid-year * definitely requires edition change * requires: Normalize before orphan check so that we can impl on type aliases * main implementor: fmease * Polonius stable on nightly :) * a-mir-formality ?? * what is the right best goal? * fuzzing? * Existential lifetimes ?? Not on roadmap: * Stabilize negative impls ? * GAT implied bounds / RTN on old solver?? * Perfect derives / coinductive traits ?? ## unsoundness https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Aopen+label%3AI-unsound+label%3AT-types Last year: https://hackmd.io/nNC_Z6nVSpW-ANkpJdSgpg?both (https://i.imgur.com/1zqc2pc.jpg) - https://github.com/rust-lang/rust/issues/114936 - requires a simple change in mir typeck - https://github.com/rust-lang/rust/issues/114728 - fixed by https://github.com/rust-lang/rust/pull/115008, oli to summarize + FCP :heavy_check_mark: - https://github.com/rust-lang/rust/issues/114061 - New solver in coherence - https://github.com/rust-lang/rust/issues/112905 - lcnr has no idea - started as of [#95474](https://github.com/rust-lang/rust/pull/95474), but [oli's comment seems correct](https://github.com/rust-lang/rust/pull/95474#issuecomment-1090199898) - see discussion at the end of the doc - https://github.com/rust-lang/rust/issues/112417 - fix by erroring on RPIT in dead code: oli - https://github.com/rust-lang/rust/issues/109387 - :shrug: unclear whether 'actually' unsound :shrug: - https://github.com/rust-lang/rust/issues/105787 - New solver in coherence - https://github.com/rust-lang/rust/issues/105295 - future compat linted https://github.com/rust-lang/rust/issues/105572 - https://github.com/rust-lang/rust/issues/104005 - WIP work in https://github.com/rust-lang/rust/pull/104098, stalled - https://github.com/rust-lang/rust/issues/102048 - New solver in coherence - https://github.com/rust-lang/rust/issues/100051 - implied bounds - https://github.com/rust-lang/rust/issues/100041 - implied bounds - https://github.com/rust-lang/rust/issues/99554 - NormalizeInOrphanCheck - https://github.com/rust-lang/rust/issues/98117 - coinduction? - https://github.com/rust-lang/rust/issues/97156 - needs work, crater run - https://github.com/rust-lang/rust/issues/85099 - needs work, has `E-mentor` tag - https://github.com/rust-lang/rust/issues/84591 - could be partially fixed rn https://github.com/rust-lang/rust/issues/84591#issuecomment-1171381753 - the higher ranked case required (implied) where bounds on binders - https://github.com/rust-lang/rust/issues/84533 - mostly fixed by https://github.com/rust-lang/rust/pull/115538 which is stalled - clean fix requires (implied) where bounds on binders - https://github.com/rust-lang/rust/issues/84366 - complex, needs design and feature work, had multiple types team meetings - https://github.com/rust-lang/rust/issues/80176 - future compat linted https://github.com/rust-lang/rust/issues/105572 - https://github.com/rust-lang/rust/issues/57893 - needs summary + design work - https://github.com/rust-lang/rust/issues/50781 - has future compat lint, unsure of status, needs summary? - https://github.com/rust-lang/rust/issues/49206 - unclear? how do you exploit his for unsoundness? Followup: Niko and Jack to put together an initial draft of unsoundess on a roadmap # niko digresses onto a question around outlives This used to be true: `fn(&'a u32): 'static` But we wanted `T::Item: 'x` if `T: 'x` and... ```rust impl<'a> Trait for fn(&'a u32) { type Item = &'a u32; } ``` But we could say that if a lifetime is used in contravariant position then it's not constrained. I wish we could change the current behavior. If we could do this, doing it over an edition might be the way. It would be nice if `T: 'static` would always mean that `T` doesn't contain any data by reference. This is related to: -- Rust allows impl Fn(T<'a>) -> T<'b> to be : 'static, which is unsound [#112905](https://github.com/rust-lang/rust/issues/112905) Issue with `TypeId`: `fn(&'a u32): 'static` means you can convert `Box<fn(&'a u32)>` to `Box<dyn Any>`, downcast to `Box<fn(&'static u32)>`. ## playing with 112905 https://github.com/rust-lang/rust/issues/112905 The heart of 112905 is leverage the dyn trait loophole to convert a... ```rust type F<'a, 'b> = impl 'static + Fn(T<'a>) -> T<'b>; ``` `F<'a, 'b>` to `F<'a, 'static>`. Which lets you call the function and convert anything into `'static`. ```rust type F<'a, 'b> = impl 'static + Fn(T<'a>, &mut T<'b>); ``` Suppose we had an explicit notation: ```rust type F<'a, 'b> = impl<'a, 'b> 'static + Fn(T<'a>, &mut T<'b>); ``` what if the type were ```rust type G<'a, 'b> = impl<'a, 'b> 'static; ``` is *that* a soundness hole? It IS possible to have ```rust mod boundary { type G<'a, 'b> = impl<'a, 'b> 'static; fn get<'a>(x: &'a u32) -> G<'a, 'a> { () // <-- is there a hidden type here that is unsound } fn take<'a, 'b>(g: G<'a, 'b>) { // ...given that caller may change 'a and 'b arbitrarily here } } fn caller<'x>(x: &'x u32) { let g0: boundary::G<'x, 'x> = get(x); let g1: boundary::G<'x, 'static> = dyn_trick(g0); boudary::take(g1); // but...so what?? } fn dyn_trick<T, U>(t: T) -> U where T: 'static, U: 'static, { let x: Box<dyn Any> = Box::new(t); *x.downcast::<U>().unwrap() } ``` Another view of #112905 is that, in this code... ```rust #![feature(type_alias_impl_trait)] struct T<'x>(&'x ()); type F<'a, 'b> = impl 'static + Fn(T<'a>) -> T<'b>; fn helper<'a, 'b>(_: [&'b &'a (); 0]) -> F<'a, 'b> { // Why does this compile? Because of an implied bound // `where `'a: 'b` (which could well have been explicit); // that relationship is required to make the hidden type // well-formed, but we lose it when |x: T<'a>| -> T<'b> { x } // this should *not* be `: 'static` } ``` ```rust #![feature(type_alias_impl_trait)] struct Foo<T: Ord> { t: T } type FooAlias<T> = impl std::fmt::Debug; fn foo<T: Ord>(t: T) -> FooAlias<T> { Foo::<T> { t } } ``` https://play.rust-lang.org/?version=nightly&mode=debug&edition=2021&gist=dc541ebd1502a24cc3885a63ac8c83ce Writing the implied `where 'a: 'b` bound correctly gives you this error: https://play.rust-lang.org/?version=nightly&mode=debug&edition=2021&gist=4a1f612ca7b8c76b3b7795ea4242be14 message: ``` error[E0478]: lifetime bound not satisfied --> src/main.rs:9:18 | 9 | type F<'a, 'b> = impl Any + Fn(T<'a>) -> T<'b>; | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | note: lifetime parameter instantiated with the lifetime `'a` as defined here --> src/main.rs:9:8 | 9 | type F<'a, 'b> = impl Any + Fn(T<'a>) -> T<'b>; | ^^ note: but lifetime parameter must outlive the lifetime `'b` as defined here --> src/main.rs:9:12 | 9 | type F<'a, 'b> = impl Any + Fn(T<'a>) -> T<'b>; | ^^ ``` [will not compile](https://play.rust-lang.org/?version=nightly&mode=debug&edition=2021&gist=2ec2196db483bf83b4d21c34dc46c070) ```rust #![forbid(unsafe_code)] // No `unsafe!` #![feature(type_alias_impl_trait)] use core::any::Any; /// Anything covariant will do, for this demo. type T<'lt> = &'lt str; type F<'a, 'b> where 'a: 'b = impl Any + Fn(T<'a>) -> T<'b>; fn helper<'a, 'b>(_: [&'b &'a (); 0]) -> F<'a, 'b> where 'a: 'b { // <-- the change |x: T<'a>| -> T<'b> { x } } fn exploit<'a, 'b>(a: T<'a>) -> T<'b> { let f: F<'a, 'a> = helper([]); let any = Box::new(f) as Box<dyn Any>; let f: F<'a, 'static> = *any.downcast().unwrap(); f(a) } fn main() { let r: T<'static> = { let local = String::from("..."); exploit(&local) }; // Since `r` now dangles, we can easily make the use-after-free // point to newly allocated memory! let _unrelated = String::from("UAF"); dbg!(r); // may print `UAF`! Run with `miri` to see the UB. } ``` In summary... NM: Not convinced this bug blocks semantic `'static`. NM: Am convinced that our implied bounds rules need work. ## Fuzzing Resources: - [Universal Fuzzing via Large Language Models](https://arxiv.org/abs/2308.04748) - [Type Systems for the Masses: Deriving Soundness Proofs and Efficient Checkers](https://www.informatik.uni-marburg.de/~seba/publications/veritas-onward.pdf) - [A survey of compiler testing](https://software-lab.org/publications/csur2019_compiler_testing.pdf)