diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index 5e3226fe8f40..867f256086f7 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -29,6 +29,8 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception - [Facet types](#facet-types) - [Identified facet types](#identified-facet-types) - [Named constraints](#named-constraints) + - [Rewrites and same-type constraints in a named constraint](#rewrites-and-same-type-constraints-in-a-named-constraint) + - [Constraints that don't depend on `.Self`](#constraints-that-dont-depend-on-self) - [Subtyping between facet types](#subtyping-between-facet-types) - [Combining interfaces by anding facet types](#combining-interfaces-by-anding-facet-types) - [Interface requiring other interfaces](#interface-requiring-other-interfaces) @@ -1110,6 +1112,75 @@ class ImplementsS { } ``` +### Rewrites and same-type constraints in a named constraint + +A `require` statement may include rewrite or same-type constraints. In the case +of `extend require`, the rewrites are +[preserved as such](appendix-rewrite-constraints.md#combining-constraints-with-extend). +But otherwise, any rewrite constraint in the +[identified facet type](#identified-facet-types) of the `require` is +[treated as a same-type constraint](appendix-rewrite-constraints.md#combining-constraints-with-require-and-impls) +instead. + +### Constraints that don't depend on `.Self` + +> **TODO:** Link to section explaining when identifying a facet type happens when +> [#5168: Forward `impl` declaration of an incomplete interface](/proposals/p005168-forward-impl-declaration-of-an-incomplete-interface.md) +> is applied to these docs. + +When identifying a facet type, we collect all constraints found in the facet +type and named constraints. Each constraint must depend on `.Self` in some way +in order to be found in future impl lookups involving the facet being +constrained. Thus, if there is no dependency on `.Self` in a constraint, it must +be satisfied immediately for the identify to complete successfully. + +```carbon +constraint N(T: type) { + require impls Z where .Z1 = {}; +} +``` + +When the above named constraint is identified as part of a facet type as +`C impls N(.Self)`, the resulting requirement `Z where .Z1 = {}` is only +constraining `C`, and not `.Self` from the top-level top-level facet type. So we +require that `C impls (Z where .Z1 = {})` is already true in order to successfully +identify. + +```carbon +interface Z(V: type) { + let Z1: type; + let Z2: type; +} + +constraint M(T2: type, U2: type) { + extend require impls Z(U2) where .Z1 = {} and .Z2 == (); +} + +interface Y { + fn YY(); +} + +class C; + +fn F(U: Y where C impls Z(.Self) where .Z1 = {} and .Z2 == (), + T: Y where C impls M(.Self, U)) { + // Member access into `T` causes its type to be identified, which succeeds. + // The identified facet type requires + // `C impls Z(U) where .Z1 = {} and .Z2 == ()` which is true from the facet + // type of `U`. + T.YY(); +} + +fn G(U: Y where C impls Z(.Self), + T: Y where C impls M(.Self, U)); + // ❌ Error: The type of `T` can not be identified. + // Member access into `T` causes its type to be identified, which fails. + // The identified facet type requires + // `C impls Z(U) where .Z1 = {} and .Z2 == ()` which we don't know to be + // true here. + T.YY(); +``` + ### Subtyping between facet types There is a subtyping relationship between facet types that allows calls of one diff --git a/proposals/p007299-ensure-where-requirements-in-named-constraints-are-visible-to-lookups.md b/proposals/p007299-ensure-where-requirements-in-named-constraints-are-visible-to-lookups.md new file mode 100644 index 000000000000..174371d6f403 --- /dev/null +++ b/proposals/p007299-ensure-where-requirements-in-named-constraints-are-visible-to-lookups.md @@ -0,0 +1,158 @@ +# Ensure `where` requirements in named constraints are visible to lookups + + + +[Pull request](https://github.com/carbon-language/carbon-lang/pull/7299) + + + +## Table of contents + +- [Abstract](#abstract) +- [Problem](#problem) +- [Background](#background) +- [Proposal](#proposal) +- [Rationale](#rationale) +- [Alternatives considered](#alternatives-considered) + - [Diagnosing constraints without a connection to the top-level `.Self` from a `require`](#diagnosing-constraints-without-a-connection-to-the-top-level-self-from-a-require) + + + +## Abstract + +Require rewrite and same-type constraints that do not depend on `.Self` to be +satisfied when a facet type is identified, since those constraints may not be +found later. + +## Problem + +It is possible to construct a named constraint that, when used, produces a +rewrite or same-type constraint with no connection to the top-level facet. This +prevents us from finding the constraint. + +```carbon +constraint N(T: type) { + extend require impls Z where .Z1 = {}; +} + +// No relationship to `U` in `C impls Z where C.Z1 = {}`. +fn F(generic U: type where C impls N(.Self)) { + {} as C.(Z.Z1); +} +``` + +The `extend require` statement constrains `Self` which in this case is `C`. +Since it does not use `T`, it has no connection to `.Self` in the facet type of +`U`. That makes the constraint impossible to find in queries that don't involve +`U` since we will not know to search its facet type. We limit searching to +components of the involved types to avoid a global search. + +## Background + +- The + [rules for rewrite constraints](/docs/design/generics/appendix-rewrite-constraints.md) + in the design. +- The rules are introduced by proposal + [#2 for the rewrite left-hand-side that 173](https://github.com/carbon-language/carbon-lang/blob/358df53c482aeaefc8869ff36f8ef332ec34af3c/proposals/p002173-associated-constant-assignment-versus-equality.md). + +## Proposal + +When identifying a facet type, collect all rewrite and same-type constraints +found while also collecting `impls` constraints from the facet type and any +named constraints it depends on. Require that any constraint which does not +depend on `.Self` is satisfied immediately, in order to identify the facet type. + +During identify, rewrite constraints are collected as rewrite constraints when +they are part of the top-level facet type being identified, or come from an +uninterrupted chain of `extend requires` statements. Otherwise, rewrite +constraints that come from a `requires` statement are collected as same-type +constraints. + +Constraints that do not depend on `.Self` must be immediately satisfied by +performing an impl lookup with that constraint as a condition. In the following +example, the identified facet type of `T` contains a rewrite `C.(Z(U).Z1) = {}` +and the same-type constraint `C.(Z(U).Z2) == ()`. So an impl lookup for `C as +Z(U) where .Z1 = {} and .Z2 == ()` must be satisfied to identify the type of +`T`. In this example, the lookup succeeds by finding a witness with the required +constraints in the facet type of `U`. + +```carbon +interface Z(V: type) { + let Z1: type; + let Z2: type; +} + +constraint N(T2: type, U2: type) { + extend require impls Z(U2) where .Z1 = {} and .Z2 == (); +} + +fn F(U: type where C impls Z(.Self) where .Z1 = {} and .Z2 == (), + T: type where C impls N(.Self, U)); +``` + +It is also possible to find an `impls` constraint that does not depend on +`.Self` in the identified facet type, through a named constraint. + +```carbon +interface Z {} +constraint A(T: type) { + require T impls Z; +} + +// The identified facet type requires `.Self impls Z`, which is then +// symbolically provided by the facet type of `U`. +fn F(U: A(.Self)) {} + +// The identified facet type requires `i32 impls Z`, which must be +// immediately satisfied. +fn G(U: A(i32)) {} +``` + +## Rationale + +We now ensure that constraints introduced by a `requires` clause in a named +constraint are either visible for lookups, or are redundant with existing rules. +This avoids a global search for the constraint, which advances our +[low context-sensitivity principle](/docs/project/principles/low_context_sensitivity.md). + +Bounding the search allows for a faster and simpler toolchain, which aligns with +the project goal for +[fast and scalable development](/docs/project/goals.md#fast-and-scalable-development). + +## Alternatives considered + +### Diagnosing constraints without a connection to the top-level `.Self` from a `require` + +In the following, the rewrite constraint `C.(Z.Z1) = {}` has no connection to +the top-level facet `U` since it does not contain any reference to the top-level +`.Self`. + +```carbon +class C; + +constraint N(T:! type) { + require impls Z where .Z1 = {}; +} + +// No relationship to `U` in `C impls Z where C.Z1 = {}`. +fn F(U:! type where C impls N(.Self)) {} +``` + +We could diagnose during identifying the type of `U` that the `where` contains a +constraint `C.(Z.Z1) = {}` which doesn't involve the self type. This would +reduce the expressiveness of the generics system and produce an error for some +uses of `N` but not for others. + +```carbon +class G(T:! type); + +// Accepted. +fn F(U:! type where G(.Self) impls N(.Self)) {} + +// Rejected. +fn F(U:! type where G({}) impls N(.Self)) {} +```