Fixes #2099. Add subtyping tests for function type with required named arguments

LanguageFeatures/Subtyping/dynamic/generated/named_function_types_arguments_binding_A01_t01.dart

@@ -3,17 +3,22 @@
 // BSD-style license that can be found in the LICENSE file.
 
 /// @assertion A type T0 is a subtype of a type T1 (written T0 <: T1) when:
-/// Named Function Types: T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>
-///   (T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})
-///
-/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ..., Sn yn,
-/// {Sn+1 yn+1, ..., Sq yq})
-/// and {yn+1, ..., yq} subset of {xn+1, ..., xm}
+/// Named Function Types:
+/// T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>(V0 x0, ..., Vn xn,
+///   {r0n+1 Vn+1 xn+1, ..., r0m Vm xm}) where r0j is empty or required for j in
+///   n+1...m
+/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ...,
+///   Sn yn, {r1n+1 Sn+1 yn+1, ..., r1q Sq yq}) where r1j is empty or required
+///   for j in n+1...q
+/// and {yn+1, ... , yq} subsetof {xn+1, ... , xm}
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Vi[Z0/X0, ..., Zk/Xk] for i in 0...n
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Tj[Z0/X0, ..., Zk/Xk] for i in n+1...q, yj = xi
+/// and for each j such that r0j is required, then there exists an i in n+1...q
+///   such that xj = yi, and r1i is required
 /// and U0[Z0/X0, ..., Zk/Xk] <: U1[Z0/Y0, ..., Zk/Yk]
 /// and B0i[Z0/X0, ..., Zk/Xk] === B1i[Z0/Y0, ..., Zk/Yk] for i in 0...k
 /// where the Zi are fresh type variables with bounds B0i[Z0/X0, ..., Zk/Xk]
+///
 /// @description Check that if T0 and T1 satisfies the rules above, then T0 is
 /// subtype of T1
 /// @author sgrekhov@unipro.ru

LanguageFeatures/Subtyping/dynamic/generated/named_function_types_arguments_binding_A01_t02.dart

@@ -3,17 +3,22 @@
 // BSD-style license that can be found in the LICENSE file.
 
 /// @assertion A type T0 is a subtype of a type T1 (written T0 <: T1) when:
-/// Named Function Types: T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>
-///   (T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})
-///
-/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ..., Sn yn,
-/// {Sn+1 yn+1, ..., Sq yq})
-/// and {yn+1, ..., yq} subset of {xn+1, ..., xm}
+/// Named Function Types:
+/// T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>(V0 x0, ..., Vn xn,
+///   {r0n+1 Vn+1 xn+1, ..., r0m Vm xm}) where r0j is empty or required for j in
+///   n+1...m
+/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ...,
+///   Sn yn, {r1n+1 Sn+1 yn+1, ..., r1q Sq yq}) where r1j is empty or required
+///   for j in n+1...q
+/// and {yn+1, ... , yq} subsetof {xn+1, ... , xm}
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Vi[Z0/X0, ..., Zk/Xk] for i in 0...n
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Tj[Z0/X0, ..., Zk/Xk] for i in n+1...q, yj = xi
+/// and for each j such that r0j is required, then there exists an i in n+1...q
+///   such that xj = yi, and r1i is required
 /// and U0[Z0/X0, ..., Zk/Xk] <: U1[Z0/Y0, ..., Zk/Yk]
 /// and B0i[Z0/X0, ..., Zk/Xk] === B1i[Z0/Y0, ..., Zk/Yk] for i in 0...k
 /// where the Zi are fresh type variables with bounds B0i[Z0/X0, ..., Zk/Xk]
+///
 /// @description Check that if T0 and T1 satisfies the rules above, then T0 is
 /// subtype of T1
 /// @author sgrekhov@unipro.ru

LanguageFeatures/Subtyping/dynamic/generated/named_function_types_arguments_binding_A01_t03.dart

@@ -3,17 +3,22 @@
 // BSD-style license that can be found in the LICENSE file.
 
 /// @assertion A type T0 is a subtype of a type T1 (written T0 <: T1) when:
-/// Named Function Types: T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>
-///   (T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})
-///
-/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ..., Sn yn,
-/// {Sn+1 yn+1, ..., Sq yq})
-/// and {yn+1, ..., yq} subset of {xn+1, ..., xm}
+/// Named Function Types:
+/// T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>(V0 x0, ..., Vn xn,
+///   {r0n+1 Vn+1 xn+1, ..., r0m Vm xm}) where r0j is empty or required for j in
+///   n+1...m
+/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ...,
+///   Sn yn, {r1n+1 Sn+1 yn+1, ..., r1q Sq yq}) where r1j is empty or required
+///   for j in n+1...q
+/// and {yn+1, ... , yq} subsetof {xn+1, ... , xm}
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Vi[Z0/X0, ..., Zk/Xk] for i in 0...n
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Tj[Z0/X0, ..., Zk/Xk] for i in n+1...q, yj = xi
+/// and for each j such that r0j is required, then there exists an i in n+1...q
+///   such that xj = yi, and r1i is required
 /// and U0[Z0/X0, ..., Zk/Xk] <: U1[Z0/Y0, ..., Zk/Yk]
 /// and B0i[Z0/X0, ..., Zk/Xk] === B1i[Z0/Y0, ..., Zk/Yk] for i in 0...k
 /// where the Zi are fresh type variables with bounds B0i[Z0/X0, ..., Zk/Xk]
+///
 /// @description Check that if T0 and T1 satisfies the rules above, then T0 is
 /// subtype of T1
 /// @author sgrekhov@unipro.ru

LanguageFeatures/Subtyping/dynamic/generated/named_function_types_arguments_binding_A02_t01.dart

@@ -3,17 +3,22 @@
 // BSD-style license that can be found in the LICENSE file.
 
 /// @assertion A type T0 is a subtype of a type T1 (written T0 <: T1) when:
-/// Named Function Types: T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>
-///   (T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})
-///
-/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ..., Sn yn,
-/// {Sn+1 yn+1, ..., Sq yq})
-/// and {yn+1, ..., yq} subset of {xn+1, ..., xm}
+/// Named Function Types:
+/// T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>(V0 x0, ..., Vn xn,
+///   {r0n+1 Vn+1 xn+1, ..., r0m Vm xm}) where r0j is empty or required for j in
+///   n+1...m
+/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ...,
+///   Sn yn, {r1n+1 Sn+1 yn+1, ..., r1q Sq yq}) where r1j is empty or required
+///   for j in n+1...q
+/// and {yn+1, ... , yq} subsetof {xn+1, ... , xm}
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Vi[Z0/X0, ..., Zk/Xk] for i in 0...n
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Tj[Z0/X0, ..., Zk/Xk] for i in n+1...q, yj = xi
+/// and for each j such that r0j is required, then there exists an i in n+1...q
+///   such that xj = yi, and r1i is required
 /// and U0[Z0/X0, ..., Zk/Xk] <: U1[Z0/Y0, ..., Zk/Yk]
 /// and B0i[Z0/X0, ..., Zk/Xk] === B1i[Z0/Y0, ..., Zk/Yk] for i in 0...k
 /// where the Zi are fresh type variables with bounds B0i[Z0/X0, ..., Zk/Xk]
+///
 /// @description Check that if T0 and T1 satisfies the rules above, then T0 is
 /// subtype of T1. Test generic types
 /// @author sgrekhov@unipro.ru

LanguageFeatures/Subtyping/dynamic/generated/named_function_types_arguments_binding_A02_t02.dart

@@ -3,17 +3,22 @@
 // BSD-style license that can be found in the LICENSE file.
 
 /// @assertion A type T0 is a subtype of a type T1 (written T0 <: T1) when:
-/// Named Function Types: T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>
-///   (T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})
-///
-/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ..., Sn yn,
-/// {Sn+1 yn+1, ..., Sq yq})
-/// and {yn+1, ..., yq} subset of {xn+1, ..., xm}
+/// Named Function Types:
+/// T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>(V0 x0, ..., Vn xn,
+///   {r0n+1 Vn+1 xn+1, ..., r0m Vm xm}) where r0j is empty or required for j in
+///   n+1...m
+/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ...,
+///   Sn yn, {r1n+1 Sn+1 yn+1, ..., r1q Sq yq}) where r1j is empty or required
+///   for j in n+1...q
+/// and {yn+1, ... , yq} subsetof {xn+1, ... , xm}
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Vi[Z0/X0, ..., Zk/Xk] for i in 0...n
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Tj[Z0/X0, ..., Zk/Xk] for i in n+1...q, yj = xi
+/// and for each j such that r0j is required, then there exists an i in n+1...q
+///   such that xj = yi, and r1i is required
 /// and U0[Z0/X0, ..., Zk/Xk] <: U1[Z0/Y0, ..., Zk/Yk]
 /// and B0i[Z0/X0, ..., Zk/Xk] === B1i[Z0/Y0, ..., Zk/Yk] for i in 0...k
 /// where the Zi are fresh type variables with bounds B0i[Z0/X0, ..., Zk/Xk]
+///
 /// @description Check that if T0 and T1 satisfies the rules above, then T0 is
 /// subtype of T1. Test generic types
 /// @author sgrekhov@unipro.ru

LanguageFeatures/Subtyping/dynamic/generated/named_function_types_arguments_binding_A02_t03.dart

@@ -3,17 +3,22 @@
 // BSD-style license that can be found in the LICENSE file.
 
 /// @assertion A type T0 is a subtype of a type T1 (written T0 <: T1) when:
-/// Named Function Types: T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>
-///   (T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})
-///
-/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ..., Sn yn,
-/// {Sn+1 yn+1, ..., Sq yq})
-/// and {yn+1, ..., yq} subset of {xn+1, ..., xm}
+/// Named Function Types:
+/// T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>(V0 x0, ..., Vn xn,
+///   {r0n+1 Vn+1 xn+1, ..., r0m Vm xm}) where r0j is empty or required for j in
+///   n+1...m
+/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ...,
+///   Sn yn, {r1n+1 Sn+1 yn+1, ..., r1q Sq yq}) where r1j is empty or required
+///   for j in n+1...q
+/// and {yn+1, ... , yq} subsetof {xn+1, ... , xm}
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Vi[Z0/X0, ..., Zk/Xk] for i in 0...n
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Tj[Z0/X0, ..., Zk/Xk] for i in n+1...q, yj = xi
+/// and for each j such that r0j is required, then there exists an i in n+1...q
+///   such that xj = yi, and r1i is required
 /// and U0[Z0/X0, ..., Zk/Xk] <: U1[Z0/Y0, ..., Zk/Yk]
 /// and B0i[Z0/X0, ..., Zk/Xk] === B1i[Z0/Y0, ..., Zk/Yk] for i in 0...k
 /// where the Zi are fresh type variables with bounds B0i[Z0/X0, ..., Zk/Xk]
+///
 /// @description Check that if T0 and T1 satisfies the rules above, then T0 is
 /// subtype of T1. Test generic types
 /// @author sgrekhov@unipro.ru

LanguageFeatures/Subtyping/dynamic/generated/named_function_types_arguments_binding_A03_t01.dart

@@ -3,17 +3,22 @@
 // BSD-style license that can be found in the LICENSE file.
 
 /// @assertion A type T0 is a subtype of a type T1 (written T0 <: T1) when:
-/// Named Function Types: T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>
-///   (T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})
-///
-/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ..., Sn yn,
-/// {Sn+1 yn+1, ..., Sq yq})
-/// and {yn+1, ..., yq} subset of {xn+1, ..., xm}
+/// Named Function Types:
+/// T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>(V0 x0, ..., Vn xn,
+///   {r0n+1 Vn+1 xn+1, ..., r0m Vm xm}) where r0j is empty or required for j in
+///   n+1...m
+/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ...,
+///   Sn yn, {r1n+1 Sn+1 yn+1, ..., r1q Sq yq}) where r1j is empty or required
+///   for j in n+1...q
+/// and {yn+1, ... , yq} subsetof {xn+1, ... , xm}
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Vi[Z0/X0, ..., Zk/Xk] for i in 0...n
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Tj[Z0/X0, ..., Zk/Xk] for i in n+1...q, yj = xi
+/// and for each j such that r0j is required, then there exists an i in n+1...q
+///   such that xj = yi, and r1i is required
 /// and U0[Z0/X0, ..., Zk/Xk] <: U1[Z0/Y0, ..., Zk/Yk]
 /// and B0i[Z0/X0, ..., Zk/Xk] === B1i[Z0/Y0, ..., Zk/Yk] for i in 0...k
 /// where the Zi are fresh type variables with bounds B0i[Z0/X0, ..., Zk/Xk]
+///
 /// @description Check that if T0 and T1 satisfies the rules above, then T0 is
 /// subtype of T1. Test generic types with high-level types
 /// @author sgrekhov@unipro.ru

LanguageFeatures/Subtyping/dynamic/generated/named_function_types_arguments_binding_A03_t02.dart

@@ -3,17 +3,22 @@
 // BSD-style license that can be found in the LICENSE file.
 
 /// @assertion A type T0 is a subtype of a type T1 (written T0 <: T1) when:
-/// Named Function Types: T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>
-///   (T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})
-///
-/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ..., Sn yn,
-/// {Sn+1 yn+1, ..., Sq yq})
-/// and {yn+1, ..., yq} subset of {xn+1, ..., xm}
+/// Named Function Types:
+/// T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>(V0 x0, ..., Vn xn,
+///   {r0n+1 Vn+1 xn+1, ..., r0m Vm xm}) where r0j is empty or required for j in
+///   n+1...m
+/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ...,
+///   Sn yn, {r1n+1 Sn+1 yn+1, ..., r1q Sq yq}) where r1j is empty or required
+///   for j in n+1...q
+/// and {yn+1, ... , yq} subsetof {xn+1, ... , xm}
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Vi[Z0/X0, ..., Zk/Xk] for i in 0...n
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Tj[Z0/X0, ..., Zk/Xk] for i in n+1...q, yj = xi
+/// and for each j such that r0j is required, then there exists an i in n+1...q
+///   such that xj = yi, and r1i is required
 /// and U0[Z0/X0, ..., Zk/Xk] <: U1[Z0/Y0, ..., Zk/Yk]
 /// and B0i[Z0/X0, ..., Zk/Xk] === B1i[Z0/Y0, ..., Zk/Yk] for i in 0...k
 /// where the Zi are fresh type variables with bounds B0i[Z0/X0, ..., Zk/Xk]
+///
 /// @description Check that if T0 and T1 satisfies the rules above, then T0 is
 /// subtype of T1. Test generic types with high-level types
 /// @author sgrekhov@unipro.ru

LanguageFeatures/Subtyping/dynamic/generated/named_function_types_arguments_binding_A03_t03.dart

@@ -3,17 +3,22 @@
 // BSD-style license that can be found in the LICENSE file.
 
 /// @assertion A type T0 is a subtype of a type T1 (written T0 <: T1) when:
-/// Named Function Types: T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>
-///   (T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})
-///
-/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ..., Sn yn,
-/// {Sn+1 yn+1, ..., Sq yq})
-/// and {yn+1, ..., yq} subset of {xn+1, ..., xm}
+/// Named Function Types:
+/// T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>(V0 x0, ..., Vn xn,
+///   {r0n+1 Vn+1 xn+1, ..., r0m Vm xm}) where r0j is empty or required for j in
+///   n+1...m
+/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ...,
+///   Sn yn, {r1n+1 Sn+1 yn+1, ..., r1q Sq yq}) where r1j is empty or required
+///   for j in n+1...q
+/// and {yn+1, ... , yq} subsetof {xn+1, ... , xm}
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Vi[Z0/X0, ..., Zk/Xk] for i in 0...n
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Tj[Z0/X0, ..., Zk/Xk] for i in n+1...q, yj = xi
+/// and for each j such that r0j is required, then there exists an i in n+1...q
+///   such that xj = yi, and r1i is required
 /// and U0[Z0/X0, ..., Zk/Xk] <: U1[Z0/Y0, ..., Zk/Yk]
 /// and B0i[Z0/X0, ..., Zk/Xk] === B1i[Z0/Y0, ..., Zk/Yk] for i in 0...k
 /// where the Zi are fresh type variables with bounds B0i[Z0/X0, ..., Zk/Xk]
+///
 /// @description Check that if T0 and T1 satisfies the rules above, then T0 is
 /// subtype of T1. Test generic types with high-level types
 /// @author sgrekhov@unipro.ru

LanguageFeatures/Subtyping/dynamic/generated/named_function_types_arguments_binding_A04_t01.dart

@@ -3,17 +3,22 @@
 // BSD-style license that can be found in the LICENSE file.
 
 /// @assertion A type T0 is a subtype of a type T1 (written T0 <: T1) when:
-/// Named Function Types: T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>
-///   (T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})
-///
-/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ..., Sn yn,
-/// {Sn+1 yn+1, ..., Sq yq})
-/// and {yn+1, ..., yq} subset of {xn+1, ..., xm}
+/// Named Function Types:
+/// T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>(V0 x0, ..., Vn xn,
+///   {r0n+1 Vn+1 xn+1, ..., r0m Vm xm}) where r0j is empty or required for j in
+///   n+1...m
+/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ...,
+///   Sn yn, {r1n+1 Sn+1 yn+1, ..., r1q Sq yq}) where r1j is empty or required
+///   for j in n+1...q
+/// and {yn+1, ... , yq} subsetof {xn+1, ... , xm}
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Vi[Z0/X0, ..., Zk/Xk] for i in 0...n
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Tj[Z0/X0, ..., Zk/Xk] for i in n+1...q, yj = xi
+/// and for each j such that r0j is required, then there exists an i in n+1...q
+///   such that xj = yi, and r1i is required
 /// and U0[Z0/X0, ..., Zk/Xk] <: U1[Z0/Y0, ..., Zk/Yk]
 /// and B0i[Z0/X0, ..., Zk/Xk] === B1i[Z0/Y0, ..., Zk/Yk] for i in 0...k
 /// where the Zi are fresh type variables with bounds B0i[Z0/X0, ..., Zk/Xk]
+///
 /// @description Check that if T0 and T1 satisfies the rules above, then T0 is
 /// subtype of T1. Test generic types with Null type
 /// @author sgrekhov@unipro.ru

LanguageFeatures/Subtyping/dynamic/generated/named_function_types_arguments_binding_A04_t02.dart

@@ -3,17 +3,22 @@
 // BSD-style license that can be found in the LICENSE file.
 
 /// @assertion A type T0 is a subtype of a type T1 (written T0 <: T1) when:
-/// Named Function Types: T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>
-///   (T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})
-///
-/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ..., Sn yn,
-/// {Sn+1 yn+1, ..., Sq yq})
-/// and {yn+1, ..., yq} subset of {xn+1, ..., xm}
+/// Named Function Types:
+/// T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>(V0 x0, ..., Vn xn,
+///   {r0n+1 Vn+1 xn+1, ..., r0m Vm xm}) where r0j is empty or required for j in
+///   n+1...m
+/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ...,
+///   Sn yn, {r1n+1 Sn+1 yn+1, ..., r1q Sq yq}) where r1j is empty or required
+///   for j in n+1...q
+/// and {yn+1, ... , yq} subsetof {xn+1, ... , xm}
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Vi[Z0/X0, ..., Zk/Xk] for i in 0...n
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Tj[Z0/X0, ..., Zk/Xk] for i in n+1...q, yj = xi
+/// and for each j such that r0j is required, then there exists an i in n+1...q
+///   such that xj = yi, and r1i is required
 /// and U0[Z0/X0, ..., Zk/Xk] <: U1[Z0/Y0, ..., Zk/Yk]
 /// and B0i[Z0/X0, ..., Zk/Xk] === B1i[Z0/Y0, ..., Zk/Yk] for i in 0...k
 /// where the Zi are fresh type variables with bounds B0i[Z0/X0, ..., Zk/Xk]
+///
 /// @description Check that if T0 and T1 satisfies the rules above, then T0 is
 /// subtype of T1. Test generic types with Null type
 /// @author sgrekhov@unipro.ru

LanguageFeatures/Subtyping/dynamic/generated/named_function_types_arguments_binding_A04_t03.dart

@@ -3,17 +3,22 @@
 // BSD-style license that can be found in the LICENSE file.
 
 /// @assertion A type T0 is a subtype of a type T1 (written T0 <: T1) when:
-/// Named Function Types: T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>
-///   (T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})
-///
-/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ..., Sn yn,
-/// {Sn+1 yn+1, ..., Sq yq})
-/// and {yn+1, ..., yq} subset of {xn+1, ..., xm}
+/// Named Function Types:
+/// T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>(V0 x0, ..., Vn xn,
+///   {r0n+1 Vn+1 xn+1, ..., r0m Vm xm}) where r0j is empty or required for j in
+///   n+1...m
+/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ...,
+///   Sn yn, {r1n+1 Sn+1 yn+1, ..., r1q Sq yq}) where r1j is empty or required
+///   for j in n+1...q
+/// and {yn+1, ... , yq} subsetof {xn+1, ... , xm}
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Vi[Z0/X0, ..., Zk/Xk] for i in 0...n
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Tj[Z0/X0, ..., Zk/Xk] for i in n+1...q, yj = xi
+/// and for each j such that r0j is required, then there exists an i in n+1...q
+///   such that xj = yi, and r1i is required
 /// and U0[Z0/X0, ..., Zk/Xk] <: U1[Z0/Y0, ..., Zk/Yk]
 /// and B0i[Z0/X0, ..., Zk/Xk] === B1i[Z0/Y0, ..., Zk/Yk] for i in 0...k
 /// where the Zi are fresh type variables with bounds B0i[Z0/X0, ..., Zk/Xk]
+///
 /// @description Check that if T0 and T1 satisfies the rules above, then T0 is
 /// subtype of T1. Test generic types with Null type
 /// @author sgrekhov@unipro.ru

LanguageFeatures/Subtyping/dynamic/generated/named_function_types_arguments_binding_A05_t01.dart

@@ -3,17 +3,22 @@
 // BSD-style license that can be found in the LICENSE file.
 
 /// @assertion A type T0 is a subtype of a type T1 (written T0 <: T1) when:
-/// Named Function Types: T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>
-///   (T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})
-///
-/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ..., Sn yn,
-/// {Sn+1 yn+1, ..., Sq yq})
-/// and {yn+1, ..., yq} subset of {xn+1, ..., xm}
+/// Named Function Types:
+/// T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>(V0 x0, ..., Vn xn,
+///   {r0n+1 Vn+1 xn+1, ..., r0m Vm xm}) where r0j is empty or required for j in
+///   n+1...m
+/// and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ...,
+///   Sn yn, {r1n+1 Sn+1 yn+1, ..., r1q Sq yq}) where r1j is empty or required
+///   for j in n+1...q
+/// and {yn+1, ... , yq} subsetof {xn+1, ... , xm}
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Vi[Z0/X0, ..., Zk/Xk] for i in 0...n
 /// and Si[Z0/Y0, ..., Zk/Yk] <: Tj[Z0/X0, ..., Zk/Xk] for i in n+1...q, yj = xi
+/// and for each j such that r0j is required, then there exists an i in n+1...q
+///   such that xj = yi, and r1i is required
 /// and U0[Z0/X0, ..., Zk/Xk] <: U1[Z0/Y0, ..., Zk/Yk]
 /// and B0i[Z0/X0, ..., Zk/Xk] === B1i[Z0/Y0, ..., Zk/Yk] for i in 0...k
 /// where the Zi are fresh type variables with bounds B0i[Z0/X0, ..., Zk/Xk]
+///
 /// @description Check that if T0 and T1 satisfies the rules above, then T0 is
 /// subtype of T1. Test generic types
 /// @author sgrekhov@unipro.ru