From d57c8f9066affe971fcc682f730a94f2165f8708 Mon Sep 17 00:00:00 2001
From: Paul Berry <paulberry@google.com>
Date: Tue, 6 Aug 2024 18:05:18 +0000
Subject: [PATCH 1/2] 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 | 23 +----------------------
 specification/dartLangSpec.tex     |  7 +++++++
 2 files changed, 8 insertions(+), 22 deletions(-)

diff --git a/resources/type-system/inference.md b/resources/type-system/inference.md
index 543a2c35f..3f1442e4c 100644
--- a/resources/type-system/inference.md
+++ b/resources/type-system/inference.md
@@ -969,27 +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`.
-
-_The point of bound resolution of `T` is to find a non-type-variable type which
-is a (minimal) supertype of `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 iff its bound resolution is __Function__._
-
 # Expression inference
 
 Expression inference is a recursive process of elaborating an expression in Dart
@@ -1602,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:
diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 15a9da304..43cd5b448 100644
--- a/specification/dartLangSpec.tex
+++ b/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}

From 74e579473f20e7c3599a10b8530dcf7771080a6a Mon Sep 17 00:00:00 2001
From: Paul Berry <paulberry@google.com>
Date: Tue, 6 Aug 2024 18:06:41 +0000
Subject: [PATCH 2/2] Add text based on review comment.

See https://github.com/dart-lang/language/pull/3937#discussion_r1655345853.
---
 specification/dartLangSpec.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 43cd5b448..138d73bbf 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -13058,7 +13058,8 @@ \subsubsection{Binding Actuals to Formals}
 \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.%
+$T_0$ for which $T$ is $T_0$ bounded. $T_0$ can be regarded as a
+non-type-variable type which is a (minimal) supertype of $T$.%
 }
 
 \LMHash{}%