---
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

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...

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...

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`.

type F<'a, 'b> = impl 'static + Fn(T<'a>, &mut T<'b>);

Suppose we had an explicit notation:

type F<'a, 'b> = impl<'a, 'b> 'static + Fn(T<'a>, &mut T<'b>);

what if the type were

type G<'a, 'b> = impl<'a, 'b> 'static;

is *that* a soundness hole? It IS possible to have

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...

#![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`
}

#![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)

#![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)