Always == not = in where clauses

[josh11b]

Instead of having two different operators and semantics when constraining an associated type to be equal to another type variable versus a concrete type, unify the semantics and consistently use just the == operator in where clauses.

[jonmeow]

Seems like a good change to me. I might remark = feels like assignment, but where feels more like a condition. It might particularly be worth noting that in examples like let PointT:! NSpacePoint where .N = 2;, let supports assignment following so using == to make it read less like an assignment might improve readability.

[josh11b]

It might particularly be worth noting that in examples like let PointT:! NSpacePoint where .N = 2;, let supports assignment following so using == to make it read less like an assignment might improve readability.

I added this rationale to the alternatives considered: fefcce6

[zygoloid]

Looks good to me.

[zygoloid]

Aside: do we have rules on how the types of the expressions on either side of == should correspond? What I implemented in explorer was: there must either be an implicit conversion from LHS to RHS or from RHS to LHS. I suppose we should probably use the same unification rules that if ... then ... else uses?

[josh11b]

I'm not sure what the question is. There will be lots of situations where you will write T:! C where .A == U.B and there won't be any correspondence between T.A and U.B, including no implicit conversions.

[zygoloid]

Here's an example:

interface C { let A:! Type; }
interface D { let B:! i32; }
fn F[U:! D, T:! C where .A == U.B]();

I would expect that we want to reject this, because the types of T.A and U.B (Type and i32) are unrelated. But if the type of T.A is some type-of-type and the type of U.B is some other type-of-type, I think we want to accept. And similarly if the type of T.A is i32 and the type of U.B is i64, I think we probably want to accept.

[josh11b]

I see. I didn't understand since the wording of this sentence and the title of this section restricts it to type variables, but I agree this document should address that point.

Should we require the compiler to detect cases where the constraints on two equal type variables are incompatible, as in:

interface D { let A:! Type; }
interface E { let B:! D where .A == i32; }
interface F { let C:! D where .A == bool; }
fn F[T:! E, U:! F where .C == T.B](x: T, y: U);

[josh11b]

What I implemented in explorer was: there must either be an implicit conversion from LHS to RHS or from RHS to LHS. I suppose we should probably use the same unification rules that if ... then ... else uses?

It seems like we should use the == operator? It does have concerns:

• Not clear if the user's operator== code can be executed at compile-time.
• Not clear if the compiler can reason about what arbitrary user == code means.

[zygoloid]

Hm, I'm concerned that using == isn't sufficient. That would give us a predicate by which we can tell whether the two associated constants are equal, but we also want to be able to use one in the place of the other, which I think we can't do if there's an arbitrary == comparing them. Here's an example of the kind of thing I'm worried about:

class A {
  var a: i32;
  external impl as ImplicitAs(i32) { fn Convert[me: Self]() -> i32 { return 0; } }
}
class B {
  var b: i32;
  external impl as ImplicitAs(i32) { fn Convert[me: Self]() -> i32 { return 1; } }
}
external impl A as EqWith(B) {
  fn Op[me: Self](b: B) -> bool { return me.a == b.b; }
}
class X(n:! i32) {}
interface Q {
  let AV:! A;
  let BV:! B;
  let N:! i32;
}
fn F[QT: Q where .AV == .BV]() {
  var v: X(QT.AV) = {};
  var w: X(QT.BV) = v;
}

We want to know if X(QT.AV) and X(QT.BV) are the same type. We have an equality in scope: where QT.AV == QT.BV. But the fact that the EqWith operation between those values returns true isn't enough for us to conclude that X(QT.AV) is the same as X(QT.BV), because in general == returning true doesn't mean that the values are substitutable for each other.

I don't have a real answer here. It seems like conversions that are not fully value-preserving and round-trippable shouldn't be allowed on the operands of == if we want to allow these kinds of semantic substitutions, but I do want to allow A:! Q where .N == 5, and we will presumably not be able to convert from the type of N to the type of 5, and I want X(A.N) and X(5) to be considered to be the same type in that context, so some amount of difference in type should be OK.

[josh11b]

Should I use the "there must either be an implicit conversion from LHS to RHS or from RHS to LHS" rule you implemented in explorer?

[zygoloid]

I don't know what rule is best. I think these cases are unproblematic and important:

• Both sides are types (.MyType == Other.YourType).
• One side is a constant and it converts to the type of the other side (.N == 5).

Can we say for now that we allow those cases and no others? (With a TODO to revisit this once we know more about what we want here.)

[josh11b]

Updated: e1c2e0e

[zygoloid]

I wonder if it's worth mentioning the case of a where appearing within an impl here. That's one case where I think = rather than == is a bit less surprising, because it does feel a bit more like you're setting the value of an associated constant.

[josh11b]

Added edf74bf

[josh11b]

I'm going to withdraw this proposal in favor of #2173 .