Skip to content

Fixes #1477. [Records] Type inference tests updated #1500

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Oct 21, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 22 additions & 3 deletions LanguageFeatures/Records/type_inference_A01_t01.dart
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,28 @@
// for details. All rights reserved. Use of this source code is governed by a
// BSD-style license that can be found in the LICENSE file.

/// @assertion Type inference and promotion flows through records in much the
/// same way it does for instances of generic classes (which are covariant in
/// Dart just like record fields are) and collection literals.
/// @assertion Given a type schema K and a record expression E of the general
/// form (e1, ..., en, d1 : e{n+1}, ..., dm : e{n+m}) inference proceeds as
/// follows.
///
/// If K is a record type schema of the form
/// (K1, ..., Kn, {d1 : K{n+1}, ...., dm : K{n+m}}) then:
///
/// - Each ei is inferred with context type schema Ki to have type Si
/// - Let Ri be the greatest closure of Ki
/// - If Si is a subtype of Ri then let Ti be Si
/// - Otherwise, if Si is dynamic, then we insert an implicit cast on ei to
/// Ri, and let Ti be Ri
/// - Otherwise, if Si is coercible to Ri (via some sequence of call method
/// tearoff or implicit generic instantiation coercions), then we insert the
/// appropriate implicit coercion(s) on ei. Let Ti be the type of the
/// resulting coerced value (which must be a subtype of Ri, possibly proper).
/// - Otherwise, it is a static error.
/// - The type of E is (T1, ..., Tn, {d1 : T{n+1}, ...., dm : T{n+m}})
/// If K is any other type schema:
///
/// - Each ei is inferred with context type schema _ to have type Ti
/// - The type of E is (T1, ..., Tn, {d1 : T{n+1}, ...., dm : T{n+m}})
///
/// @description Checks type inference for records.
/// @author [email protected]
Expand Down
41 changes: 41 additions & 0 deletions LanguageFeatures/Records/type_inference_A01_t02.dart
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
// Copyright (c) 2022, the Dart project authors. Please see the AUTHORS file
// for details. All rights reserved. Use of this source code is governed by a
// BSD-style license that can be found in the LICENSE file.

/// @assertion Given a type schema K and a record expression E of the general
/// form (e1, ..., en, d1 : e{n+1}, ..., dm : e{n+m}) inference proceeds as
/// follows.
///
/// If K is a record type schema of the form
/// (K1, ..., Kn, {d1 : K{n+1}, ...., dm : K{n+m}}) then:
///
/// - Each ei is inferred with context type schema Ki to have type Si
/// - Let Ri be the greatest closure of Ki
/// - If Si is a subtype of Ri then let Ti be Si
/// - Otherwise, if Si is dynamic, then we insert an implicit cast on ei to
/// Ri, and let Ti be Ri
/// - Otherwise, if Si is coercible to Ri (via some sequence of call method
/// tearoff or implicit generic instantiation coercions), then we insert the
/// appropriate implicit coercion(s) on ei. Let Ti be the type of the
/// resulting coerced value (which must be a subtype of Ri, possibly proper).
/// - Otherwise, it is a static error.
/// - The type of E is (T1, ..., Tn, {d1 : T{n+1}, ...., dm : T{n+m}})
/// If K is any other type schema:
///
/// - Each ei is inferred with context type schema _ to have type Ti
/// - The type of E is (T1, ..., Tn, {d1 : T{n+1}, ...., dm : T{n+m}})
///
/// @description Checks type inference for records.
/// @author [email protected]

// SharedOptions=--enable-experiment=records

main() {
(num,) r1 = (42,) ..$0.isOdd;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, yes, we can do that, cool!


({num n}) r2 = (n: 42) ..n.isOdd;

(num, {Object s}) r3 = (42, s: "")
..$0.isOdd
..s.substring(0);
}
62 changes: 62 additions & 0 deletions LanguageFeatures/Records/type_inference_A01_t03.dart
Original file line number Diff line number Diff line change
@@ -0,0 +1,62 @@
// Copyright (c) 2022, the Dart project authors. Please see the AUTHORS file
// for details. All rights reserved. Use of this source code is governed by a
// BSD-style license that can be found in the LICENSE file.

/// @assertion Given a type schema K and a record expression E of the general
/// form (e1, ..., en, d1 : e{n+1}, ..., dm : e{n+m}) inference proceeds as
/// follows.
///
/// If K is a record type schema of the form
/// (K1, ..., Kn, {d1 : K{n+1}, ...., dm : K{n+m}}) then:
///
/// - Each ei is inferred with context type schema Ki to have type Si
/// - Let Ri be the greatest closure of Ki
/// - If Si is a subtype of Ri then let Ti be Si
/// - Otherwise, if Si is dynamic, then we insert an implicit cast on ei to
/// Ri, and let Ti be Ri
/// - Otherwise, if Si is coercible to Ri (via some sequence of call method
/// tearoff or implicit generic instantiation coercions), then we insert the
/// appropriate implicit coercion(s) on ei. Let Ti be the type of the
/// resulting coerced value (which must be a subtype of Ri, possibly proper).
/// - Otherwise, it is a static error.
/// - The type of E is (T1, ..., Tn, {d1 : T{n+1}, ...., dm : T{n+m}})
/// If K is any other type schema:
///
/// - Each ei is inferred with context type schema _ to have type Ti
/// - The type of E is (T1, ..., Tn, {d1 : T{n+1}, ...., dm : T{n+m}})
///
/// @description Checks an implicit downcast for records
/// @author [email protected]

// SharedOptions=--enable-experiment=records

import "../../Utils/expect.dart";
import "../../Utils/static_type_helper.dart";

class Callable {
void call(num x) {}
}

T id<T>(T x) => x;

main() {
var c = Callable();
dynamic d = 3;
(num, double, int Function(int), void Function(num)) r1 = (d, 3, id, c)
..expectStaticType<
Exactly<(num, double, int Function(int), void Function(num))>>();
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's interesting! I think it's a correct expectation that the first positional variable initializer d gets transformed into d as num, and hence the record type has num as its first positional type.

I think this is interesting because it tests the detailed ordering of the effects: If we had instead transformed the initializing expression into (d, 3, id, c) as (num, <and more>) then the expectStaticType would see dynamic as the declared type of the first positional variable of the record literal. So they might have to change some things in the analyzer/CFE in order to make things happen in the specified order.


Expect.throws(() {
dynamic d2 = 3.14;
(int, double, int Function(int), void Function(num)) r2 = (d2, 3, id, c);
});
Expect.throws(() {
(r1.$1 as dynamic).isEven;
});
Expect.throws(() {
(r1.$2 as dynamic)("42");
});
Expect.throws(() {
(r1.$3 as dynamic)("42");
});
}
63 changes: 63 additions & 0 deletions LanguageFeatures/Records/type_inference_A01_t04.dart
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
// Copyright (c) 2022, the Dart project authors. Please see the AUTHORS file
// for details. All rights reserved. Use of this source code is governed by a
// BSD-style license that can be found in the LICENSE file.

/// @assertion Given a type schema K and a record expression E of the general
/// form (e1, ..., en, d1 : e{n+1}, ..., dm : e{n+m}) inference proceeds as
/// follows.
///
/// If K is a record type schema of the form
/// (K1, ..., Kn, {d1 : K{n+1}, ...., dm : K{n+m}}) then:
///
/// - Each ei is inferred with context type schema Ki to have type Si
/// - Let Ri be the greatest closure of Ki
/// - If Si is a subtype of Ri then let Ti be Si
/// - Otherwise, if Si is dynamic, then we insert an implicit cast on ei to
/// Ri, and let Ti be Ri
/// - Otherwise, if Si is coercible to Ri (via some sequence of call method
/// tearoff or implicit generic instantiation coercions), then we insert the
/// appropriate implicit coercion(s) on ei. Let Ti be the type of the
/// resulting coerced value (which must be a subtype of Ri, possibly proper).
/// - Otherwise, it is a static error.
/// - The type of E is (T1, ..., Tn, {d1 : T{n+1}, ...., dm : T{n+m}})
/// If K is any other type schema:
///
/// - Each ei is inferred with context type schema _ to have type Ti
/// - The type of E is (T1, ..., Tn, {d1 : T{n+1}, ...., dm : T{n+m}})
///
/// @description Checks an implicit downcast for records
/// @author [email protected]

// SharedOptions=--enable-experiment=records

import "../../Utils/expect.dart";
import "../../Utils/static_type_helper.dart";

({List<int> list, Map<String, int> map, Set<String> set}) foo() =>
(list: [], map: {}, set: {}) ..expectStaticType<Exactly<
({List<int> list, Map<String, int> map, Set<String> set})>>();

void bar((List<int>, Map<String, int>, Set<String>) r) {
Expect.throws(() {(r.$0 as dynamic).add("");});
Expect.throws(() {(r.$1 as dynamic)[""] = "";});
Expect.throws(() {(r.$1 as dynamic)[42] = 42;});
Expect.throws(() {(r.$2 as dynamic).add(42);});
}

main() {
(List<int>, Map<String, int>, {Set<String> set}) r = ([], {}, set: {})
..expectStaticType<Exactly<
(List<int>, Map<String, int>, {Set<String> set})>>();
Expect.throws(() {(r.$0 as dynamic).add("");});
Expect.throws(() {(r.$1 as dynamic)[""] = "";});
Expect.throws(() {(r.$1 as dynamic)[42] = 42;});
Expect.throws(() {(r.set as dynamic).add(42);});

Expect.throws(() {(foo().list as dynamic).add("");});
Expect.throws(() {(foo().map as dynamic)[""] = "";});
Expect.throws(() {(foo().map as dynamic)[42] = 42;});
Expect.throws(() {(foo().set as dynamic).add(42);});

bar(([], {}, {})
..expectStaticType<Exactly<(List<int>, Map<String, int>, Set<String>)>>());
}
45 changes: 45 additions & 0 deletions LanguageFeatures/Records/type_inference_A01_t05.dart
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
// Copyright (c) 2022, the Dart project authors. Please see the AUTHORS file
// for details. All rights reserved. Use of this source code is governed by a
// BSD-style license that can be found in the LICENSE file.

/// @assertion Given a type schema K and a record expression E of the general
/// form (e1, ..., en, d1 : e{n+1}, ..., dm : e{n+m}) inference proceeds as
/// follows.
///
/// If K is a record type schema of the form
/// (K1, ..., Kn, {d1 : K{n+1}, ...., dm : K{n+m}}) then:
///
/// - Each ei is inferred with context type schema Ki to have type Si
/// - Let Ri be the greatest closure of Ki
/// - If Si is a subtype of Ri then let Ti be Si
/// - Otherwise, if Si is dynamic, then we insert an implicit cast on ei to
/// Ri, and let Ti be Ri
/// - Otherwise, if Si is coercible to Ri (via some sequence of call method
/// tearoff or implicit generic instantiation coercions), then we insert the
/// appropriate implicit coercion(s) on ei. Let Ti be the type of the
/// resulting coerced value (which must be a subtype of Ri, possibly proper).
/// - Otherwise, it is a static error.
/// - The type of E is (T1, ..., Tn, {d1 : T{n+1}, ...., dm : T{n+m}})
/// If K is any other type schema:
///
/// - Each ei is inferred with context type schema _ to have type Ti
/// - The type of E is (T1, ..., Tn, {d1 : T{n+1}, ...., dm : T{n+m}})
///
/// @description Checks type inference for records.
/// @author [email protected]

// SharedOptions=--enable-experiment=records

import "../../Utils/expect.dart";

class C<X> {
Type get typeArgument => X;
}

class D<X extends Y, Y> extends C<Y> {}

main() {
(C<int>, {C<double> x}) r = (D(), x: D());
Expect.equals(int, r.$0.typeArgument);
Expect.equals(double, r.x.typeArgument);
}
25 changes: 22 additions & 3 deletions LanguageFeatures/Records/type_inference_A02_t01.dart
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,28 @@
// for details. All rights reserved. Use of this source code is governed by a
// BSD-style license that can be found in the LICENSE file.

/// @assertion Type inference and promotion flows through records in much the
/// same way it does for instances of generic classes (which are covariant in
/// Dart just like record fields are) and collection literals.
/// @assertion Given a type schema K and a record expression E of the general
/// form (e1, ..., en, d1 : e{n+1}, ..., dm : e{n+m}) inference proceeds as
/// follows.
///
/// If K is a record type schema of the form
/// (K1, ..., Kn, {d1 : K{n+1}, ...., dm : K{n+m}}) then:
///
/// - Each ei is inferred with context type schema Ki to have type Si
/// - Let Ri be the greatest closure of Ki
/// - If Si is a subtype of Ri then let Ti be Si
/// - Otherwise, if Si is dynamic, then we insert an implicit cast on ei to
/// Ri, and let Ti be Ri
/// - Otherwise, if Si is coercible to Ri (via some sequence of call method
/// tearoff or implicit generic instantiation coercions), then we insert the
/// appropriate implicit coercion(s) on ei. Let Ti be the type of the
/// resulting coerced value (which must be a subtype of Ri, possibly proper).
/// - Otherwise, it is a static error.
/// - The type of E is (T1, ..., Tn, {d1 : T{n+1}, ...., dm : T{n+m}})
/// If K is any other type schema:
///
/// - Each ei is inferred with context type schema _ to have type Ti
/// - The type of E is (T1, ..., Tn, {d1 : T{n+1}, ...., dm : T{n+m}})
///
/// @description Checks horizontal inference for records.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think horizontal inference is applicable to record literals (at least, I don't remember hearing anything about it). But it sounds like an interesting additional feature, so it's great that we have it on the table! I'm creating a new language repo issue about this question.

Next, I can see that this test is actually about a situation involving a generic function and an invocation thereof, and the new thing is that some types involved in the associated horizontal inference for that function invocation are record types. Very good, we need that!

As far as I can see, we have the stages {b, c, d} and {a}, and T and U are as stated. So that looks good!

See dart-lang/language#2578 as well, we may need some additional tests (possibly that it doesn't work, if the language and implementation teams think it should not be supported, or that it should wait).

/// @author [email protected]
Expand Down