Stream: wg-traits

Topic: associated types and normalization


Jack Huey (Dec 23 2019 at 18:36, on Zulip):

So @nikomatsakis I was going through last week's design meeting to update the minutes, and thought about something in regards to the not direction for designing whether to use the placeholder type

Jack Huey (Dec 23 2019 at 18:37, on Zulip):

So, I haven't looked at the code yet, and don't quite remember

Jack Huey (Dec 23 2019 at 18:37, on Zulip):

but can we ever know that there doesn't exist an impl for a type?

Jack Huey (Dec 23 2019 at 18:37, on Zulip):

(because of downstream impls?)

Jack Huey (Dec 23 2019 at 18:38, on Zulip):

I guess this overlaps with coherence rules, but I feel like we get into a grey area here

Jack Huey (Dec 23 2019 at 18:38, on Zulip):

Where in some cases we can use the placeholder, and in some cases that not { exists ... goal is CannotProve

nikomatsakis (Dec 24 2019 at 11:31, on Zulip):

but can we ever know that there doesn't exist an impl for a type?

Funny you should ask about this. I've just been pondering it. You may enjoy Aaron's blog post on negative reasoning and modal logic from some time ago, which explains a few things here.

Last update: Jun 07 2020 at 09:35UTC