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.
The cycle in the following test should be ambiguous or even accepted, not a hard error:
normalizes_to(<i32 as Trait>::Assoc, ())depends onnormalizes_to(<u32 as Trait>::Assoc, ()), depends onProjection(<i32 as Trait>::Assoc, ())which depends onnormalizes_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:
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.