# region constraints

## tangent: `param_env` in the solver

only place whch should update the `param_env` is instantiating a binder. This place also has to deal with higher ranked region constraints.

### Ideal

`param_env` part of the `EvalCtxt`, only place which has to care about changes to the `param_env` is `compute_goal` if there's a binder. Issues: equate eagerly instantiates bound variables instead of using subgoals.

### What to do without that

Region obligations don't have a param env and ideally we prove all of them when "exiting a binder" so all region obligations have the same param env.

For now: simply use the `param_env` of the context even if it is wrong.

## destructuring type outlives "eagerly"

### interesting cases:

- `EscapingAlias` and `Alias`
- `ty::Infer`

- `components_must_outlive`
- `Region` `Param` trivial
- `ty::Infer`: actually can return an outlives bound to the caller because the inference var cannot mention placeholders. This doesn't 100% work once we have implied bounds on binders. Could also be known to outlive some other type which outlives the placeholder due to an implied bound.

## getting rid of placeholders when leaving binders

Mostly doesn't require us to compute type outlives eagerly.

For `whatever: 'placeholder`, simply require `'whatever: 'static`.

for `'placeholder: 'whatever` check `'placeholder == 'whatever'`, else error

what can we do for `TyWithPlaceholder: 'whatever`, mostly `<?0 as Trait<'placeholder, 'b>>::Assoc: 'c`. This may hold but we have no way to tell.

Step 1, consider this ambig if `normalizes-to` returns ambig, left with
`<T as Trait<'placeholder, 'b>>::Assoc: 'c`. Issue: `for<'a> <T as Trait<'a, 'b>>::Assoc: 'c` bound in env, cannot eagerly check whether that one applies.

I don't think this works without returning `OR`

## coinduction makes me sad

pub struct Bar
where
    for<'a> &'a mut Bar:;

- `for<'a> WF(&'a mut Bar)` (attempt 0)
- `WF(&'a.1 mut Bar)`
- `outlives(Bar, 'a.1)` OK `[Bar: 'a.1]`
- `WF(Bar)`
- `for<'a> WF(&'a mut Bar)` cycle OK `[]`
- RESULT: OK `[Bar: 'a.1]`
- `for<'a> WF(&'a mut Bar)` (attempt 1)
- `WF(&'a.1 mut Bar)`
- `outlives(Bar, 'a.1)` OK `[Bar: 'a.1]`
- `WF(Bar)`
- `for<'a> WF(&'a mut Bar)` cycle OK `[Bar: 'a.2]` (create new universe)
- RESULT: OK `[Bar: 'a.1, Bar: 'a.2]`
- `for<'a> WF(&'a mut Bar)` (attempt 2)
- `WF(&'a.1 mut Bar)`
- `outlives(Bar, 'a.1)` OK `[Bar: 'a.1]`
- `WF(Bar)`
- `for<'a> WF(&'a mut Bar)` cycle OK `[Bar: 'a.2, Bar: 'a.3]` (create new universe)
- RESULT: OK `[Bar: 'a.1, Bar: 'a.2, Bar: 'a.3]`

starting with `WF(BAR)`
- `WF(Bar)` iteration 0
- `for<'a> WF(&'a mut Bar)`
- `WF(&'a.1 mut Bar)`
- `outlives(Bar, 'a.1)` OK `[Bar: 'a.1]`
- `WF(Bar)` cycle OK `[]`
- `WF(Bar)` iteration 1
- `for<'a> WF(&'a mut Bar)`
- `WF(&'a.1 mut Bar)`
- `outlives(Bar, 'a.1)` OK `[Bar: 'a.1]`
- `WF(Bar)` cycle OK `[Bar: 'a.?]`

struct Foo
where
    Foo:,
    for<'a> &'a ():;

- `WF(Foo)` iteration 0
- `WF(Foo)` cycle OK `[]`
- `for<'a> WF(&'a ())` OK `[(): 'a.1]` (new universe for unnameable placeholder)
- result OK `[(): 'a.1]`
- `WF(Foo)` iteration 1 (in new infcx)
- `WF(Foo)` cycle OK `[(): 'a.1]` (new universe for unnameable placeholder)
- `for<'a> WF(&'a ())` OK `[(): 'a.2]` (new universe for unnameable placeholder)
- result OK `[(): 'a.1, (): 'a.2]` yikes (have to rerun again)

## Options

when we hit a cycle, backtrack and then reprove without canonicalization. The provisional cache is a lot simpler as we don't have to deal with canonicalization anymore. That kinda sucks but would work

actually implement `OR` and destruct any type outlives containing binders eagerly.

implement a way which merges constraints including unnameable universes if they are otherwise identical.