lazy norm, infinitely sized types, and the occurs check

[lcnr]

for type Alias = Vec<Alias>;, equating Alias with Vec<Alias> may succeed:

• normalizes-to(Alias, Vec<Alias>) -> Vec<Alias>
  • equate(Vec<Alias>, Vec<Alias>) ok via structural equality fast-path

This would cause the occurs check to be incomplete as ?0 eq Vec<?0> can be proven by instantiating ?0 with Alias. The occurs check is strictly required:

trait From<T> {}
impl<T> From<T> for T {}
impl<T> From<T> for Box<T> {}

This issue is pretty much purely theoretical as we're eagerly replacing all aliases inside of the normalized type with infer vars when equating it with the expected term. I don't necessarily believe we need to handle this until somebody crafts an example where this causes 'overlap' of impls allowed due to the occurs check.

[lcnr]

cc https://hackmd.io/N0rzMn94QZOfbaAVOl4f6A#finite-size-is-good-actually

one solution would be to attempt to eagerly detect associated type definitions which may expand to infinite types. This is already allowed on stable and would therefore require a breaking change. One such example is the following:

trait Trait {
    type Assoc;
}

impl<T: Trait> Trait for Vec<T> {
    type Assoc = T::Assoc;
}

trait Indir {
     type IndirAssoc<T: Trait>: Trait;
}

struct Map<T>(T);
impl<T: Indir> Trait for Map<T> {
    type Assoc = <T::IndirAssoc<Self> as Trait>::Assoc;
}

// in a downstream crate
struct Local;
impl Indir for Local {
    type IndirAssoc<T: Trait> = Vec<T>;
}

// `<Map<Local> as Trait>::Assoc` is now infinite,
// all impls are
// fine by itself.

[nikomatsakis]

Conclusion: we are going to ignore this for now. We don't know of a concrete problem. We do know of various solutions (noted below) all of which seem unappealing but also largely orthogonal to other issues we have to address so we prefer to ignore this problem for now.

Options include:

• Adding some kind of where-clause that guarantees termination to impls that have "sufficiently complicated" values for their associated types (e.g., <T::IndirAssoc<Self> as Trait>::Assoc;) -- breaking change but soundness justified, unclear impact.
• (Potentially) post-monomorphization checks after normalization -- we already check for recursion depth but we could also enforce conditions that fully monomorphized trait references e.g. cannot reference Self (and make sure that we fully normalize everywhere we need to)
• We also observe that even if there are potentially overlapping impls, if we at monomorphization time we encounter that, we will (currently) ICE -- mostly (object impls...).