Types are values of type `type` (#2360)

Define a "type" to be a value of type `type`. Contexts expecting a type perform an implicit conversion to `type`. Values like `()` and `(i32, i32)` and `{}` are no longer types, but instead implicitly convert to `type`. Values of interface or constraint type (now called "facets") are similarly not formally types but implicitly convert to `type`.

Co-authored-by: Chandler Carruth <chandlerc@gmail.com>
Co-authored-by: josh11b <josh11b@users.noreply.github.com>
Co-authored-by: Jon Ross-Perkins <jperkins@google.com>

proposals/p2360.md

@@ -0,0 +1,650 @@
+# Types are values of type `type`
+
+<!--
+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/2360)
+
+<!-- toc -->
+
+## Table of contents
+
+-   [Abstract](#abstract)
+-   [Problem](#problem)
+    -   [Tuples behave inconsistently](#tuples-behave-inconsistently)
+    -   [Qualified access to constraint members is inconsistent](#qualified-access-to-constraint-members-is-inconsistent)
+-   [Background](#background)
+-   [Proposal](#proposal)
+-   [Details](#details)
+    -   [Terminology](#terminology)
+    -   [`type` and `Core.Type`](#type-and-coretype)
+    -   [Compound member access](#compound-member-access)
+        -   [Instance binding](#instance-binding)
+        -   [Impl lookup](#impl-lookup)
+        -   [Examples](#examples)
+    -   [Tuple and struct literals](#tuple-and-struct-literals)
+    -   [Name lookup into values with constrained types](#name-lookup-into-values-with-constrained-types)
+    -   [Types in diagnostics](#types-in-diagnostics)
+-   [Rationale](#rationale)
+    -   [Teachability](#teachability)
+-   [Alternatives considered](#alternatives-considered)
+    -   [Alternative member access rules](#alternative-member-access-rules)
+    -   [Alternative terminology](#alternative-terminology)
+    -   [`Core.Type` is an empty named constraint](#coretype-is-an-empty-named-constraint)
+    -   [Write tuple types differently than tuples](#write-tuple-types-differently-than-tuples)
+
+<!-- tocstop -->
+
+## Abstract
+
+Define a "type" to be a value of type `type`. Contexts expecting a type perform
+an implicit conversion to `type`. Values like `()`, `(i32, i32)`, and `{}` are
+no longer types, but instead implicitly convert to `type`. Values of interface
+or constraint type (now called "facets") are similarly not formally types but
+implicitly convert to `type`.
+
+The practical impact to the language semantics is relatively small. This
+proposal primarily establishes clearer, more principled terminology and design
+concepts with a few narrow improvements to the design's consistency.
+
+## Problem
+
+### Tuples behave inconsistently
+
+Currently, the type of `(i32, i32)` is `(Type, Type)`, and similarly the type of
+`(Type, Type)` is also `(Type, Type)`. This leads to an inconsistency: for most
+values, asking for the type, then the type-of-type, and so on, quickly leads to
+`Type`, whose type is `Type`. But for a few values, notably tuples and empty
+structs, we instead bottom out at a different value.
+
+This leads to implementation complexity and a lack of clarity around what is or
+is not a type. It is easy to find examples where explorer misbehaves or crashes
+due to getting tuple values and types mixed up.
+
+Moreover, this inconsistency is limited to a few built-in types. There is no way
+to design a class type so it behaves like a tuple type.
+
+### Qualified access to constraint members is inconsistent
+
+Given the expression `x.(Interface.Function)`, where the function is an instance
+method, the behavior depends on whether `x` is a type.
+
+-   If `x` is not a type, but a value of type `T`, this requires
+    `T is Interface` and looks for `Function` in the corresponding `impl`.
+    Instance binding is performed.
+-   If `x` is a type, this requires `x` to have symbolic value phase and
+    requires that `x is Interface`. The result is an unbound member name.
+
+This dual meaning has some problematic consequences:
+
+-   Even if `Interface.Function` is non-dependent, if `x` depends on a template
+    parameter then we must treat the compound member access as being dependent.
+    Qualification cannot be used to avoid dependence in templates.
+-   Worse, if `x` is a template parameter, the interpretation will differ
+    between instantiations, meaning that a template and a checked generic will
+    have a discontinuity in behavior when `x` happens to be a type.
+-   While it is possible to `impl Type as ...`, this rule means it is not
+    possible to directly invoke methods that have been implemented this way. For
+    example, given an `impl Type as DebugPrintable`,
+    `i32.(DebugPrintable.Print)()` will look for `i32 as DebugPrintable` not
+    `Type as DebugPrintable`.
+
+## Background
+
+-   [#989: Member access expressions](/proposals/p0989.md) introduced the
+    current compound member access rules.
+-   [Issue #495](https://github.com/carbon-language/carbon-lang/issues/495)
+    suggested adding an implicit conversion from tuples of types to type `Type`.
+-   [Issue #508](https://github.com/carbon-language/carbon-lang/issues/508)
+    raised the question of whether we want tuples like `((), (), ())` to be
+    self-typed.
+-   [Issue #2113](https://github.com/carbon-language/carbon-lang/issues/2113)
+    gave us spelling and behavior guidelines for predefined names like `type`.
+
+## Proposal
+
+Instead of treating type-like values as being types regardless of the type of
+those values, we define a _type_ as being a value of type `type`.
+
+This has the following consequences:
+
+-   `()` is a value of type `() as type`, not a value of type `()` (because the
+    latter is not a type).
+    -   `() as type` is a value of type `type`.
+    -   Similarly, `(i32, i32)` is of type `(type, type) as type`, which is of
+        type `type`.
+    -   Similarly, `{}` is of type `{} as type`, which is of type `type`.
+    -   More generally, _the type of any type is `type`_.
+-   Given `T:! Hashable`, `T` is formally not a type, because it is not of type
+    `type`. Indeed, member lookup into `type`, and hence into types, finds
+    nothing, but member lookup into `T` finds members of `Hashable`.
+-   Contexts in which a type is required, such as on the right hand side of a
+    `:` or `:!` binding or the return type of a function, perform an implicit
+    conversion to type `type`.
+    -   This means that a user-defined type can implement `ImplicitAs(type)`,
+        annotated in whatever way we eventually decide to annotate functions
+        that are usable at compile time, and values of that type will be usable
+        as types, in the same way that `()` and `{}` are.
+-   There are no singleton type-of-types. It's still possible to have, for
+    example, the type of `i32` be a type whose only value is `i32`. The value
+    `i32` would then not formally be a type, as its type would not be `type`,
+    but it could still implicitly convert to `type`, as `()` does, if we so
+    desire.
+    -   This extends to other cases: we could say that for integer literals,
+        which we have recently been describing as having type `IntLiteral(n)`,
+        there is an `impl IntLiteral(n) as ImplicitAs(type)` which converts a
+        value of type `IntLiteral(n)` to the `type` value `IntLiteral(n)`. This
+        would then permit `let v: 0 = 0;`.
+    -   Such changes to `i32` or integer literals are not part of this proposal.
+
+## Details
+
+### Terminology
+
+The changes to the language rules in this proposal are fairly small, but there
+is a significant change in how we describe those rules. We now use the following
+terminology:
+
+-   A _type_ is a value of type `type`.
+-   A _facet type_ is a type whose values are some subset of the values of
+    `type`, determined by a set of constraints.
+
+    -   Interface types and named constraint types are facet types whose
+        constraints are that the interface or named constraint is satisfied by
+        the type.
+    -   The values produced by `&` operations between facet types and by `where`
+        expressions are facet types, whose set of constraints are determined by
+        the `&` or `where` expression.
+    -   `type` is a facet type whose set of constraints is empty.
+
+    We previously referred to a facet type as a type-of-type, but that is no
+    longer accurate, as the type of any type is now by definition `type`.
+
+-   A _facet_ is a value of a facet type. For example, `i32 as Hashable` is a
+    facet, and `Hashable` is a facet type. Note that all types are facets.
+    -   A facet value can be thought of as a tuple of a possibly-symbolic
+        identity for a type, plus any witnesses needed to demonstrate that the
+        type satisfies the constraints of the facet type. A type is then a facet
+        value that has no witnesses.
+-   We use the term _generic type_ to refer to a type or facet introduced by a
+    `:!` binding, such as in a generic parameter or associated constant.
+    -   This gives rise to terms such as _generic type parameter_ and
+        _associated generic type_.
+    -   It is worth noting that a generic type is not necessarily a type. It may
+        be a facet, and its type may be a facet type other than `type`.
+
+### `type` and `Core.Type`
+
+This proposal introduces the name `type` as a keyword -- a type literal -- that
+names the facet type with an empty set of constraints. This keyword replaces the
+provisional name `Type` for this functionality.
+
+In [issue #2113](https://github.com/carbon-language/carbon-lang/issues/2113), it
+was decided that such functionality may be an alias for a name in the prelude,
+such as `Core.Type`. This proposal does not introduce a corresponding prelude
+name. The facet type `type` is primitive and provided by the compiler, and not
+an alias.
+
+[As noted in the generics design](/docs/design/generics/details.md#named-constraints),
+a declaration such as `constraint MyVersionOfType {}` would introduce a facet
+type that is equivalent to `type`. This proposal does not change this decision.
+Because such a named constraint `MyVersionOfType` is equivalent to `type`, that
+is, because they are the same facet type, a value `T:! MyVersionOfType` is a
+type under this proposal. There is an open
+[issue for leads](https://github.com/carbon-language/carbon-lang/issues/2409) on
+whether this is the right behavior or if we'd prefer a different rule.
+
+### Compound member access
+
+#### Instance binding
+
+For the syntax `x.y`, if `x` is an entity that has member names, such as a
+namespace or a type, then `y` is looked up within `x`, and instance binding is
+not performed. Otherwise, `y` is looked up within the type of `x` and instance
+binding is performed if an instance member is found.
+
+The syntax `x.(Y)`, where `Y` names an instance member, always performs instance
+binding. Therefore, for a suitable `DebugPrintable`:
+
+-   `1.(DebugPrintable.Print)()` still prints `1`, as before.
+-   `i32.(DebugPrintable.Print)()` now prints `i32`, rather than forming a
+    member name.
+-   `1.(i32.(DebugPrintable.Print))()` is now an error, rather than printing
+    `1`.
+
+In order to get the old effect of `x.(MyType.(MyInterface.InstanceMember))()`,
+one can now write `x.((MyType as MyInterface).InstanceMember)()`. This behaves
+the same as the member access in:
+
+```
+fn F(MyType:! MyInterface, x: MyType) -> auto {
+  return x.(MyType.InstanceMember)();
+}
+```
+
+... because it is the same thing. `MyType as InstanceMember` is a facet, which
+roughly corresponds to a fully-instanstiated `impl`, and lookup into a facet
+finds members of that corresponding `impl`. And if `MyType` is declared as
+`MyType:! MyInterface` instead of as `MyType:! type`, then `MyType` and
+`MyType as MyInterface` are equivalent.
+
+#### Impl lookup
+
+Prior to this proposal, when a member access names a member of interface `I`,
+the rules for `impl` lookup also depend on whether the left hand operand is a
+type:
+
+-   If the left hand operand is a type-of-type (now, facet type), `impl` lookup
+    is not performed.
+-   If the left hand operand evaluates to a type `T`, then `impl` lookup is
+    performed for `T as I`.
+-   Otherwise, the first operand is an expression of some type `T`, and `impl`
+    lookup is performed for `T as I`.
+
+Due to the non-uniform treatment of types and non-types, this rule is also
+changed to the following:
+
+-   For a simple member access `a.b` where `b` names a member of an interface
+    `I`:
+    -   If the interface member was found by searching a non-facet-type scope
+        `T`, for example a class or an adapter, then `impl` lookup is performed
+        for `T as I`. For example:
+        -   `MyClass.AliasForInterfaceMember` finds the member of the
+            `impl MyClass as I`, not the interface member.
+        -   `my_value.AliasForInterfaceMember`, with `my_value: MyClass`, finds
+            the member of the `impl MyClass as I`, and performs instance binding
+            if the member is an instance member.
+        -   In the case where the member was found in a base class of the class
+            that was searched, `T` is the derived class that was searched, not
+            the base class in which the name was declared.
+    -   Otherwise, `impl` lookup is not performed:
+        -   `MyInterface.AliasForInterfaceMember` finds the member in the
+            interface `MyInterface` and does not perform `impl` lookup.
+-   For a compound member access `a.(b)` where `b` names a member of an
+    interface `I`, `impl` lookup is performed for `T as I`, where:
+    -   If `b` is an instance member, `T` is the type of `a`.
+        -   `my_value.(Interface.InstanceInterfaceMember)()`, where `my_value`
+            is of type `MyClass`, uses `MyClass as Interface`.
+        -   `MyClass.(Interface.InstanceInterfaceMember)()` uses
+            `type as Interface`.
+    -   Otherwise, `a` is implicitly converted to `I`, and `T` is the result of
+        symbolically evaluating the converted expression.
+        -   `MyClass.(Interface.NonInstanceInterfaceMember)()` uses
+            `MyClass as Interface`.
+        -   `my_value.(Interface.NonInstanceInterfaceMember)()` is an error
+            unless `my_value` implicitly converts to a type.
+
+This approach aims to change as little as possible of the existing `impl` lookup
+behavior while removing inconsistencies and behavioral differences based on
+whether a value is a type.
+
+#### Examples
+
+```
+interface Iface {
+  fn Static();
+  fn Method[me: Self]();
+}
+
+impl type as Iface { ... }
+
+fn F[T:! Iface](x: T) {
+  // ✅ Uses `T as Iface`.
+  x.Static();
+  T.Static();
+  // ❌ Uses `T as Iface`, but method call is missing an instance.
+  T.Method();
+  // ✅ OK, instance is provided. Uses `T as Iface`.
+  x.Method();
+  x.(T.Method)();
+
+  // ❌ Would use `(x as Iface).Static`.
+  // Error because `x` is not a symbolic constant.
+  x.(Iface.Static)();
+  // ✅ Uses `(T as Iface).Static`.
+  T.(Iface.Static)();
+  // ✅ Uses `(type as Iface).Static`.
+  type.(Iface.Static)();
+
+  // ✅ Uses `(T as Iface).Method`, with `me = x`.
+  x.(Iface.Method)();
+  // ✅ Uses `(type as Iface).Method`, with `me = T`.
+  T.(Iface.Method)();
+}
+
+base class Base {
+  fn Static();
+  fn Method[me: Self]();
+  alias IfaceStatic = Iface.Static;
+  alias IfaceMethod = Iface.Method;
+}
+external impl Base as Iface { ... }
+
+fn G(b: Base) {
+  // ✅ OK
+  b.Static();
+  Base.Static();
+  // ❌ Uses `Base as Iface`, but method call is missing an instance.
+  Base.Method();
+  // ✅ OK
+  b.Method();
+  b.(Base.Method)();
+
+  // ✅ OK, same as `(Base as Iface).Static()`.
+  b.IfaceStatic();
+  Base.IfaceStatic();
+  // ❌ Uses `Base as Iface`, but method call is missing an instance.
+  Base.IfaceMethod();
+  // ✅ OK, uses `Base as Iface`.
+  b.IfaceMethod();
+  b.(Base.IfaceMethod)();
+  b.((Base as Iface).Method)();
+  b.(Iface.Method)();
+}
+
+class Derived extends Base {}
+external impl Derived as Iface { ... }
+
+fn H(d: Derived) {
+  // ✅ OK, calls `Base.Static`.
+  d.Static();
+  Derived.Static();
+  // ❌ Uses `Derived as Iface`, but method call is missing an instance.
+  Derived.Method();
+  // ✅ OK, calls `Base.Method`.
+  d.Method();
+  d.(Base.Method)();
+  d.(Derived.Method)();
+
+  // ✅ OK, same as `(Derived as Iface).Static()`.
+  d.IfaceStatic();
+  Derived.IfaceStatic();
+  // ❌ Uses `Derived as Iface`, but method call is missing an instance.
+  Derived.IfaceMethod();
+  // ✅ OK, uses `Derived as Iface`.
+  d.IfaceMethod();
+  d.(Derived.IfaceMethod)();
+  d.((Derived as Iface).Method)();
+  d.(Iface.Method)();
+  // ✅ OK, uses `Base as Iface`.
+  d.(Base.IfaceMethod)();
+  d.((Base as Iface).Method)();
+}
+```
+
+### Tuple and struct literals
+
+A tuple literal such as `(1, 2, 3)` produces a tuple value. Its type cannot be
+written directly as a literal: the literal `(i32, i32, i32)` also produces a
+tuple value, not a type value. However, the type of `(1, 2, 3)` is easy to
+express: it is the result of implicitly converting `(i32, i32, i32)` to a type,
+so for example `(i32, i32, i32) as type` evaluates to the type of `(1, 2, 3)`.
+
+There is no conversion from a tuple type to a tuple value, because tuple types
+are values of type `type`, and the type `type` does not implicitly convert to a
+tuple type. For metaprogramming, it is likely that we will benefit from having a
+mechanism to convert a tuple type into a tuple of types, but this is likely to
+be possible using a variadic:
+
+```
+// Takes a tuple of values. Returns a tuple containing the types of those values.
+fn TupleTypeToTupleOfTypes[Types:! type,...](x: (Types,...)) -> auto {
+  return (Types,...);
+}
+```
+
+### Name lookup into values with constrained types
+
+Given a generic function with a generic type parameter, uses of that parameter
+will be implicitly converted to type `type`. For example:
+
+```
+fn F[T:! Printable](x: T) { x.Print(); }
+```
+
+... is equivalent to ...
+
+```
+fn F[T:! Printable](x: T as type) { x.Print(); }
+```
+
+As a result, we can no longer describe lookup for `x` as looking into the
+type-of-type, that is, the type of the expression after `x:`, because after
+implicit conversion, that expression is of type `type`. Instead, lookup will
+look into the type of `x`, which symbolically evaluates to the value
+corresponding to `T` in type `type`, and will look at that value to determine
+where else to look. Because that value is symbolically the name of a generic
+type parameter, we will look in the type of `T`, which is `Printable`.
+
+### Types in diagnostics
+
+Concern has been raised that this proposal could lead to `as type` appearing
+frequently in diagnostics when types are printed. This is not expected to be the
+case. When a type appears in a diagnostic, it will generally be in one of two
+forms:
+
+-   A reflection of source-level syntax that the programmer wrote.
+-   A string generated by the compiler to describe the type to the programmer.
+
+In both cases, we expect the type of a variable such as `var v: (i32, i32)` to
+be displayed as `(i32, i32)`, not as `(i32, i32) as type`, unless either the
+context requires the `as type` suffix for disambiguation or the programmer wrote
+it in the source code.
+
+This is analogous to how integer literals behave: when describing the value `1`
+of type `i32` in a diagnostic, the type is usually treated as assumed context,
+so the diagnostic would say simply `1` rather than `1 as i32`. Similarly, C++
+compilers typically avoid printing things like `(short)5` when including values
+of type `short`, for which there is no literal syntax, in diagnostics.
+
+## Rationale
+
+-   [Language tools and ecosystem](/docs/project/goals.md#language-tools-and-ecosystem)
+    -   Making the behavior of tuples and empty structs more like other types is
+        easier for tooling to handle.
+-   [Software and language evolution](/docs/project/goals.md#software-and-language-evolution)
+    -   The transition between templates and generics is made smoother by
+        changing compound member access to behave consistently regardless of
+        whether the left-hand operand is a type.
+-   [Code that is easy to read, understand, and write](/docs/project/goals.md#code-that-is-easy-to-read-understand-and-write)
+    -   Bottoming out at the same type, `type`, for all types is likely to be
+        easier to understand. However, having `(i32, i32)` not be the type of a
+        pair of integers, but instead be _implicitly convertible to_ the type of
+        a pair of integers, is likely to be harder to understand. It's unclear
+        which of these will be more dominant, but the new behavior is more
+        consistent.
+
+### Teachability
+
+One of the bigger concerns with this proposal is how teachable it is. The
+details of this model are likely to be challenging for new-comers to Carbon,
+even ones with experience in C++.
+
+When explaining this model, we suggest focusing on the goal and how it is
+achieved, rather than what happens under the covers. For example, we can say
+
+> You can use `var n: (i32, i32)` to declare that `n` is a pair of `i32`s
+
+without mentioning that the actual type of `(i32, i32)` is `(type, type)`, and
+that an implicit conversion is performed here. This is analogous to how we can
+say
+
+> You can use `n = (1, 2);` to assign `1` to the first element of `n` and `2` to
+> the second element
+
+without mentioning that again an implicit conversion is performed.
+
+In practice, this is a relatively small change from Carbon's design prior to
+this proposal, and there are also teachability concerns with the ability to
+treat a tuple of types as a type despite it _not_ being a value of type `type`.
+Should there prove to be sustained problems with teachability, we should
+consider making more significant changes, such as adopting a distinct syntax for
+tuple types and empty structs.
+
+## Alternatives considered
+
+### Alternative member access rules
+
+We considered rules where `T.(Interface.Member)` would either always mean
+`(T as Interface).Member` or always mean `(typeof(T) as Interface).Member`, but
+that did not allow aliases to work as expected. We wanted an alias to an
+interface method or class function defined inside of a class to be usable as a
+method or class function member of the class.
+
+```
+interface A {
+  fn F[me: Self]();
+  fn S();
+}
+class B {
+  external impl as A;
+  alias G = A.F;
+  fn H[me: Self]();
+  alias T = A.S;
+  fn U();
+}
+```
+
+We want `B.G` to act like a method of `B`, like `B.H`, and `B.T` to act like a
+static class function of `B`, like `B.U`. We could have accomplished this by
+requiring those aliases to be written in a different way, for example
+`alias G = (Self as A).F`, but needing to do that was surprising. We made it
+work by making the interpretation of `T.(Interface.Member)` depend on whether
+`Member` was an _instance_ member of `Interface`, with an implicit `me`
+parameter, or not.
+
+This was discussed in
+[the #syntax channel on discord on 2022-11-07](https://discord.com/channels/655572317891461132/709488742942900284/1039298322625744987)
+and in
+[open discussion on 2022-11-10](https://docs.google.com/document/d/1tEt4iM6vfcY0O0DG0uOEMIbaXcZXlNREc2ChNiEtn_w/edit#heading=h.1y65biik2vr).
+
+### Alternative terminology
+
+We considered various alternatives for the terminology choices listed above in
+[open discussion on 2022-10-27](https://docs.google.com/document/d/1tEt4iM6vfcY0O0DG0uOEMIbaXcZXlNREc2ChNiEtn_w/edit#heading=h.lecxe8qywdxa).
+
+Instead of "facet type" we considered:
+
+-   constraint type
+    -   Concern: a "foo type" can mean "a type that is also a foo" like "class
+        type" or it can mean "a type that holds foos" like "integer type".
+-   constrained type
+    -   Concern: for some of us, this name seemed to better describe facets than
+        facet types.
+-   constraint
+    -   Concern: this may sound like it should refer to a boolean predicate,
+        `T is C`, not `C` itself.
+-   kind
+    -   Concern: while this terminology is used to describe the type of a type
+        in computer science literature, that usage is different from this one in
+        that it generally refers to the arity of type constructors rather than
+        classifying subsets of the set of types.
+
+Instead of "generic type" we considered:
+
+-   archetype
+    -   Concern: the usage here didn't match some of our intuitions based on
+        existing usage of this term.
+    -   Concern: while this might fit usage within the scope of the parameter,
+        it fits usage from outside the scope less well. It seemed awkward to say
+        that a class has an archetype parameter, as opposed to our chosen
+        terminology of a generic type parameter.
+-   constrained type variable
+    -   Concern: for some of us, the name "constrained type" seemed to better
+        describe facet types than facets.
+-   type-like
+    -   Concern: derived terms like "generic type-like parameter" and
+        "associated type-like constant" are awkward.
+-   kinded
+    -   Concern: derived terms like "generic kinded parameter" and "associated
+        kinded constant" are awkward.
+
+Instead of "facet" we considered:
+
+-   type
+    -   The idea here is that, because facets can be used in type contexts,
+        calling them types is reasonable.
+    -   Concern: we want `i32 as Sortable` and `i32 as Hashable` to be
+        different, but we do not want to say that they are "different types".
+    -   Concern: we use `type` to refer to types, not facets, and it's important
+        that conversion to type `type` erases the facet type from a facet. If we
+        call facets "types" then we mean different things by "type" and
+        "`type`", and for example conversion of a type to type `type` would
+        change its meaning, which seems surprising.
+-   impl
+    -   Concern: facets are analogous to `impl`s but are not in direct
+        correspondence, because a facet can be for a constraint that involves
+        multiple interfaces and hence potentially multiple `impl`s, and an
+        `impl` can be for a constraint that involves multiple interfaces and
+        hence a facet can refer to only _part of_ an `impl`.
+-   archetype
+    -   Concern: this seems inappropriate for non-generic facets, such as
+        `i32 as Hashable`.
+-   witness
+    -   Concern: doesn't quite represent what we mean: a facet is more like a
+        pair of a type and a witness that that type implements the facet's type.
+
+### `Core.Type` is an empty named constraint
+
+We considered making `type` an alias for an empty type constraint defined in the
+prelude, `Core.Type`. While it is possible to define a constraint that is
+equivalent to `type` as a named constraint, we decided not to define `type` as
+an alias to such a named constraint in order to reduce complexity:
+
+-   Type-checking the prelude itself becomes more challenging if `type` is a
+    named constraint, due to the ubiquity of its usage.
+-   If `type` is an alias to `Core.Type`, then either the implementation would
+    need to ensure that it introduces no member names and no constraints, or it
+    would need to faithfully look into `Core.Type` every type a property of
+    `type` is consulted, adding either compile-time cost or complexity to the
+    implementation.
+
+Given that we have no current desire to add member names or constraints to
+`type`, we do not get any benefit from defining it in the Carbon library. If we
+later choose to make `type` imply some other constraints by default, such as
+`Sized` or `Movable`, this decision should be revisited.
+
+This was discussed in:
+
+-   [#naming on 2022-10-31](https://discord.com/channels/655572317891461132/963846118964350976/1036750048899366954)
+-   [#syntax on 2022-10-27](https://discord.com/channels/655572317891461132/709488742942900284/1035222720864071740)
+-   [open discussion on 2022-10-31](https://docs.google.com/document/d/1tEt4iM6vfcY0O0DG0uOEMIbaXcZXlNREc2ChNiEtn_w/edit#heading=h.9x8m0qwhuux)
+
+### Write tuple types differently than tuples
+
+We considered having the way to write tuple types be different than tuples. So
+instead of `var x: (i32, i32) = (1, 2);` you might write:
+
+```carbon
+var x: TupleType(i32, i32) = (1, 2);
+
+// Or, with dedicated syntax:
+var y: (|i32, i32|) = (1, 2);
+```
+
+There are a few reasons we decided not to go with this approach:
+
+-   There is a significant cost to having more balanced delimiters, particularly
+    ones consisting of multiple characters.
+-   Since types are values in Carbon, `(i32, i32)` is a valid and meaningful
+    expression. Users would be surprised if they cannot use it as a type.
+-   Allowing tuples in pattern syntax but not in type syntax may be surprising.
+    For example, given that `var (x: i32, y: i32);` is valid, it may be
+    surprising if `var p: (i32, i32);` is not valid.
+-   We expect that, when teaching or speaking casually, we would not need to
+    explain that `(i32, i32)` was not a type but was usable as a type. That
+    distinction would generally not affect users, who would generally be able to
+    treat the type of a tuple as the tuple of the types of its elements.
+-   This would prevent operations from working generically on both tuples values
+    and tuple types. We would need to instead duplicate the set of operations.
+    For example, there would need to be separate `TupleCat` and `TupleTypeCat`
+    operations to perform concatenation. This would be extra machinery, and a
+    burden for users to know about all of the functions and call the right one.
+
+This was discussed
+[in the #syntax channel on 2022-11-03](https://discord.com/channels/655572317891461132/708431657849585705/1037793379813167166)
+and
+[in open discussion on on 2022-12-07](https://docs.google.com/document/d/1gnJBTfY81fZYvI_QXjwKk1uQHYBNHGqRLI2BS_cYYNQ/edit?resourcekey=0-ql1Q1WvTcDvhycf8LbA9DQ#heading=h.qu6e01wbzrhz).