# Associated constant assignment versus equality

<!--
Part of the Carbon Language project, under the Apache License v2.0 with LLVM
Exceptions. See /LICENSE for license information.
SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
-->

[Pull request](https://github.com/carbon-language/carbon-lang/pull/2173)

<!-- toc -->

## Table of contents

-   [Abstract](#abstract)
-   [Problem](#problem)
    -   [Equal types with different interfaces](#equal-types-with-different-interfaces)
    -   [Type canonicalization](#type-canonicalization)
    -   [Transitivity of equality](#transitivity-of-equality)
    -   [Coherence](#coherence)
-   [Background](#background)
-   [Proposal](#proposal)
-   [Details](#details)
    -   [Rewrite constraints](#rewrite-constraints)
    -   [Combining constraints with `&`](#combining-constraints-with-)
    -   [Combining constraints with `and`](#combining-constraints-with-and)
    -   [Combining constraints with `extends`](#combining-constraints-with-extends)
    -   [Combining constraints with `impl as` and `is`](#combining-constraints-with-impl-as-and-is)
    -   [Constraint resolution](#constraint-resolution)
    -   [Precise rules and termination](#precise-rules-and-termination)
        -   [Qualified name lookup](#qualified-name-lookup)
        -   [Type substitution](#type-substitution)
        -   [Examples](#examples)
        -   [Termination](#termination)
    -   [Same type constraints](#same-type-constraints)
        -   [Implementation of same-type `ImplicitAs`](#implementation-of-same-type-implicitas)
    -   [Observe declarations](#observe-declarations)
    -   [Implementing an interface](#implementing-an-interface)
    -   [Ergonomics](#ergonomics)
    -   [Implementation experience](#implementation-experience)
-   [Rationale](#rationale)
-   [Alternatives considered](#alternatives-considered)
    -   [Status quo](#status-quo)
    -   [Restrict constraints to allow computable type equality](#restrict-constraints-to-allow-computable-type-equality)
    -   [Find a fully transitive approach to type equality](#find-a-fully-transitive-approach-to-type-equality)
    -   [Different syntax for rewrite constraint](#different-syntax-for-rewrite-constraint)
    -   [Different syntax for same-type constraint](#different-syntax-for-same-type-constraint)
    -   [Required ordering for rewrites](#required-ordering-for-rewrites)
    -   [Multi-constraint `where` clauses](#multi-constraint-where-clauses)
    -   [Rewrite constraints in `impl as` constraints](#rewrite-constraints-in-impl-as-constraints)

<!-- tocstop -->

## Abstract

Split the `where A == B` constraint in two: `where .A = B` produces a new
constraint from an old one, where the value of `.A` in the new constraint is
known and eagerly rewritten to `B`, and `where A == B`, which does not cause `A`
and `B` to be considered as identical by language rules but does permit implicit
(no-op) conversion between them.

This aims to provide an efficiently-computable and human-understandable type
equality rule, with type canonicalization and therefore transitive type
equality, without sacrificing too much in the way of ergonomics and without
sacrificing determinism, while still providing the full power of a general type
constraint system in a less ergonomic form.

## Problem

### Equal types with different interfaces

When an associated type is constrained to be a concrete type, it is desirable
for the associated type to behave like that concrete type:

```
interface Hashable {
  fn Hash[me: Self]() -> u128;
}
interface X {
  let R:! Hashable;
  fn Make() -> R;
}
fn F[T:! X where .R == i32](x: T) -> i32 {
  return T.Make() + 1;
}
```

Here, we want to be able to use the result of `F.Make()` in all regards like an
`i32`. Assuming an `i32.Abs` function exists, and `i32` implements `Hashable`
externally, it is more desirable for `F.Make().Abs()` to work than it is for
`F.Make().Hash()` to work.

We are
[currently aiming to address this](https://github.com/carbon-language/carbon-lang/pull/2070)
by saying that when two type expressions are constrained to be equal, a value
whose type is either of those type expressions provides the (disjoint) union of
their interfaces. This leads to a surprise:

```
fn G[T:! X where .R == i32](x: T) -> u128 {
  let n: i32 = 1;
  let m: i64 = 2;
  return n.Hash() ^ m.Hash();
}
```

Here, the call to `n.Hash()` is valid but the call to `m.Hash()` is invalid,
because the type `i32` of `n` is constrained to be equal to `T.R` which is of
type `Hashable`, but the type `i64` is not constrained in that way and does not
implement `Hashable` internally.

This suggests that there might be two different behaviors that we want when
adding a constraint: either we are changing the interface, or not. This is
analogous to internal versus external implementation of an interface.

### Type canonicalization

There are a variety of contexts in which types are compared for equality. In
some of those contexts, it might be acceptable to perform a search and a
computation, and it might be acceptable to have false negatives. For example,
when analyzing an argument being passed to a function in a generic, it might be
OK to say "we can't prove that the argument has a type that is equal to (or
convertible to) the type of the parameter", so long as the developer has some
way to demonstrate that the types are the same if that is indeed the case.

However, not all comparisons of generic types have that property. As an extreme
and hopefully avoidable example, suppose a C++-like linkage model is used, with
name mangling. We may need to determine whether two type expressions are equal
at link time, by reducing them both to strings that are guaranteed to be
identical if the types are equal and non-identical otherwise. This requires some
form of type canonicalization: reducing all equal type expressions to some
common representation where we can faithfully perform equality comparisons.

Even if the semantics of Carbon don't require canonicalization, it is still a
very useful property for implementation purposes. For example, if type
canonicalization is possible to perform efficiently, building a data structure
mapping from a type to some value becomes much simpler, and if the
representation of a type expression carries its canonical form then type
equality comparisons can be done in constant time.

### Transitivity of equality

For ergonomic purposes, it is valuable for the notion of type expression
equality to be transitive: if type A is known to be the same as type B, and type
B is known to be the same as type C, then shouldn't we be able to use an A where
a C is required? See
[#1369](https://github.com/carbon-language/carbon-lang/issues/1369) for an
explanation of why this is important.

However, if we permit arbitrary constraints and have a transitive equality rule,
then type equality is isomorphic to the
[word problem for finitely-presented monoids](https://en.wikipedia.org/wiki/Word_problem_for_groups),
which is undecidable, and certainly not computable, in general.

Therefore we must impose a restriction somewhere: either not all constraints are
permissible, or we do not have transitivity, or we impose some other constraint
on the language to avoid the hard cases. Some languages merely impose some kind
of depth limit on their search for a proof of equality.

Note that if we can perform type canonicalization, then type equality is
necessarily transitive: if all equal _pairs_ of types canonicalize to the same
representation, then _all_ equal types canonicalize to the same representation
transitively.

### Coherence

In order to avoid surprises in the language behavior, we want Carbon to have the
property that learning more about the type of a value should not cause the
behavior of an expression to change from one valid behavior to another valid
behavior.

It's important to distinguish here between learning more about a type, such as
learning that it implements a particular interface – for example, from an added
import – and changing the type, such as by writing a different expression after
a `:` or `:!`. Changing the type of a value is expected to be able to change the
behavior of an expression using that value.

## Background

There has been a lot of work in this space. Some previous relevant proposals:

-   [#731: generics details 2](https://github.com/carbon-language/carbon-lang/pull/731)
    introduced associated types, with the intent that a mechanism to constrain
    their value would be provided in a later proposal.
-   [#818: generics details 3](https://github.com/carbon-language/carbon-lang/pull/818)
    introduced `where` constraints for generics, with an open question for
    whether and how we might restrict constraints in order to give a decidable
    type equality rule.
    -   #818 represents the status quo of approved proposals. It has both `=`
        and `==` where constraints, which are similar to, but somewhat different
        from, those in this proposal.
    -   `=` constraints require a concrete type on their right-hand side. The
        left-hand side is not restricted. The facet type of the left-hand side
        type is changed to match the right-hand side.
    -   `==` constraints do not affect the facet type of either operand.
    -   As an answer to the question of how to produce a decidable type equality
        rule, both kinds of constraints are applied automatically, but only at a
        depth of one constraint. Neither form is transitive but both can be
        transitively extended using `observe` declarations.
-   [#2070: always `==` not `=` in `where` clauses](https://github.com/carbon-language/carbon-lang/pull/2070)
    describes an attempt to unify the syntax and semantics of `=` and `==`
    constraints, under which we would always merge the facet types of the
    operands. That proposal has not yet been accepted, and this proposal intends
    to supersede it.

## Proposal

Replace the semantics of the existing `where A == B` and `where A = B`
constraints and restrict the syntax of `where A = B` as follows:

-   `where .A = T` specifies a _rewrite_ constraint. The left-hand side is
    required to name an associated constant. If that associated constant `.A` is
    named as a member of a type declared with this constraint, it is rewritten
    to `T`. This means that the interface of the type changes, and the behavior
    is in all respects as if `T` had been specified directly.
-   `where X == Y` specifies a _same-type_ constraint. This is treated much like
    `where X is SameAs(Y)`. Here, `SameAs` is a hypothetical constraint that is
    reflexive (`T is SameAs(T)` for all `T`), commutative (`T is SameAs(U)` if
    and only if `U is SameAs(T)`), and not implementable by the developer.
    Moreover, if `F` is any pure type function, `T is SameAs(U)` implies
    `F(T) is SameAs(F(U)`). `observe` statements can be used to form transitive
    `SameAs` relations. Same-type constraints are not used automatically by the
    language rules for any purpose, but a blanket `ImplicitAs` impl permits
    conversions between types that are known to be the same:
    ```
    impl forall [T:! type, U:! type where .Self == T] T as ImplicitAs(U);
    ```

A type implements `C where .A = T` if and only if it implements
`C where .A == T`, assuming both constraints are valid – the inhabitants of
these two facet types are the same, but they are different facet types and
provide different interfaces for corresponding type values.

## Details

### Rewrite constraints

In a rewrite constraint, the left-hand operand of `=` must be a `.` followed by
the name of an associated constant. `.Self` is not permitted.

```
interface RewriteSelf {
  // ❌ Error: `.Self` is not the name of an associated constant.
  let Me:! type where .Self = Self;
}
interface HasAssoc {
  let Assoc:! type;
}
interface RewriteSingleLevel {
  // ✅ Uses of `A.Assoc` will be rewritten to `i32`.
  let A:! HasAssoc where .Assoc = i32;
}
interface RewriteMultiLevel {
  // ❌ Error: Only one level of associated constant is permitted.
  let B:! RewriteSingleLevel where .A.Assoc = i32;
}
```

This notation is permitted anywhere a constraint can be written, and results in
a new constraint with a different interface: the named member effectively no
longer names an associated constant of the constrained type, and is instead
treated as a rewrite rule that expands to the right-hand side of the constraint,
with any mentioned parameters substituted into that type.

```
interface Container {
  let Element:! type;
  let Slice:! Container where .Element = Element;
  fn Add[addr me: Self*](x: Element);
}
// `T.Slice.Element` rewritten to `T.Element`
//     because type of `T.Slice` says `.Element = Element`.
// `T.Element` rewritten to `i32`
//     because type of `T` says `.Element = i32`.
fn Add[T:! Container where .Element = i32](p: T*, y: T.Slice.Element) {
  // ✅ Argument `y` has the same type `i32` as parameter `x` of
  // `T.(Container.Add)`, which is also rewritten to `i32`.
  p->Add(y);
}
```

Rewrites aren't performed on the left-hand side of such an `=`, so
`where .A = .B and .A = C` is not rewritten to `where .A = .B and .B = C`.
Instead, such a `where` clause is invalid when the constraint is
[resolved](#constraint-resolution) unless each rule for `.A` specifies the same
rewrite.

Note that `T:! C where .R = i32` can result in a type `T.R` whose behavior is
different from the behavior of `T.R` given `T:! C`. For example, member lookup
into `T.R` can find different results and operations can therefore have
different behavior. However, this does not violate coherence because the facet
types `C` and `C where .R = i32` don't differ by merely having more type
information; rather, they are different facet types that have an isomorphic set
of values, somewhat like `i32` and `u32`. An `=` constraint is not merely
learning a new fact about a type, it is requesting different behavior.

### Combining constraints with `&`

Suppose we have `X = C where .R = A` and `Y = C where .R = B`. What should
`C & X` produce? What should `X & Y` produce?

We could perhaps say that `X & Y` results in a facet type where the type of `R`
has the union of the interface of `A` and the interface of `B`, and that `C & X`
similarly results in a facet type where the type of `R` has the union of the
interface of `A` and the interface originally specified by `C`. However, this
proposal suggests a simpler rule:

-   Combining two rewrite rules with different rewrite targets results in a
    facet type where the associated constant is ambiguous. Given `T:! X & Y`,
    the type expression `T.R` is ambiguous between a rewrite to `A` and a
    rewrite to `B`. But given `T:! X & X`, `T.R` is unambiguously rewritten to
    `A`.
-   Combining a constraint with a rewrite rule with a constraint with no rewrite
    rule preserves the rewrite rule. For example, supposing that
    `interface Container` extends `interface Iterable`, and `Iterable` has an
    associated constant `Element`, the constraint
    `Container & (Iterable where .Element = i32)` is the same as the constraint
    `(Container & Iterable) where .Element = i32` which is the same as the
    constraint `Container where .Element = i32`.

If the rewrite for an associated constant is ambiguous, the facet type is
rejected during [constraint resolution](#constraint-resolution).

### Combining constraints with `and`

It's possible for one `=` constraint in a `where` to refer to another. When this
happens, the facet type `C where A and B` is interpreted as
`(C where A) where B`, so rewrites in `A` are applied immediately to names in
`B`, but rewrites in `B` are not applied to names in `A` until the facet type is
[resolved](#constraint-resolution):

```
interface C {
  let T:! type;
  let U:! type;
  let V:! type;
}
class M {
  alias Me = Self;
}
// ✅ Same as `C where .T = M and .U = M.Me`, which is
// the same as `C where .T = M and .U = M`.
fn F[A:! C where .T = M and .U = .T.Me]() {}
// ❌ No member `Me` in `A.T:! type`.
fn F[A:! C where .U = .T.Me and .T = M]() {}
```

### Combining constraints with `extends`

Within an interface or named constraint, `extends` can be used to extend a
constraint that has rewrites.

```
interface A {
  let T:! type;
  let U:! type;
}
interface B {
  extends A where .T = .U and .U = i32;
}

var n: i32;

// ✅ Resolved constraint on `T` is
// `B where .(A.T) = i32 and .(A.U) = i32`.
// `T.(A.T)` is rewritten to `i32`.
fn F(T:! B) -> T.(A.T) { return n; }
```

### Combining constraints with `impl as` and `is`

Within an interface or named constraint, the `impl T as C` syntax does not
permit `=` constraints to be specified directly. However, such constraints can
be specified indirectly, for example if `C` is a named constraint that contains
rewrites. Because these constraints don't change the type of `T`, rewrite
constraints in this context will never result in a rewrite being performed, and
instead are equivalent to `==` constraints.

```
interface A {
  let T:! type;
  let U:! type;
}
constraint C {
  extends A where .T = .U and .U = i32;
}
constraint D {
  extends A where .T == .U and .U == i32;
}
interface B {
  // OK, equivalent to `impl as D;` or
  // `impl as A where .T == .U and .U == i32;`.
  impl as C;
}

var n: i32;

// ❌ No implicit conversion from `i32` to `T.(A.T)`.
// Resolved constraint on `T` is
// `B where T.(A.T) == T.(A.U) and T.(A.U) = i32`.
// `T.(A.T)` is single-step equal to `T.(A.U)`, and
// `T.(A.U)` is single-step equal to `i32`, but
// `T.(A.T)` is not single-step equal to `i32`.
fn F(T:! B) -> T.(A.T) { return n; }
```

A purely syntactic check is used to determine if an `=` is specified directly in
an expression:

-   An `=` constraint is specified directly in its enclosing `where` expression.
-   If an `=` constraint is specified directly in an operand of an `&` or
    `(`...`)`, then it is specified directly in that enclosing expression.

In an `impl as C` or `impl T as C` declaration in an interface or named
constraint, `C` is not allowed to directly specify any `=` constraints:

```
// Compile-time identity function.
fn Identity[T:! type](x:! T) -> T { return x; }

interface E {
  // ❌ Rewrite constraint specified directly.
  impl as A where .T = .U and .U = i32;
  // ❌ Rewrite constraint specified directly.
  impl as type & (A where .T = .U and .U = i32);
  // ✅ Not specified directly, but does not result
  // in any rewrites being performed.
  impl as Identity(A where .T = .U and .U = i32);
}
```

The same rules apply to `is` constraints. Note that `.T == U` constraints are
also not allowed in this context, because the reference to `.T` is rewritten to
`.Self.T`, and `.Self` is ambiguous.

```
// ❌ Rewrite constraint specified directly in `is`.
fn F[T:! A where .U is (A where .T = i32)]();

// ❌ Reference to `.T` in same-type constraint is ambiguous:
// does this mean the outer or inner `.Self.T`?
fn G[T:! A where .U is (A where .T == i32)]();

// ✅ Not specified directly, but does not result
// in any rewrites being performed. Return type
// is not rewritten to `i32`.
fn H[T:! type where .Self is C]() -> T.(A.U);

// ✅ Return type is rewritten to `i32`.
fn I[T:! C]() -> T.(A.U);
```

### Constraint resolution

When a facet type is used as the declared type of a type `T`, the constraints
that were specified within that facet type are _resolved_ to determine the
constraints that apply to `T`. This happens:

-   When the constraint is used explicitly, when declaring a generic parameter
    or associated constant of the form `T:! Constraint`.
-   When declaring that a type implements a constraint with an `impl`
    declaration, such as `impl T as Constraint`. Note that this does not include
    `impl ... as` constraints appearing in `interface` or `constraint`
    declarations.

In each case, the following steps are performed to resolve the facet type's
abstract constraints into a set of constraints on `T`:

-   If multiple rewrites are specified for the same associated constant, they
    are required to be identical, and duplicates are discarded.
-   Rewrites are performed on other rewrites in order to find a fixed point,
    where no rewrite applies within any other rewrite. If no fixed point exists,
    the generic parameter declaration or `impl` declaration is invalid.
-   Rewrites are performed throughout the other constraints in the facet type --
    that is, in any `==` constraints and `is` constraints -- and the type
    `.Self` is replaced by `T` throughout the constraint.

```
// ✅ `.T` in `.U = .T` is rewritten to `i32` when initially
// forming the facet type.
// Nothing to do during constraint resolution.
fn InOrder[A:! C where .T = i32 and .U = .T]() {}
// ✅ Facet type has `.T = .U` before constraint resolution.
// That rewrite is resolved to `.T = i32`.
fn Reordered[A:! C where .T = .U and .U = i32]() {}
// ✅ Facet type has `.U = .T` before constraint resolution.
// That rewrite is resolved to `.U = i32`.
fn ReorderedIndirect[A:! (C where .T = i32) & (C where .U = .T)]() {}
// ❌ Constraint resolution fails because
// no fixed point of rewrites exists.
fn Cycle[A:! C where .T = .U and .U = .T]() {}
```

To find a fixed point, we can perform rewrites on other rewrites, cycling
between them until they don't change or until a rewrite would apply to itself.
In the latter case, we have found a cycle and can reject the constraint. Note
that it's not sufficient to expand only a single rewrite until we hit this
condition:

```
// ❌ Constraint resolution fails because
// no fixed point of rewrites exists.
// If we only expand the right-hand side of `.T`,
// we find `.U`, then `.U*`, then `.U**`, and so on,
// and never detect a cycle.
// If we alternate between them, we find
// `.T = .U*`, then `.U = .U**`, then `.V = .U***`,
// then `.T = .U**`, then detect that the `.U` rewrite
// would apply to itself.
fn IndirectCycle[A:! C where .T = .U and .U = .V* and .V = .U*]();
```

After constraint resolution, no references to rewritten associated constants
remain in the constraints on `T`.

If a facet type is never used to constrain a type, it is never subject to
constraint resolution, and it is possible for a facet type to be formed for
which constraint resolution would always fail. For example:

```
package Broken api;

interface X {
  let T:! type;
  let U:! type;
}
let Bad:! auto = (X where .T = .U) & (X where .U = .T);
// Bad is not used here.
```

In such cases, the facet type `Broken.Bad` is not usable: any attempt to use
that facet type to constrain a type would perform constraint resolution, which
would always fail because it would discover a cycle between the rewrites for
`.T` and for `.U`. In order to ensure that such cases are diagnosed, a trial
constraint resolution is performed for all facet types. Note that this trial
resolution can be skipped for facet types that are actually used, which is the
common case.

### Precise rules and termination

This section explains the detailed rules used to implement rewrites. There are
two properties we aim to satisfy:

1.  After type-checking, no symbolic references to associated constants that
    have an associated rewrite rule remain.
2.  Type-checking always terminates in a reasonable amount of time, ideally
    linear in the size of the problem.

Rewrites are applied in two different phases of program analysis.

-   During qualified name lookup and type checking for qualified member access,
    if a rewritten member is looked up, the right-hand side's value and type are
    used for subsequent checks.
-   During substitution, if the symbolic name of an associated constant is
    substituted into, and substitution into the left-hand side results in a
    value with a rewrite for that constant, that rewrite is applied.

In each case, we always rewrite to a value that satisfies property 1 above, and
these two steps are the only places where we might form a symbolic reference to
an associated cosntant, so property 1 is recursively satisfied. Moreover, we
apply only one rewrite in each of the above cases, satisfying property 2.

#### Qualified name lookup

Qualified name lookup into either a type parameter or into an expression whose
type is a symbolic type `T` -- either a type parameter or an associated type --
considers names from the facet type `C` of `T`, that is, from `T`’s declared
type.

```
interface C {
  let M:! i32;
  let U:! C;
}
fn F[T:! C](x: T) {
  // Value is C.M in all four of these
  let a: i32 = x.M;
  let b: i32 = T.M;
  let c: i32 = x.U.M;
  let d: i32 = T.U.M;
}
```

When looking up the name `N`, if `C` is an interface `I` and `N` is the name of
an associated constant in that interface, the result is a symbolic value
representing "the member `N` of `I`". If `C` is formed by combining interfaces
with `&`, all such results are required to find the same associated constant,
otherwise we reject for ambiguity.

If a member of a class or interface is named in a qualified name lookup, the
type of the result is determined by performing a substitution. For an interface,
`Self` is substituted for the self type, and any parameters for that class or
interface (and enclosing classes or interfaces, if any) are substituted into the
declared type.

```
interface SelfIface {
  fn Get[me: Self]() -> Self;
}
class UsesSelf(T:! type) {
  // Equivalent to `fn Make() -> UsesSelf(T)*;`
  fn Make() -> Self*;
  impl as SelfIface;
}

// ✅ `T = i32` is substituted into the type of `UsesSelf(T).Make`,
// so the type of `UsesSelf(i32).Make` is `fn () -> UsesSelf(i32)*`.
let x: UsesSelf(i32)* = UsesSelf(i32).Make();

// ✅ `Self = UsesSelf(i32)` is substituted into the type
// of `SelfIface.Get`, so the type of `UsesSelf(i32).(SelfIface.Get)`
// is `fn [me: UsesSelf(i32)]() -> UsesSelf(i32)`.
let y: UsesSelf(i32) = x->Get();
```

None of this is new in this proposal. This proposal adds the rule:

If a facet type `C` into which lookup is performed includes a `where` clause
saying `.N = U`, and the result of qualified name lookup is the associated
constant `N`, that result is replaced by `U`, and the type of the result is the
type of `U`. No substitution is performed in this step, not even a `Self`
substitution -- any necessary substitutions were already performed when forming
the facet type `C`, and we don’t consider either the declared type or value of
the associated constant at all for this kind of constraint. Going through an
example in detail:

```
interface A {
  let T:! type;
}
interface B {
  let U:! type;
  // More explicitly, this is of type `A where .(A.T) = Self.(B.U)`
  let V:! A where .T = U;
}
// Type of T is B.
fn F[T:! B](x: T) {
  // The type of the expression `T` is `B`.
  // `T.V` finds `B.V` with type `A where .(A.T) = Self.(B.U)`.
  // We substitute `Self` = `T` giving the type of `u` as
  // `A where .(A.T) = T.(B.U)`.
  let u:! auto = T.V;
  // The type of `u` is `A where .(A.T) = T.(B.U)`.
  // Lookup for `u.T` resolves it to `u.(A.T)`.
  // So the result of the qualified member access is `T.(B.U)`,
  // and the type of `v` is the type of `T.(B.U)`, namely `type`.
  // No substitution is performed in this step.
  let v:! auto = u.T;
}
```

The more complex case of

```
fn F2[T:! B where .U = i32](x: T);
```

is discussed later.

#### Type substitution

At various points during the type-checking of a Carbon program, we need to
substitute a set of (binding, value) pairs into a symbolic value. We saw an
example above: substituting `Self = T` into the type `A where .(A.T) = Self.U`
to produce the value `A where .(A.T) = T.U`. Another important case is the
substitution of inferred parameter values into the type of a function when
type-checking a function call:

```
fn F[T:! C](x: T) -> T;
fn G(n: i32) -> i32 {
  // Deduces T = i32, which is substituted
  // into the type `fn (x: T) -> T` to produce
  // `fn (x: i32) -> i32`, giving `i32` as the type
  // of the call expression.
  return F(n);
}
```

Qualified name lookup is not re-done as a result of type substitution. For a
template, we imagine there’s a completely separate step that happens before type
substitution, where qualified name lookup is redone based on the actual value of
template arguments; this proceeds as described in the previous section.
Otherwise, we performed the qualified name lookup when type-checking the
generic, and do not do it again:

```
interface IfaceHasX {
  let X:! type;
}
class ClassHasX {
  class X {}
}
interface HasAssoc {
  let Assoc:! IfaceHasX;
}

// Qualified name lookup finds `T.(HasAssoc.Assoc).(IfaceHasX.X)`.
fn F(T:! HasAssoc) -> T.Assoc.X;

fn G(T:! HasAssoc where .Assoc = ClassHasX) {
  // `T.Assoc` rewritten to `ClassHasX` by qualified name lookup.
  // Names `ClassHasX.X`.
  var a: T.Assoc.X = {};
  // Substitution produces `ClassHasX.(IfaceHasX.X)`,
  // not `ClassHasX.X`.
  var b: auto = F(T);
}
```

During substitution, we might find a member access that named an opaque symbolic
associated constant in the original value can now be resolved to some specific
value. It’s important that we perform this resolution:

```
interface A {
  let T:! type;
}
class K { fn Member(); }
fn H[U:! A](x: U) -> U.T;
fn J[V:! A where .T = K](y: V) {
  // We need the interface of `H(y)` to include
  // `K.Member` in order for this lookup to succeed.
  H(y).Member();
}
```

The values being substituted into the symbolic value are themselves already
fully substituted and resolved, and in particular, satisfy property 1 given
above.

Substitution proceeds by recursively rebuilding each symbolic value, bottom-up,
replacing each substituted binding with its value. Doing this naively will
propagate values like `i32` in the `F`/`G` case earlier in this section, but
will not propagate rewrite constants like in the `H`/`J` case. The reason is
that the `.T = K` constraint is in the _type_ of the substituted value, rather
than in the substituted value itself: deducing `T = i32` and converting `i32` to
the type `C` of `T` preserves the value `i32`, but deducing `U = V` and
converting `V` to the type `A` of `U` discards the rewrite constraint.

In order to apply rewrites during substitution, we associate a set of rewrites
with each value produced by the recursive rebuilding procedure. This is somewhat
like having substitution track a refined facet type for the type of each value,
but we don’t need -- or want -- for the type to change during this process, only
for the rewrites to be properly applied. For a substituted binding, this set of
rewrites is the rewrites found on the type of the corresponding value prior to
conversion to the type of the binding. When rebuilding a member access
expression, if we have a rewrite corresponding to the accessed member, then the
resulting value is the target of the rewrite, and its set of rewrites is that
found in the type of the target of the rewrite, if any. Because the target of
the rewrite is fully resolved already, we can ask for its type without
triggering additional work. In other cases, the rewrite set is empty; all
necessary rewrites were performed when type-checking the value we're
substituting into.

Continuing an example from [qualified name lookup](#qualified-name-lookup):

```
interface A {
  let T:! type;
}
interface B {
  let U:! type;
  let V:! A where .T = U;
}

// Type of the expression `T` is `B where .(B.U) = i32`
fn F2[T:! B where .U = i32](x: T) {
  // The type of the expression `T` is `B where .U = i32`.
  // `T.V` is looked up and finds the associated type `(B.V)`.
  // The declared type is `A where .(A.T) = Self.U`.
  // We substitute `Self = T` with rewrite `.U = i32`.
  // The resulting type is `A where .(A.T) = i32`.
  // So `u` is `T.V` with type `A where .(A.T) = i32`.
  let u:! auto = T.V;
  // The type of `u` is `A where .(A.T) = i32`.
  // Lookup for `u.T` resolves it to `u.(A.T)`.
  // So the result of the qualified member access is `i32`,
  // and the type of `v` is the type of `i32`, namely `type`.
  // No substitution is performed in this step.
  let v:! auto = u.T;
}
```

#### Examples

```
interface Container {
  let Element:! type;
}
interface SliceableContainer {
  extends Container;
  let Slice:! Container where .Element = Self.(Container.Element);
}
// ❌ Qualified name lookup rewrites this facet type to
// `SliceableContainer where .(Container.Element) = .Self.(Container.Element)`.
// Constraint resolution rejects this because this rewrite forms a cycle.
fn Bad[T:! SliceableContainer where .Element = .Slice.Element](x: T.Element) {}
```

```
interface Helper {
  let D:! type;
}
interface Example {
  let B:! type;
  let C:! Helper where .D = B;
}
// ✅ `where .D = ...` by itself is fine.
// `T.C.D` is rewritten to `T.B`.
fn Allowed(T:! Example, x: T.C.D);
// ❌ But combined with another rewrite, creates an infinite loop.
// `.C.D` is rewritten to `.B`, resulting in `where .B = .B`,
// which causes an error during constraint resolution.
// Using `==` instead of `=` would make this constraint redundant,
// rather than it being an error.
fn Error(T:! Example where .B = .C.D, x: T.C.D);
```

```
interface Allowed;
interface AllowedBase {
  let A:! Allowed;
}
interface Allowed {
  extends AllowedBase where .A = .Self;
}
// ✅ The final type of `x` is `T`. It is computed as follows:
// In `((T.A).A).A`, the inner `T.A` is rewritten to `T`,
// resulting in `((T).A).A`, which is then rewritten to
// `(T).A`, which is then rewritten to `T`.
fn F(T:! Allowed, x: ((T.A).A).A);
```

```
interface MoveYsRight;
constraint ForwardDeclaredConstraint(X:! MoveYsRight);
interface MoveYsRight {
  let X:! MoveYsRight;
  // Means `Y:! MoveYsRight where .X = X.Y`
  let Y:! ForwardDeclaredConstraint(X);
}
constraint ForwardDeclaredConstraint(X:! MoveYsRight) {
  extends MoveYsRight where .X = X.Y;
}
// ✅ The final type of `x` is `T.X.Y.Y`. It is computed as follows:
// The type of `T` is `MoveYsRight`.
// The type of `T.Y` is determined as follows:
// -   Qualified name lookup finds `MoveYsRight.Y`.
// -   The declared type is `ForwardDeclaredConstraint(Self.X)`.
// -   That is a named constraint, for which we perform substitution.
//     Substituting `X = Self.X` gives the type
//     `MoveYsRight where .X = Self.X.Y`.
// -   Substituting `Self = T` gives the type
//     `MoveYsRight where .X = T.X.Y`.
// The type of `T.Y.Y` is determined as follows:
// -   Qualified name lookup finds `MoveYsRight.Y`.
// -   The declared type is `ForwardDeclaredConstraint(Self.X)`.
// -   That is a named constraint, for which we perform substitution.
//     Substituting `X = Self.X` gives the type
//     `MoveYsRight where .X = Self.X.Y`.
// -   Substituting `Self = T.Y` with
//     rewrite `.X = T.X.Y` gives the type
//     `MoveYsRight where .X = T.Y.X.Y`, but
//     `T.Y.X` is replaced by `T.X.Y`, giving
//     `MoveYsRight where .X = T.X.Y.Y`.
// The type of `T.Y.Y.X` is determined as follows:
// -   Qualified name lookup finds `MoveYsRight.X`.
// -   The type of `T.Y.Y` says to rewrite that to `T.X.Y.Y`.
// -   The result is `T.X.Y.Y`, of type `MoveYsRight`.
fn F4(T:! MoveYsRight, x: T.Y.Y.X);
```

#### Termination

Each of the above steps performs at most one rewrite, and doesn't introduce any
new recursive type-checking steps, so should not introduce any new forms of
non-termination. Rewrite constraints thereby give us a deterministic,
terminating type canonicalization mechanism for associated constants: in `A.B`,
if the type of `A` specifies that `.B = C`, then `A.B` is replaced by `C`.
Equality of types constrained in this way is transitive.

However, some existing forms of non-termination may remain, such as template
instantiation triggering another template instantiation. Such cases will need to
be detected and handled in some way, such as by a depth limit, but doing so
doesn't compromise the soundness of the type system.

### Same type constraints

A same-type constraint describes that two type expressions are known to evaluate
to the same value. Unlike a rewrite constraint, however, the two type
expressions are treated as distinct types when type-checking a generic that
refers to them.

Same-type constraints are brought into scope, looked up, and resolved exactly as
if there were a `SameAs(U:! type)` interface and a `T == U` impl corresponded to
`T is SameAs(U)`, except that `==` is commutative. As such, it's not possible to
ask for a list of types that are the same as a given type, nor to ask whether
there exists a type that is the same as a given type and has some property. But
it is possible to ask whether two types are (non-transitively) the same.

In order for same-type constraints to be useful, they must allow the two types
to be treated as actually being the same in some context. This can be
accomplished by the use of `==` constraints in an `impl`, such as in the
built-in implementation of `ImplicitAs`:

```
final impl forall [T:! type, U:! type where .Self == T] T as ImplicitAs(U) {
  fn Convert[me: Self](other: U) -> U { ... }
}
```

It superficially seems like it would be convenient if such implementations were
made available implicitly – for example, by writing
`impl forall [T:! type] T as ImplicitAs(T)` – but in more complex examples that
turns out to be problematic. Consider:

```
interface CommonTypeWith(U:! type) {
  let Result:! type;
}
final impl forall [T:! type] T as CommonTypeWith(T) where .Result = T {}

fn F[T:! Potato, U:! Hashable where .Self == T](x: T, y: U) -> auto {
  // What is T.CommonTypeWith(U).Result? Is it T or U?
  return (if cond then x else y).Hash();
}
```

With this proposal, `impl` validation for `T as CommonTypeWith(U)` fails: we
cannot pick a common type when given two distinct type expressions, even if we
know they evaluate to the same type, because we would not know which API the
result should have.

#### Implementation of same-type `ImplicitAs`

It is possible to implement the above `impl` of `ImplicitAs` directly in Carbon,
without a compiler builtin, by taking advantage of the built-in conversion
between `C where .A = X` and `C where .A == X`:

```
interface EqualConverter {
  let T:! type;
  fn Convert(t: T) -> Self;
}
fn EqualConvert[T:! type](t: T, U:! EqualConverter where .T = T) -> U {
  return U.Convert(t);
}
impl forall [U:! type] U as EqualConverter where .T = U {
  fn Convert(u: U) -> U { return u; }
}

impl forall [T:! type, U:! type where .Self == T] T as ImplicitAs(U) {
  fn Convert[self: Self]() -> U { return EqualConvert(self, U); }
}
```

The transition from `(T as ImplicitAs(U)).Convert`, where we know that `U == T`,
to `EqualConverter.Convert`, where we know that `.T = U`, allows a same-type
constraint to be used to perform a rewrite.

This implementation is in use in Carbon Explorer.

### Observe declarations

Same-type constraints are non-transitive, just like other constraints such as
`ImplicitAs`. The developer can use an `observe` declaration to bring a new
same-type constraint into scope:

```
observe A == B == C;
```

notionally does much the same thing as

```
impl A as SameAs(C) { ... }
```

where the `impl` makes use of `A is SameAs(B)` and `B is SameAs(C)`.

### Implementing an interface

When implementing an interface, the `=` syntax must be used, and each associated
constant without a default must be explicitly assigned-to:

```
impl IntVec as Container where .Element = i32 { ... }
```

not

```
impl IntVec as Container where .Element == i32 { ... }
```

The latter would be treated as

```
impl IntVec as Container where IntVec.Element is SameAs(i32) { ... }
```

... which only checks the value of `Element` rather than specifying it.

As in other contexts, `Self.Element` is rewritten to `i32` within the context of
the `impl`.

### Ergonomics

This proposal can be viewed as dividing type constraints into two categories:

-   Ergonomic, but quite restricted, constraints using `=`.
-   Non-ergonomic, but fully general, constraints using `==`.

In order for this to be an effective and ergonomic strategy, we require both
that the difference between these two kinds of constraints are readily
understood by developers, and that the more-ergonomic `=` constraints cover
sufficiently many scenarios that the developer seldom needs to write code to
request a conversion between types that are known to be the same.

Ideally, we hope that `=` constraints will cover all real situations, and `==`
constraints will never need to be written, outside of the one `ImplicitAs`
implementation described above. If this turns out to be true in practice, we
should consider removing `==` syntax from the language. However, this will not
remove `==` semantics, both because of the behavior of `ImplicitAs` and because
`impl T as C where .A = B` constraints in an interface or named constraint give
rise to `==` semantics.

### Implementation experience

This proposal has been mostly implemented in Carbon Explorer, and appears to
behave as expected. However, Explorer does not yet support forward declarations
of interfaces and constraints, which means that some of the more interesting
cases can't be tested.

## Rationale

-   [Language tools and ecosystem](/docs/project/goals.md#language-tools-and-ecosystem)
    -   This rule is easy to implement, and even a naive implementation should
        be efficient.
-   [Software and language evolution](/docs/project/goals.md#software-and-language-evolution)
    -   The status quo causes coincidentally equal types to have the same
        interface. Under this proposal, the interface of a type is not affected
        by coincidental equality, only by intentional assignment to an
        associated type.
-   [Code that is easy to read, understand, and write](/docs/project/goals.md#code-that-is-easy-to-read-understand-and-write)
    -   Using `=` rather than `==` in `impl`s is easier to read and write.
    -   The interface available on a type is more predictable in this proposal
        than in the status quo ante, making code easier to understand.

## Alternatives considered

### Status quo

The [Problem](#problem) section describes some concerns with the status quo
approach. This proposal aims to address those concerns.

### Restrict constraints to allow computable type equality

We could somehow restrict which constraints can be specified, in order to ensure
that our type equality rule is efficiently computable, perhaps even in a way
that permits a deterministic computation of a canonical type. The exact details
of how we would do this have not been worked out, but this might lead to a
coherent rule that has transitive type equality. However, this would not solve
the "equal types with different interfaces" problem.

### Find a fully transitive approach to type equality

This proposal makes type equality transitive, but still has non-transitive
"same-type" constraints describing types that are known to always eventual be
the same after substitution, but which are not treated as the same type value
while type-checking a generic. This proposal also imposes a directionality on
rewrites, a restriction to only rewrite at a depth of exactly one associated
constant, and a restriction that only one value can be specified as equal to a
given associated constant. We could seek a type equality rule that would avoid
having two different kinds of equality and would avoid some or all of the
restrictions placed on rewrite constraints.

One candidate approach is to accept that the full generality of the equality
problem is
[hard](https://link.springer.com/content/pdf/10.1007/3-540-17220-3_7.pdf), but
attempt to solve it anyway. Because of the close correspondence between Turing
machines and string rewriting systems, this results in a type system with no
upper bound on its runtime. We consider this unacceptable for Carbon, but it is
the approach taken by some other modern languages:

-   Swift has an
    [undecidable type system](https://forums.swift.org/t/swift-type-checking-is-undecidable/39024)
    due to this, and handles the problem by placing a limit on the complexity of
    cases they will accept, but that seems unsuited to Carbon's goals, as the
    rule cannot be readily understood by a developer nor effectively worked
    around.
-   Rust also has an
    [undecidable type system](https://sdleffler.github.io/RustTypeSystemTuringComplete/)
    (content warning: contains many instances of an obscene word as part of a
    programming language name) for the same reason, and similarly has a
    recursion limit.

See also
[Typing is Hard](https://web.archive.org/web/20231223005655/https://3fx.ch/typing-is-hard.html),
which lists similar information for a variety of other languages. Note that most
languages listed have an undecidable type system.

Another candidate approach is to find a way to reduce the inputs to the
type-checking step as a set of non-quantified equalities. The resulting system
of equalities can then be
[solved efficiently](https://dl.acm.org/doi/pdf/10.1145/322186.322198) to
determine whether two types are known to be the same. This approach appears
sufficient to cope with locally declared constraints, but when constraints
appear within interfaces, they can give rise to an infinite family of
equalities, and picking any finite subset risks the result being non-transitive
in general, if a different subset of equalities might be considered in a
different type-checking context.

### Different syntax for rewrite constraint

We could use a different syntax, such as `~>`, for rewrite constraints. This
would have the advantage of not using assignment for an operation that's not
always doing something that developers will think of as assignment. It also
avoids hard-to read code in cases where a binding has an initializer:

```
// This proposal.
let T:! Add where .Result = i32 = i32;
// Alternative syntax.
let T:! Add where .Result ~> i32 = i32;
```

However, it seems valuable to use only a single syntax for specifying these
constraints, and equality is the appropriate mental model most of the time.
Moreover, in an `impl` declaration, we really are assigning to the associated
constant in the sense of setting a value, rather than merely constraining a
value.

This decision should be revisited if a superior syntax that avoids the above
visual ambiguity is suggested.

### Different syntax for same-type constraint

We considered various options for the spelling of a same-type constraint:

-   `where A == B`
-   `where A ~ B`
-   some other operator symbol
-   `where A is SameType(B)`, or some other constraint name

The advantage of `==` is that it has a lot of desirable implications: it's
familiar, symmetric, and connotes the left and right operand being the same.
However, it also might be taken as suggesting that the `==` overloaded operator
is used to determine equality. A different spelling would also indicate that
this is an unusual constraint, and would be easier to search for. Concerns were
also raised that `==` might suggest transitivity if taken to mean "same value"
rather than something like the Carbon `==` binary operator, and the transitivity
of `==` constraints is not automatic.

The `~` operator is currently not in use as a binary operator. However, that
makes it quite valuable syntactic real estate, and it may see little use in this
context in practice. A longer operator could be used, but any choice other than
`==` will present an unfamiliarity barrier, and longer operators will be harder
to remember.

A named constraint is appealing, but this operator does not behave like a named
constraint in that it is automatically symmetrized, not implementable, and
especially in its interactions with `observe` declarations. It is unclear how
`observe` declarations would be written with a named `SameType` constraint:

```
// Maybe something like this special-case and verbose syntax?
observe A is SameType(B) and B is SameType(C) => A is SameType(C);
```

The fundamental connection between same-type constraints and `observe` suggests
that dedicated syntax is justified.

For now, we use `==`, despite it having a different meaning in the context of a
constraint than in expression contexts. This is analogous to how `=` and `and`
have different meanings in this context from in expressions, so the behavior
divergence is at least consistent. It's also not clear at this stage how much
usage same-type constraints will have, compared to rewrite constraints, so it's
hard to judge the other arguments in favor of and against other operators. It
would be reasonable to revisit this decision when we have more usage
information.

### Required ordering for rewrites

We considered a rule where a rewrite would need to be specified in a constraint
before the associated constant is used. For example:

```
interface C {
  let T:! type;
  let U:! type;
}
// Could reject, `.U` referenced before rewrite is defined.
fn G[A:! C where .T = .U and .U = i32]() {}
```

This would remove the need to perform constraint resolution. Instead, we could
apply rewrites as we form the constraint, and constraints formed in this way
would always satisfy the property that they don't refer to associated constants
that have a rewrite.

It may also be less surprising to use this rule. Because Carbon uses top-down
processing for type-checking in general, it may be unexpected that a rewrite
rule would rewrite an earlier occurrence of its rewrite target, even though this
happens in practice at a later point in time, during constraint resolution.

However, such an approach would not give a satisfactory outcome for cases such
as:

```
constraint X {
  extends C where .T = .U;
}
constraint Y {
  extends C where .U = i32;
}
// Desired behavior is that `.T` and `.U` both rewrite to `i32`.
fn G[A:! X & Y]() -> A.T { return 0; }
```

Performing earlier-appearing rewrites in later constraints and additionally
performing a constraint resolution step to apply rewrites throughout the
constraint seems to give better outcomes for the examples we considered.

### Multi-constraint `where` clauses

Instead of treating `A where B and C` as `(A where B) where C`, we could model
it as `(A where B) & (A where C)`.

Specifically, given

```
interface C {
  let T:! type;
  let U:! type;
}
```

this would treat `C where .T = A and .U = B` as
`(C where .T = A) & (C where .U = B)`, where the type of `.Self` would be `C` in
both clauses, with both constraints applied "simultaneously" to `C`. This would
mean that the order of clauses doesn’t matter.

However, if we do this, then neither right-hand side is rewritten by name
lookup, and thus we would reject cases such as
`C where .T = i32 and .U = .T.(Add.Result)`. This case seems reasonable, and we
would prefer to accept it.

Therefore, the rule we select is that, as soon as a rewrite is declared, it is
in scope, and later references to that associated constant refer to the
rewritten value with its rewritten type. We still reject cases like
`C where .U = .T.(Add.Result) and .T = i32`, because we do not know that
`T is Add` from the declared type of `C.T`.

The same rule applies to `is` constraints: we accept
`C where .T is Add and .U = .T.(Add.Result)`, but reject
`C where .U = .T.(Add.Result) and .T is Add`.

### Rewrite constraints in `impl as` constraints

A rewrite constraint can appear indirectly in an `impl as` constraint in an
interface or named constraint:

```
interface A {
  let T:! type;
}
constraint AInt {
  extends A where .T = i32;
}
interface B {
  // Or, `impl as A where .T = i32;`
  impl as AInt;
}
```

When this happens, the rewrite constraint does not result in rewrites being
performed when the associated constant is mentioned in a member access into that
interface or named constraint:

```
// Return type is not rewritten to `i32`,
// but there is still a same-type constraint.
fn F(T:! B) -> T.(A.T) {
  // OK, `i32` implicitly converts to `T.(A.T)`.
  return 0 as i32;
}
```

This may be surprising: `B` says that its `.(A.T)` has a rewrite to `i32`, but
that rewrite is not performed. In contrast, rewrites in an `extends` constraint
do become part of the enclosing interface or named constraint.

```
interface C {
  extends AInt;
}
// Return type is rewritten to `i32`.
fn G(T:! C) -> T.T;
```

Something similar happens with `impl T as` constraints. The following two
interfaces `A1` and `A2` are not equivalent:

```
interface A1 {
  let X:! Add where .Result = i32;
}
constraint AddToi32 {
  extends Add where .Result = i32;
}
interface A2 {
  let X:! Add;
  impl X as AddToi32;
}
```

In the former case, references to `A.X.Result` are rewritten to `i32`, and in
the latter case, they are not, because the rewrite is not part of the type of
`X`.

The general principle here is that rewrites are part of the declared type of a
name, and can't be changed after the fact by another declaration. For the
`impl T as` case, this behavior is also a necessary part of the termination
argument. If rewrites from `impl T as` constraints were used, it would be
possible to form a rewrite cycle:

```
interface C { let X:! type; }
interface A {
  let U:! C;
  let T:! C;
}
interface B1 {
  extends A;
  impl T as C where .X = U.X;
}
interface B2 {
  extends A;
  impl U as C where .X = T.X;
}
// `V.T.X` ~> `V.U.X` ~> `V.T.X` ~> ...
fn F(V:! B1 & B2) -> V.T.X;
```

We could allow the specific case of `impl as` (not `impl T as`) to introduce
rewrites. The advantage of this change is that this behavior may be less
surprising in some cases. However, this would mean that an `impl as` sometimes
changes the interface of the enclosing constraint, and behaves inconsistently
from an `impl T as` constraint, so this proposal does not adopt that behavior.

We could allow `impl T as` to introduce rewrites for `T` in general, but we
would need to find some way to fix the resulting holes in the termination
argument.

To minimize the scope of confusion, we currently disallow rewrites from
appearing _syntactically_ within an `impl as` or `impl T as` constraint. We
could allow these constructs. However, a `.T = V` constraint would be equivalent
to a `.T == V` constraint, and the latter more clearly expresses the resulting
semantics, so disallowing the misleading form seems preferable.
