Refactor propagation to be more explicit

[nikomatsakis]

In conjunction with @soltanmm, and with an aim towards enabling lazy normalization, HR-caching, specialization's lifetime dispatch rules, and a number of other things, we should refactor the way we propagate obligations and mutable state through the inference context.

The general idea is to make the result of unification also carry a list of obligations. This can be used by lazy normalizing to carry the results of normalization, but we should also (eventually) move all mutation of the region inference state out and use it to carry region edges that result. This will help simplify the skolemization code, with the lifetime dispatch logic, and with more advanced caching. It might also make sense to eventually move the unification of type variables too, so that unify is a pure function.

At the moment, this issue exists mainly to serve as a placeholder for FIXME, but I hope to expand with a bit more design and also some checklist of to-do items. :)

[soltanmm]

A note (both for myself to walk back to and I guess as a minor update):
Turns out that the obligation plumbing is incomplete AFAICT; switching up the variance appears to drop obligations on the floor. So, that'll happen in another PR before the originally planned next-step of propagating region inference obligations for the Sub and Equate relations over regions.

[jroesch]

cc me

[nikomatsakis]

@soltanmm I have a branch that is using the plumbing now to handle all region obligations. It's not quite right for higher-ranked stuff yet -- but seems to basically work:

failures:
[compile-fail] compile-fail/hr-subtype.rs
[compile-fail] compile-fail/lifetime-bound-will-change-warning.rs
[compile-fail] compile-fail/object-lifetime-default-from-rptr-box-error.rs
[compile-fail] compile-fail/object-lifetime-default-from-rptr-struct-error.rs
[compile-fail] compile-fail/object-lifetime-default-mybox.rs
[compile-fail] compile-fail/regions-bounds.rs
[compile-fail] compile-fail/regions-fn-subtyping-return-static.rs
[compile-fail] compile-fail/regions-infer-at-fn-not-param.rs
[compile-fail] compile-fail/regions-infer-contravariance-due-to-decl.rs
[compile-fail] compile-fail/regions-infer-covariance-due-to-decl.rs
[compile-fail] compile-fail/regions-infer-not-param.rs
[compile-fail] compile-fail/regions-infer-paramd-indirect.rs
[compile-fail] compile-fail/regions-trait-1.rs
[compile-fail] compile-fail/regions-variance-contravariant-use-covariant-in-second-position.rs
[compile-fail] compile-fail/regions-variance-contravariant-use-covariant.rs
[compile-fail] compile-fail/regions-variance-covariant-use-contravariant.rs
[compile-fail] compile-fail/trait-matching-lifetimes.rs
[compile-fail] compile-fail/variance-use-contravariant-struct-1.rs
[compile-fail] compile-fail/variance-use-covariant-struct-1.rs

test result: FAILED. 2465 passed; 19 failed; 13 ignored; 0 measured

[nikomatsakis]

This is the branch https://github.com/nikomatsakis/rust/tree/region-obligations

[nikomatsakis]

I've been plugging away on the higher-ranked code. It's coming along, but it's a bit trickier than I naively expected (e.g., I forgot about plug_leaks).

I'm thinking more and more I need to writeup the overall plan here. I still think we're on the right track, but the end-game is complicated. (e.g., in order to make lazy norm and higher-ranked stuff work -- which is of course one of the main motivations -- is going to require some refactoring to better handle higher-ranked reasoning in general.)

Sorry, I know this is vague, just don't have time for such a write-up this second.

[Mark-Simulacrum]

@nikomatsakis Could you provide an update on this?

[soltanmm]

IIRC all the reasons to do this are similarly addressed by efforts in Chalk and its eventual integration (though I'm saying this as someone who's been out of the loop for a while).

[nikomatsakis]

@Mark-Simulacrum getting there, still some FIXMEs related to this issue. I hope to be resolving them soon. (ps @soltanmm, we should chat, I don't have your new e-mail)

[nikomatsakis]

I'd call this done.