---
# System prepended metadata

title: Chalk planning

---

# Chalk planning

## 2022-09-12

Niko jotting down some notes.

Key formality/chalk capabilities and ideas

```mermaid
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?

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

