Stream: t-lang

Topic: const pattern match semantics #67343


pnkfelix (Apr 28 2020 at 21:18, on Zulip):

I honestly cannot remember to what level of detail we had discussed this, so I wanted to try to check here first:

pnkfelix (Apr 28 2020 at 21:20, on Zulip):

I am pretty sure we had previously agreed to adopt @ecstatic-morse 's approach for using a MIR "value-based" semantics for validating that all parts of a const in a pattern match implement PartialEq and Eq via #[derive(..)]

pnkfelix (Apr 28 2020 at 21:20, on Zulip):

But the thing I am not certain about is whether we had all agreed that we were okay with using a value-based semantics across crate boundaries

pnkfelix (Apr 28 2020 at 21:21, on Zulip):

(the main alternative I could imagine is to use a type-based semantics across crate boundaries)

pnkfelix (Apr 28 2020 at 21:23, on Zulip):

I guess the point of this is that whether crate authors will realize that changing the value of a const item such that it becomes not structurally-matchable will break downstream crates.

nikomatsakis (Apr 28 2020 at 21:23, on Zulip):

I have no memory of this :)

nikomatsakis (Apr 28 2020 at 21:23, on Zulip):

but at this point I just want it resolved

pnkfelix (Apr 28 2020 at 21:23, on Zulip):

The relevant note from PR #67343 is in its description; I will copy it here for ease of reference:

AFAIK, it's not settled that these are the semantics we actually want: it's just how the Qualif framework happens to work. If the cross-crate part is undesirable, it would be quite easy to change the result of mir_const_qualif().custom_eq to true before encoding it in the crate metadata. This way, other crates would have to assume that all publicly exported constants may not be safe for matching.

nikomatsakis (Apr 28 2020 at 21:24, on Zulip):

that said, I do think that -- in general -- one canot change const values without breakage, right?

pnkfelix (Apr 28 2020 at 21:24, on Zulip):

nikomatsakis said:

that said, I do think that -- in general -- one canot change const values without breakage, right?

I was indeed wondering that as I was typing

pnkfelix (Apr 28 2020 at 21:24, on Zulip):

and if that is the case, then maybe I am making a mountain out of a molehill

nikomatsakis (Apr 28 2020 at 21:24, on Zulip):

well, it comes I guess to how we wind up settling on equality but

pnkfelix (Apr 28 2020 at 21:25, on Zulip):

In any case, I get the impression that it would be quite easy for @ecstatic-morse to adopt the more conservative semantics

nikomatsakis (Apr 28 2020 at 21:25, on Zulip):

this builds for sure

const A: usize = 2;
const B: usize = 2;

fn main() {
    let mut x: [u32; A] = [1, 2];
    let y: [u32; B] = [3, 4];
    x = y;
}
nikomatsakis (Apr 28 2020 at 21:25, on Zulip):

and I guess the same is true across crates

pnkfelix (Apr 28 2020 at 21:25, on Zulip):

nikomatsakis said:

well, it comes I guess to how we wind up settling on equality but

hmm, I had thought in either case (with or without cross-crate support), we would still be equally able to support structural or semantic equality, no?

nikomatsakis (Apr 28 2020 at 21:26, on Zulip):

I remember talking about this topic a lot with @Ariel Ben-Yehuda and @eddyb years back but I kind of lost track on this question

pnkfelix (Apr 28 2020 at 21:26, on Zulip):

My suspicion is that this is fine

nikomatsakis (Apr 28 2020 at 21:26, on Zulip):

to me it's always been the "key" thing to think and discuss with const generics so I'm frustrated that I don't have a crisp articulation of the current thinking :)

pnkfelix (Apr 28 2020 at 21:27, on Zulip):

i.e. that supporting the cross-crate thing here is fine. (In particular, I'm betting that if there was some problem with it, @eddyb would have raised a ruckus with respect to this PR a long time ago...)

nikomatsakis (Apr 28 2020 at 21:27, on Zulip):

pnkfelix said:

hmm, I had thought in either case (with or without cross-crate support), we would still be equally able to support structural or semantic equality, no?

I'm not sure I understand

pnkfelix (Apr 28 2020 at 21:27, on Zulip):

nikomatsakis said:

I'm not sure I understand

pnkfelix (Apr 28 2020 at 21:27, on Zulip):

well

pnkfelix (Apr 28 2020 at 21:28, on Zulip):

the linked PR is still in service of us being ambivalent of the choice between structural or semantic equality for consts in patterns

pnkfelix (Apr 28 2020 at 21:28, on Zulip):

and thus

pnkfelix (Apr 28 2020 at 21:28, on Zulip):

I had figured

pnkfelix (Apr 28 2020 at 21:28, on Zulip):

even if it allows the more expressive form across crates

pnkfelix (Apr 28 2020 at 21:28, on Zulip):

it is still going to be something where the only code that is accepted

pnkfelix (Apr 28 2020 at 21:29, on Zulip):

is code that is compatible with structural match or use of PartialEq::eq for its semantics

nikomatsakis (Apr 28 2020 at 21:29, on Zulip):

I see

nikomatsakis (Apr 28 2020 at 21:30, on Zulip):

Something else that I had remembered but I am now re-remembering

nikomatsakis (Apr 28 2020 at 21:30, on Zulip):

is that equality in const generics

nikomatsakis (Apr 28 2020 at 21:30, on Zulip):

will presumably not be based on PartialEq

nikomatsakis (Apr 28 2020 at 21:30, on Zulip):

but rather a different notion of equality

pnkfelix (Apr 28 2020 at 21:30, on Zulip):

having said that, it will be pretty wild if we use structural semantics for constants that are defined like const C = if TEST { E::Var1 } else { E::Var2 };

nikomatsakis (Apr 28 2020 at 21:31, on Zulip):

which is kind of neither here nor there I guess

nikomatsakis (Apr 28 2020 at 21:31, on Zulip):

pnkfelix said:

having said that, it will be pretty wild if we use structural semantics for constants that are defined like const C = if TEST { E::Var1 } else { E::Var2 };

yes

nikomatsakis (Apr 28 2020 at 21:31, on Zulip):

similarly const X = some_const_fn(...);

nikomatsakis (Apr 28 2020 at 21:31, on Zulip):

though you might want it, it's very unclear

pnkfelix (Apr 28 2020 at 21:32, on Zulip):

ooh boy

pnkfelix (Apr 28 2020 at 21:32, on Zulip):

nikomatsakis said:

but rather a different notion of equality

was this due to floating point NaN issues? Or something else?

nikomatsakis (Apr 28 2020 at 21:35, on Zulip):

well

nikomatsakis (Apr 28 2020 at 21:35, on Zulip):

the obvious example is impl PartialEq for MyType { fn is_eq(&self) -> bool { false } }

nikomatsakis (Apr 28 2020 at 21:35, on Zulip):

two things might be "equal" constants (same bitpatterns) but not equal at runtime

pnkfelix (Apr 28 2020 at 21:35, on Zulip):

right

nikomatsakis (Apr 28 2020 at 21:35, on Zulip):

this is very "close" to the pattern questions

pnkfelix (Apr 28 2020 at 21:35, on Zulip):

that's the classic example that I reference

pnkfelix (Apr 28 2020 at 21:35, on Zulip):

but

pnkfelix (Apr 28 2020 at 21:35, on Zulip):

I would think that

pnkfelix (Apr 28 2020 at 21:36, on Zulip):

if we commit to so-called semantic equality

pnkfelix (Apr 28 2020 at 21:36, on Zulip):

i.e. if we commit to dispatching to PartialEq::eq

pnkfelix (Apr 28 2020 at 21:36, on Zulip):

then all such matches on MyType will just fail?

nikomatsakis (Apr 28 2020 at 21:36, on Zulip):

but I'm talking about const generics equality

nikomatsakis (Apr 28 2020 at 21:36, on Zulip):

e.g., given const C: MyType = .., are Foo<C> and Foo<C> equal types?

pnkfelix (Apr 28 2020 at 21:37, on Zulip):

oh right

nikomatsakis (Apr 28 2020 at 21:37, on Zulip):

what about Foo<C> and Foo<D> where C and D are two distinct constants with same bit pattern

pnkfelix (Apr 28 2020 at 21:37, on Zulip):

you all keep reconnecting these two things

nikomatsakis (Apr 28 2020 at 21:37, on Zulip):

they are distinct for sure

pnkfelix (Apr 28 2020 at 21:37, on Zulip):

and I keep acting like we can treat match as living in its own little bubble

nikomatsakis (Apr 28 2020 at 21:37, on Zulip):

pattern matching is a runtime operation

nikomatsakis (Apr 28 2020 at 21:37, on Zulip):

but

nikomatsakis (Apr 28 2020 at 21:37, on Zulip):

I guess I'm just saying that we will have two notions of equality

pnkfelix (Apr 28 2020 at 21:37, on Zulip):

nikomatsakis said:

is that equality in const generics

when you wrote this, I read it as "matching of associated consts"

nikomatsakis (Apr 28 2020 at 21:37, on Zulip):

and some of the concerns, e.g., wanting to know that we always have a place to branch to

nikomatsakis (Apr 28 2020 at 21:37, on Zulip):

or exhaustiveness etc

pnkfelix (Apr 28 2020 at 21:37, on Zulip):

which is not at all what you wrote, of course

nikomatsakis (Apr 28 2020 at 21:38, on Zulip):

seem related

nikomatsakis (Apr 28 2020 at 21:38, on Zulip):

I guess it softens me to the "two notions" of equality, if we can make the "static-y" equality for const generics and pattern matching kind of line up

pnkfelix (Apr 28 2020 at 21:38, on Zulip):

well my point is that in the end, we can always fall back on having match arms fail to fire

nikomatsakis (Apr 28 2020 at 21:38, on Zulip):

as long as there is an _ arm...

pnkfelix (Apr 28 2020 at 21:38, on Zulip):

sure

pnkfelix (Apr 28 2020 at 21:39, on Zulip):

presumably the exhautiveness checker will give up in cases where you did not derive the PartialEq impl

nikomatsakis (Apr 28 2020 at 21:39, on Zulip):

I'm sort of looking for an excuse to give up and embrace the "syntactic equality", I guess :)

pnkfelix (Apr 28 2020 at 21:39, on Zulip):

and thus you will get errors if you leave out _ => ...

pnkfelix (Apr 28 2020 at 21:39, on Zulip):

Wouldn't it be great

pnkfelix (Apr 28 2020 at 21:39, on Zulip):

if we used NaN

pnkfelix (Apr 28 2020 at 21:39, on Zulip):

as an excuse

pnkfelix (Apr 28 2020 at 21:39, on Zulip):

to embrace syntactic equality

pnkfelix (Apr 28 2020 at 21:40, on Zulip):

such totally unrelated linguistic elements

pnkfelix (Apr 28 2020 at 21:40, on Zulip):

but also

pnkfelix (Apr 28 2020 at 21:40, on Zulip):

hmm

pnkfelix (Apr 28 2020 at 21:40, on Zulip):

/me wonders about the Foo<C> example

pnkfelix (Apr 28 2020 at 21:42, on Zulip):

like, okay: You go ahead and put in non equivalence relation as your impl PartialEq for MyType ... So in the worst case, if we did use semantic equality even at the type level

pnkfelix (Apr 28 2020 at 21:42, on Zulip):

(and, i dunno, used miri within the type checker)

pnkfelix (Apr 28 2020 at 21:42, on Zulip):

ignoring the engineering issues that arise

pnkfelix (Apr 28 2020 at 21:42, on Zulip):

Just in terms of user experience: What's the worst that happens?

Josh Triplett (Apr 28 2020 at 21:43, on Zulip):

pnkfelix said:

But the thing I am not certain about is whether we had all agreed that we were okay with using a value-based semantics across crate boundaries

When we discussed it in the meeting, that topic didn't come up at all. I do personally agree that cross-crate doesn't need special handling.

pnkfelix (Apr 28 2020 at 21:44, on Zulip):

Someone sees some truly bonkers behavior where the compiler rejects things like the assignment x = x; because the type-checker claims typeof(x) != typeof(x) ?

pnkfelix (Apr 28 2020 at 21:44, on Zulip):

The main problem I see there is that, ideally, you'd want very specific feedback about why the expected and actual types are different

nikomatsakis (Apr 28 2020 at 21:44, on Zulip):

yeah but also

nikomatsakis (Apr 28 2020 at 21:45, on Zulip):

if you have a PartialEq whose comparison function is not a const fn

nikomatsakis (Apr 28 2020 at 21:45, on Zulip):

it can't be compared

nikomatsakis (Apr 28 2020 at 21:45, on Zulip):

so we either have to forbid those types from being used as const generics..

nikomatsakis (Apr 28 2020 at 21:45, on Zulip):

I think that was what bothered me, that it introduced a kind of "class" of types

nikomatsakis (Apr 28 2020 at 21:45, on Zulip):

that is sort of ad-hoc

pnkfelix (Apr 28 2020 at 21:46, on Zulip):

I assume in this hypothetical universe, people would actually declare their partial eq method to be a const fn

pnkfelix (Apr 28 2020 at 21:46, on Zulip):

it would not be e.g. inferred from the structure of its body

pnkfelix (Apr 28 2020 at 21:47, on Zulip):

Josh Triplett said:

pnkfelix said:

But the thing I am not certain about is whether we had all agreed that we were okay with using a value-based semantics across crate boundaries

When we discussed it in the meeting, that topic didn't come up at all. I do personally agree that cross-crate doesn't need special handling.

Okay I'm glad I brought this up, at least. I don't know whether we need to make it part of this week's agenda, but I suppose it woudn't hurt. I don't think we need to block landing this PR on it.

pnkfelix (Apr 28 2020 at 21:47, on Zulip):

(because I believe that it would be easy to toggle to the other semantics if we did decide in the meeting that would be preferable.)

pnkfelix (Apr 28 2020 at 21:47, on Zulip):

I'll add this as an agenda item.

Asa Zeren (Apr 28 2020 at 21:48, on Zulip):

pnkfelix said:

I assume in this hypothetical universe, people would actually declare their partial eq method to be a const fn

How would that interact with #[derive(PartialEq)]? Would the derived impl be const sometimes, always, or never.

pnkfelix (Apr 28 2020 at 21:49, on Zulip):

... hmm. I had assumed that if you were able to make arbitrary methods of an impl into const fn (assuming their bodies were compatible with being const fn), then we could make derive(PartialEq) do so...

pnkfelix (Apr 28 2020 at 21:49, on Zulip):

I suppose there may be things the derived partial eq impl does today that are not expressible in const fn

pnkfelix (Apr 28 2020 at 21:49, on Zulip):

(e.g. inspecting the discriminant may not be legal in const fn today?)

pnkfelix (Apr 28 2020 at 21:50, on Zulip):

its been a long time since I messed around with the innards of those derives...

Josh Triplett (Apr 28 2020 at 21:50, on Zulip):

It'd be nice if all derive(PartialEq) calls were const if the fields' PartialEq impls are.

pnkfelix (Apr 28 2020 at 21:50, on Zulip):

Asa Zeren said:

How would that interact with #[derive(PartialEq)]? Would the derived impl be const sometimes, always, or never.

(I guess I was hoping the answer was "always", but now I do not know if that's possible...)

pnkfelix (Apr 28 2020 at 21:51, on Zulip):

Right: Of course you hit a problem with type parameters

pnkfelix (Apr 28 2020 at 21:51, on Zulip):

where a given generic type parameter may have a PartialEq implementation that is itself not a const fn impl ... sigh...

pnkfelix (Apr 28 2020 at 21:51, on Zulip):

okay maybe this is all ridiculous then

Asa Zeren (Apr 28 2020 at 21:51, on Zulip):

if partial eq only sometimes uses const fns, then there would be no source level indication, and so changing a type (including transitively) would mysteriously break things, and make it very easy to break semver

Asa Zeren (Apr 28 2020 at 21:52, on Zulip):

Perhaps one could go with a new trait ConstPartialEq or some such

pnkfelix (Apr 28 2020 at 21:52, on Zulip):

another approach would be an opt-in of some kind

pnkfelix (Apr 28 2020 at 21:52, on Zulip):

yeah, I was thinking more along the lines of derive(PartialEq(const)), but in any case

pnkfelix (Apr 28 2020 at 21:53, on Zulip):

some way to actually signal intent

pnkfelix (Apr 28 2020 at 21:53, on Zulip):

which, given how relatively rare generic constants are ... maybe that would be okay?

Asa Zeren (Apr 28 2020 at 21:53, on Zulip):

The nice thing about a trait is that it would remove the 'ad-hoc' classification of types.

pnkfelix (Apr 28 2020 at 21:53, on Zulip):

pretty hokey though

Josh Triplett (Apr 28 2020 at 21:53, on Zulip):

It feels like we need a more systematic way of handling const in traits.

Josh Triplett (Apr 28 2020 at 21:53, on Zulip):

(And functions, but especially traits.)

pnkfelix (Apr 28 2020 at 21:53, on Zulip):

nikomatsakis said:

I think that was what bothered me, that it introduced a kind of "class" of types

yeah now I think I understand what @nikomatsakis was getting at here

pnkfelix (Apr 28 2020 at 21:54, on Zulip):

anyway gotta go afk

pnkfelix (Apr 28 2020 at 21:54, on Zulip):

sorry for stirring the pot. :)

eddyb (Apr 29 2020 at 02:53, on Zulip):

pnkfelix said:

i.e. that supporting the cross-crate thing here is fine. (In particular, I'm betting that if there was some problem with it, eddyb would have raised a ruckus with respect to this PR a long time ago...)

we already leak properties cross-crate like whether the value needs destructors or whether it contains UnsafeCell values

eddyb (Apr 29 2020 at 02:55, on Zulip):

as for const generics, we don't want to dispatch to user code at all. it's just not worth it, from a typesystem-must-be-sound-at-any-cost perspective

eddyb (Apr 29 2020 at 02:57, on Zulip):

but we do want to limit the types we allow in const generics to those with structural Eq, to avoid confusing semantics, and limit primitive leaf values to those that are effectively plain integers (while references behave as newtypes, not pointers, because of their by-value-eq semantics)

nikomatsakis (Apr 29 2020 at 10:38, on Zulip):

That last point is not obvious to me.

nikomatsakis (Apr 29 2020 at 10:39, on Zulip):

By which I just mean: it avoids confusing semantics, but it shuts out use cases too, and I'm not sure what is best -- especially as "structural equality" is this "latent concept" right now and not something users can declare. And if it becomes something users can declare, then that's adding another thing to have to understand.

nikomatsakis (Apr 29 2020 at 10:40, on Zulip):

Anyway I think it's a good question to defer for the moment, when it comes to const generics, which maybe implies it's ok to defer the question of match semantics too until we're further down the road.

nikomatsakis (Apr 29 2020 at 13:33, on Zulip):

@pnkfelix this comment by @oli and some of the replies are relevant, they talk about the 'opacity' of constant definitions vs const fn with respect to the "precise variant" analysis

varkor (Apr 29 2020 at 16:56, on Zulip):

Josh Triplett said:

It feels like we need a more systematic way of handling const in traits.

This in part seems like the focus of the generic parameters in const fn RFC. Maybe it's worth starting up a lang WG to discuss these sorts of issues more comprehensively and holistically?

varkor (Apr 29 2020 at 16:57, on Zulip):

(I'm definitely interested in being part of these discussions when they do happen.)

RalfJ (Apr 30 2020 at 06:55, on Zulip):

I also recently discovered that pattern matching places an entire new set of soundness concerns on const-eval that so far we have not explicitly documented anywhere, and that I was not aware of...

RalfJ (Apr 30 2020 at 06:57, on Zulip):

not sure if that has been discussed in this context already, but the fact that we do pattern-matching through arbitrary reference types places some serious restrictions on use of consts outside patterns. namely, it would otherwise be completely okay to have a const pointing to a (potentially mutable) static; with pattern matching however we must ensure that consts transitively do not point to anything mutable anywhere ever.

Josh Triplett (Apr 30 2020 at 07:01, on Zulip):

Why would it ever be acceptable to have a reference to a mutable thing and still be able to mutate that thing?

Josh Triplett (Apr 30 2020 at 07:02, on Zulip):

That seems like it violates the most fundamental property of the borrow checker.

RalfJ (Apr 30 2020 at 18:05, on Zulip):

at leas mutating it through that reference should be fine, right?

RalfJ (Apr 30 2020 at 18:05, on Zulip):

like, &mut SOMETHING_GLOBAL is a constant value, and there seems to be no harm in letting people put it in a constant

RalfJ (Apr 30 2020 at 18:06, on Zulip):

or, more likely, &SOMETHING_GLOBAL_WITH_INTERIOR_MUT

RalfJ (Apr 30 2020 at 18:07, on Zulip):

if it wasn't for patterns, consts could refer to interior mutable statics just fine (and there are no aliasing issues because of UnsafeCell)

Last update: Jun 05 2020 at 22:50UTC