rustc-chalk integration 2019-03-19

High level view

chalk-engine

  • Has some resident state
  • You can submit a goal to try to prove
  • It will give you back an iterator — it’s lazy
  • Each time you  ask for an answer, it will do a minimum amount  of computation to get it
  • Maintains a “table” — one per “canonical goal” — which holds the answers so far
  • This acts as a cache
  • Answers look like an assignment of known inference variables
  • e.g. if you ask Vec<?T>: Debug you get a stream of answers, e.g.
  • yes if ?T = i32
  • yes if ?T = u32
  • etc — it’s an infinite stream
  • When you ask for the “next answer”, you can sometimes end up with a recursive reference to an answer
  • e.g. Vec<?T>: Debug could lead to ?T = Vec<$0> and recurs
  • The table also maintains a list of “strands”
  • A kind of co-routine
  • Basically “in progress” answers
  • When  you first create a table, you have no answers, but you do have strands
  • Roughly corresponding to the set of initial impls
  • Must be some superset of applicable program clauses — you want to filter based on the goal
  • This is often a coarse filter, e.g. on top-level Self type
  • These initial strands are populated via a callback
  • Largely tries to treat the objects it deals with abstractly (i.e. through associated types)

“Trait engine” i.e. FulfillmentContext in rustc

  • We’re in the process of typechecking in rustc
  • As we do so, we may arrive at a goal like SomeType: SomeTrait, which is placed into the current goal list
  • At any time, we can go through the list of goals and try to prove them
  • When we do so, we first canonicalize the goal
  • This is where we have a rustc query — right outside the aggregator
  • There’s a shim —  the aggregator — that sits between rustc and chalk-engine
  • This shim is what pulls on the answer iterators from chalk-engine and will continue until no further progress is possible
  • Either we’ve seen all the answers, or we’ve generalized the result such that we know no further answers could change the result (at most general, we learn nothing about the inference variables)
  • It can call back into chalk-engine and ask “does every remaining answer look like X?”
  • Tries to produce a maximally precise substitution for the inference variables 
  • If all the input types are known,  then the answer from the aggregator is just “yes” or “no”

  • TraitEngine is a trait in rustc — what the typechecker needs from the fulfillment context
  • Implemented by both old trait system and chalk integration (see chalk_fulfill.rs)

Inference context

  • Arrive at a goal like Vec<?32>: Debug
  • Passes goal to the trait engine, which maintains a handle back to the inference context

Concerns with current design

  • Because of things like Sized bounds, it can be very common to yield an answer “unknown”
  • e.g. forall<T> Foo for Vec<T> before we know that T is Sized we can’t say much
  • But we can perhaps at least yield that it must be a Vec, even if we’re not sure whether the implementation holds