Stream: wg-traits

Topic: design meeting 2019.12.09


nikomatsakis (Dec 09 2019 at 19:02, on Zulip):

Hey @WG-traits =)

I don't have a dedicated topic for today's meeting, but what I was thinking would be useful was to try and "plot out" some of the big picture roadmap questions. I created a hackmd and was starting to write stuff into it. I'd hoped to have this ready before this time slot but c'est la vie

nikomatsakis (Dec 09 2019 at 19:05, on Zulip):

also, I don't think we ever wrote up our notes from the last design meeting, where we talked about types, right?

Jack Huey (Dec 09 2019 at 19:05, on Zulip):

I am around-ish. Enough to listen and respond to some comments (if we do talk about something), but not really enough to discuss in-depth

nikomatsakis (Dec 09 2019 at 19:05, on Zulip):

ok, I'm going to edit the hackmd and leave random things in this channel :P

nikomatsakis (Dec 09 2019 at 19:05, on Zulip):

I was also talking to @David Barsky on Friday, who may have some time to pursue some of this work in January

Jack Huey (Dec 09 2019 at 19:05, on Zulip):

That being said, I nominate we talk next week about the associated types problem

Jack Huey (Dec 09 2019 at 19:06, on Zulip):

#238 I think

nikomatsakis (Dec 09 2019 at 19:06, on Zulip):

yeah, that's probably a good idea

nikomatsakis (Dec 09 2019 at 19:06, on Zulip):

maybe I can add it to the calendar

Jack Huey (Dec 09 2019 at 19:06, on Zulip):

I had some more time on the plane yesterday to play around with it more

nikomatsakis (Dec 09 2019 at 19:07, on Zulip):

I guess you mean https://github.com/rust-lang/chalk/issues/234

Jack Huey (Dec 09 2019 at 19:07, on Zulip):

But there are some key questions that need to be discussed

Jack Huey (Dec 09 2019 at 19:07, on Zulip):

Yes, that

nikomatsakis (Dec 09 2019 at 19:07, on Zulip):

Indeed, it's definitely a topic in the spirit I hope to use this meeting for more and more: one where the right answer is rather unclear

Jack Huey (Dec 09 2019 at 19:08, on Zulip):

Maybe today, we can discuss/think about the rust-analyzer infinite loop problem?

nikomatsakis (Dec 09 2019 at 19:08, on Zulip):

Yes. I've thought about that and I think I know the strategy I would like to pursue

nikomatsakis (Dec 09 2019 at 19:08, on Zulip):

It actually fits some of the work we've been doing

nikomatsakis (Dec 09 2019 at 19:08, on Zulip):

In short, the idea is to separate unification (syntactic equality) from type relation (Rust type equality)

nikomatsakis (Dec 09 2019 at 19:09, on Zulip):

Today we conflate them and that is part of what is leading us into trouble here

nikomatsakis (Dec 09 2019 at 19:09, on Zulip):

You may recall that in past meetings I talked about a similar theme

Jack Huey (Dec 09 2019 at 19:09, on Zulip):

Sounds like #234?

nikomatsakis (Dec 09 2019 at 19:09, on Zulip):

Certainly related

nikomatsakis (Dec 09 2019 at 19:10, on Zulip):

When we were introducing the generic types, one of my goals was to take

nikomatsakis (Dec 09 2019 at 19:10, on Zulip):

clauses that include projection types

nikomatsakis (Dec 09 2019 at 19:10, on Zulip):

and compile them down

nikomatsakis (Dec 09 2019 at 19:10, on Zulip):

I probably talked about it in #234, yeah

nikomatsakis (Dec 09 2019 at 19:11, on Zulip):

so e.g.

forall<T> {
    Foo(<T as Iterator>::Item: Blah<T>) :- ...
}

might become

forall<T, U> {
    Foo(U: Blah<T>) :- ProjectionEq(<T as Iterator>::Item -> U), ...
}
Jack Huey (Dec 09 2019 at 19:11, on Zulip):

That's somewhat the approach I've been taking playing around

nikomatsakis (Dec 09 2019 at 19:11, on Zulip):

I had that working but I stopped at some point because I realized there was a problem around higher-ranked things

nikomatsakis (Dec 09 2019 at 19:11, on Zulip):

but what I realized recently was that I was giving up too easily

nikomatsakis (Dec 09 2019 at 19:12, on Zulip):

in short when we are creating clauses (and goals) we can find all the cases where syntactic equality and Rust type equality diverge and compile them with a similar pattern:

nikomatsakis (Dec 09 2019 at 19:12, on Zulip):

introduce a variable + a clause that constraints the variable

Jack Huey (Dec 09 2019 at 19:12, on Zulip):

On mobile, so I can't link right now, but there was a couple tests that I found that are "ambiguous" now that seem like they should be unique

Jack Huey (Dec 09 2019 at 19:12, on Zulip):

Will link later

nikomatsakis (Dec 09 2019 at 19:12, on Zulip):

this comes up in I think 3 cases:

nikomatsakis (Dec 09 2019 at 19:13, on Zulip):

the reason that I stumbled on this again recently is that I was trying to mock up the approach to region solving that I wanted to use, where chalk is responsible for handling higher-ranked lifetimes (cc @Matthew Jasper, @lqd)

nikomatsakis (Dec 09 2019 at 19:13, on Zulip):

and to do that I found I really needed to separate out syntactic equality of lifetimes with Rust equality

Jack Huey (Dec 09 2019 at 19:14, on Zulip):

Can we elaborate on that?

nikomatsakis (Dec 09 2019 at 19:14, on Zulip):

e.g. I wanted to be able to write a transitive rule for lifetimes like so:

Outlives(A: C) :- Outlives(A: B), Outlives(B: C)

(the actual rule would be mildly different, but that's the idea)

nikomatsakis (Dec 09 2019 at 19:15, on Zulip):

Can we elaborate on that?

doing so :)

nikomatsakis (Dec 09 2019 at 19:15, on Zulip):

the idea being that if you had in your environment something like 'a : 'b and 'b: 'c, I'd like to be able to find "all the things that 'a outlives in the environment")

nikomatsakis (Dec 09 2019 at 19:15, on Zulip):

but right now whenever you try to equate two lifetimes in chalk, it always succeeds, and it generates a "constraint" that propagates out that says that the outer context must prove they are equal

nikomatsakis (Dec 09 2019 at 19:16, on Zulip):

the idea is that chalk can't solve all of those constraints itself, it generates constraints that are fed to the borrow checker later

nikomatsakis (Dec 09 2019 at 19:16, on Zulip):

(the idea I am exploring around higher-ranked lifetimes is basically saying: actually chalk can figure this out for higher-ranked cases like forall<'a> { ... }, precisely because in that case we're not supposed to assume anything other than what assumptions we've been explicitly given)

nikomatsakis (Dec 09 2019 at 19:17, on Zulip):

ordinarily I'd write some of this logic in Rust code

nikomatsakis (Dec 09 2019 at 19:17, on Zulip):

but I wanted to express it in the trait solver

nikomatsakis (Dec 09 2019 at 19:17, on Zulip):

and right now it can't because it's always treating all lifetimes as equal, effectively

nikomatsakis (Dec 09 2019 at 19:18, on Zulip):

anyway, I can go more into that in a sec, but the same sort of problem is cropping up that causes the rust-analyzer infinite loop

Jack Huey (Dec 09 2019 at 19:19, on Zulip):

Ok, on laptop now

Jack Huey (Dec 09 2019 at 19:20, on Zulip):

Can you explain why this is ambiguous? https://github.com/rust-lang/chalk/blob/ba116c4d88f98358e9ff03eaa7fe84e6933fb377/tests/test/projection.rs#L454

Jack Huey (Dec 09 2019 at 19:20, on Zulip):

Related?

nikomatsakis (Dec 09 2019 at 19:20, on Zulip):

anyway, I can go more into that in a sec, but the same sort of problem is cropping up that causes the rust-analyzer infinite loop

I'm pondering this statement I made and wondering how true it is

nikomatsakis (Dec 09 2019 at 19:21, on Zulip):

in particular, if we "truncate" some of the environment and introduce inference variables

nikomatsakis (Dec 09 2019 at 19:21, on Zulip):

or really any part of the query

nikomatsakis (Dec 09 2019 at 19:21, on Zulip):

the resulting answer could include values for those variables

nikomatsakis (Dec 09 2019 at 19:21, on Zulip):

anyway what we do now is to "equate" the type that was replaced with a variable with the type that the answer gave back

nikomatsakis (Dec 09 2019 at 19:22, on Zulip):

and I was proposing that we could switch that to syntactic equality

nikomatsakis (Dec 09 2019 at 19:22, on Zulip):

but actually that seems...wrong

nikomatsakis (Dec 09 2019 at 19:22, on Zulip):

e.g., if we had a query like u32: Bar<i32> (say) and we chose to truncate that to u32: Bar<?T>

nikomatsakis (Dec 09 2019 at 19:23, on Zulip):

and then (from some impl) we get a result like ?T := <vec::IntoIter<i32> as Iterator>::Item

nikomatsakis (Dec 09 2019 at 19:23, on Zulip):

we'd prefer to determine that those are equal

nikomatsakis (Dec 09 2019 at 19:24, on Zulip):

e.g., if we had a query like u32: Bar<i32> (say) and we chose to truncate that to u32: Bar<?T>

this is the core mechanism of what we're doing, in case that wasn't clear; the assumption is that we can replace parts of the input with variables and that the solver will cope with that, though it may generate ambiguity where there was none before

nikomatsakis (Dec 09 2019 at 19:24, on Zulip):

Can you explain why this is ambiguous? https://github.com/rust-lang/chalk/blob/ba116c4d88f98358e9ff03eaa7fe84e6933fb377/tests/test/projection.rs#L454

anyway, about this test

detrumi (Dec 09 2019 at 19:25, on Zulip):

Why aren't we just leaving the i32 there? Wouldn't that make solving easier?

nikomatsakis (Dec 09 2019 at 19:25, on Zulip):

that ambiguity is not necessary, no, and I spent some time writing about various ways we might fix it in an issue somewhere

nikomatsakis (Dec 09 2019 at 19:26, on Zulip):

Why aren't we just leaving the i32 there? Wouldn't that make solving easier?

we do this when types get too big

nikomatsakis (Dec 09 2019 at 19:26, on Zulip):

in principle we can do it anywhere we like

Jack Huey (Dec 09 2019 at 19:26, on Zulip):

it's been a bit, so I can't remember the exact details of how the infinite loop happens (though I did make a comment about it on the issue)

nikomatsakis (Dec 09 2019 at 19:26, on Zulip):

the infinite loop arises because

nikomatsakis (Dec 09 2019 at 19:26, on Zulip):

we have an input like Foo: Bar<<T as Iterator>::Item>

nikomatsakis (Dec 09 2019 at 19:26, on Zulip):

we replace it with Foo: Bar<?X>

nikomatsakis (Dec 09 2019 at 19:27, on Zulip):

it turns out that the query results in an answer where we just have ?X unconstrained --

nikomatsakis (Dec 09 2019 at 19:27, on Zulip):

in particular we get back a mapping like forall<?Y> [ ?X := ?Y ]

Jack Huey (Dec 09 2019 at 19:27, on Zulip):

I don't think that's what's happening with this issue

nikomatsakis (Dec 09 2019 at 19:27, on Zulip):

to process this answer, we create a fresh inference variable for ?Y and then we equate the "old type" with it

nikomatsakis (Dec 09 2019 at 19:27, on Zulip):

so we have to prove that <T as Iterator>::Item = ?Y for this fresh variable

nikomatsakis (Dec 09 2019 at 19:27, on Zulip):

that in turn generates a new obligation for us to prove

Jack Huey (Dec 09 2019 at 19:27, on Zulip):

in never leaves that loop

nikomatsakis (Dec 09 2019 at 19:27, on Zulip):

but that new obligation also has an environment that is too big

nikomatsakis (Dec 09 2019 at 19:27, on Zulip):

i.e., it has the same environment we started with

nikomatsakis (Dec 09 2019 at 19:28, on Zulip):

which then gets truncated again, starting us back on this cycle

nikomatsakis (Dec 09 2019 at 19:28, on Zulip):

one way to side-step this particular case would be

nikomatsakis (Dec 09 2019 at 19:28, on Zulip):

to recognize that if you have a variable in the answer that only appears once, it's meaningless

nikomatsakis (Dec 09 2019 at 19:28, on Zulip):

I don't think that's what's happening with this issue

pretty sure it is

nikomatsakis (Dec 09 2019 at 19:28, on Zulip):

but not 100% sure :)

nikomatsakis (Dec 09 2019 at 19:28, on Zulip):

at least, that's what I observed when last I looked at it

nikomatsakis (Dec 09 2019 at 19:28, on Zulip):

maybe there are two problems?

nikomatsakis (Dec 09 2019 at 19:29, on Zulip):

in any case, the fix that I did in my branch was to say that if you have

Jack Huey (Dec 09 2019 at 19:29, on Zulip):

let me look over your comments once more real quickly

nikomatsakis (Dec 09 2019 at 19:29, on Zulip):

<T as Iterator>::Item = ?Y and ?Y is unconstrained,

Jack Huey (Dec 09 2019 at 19:29, on Zulip):

it might be right just reading it wrong

nikomatsakis (Dec 09 2019 at 19:29, on Zulip):

you can just equate ?T with <T as Iterator>::Item (i.e., the unnormalized form)

nikomatsakis (Dec 09 2019 at 19:29, on Zulip):

I dont' think this is wrong

nikomatsakis (Dec 09 2019 at 19:29, on Zulip):

but I think we used to have an invariant that we never unified a variable with an unnormalized projection

nikomatsakis (Dec 09 2019 at 19:29, on Zulip):

this might in turn be useful for things like being more specific about what impls we want

nikomatsakis (Dec 09 2019 at 19:30, on Zulip):

your fix was just to avoid truncating the environment

nikomatsakis (Dec 09 2019 at 19:30, on Zulip):

that also seems "ok for now"

Jack Huey (Dec 09 2019 at 19:30, on Zulip):

yes, that's right

nikomatsakis (Dec 09 2019 at 19:30, on Zulip):

my only hesitation was that, in general, we might move to a place where the environment can contain more variables

nikomatsakis (Dec 09 2019 at 19:30, on Zulip):

but today in Rust it doesn't really happen and maybe we just cross that bridge when we come to it

nikomatsakis (Dec 09 2019 at 19:31, on Zulip):

I think if we are going to do one of the two fixes I might prefer yours :)

nikomatsakis (Dec 09 2019 at 19:31, on Zulip):

it feels a bit more limited

Jack Huey (Dec 09 2019 at 19:31, on Zulip):

that was my thought

nikomatsakis (Dec 09 2019 at 19:31, on Zulip):

we can always have a pending FIXME explaining the motivation and then considering other alternatives later as we've made progress elsewhere

nikomatsakis (Dec 09 2019 at 19:31, on Zulip):

ok, I'm convinced

nikomatsakis (Dec 09 2019 at 19:31, on Zulip):

I can land that PR

Jack Huey (Dec 09 2019 at 19:32, on Zulip):

though definitely file a followup issue so we eventually try to write a test to break it again

detrumi (Dec 09 2019 at 19:32, on Zulip):

Jack's solution feels like we're doing a fix for the symptom and not the problem, while niko's fix feels like a fix for a specific instance of a more general problem

Jack Huey (Dec 09 2019 at 19:32, on Zulip):

Basically, yeah

nikomatsakis (Dec 09 2019 at 19:33, on Zulip):

Jack's solution feels like we're doing a fix for the symptom and not the problem, while niko's fix feels like a fix for a specific instance of a more general problem

yeah

nikomatsakis (Dec 09 2019 at 19:33, on Zulip):

I'd rather treat the problem but I think we don't quite know how yet

nikomatsakis (Dec 09 2019 at 19:33, on Zulip):

I guess in particular hm

Jack Huey (Dec 09 2019 at 19:33, on Zulip):

It's definitely going to overlap with #234 though

nikomatsakis (Dec 09 2019 at 19:33, on Zulip):

I wonder if the only bad scenario is this case where the answer actually gave back no real information

nikomatsakis (Dec 09 2019 at 19:34, on Zulip):

perhaps, perhaps not

nikomatsakis (Dec 09 2019 at 19:34, on Zulip):

that's the thing I'm not quite sure of :)

Jack Huey (Dec 09 2019 at 19:34, on Zulip):

fair enough

detrumi (Dec 09 2019 at 19:37, on Zulip):

Anyway, I agree that Jack's fix is the way to go for now, since we're not sure yet how to fix the problem, or where else it will pop up. The only danger is that we introduce special cases which we might forget to remove after the problem is fixed

Jack Huey (Dec 09 2019 at 19:38, on Zulip):

that ambiguity is not necessary, no, and I spent some time writing about various ways we might fix it in an issue somewhere

so, it should be unique ideally?

nikomatsakis (Dec 09 2019 at 19:38, on Zulip):

Yes. I think the question though is

nikomatsakis (Dec 09 2019 at 19:38, on Zulip):

where to detect that

nikomatsakis (Dec 09 2019 at 19:38, on Zulip):

I have so far been leaning towards making this the job of the "anti-unifier"

nikomatsakis (Dec 09 2019 at 19:38, on Zulip):

though in some ways it seems suboptimal

nikomatsakis (Dec 09 2019 at 19:38, on Zulip):

I guess I might as well walk through a bit what's going on there

nikomatsakis (Dec 09 2019 at 19:39, on Zulip):

since we have been chatting this much anyway :)

nikomatsakis (Dec 09 2019 at 19:39, on Zulip):

or should we keep it for a dedicated meeting?

nikomatsakis (Dec 09 2019 at 19:39, on Zulip):

I guess I can give the short version for now

Jack Huey (Dec 09 2019 at 19:39, on Zulip):

I wouldn't mind walking through it

Jack Huey (Dec 09 2019 at 19:39, on Zulip):

on my branches, I've actually gotten the to be unique

nikomatsakis (Dec 09 2019 at 19:39, on Zulip):

basically the problem is that, in general, there are two ways to deal with "projections". You can either think about them as placeholders or you can normalize them.

nikomatsakis (Dec 09 2019 at 19:40, on Zulip):

Sometimes you only have one route available

Jack Huey (Dec 09 2019 at 19:40, on Zulip):

though, I'm running into issues with the AntiUnifier

nikomatsakis (Dec 09 2019 at 19:40, on Zulip):

e.g., forall<T> { if (T: Iterator) { ... } }

Jack Huey (Dec 09 2019 at 19:40, on Zulip):

it's too dumb

nikomatsakis (Dec 09 2019 at 19:40, on Zulip):

in there, if you have a type T::Item

nikomatsakis (Dec 09 2019 at 19:40, on Zulip):

or, more accurately, <T as Iterator>::Item

nikomatsakis (Dec 09 2019 at 19:41, on Zulip):

there is really only one option for it, which is to think of it as a placeholder

nikomatsakis (Dec 09 2019 at 19:41, on Zulip):

in chalk we model this as a kind of "applicative" type

nikomatsakis (Dec 09 2019 at 19:41, on Zulip):

you might sometimes see (Iterator::Item)<T>

nikomatsakis (Dec 09 2019 at 19:41, on Zulip):

that is kind of the "placeholder" for <T as Iterator>::Item

nikomatsakis (Dec 09 2019 at 19:41, on Zulip):

it means "whatever the item type of T is"

nikomatsakis (Dec 09 2019 at 19:41, on Zulip):

the other option is that, if you can find an impl, you can normalize it

nikomatsakis (Dec 09 2019 at 19:42, on Zulip):

so e.g. <vec::IntoIter<i32> as Iterator>::Item can be normalized to i32

nikomatsakis (Dec 09 2019 at 19:42, on Zulip):

and of course sometimes we have information from our environment; in Rust notation, where T: Iterator<Item = u32>

nikomatsakis (Dec 09 2019 at 19:43, on Zulip):

anyway what we do in the compiler is to kind of have a "normalization" function that that tries to find an impl etc and falls back to the placeholder

nikomatsakis (Dec 09 2019 at 19:43, on Zulip):

that is kind of an "if (...) else if (...)"

nikomatsakis (Dec 09 2019 at 19:43, on Zulip):

this is not something that "plain logic" can model very well

nikomatsakis (Dec 09 2019 at 19:44, on Zulip):

so in chalk what we have more like two possible rules, one that says "normalize from an impl" and one that says "use the placeholder"

nikomatsakis (Dec 09 2019 at 19:44, on Zulip):

but this also means you get back two possible answers

nikomatsakis (Dec 09 2019 at 19:44, on Zulip):

in principle we could introduce some "cuts" or other things to kind of try one alterantive and -- if it fails -- try the other

nikomatsakis (Dec 09 2019 at 19:45, on Zulip):

but I'm a bit nervous about it

detrumi (Dec 09 2019 at 19:45, on Zulip):

That seems like a big step

nikomatsakis (Dec 09 2019 at 19:45, on Zulip):

there are some complex scenarios but also

nikomatsakis (Dec 09 2019 at 19:45, on Zulip):

there are times when you have recursion during normalization, at least you can -- I'd like to dig a more into rustc to help spell out some of the scenarios where I remember this cropping up

nikomatsakis (Dec 09 2019 at 19:46, on Zulip):

but suffice to say if we added cuts, we also have to address the question of cycles

nikomatsakis (Dec 09 2019 at 19:46, on Zulip):

e.g., if we are in the process of solving Normalize(<T as Iterator>::Item = ?U) and we wind up needing to solve that same query recursively --

nikomatsakis (Dec 09 2019 at 19:46, on Zulip):

does that mean we "failed to normalize"? and hence we can fallback to the placeholder?

nikomatsakis (Dec 09 2019 at 19:47, on Zulip):

but if we fallback then, what about the outer Normalize goal -- it may still succeed

nikomatsakis (Dec 09 2019 at 19:47, on Zulip):

and now we had a kind of inconsistency

nikomatsakis (Dec 09 2019 at 19:47, on Zulip):

This is why I was curious to see whether we could keep the current structure, which is naive but clear

nikomatsakis (Dec 09 2019 at 19:47, on Zulip):

but the problem with the current one is:

nikomatsakis (Dec 09 2019 at 19:47, on Zulip):
nikomatsakis (Dec 09 2019 at 19:47, on Zulip):

but also

nikomatsakis (Dec 09 2019 at 19:47, on Zulip):
Jack Huey (Dec 09 2019 at 19:48, on Zulip):

So, what I've been trying out locally is instead keeping track of basically what a projection "normalizes to" in the answer itself

nikomatsakis (Dec 09 2019 at 19:48, on Zulip):

(maybe this doesn't show up at the outer levels as two answers)

nikomatsakis (Dec 09 2019 at 19:49, on Zulip):

(side note: One of the things I had hoped to be true of chalk is that it let us kind of unify "normalizations" and other kinds of goals into one framework; that may just not work out as I had hoped, but oh well)

nikomatsakis (Dec 09 2019 at 19:49, on Zulip):

So, what I've been trying out locally is instead keeping track of basically what a projection "normalizes to" in the answer itself

say a bit more

Jack Huey (Dec 09 2019 at 19:49, on Zulip):

sure

Jack Huey (Dec 09 2019 at 19:50, on Zulip):

hold on, gonna try to find the test I'm thinking of

Jack Huey (Dec 09 2019 at 19:50, on Zulip):

https://github.com/rust-lang/chalk/blob/ba116c4d88f98358e9ff03eaa7fe84e6933fb377/tests/test/projection.rs#L123

Jack Huey (Dec 09 2019 at 19:51, on Zulip):

So, here the answers that we get back today are (Trait1::Type)<S> and u32

Jack Huey (Dec 09 2019 at 19:51, on Zulip):

And the aggregator can't aggregate these

Jack Huey (Dec 09 2019 at 19:52, on Zulip):

instead, the answers could be (Trait1::Type)<S> (the unnormalized placeholder) and (Trait1::Type)<S> as u32 (the normalized type)

Jack Huey (Dec 09 2019 at 19:52, on Zulip):

Then the aggregator can aggregate these

Jack Huey (Dec 09 2019 at 19:52, on Zulip):

Which, this doesn't seem too effective alone

Jack Huey (Dec 09 2019 at 19:53, on Zulip):

But you can also think about the case where there may be multiple answers (not just one)

nikomatsakis (Dec 09 2019 at 19:53, on Zulip):

yeah so I was imaining just having the aggregator see

nikomatsakis (Dec 09 2019 at 19:53, on Zulip):

if there are two types, and one of them is a placeholder

nikomatsakis (Dec 09 2019 at 19:53, on Zulip):

it can go ahead and try to normalize the placeholder to the other type

nikomatsakis (Dec 09 2019 at 19:53, on Zulip):

if that succeeds, it can discard the placeholder

nikomatsakis (Dec 09 2019 at 19:53, on Zulip):

but i'm not sure how easy that would be to do in practice :)

nikomatsakis (Dec 09 2019 at 19:54, on Zulip):

this would however be a boolean query

nikomatsakis (Dec 09 2019 at 19:54, on Zulip):

it would have at most one answer, in other words

Jack Huey (Dec 09 2019 at 19:54, on Zulip):

So, so you have (Trait1::Type)<S> as u32 and (Trait1::Type)<T> as i32

nikomatsakis (Dec 09 2019 at 19:54, on Zulip):

sure, that can happen, but that's ok

nikomatsakis (Dec 09 2019 at 19:54, on Zulip):

those are distinct types

Jack Huey (Dec 09 2019 at 19:54, on Zulip):

the aggregator could change this to (Trait1::Type)<?0>

Jack Huey (Dec 09 2019 at 19:55, on Zulip):

(I wrote an actually test in one my branches, but a bit distracted, so I'll have to find it later)

nikomatsakis (Dec 09 2019 at 19:55, on Zulip):

I guess I'm nervous about tracking the normalization this way

nikomatsakis (Dec 09 2019 at 19:55, on Zulip):

though I'm trying to put my finger on why

Jack Huey (Dec 09 2019 at 19:55, on Zulip):

That's fair enough

nikomatsakis (Dec 09 2019 at 19:56, on Zulip):

I was going to say that I don't like to have multiple equal representations or a type, but of course we do today, which is sort of the whole problem

nikomatsakis (Dec 09 2019 at 19:56, on Zulip):

I guess also i'm not sure I see that it solves the underlying challenge

Jack Huey (Dec 09 2019 at 19:56, on Zulip):

I've also played with removing the placeholder type entirely

nikomatsakis (Dec 09 2019 at 19:56, on Zulip):

( or at least not in a better way that having the aggregator do a normalization query, though I should try to determine what I mean by "better" there )

nikomatsakis (Dec 09 2019 at 19:56, on Zulip):

that said, there are some other alterantvies

nikomatsakis (Dec 09 2019 at 19:57, on Zulip):

for example, there's a paper that aims to handle normalization in a haskell context

Jack Huey (Dec 09 2019 at 19:57, on Zulip):

I saw that

nikomatsakis (Dec 09 2019 at 19:57, on Zulip):

I think that amounts to taking more the approach I was outlining in the beginning, at least from what I glean so far from reading and pondering it

nikomatsakis (Dec 09 2019 at 19:57, on Zulip):

basically trying to make normalization be more of a function that converts things to a canonical form

Jack Huey (Dec 09 2019 at 19:57, on Zulip):

How would the aggregator handle (Trait1::Type)<S> u32 (Trait1::Type)<T> i32

Jack Huey (Dec 09 2019 at 19:58, on Zulip):

especially if u32 and i32 came first?

nikomatsakis (Dec 09 2019 at 19:58, on Zulip):

it would just give ?X

Jack Huey (Dec 09 2019 at 19:58, on Zulip):

(since order isn't specified)

nikomatsakis (Dec 09 2019 at 19:58, on Zulip):

but that seems ok

nikomatsakis (Dec 09 2019 at 19:58, on Zulip):

I am not convinced we should handle that case, I guess

Jack Huey (Dec 09 2019 at 19:58, on Zulip):

let me see if I can find the test case

nikomatsakis (Dec 09 2019 at 19:58, on Zulip):

in particular that's a kind of weird answer

nikomatsakis (Dec 09 2019 at 19:58, on Zulip):

it's saying "the answer is some Type projected from something (but I don't know what)"

nikomatsakis (Dec 09 2019 at 19:59, on Zulip):

that maybe true for some values of something

nikomatsakis (Dec 09 2019 at 19:59, on Zulip):

but likely not all

nikomatsakis (Dec 09 2019 at 19:59, on Zulip):

and it is sort of not... required to project Type from something to reach that answer, right?

nikomatsakis (Dec 09 2019 at 19:59, on Zulip):

in other words, the aggregator is supposed to be giving back things that are "required" -- the only query that could succeed would be one that included these components

Jack Huey (Dec 09 2019 at 19:59, on Zulip):

https://github.com/rust-lang/chalk/compare/master...jackh726:associated_types#diff-055bea933f4bb1135dd71fa066e5d457R1301

nikomatsakis (Dec 09 2019 at 19:59, on Zulip):

this is a bit of a weird case because the two things are kind of aliases for one another

nikomatsakis (Dec 09 2019 at 20:00, on Zulip):

( yeah, I guess I feel ok with coming back with ? in that case )

nikomatsakis (Dec 09 2019 at 20:01, on Zulip):

but it is somewhat interesting

Jack Huey (Dec 09 2019 at 20:01, on Zulip):

So with that test, you could give back?0 = ^0, ?1 = (Trait1::Type)<^0>

nikomatsakis (Dec 09 2019 at 20:02, on Zulip):

ok, we're at the end of an hour, but this was a good intro, let's dive deeper next time, in the meantime I want to push a bit more on that hackmd :P -- also, I'd like to merge your PR @Jack Huey, though I think I want to add my test case to it

Jack Huey (Dec 09 2019 at 20:02, on Zulip):

yeah I have to go

Jack Huey (Dec 09 2019 at 20:02, on Zulip):

I added the test :)

Jack Huey (Dec 09 2019 at 20:02, on Zulip):

We can make a hackmd for this

Jack Huey (Dec 09 2019 at 20:02, on Zulip):

I'll also link my branches for later

Jack Huey (Dec 09 2019 at 20:02, on Zulip):

(or in the hackmd)

detrumi (Dec 09 2019 at 20:03, on Zulip):

Can one of you link that paper as well?

nikomatsakis (Dec 09 2019 at 20:03, on Zulip):

hackmd for normalization, next meeting

nikomatsakis (Dec 09 2019 at 20:03, on Zulip):

feel free to add notes there etc

Jack Huey (Dec 09 2019 at 20:05, on Zulip):

I'll add the paper

Jack Huey (Dec 09 2019 at 20:06, on Zulip):

Another thought for next week is if we actually need Normalize or if we can get away with just ProjectionEq. They seem redundant.

nikomatsakis (Dec 09 2019 at 20:08, on Zulip):

Yeah, I'm trying to remember why we have both. I don't think they're redundant but they may be. When we introducd these changes we had a different solver than was less general, and we may have been trying to work around some of its limitations (@scalexm may remember, but I doubt it, it was a while ago).

Last update: Jun 07 2020 at 09:45UTC