Переглянути джерело

Preserve named constraints across `where` (#7104)

We were not copying named constraints in the base facet type over to the
result of the WhereExpr eval.

Add tests that cover this by doing `impl as Constraint where ...` with
rewrite contraints either in the impl-as or in the named constraint.
When the interface is generic, these tests fail (as TODOs). When the
impl is used in impl lookup, we crash (with TODOs in the tests).

Part of #6991.
Dana Jansens 1 тиждень тому
батько
коміт
9c9f5cb52c

+ 3 - 0
toolchain/check/eval.cpp

@@ -2568,7 +2568,10 @@ static auto AddRequirementBase(Context& context,
     const auto& base_info =
     const auto& base_info =
         context.facet_types().Get(base_facet_type->facet_type_id);
         context.facet_types().Get(base_facet_type->facet_type_id);
     info->extend_constraints.append(base_info.extend_constraints);
     info->extend_constraints.append(base_info.extend_constraints);
+    info->extend_named_constraints.append(base_info.extend_named_constraints);
     info->self_impls_constraints.append(base_info.self_impls_constraints);
     info->self_impls_constraints.append(base_info.self_impls_constraints);
+    info->self_impls_named_constraints.append(
+        base_info.self_impls_named_constraints);
     info->type_impls_interfaces.append(base_info.type_impls_interfaces);
     info->type_impls_interfaces.append(base_info.type_impls_interfaces);
     info->type_impls_named_constraints.append(
     info->type_impls_named_constraints.append(
         base_info.type_impls_named_constraints);
         base_info.type_impls_named_constraints);

+ 2 - 2
toolchain/check/testdata/facet/validate_impl_constraints.carbon

@@ -150,7 +150,7 @@ fn G() {
   impl C as Z {}
   impl C as Z {}
   impl C as Y {}
   impl C as Y {}
   impl C as X(C) {}
   impl C as X(C) {}
-  // CHECK:STDERR: fail_todo_where_period_self_rhs_sees_lhs.carbon:[[@LINE+7]]:3: error: cannot convert type `C` into type implementing `Z where .Self impls X(.Self as Z & Y)` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR: fail_todo_where_period_self_rhs_sees_lhs.carbon:[[@LINE+7]]:3: error: cannot convert type `C` into type implementing `Z & N where .Self impls X(.Self as Z & Y)` [ConversionFailureTypeToFacet]
   // CHECK:STDERR:   F(C);
   // CHECK:STDERR:   F(C);
   // CHECK:STDERR:   ^~~~
   // CHECK:STDERR:   ^~~~
   // CHECK:STDERR: fail_todo_where_period_self_rhs_sees_lhs.carbon:[[@LINE-10]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
   // CHECK:STDERR: fail_todo_where_period_self_rhs_sees_lhs.carbon:[[@LINE-10]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
@@ -181,7 +181,7 @@ fn G() {
   impl C as Z {}
   impl C as Z {}
   impl C as Y {}
   impl C as Y {}
   impl R(C) as X(C) {}
   impl R(C) as X(C) {}
-  // CHECK:STDERR: fail_todo_where_type_rhs_sees_lhs.carbon:[[@LINE+7]]:3: error: cannot convert type `C` into type implementing `Z where R(.Self as Z & Y) impls X(.Self as Z & Y)` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR: fail_todo_where_type_rhs_sees_lhs.carbon:[[@LINE+7]]:3: error: cannot convert type `C` into type implementing `Z & N where R(.Self as Z & Y) impls X(.Self as Z & Y)` [ConversionFailureTypeToFacet]
   // CHECK:STDERR:   F(C);
   // CHECK:STDERR:   F(C);
   // CHECK:STDERR:   ^~~~
   // CHECK:STDERR:   ^~~~
   // CHECK:STDERR: fail_todo_where_type_rhs_sees_lhs.carbon:[[@LINE-10]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
   // CHECK:STDERR: fail_todo_where_type_rhs_sees_lhs.carbon:[[@LINE-10]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]

+ 122 - 0
toolchain/check/testdata/impl/impl_as_named_constraint.carbon

@@ -169,6 +169,128 @@ constraint B(X:! Undefined) {
 
 
 impl () as B(1) {}
 impl () as B(1) {}
 
 
+// --- impl_as_constraint_where_rewrite.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let I1:! type;
+}
+
+constraint N {
+  extend require impls I;
+}
+
+class C;
+impl C as N where .I1 = C {}
+
+fn F(_:! I where .I1 = .Self) {}
+fn G() {
+// TODO: This crashes.
+//   F(C);
+}
+
+// --- impl_as_concrete_generic_constraint_where_rewrite.carbon
+library "[[@TEST_NAME]]";
+
+interface I(T:! type) {
+  let I1:! type;
+}
+
+class C;
+
+constraint N {
+  extend require impls I(C);
+}
+
+impl C as N where .I1 = C {}
+
+fn F(_:! I(.Self) where .I1 = .Self) {}
+fn G() {
+// TODO: This crashes.
+//   F(C);
+}
+
+// --- fail_todo_impl_as_symbolic_generic_constraint_where_rewrite.carbon
+library "[[@TEST_NAME]]";
+
+interface I(T:! type) {
+  let I1:! type;
+}
+
+constraint N {
+  extend require impls I(Self);
+}
+
+class C;
+// CHECK:STDERR: fail_todo_impl_as_symbolic_generic_constraint_where_rewrite.carbon:[[@LINE+7]]:1: error: associated constant I1 not given a value in impl of interface I [ImplAssociatedConstantNeedsValue]
+// CHECK:STDERR: impl C as N where .I1 = C {}
+// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR: fail_todo_impl_as_symbolic_generic_constraint_where_rewrite.carbon:[[@LINE-11]]:7: note: associated constant declared here [AssociatedConstantHere]
+// CHECK:STDERR:   let I1:! type;
+// CHECK:STDERR:       ^~~~~~~~~
+// CHECK:STDERR:
+impl C as N where .I1 = C {}
+
+fn F(_:! I(.Self) where .I1 = .Self) {}
+fn G() {
+// TODO: This crashes.
+//   F(C);
+}
+
+// --- fail_todo_impl_as_constraint_containing_rewrite_for_concrete_interface.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  let I1:! type;
+}
+
+constraint N {
+  extend require impls I where .I1 = Self;
+}
+
+class C;
+// CHECK:STDERR: fail_todo_impl_as_constraint_containing_rewrite_for_concrete_interface.carbon:[[@LINE+7]]:1: error: associated constant I1 not given a value in impl of interface I [ImplAssociatedConstantNeedsValue]
+// CHECK:STDERR: impl C as N {}
+// CHECK:STDERR: ^~~~~~~~~~~~~
+// CHECK:STDERR: fail_todo_impl_as_constraint_containing_rewrite_for_concrete_interface.carbon:[[@LINE-11]]:7: note: associated constant declared here [AssociatedConstantHere]
+// CHECK:STDERR:   let I1:! type;
+// CHECK:STDERR:       ^~~~~~~~~
+// CHECK:STDERR:
+impl C as N {}
+
+fn F(_:! I where .I1 = .Self) {}
+fn G() {
+// TODO: This crashes.
+//   F(C);
+}
+
+// --- fail_todo_impl_as_constraint_containing_rewrite_for_generic_interface.carbon
+library "[[@TEST_NAME]]";
+
+interface I(T:! type) {
+  let I1:! type;
+}
+
+constraint N {
+  extend require impls I(Self) where .I1 = Self;
+}
+
+class C;
+// CHECK:STDERR: fail_todo_impl_as_constraint_containing_rewrite_for_generic_interface.carbon:[[@LINE+7]]:1: error: associated constant I1 not given a value in impl of interface I [ImplAssociatedConstantNeedsValue]
+// CHECK:STDERR: impl C as N {}
+// CHECK:STDERR: ^~~~~~~~~~~~~
+// CHECK:STDERR: fail_todo_impl_as_constraint_containing_rewrite_for_generic_interface.carbon:[[@LINE-11]]:7: note: associated constant declared here [AssociatedConstantHere]
+// CHECK:STDERR:   let I1:! type;
+// CHECK:STDERR:       ^~~~~~~~~
+// CHECK:STDERR:
+impl C as N {}
+
+fn F(_:! I(.Self) where .I1 = .Self) {}
+fn G() {
+// TODO: This crashes.
+//   F(C);
+}
+
 // CHECK:STDOUT: --- fail_error_self_in_require.carbon
 // CHECK:STDOUT: --- fail_error_self_in_require.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
 // CHECK:STDOUT: constants {