inference, lazy normalization, and occurs check

[nikomatsakis]

One interesting question is how the occurs check interacts with lazy normalization. Consider the inference unit test projection_eq. It attempts to solve an equation like exists(A -> A = Item0<<A as Item1>::foo>), which is currently rejected. In some sense, this is obviously an infinitely sized type, and indeed <A as Item1>::foo might normalize to A. But it could also normalize to u32, in which case normalization would make the type finite size.

Perhaps the best answer is to substitute a new variable (and a new normalization obligation). So that after processin that result, A would be bound to A = Item0<B> where <A as Item1::Foo> == B? If B wound up including A, then the occurs check would fail then.

(We just have to be wary of this recurring infinitely...)

[nikomatsakis]

Thinking more about this, I have to wonder why I opted to have have chalk "defer" normalization the way that is does (i.e., by producing a new obligation to be solved), rather than just solving it in place (recursively). I've wondered before, but it didn't seem to make much difference. But when you think about the need to track recursion depth, it might make things mildly simpler.

[soltanmm]

I'm not familiar with how the code currently behaves, but to get me thinking about this and because I want to contribute, here're some bouncy thoughts:

This sounds like something that'd fall out of having a 'progress' measure. If all the atoms (types) are grouped into equivalence classes with each equivalence class having some designated element (e.g. by organizing w/ union-find and doing a union every time a == obligation is made) normalizing all types in encountered obligations to the 'minimum' element and 'forgetting' about duplicated obligations, then 'progress' can be measured w.r.t. whether or not 'new' obligations are generated.

The only way for the above to loop indefinitely is if there's an infinitely sized type that doesn't repeat itself. I think that should only happen in pathological cases like someone using the type system to compute π or whatever (and that can then be sort-of-caught by checking the sizes of produced types). Though, then there's no 'recursion limit' per se, one'd need to give a limit to the maximum type size instead.

EDIT: well, okay, union-find wouldn't work because one'd need to map from the members of the set back to the designated member, but the gist of it is still there derp

EDIT EDIT: also I guess it could go infinitely if obligations are allowed to have an arbitrarily large (growing) number of atoms in them, but I don't think that's the case?

[jackh726]

@nikomatsakis Is this issue still relevant? It sounds similar to (#234) and (#280). The FIXME in the code isn't there anymore. Can this issue be closed?

[nikomatsakis]

Yeah, I'm going to close this. We may indeed find some problems relating to this underlying pattern in practice, but we may not -- my concern would be that maybe there is something that we are able to type-check if we eagerly normalize (as rustc does) but which produces an "infinite type" if we are lazy. But the best way to find that would be to be converted rustc to a more lazy approach, I think.