Skip to content

entering normalization where-bounds incorrectly considered non-productive #273

@lcnr

Description

@lcnr

The cycle in the following test should be ambiguous or even accepted, not a hard error:

trait Trait {
    type Assoc;
}

impl Trait for i32 {
    type Assoc = <u32 as Trait>::Assoc;
}

impl Trait for u32
where
    // i32: Trait // this compiles with the new olver
    i32: Trait<Assoc = ()>,
{
    type Assoc = ();
}

normalizes_to(<i32 as Trait>::Assoc, ()) depends on normalizes_to(<u32 as Trait>::Assoc, ()), depends on Projection(<i32 as Trait>::Assoc, ()) which depends on normalizes_to(<i32 as Trait>::Assoc, ()).

This cycle is currently considered non-productive, resulting normalization to fail with an error. However, when modelling it with @Nadrieril, this sort of cycle should actually be accepted. This means returning an error here is too strict. We modeled this by lowering it to dictionary passing style in their dependently typed calculus, cc https://rust-lang.zulipchat.com/#narrow/channel/144729-t-types/topic/A.20calculus.20for.20dictionary-passing-style/with/579840401.

This can be a problem due to two reasons:

  • coherence treats this kind of cycle as unproductive and errors, only for us to use the cycle in a way where we don't detect it as non-productive, causing overflow
  • changing this to be accepted in the future will impact inference, causing otherwise avoidable breakage

I don't quite know what to do here for now.

I think the reason we made these cycles non-productive is that we otherwise get incorrect ambiguity errors 🤔

We also haven't actually decided about the precise lowering of traits to that dictionary passing style, now is it guaranteed that this is the correct model at all, so this is all just up in the air. We could avoid having to make a decision here if weakening this to ambiguity doesn't break anything.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions