Stream: wg-traits

Topic: unification in chalk


nikomatsakis (Oct 15 2018 at 17:41, on Zulip):

@scalexm so, I was looking more at some of the chalk methods -- if we are moving away from predicate -- we may need our own "unification code" for chalk

nikomatsakis (Oct 15 2018 at 17:41, on Zulip):

which is actually not that hard to do

nikomatsakis (Oct 15 2018 at 17:41, on Zulip):

but it would probably be the third instance of the same basic logic

nikomatsakis (Oct 15 2018 at 17:41, on Zulip):

which I am not super thrilled about

nikomatsakis (Oct 15 2018 at 17:42, on Zulip):

right now, there is the "main type relating" code, and then NLL has its own copy

nikomatsakis (Oct 15 2018 at 17:42, on Zulip):

the main one yields up PredicateObligation<'tcx> results

nikomatsakis (Oct 15 2018 at 17:42, on Zulip):

but we would rather want Goal values

nikomatsakis (Oct 15 2018 at 17:43, on Zulip):

otoh that may be inevtable because the chalk unifier would be the one in charge of handling the lazy norm logic I guess

scalexm (Oct 15 2018 at 17:44, on Zulip):

@nikomatsakis ok so I guess I can just take the existing unifier code and rewrite it so as it uses goals?

nikomatsakis (Oct 15 2018 at 17:45, on Zulip):

I am pondering

nikomatsakis (Oct 15 2018 at 17:45, on Zulip):

I'd probably model it on the NLL code

nikomatsakis (Oct 15 2018 at 17:45, on Zulip):

however:

nikomatsakis (Oct 15 2018 at 17:45, on Zulip):

we have at times been wondering if it makes sense to even use an infcx at all

nikomatsakis (Oct 15 2018 at 17:46, on Zulip):

ah well I don't want to revisit that decision yet

nikomatsakis (Oct 15 2018 at 17:47, on Zulip):

let's discuss at the planning meeting; but in short I think that ā€” much as it pains me ā€” it probably makes sense to have Yet Another Unifier, yeah. We really need to see what we can do about reducing that though

nikomatsakis (Oct 15 2018 at 17:47, on Zulip):

I want to try and get a bit further through this list of unimplemented! helpers

Jake Goulding (Oct 15 2018 at 18:57, on Zulip):

Unify the unifiers!

nikomatsakis (Oct 15 2018 at 18:57, on Zulip):

"who will unify the unifiers...?"

nikomatsakis (Oct 15 2018 at 18:58, on Zulip):

I am totally going to go create a rustc issue with that title

scalexm (Nov 01 2018 at 17:54, on Zulip):

@nikomatsakis where is the NLL unifier defined?

nikomatsakis (Nov 01 2018 at 17:55, on Zulip):

say more :)

nikomatsakis (Nov 01 2018 at 17:55, on Zulip):

there isn't really a "NLL unifier" per se

nikomatsakis (Nov 01 2018 at 17:55, on Zulip):

well I guess maybe you mean this https://github.com/rust-lang/rust/blob/master/src/librustc_mir/borrow_check/nll/type_check/relate_tys.rs

scalexm (Nov 01 2018 at 17:55, on Zulip):

ah, yeah my question is maybe a bit vague, you told me that the simplest thing for chalk would be to have yet another copy of the unification code

nikomatsakis (Nov 01 2018 at 17:56, on Zulip):

oh

nikomatsakis (Nov 01 2018 at 17:56, on Zulip):

so you were looking for reference?

scalexm (Nov 01 2018 at 17:57, on Zulip):

yes that's right :)

nikomatsakis (Nov 01 2018 at 17:58, on Zulip):

I'm trying to remember why I said that :)

nikomatsakis (Nov 01 2018 at 17:58, on Zulip):

oh, I guess in part because of lazy norm

nikomatsakis (Nov 01 2018 at 17:59, on Zulip):

(sound right?)

scalexm (Nov 01 2018 at 17:59, on Zulip):

yes, and that we wanted to use Goal etc instead of ty::PredicateObligation

nikomatsakis (Nov 01 2018 at 18:01, on Zulip):

ok, well, then probably the code I referred you to just now is what I was thinking of

nikomatsakis (Nov 01 2018 at 18:01, on Zulip):

I guess those are still good reasons

scalexm (Nov 01 2018 at 18:03, on Zulip):

ok cool

scalexm (Nov 03 2018 at 15:32, on Zulip):

@nikomatsakis are you around by any chance?

scalexm (Nov 05 2018 at 21:07, on Zulip):

@nikomatsakis fyi https://github.com/rust-lang-nursery/chalk/issues/189 is blocking the implementation of ChalkContext::instantiate_ex_clause

scalexm (Nov 05 2018 at 21:08, on Zulip):

also, I was thinking that if we generalized the NLL relating code so that it handles inference variables in both sides of the relation, it would be easy for me to adapt it for chalk

scalexm (Nov 05 2018 at 21:09, on Zulip):

I just extended a bit the TypeRelatingDelegate delegate and added a NormalizationStrategy enum (with Lazy/Eager variants)

Alexander Regueiro (Nov 06 2018 at 02:02, on Zulip):

@nikomatsakis okay sure. could you recommend someone to take a look at my PR in the meanwhile maybe?

nikomatsakis (Nov 07 2018 at 09:36, on Zulip):

@scalexm what is current status here?

scalexm (Nov 07 2018 at 10:17, on Zulip):

@nikomatsakis I have placeholder types etc, as I said I think Iā€™m going to extend the NLL relating code so that it handles inference variables in both sides and I can use it for chalk

scalexm (Nov 07 2018 at 10:19, on Zulip):

Because apart from that, I found it easy to just inject lazy normalization into it

scalexm (Nov 07 2018 at 22:08, on Zulip):

ok @nikomatsakis, I think the main work on unification was done in this commit: https://github.com/rust-lang/rust/commit/7f4ca7ff35b34a4923bb92a4e9f251c8aa1cc935

scalexm (Nov 07 2018 at 22:08, on Zulip):

however there are a few little unknowns for which I might need your help

scalexm (Nov 07 2018 at 22:09, on Zulip):

tell me when you have a bit of time to discuss (this can be done through text messages)

nikomatsakis (Nov 08 2018 at 16:03, on Zulip):

hmm

nikomatsakis (Nov 08 2018 at 16:03, on Zulip):

@scalexm perhaps I can carve out some time tomorrow morning?

scalexm (Nov 08 2018 at 16:06, on Zulip):

@nikomatsakis seems fine

nikomatsakis (Nov 12 2018 at 18:58, on Zulip):

@scalexm so obviously that failed

nikomatsakis (Nov 12 2018 at 18:58, on Zulip):

:)

nikomatsakis (Nov 12 2018 at 18:59, on Zulip):

want to chat tomorrow morning though? perhaps at 10am my time (4pm your time)?

scalexm (Nov 12 2018 at 18:59, on Zulip):

@nikomatsakis yeah that's cool

scalexm (Nov 13 2018 at 15:40, on Zulip):

@nikomatsakis https://github.com/rust-lang/rust/compare/master...scalexm:unification

nikomatsakis (Nov 13 2018 at 15:43, on Zulip):
struct Foo<A, B> where A: Iterator<Item = B> { a: A }
nikomatsakis (Nov 13 2018 at 15:45, on Zulip):

Foo<A1, ?B1> <: Foo<A2, ?B2>

nikomatsakis (Nov 13 2018 at 15:59, on Zulip):
for<'a, 'b> fn(&'a u32, &'b u32) == for<'a> fn(&'a u32, &'a u32)
scalexm (Nov 13 2018 at 16:03, on Zulip):

https://github.com/rust-lang/rust/commit/a8c21cd2d3c4ac119a4b107aa4e0cdaf6d2e40f8#diff-32301bf61aae94fb34652b6c581a507fL255

Alexander Regueiro (Nov 13 2018 at 16:43, on Zulip):

@nikomatsakis any time to look at my questions / WIP PR today maybe?

nikomatsakis (Nov 13 2018 at 16:43, on Zulip):

on my list for today, yes

Alexander Regueiro (Nov 13 2018 at 16:53, on Zulip):

:tada:

Alexander Regueiro (Nov 13 2018 at 16:53, on Zulip):

thanks

scalexm (Nov 15 2018 at 19:07, on Zulip):

@nikomatsakis so I have all the chalk callbacks implemented in my unification branch (modulo the ones that @Sunjay Varma and @uberjay are working on)

scalexm (Nov 15 2018 at 19:07, on Zulip):

there are probably a lot of bugs, so I guess a way to test everything is to proceed on switching the trait solver to use chalk

scalexm (Nov 15 2018 at 19:08, on Zulip):

any guidance for that? I'm not sure I know where to start

scalexm (Nov 15 2018 at 19:11, on Zulip):

ok I guess first step is to implement the TraitEngine trait that @csmoe added

nikomatsakis (Nov 15 2018 at 19:18, on Zulip):

yep that's right @scalexm

scalexm (Nov 28 2018 at 15:35, on Zulip):

@nikomatsakis could you find some time to review https://github.com/rust-lang/rust/pull/56214?

scalexm (Nov 28 2018 at 15:36, on Zulip):

I think I have fixed most bugs since my chalk branch seems to work pretty well now

nikomatsakis (Nov 28 2018 at 15:36, on Zulip):

yep; still feeling a bit sick today but I expect to at least do some reviewing in between naps :)

Last update: Nov 12 2019 at 15:35UTC