Skip to content

occurs check with aliases results in error, not ambiguity #105787

Closed
@lcnr

Description

@lcnr

edit: this issue has been partially fixed in #117088, so any remaining incompleteness (and therefore incorrectly accepted overlap) is a lot harder to trigger. See rust-lang/trait-system-refactor-initiative#8 for a list of known issues with generalization. Keeping this issue open as is to track this, but we should try to write a test which relies on one of the other problems of that issue, now that the problem case 2 has been fixed.


// Using the higher ranked projection hack to prevent us from replacing the projection
// with an inference variable.
trait ToUnit<'a> {
    type Unit;
}

struct LocalTy;
impl<'a> ToUnit<'a> for *const LocalTy {
    type Unit = ();
}

impl<'a, T: Copy + ?Sized> ToUnit<'a> for *const T {
    type Unit = ();
}

trait Overlap<T> {
    type Assoc;
}

type Assoc<'a, T> = <*const T as ToUnit<'a>>::Unit;

impl<T> Overlap<T> for T {
    type Assoc = usize;
}

impl<T> Overlap<for<'a> fn(&'a (), Assoc<'a, T>)> for T
where
    for<'a> *const T: ToUnit<'a>,
{
    type Assoc = Box<usize>;
}

fn foo<T: Overlap<U>, U>(x: T::Assoc) -> T::Assoc {
    x
}

fn main() {
    foo::<for<'a> fn(&'a (), ()), for<'a> fn(&'a (), ())>(3usize);
}

for<'a> fn(&'a (), ())>: Overlap<for<'a> fn(&'a (), ())>> can be satisfied using both impls, ignoring a deficiency of the current normalization routine which means that right now the second impl pretty much never applies.

Currently inference constraints from equating the self type are not used to normalize the trait argument so we fail when equating () with Assoc<'a, for<'a> fn(&'a (), ())> even those these two are the same type. This will change once deferred projection equality is implemented.

why this currently passes coherence

Coherence does a pairwise check for all relevant impls. It starts by instantiating the impl parameters with inference vars and equating the impl headers. When we do that with Overlap<T> for T and Overlap<for<'a> fn(&'a (), Assoc<'a, T>)> for T we have:

  • eq(?0: Overflap<?0>, ?1: Overlap<for<'a> fn(&'a (), <*const ?1 as ToUnit<'a>>::Unit)>)
    • eq(?0, ?1) constrains ?1 to be equal to ?0
    • eq(?0, for<'a> fn(&'a (), <*const ?0 as ToUnit<'a>>::Unit)>): this now fails the occurs check

The occurs check is necessary to prevent ourselves from creating infinitely large types, e.g. ?0 = Vec<?0>. But it does mean that coherence considers these two impls to be disjoint. Because the inference var only occurs inside of a projection, there's a way to equate these two types without resulting in an infinitely large type by normalizing the projection.

Metadata

Metadata

Assignees

Labels

A-coherenceArea: CoherenceA-impl-traitArea: `impl Trait`. Universally / existentially quantified anonymous types with static dispatch.A-trait-systemArea: Trait systemC-bugCategory: This is a bug.I-unsoundIssue: A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/SoundnessP-mediumMedium priorityT-typesRelevant to the types team, which will review and decide on the PR/issue.

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions