Always relate with Invariant to non-General inference vars by jackh726 · Pull Re...

Contributor

matthewjasper commented 20 days ago

Rustc doesn't unify inference variables with subtype bounds:

https://github.com/rust-lang/rust/blob/b776d1c3e3db8befabb123ebb1e46c3531eaed46/compiler/rustc_infer/src/infer/sub.rs#L87-L112

Looking at unification, the only difference here with rustc in this area is that {int_var} <: {ty_var} is turned into {int_var} = {ty_var} (and likewise with floats, and with the subtype relation reversed).

jackh726 commented 20 days ago

Looking at unification, the only difference here with rustc in this area is that {int_var} <: {ty_var} is turned into {int_var} = {ty_var} (and likewise with floats, and with the subtype relation reversed).

Ugh yeah, that's what I was missing and what the proper change is.

jackh726 commented 20 days ago

Actually, that alone is not enough to make the test pass :/

matthewjasper commented 19 days ago

I'm not sure if the test case with two arbitrary variables needs to pass. One of the variables will eventually be resolved if the program is going to compile.

jackh726 commented 19 days ago

I wondered about that. I did test with the original test from @flodiebold with the int T and that didn't pass.

nikomatsakis commented 19 days ago

I don't love this solution. Like @matthewjasper, I'm not sure that the test with two arbitrary variables needs to pass. @jackh726 can you share what you tried with integer variables? In rustc, we definitely consider integer variables "more specific" than normal variables (so e.g. a general variable would be "assigned" the value of an integer variable).

jackh726 commented 19 days ago

Yeah, I updated.

jackh726 commented 19 days ago

So, to elaborate on why only always unifying non-general inference vars doesn't work:
First, we start off trying to unify our goal Implemented(MyClosure<"rust" for<0> [?0 := (&'static ?0), ?1 := 0]>: FnOnce<1<(&'static ?1i)>>) with our (instantiated) clause Implemented(MyClosure<"rust" for<0> [?0 := ?2, ?1 := 0]>: FnOnce<1<?2>>).

From there, we try to unify MyClosure<"rust" for<0> [?0 := (&'static ?0), ?1 := 0]> and MyClosure<"rust" for<0> [?0 := ?2, ?1 := 0]> first. When ?2 tries to get unified with (&'static ?0), it is generalized and set to (&'?3 ?4). From the next unification, we get ?4 < ?0 (and the reverse too, since both Covariant and Contravariant, since we're in Invariant).

By this point, when we unify 1<(&'static ?1i)> and 1<?2>, it's too late, and we've already added the subtype goals.

jackh726 commented 19 days ago

Okay, so we probably just need to actually resolve inference vars when trying to simplify a subtype goal...

jackh726 commented 19 days ago

Okay so that worked.

nikomatsakis commented 15 days ago

oops, I forgot, we use bors now don't we... d'oh