# Chalk planning

## 2022-09-12

Niko jotting down some notes.

Key formality/chalk capabilities and ideas

flowchart LR
  Implications 
  ExistsPredicates
  GeneralizedForAllPredicates
  HigherRankedInTraitSystem
  
  Implications --> ExistsPredicates 
  Implications --> GeneralizedForAllPredicates
  HigherRankedInTraitSystem --> Polonius
  Polonious

### Implications (`P => Q`)

Being able to introduce new facts into the environment.

Needed to support `exists<T>` goals as where-clauses. Also needed to prove the desired design for GAT implied bounds.

Introdues some complications. Have to be able to deal with things like `'a: 'b`.

### ForAll over anything

Generalizing forall beyond lifetimes. This is already *mostly* plumbed through rustc, I believe, in the form of placeholders.

### Exists where-clauses

Needed for properly modeling RPIT.

Easy with

## 2022-09-02

### OUTCOME

* coherence/specialization/wfcheck
* move these to a separate solver
* remove code from rustc solvers that is geared towards specialization
* convert some of the `select_all_or_error` to evaluate or queries today
* could enumerate a set of issues for these
* try to replace some of the ad-hoc logic with more logical logic

---

* chalk-ty library extraction
* can we extract the inference context and the operations on it?
* mir formality subtyping
* different type syntax
* richer types (forall T, T ensures P, P => T)
* simplesub <-- does this get us into trouble around `fn` types
* managing higher-ranked and outlives calculations <-- lcnr
* interaction of ty and goals

### biggest goals

* a lowering from Rust syntax into program clauses that controls trait matching
* a reusable library that encapsulates trait matching, type operations, etc
* query setup that allows you to solve constraints without affecting the existing environment

### Chalk deferred items

* Const eval
* SLG: associated type ambiguity
* Placeholder canonicalization
* Finishing touches on folder traits
* projections: ty -> term
* closure bug: https://github.com/rust-lang/chalk/issues/688
* Region constraints??
* Specialization
* Sem/syn equality? (not sure, needs thinking)
* early bound vs late bound

### A-mir-formality

* differences between chalk or rustc
* missing pieces:
* specialization
* TAITs

#### associated type normalization, a redive

#### implied bounds

### sem-syn equality

related developments:

* unsoundness-esque interaction with `TypeId` that lcnr found
* type alias work
* refinement traits

### diagnostics

* how many solvers
* do we want a separate diagnostic solver?

trait Foo {
    fn bar<T>(&self, t: T) -> T;   
}

<T as Foo>::bar::<u32>()
<T as Foo>::bar(&'a Self, u32)

Normalize(
    <?A as Foo>::bar::<'?x, ?B>(&'?x ?A, ?B),
    ?B,
)

### shallow subtyping

### rustc architecture

* env layer
* tracks
* placeholders
* inference variables
* unifications for inference variables (A := B)
* relations between inference variables (A <= B)
* trait solver proper ("logic layer" in mir-formality)
* `(Env, Goal) -> Solution`
* type relations code
* `(Env, Relation) -> (Env, Goals)`
* defines
* subtyping
* region-outlives
* ty-outlives
* coherence, wfcheck
* checking for overlap
* comparing impl against trait
* specialization
* uses a fresh fulfillment context to compute implication
* `compare_method`
* compare entailment of various kinds
* HIR WF Check
* walks the HIR and reports errors, pretty easy case, but does report errors
* check const
* const qualification
* TAITs
* check that hidden type is well-formed and meets its bounds
* rustdoc
* `AutoTraitFinder`
* borrow checker
* takes as input:
* MIR CFG
* type checker
* takes as input:
* MIR
* compute implied outlives bounds
* require_same_types from check_many_fn
* should be a query, but needs diagnostics
* `check_opaque_meets_bounds`
* part of typecheck, reports errors
* `can_type_implement_copy`
* probably can just be a call to evaluate
* other special traits
* e.g., `DispatchFromDyn`
* `implied_outlives_bounds`

#### creepy coercions

* `expected_inputs_for_output` -- part of coercion logic
* the "should coerce unsized" apply does some creepy stuff
* `can_coerce`
* autoderef loop
* doesn't really need to normalize at all, could just use `predicate_may_hold`

#### low-level methods and functions

* trans / codegen_fulfill_obligation
* should become normalization queries in the fullness of time
* `impossible_predicates`
* `type_known_to_meet_bound_modulo_regions`
* where is this used?? can we query it?
* `fully_normalize` -- can become a query or perhaps just invoke `type_meets_bound`
* `type_implements_fn_trait` -- error reporting, clearly a query
* `scrape_region_constraints` -- part of the complex NLL query region system

#### structural match

* `structural_match`

### rustc uses the trait solver..where?

* selection context
* coherence
* HIR type checker enqueues obligations
* MIR type checker
* query operations
* dropck
* evaluation
* method evaluation asks for evaluations to figure out which
* other weird things