# Jack and Niko 1:1 time

## 2023-01-23

### POPL meeting with egg crate people

Option 1: use egg to replace ena, essentially, growing the ability to have `T = u32` and other such things. Have to modify unification procedure accordingly and have some sort of "saturate" step when you encounter projection types. Only have to saturate a projection type once.

Saturate(projection) =
Solve NormalizesTo(projection, ?T) and for each solution `?T` add `projection = ?T` to the egraph

Option 2: some sort of meta-trick-desugaring-thing that Niko didn't 100% understand, basically converting to a form of datalog.

### Lattice

* typical logic programming is all inputs `A(T0...Tn)`
* `A(T0..Tn) = V` where `V` is defined across a lattice
* lattice gives you a notion of a "minimal" and "maximal" solution

### Jack Huey explorations

* unifying variables and projection types
* https://rust-lang.zulipchat.com/#narrow/stream/362009-t-types.2Fetc.2Flazy-norm-strategems/topic/new.20strategy.20experimentation.20in.20Chalk/near/318424246

exists<T> {
  <MyClosure<fn() -> T> as FnOnce>::Output = T
}

### Why you don't want a maximal value

imagine this scenario

fn foo<T, U: ?Sized>()
where
    T: Iterator<Item = U>

`T::Item` normalizes to `U`, but we don't know that `U: Sized`...?

Option 1:

* Elaboration rule, if you know that `T::Item` normalizes to `U`, you can propagate the bounds

Does that suffice? If it comes from an impl, impl had to prove proj impls bounds based on its where clauses, and we had to prove its where clauses... so....

fn foo<'a, T>() where (&'a T): Iterator<Item = u32> {
  let _: fn(<&'a T as Iterator>::Item); // <- have implied bounds that T: 'a
  let _: if(WF(<&'a T as Iterator>::Item)) fn(<&'a T as Iterator>::Item); // <- have implied bounds that T: 'a
  let _: fn(u32); // <- no more implied bounds
  let _: for<'a, T> if<T: 'a> fn(u32);
}

"fallback" test:
https://github.com/rust-lang/chalk/blob/808257c76d5b112ad2a6d837984de3725f293dc2/tests/test/projection.rs#L57

a-mir-formality tests:
https://github.com/jackh726/a-mir-formality/commit/32c64480cfb40a8bf7c7d10f355c84047ac25949