Eliminate the notion of "bound resolution" from inference.md.

In its place, the spec's definition of "T_0 bounded" is tightened up
so that for any type T, there is exactly one type T_0 such that T is
T_0 bounded. Then, instead of saying "let U_0 be the bound resolution
of T_0", we can say "let U_0 be the unique type such that T_0 is U_0
bounded."

This avoids some redundancy, since we no longer need to define
separate but related notions of "T_0 bounded" and "bound resolution".

resources/type-system/inference.md

@@ -969,24 +969,6 @@ with respect to `L` under constraints `C0`
   - If for `i` in `0...m`, `Mi` is a subtype match for `Ni` with respect to `L`
   under constraints `Ci`.
 
-## Bound resolution
-
-For any type `T`, the _bound resolution_ of `T` is a type `U`, defined by the
-following recursive process:
-
-- If `T` is a type variable `X`, then let `B` be the bound of `X`. Then let `U`
-  be the bound resolution of `B`.
-
-- Otherwise, if `T` is a promoted type variable `X&B`, then let `U` be the bound
-  resolution of `B`.
-
-- Otherwise, let `U` be `T`.
-
-_Note that the spec notions of __dynamic__ boundedness and __Function__
-boundedness can be defined in terms of bound resolution, as follows: a type is
-__dynamic__ bounded iff its bound resolution is __dynamic__, and a type is
-__Function__ bounded if its bound resolution if __Function__._
-
 # Expression inference
 
 Expression inference is a recursive process of elaborating an expression in Dart
@@ -1599,7 +1581,7 @@ static type `T`, where `m` and `T` are determined as follows:
 
 - If `T_0` is `void`, there is a compile-time error.
 
-- Let `U_0` be the [bound resolution](#Bound-resolution) of `T_0`.
+- Let `U_0` be the unique type such that `T_0` is `U_0` bounded.
 
 - If `U_0` is `dynamic` or `Never`, or `U_0` is `Function` and `id` is `call`,
   then:

specification/dartLangSpec.tex

@@ -13039,6 +13039,7 @@ \subsubsection{Binding Actuals to Formals}
 \LMHash{}%
 For a given type $T_0$, we introduce the notion of a
 \IndexCustom{$T_0$ bounded type}{type!T0 bounded}:
+If $T_0$ is neither a type variable nor an intersection type, then
 $T_0$ itself is $T_0$ bounded;
 if $B$ is $T_0$ bounded and
 $X$ is a type variable with bound $B$
@@ -13054,6 +13055,12 @@ \subsubsection{Binding Actuals to Formals}
 Similarly for a
 \IndexCustom{\FUNCTION{} bounded type}{type!function bounded}.
 
+\commentary{%
+Since it is illegal for a type parameter to be a supertype of its own
+bound, it follows that for any type $T$, there exists exactly one type
+$T_0$ for which $T$ is $T_0$ bounded.%
+}
+
 \LMHash{}%
 A
 \IndexCustom{function-type bounded type}{type!function-type bounded}