Issue #370, instantiate-to-bounds: added static tests for non-function type aliases.
diff --git a/LanguageFeatures/Instantiate-to-bound/class/static/class_l1_t04.dart b/LanguageFeatures/Instantiate-to-bound/class/static/class_l1_t04.dart
index 9ba32bd..e57142f 100644
--- a/LanguageFeatures/Instantiate-to-bound/class/static/class_l1_t04.dart
+++ b/LanguageFeatures/Instantiate-to-bound/class/static/class_l1_t04.dart
@@ -44,7 +44,6 @@
  *   [<U1,m ..., Uk,m>].
  * @description Checks that instantiation to bounds works as expected for
  * [class A<X extends A<X>>], [class B<X extends A<A<X>>>]
- * @compile-error
  * @Issue 34726, 34948
  * @author iarkh@unipro.ru
  */
diff --git a/LanguageFeatures/Instantiate-to-bound/class/static/class_l1_t05.dart b/LanguageFeatures/Instantiate-to-bound/class/static/class_l1_t05.dart
index c18324a..9901ab6 100644
--- a/LanguageFeatures/Instantiate-to-bound/class/static/class_l1_t05.dart
+++ b/LanguageFeatures/Instantiate-to-bound/class/static/class_l1_t05.dart
@@ -44,7 +44,6 @@
  *   [<U1,m ..., Uk,m>].
  * @description Checks that instantiate-to-bounds works as expected for the
  * class [O<X extends M<O<X>>>].
- * @compile-error
  * @author iarkh@unipro.ru
  */
 typedef F<X> = void Function<Y extends X>();
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_FutureOr_l1_t01.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_FutureOr_l1_t01.dart
index 7e14744..333b091 100644
--- a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_FutureOr_l1_t01.dart
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_FutureOr_l1_t01.dart
@@ -1,5 +1,5 @@
 /*
- * Copyright (c) 2018, the Dart project authors.  Please see the AUTHORS file
+ * Copyright (c) 2019, 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.
  */
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_FutureOr_l1_t02.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_FutureOr_l1_t02.dart
index c8a9278..2f38d56 100644
--- a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_FutureOr_l1_t02.dart
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_FutureOr_l1_t02.dart
@@ -1,5 +1,5 @@
 /*
- * Copyright (c) 2018, the Dart project authors.  Please see the AUTHORS file
+ * Copyright (c) 2019, 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.
  */
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_l3_t01.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_l3_t01.dart
index 4d5bd70..889a9ce 100644
--- a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_l3_t01.dart
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_l3_t01.dart
@@ -51,8 +51,7 @@
 import "../../../../Utils/expect.dart";
 
 class A<X, Y, Z> {}
-typedef G<X1 extends X2, X2 extends X3, X3 extends G<X1, X2, X3>> =
-    A<X1, X2, X3>;
+typedef G<X1 extends X2, X2 extends X3, X3 extends G<X1, X2, X3>> = A<X1, X2, X3>;
 
 main() {
   Expect.equals(
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_typedef_l1_t01.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_typedef_l1_t01.dart
index b3d81c3..deb3bad 100644
--- a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_typedef_l1_t01.dart
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_typedef_l1_t01.dart
@@ -53,11 +53,11 @@
 typedef G<X> = X Function();
 class C<X> {}
 
-typedef A<X extends G<C<X>>> = C<X>;
+typedef A<X extends G<A<X>>> = C<X>;
 
 main() {
   Expect.equals(
-    typeOf<A<G<C<dynamic>>>>(),
+    typeOf<A<G<A<dynamic>>>>(),
     typeOf<A>()
   );
 }
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_typedef_l1_t02.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_typedef_l1_t02.dart
index 7c98955..3aba5e0 100644
--- a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_typedef_l1_t02.dart
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/dynamic/nonfunction_typedef_l1_t02.dart
@@ -53,7 +53,7 @@
 typedef G<X> = void Function(X);
 class C<X> {}
 
-typedef A<X extends G<C<X>>> = C<X>;
+typedef A<X extends G<A<X>>> = C<X>;
 
 main() {
   Expect.equals(
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_FutureOr_l1_t01.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_FutureOr_l1_t01.dart
new file mode 100644
index 0000000..b22a9a2
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_FutureOr_l1_t01.dart
@@ -0,0 +1,64 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiate-to-bounds works as expected for [typedef
+ * A<X extends FutureOr<X>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+import "dart:async";
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class C<X> {}
+typedef A<X extends FutureOr<X>> = C<X>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+  F<A<FutureOr<dynamic> >> target = fsource;
+  A();
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_FutureOr_l1_t02.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_FutureOr_l1_t02.dart
new file mode 100644
index 0000000..e28dc8f
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_FutureOr_l1_t02.dart
@@ -0,0 +1,71 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiate-to-bounds works as expected for [A<X
+ * extends FutureOr<A<X>>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+import "dart:async";
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+// Probably does not work here because of the issue 34264
+class C<X> {}
+typedef A<X extends FutureOr<A<X>>> = C<X>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+  F<A<FutureOr<A<dynamic>>>> target = fsource;
+
+  F<A<dynamic>> target1 = fsource;                           //# 01: compile-time error
+  F<A<FutureOr<dynamic>>> target2 = fsource;                 //# 02: compile-time error
+  F<A<FutureOr<A<FutureOr<dynamic>>>>> target3 = fsource;    //# 03: compile-time error
+  F<A<FutureOr<A<FutureOr<A<dynamic>>>>>> target4 = fsource; //# 04: compile-time error
+
+  A(); //# 05: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l1_t01.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l1_t01.dart
new file mode 100644
index 0000000..87c8a16
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l1_t01.dart
@@ -0,0 +1,68 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiate-to-bounds works as expected for
+ * [typedef A<X extends A<X>>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class C<X> {}
+typedef A<X extends A<X>> = C<X>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+  F<A<A<dynamic>>> target = fsource;
+
+  F<A<dynamic>> target1 = fsource;             //# 01: compile-time error
+  F<A<A<A<dynamic>>>> target2 = fsource;       //# 02: compile-time error
+  F<A<A<A<A<dynamic>>>>> target3 = fsource;    //# 03: compile-time error
+  F<A<A<A<A<A<dynamic>>>>>> target4 = fsource; //# 04: compile-time error
+
+  A();  //# 05: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l1_t02.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l1_t02.dart
new file mode 100644
index 0000000..5013beb
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l1_t02.dart
@@ -0,0 +1,74 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiation to bounds works OK for [typedef A<X
+ * extends A<A<X>>>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class C<X> {}
+typedef A<X extends A<A<X>>> = C<X>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+
+  F<A<A<A<dynamic>>>> target = fsource;
+
+  F<A<dynamic>> target1 = fsource;             //# 01: compile-time error
+  F<A<A<dynamic>>> target2 = fsource;          //# 02: compile-time error
+  F<A<A<A<A<dynamic>>>>> target3 = fsource;    //# 03: compile-time error
+  F<A<A<A<A<A<dynamic>>>>>> target4 = fsource; //# 04: compile-time error
+
+  F<A<Null>> target5 = fsource;             //# 05: compile-time error
+  F<A<A<Null>>> target6 = fsource;          //# 06: compile-time error
+  F<A<A<A<A<Null>>>>> target7 = fsource;    //# 07: compile-time error
+  F<A<A<A<A<A<Null>>>>>> target8 = fsource; //# 08: compile-time error
+
+  A(); //# 09: compile-time error
+}
\ No newline at end of file
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l1_t03.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l1_t03.dart
new file mode 100644
index 0000000..92980d7
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l1_t03.dart
@@ -0,0 +1,75 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiation to bounds works as expected for
+ * [class A<X extends A<X>>], [class B<X extends A<X>>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class A<X extends A<X>> {}
+typedef B<X extends A<X>> = A<X>;
+
+main() {
+  B source;
+  var fsource = toF(source);
+
+  F<B<A<dynamic>>> target = fsource;
+
+  F<B<dynamic>> target1 = fsource;             //# 01: compile-time error
+  F<B<A<A<dynamic>>>> target2 = fsource;       //# 02: compile-time error
+  F<B<A<A<A<dynamic>>>>> target3 = fsource;    //# 03: compile-time error
+  F<B<A<A<A<A<dynamic>>>>>> target4 = fsource; //# 04: compile-time error
+
+  F<B<Null>> target5 = fsource;             //# 05: compile-time error
+  F<B<A<Null>>> target6 = fsource;          //# 06: compile-time error
+  F<B<A<A<Null>>>> target7 = fsource;       //# 07: compile-time error
+  F<B<A<A<A<Null>>>>> target8 = fsource;    //# 08: compile-time error
+  F<B<A<A<A<A<Null>>>>>> target9 = fsource; //# 09: compile-time error
+
+  B(); //# 10: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l1_t04.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l1_t04.dart
new file mode 100644
index 0000000..633fbe1
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l1_t04.dart
@@ -0,0 +1,75 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiation to bounds works as expected for
+ * [class A<X extends A<X>>], [class B<X extends A<A<X>>>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class A<X extends A<X>> {}
+typedef B<X extends A<A<X>>> = A<X>;
+
+main() {
+  B source;
+  var fsource = toF(source);
+
+  F<B<A<A<dynamic>>>> target = fsource;
+
+  F<B<dynamic>> target1 = fsource;             //# 01: compile-time error
+  F<B<A<dynamic>>> target2 = fsource;          //# 02: compile-time error
+  F<B<A<A<A<dynamic>>>>> target3 = fsource;    //# 03: compile-time error
+  F<B<A<A<A<A<dynamic>>>>>> target4 = fsource; //# 04: compile-time error
+
+  F<B<Null>> target5 = fsource;             //# 05: compile-time error
+  F<B<A<Null>>> target6 = fsource;          //# 06: compile-time error
+  F<B<A<A<Null>>>> target7 = fsource;       //# 07: compile-time error
+  F<B<A<A<A<Null>>>>> target8 = fsource;    //# 08: compile-time error
+  F<B<A<A<A<A<Null>>>>>> target9 = fsource; //# 09: compile-time error
+
+  B(); //# 10: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l1_t05.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l1_t05.dart
new file mode 100644
index 0000000..a751dfb
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l1_t05.dart
@@ -0,0 +1,75 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiate-to-bounds works as expected for the
+ * class [O<X extends M<O<X>>>].
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class M<X> {}
+typedef O<X extends M<O<X>>> = M<O<X>>;
+
+main() {
+  O source;
+  var fsource = toF(source);
+
+  F<O<M<O<dynamic>>>> target = fsource;
+
+  F<O<dynamic>> target1 = fsource;             //# 01: compile-time error
+  F<O<M<dynamic>>> target2 = fsource;          //# 02: compile-time error
+  F<O<M<O<M<dynamic>>>>> target3 = fsource;    //# 03: compile-time error
+  F<O<M<O<M<O<dynamic>>>>>> target4 = fsource; //# 04: compile-time error
+
+  F<O<Null>> target5 = fsource;             //# 05: compile-time error
+  F<O<M<Null>>> target6 = fsource;          //# 06: compile-time error
+  F<O<M<O<Null>>>> target7 = fsource;       //# 07: compile-time error
+  F<O<M<O<M<Null>>>>> target8 = fsource;    //# 08: compile-time error
+  F<O<M<O<M<O<Null>>>>>> target9 = fsource; //# 09: compile-time error
+
+  O(); //# 10: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l1_t06.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l1_t06.dart
new file mode 100644
index 0000000..0c38aec
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l1_t06.dart
@@ -0,0 +1,79 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiate-to-bounds works as expected for [typedef
+ * O<X extends M<O<M<O<M<O<X>>>>>>>].
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class M<X> {}
+typedef O<X extends M<O<M<O<M<O<X>>>>>>> = M<O<X>>;
+
+main() {
+  O source;
+  var fsource = toF(source);
+
+  F<O<M<O<M<O<M<O<dynamic>>>>>>>> target = fsource;
+
+  F<O<dynamic>> target1 = fsource;                //# 01: compile-time error
+  F<O<M<dynamic>>> target2 = fsource;             //# 02: compile-time error
+  F<O<M<O<M<dynamic>>>>> target3 = fsource;       //# 03: compile-time error
+  F<O<M<O<M<O<dynamic>>>>>> target4 = fsource;    //# 04: compile-time error
+  F<O<M<O<M<O<M<dynamic>>>>>>> target5 = fsource; //# 05: compile-time error
+
+  F<O<M<O<M<O<M<O<M<dynamic>>>>>>>>> target6 = fsource;    //# 06: compile-time error
+  F<O<M<O<M<O<M<O<M<O<dynamic>>>>>>>>>> target7 = fsource; //# 07: compile-time error
+
+  F<O<Null>> target8 = fsource;              //# 08: compile-time error
+  F<O<M<Null>>> target9  = fsource;          //# 09: compile-time error
+  F<O<M<O<Null>>>> target10 = fsource;       //# 10: compile-time error
+  F<O<M<O<M<Null>>>>> target11 = fsource;    //# 11: compile-time error
+  F<O<M<O<M<O<Null>>>>>> target12 = fsource; //# 12: compile-time error
+
+  O(); //# 13: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t01.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t01.dart
new file mode 100644
index 0000000..463b8b8
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t01.dart
@@ -0,0 +1,67 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiate-to-bounds works as expected for [typedef
+ * A<X1 extends X2, X2 extends A<X1, X2>>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class C<X1, X2> {}
+typedef A<X1 extends X2, X2 extends A<X1, X2>> = C<X1, X2>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+
+  F<A<dynamic, A<dynamic, dynamic>>> target = fsource;
+
+  F<A<dynamic, dynamic>> target1 = fsource;                         //# 01: compile-time error
+  F<A<A<dynamic, dynamic>, A<dynamic, dynamic>>> target2 = fsource; //# 02: compile-time error
+
+  A(); //# 03: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t02.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t02.dart
new file mode 100644
index 0000000..324fe2e
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t02.dart
@@ -0,0 +1,67 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiate-to-bounds works as expected for [typedef
+ * [A<X1 extends A<X1, X2>, X2 extends X1>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class C<X1, X2> {}
+typedef A<X1 extends A<X1, X2>, X2 extends X1> = C<X1, X2>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+
+  F<A<A<dynamic, dynamic>, dynamic>> target = fsource;
+
+  F<A<dynamic, dynamic>> target1 = fsource;             //# 01: compile-time error
+  F<A<dynamic, A<dynamic, dynamic>>> target2 = fsource; //# 02: compile-time error
+
+  A(); //# 03: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t03.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t03.dart
new file mode 100644
index 0000000..b8ba61e
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t03.dart
@@ -0,0 +1,67 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiate-to-bounds works as expected for [typedef
+ * A<String, X extends A<Null, A<String,X>>>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class C<X1, X2> {}
+typedef A<Y extends String, X extends A<Null, A<String, X>>> = C<Y, X>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+
+  F<A<String, A<Null, A<String, dynamic>>>> target = fsource;
+
+  F<A<dynamic, dynamic>> target1 = fsource;                         //# 01: compile-time error
+  F<A<dynamic, A<dynamic, A<dynamic, dynamic>>>> target2 = fsource; //# 02: compile-time error
+
+  A(); //# 03: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t04.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t04.dart
new file mode 100644
index 0000000..382d8b9
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t04.dart
@@ -0,0 +1,67 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiate-to-bounds works as expected for [typedef
+ * A<String, X extends A<void, A<String,X>>>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class C<X, Y> {}
+typedef A<Y extends String, X extends A<void, A<String, X>>> = C<Y, X>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+
+  F<A<String, A<void, A<String, dynamic>>>> target = fsource;
+
+  F<A<dynamic, dynamic>> target1 = fsource;                         //# 01: compile-time error
+  F<A<dynamic, A<dynamic, A<dynamic, dynamic>>>> target2 = fsource; //# 02: compile-time error
+
+  A(); //# 03: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t05.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t05.dart
new file mode 100644
index 0000000..d0fcd6f
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t05.dart
@@ -0,0 +1,69 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiate-to-bounds works as expected for [typedef
+ * A<X1 extends X2, X2 extends A<X1, X2>>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class B<X extends B<X, Y>, Y> {}
+typedef A<X1 extends B<X1, X2>, X2 extends X1> = B<X1, X2>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+
+  F<A<B<dynamic, dynamic>, B<dynamic, dynamic>>> target = fsource;
+
+  F<A<dynamic, dynamic>> target1 = fsource;                                                 //# 01: compile-time error
+  F<A<B<dynamic, dynamic>, dynamic>> target2 = fsource;                                     //# 02: compile-time error
+  F<A<dynamic, B<dynamic, dynamic>>> target3 = fsource;                                     //# 03: compile-time error
+  F<A<B<B<dynamic, dynamic>, B<dynamic, dynamic>>, B<dynamic, dynamic>>> target4 = fsource; //# 04: compile-time error
+
+  A();                                                                                      //# 05: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t06.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t06.dart
new file mode 100644
index 0000000..7a206e8
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t06.dart
@@ -0,0 +1,68 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiate-to-bounds works as expected for [class
+ * B<X extends B<X>>], [class A<X1 extends B<X1>, X2>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class B<X extends B<X, Y>, Y> {}
+typedef A<X1 extends B<X1, X2>, X2> = B<X1, X2>;
+
+
+main() {
+  A source;
+  var fsource = toF(source);
+
+  F<A<B<dynamic, dynamic>, dynamic>> target = fsource;
+
+  F<A<dynamic, dynamic>> target1 = fsource;                                     //# 01: compile-time error
+  F<A<B<B<dynamic, dynamic>, B<dynamic, dynamic>>, dynamic>> target2 = fsource; //# 02: compile-time error
+
+  A();                                                                          //# 03: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t07.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t07.dart
new file mode 100644
index 0000000..d57ba36
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t07.dart
@@ -0,0 +1,67 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiate-to-bounds works as expected for [class
+ * B<X extends B<X, Y>, Y>], [typedef A<X1, X2 extends B<X2, X1>>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class B<X extends B<X, Y>, Y> {}
+typedef A<X1, X2 extends B<X2, X1>> = B<X1, X2>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+
+  F<A<dynamic, B<dynamic, dynamic>>> target = fsource;
+
+  F<A<dynamic, dynamic>> target1 = fsource;                                     //# 01: compile-time error
+  F<A<dynamic, B<B<dynamic, dynamic>, B<dynamic, dynamic>>>> target2 = fsource; //# 02: compile-time error
+
+  A();                                                                          //# 03: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t08.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t08.dart
new file mode 100644
index 0000000..794f678
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t08.dart
@@ -0,0 +1,68 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiate-to-bounds works as expected for [typedef
+ * B<X extends B<X, Y>, Y>], [typedef A<X1 extends X2, X2 extends B<X1, X2>>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class B<X extends B<X, Y>, Y> {}
+typedef A<X1 extends X2, X2 extends B<X1, X2>> = B<X1, X2>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+
+  F<A<B<dynamic, dynamic>, B<dynamic, dynamic>>> target = fsource;
+
+//  F<A<dynamic, dynamic>> target1 = fsource;    //# 01: compile-time error
+//  F<A<dynamic, B<dynamic>>> target2 = fsource; //# 02: compile-time error
+//  F<A<B<dynamic>, dynamic>> target3 = fsource; //# 03: compile-time error
+
+//  A();  //# 04: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t09.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t09.dart
new file mode 100644
index 0000000..d79207d
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t09.dart
@@ -0,0 +1,70 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiate-to-bounds works as expected for [class
+ * B<X extends B<X>>], [class C<X, Y>], [typedef A<X1 extends B<X2>, X2 extends
+ * B<X2>>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class B<X extends B<X>> {}
+class C<X, Y> {}
+typedef A<X1 extends B<X2>, X2 extends B<X2>> = C<X1, X2>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+
+  F<A<B<B<dynamic>>, B<dynamic>>> target = fsource;
+
+  F<A<dynamic, dynamic>> target1 = fsource;    //# 01: compile-time error
+  F<A<dynamic, B<dynamic>>> target2 = fsource; //# 02: compile-time error
+  F<A<B<dynamic>, dynamic>> target3 = fsource; //# 03: compile-time error
+
+  A();                                         //# 04: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t10.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t10.dart
new file mode 100644
index 0000000..f0b600b
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l2_t10.dart
@@ -0,0 +1,65 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiate-to-bounds works as expected for [typedef
+ * A<X1 extends A<X1, X2>, X2 extends A<X1, X2>>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class B<X, Y> {}
+typedef A<X1 extends A<X1, X2>, X2 extends A<X1, X2>> = B<X1, X2>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+
+  F<A<A<dynamic, dynamic>, A<dynamic, dynamic>>> target = fsource;
+
+  F<A<dynamic, dynamic>> target1 = fsource; //# 01: compile-time error
+  A();                                      //# 02: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l3_t01.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l3_t01.dart
new file mode 100644
index 0000000..dd214c2
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l3_t01.dart
@@ -0,0 +1,67 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiate-to-bounds works as expected for [typedef
+ * G<X1 extends X2, X2 extends X3, X3 extends G<X1, X2, X3>>]
+ *  extends X2, X2 extends A<X1, X2>>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class A<X, Y, Z> {}
+typedef G<X1 extends X2, X2 extends X3, X3 extends G<X1, X2, X3>> = A<X1, X2, X3>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+
+  F<A<dynamic, dynamic, A<dynamic, dynamic, dynamic>>> target = fsource;
+
+  F<A<dynamic, dynamic, dynamic>> target1 = fsource;  //# 01: compile-time error
+
+  A();                                                //# 02: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l4_t01.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l4_t01.dart
new file mode 100644
index 0000000..8798e602
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_l4_t01.dart
@@ -0,0 +1,73 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiate-to-bounds works as expected for [typedef
+ * G<X1 extends A<X1>, X2 extends A<X1>, X3 extends B, X4 extends X2>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class A<X> {}
+class B<X> extends A<X> {}
+class C<X1, X2, X3, X4> {}
+
+typedef G<X1 extends A<X1>, X2 extends A<X1>, X3 extends B, X4 extends X2> =
+    C<X1, X2, X3, X4>;
+
+main() {
+  G source;
+
+  var fsource = toF(source);
+
+  F<G<A<dynamic>, A<A<dynamic>>, B<dynamic>, A<A<dynamic>>>> target = fsource;
+
+  F<G<dynamic, A<A<dynamic>>, B<dynamic>, A<A<dynamic>>>> target1 = fsource; //# 01: compile-time error
+  F<G<A<dynamic>, A<dynamic>, B<dynamic>, A<dynamic>>> target2 = fsource;    //# 02: compile-time error
+  F<G<A<dynamic>, A<A<dynamic>>, B<dynamic>, A<dynamic>>> target3 = fsource; //# 03: compile-time error
+
+  G();                                                                       //# 04: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l1_t01.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l1_t01.dart
new file mode 100644
index 0000000..854e307
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l1_t01.dart
@@ -0,0 +1,77 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiation to bounds works OK for the class with
+ * [typedef G<X> = X Function()] parameter (covariant)
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+typedef G<X> = X Function();
+class C<X> {}
+
+typedef A<X extends G<A<X>>> = C<X>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+  F<A<G<A<dynamic>>>> target = fsource;
+
+  F<A<G<A<Null>>>> target0 = fsource;          //# 01: compile-time error
+
+  F<A<dynamic>> target1 = fsource;             //# 02: compile-time error
+  F<A<G<dynamic>>> target2 = fsource;          //# 03: compile-time error
+  F<A<G<A<G<dynamic>>>>> target3 = fsource;    //# 04: compile-time error
+  F<A<G<A<G<A<dynamic>>>>>> target4 = fsource; //# 05: compile-time error
+
+  F<A<Null>> target5 = fsource;                //# 06: compile-time error
+  F<A<G<Null>>> target6 = fsource;             //# 07: compile-time error
+  F<A<G<A<G<Null>>>>> target7 = fsource;       //# 08: compile-time error
+  F<A<G<A<G<A<Null>>>>>> target8 = fsource;    //# 09: compile-time error
+
+  A();                                         //# 10: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l1_t02.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l1_t02.dart
new file mode 100644
index 0000000..3d87c2e
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l1_t02.dart
@@ -0,0 +1,75 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiation to bounds works OK for the class with
+ * [typedef G<X> = Function(X)] parameter (contravariant)
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+typedef G<X> = void Function(X);
+class C<X> {}
+
+typedef A<X extends G<A<X>>> = C<X>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+  F<A<G<C<Null>>>> target = fsource;
+
+  F<A<dynamic>> target1 = fsource;             //# 01: compile-time error
+  F<A<G<dynamic>>> target2 = fsource;          //# 02: compile-time error
+  F<A<G<C<G<dynamic>>>>> target3 = fsource;    //# 03: compile-time error
+  F<A<G<C<G<A<dynamic>>>>>> target4 = fsource; //# 04: compile-time error
+
+  F<A<Null>> target5 = fsource;                //# 05: compile-time error
+  F<A<G<Null>>> target6 = fsource;             //# 06: compile-time error
+  F<A<G<A<G<Null>>>>> target7 = fsource;       //# 07: compile-time error
+  F<A<G<A<G<A<Null>>>>>> target8 = fsource;    //# 08: compile-time error
+
+  A();                                         //# 09: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l1_t03.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l1_t03.dart
new file mode 100644
index 0000000..1be837d
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l1_t03.dart
@@ -0,0 +1,58 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiation to bounds works OK for [typedef G<X> =
+ * X Function(X)], [class C<X>], [typedef A<X extends G<A<X>>>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef G<X> = X Function(X);
+class C<X> {}
+typedef A<X extends G<A<X>>> = C<X>;
+
+main() {
+  A source; //# 01: compile-time error
+  A();      //# 02: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l1_t04.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l1_t04.dart
new file mode 100644
index 0000000..4de478e
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l1_t04.dart
@@ -0,0 +1,77 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiation to bounds works OK for the class with
+ * [typedef G<X> = X Function()] parameter (contravariant)
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+typedef G<X> = void Function();
+class C<X> {}
+
+typedef A<X extends G<C<X>>> = C<X>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+  F<A<G<A<dynamic>>>> target = fsource;
+
+  F<A<G<A<Null>>>> target0 = fsource;
+
+  F<A<dynamic>> target1 = fsource;          //# 01: compile-time error
+  F<A<G<dynamic>>> target2 = fsource;
+  F<A<G<A<G<dynamic>>>>> target3 = fsource;
+  F<A<G<A<G<A<dynamic>>>>>> target4 = fsource;
+
+  F<A<Null>> target5 = fsource;             //# 02: compile-time error
+  F<A<G<Null>>> target6 = fsource;
+  F<A<G<A<G<Null>>>>> target7 = fsource;
+  F<A<G<A<G<A<Null>>>>>> target8 = fsource;
+
+  A();
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t01.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t01.dart
new file mode 100644
index 0000000..3cea9ee
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t01.dart
@@ -0,0 +1,68 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiation to bounds works OK for [typedef G<X> =
+ * X Function()], [typedef A<X extends G<A<X, Y>>, Y extends X>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+typedef G<X> = X Function();
+class C<X, Y> {}
+typedef A<X extends G<C<X, Y>>, Y extends X> = C<X, Y>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+  F<A<G<A<dynamic, dynamic>>, dynamic>> target = fsource;
+
+  F<A<dynamic, dynamic>> target1 = fsource;                   //# 01: compile-time error
+  F<A<G<dynamic>, dynamic>> target2 = fsource;                //# 02: compile-time error
+  F<A<G<A<G<dynamic>, dynamic>>, dynamic>> target3 = fsource; //# 03: compile-time error
+
+  A();                                                        //# 04: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t02.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t02.dart
new file mode 100644
index 0000000..4b423cc
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t02.dart
@@ -0,0 +1,85 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiation to bounds works OK for [typedef G<X> =
+ * Function(X)], [class A<X extends G<A<X, Y>>, Y extends X>]
+ *
+ * In the test we have [G] with one type argument which is contravariant, so the
+ * meaning of the raw [A] is [A<G<A<Null, Null>>, dynamic>], obtained as
+ * follows:
+ *
+ * X                  Y
+ * ----------------------------------
+ * G<A<X, Y>>         X             // Initial values.
+ * G<A<Null, Null>>   dynamic       // Break SCC {X, Y}.
+ *
+ * The resulting type is well-bounded, because it is super-bounded, because
+ * [dynamic <: G<...>] fails, but [A<G<A<Object, Object>>, Null>] is
+ * regular-bounded, because [Null <: ...` and `G<A<Object, Object>> <:
+ * G<A<..., ...>>].
+ * This also shows that the instance creation at the end is a compile-time
+ * error.
+ *
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+typedef G<X> = Function(X);
+class C<X, Y> {}
+typedef A<X extends G<C<X,Y>>, Y extends X> = C<X, Y>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+  F<A<G<A<Null, Null>>, dynamic>> target = fsource;
+
+  F<A<dynamic, dynamic>> target1 = fsource;                   //# 01: compile-time error
+  F<A<G<dynamic>, dynamic>> target2 = fsource;                //# 02: compile-time error
+  F<A<G<A<G<dynamic>, dynamic>>, dynamic>> target3 = fsource; //# 03: compile-time error
+
+  A();                                                        //# 04: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t03.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t03.dart
new file mode 100644
index 0000000..4d15484
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t03.dart
@@ -0,0 +1,61 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiation to bounds works OK for [typedef G<X> =
+ * X Function(X)], [typedef A<X extends G<A<X, Y>>, Y extends X>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class C<X, Y> {}
+typedef G<X> = X Function(X);
+typedef A<X extends G<A<X, Y>>, Y extends X> = C<X, Y>;
+
+main() {
+  A source;  //# 01: compile-time error
+  A();       //# 02: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t04.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t04.dart
new file mode 100644
index 0000000..816267c
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t04.dart
@@ -0,0 +1,68 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiation to bounds works OK for [typedef G<X> =
+ * void Function()], [typedef A<X extends G<C<X,Y>>, Y extends X>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class C<X, Y> {}
+typedef G<X> = void Function();
+typedef A<X extends G<C<X,Y>>, Y extends X> = C<X, Y>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+  F<A<G<A<dynamic, dynamic>>, dynamic>> target = fsource;
+
+  F<A<dynamic, dynamic>> target1 = fsource;           //# 01: compile-time error
+  F<A<G<dynamic>, dynamic>> target2 = fsource;
+  F<A<G<A<G<dynamic>, dynamic>>, dynamic>> target3 = fsource;
+
+  A();
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t05.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t05.dart
new file mode 100644
index 0000000..63a4d25
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t05.dart
@@ -0,0 +1,70 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiation to bounds works OK for [typedef G<X> =
+ * X Function()], [typedef A<X extends G<A<Y, X>>, Y extends G<A<X, Y>>>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class C<X, Y> {}
+typedef G<X> = X Function();
+typedef A<X extends G<C<Y, X>>, Y extends G<C<X, Y>>> = C<X, Y>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+  F<A<G<A<dynamic, dynamic>>, G<A<dynamic, dynamic>>>> target = fsource;
+
+  F<A<dynamic, G<A<dynamic, dynamic>>>> target1 = fsource;                   //# 01: compile-time error
+  F<A<G<dynamic>, G<A<dynamic, dynamic>>>> target2 = fsource;                //# 02: compile-time error
+  F<A<G<A<G<dynamic>, dynamic>>, G<A<dynamic, dynamic>>>> target3 = fsource; //# 03: compile-time error
+  F<A<G<A<dynamic, dynamic>>, dynamic>> target4 = fsource;                   //# 04: compile-time error
+  F<A<G<A<dynamic, dynamic>>, G<dynamic>>> target5 = fsource;                //# 05: compile-time error
+
+  A();  //# 06: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t06.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t06.dart
new file mode 100644
index 0000000..4b8400c
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t06.dart
@@ -0,0 +1,72 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiation to bounds works OK for [typedef G<X> =
+ * Function(X)], [class A<X extends G<A<Y, X>>, Y extends G<A<X, Y>>>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class C<X, Y> {}
+typedef G<X> = Function(X);
+typedef A<X extends G<C<Y, X>>, Y extends G<C<X, Y>>> = C<X, Y>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+  F<A<G<A<Null, Null>>, G<A<Null, Null>>>> target = fsource;
+
+
+  F<A<G<A<dynamic, dynamic>>, G<A<dynamic, dynamic>>>> target1 = fsource;    //# 01: compile-time error
+  F<A<dynamic, G<A<dynamic, dynamic>>>> target2 = fsource;                   //# 02: compile-time error
+  F<A<G<dynamic>, G<A<dynamic, dynamic>>>> target3 = fsource;                //# 03: compile-time error
+  F<A<G<A<G<dynamic>, dynamic>>, G<A<dynamic, dynamic>>>> target4 = fsource; //# 04: compile-time error
+  F<A<G<A<dynamic, dynamic>>, dynamic>> target5 = fsource;                   //# 05: compile-time error
+  F<A<G<A<dynamic, dynamic>>, G<dynamic>>> target6 = fsource;                //# 06: compile-time error
+
+  A();                                                                       //# 07: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t07.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t07.dart
new file mode 100644
index 0000000..e8d1bfa
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t07.dart
@@ -0,0 +1,61 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiation to bounds works OK for [typedef G<X> =
+ * X Function()], [class A<X extends G<A<Y, X>>, Y extends G<A<X, Y>>>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class C<X, Y> {}
+typedef G<X> = X Function(X);
+typedef A<X extends G<A<Y, X>>, Y extends G<A<X, Y>>> = C<X, Y>;
+
+main() {
+  A source; //# 01: compile-time error
+  A();      //# 02: compile-time error
+}
diff --git a/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t08.dart b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t08.dart
new file mode 100644
index 0000000..a2824c0
--- /dev/null
+++ b/LanguageFeatures/Instantiate-to-bound/nonfunction_typedef/static/nonfunction_typedef_l2_t08.dart
@@ -0,0 +1,70 @@
+/*
+ * Copyright (c) 2019, 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 Instantiate to bound then computes an actual type argument list
+ * for [G] as follows:
+ *
+ *   Let [Ui],[1] be [Si], for all [i] in [1 .. k]. (This is the "current value"
+ *   of the bound for type variable [i], at step [1]; in general we will
+ *   consider the current step, [m], and use data for that step, e.g., the bound
+ *   [Ui],[m], to compute the data for step [m + 1]).
+ *
+ *   Let [-->m] be a relation among the type variables [X1 .. Xk] such that
+ *   [Xp -->m Xq] iff [Xq] occurs in [Up],[m] (so each type variable is related
+ *   to, that is, depends on, every type variable in its bound, possibly
+ *   including itself). Let [==>m] be the transitive closure of [-->m]. For each
+ *   [m], let [Ui],[m+1], for [i] in [1 .. k], be determined by the following
+ *   iterative process:
+ *
+ *   1. If there exists a [j] in [1 .. k] such that [Xj ==>m X0j] (that is, if
+ *   the dependency graph has a cycle) let [M1 .. Mp] be the strongly connected
+ *   components (SCCs) with respect to [-->m] (that is, the maximal subsets of
+ *   [X1 .. Xk] where every pair of variables in each subset are related in both
+ *   directions by [==>m]; note that the SCCs are pairwise disjoint; also, they
+ *   are uniquely defined up to reordering, and the order does not matter). Let
+ *   [M] be the union of [M1 .. Mp] (that is, all variables that participate in
+ *   a dependency cycle). Let [i] be in [1 .. k]. If [Xi] does not belong to [M]
+ *   then [Ui,m+1 = Ui,m]. Otherwise there exists a [q] such that [Xi] belongs
+ *   to [Mq]; [Ui,m+1] is then obtained from [Ui,m] by replacing every covariant
+ *   occurrence of a variable in [Mq] by [dynamic], and replacing every
+ *   contravariant occurrence of a variable in [Mq] by [Null].
+ *
+ *   2. Otherwise, (if no dependency cycle exists) let [j] be the lowest number
+ *   such that [Xj] occurs in [Up,m] for some [p] and [Xj -/->m Xq] for all [q]
+ *   in [1..k] (that is, [Uj,m] is closed, that is, the current bound of [Xj]
+ *   does not contain any type variables; but [Xj] is being depended on by the
+ *   bound of some other type variable). Then, for all [i] in [1 .. k], [Ui,m+1]
+ *   is obtained from [Ui,m] by replacing every covariant occurrence of [Xj] by
+ *   [Uj,m], and replacing every contravariant occurrence of [Xj] by [Null].
+ *
+ *   3. Otherwise, (when no dependencies exist) terminate with the result
+ *   [<U1,m ..., Uk,m>].
+ * @description Checks that instantiation to bounds works OK for [typedef G<X> =
+ * void Function()], [typedef A<X extends G<A<Y, X>>, Y extends G<A<X, Y>>>]
+ * @author iarkh@unipro.ru
+ */
+// SharedOptions=--enable-experiment=nonfunction-type-aliases
+
+typedef F<X> = void Function<Y extends X>();
+F<X> toF<X>(X x) => null;
+
+class C<X, Y> {}
+typedef G<X> = void Function();
+typedef A<X extends G<C<Y, X>>, Y extends G<C<X, Y>>> = C<X, Y>;
+
+main() {
+  A source;
+  var fsource = toF(source);
+  F<A<G<A<dynamic, dynamic>>, G<A<dynamic, dynamic>>>> target = fsource;
+
+  F<A<dynamic, G<A<dynamic, dynamic>>>> target1 = fsource;                   //# 01: compile-time error
+  F<A<G<dynamic>, G<A<dynamic, dynamic>>>> target2 = fsource;
+  F<A<G<A<G<dynamic>, dynamic>>, G<A<dynamic, dynamic>>>> target3 = fsource;
+  F<A<G<A<dynamic, dynamic>>, dynamic>> target4 = fsource;                   //# 02: compile-time error
+  F<A<G<A<dynamic, dynamic>>, G<dynamic>>> target5 = fsource;
+
+  A();
+}