Stream: wg-traits

Topic: panic: truncate extracted a pending value


Jack Huey (Jan 08 2020 at 20:14, on Zulip):

I've been investigating this issue a bit

Jack Huey (Jan 08 2020 at 20:14, on Zulip):

I think I've found the problem

Jack Huey (Jan 08 2020 at 20:14, on Zulip):

but wanted to ask you a question @nikomatsakis

Jack Huey (Jan 08 2020 at 20:15, on Zulip):

So, I'm using the higher_ranked_inline_bound_on_gat test with max_size of 3 to reproduce this

Jack Huey (Jan 08 2020 at 20:15, on Zulip):

And essentially what I think is wrong is:

Jack Huey (Jan 08 2020 at 20:16, on Zulip):

This goal LocalImplAllowed(for<1> fn<Ref<'^0, !1_1>>: Fn<Ref<'!1_0, !1_1>>) gets truncated to LocalImplAllowed(for<1> fn<?0>: Fn<Ref<'!1_0, !1_1>>)

Jack Huey (Jan 08 2020 at 20:16, on Zulip):

Then that second goal gets canonicalized into LocalImplAllowed(for<1> fn<^1>: Fn<Ref<'!1_0, !1_1>>)

Jack Huey (Jan 08 2020 at 20:16, on Zulip):

When I think it should get canonicalized into LocalImplAllowed(for<1> fn<^0>: Fn<Ref<'!1_0, !1_1>>)

Jack Huey (Jan 08 2020 at 20:17, on Zulip):

Or maybe LocalImplAllowed(for<1> fn<'^0>: Fn<Ref<'!1_0, !1_1>>)

Jack Huey (Jan 08 2020 at 20:19, on Zulip):

But anyways, when the answer for that goal is generated, and it is attempted to apply in apply_answer_subst and trys to unify Ref<'^0, !1_1> and ^1, it can't shift down by one because of the '^0 in the first

Jack Huey (Jan 08 2020 at 20:19, on Zulip):

When I think it should get canonicalized into LocalImplAllowed(for<1> fn<^0>: Fn<Ref<'!1_0, !1_1>>)

This is basically my question. Am I right here?

Jack Huey (Jan 09 2020 at 16:01, on Zulip):

@nikomatsakis Do you have a minute to quickly talk about this?

Jack Huey (Jan 09 2020 at 16:02, on Zulip):

Gonna be traveling today, so might be able to try to fix this

Jack Huey (Jan 09 2020 at 16:11, on Zulip):

Actually, I don't think that inference variable should be changed to a bound var at all here

Jack Huey (Jan 09 2020 at 16:12, on Zulip):

Actually, I don't think that inference variable should be changed to a bound var at all here

Jack Huey (Jan 09 2020 at 16:12, on Zulip):

Shoot okay, that's what it is

nikomatsakis (Jan 13 2020 at 15:36, on Zulip):

Hey @Jack Huey, I have a minute right now

nikomatsakis (Jan 13 2020 at 15:37, on Zulip):

This goal LocalImplAllowed(for<1> fn<Ref<'^0, !1_1>>: Fn<Ref<'!1_0, !1_1>>) gets truncated to LocalImplAllowed(for<1> fn<?0>: Fn<Ref<'!1_0, !1_1>>)

I think..this truncation is kind of wrong

nikomatsakis (Jan 13 2020 at 15:37, on Zulip):

I've been wondering about truncation, actually

nikomatsakis (Jan 13 2020 at 15:38, on Zulip):

In particular, I've been wondering if we should replace it with something like:

nikomatsakis (Jan 13 2020 at 15:38, on Zulip):

if a goal would be truncated, just replace it with CannotProve

Jack Huey (Jan 13 2020 at 16:28, on Zulip):

(removed)

Jack Huey (Jan 13 2020 at 16:29, on Zulip):

Yeah, I've had some thoughts about truncation

Jack Huey (Jan 13 2020 at 16:30, on Zulip):

bit scattered right now, but I think just replacing it with CannotProve might work, but I think there might be a better solution

Jack Huey (Jan 13 2020 at 16:31, on Zulip):

re. that truncation in particular, the more I thought about it, the more "wrong" it felt

Jack Huey (Jan 13 2020 at 16:31, on Zulip):

but I can't put my finger on why

nikomatsakis (Jan 13 2020 at 16:36, on Zulip):

if a goal would be truncated, just replace it with CannotProve

actually what I really wanted was to flounder it, I think

nikomatsakis (Jan 13 2020 at 16:36, on Zulip):

basically, it's a kind of error case

nikomatsakis (Jan 13 2020 at 16:37, on Zulip):

truncation was inspired by other solvers

nikomatsakis (Jan 13 2020 at 16:37, on Zulip):

it has a solid foundation, of sorts, in the sense that (in theory) the solvers ought to be able to enumerate the full set of solutions

nikomatsakis (Jan 13 2020 at 16:37, on Zulip):

but I think for a variety of practical reasons that doesn't make sense in our setting

Jack Huey (Jan 13 2020 at 16:38, on Zulip):

It seems like other than perf, all of rust-analyzer's issues have been from truncation

nikomatsakis (Jan 13 2020 at 16:39, on Zulip):

I basically think we should consider truncation an error case

nikomatsakis (Jan 13 2020 at 16:39, on Zulip):

i.e., it's not supposed to happen

nikomatsakis (Jan 13 2020 at 16:39, on Zulip):

this was always the idea

Jack Huey (Jan 13 2020 at 16:40, on Zulip):

in my branches to fix the other issue (https://github.com/jackh726/chalk/tree/ambiguous_as_cannotprove), I used CannotProve as a delayed_subgoal in the case of truncation

nikomatsakis (Jan 13 2020 at 16:40, on Zulip):

rustc has a similar policy around large types, but it just aborts compilation

nikomatsakis (Jan 13 2020 at 16:40, on Zulip):

I suspect we should just do the same

Jack Huey (Jan 13 2020 at 16:40, on Zulip):

could be worth trying

nikomatsakis (Jan 13 2020 at 16:42, on Zulip):

but it will require us to probably fix some other problems for r-a

Jack Huey (Jan 13 2020 at 16:43, on Zulip):

Biggest is perf I think

Jack Huey (Jan 13 2020 at 16:43, on Zulip):

(you already saw my solve_limited PR)

Jack Huey (Jan 14 2020 at 05:39, on Zulip):

@nikomatsakis floundering instead of truncating: https://github.com/rust-lang/chalk/pull/322

Jack Huey (Jan 14 2020 at 21:21, on Zulip):

@nikomatsakis you around?

Jack Huey (Jan 14 2020 at 22:45, on Zulip):

@matklad you might be interested in testing out this branch with rust-analyzer, since it should fix a lot of bugs? impl Trait has returned yet, though

Jack Huey (Jan 14 2020 at 22:46, on Zulip):

And off topic, but I'm also curious of your thoughts on: https://github.com/rust-lang/chalk/pull/321

matklad (Jan 14 2020 at 22:46, on Zulip):

I've tried to point Rust-analyzer to it, but hit some compiler errors. Looks like an API might have changed in the recent chalk. I haven't looked into this further though. cc @Florian Diebold :D

Jack Huey (Jan 14 2020 at 22:47, on Zulip):

e.g. would being able to stop Chalk solving via a should_panic Fn be sufficient for now?

matklad (Jan 14 2020 at 23:00, on Zulip):

What's should_panic? I only see should_continue

matklad (Jan 14 2020 at 23:01, on Zulip):

But I think I like should_continue -- seems the minimal thing that can possible work for our use-case

Jack Huey (Jan 14 2020 at 23:05, on Zulip):

Oops, typo. should_continue

Jack Huey (Jan 14 2020 at 23:05, on Zulip):

Basically, is being able to stop solving based solely on time a good start for now?

matklad (Jan 14 2020 at 23:06, on Zulip):

Hm, that makes me think....

If chalk supports should_continue in that PR, does that mean that https://github.com/rust-lang/chalk/issues/260 is also fixed?

matklad (Jan 14 2020 at 23:06, on Zulip):

I imagine that these are actually more-or-less equivalent

Jack Huey (Jan 14 2020 at 23:09, on Zulip):

No, it's still not UnwindSafe

Jack Huey (Jan 14 2020 at 23:09, on Zulip):

I have some thoughts on how to make it so, but it's a bit low priority right now

Last update: Jan 21 2020 at 09:00UTC