carbon-language/carbon-lang
1
0
Fork 0
mirror of https://github.com/carbon-language/carbon-lang.git synced 2026-10-05 22:02:55 +01:00
Code Issues Packages Projects Releases 10 Wiki Activity

Set the value of .Self in a where to that of the outer .Self. (#2344)

Browse Source 
Prior to this change, declarations like `let N:! X(.Self) where .(X(.Self).Y) == 5;` have the surprising behavior of the two `.Self` expressions resolving to two different symbolic values. Fix this by forcing the inner one to have the same symbolic value as the outer one, albeit with a different type.
This commit is contained in:
Richard Smith
2022-10-25 11:59:42 -07:00
committed by GitHub
parent c68cced1fb
commit bc7bf325d6
8 changed files with 69 additions and 44 deletions
Download Patch File Download Diff File Expand all files Collapse all files
explorer/testdata/assoc_const/fail_impl_used_by_later_rewrite.carbon
Vendored
+4 -3
View File
@@ -17,14 +17,15 @@ interface Y(T:! Type) {
interface Z {
// The `i32 is X(.Self)` constraint is indirectly required by
// specifying that `.M = i32`.
// TODO: This testcase should be accepted, but is currently not because the
// two `.Self`s here refer to different symbolic types.
// CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_impl_used_by_later_rewrite.carbon:[[@LINE+1]]: could not find implementation of interface X(T = N) for i32
let N:! Y(.Self) where i32 is X(.Self) and .M = i32;
}
impl i32 as X(i32) {}
impl i32 as Y(i32) where .M = i32 {}
// TODO: This testcase should be accepted, but is currently not because the
// rewrite for `.N` is not properly applied to impl constraints within the type
// of N.
// CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_impl_used_by_later_rewrite.carbon:[[@LINE+1]]: could not find implementation of interface Y(T = (.Self).(Z.N)) for i32
impl i32 as Z where .N = i32 {}
fn F[A:! Z](a: A) -> A { return a; }
explorer/testdata/assoc_const/fail_implied_constraints.carbon
Vendored
+2 -8
View File
@@ -18,16 +18,10 @@ interface Z {
// We reject this even though it is the responsibility of the `impl as Z` to
// provide a type `N` such that `i32 is X(N)`. We might want to treat this as
// an implied constraint and allow this in the future.
// CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_implied_constraints.carbon:[[@LINE+1]]: could not find implementation of interface X(T = N) for i32
// CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_implied_constraints.carbon:[[@LINE+1]]: could not find implementation of interface X(T = (Self).(Z.N)) for i32
let N:! Y(.Self) where .M = i32;
}
impl i32 as X(i32) {}
impl i32 as Y(i32) where .M = i32 {}
impl i32 as Z where .N = i32 {}
fn F[A:! Z](a: A) -> A { return a; }
fn Main() -> i32 {
return F(0);
return 0;
}
explorer/testdata/assoc_const/fail_rewrite_depends_on_later_rewrite.carbon
Vendored
+1 -1
View File
@@ -13,7 +13,7 @@ interface HasTypeAndValue {
let V:! T;
}
// CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_rewrite_depends_on_later_rewrite.carbon:[[@LINE+1]]: type error in rewrite constraint: 'i32' is not implicitly convertible to '(.Self).(HasTypeAndValue.T)'
// CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_rewrite_depends_on_later_rewrite.carbon:[[@LINE+1]]: type error in rewrite constraint: 'i32' is not implicitly convertible to '(X).(HasTypeAndValue.T)'
fn F(X:! HasTypeAndValue where .V = 5 and .T = i32) -> i32 { return X.V; }
impl i32 as HasTypeAndValue where .T = i32 and .V = 5 {}