Skip to content

Commit a5a5e38

Browse files
danakjdanakj
authored
More tests for early rewrite application and implied constraints (#5892)
Attempting to capture all the use cases described in [open discussion 2025-07-31](https://docs.google.com/document/d/1Yt-i5AmF76LSvD4TrWRIAE_92kii6j5yFiW-S7ahzlg/edit?tab=t.0#heading=h.lup43xycic7t).
1 parent 7198050 commit a5a5e38

File tree

2 files changed

+305
-18
lines changed

2 files changed

+305
-18
lines changed

‎toolchain/check/testdata/facet/early_rewrites.carbon

Lines changed: 262 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,11 @@
1313
// Tests where `ImplWitnessAccess` on the RHS of a rewrite constraint is used in
1414
// other constraints within the same facet type in ways that require the RHS to
1515
// be evaluated to a concrete value before the facet type is resolved (such as
16-
// by passing it as a parameter to a generic class).
16+
// by passing it as a parameter to a generic class). This can be done either by
17+
// eagerly reading rewrite constraints from the same facet type, or by relying
18+
// on implied constraints which are checked later.
1719

18-
// --- nested_constraint_visible_in_type_parameter.carbon
20+
// --- fail_todo_implied_constraint_on_self.carbon
1921
library "[[@TEST_NAME]]";
2022

2123
interface Z {
@@ -26,9 +28,140 @@ interface Z {
2628
class C(T:! Z where .Z1 = ()) {}
2729

2830
interface J {
31+
// Implied: .Z1 == ()
32+
// CHECK:STDERR: fail_todo_implied_constraint_on_self.carbon:[[@LINE+7]]:26: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
33+
// CHECK:STDERR: let J1:! Z where .Z2 = C(.Self);
34+
// CHECK:STDERR: ^~~~~~~~
35+
// CHECK:STDERR: fail_todo_implied_constraint_on_self.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
36+
// CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
37+
// CHECK:STDERR: ^
38+
// CHECK:STDERR:
39+
let J1:! Z where .Z2 = C(.Self);
40+
}
41+
42+
fn F(T:! J) {}
43+
44+
class D;
45+
// Satisfies the implied constraint in J.J1.
46+
// CHECK:STDERR: fail_todo_implied_constraint_on_self.carbon:[[@LINE+7]]:38: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
47+
// CHECK:STDERR: impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
48+
// CHECK:STDERR: ^~~~~~~~
49+
// CHECK:STDERR: fail_todo_implied_constraint_on_self.carbon:[[@LINE-21]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
50+
// CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
51+
// CHECK:STDERR: ^
52+
// CHECK:STDERR:
53+
impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
54+
fn G(T:! J where .J1 = D) {
55+
F(T);
56+
}
57+
58+
// --- fail_todo_implied_constraint_on_associated_constant.carbon
59+
library "[[@TEST_NAME]]";
60+
61+
interface Z {
62+
let Z1:! type;
63+
let Z2:! type;
64+
}
65+
66+
interface Tuple {}
67+
impl () as Tuple {}
68+
69+
class C(T:! Tuple) {}
70+
71+
interface J {
72+
// Implied: .Z1 impls Tuple
73+
// CHECK:STDERR: fail_todo_implied_constraint_on_associated_constant.carbon:[[@LINE+7]]:26: error: cannot convert type `.(Z.Z1)` into type implementing `Tuple` [ConversionFailureTypeToFacet]
74+
// CHECK:STDERR: let J1:! Z where .Z2 = C(.Z1);
75+
// CHECK:STDERR: ^~~~~~
76+
// CHECK:STDERR: fail_todo_implied_constraint_on_associated_constant.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
77+
// CHECK:STDERR: class C(T:! Tuple) {}
78+
// CHECK:STDERR: ^
79+
// CHECK:STDERR:
80+
let J1:! Z where .Z2 = C(.Z1);
81+
}
82+
83+
fn F(T:! J) {}
84+
85+
class D;
86+
// Satisfies the implied constraint in J.J1.
87+
impl D as Z where .Z1 = () and .Z2 = C(()) {}
88+
fn G(T:! J where .J1 = D) {
89+
F(T);
90+
}
91+
92+
// --- fail_todo_nested_constraint_visible_in_type_parameter.carbon
93+
library "[[@TEST_NAME]]";
94+
95+
interface Z {
96+
let Z1:! type;
97+
let Z2:! type;
98+
}
99+
100+
class C(T:! Z where .Z1 = ()) {}
101+
102+
interface J {
103+
// Implied: .Z1 == (), but this is also explicitly required for J1.
29104
let J1:! (Z where .Z1 = ()) where .Z2 = C(.Self);
30105
}
31106

107+
fn F(T:! J) {}
108+
109+
class D;
110+
// Satisfies the implied constraint in J.J1.
111+
// CHECK:STDERR: fail_todo_nested_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:38: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
112+
// CHECK:STDERR: impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
113+
// CHECK:STDERR: ^~~~~~~~
114+
// CHECK:STDERR: fail_todo_nested_constraint_visible_in_type_parameter.carbon:[[@LINE-14]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
115+
// CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
116+
// CHECK:STDERR: ^
117+
// CHECK:STDERR:
118+
impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
119+
// CHECK:STDERR: fail_todo_nested_constraint_visible_in_type_parameter.carbon:[[@LINE+4]]:24: error: cannot convert type `D` into type implementing `Z where .(Z.Z1) = () and .(Z.Z2) = C(.Self)` [ConversionFailureTypeToFacet]
120+
// CHECK:STDERR: fn G(T:! J where .J1 = D) {
121+
// CHECK:STDERR: ^
122+
// CHECK:STDERR:
123+
fn G(T:! J where .J1 = D) {
124+
F(T);
125+
}
126+
127+
// --- fail_todo_outer_nested_constraint_visible_in_type_parameter.carbon
128+
library "[[@TEST_NAME]]";
129+
130+
interface Z {
131+
let Z1:! type;
132+
let Z2:! type;
133+
}
134+
135+
class C(T:! Z where .Z1 = ()) {}
136+
137+
interface J {
138+
// Implied: .Z1 == (), but this is also explicitly required for J1.
139+
// CHECK:STDERR: fail_todo_outer_nested_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:27: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
140+
// CHECK:STDERR: let J1:! (Z where .Z2 = C(.Self)) where .Z1 = ();
141+
// CHECK:STDERR: ^~~~~~~~
142+
// CHECK:STDERR: fail_todo_outer_nested_constraint_visible_in_type_parameter.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
143+
// CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
144+
// CHECK:STDERR: ^
145+
// CHECK:STDERR:
146+
let J1:! (Z where .Z2 = C(.Self)) where .Z1 = ();
147+
}
148+
149+
fn F(T:! J) {}
150+
151+
class D;
152+
// Satisfies the implied constraint in J.J1.
153+
// CHECK:STDERR: fail_todo_outer_nested_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:38: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
154+
// CHECK:STDERR: impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
155+
// CHECK:STDERR: ^~~~~~~~
156+
// CHECK:STDERR: fail_todo_outer_nested_constraint_visible_in_type_parameter.carbon:[[@LINE-21]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
157+
// CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
158+
// CHECK:STDERR: ^
159+
// CHECK:STDERR:
160+
impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
161+
fn G(T:! J where .J1 = D) {
162+
F(T);
163+
}
164+
32165
// --- fail_todo_earlier_constraint_visible_in_type_parameter.carbon
33166
library "[[@TEST_NAME]]";
34167

@@ -39,20 +172,34 @@ interface Z {
39172

40173
class C(T:! Z where .Z1 = ()) {}
41174

42-
// TODO: Should this pass? Or do we need a `where` between .Z1 and .Z2 to make
43-
// .Z1's value visible to .Z2?
44-
// See https://github.com/carbon-language/carbon-lang/issues/5884.
45175
interface J {
176+
// Implied: .Z1 == (), but this is also explicitly required for J1.
46177
// CHECK:STDERR: fail_todo_earlier_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:39: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
47178
// CHECK:STDERR: let J1:! Z where .Z1 = () and .Z2 = C(.Self);
48179
// CHECK:STDERR: ^~~~~~~~
49-
// CHECK:STDERR: fail_todo_earlier_constraint_visible_in_type_parameter.carbon:[[@LINE-9]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
180+
// CHECK:STDERR: fail_todo_earlier_constraint_visible_in_type_parameter.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
50181
// CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
51182
// CHECK:STDERR: ^
52183
// CHECK:STDERR:
53184
let J1:! Z where .Z1 = () and .Z2 = C(.Self);
54185
}
55186

187+
fn F(T:! J) {}
188+
189+
class D;
190+
// Satisfies the implied constraint in J.J1.
191+
// CHECK:STDERR: fail_todo_earlier_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:38: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
192+
// CHECK:STDERR: impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
193+
// CHECK:STDERR: ^~~~~~~~
194+
// CHECK:STDERR: fail_todo_earlier_constraint_visible_in_type_parameter.carbon:[[@LINE-21]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
195+
// CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
196+
// CHECK:STDERR: ^
197+
// CHECK:STDERR:
198+
impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
199+
fn G(T:! J where .J1 = D) {
200+
F(T);
201+
}
202+
56203
// --- fail_todo_later_constraint_visible_in_type_parameter.carbon
57204
library "[[@TEST_NAME]]";
58205

@@ -63,20 +210,105 @@ interface Z {
63210

64211
class C(T:! Z where .Z1 = ()) {}
65212

66-
// TODO: Should this pass? Or do we need a `where` between .Z1 and .Z2 to make
67-
// .Z1's value visible to .Z2?
68-
// See https://github.com/carbon-language/carbon-lang/issues/5884.
69213
interface J {
214+
// Implied: .Z1 == (), but this is also explicitly required for J1.
70215
// CHECK:STDERR: fail_todo_later_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:26: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
71216
// CHECK:STDERR: let J1:! Z where .Z2 = C(.Self) and .Z1 = ();
72217
// CHECK:STDERR: ^~~~~~~~
73-
// CHECK:STDERR: fail_todo_later_constraint_visible_in_type_parameter.carbon:[[@LINE-9]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
218+
// CHECK:STDERR: fail_todo_later_constraint_visible_in_type_parameter.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
74219
// CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
75220
// CHECK:STDERR: ^
76221
// CHECK:STDERR:
77222
let J1:! Z where .Z2 = C(.Self) and .Z1 = ();
78223
}
79224

225+
fn F(T:! J) {}
226+
227+
class D;
228+
// Satisfies the implied constraint in J.J1.
229+
// CHECK:STDERR: fail_todo_later_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:38: error: cannot convert type `.Self` that implements `Z` into type implementing `Z where .(Z.Z1) = ()` [ConversionFailureFacetToFacet]
230+
// CHECK:STDERR: impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
231+
// CHECK:STDERR: ^~~~~~~~
232+
// CHECK:STDERR: fail_todo_later_constraint_visible_in_type_parameter.carbon:[[@LINE-21]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
233+
// CHECK:STDERR: class C(T:! Z where .Z1 = ()) {}
234+
// CHECK:STDERR: ^
235+
// CHECK:STDERR:
236+
impl D as Z where .Z1 = () and .Z2 = C(.Self) {}
237+
fn G(T:! J where .J1 = D) {
238+
F(T);
239+
}
240+
241+
// --- fail_todo_early_rewrite_applied.carbon
242+
library "[[@TEST_NAME]]";
243+
244+
interface Z {
245+
let Z1:! type;
246+
let Z2:! type;
247+
}
248+
249+
interface Tuple {}
250+
impl () as Tuple {}
251+
class C(T:! Tuple) {}
252+
253+
interface J {
254+
// Implied: .Z1 == (), but this is also explicitly required for J1.
255+
// CHECK:STDERR: fail_todo_early_rewrite_applied.carbon:[[@LINE+7]]:39: error: cannot convert type `.(Z.Z1)` into type implementing `Tuple` [ConversionFailureTypeToFacet]
256+
// CHECK:STDERR: let J1:! Z where .Z1 = () and .Z2 = C(.Z1);
257+
// CHECK:STDERR: ^~~~~~
258+
// CHECK:STDERR: fail_todo_early_rewrite_applied.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
259+
// CHECK:STDERR: class C(T:! Tuple) {}
260+
// CHECK:STDERR: ^
261+
// CHECK:STDERR:
262+
let J1:! Z where .Z1 = () and .Z2 = C(.Z1);
263+
}
264+
265+
fn F(T:! J) {}
266+
267+
class D;
268+
// Satisfies the implied constraint in J.J1.
269+
impl D as Z where .Z1 = () and .Z2 = C(()) {}
270+
fn G(T:! J where .J1 = D) {
271+
F(T);
272+
}
273+
274+
// --- fail_todo_early_rewrite_applied_extra_indirection.carbon
275+
library "[[@TEST_NAME]]";
276+
277+
interface Z {
278+
let Z1:! type;
279+
let Z2:! type;
280+
}
281+
282+
interface Y {
283+
let Y1:! Z;
284+
}
285+
286+
interface Tuple {}
287+
impl () as Tuple {}
288+
class C(T:! Tuple) {}
289+
290+
interface J {
291+
// Implied: .Z1 == (), but this is also explicitly required for J1.
292+
// CHECK:STDERR: fail_todo_early_rewrite_applied_extra_indirection.carbon:[[@LINE+7]]:59: error: cannot convert type `.(Y.Y1).(Z.Z1)` into type implementing `Tuple` [ConversionFailureTypeToFacet]
293+
// CHECK:STDERR: let J1:! Y & Z where .Y1 = .Self and .Z1 = () and .Z2 = C(.Y1.Z1);
294+
// CHECK:STDERR: ^~~~~~~~~
295+
// CHECK:STDERR: fail_todo_early_rewrite_applied_extra_indirection.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
296+
// CHECK:STDERR: class C(T:! Tuple) {}
297+
// CHECK:STDERR: ^
298+
// CHECK:STDERR:
299+
let J1:! Y & Z where .Y1 = .Self and .Z1 = () and .Z2 = C(.Y1.Z1);
300+
}
301+
302+
fn F(T:! J) {}
303+
304+
class D;
305+
// Satisfies the implied constraint in J.J1.
306+
impl D as Z where .Z1 = () and .Z2 = C(()) {}
307+
impl D as Y where .Y1 = D {}
308+
fn G(T:! J where .J1 = D) {
309+
F(T);
310+
}
311+
80312
// --- fail_todo_resolved_constraint_visible_in_type_parameter.carbon
81313
library "[[@TEST_NAME]]";
82314

@@ -94,16 +326,28 @@ interface Tuple {}
94326
impl () as Tuple {}
95327
class C(T:! Tuple) {}
96328

97-
// TODO: Should this pass? Or do we need a `where` between .Z2 and .Z3 to make
98-
// .Z2's value visible to .Z3?
99-
// See https://github.com/carbon-language/carbon-lang/issues/5884.
100329
interface J {
101-
// CHECK:STDERR: fail_todo_resolved_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:80: error: cannot convert type `.(Z.Z2)` into type implementing `Tuple` [ConversionFailureTypeToFacet]
102-
// CHECK:STDERR: let J1:! (Z & Y where .Y1 = ()) where .Z1 = .Self and .Z2 = .Z1.Y1 and .Z3 = C(.Z2);
103-
// CHECK:STDERR: ^~~~~~
104-
// CHECK:STDERR: fail_todo_resolved_constraint_visible_in_type_parameter.carbon:[[@LINE-9]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
330+
// Implied: .Y1 impls Tuple, but this is also explicitly required for J1.
331+
// CHECK:STDERR: fail_todo_resolved_constraint_visible_in_type_parameter.carbon:[[@LINE+7]]:76: error: cannot convert type `.(Z.Z2)` into type implementing `Tuple` [ConversionFailureTypeToFacet]
332+
// CHECK:STDERR: let J1:! Z & Y where .Y1 = () and .Z1 = .Self and .Z2 = .Z1.Y1 and .Z3 = C(.Z2);
333+
// CHECK:STDERR: ^~~~~~
334+
// CHECK:STDERR: fail_todo_resolved_constraint_visible_in_type_parameter.carbon:[[@LINE-7]]:9: note: initializing generic parameter `T` declared here [InitializingGenericParam]
105335
// CHECK:STDERR: class C(T:! Tuple) {}
106336
// CHECK:STDERR: ^
107337
// CHECK:STDERR:
108-
let J1:! (Z & Y where .Y1 = ()) where .Z1 = .Self and .Z2 = .Z1.Y1 and .Z3 = C(.Z2);
338+
let J1:! Z & Y where .Y1 = () and .Z1 = .Self and .Z2 = .Z1.Y1 and .Z3 = C(.Z2);
339+
}
340+
341+
fn F(T:! J) {}
342+
343+
class D;
344+
// Satisfies the implied constraint in J.J1.
345+
impl D as Y where .Y1 = () {}
346+
// CHECK:STDERR: fail_todo_resolved_constraint_visible_in_type_parameter.carbon:[[@LINE+4]]:25: error: cannot convert type `.Self` that implements `Z` into type implementing `Y` [ConversionFailureFacetToFacet]
347+
// CHECK:STDERR: impl D as Z where .Z1 = .Self and .Z2 = () and .Z3 = C(()) {}
348+
// CHECK:STDERR: ^~~~~
349+
// CHECK:STDERR:
350+
impl D as Z where .Z1 = .Self and .Z2 = () and .Z3 = C(()) {}
351+
fn G(T:! J where .J1 = D) {
352+
F(T);
109353
}

‎toolchain/check/testdata/impl/impl_assoc_const.carbon

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -344,6 +344,49 @@ interface M { let X:! type; }
344344

345345
impl () as M where .X = (M where .X = (M where .X = {})) {}
346346

347+
// --- fail_todo_period_self_impl_lookup.carbon
348+
library "[[@TEST_NAME]]";
349+
350+
interface Y {}
351+
interface Z {
352+
let Z1:! Y;
353+
}
354+
355+
class C;
356+
impl C as Y {}
357+
// CHECK:STDERR: fail_todo_period_self_impl_lookup.carbon:[[@LINE+4]]:25: error: cannot convert type `.Self` that implements `Z` into type implementing `Y` [ConversionFailureFacetToFacet]
358+
// CHECK:STDERR: impl C as Z where .Z1 = .Self {}
359+
// CHECK:STDERR: ^~~~~
360+
// CHECK:STDERR:
361+
impl C as Z where .Z1 = .Self {}
362+
363+
// --- fail_todo_period_self_compared_with_concrete_self.carbon
364+
library "[[@TEST_NAME]]";
365+
366+
interface Y {}
367+
interface Z {
368+
let Z1:! Y;
369+
}
370+
371+
class C;
372+
impl C as Y {}
373+
impl C as Z where .Z1 = C {}
374+
375+
// CHECK:STDERR: fail_todo_period_self_compared_with_concrete_self.carbon:[[@LINE+4]]:24: error: cannot convert type `.Self` that implements `Z` into type implementing `Y` [ConversionFailureFacetToFacet]
376+
// CHECK:STDERR: fn F(T:! Z where .Z1 = .Self) {}
377+
// CHECK:STDERR: ^~~~~
378+
// CHECK:STDERR:
379+
fn F(T:! Z where .Z1 = .Self) {}
380+
fn G() {
381+
F(C);
382+
383+
// CHECK:STDERR: fail_todo_period_self_compared_with_concrete_self.carbon:[[@LINE+4]]:23: error: cannot convert type `.Self` that implements `Z` into type implementing `Y` [ConversionFailureFacetToFacet]
384+
// CHECK:STDERR: C as (Z where .Z1 = .Self);
385+
// CHECK:STDERR: ^~~~~
386+
// CHECK:STDERR:
387+
C as (Z where .Z1 = .Self);
388+
}
389+
347390
// CHECK:STDOUT: --- fail_many_different.carbon
348391
// CHECK:STDOUT:
349392
// CHECK:STDOUT: constants {

0 commit comments

Comments
 (0)