---
# System prepended metadata

title: Solver Deep Dive Outline

---

# Solver Deep Dive Outline

Target audience: types team members/experienced contributors

## User Facing API

- trait solving: just use an `ObligationCtxt` as before
    - Mention the subtlety around using fulfillment in the old solver, that's no longer a blocker
    - Discouraged using `evaluate_predicate` + friends (`predicate_must_hold_modulo_regions`, etc)
- Typing modes (https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/type.TypingMode.html)
    - We use them to tweak behavior in the solver
    - generally shouldn't add new ones :< impacts caching, makes reasoning about correctness harder
    - users should generally use the existing `TypingEnv` they are within, e.g.
        - stored in `InferCtxt` in most cases
        - also, `.typing_env()` in `LateContext` and `HasTypingEnv` during codegen
        - stored in MIR body (careful during phase transitions :<)
    - used by coherence to deal with unknown impls and avoid incomplete inference
    - used to change the way we handle opaques
        - define modulo regions `Analysis` mode
        - define them in considering regions in `Borrowck` mode
        - reveal only ones from the current body in `PostBorrowck` mode
        - reveal all in `PostAnalysis` mode
        - generally do not use non-canonical caching/queries in `Analysis` and `Borrowck` mode. these do not track the `opaque_type_storage`
    - also impacts specialization :<

(lcnr above, errs below?)

- normalization :angel: (https://rustc-dev-guide.rust-lang.org/normalization.html#what-is-normalization)
    - Relating types doesn't need normalization first
    - we automatically normalize when generalizing types (u shouldn't rely on that)
    - Before you match on `.kind()`, call `structurally_normalize_*`
    - Where we expect things to already be normalized
        - Writeback results (writeback explicitly normalizes)
        - Types in the MIR body (pre-instantation)
            - still need to norm when doing field projects etc etc
    - Deeply normalizing
        - `.deeply_normalize` "in the type system"
            - assumes that the normalziation won't be ambiguous
                - necessary to properly normalize hr aliases (old solver doesn't :3)
            - Though think deeply about whether the type really needs deep normalization
            - `deeply_normalize_for_diagnostics` for when a type just needs to be simplified for displaying reasons
        - `.normalize_erasing_regions` generally only in "codegen", though you should be careful about using this
- Proof tree visitors
    - what are they, how do they work, they have worse caching, need to be careful
    - ideally shouldn't be used too much in the happy path
    - Example of a few:
        - Closure inference
        - Select
        - Diagnostics

---

Other next-solver ideas:
* Revised walkthrough of proving a goal
* How to add a new built-in trait
* search_graph
* canonicalization in-depth

Other types team ideas:
* Coercions redo?
* generalization
