---
tags: deep-dive
---

# Deep dive fun times

## 2023-11-06

lcnr: Been experimenting with the new `AliasRelate`, hit some interesting questions.

WIP PR: https://github.com/rust-lang/rust/pull/117278

basic idea: try to normalize both sides as much as possible and then relate the resulting types

old approach: one-step-normalize-lhs-to-rhs, one-step-normalize-rhs-to-lhs, args-relate

#### The issue discussed below, summarized:

- structurally equal aliases have to be semantically equal
- because of MIR borrowck: structurally equal aliases *modulo regions* have to be semantically equal *potentially resulting in region constraints*
- simply equating the generic arguments is incomplete and unsound in coherence as normalization could cause them to be unused

=> for aliases, whose normalization result in ambiguity or overflow, semantic equality is not idempotent, meaning that these 3 requirements cannot be all be satisfied.

---

https://github.com/rust-lang/trait-system-refactor-initiative/issues/74

https://hackmd.io/RxTOQYl9Tr2DM2tCNsfNtw#QUESTION-alias-relate-for-cyclic-aliases

> Given `T: Trait<Assoc = T::Assoc>`, should `<T as Trait>::Assoc == <T as Trait>::Assoc` hold?

the where bound can trivially proven, but is used by normalization https://github.com/rust-lang/trait-system-refactor-initiative/issues/1

pretty much: should "structurally equal" imply "semantically equal": YES

with `normalizes(lhs) == normalize(rhs)` for alias-relate in the new solver, it does not hold for
`<T as Trait>::Assoc == <T as Trait>::Assoc` given the where-bound `T: Trait<Assoc = T::Assoc>`.

three scenarios:

* `forall<T>` -- not well formec
* `forall<T> if (T: Trait)` -- on PR, works
* `forall<T> if (T: Trait<Assoc = T::Assoc>)` -- on PR, does not work
* why? normalization overflows

how MIR formality works

* normalization computes a *set* of equivalent spellings for A and B
* and looks for intersection between them
* I *think* what would happen is that normalizing with `T: Trait<Assoc = T::Assoc>` would eventually get inductive overflow
* but it would succeed because we always assume `T normalizes-to T` is an option

`<T as Trait<'a>>::Assoc == <T as Trait<'b>>::Assoc` given the where-bound `T: for<'c> Trait<'c, Assoc = <T as Trait<'c>::Assoc>`.

* the "non-normalizing" case now has non-trivial region constraints

This case is equivalent to the exact structurally equal case, because of MIR typeck.

HIR typeck tries

    let x: Invariant<<T as Trait<'a>>::Assoc> = mk();
    let y: Invariant<<T as Trait<'a>>::Assoc> = x;

^ this should compile.

we erase regions during mir building.

at the start of mir typeck we replace each instantance of these erased regions with a new **unique** region var

now checking the assignment requires `<T as Trait<'n>>::Assoc == <T as Trait<'m>>::Assoc`, which would still overflow ~> MIR typeck fails

@lcnr invariant: "structural equality modulo free regions has to imply semantic equality (potentially resulting in region constraints in the root)"

* `Vec<&'a u32>` and `Vec<&'b u32>` -- structurally equal modulo free regions, but not semantically equal?? -- addressed by adding "potentially resulting in region constraints"

@lcnr believes: with current WF types there is no alias-relate which keeps this invariant while being complete.

new WF rule: all aliases must either be rigid themselves or can be normalized to something that is.

impl<A, B> Foo for A
where
    A: Iterator,
    B: Foo<Bar = A::Item>, // this is ok because we can normalize to a rigid alias
{}

impl<A, B> Foo for A
where
    A: Iterator<Item = A::Item>,  // nikomatsakis thinks maybe OK, because syntactic equality has no constraints
    B: Foo<Bar = A::Item>,
{}

impl<'x, A, B> Foo for A
where
    A: IteratorLike<'x, Item = <A as IteratorLike<'x>>::Item>, // syntactic equality implies region constraints, fails above test for sure
    B: Foo<Bar = A::Item>, // this is ok because we can normalize to a rigid alias
{}

TAIT issue with this:
https://github.com/rust-lang/trait-system-refactor-initiative/issues/74 this program would be forbidden.

more explicitly...

#![feature(type_alias_impl_trait)]

type Tait<'a> = impl Sized;

#[defines(Tait)]
fn define<'a>(x: &'a ()) -> Tait<'a> {
    ()
}

#[defines(Tait)]
fn x<'a>(x: &'a (), t: Tait<'a>) -> Tait<'a> {
    t // Problem case!
}

nikomatsakis vaguely thinks it'd be ok to require...

#![feature(type_alias_impl_trait)]

type Tait<'a> = impl Sized;

fn define<'a>(x: &'a ()) -> Tait<'a> {
    ()
}

#[defines()] // explicit declaration
fn x<'a>(x: &'a (), t: Tait<'a>) -> Tait<'a> {
    t
}

...but this it not lang-team consensus.

Sub-question: to what extent can Rust infer when we could have been universally quantified over an inference variable (let-generalization) in the face of erased regions?

## 2023-10-30

Reviewing [this branch](https://github.com/nikomatsakis/a-mir-formality-ndm/blob/b9d77d1ec5c4eb7d12a8a8f5c4a679c10a35cf63/crates/formality-prove/src/prove/is_local.rs)

rename `prove_not_goal` to `disprove` and add some comments about how universal/existential works etc

Observation:

* `is_local_parameter` -- currently disables coherence-mode, that seems goofy, we want to do better, but how do we define "unambiguously true"
* write some tests about these rules and check how it works
* `not_downstream`

Examining alias types, ignoring normalization:

* `T::Item`
* could be downstream
* not known to be local
* `<MyType<T> as Iterator>::Item`
* could be downstream
* not known to be local
* `<u32 as Trait>::Foo`
* cannot be downstream
* not known to be local
* a-mir-formality doesn't handle this case (neither does rustc)

Good target to fuzz

* generate impls and compare rustc vs a-mir-formality
* how to focus on coherence?
* can we fuzz the orphan rules?
* e.g., check that the impls in a downstream crate cannot be instantiated with types in upstream crates
* or check for a trait with a single impl that is downstream and check that it cannot be instantiated for upstream types (as a starting point)
* fuzz for overlap
* generate pairs of impls
* use first impl to guide fuzzer to generate matching types
* and then check if they match the second impl
* or generate random types (that are not obviously wrong) and fuzz it against the second impl

More interesting eample:

* Neither impl is a subtype of the other but they have an intersection
* add an Example 2 that covers this case

Why do compute intersections with coherence mode? Create examples

* Normalization can introduce "unnecessary" constraints that are
* can we have an example where trying to prove the assumptions will result in *extra* constraints that we can use?
* would have to lean on the inference rules

trait Trait<T> {}

trait NegImpl {}

impl<T, U> Trait<U> for T
where
    (): ConstrainToU32<U>, // Needs to avoid the trait_ref_is_local check
{}

impl<T, U: NegImpl> Trait<U> for T {}


impl NegImpl for u32 {}

## 2023-09-11

Covering issues with the provisional cache https://github.com/rust-lang/trait-system-refactor-initiative/issues/54

broken test: https://github.com/rust-lang/rust/blob/68c2f5ba0ffb6f7f0724dd62c7562daa634caaec/tests/ui/traits/new-solver/cycles/inductive-not-on-stack.rs#L15-L25C22

Root goal A and two cycles

RESULT: rip out the provisional cache
* may add caches again in the future, caches are probably not fundamentally unusable
* need to cache the fact that X is only true if Y, instead of just assuming X is true
* store in prov result, saying whether there was an inductive or coinductive cycle further up the stack
* lots of complexity, ripping it out for now since it doesn't seem strictly necessary

caching roots of cycles and reusing it from other cycle participants is broken https://rust.godbolt.org/z/MoTrvjvY6

* lcnr explains, niko understands, oli doesn't :laughing:

cycle `A -> B -> A`: ideal: finish, then cache both the final result of `A` and `B`. This deosn't work because of query system reasons.

instead (previously): put only `A` into the global cache, dropping `B`. When proving `B` the next time, we access `A` from the cache, still avoiding having to reprove the whole cycle.

test in rust test suite https://github.com/rust-lang/rust/blob/master/tests/ui/traits/new-solver/cycles/coinduction/incompleteness-unstable-result.rs

## 2023-06-19

Plan: walk through some of the examples to compare/contrast how different solvers work.

- https://hackmd.io/N0rzMn94QZOfbaAVOl4f6A#2023-05-26

#### how the solvers work

trait Foo { }
impl Foo for () { }
impl<T: Foo> Foo for Option<T> { }
fn test<X: Foo>() { }
fn main() { test::<Option<()>>(); }

* 'evaluate':
* go from an obligation to a "yes/no/maybe" result, more or less

evaluate status quo

- entry point: [`evaluate_root_obligation`](https://github.com/rust-lang/rust/blob/18a6d911caba59605eb03db1452848a85d2e5879/compiler/rustc_trait_selection/src/traits/select/mod.rs#L524) with a goal `Option<()>: Foo`
- [`evaluate_predicate_recursively`](https://github.com/rust-lang/rust/blob/18a6d911caba59605eb03db1452848a85d2e5879/compiler/rustc_trait_selection/src/traits/select/mod.rs#LL629C19-L629C19) also called with `Option<()>: Foo`
- matches on `PredicateKind`, calls [`evaluate_trait_predicate_recursively`](https://github.com/rust-lang/rust/blob/18a6d911caba59605eb03db1452848a85d2e5879/compiler/rustc_trait_selection/src/traits/select/mod.rs#L995)
- calls [`evaluate_stack`](https://github.com/rust-lang/rust/blob/18a6d911caba59605eb03db1452848a85d2e5879/compiler/rustc_trait_selection/src/traits/select/mod.rs#L1045) which actually delegates to selection -> confirmation
- [`select_from_obligation`](https://github.com/rust-lang/rust/blob/18a6d911caba59605eb03db1452848a85d2e5879/compiler/rustc_trait_selection/src/traits/select/mod.rs#L306): compute a single candidate which should be used to prove the obligation, here this is an `ImplCandidate`
- confirm: apply the constraints and "nested obligations" of that candidate
- nested obligations include `(): Foo` which is proven via [`evaluate_predicate_recursively`](https://github.com/rust-lang/rust/blob/18a6d911caba59605eb03db1452848a85d2e5879/compiler/rustc_trait_selection/src/traits/select/mod.rs#LL629C19-L629C19) again.

a-mir-formality impl:
- via macros parses syntax fairly close to surface Rust
- lowered to an IR in `decls` via `to_prove_decls`
- IR is then checked via `check_current_crate`
- checks each item in the crate
- ends up using `prove_goal` in an `Env` (`InferCtxt` in rustc without constraints (inference and region constraints are tracked separately)) and given some `assumptions` (`where`-clauses).
- returns set of ways the goal can be proven `Set<Constraints>`, pretty much an OR of candidates
- query cycles are avoided by running queries to a fixpoint (afaict propagate errors to the root and rerun until the root doesn't change)

---

trait Foo: Bar { }
fn is_foo<X: Foo>() { is_bar::<X>()}
fn is_bar<X: Bar>() { }

---

#[rustc_coinductive]
trait Coinductive { }

impl Coinductive for () { }

impl<T> Coinductive for Option<T>
where
    T: Coinductive
{ }

impl<T> Coinductive for List<T>
where
    Option<List<T>>: Coinductive
{ }

struct List<T> { next: Option<List<T>> }

fn test<X: Coinductive>() { }

fn main() { test::<Option<List<()>>>(); }