Type System Documentation

[nikomatsakis]

Metadata
Point of contact	@BoxyUwU
Team(s)	types
Goal document	2025h2/typesystem-docs

Summary

Improve documentation of type system components to aide in types team onboarding and communication about changes to the type system .

Tasks and status

• Discussion and moral support (types )
• Triage Analysis Chapter (@BoxyUwU)
• Const Generics Documentation (@BoxyUwU)
• New Solver Documentation (@BoxyUwU, @lcnr)

[nikomatsakis]

This issue is intended for status updates only.

For general questions or comments, please contact the owner(s) directly.

[BoxyUwU]

A bit late on this update but I've sat down with @lcnr a little while back and we tried to come up with a list of topics that we felt fell under type system documentation. This is an entirely unordered list and some topics may already be adequately covered in the dev guide already.

Regardless this effectively serves as a "shiny future" for everything I'd like to have documentation about somewhere (be it dev guide or in-tree module level documentation):

• opaque types
  • non defining vs defining uses
  • member constraints (borrowck overlap)
  • checking item bounds
  • high level normalization/opaque type storage approach (new solver)
  • normalization incompleteness
  • method/function incompleteness
  • how does use<...> work
  • 'erased regions causes problems with outlives item bounds in liveness
  • consistency across defining scopes
  • RPITIT inference? does this have special stuff
  • capturing of bound vars in opaques under binders, Fn bounds are somewhat special in relation to this
  • opaques inheriting late bound function parameters
• non opaque type, impl Trait
  • RPITIT in traits desugaring
  • impl Trait in bindings
  • APIT desugaring impl details
• const generics
  • anonymous constants
  • ConstArgHasType
  • TSVs vs RVs and generally upstream doc from lang meeting to dev guide
  • deterministic CTFE requirement
• HIR typeck
  • expectations (and how used incorrectly :3)
  • method lookup + assorted code cleanups
  • coercions
  • auto-deref/reborrows (in coercions/method selection)
  • closure signature inference
  • fudge_inference_if_ok :>
  • diverging block handling :3
  • fallback :3
• MIR borrowck
  • MIR typeck
    • why do we want two typecks
    • region dependent goals in new solver (interaction with lack-of region uniquification)
  • overlaps with opaque types
  • compute region graph
  • closure requirements
  • borrowck proper
• compare predicate entailment :>
  • param env jank
  • implied bounds handling
• trait objects: recent FCPs :3
  • dyn compatibility soundness interactions (see coerce pointee/arbitrary self types stuff)
  • dyn compatibility for impl reasons (monomorphization)
  • projection bounds handling
  • args not required for wf
• ty::Infer in ty overview
• generalization
• coroutines
  • deferred coroutine obligations
  • witness types?
  • why -Zhigher-ranked-assumptions exists
• binders and universes existsA forallB A == B
  • build more of an intuition than current docs :thinking_face:
• talk about hr implied bounds there/be more explicit/clear in https://rustc-dev-guide.rust-lang.org/traits/implied-bounds.html?highlight=implied#proving-implicit-implied-bounds
• incompleteness
  • what is it
  • what kinds are OK (not entirely sure yet. small explanation and add a note)
• trait solving
  • cycles
  • general overview of how trait solving works as a concept (probably with example and handwritten proof trees)
    • important: first go "prove stuff by recursively proving nested requirements", then later introduce candidates
    • clauses/predicates
  • running pending goals in a loop
  • what kinds of incompleteness (overlap with opaques)
  • builtin impls and how to add them
• hir to ty lowering :>
  • itemctxt vs fnctxt behaviours
  • normalization in lowering
  • lowering should be lossy
  • idempotency(?)
  • cycles from param env construction
  • const generics jank about Self and no generic parameters allowed
• well formedness checking + wf disambiguation page
• normalization & aliases
  • be more clear about normalizing ambig aliases to infer vars :thinking_face:
  • normalize when equating infer vars with aliases (overlap with generalization?)
  • item bounds checking
  • interactions with implied bounds (overlap with implied bounds and hir ty lowering)
• variance

Since making this list I've started working on writing documentation about coercions/adjustments. So far this has mostly resulted in spending a lot of time reading the relevant code in rustc. I've discovered a few bugs and inconsistencies in behaviour and made some nice code cleanups which should be valuable for people learning how coercions are implemented already. This can be seen in #147565

I intend to start actually writing stuff in the dev guide for coercions/adjustments now as that PR is almost done.

I also intend to use a zulip thread (#t-compiler/rustc-dev-guide > Type System Docs Rewrite) for more "lightweight" and informal updates on this project goal, as well as just miscellaneous discussion about work relating to this project goal