Skip to content

#2953. Add inference with bounds tests #2957

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 3 commits into from
Nov 11, 2024
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
49 changes: 49 additions & 0 deletions TypeSystem/inference/constraint_solving_A01_t01.dart
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
// Copyright (c) 2024, 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 The constraint solution for a set of type variables
/// `{X0, ..., Xn}` with respect to a constraint set `C` and partial solution
/// `{T0, ..., Tn}`, is defined to be the set of type schemas `{U0, ..., Un}`
/// such that:
/// - If `Ti` is known (that is, does not contain `_`), then `Ui = Ti`. (Note
/// that the upcoming "variance" feature will relax this rule so that it
/// only applies to type variables without an explicitly declared variance.)
/// - Otherwise, let `Vi` be the constraint solution for the type variable
/// `Xi` with respect to the constraint set `C`.
/// - If `Vi` is not known (that is, it contains `_`), then `Ui = Vi`.
/// - Otherwise, if `Xi` does not have an explicit bound, then `Ui = Vi`.
/// - Otherwise, let `Mb <: Xi <: Mt` be the merge of `C` with respect to
/// `Xi`. If `Mb` is not `_`, let `C1` be the constraint set produced by the
/// subtype constraint generation algorithm for `P = Mb`, `Q = B`,
/// `L = {X0, ..., Xn}`. Then `Ui` is the constraint solution for the type
/// variable `Xi` with respect to the constraint set `C + C1`. *Note that
/// `X` is in `L` and that `Mb` doesn't contain any of `X0, ..., Xn`.*
/// - Otherwise, let `Bi` be the bound of `Xi`. Then, let `Bi'` be the type
/// schema formed by substituting type schemas
/// `{U0, ..., Ui-1, Ti, ..., Tn}` in place of the type variables
/// `{X0, ..., Xn}` in `Bi`. (That is, we substitute `Uj` for `Xj` when
/// `j < i` and `Tj` for `Xj` when `j >= i`). Then `Ui` is the constraint
/// solution for the type variable `Xi` with respect to the constraint set
/// `C + (X <: Bi')`.
///
/// @description Checks bounds are taken into account during the inference.
/// @note The case "Otherwise, let `Mb <: Xi <: Mt` be the merge of `C`..." from
/// the above.
/// @author [email protected]

// SharedOptions=--enable-experiment=inference-using-bounds

import '../../Utils/expect.dart';

class A<X extends A<X>> {}
class B extends A<B> {}
class C extends B {}

Type f<X extends A<X>>(X x) => X;

void main() {
Expect.equals(B, f(B()));
Expect.equals(B, f<B>(C()));
Expect.equals(B, f(C()));
}
54 changes: 54 additions & 0 deletions TypeSystem/inference/constraint_solving_A01_t02.dart
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
// Copyright (c) 2024, 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 The constraint solution for a set of type variables
/// `{X0, ..., Xn}` with respect to a constraint set `C` and partial solution
/// `{T0, ..., Tn}`, is defined to be the set of type schemas `{U0, ..., Un}`
/// such that:
/// - If `Ti` is known (that is, does not contain `_`), then `Ui = Ti`. (Note
/// that the upcoming "variance" feature will relax this rule so that it
/// only applies to type variables without an explicitly declared variance.)
/// - Otherwise, let `Vi` be the constraint solution for the type variable
/// `Xi` with respect to the constraint set `C`.
/// - If `Vi` is not known (that is, it contains `_`), then `Ui = Vi`.
/// - Otherwise, if `Xi` does not have an explicit bound, then `Ui = Vi`.
/// - Otherwise, let `Mb <: Xi <: Mt` be the merge of `C` with respect to
/// `Xi`. If `Mb` is not `_`, let `C1` be the constraint set produced by the
/// subtype constraint generation algorithm for `P = Mb`, `Q = B`,
/// `L = {X0, ..., Xn}`. Then `Ui` is the constraint solution for the type
/// variable `Xi` with respect to the constraint set `C + C1`. *Note that
/// `X` is in `L` and that `Mb` doesn't contain any of `X0, ..., Xn`.*
/// - Otherwise, let `Bi` be the bound of `Xi`. Then, let `Bi'` be the type
/// schema formed by substituting type schemas
/// `{U0, ..., Ui-1, Ti, ..., Tn}` in place of the type variables
/// `{X0, ..., Xn}` in `Bi`. (That is, we substitute `Uj` for `Xj` when
/// `j < i` and `Tj` for `Xj` when `j >= i`). Then `Ui` is the constraint
/// solution for the type variable `Xi` with respect to the constraint set
/// `C + (X <: Bi')`.
///
/// @description Checks bounds are taken into account during the inference.
/// @note The case "Otherwise, let `Mb <: Xi <: Mt` be the merge of `C`..." from
/// the above.
/// @author [email protected]

// SharedOptions=--enable-experiment=inference-using-bounds

import '../../Utils/expect.dart';

class A1<X extends A1<X, Y>, Y extends A2<X, Y>> {}
class A2<X extends A1<X, Y>, Y extends A2<X, Y>> {}
class B1 extends A1<B1, B2> {}
class B2 extends A2<B1, B2> {}
class C1 extends B1 {}
class C2 extends B2 {}
class D implements B1, B2 {}

(Type, Type) f<X extends A1<X, Y>, Y extends A2<X, Y>>(X x, Y y) => (X, Y);

void main() {
Expect.equals((B1, B2), f<B1, B2>(B1(), B2()));
Expect.equals((B1, B2), f<B1, B2>(C1(), C2()));
Expect.equals((B1, B2), f(B1(), B2()));
Expect.equals((B1, B2), f(C1(), C2()));
}
46 changes: 46 additions & 0 deletions TypeSystem/inference/constraint_solving_A01_t03.dart
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
// Copyright (c) 2024, 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 The constraint solution for a set of type variables
/// `{X0, ..., Xn}` with respect to a constraint set `C` and partial solution
/// `{T0, ..., Tn}`, is defined to be the set of type schemas `{U0, ..., Un}`
/// such that:
/// - If `Ti` is known (that is, does not contain `_`), then `Ui = Ti`. (Note
/// that the upcoming "variance" feature will relax this rule so that it
/// only applies to type variables without an explicitly declared variance.)
/// - Otherwise, let `Vi` be the constraint solution for the type variable
/// `Xi` with respect to the constraint set `C`.
/// - If `Vi` is not known (that is, it contains `_`), then `Ui = Vi`.
/// - Otherwise, if `Xi` does not have an explicit bound, then `Ui = Vi`.
/// - Otherwise, let `Mb <: Xi <: Mt` be the merge of `C` with respect to
/// `Xi`. If `Mb` is not `_`, let `C1` be the constraint set produced by the
/// subtype constraint generation algorithm for `P = Mb`, `Q = B`,
/// `L = {X0, ..., Xn}`. Then `Ui` is the constraint solution for the type
/// variable `Xi` with respect to the constraint set `C + C1`. *Note that
/// `X` is in `L` and that `Mb` doesn't contain any of `X0, ..., Xn`.*
/// - Otherwise, let `Bi` be the bound of `Xi`. Then, let `Bi'` be the type
/// schema formed by substituting type schemas
/// `{U0, ..., Ui-1, Ti, ..., Tn}` in place of the type variables
/// `{X0, ..., Xn}` in `Bi`. (That is, we substitute `Uj` for `Xj` when
/// `j < i` and `Tj` for `Xj` when `j >= i`). Then `Ui` is the constraint
/// solution for the type variable `Xi` with respect to the constraint set
/// `C + (X <: Bi')`.
///
/// @description Checks bounds are taken into account during the inference.
/// @note The case "Otherwise, let `Mb <: Xi <: Mt` be the merge of `C`..." from
/// the above.
/// @author [email protected]

// SharedOptions=--enable-experiment=inference-using-bounds

import '../../Utils/static_type_helper.dart';

class A<X extends Iterable<Y>, Y> {
A(X x);
}

void main() {
A([1]).expectStaticType<Exactly<A<List<int>, int>>>();
A([1 as num]).expectStaticType<Exactly<A<List<num>, num>>>();
}
45 changes: 45 additions & 0 deletions TypeSystem/inference/constraint_solving_A01_t04.dart
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
// Copyright (c) 2024, 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 The constraint solution for a set of type variables
/// `{X0, ..., Xn}` with respect to a constraint set `C` and partial solution
/// `{T0, ..., Tn}`, is defined to be the set of type schemas `{U0, ..., Un}`
/// such that:
/// - If `Ti` is known (that is, does not contain `_`), then `Ui = Ti`. (Note
/// that the upcoming "variance" feature will relax this rule so that it
/// only applies to type variables without an explicitly declared variance.)
/// - Otherwise, let `Vi` be the constraint solution for the type variable
/// `Xi` with respect to the constraint set `C`.
/// - If `Vi` is not known (that is, it contains `_`), then `Ui = Vi`.
/// - Otherwise, if `Xi` does not have an explicit bound, then `Ui = Vi`.
/// - Otherwise, let `Mb <: Xi <: Mt` be the merge of `C` with respect to
/// `Xi`. If `Mb` is not `_`, let `C1` be the constraint set produced by the
/// subtype constraint generation algorithm for `P = Mb`, `Q = B`,
/// `L = {X0, ..., Xn}`. Then `Ui` is the constraint solution for the type
/// variable `Xi` with respect to the constraint set `C + C1`. *Note that
/// `X` is in `L` and that `Mb` doesn't contain any of `X0, ..., Xn`.*
/// - Otherwise, let `Bi` be the bound of `Xi`. Then, let `Bi'` be the type
/// schema formed by substituting type schemas
/// `{U0, ..., Ui-1, Ti, ..., Tn}` in place of the type variables
/// `{X0, ..., Xn}` in `Bi`. (That is, we substitute `Uj` for `Xj` when
/// `j < i` and `Tj` for `Xj` when `j >= i`). Then `Ui` is the constraint
/// solution for the type variable `Xi` with respect to the constraint set
/// `C + (X <: Bi')`.
///
/// @description Checks bounds are taken into account during the inference.
/// @note The case "Otherwise, let `Mb <: Xi <: Mt` be the merge of `C`..." from
/// the above.
/// @author [email protected]

// SharedOptions=--enable-experiment=inference-using-bounds

import '../../Utils/static_type_helper.dart';

class A<X extends Iterable<Y>, Y extends Iterable<Z>, Z> {
A(X x);
}

void main() {
A([[1]]).expectStaticType<Exactly<A<List<List<int>>, List<int>, int>>>();
}
47 changes: 47 additions & 0 deletions TypeSystem/inference/constraint_solving_A01_t05.dart
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
// Copyright (c) 2024, 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 The constraint solution for a set of type variables
/// `{X0, ..., Xn}` with respect to a constraint set `C` and partial solution
/// `{T0, ..., Tn}`, is defined to be the set of type schemas `{U0, ..., Un}`
/// such that:
/// - If `Ti` is known (that is, does not contain `_`), then `Ui = Ti`. (Note
/// that the upcoming "variance" feature will relax this rule so that it
/// only applies to type variables without an explicitly declared variance.)
/// - Otherwise, let `Vi` be the constraint solution for the type variable
/// `Xi` with respect to the constraint set `C`.
/// - If `Vi` is not known (that is, it contains `_`), then `Ui = Vi`.
/// - Otherwise, if `Xi` does not have an explicit bound, then `Ui = Vi`.
/// - Otherwise, let `Mb <: Xi <: Mt` be the merge of `C` with respect to
/// `Xi`. If `Mb` is not `_`, let `C1` be the constraint set produced by the
/// subtype constraint generation algorithm for `P = Mb`, `Q = B`,
/// `L = {X0, ..., Xn}`. Then `Ui` is the constraint solution for the type
/// variable `Xi` with respect to the constraint set `C + C1`. *Note that
/// `X` is in `L` and that `Mb` doesn't contain any of `X0, ..., Xn`.*
/// - Otherwise, let `Bi` be the bound of `Xi`. Then, let `Bi'` be the type
/// schema formed by substituting type schemas
/// `{U0, ..., Ui-1, Ti, ..., Tn}` in place of the type variables
/// `{X0, ..., Xn}` in `Bi`. (That is, we substitute `Uj` for `Xj` when
/// `j < i` and `Tj` for `Xj` when `j >= i`). Then `Ui` is the constraint
/// solution for the type variable `Xi` with respect to the constraint set
/// `C + (X <: Bi')`.
///
/// @description Checks bounds are taken into account during the inference.
/// @note The case "Otherwise, let `Mb <: Xi <: Mt` be the merge of `C`..." from
/// the above.
/// @author [email protected]

// SharedOptions=--enable-experiment=inference-using-bounds

import 'dart:async';
import '../../Utils/expect.dart';

Type foo<T extends Object>(T? t) => T;

Type bar(FutureOr<Object?> x) => foo(x);

main() {
Expect.equals(Object, bar(42));
Expect.equals(Object, bar(null));
}