Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

equality of aliases with ambiguous normalization #75

Open
lcnr opened this issue Nov 9, 2023 · 0 comments
Open

equality of aliases with ambiguous normalization #75

lcnr opened this issue Nov 9, 2023 · 0 comments

Comments

@lcnr
Copy link
Contributor

lcnr commented Nov 9, 2023

Equating aliases whose normalization is ambiguous is sus™ as there are conflicting requirements.

Equate should be complete

We do not want the equating of two types to result in unnecessary inference or region constraints. Both because it is not nice™ and also because it is unsound when done during coherence (rust-lang/rust#102048). This means that for an ambiguous alias like <T as WithAssoc<'lt>>::Assoc in the below example, we must not simply equate the generic arguments of the alias.

trait Trait<T> {}

trait WithAssoc<'a> {
    type Assoc;
}

impl<T: for<'a> WithAssoc<'a>> Trait<T> for for<'a> fn(<T as WithAssoc<'a>>::Assoc) {}

impl<'a, T: WithAssoc<'a>> Trait<T> for fn(<T as WithAssoc<'a>>::Assoc) {}

Type relations should be idempotent

Relating a type with itself should always succeed. Because of MIR typeck we have an even stronger invariant: relating a type with itself (modulo regions) should always succed (potentially emitting region constraints).

This is necessary as we erase regions after HIR typeck and replace them with unique region inference variables during MIR typeck. The below example currently fails because we try to eagerly normalize <T as Trait<'a>>::Assoc somewhere, avoiding this issue.

struct Invariant<T>(*mut T);
trait Trait<'a> {
    type Assoc;
}

fn foo<'a, T>(
    x: Invariant<<T as Trait<'a>>::Assoc>,
) -> Invariant<<T as Trait<'a>>::Assoc>
where
    T: for<'b> Trait<'b, Assoc = <T as Trait<'b>>::Assoc>,
{
    let y = x;
    y
}

We currently uniquify lifetimes when canonicalizing solver inputs to avoid any dependencies on the exact lifetimes. Not doing so ended up causing ICEs during MIR typeck: #27. This means we need to handle types which are structurally equal up to regions everywhere, causing issues for non-defining uses of opaque types in their defining scope (#74)

Relating aliases whose normalization is ambiguous cannot be both complete and idempotent (ignoring regions) at the same time


@lcnr would like to "fix" this by requiring aliases to be either normalizable or rigid, causing aliases with ambiguous normalization to not be well-formed. This means we don't have to worry if their behavior is inconsistent.

bors added a commit to rust-lang-ci/rust that referenced this issue Nov 17, 2023
…rors

new solver normalization improvements

cool beans

At the core of this PR is a `try_normalize_ty` which stops for rigid aliases by using `commit_if_ok`.

Reworks alias-relate to fully normalize both the lhs and rhs and then equate the resulting rigid (or inference) types. This fixes rust-lang/trait-system-refactor-initiative#68 by avoiding the exponential blowup. Also supersedes rust-lang#116369 by only defining opaque types if the hidden type is rigid.

I removed the stability check in `EvalCtxt::evaluate_goal` due to rust-lang/trait-system-refactor-initiative#75. While I personally have opinions on how to fix it, that still requires further t-types/`@nikomatsakis` buy-in, so I removed that for now. Once we've decided on our approach there, we can revert this commit.

r? `@compiler-errors`
bors added a commit to rust-lang/miri that referenced this issue Nov 21, 2023
new solver normalization improvements

cool beans

At the core of this PR is a `try_normalize_ty` which stops for rigid aliases by using `commit_if_ok`.

Reworks alias-relate to fully normalize both the lhs and rhs and then equate the resulting rigid (or inference) types. This fixes rust-lang/trait-system-refactor-initiative#68 by avoiding the exponential blowup. Also supersedes #116369 by only defining opaque types if the hidden type is rigid.

I removed the stability check in `EvalCtxt::evaluate_goal` due to rust-lang/trait-system-refactor-initiative#75. While I personally have opinions on how to fix it, that still requires further t-types/`@nikomatsakis` buy-in, so I removed that for now. Once we've decided on our approach there, we can revert this commit.

r? `@compiler-errors`
lnicola pushed a commit to lnicola/rust-analyzer that referenced this issue Apr 7, 2024
new solver normalization improvements

cool beans

At the core of this PR is a `try_normalize_ty` which stops for rigid aliases by using `commit_if_ok`.

Reworks alias-relate to fully normalize both the lhs and rhs and then equate the resulting rigid (or inference) types. This fixes rust-lang/trait-system-refactor-initiative#68 by avoiding the exponential blowup. Also supersedes #116369 by only defining opaque types if the hidden type is rigid.

I removed the stability check in `EvalCtxt::evaluate_goal` due to rust-lang/trait-system-refactor-initiative#75. While I personally have opinions on how to fix it, that still requires further t-types/`@nikomatsakis` buy-in, so I removed that for now. Once we've decided on our approach there, we can revert this commit.

r? `@compiler-errors`
RalfJung pushed a commit to RalfJung/rust-analyzer that referenced this issue Apr 27, 2024
new solver normalization improvements

cool beans

At the core of this PR is a `try_normalize_ty` which stops for rigid aliases by using `commit_if_ok`.

Reworks alias-relate to fully normalize both the lhs and rhs and then equate the resulting rigid (or inference) types. This fixes rust-lang/trait-system-refactor-initiative#68 by avoiding the exponential blowup. Also supersedes #116369 by only defining opaque types if the hidden type is rigid.

I removed the stability check in `EvalCtxt::evaluate_goal` due to rust-lang/trait-system-refactor-initiative#75. While I personally have opinions on how to fix it, that still requires further t-types/`@nikomatsakis` buy-in, so I removed that for now. Once we've decided on our approach there, we can revert this commit.

r? `@compiler-errors`
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant