old solver doesn't check normalization constraints in `compare_impl_item`

[lcnr]

trait Trait {
    type Assoc<'a>
    where
        Self: 'a;
}
impl<'b> Trait for &'b u32 {
    type Assoc<'a> = &'a u32
    where
        Self: 'a; 
}

trait Bound<T> {}
trait Entailment<T: Trait> {
    fn method()
    where
        Self: for<'a> Bound<<T as Trait>::Assoc<'a>>;
}

impl<'b, T> Entailment<&'b u32> for T {
    // Instantiates trait where-clauses with `&'b u32` and then normalizes
    // `T: for<'a> Bound<<&'b u32 as Trait>::Assoc<'a>>` in a separate infcx
    // without checking region constraints.
    //
    // It normalizes to `T: Bound<&'a u32>`, dropping the `&'b u32: 'a` constraint.
    fn method()
    where
        Self: for<'a> Bound<&'a u32>
    {}
}

fn main() {}

https://github.com/rust-lang/rust/blob/aaa861493456e8a10e552dd208f85486de772007/compiler/rustc_hir_analysis/src/check/compare_impl_item.rs#L238-L239

The new solver doesn't eagerly normalize the hybrid env in compare_impl_item, so it actually ends up normalizing <&'b u32 as Trait>::Assoc<'a> in the 'main' infcx, checking the resulting region constraints

This requires the associated type to be rigid in the trait method and normalizeable in the hybrid env. To do that, the trait bound proving T: Trait needs to be on the trait instead of the method. Alternatively, we could probably use a where-bound which ends up global after instantiating with the impl args.

affected tests

• tests/ui/higher-ranked/trait-bounds/issue-102899.rs
• tests/ui/higher-ranked/trait-bounds/issue-100689.rs

[lcnr]

I don't think this is necessarily unsound as calling the trait method should end up having us prove (and normalize) the trait predicates again. So if normalization in the impl results in an error, it should also error when trying to use the impl in these cases.

I believe that we should try to break this code in the old solver. I am unsure how we'd best hack around this in the new solver and would be quite unhappy if we have to.

[compiler-errors]

I think the analysis in this issue is a bit misguided -- the "root cause" here is that applying a param-env candidate for a projection bound doesn't register the GAT wf obligations in the old solver (just impl candidates). Removing this fixes the issue:

https://github.com/rust-lang/rust/blob/f44efbf9e11b1b6bba77c046d7dd150de37e0e0f/compiler/rustc_next_trait_solver/src/solve/normalizes_to/mod.rs#L135-L142

We could perhaps check GAT where clauses on all candidates in the old solver, or make the new solver only check GAT where clauses for impls.

[compiler-errors]

Actually, I was the one who was misguided. We do register GAT wf clauses for param-env candidates 🤔 but this is ignored (i.e. doesn't turn into a region error) in the old solver due to the .ignore_regions() call in do_normalize_predicates in param-env normalization. That sucks lol

[lcnr]

• not checking GAT where-clauses during normalization fixes this in the new solver
• we are unsure whether not checking GAT where-clauses is correct
  • should be theoretically implied by WF
  • but what about cycles etc etc
• breaking in the old solver feels kinda iffy 🤔

[lcnr]

also affects egglog-core-relations https://rust-lang.zulipchat.com/#narrow/channel/364551-t-types.2Ftrait-system-refactor/topic/crater.20triage.3A.20.60egglog.60.20lifetime.20bound.20not.20satisfied/with/547816552

pub struct ScopedActionBuffer<'inner, 'scope>(pub (&'inner (), &'scope ()));

pub trait ActionBuffer<'state> {
    type AsLocal<'a>
    where
        'state: 'a;
    fn recur(work_: impl for<'a> FnOnce(&mut Self::AsLocal<'a>));
}

impl<'scope> ActionBuffer<'scope> for ScopedActionBuffer<'_, 'scope> {
    type AsLocal<'a>
        = ScopedActionBuffer<'a, 'scope>
    where
        'scope: 'a;
    fn recur(_: impl for<'a> FnOnce(&mut ScopedActionBuffer<'a, 'scope>)) {}
}

[lcnr]

We could also normalize the ParamEnv in the new solver here. Seems ass as we don't do it anywhere else. Always normalizing ParamEnvs also sucks and seems like a big change.

Normalizing via impls currently checks GAT where-clauses. This is necessary for soundness :> see rust-lang/rust#148783

This will be solved by "add assumptions on binders MVP". That's something we want in the medium term, but should not block the stabilization of the new solver on it.

Making this intended breakage also kinda sucks. There isn't really a good way to communicate this breakage to users Ah well, just be inconsistent but with a FIXME.