# Types team 2023 roadmap deep dive

## Major goals

* Building a platform that can scale to the new features we will need
* Sound, testable, documented type system
* Sustainable open-source team to maintain this

## Strategy over the next year years

### Zero soundness bugs
* 2023: Develop key tools we need to solve hard bugs: new trait solver, formality. Consider lints.
* 2024: Finalize trait solver, begin improving type system.
* 2025-2026: Fix and close all open issues. Any remaining issues are top priority to fix as they are opened.

### Model that is tested against rustc, fuzz tested, plus has a soundness proof

* Status as of March 2023: Experimental repository
* 2023: Introduce mir-formality as official Rust repository: fuzzing support, ability to test against rustc test suite
* require modelling all new 'core typesystem features' in a mir-formality for stabilization
* 2024: Grow model by testing against Rust test suite, explore techniques for soundness proofs
* ...
* 2027: Profit (this plan will require some elaboration lol).

### Develop a new trait solver which can be maintained and extended

* Examples of extensions we know we'll need: implications, lazy normalization, local/global caching
* Status as of March 2023: Experimental support in rustc
* 2023: ship 1 component of rustc with new solver on stable (e.g., coherence), able to compile crates with medium complexity using an experimental flag, develop migration plan
* 2024: new trait solver used across rustc (in migration mode), at least for Rust 2024 code (and maybe other editions)
* 2025: complete migration

## Tenets

* Soundness
* fix easy things
* but the main ones that are hard are hard because we need a better type sytem to be able to fix them in a satisfactory way
* unless we think that there is a high chance of people writing broken code, I would rather we prioritize fixing them non-disruptively

## Big graph

flowchart TD
    subgraph 2023
        MirFormalityRfc
        TraitSolverNightly
    end
    
    subgraph 2024
        SoundnessInitiative
    end
    
    Soundness["Zero soundness bugs"]
    EaseOfUse["Expressivenss and core Rust ease of use"]
    
    MirFormalityRfc --> MirFormality
    TraitSolverNightly --> TraitSolver
    
    SoundnessInitiative --> Soundness
    
    TraitSolver
    MirFormality
    MirFormality --> Soundness
    TraitSolver --> Soundness
    
    Polonius --> EaseOfUse

    TAIT --> EaseOfUse
    
    Aliases --> EaseOfUse
    
    TraitSolver --> ExpandedImpliedBounds
    ExpandedImpliedBounds --> EaseOfUse
    
    GATImpliedBounds --> EaseOfUse
    
    EaseOfUse

## EOY 2023: New foundations designed and in initial use

- New trait solver replaces evaluate, but not used everywhere
- Onboarding plan and documentation for new trait solver
- MIR Formality integrated into language design process

**Trait solver.**

**a-mir-formality.** TODO ()

**Polonius.** TODO (lqd)

## EOY 2024: New foundations shipped and shared

**Soundness initiative begins.**

**GAT things?** TODO

- New trait solver shared by rustc and rust-analyzer
- milestone: type-ir used by rustc/rust-analyzer
- Clean API for extensible trait errors / visualization
- at least available internally
- Shiny new features:
- Polonius
- GAT implied bounds
- impl trait every-dang-where
- Edition boundary things
- Trait changes e.g. opt-in dyn-ness
- Inference changes --
- make `Into` stop inferring?
- early-late interactions?

## EOY 2027: :euro: Profit :euro:

- (Types) I-unsound issues resolved :tada:
- Most extensions are easy to do; large extensions are feasible
- MIR Formality passes 99.9% of Rust test suite

## What do we want out of this meeting?

- Update of what has been happening?
- Where is the new trait solver?
- Edition boundary -- anything we want to do?

## Roadmap proposal

### 2023

**TAIT.**

### 2024

### 2027