[m-rev.] for review: Document how tuple types work in subtypes/coerce.

[Peter Wang]

doc/reference_manual.texi:
    Include tuple types in the discussion of how subtype constructor
    arguments may vary.

    Include tuple types in the discussion of type-correctness of
    coerce.

diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
index e382fea4d..53ea1dca9 100644
--- a/doc/reference_manual.texi
+++ b/doc/reference_manual.texi
@@ -3357,8 +3357,9 @@ It may change the types of some of the arguments of some of the constructors,
 
 Formally, this means that
 if the supertype @samp{t} has a constructor @samp{f(T1, ..., Tn)},
-and the subtype @samp{s =< t} has a constructor @samp{f(S1, ..., Sn)}.
-then for each @var{Si}, the condition @samp{Si =< Ti} must hold.
+and the subtype @samp{s =< t} has a constructor @samp{f(S1, ..., Sn)},
+then for each @var{Si}, the condition @samp{Si =< Ti} must hold,
+where @samp{=<} is the subtype relation below.
 @end itemize
 
 This is an example of the first kind of difference:
@@ -3415,24 +3416,17 @@ that does not occur in @var{supertype}.
 (In the following discussion,
 we assume that all equivalence types have been expanded out.)
 
-Mercury considers it possible
-for a type @samp{S} to be a subtype of type @samp{T}, where @samp{S != T},
-in two cases:
-where @samp{S} and @samp{T} are both discriminated union type,
-and where they are both higher order types.
-In every other case,
- at samp{S} is a subtype of @samp{T}, denoted @samp{S =< T},
-if and only if @samp{S} and @samp{T} are syntactically identical,
-i.e.@ @samp{S = T}.
-
-A discriminated union type @samp{S}
-can be a subtype of another discriminated union type @samp{T}
-in two distinct ways:
+The subtype relation @samp{S =< T} has four cases to consider:
+when @samp{S} and @samp{T} are both discriminated union types,
+when they are both tuple types,
+when they are both higher order types,
+and all other types.
 
+For discriminated union types @samp{S} and @samp{T}:
 @itemize
 @item
 If @samp{S} and @samp{T} have the same principal type constructor,
-say @var{f/n}, which implies that
+say @samp{f/n}, which implies that
 @samp{S = f(S1, ..., Sn)} and @samp{T = f(T1, ..., Tn)},
 then @samp{S =< T} holds if and only if
 for all @var{i} in @samp{1..n}, @samp{Si =< Ti}.
@@ -3453,11 +3447,19 @@ are replaced by the corresponding for @var{Si} to give @var{Usub},
 then @samp{Usub =< T} must hold.
 @end itemize
 
+For two tuple types
+ at samp{S = @{S1, ..., Sn@}} and @samp{T = @{T1, ..., Tn@}},
+ at samp{S =< T} holds if and only if
+ at samp{Si =< Ti} for all @samp{i} in @samp{1..n}.
+This is analogous to the case for discriminated union types
+with the same principal type constructor.
+
 A higher order type @samp{S}
 can be a subtype of another higher order type @samp{T}
 in only one way.
 Since subtype definitions do not apply to higher order types,
-this way is analogous to the first way above.
+this way is analogous to the case for discriminated union types
+with the same principal type constructor.
 
 @itemize
 @item
@@ -3482,7 +3484,9 @@ if and only if all of the following conditions hold:
     @end itemize
 @end itemize
 
-In every case not covered above, @samp{S =< T} if and only if @samp{S = T}.
+For all other types,
+ at samp{S =< T} if and only if @samp{S = T},
+i.e.@ they are syntactically identical.
 
 A subtype may be exported as an abstract type
 by declaring only the name of the subtype in the
@@ -8473,13 +8477,13 @@ if the two types are the same
 
 @item
 @samp{Si < Ti}
-if @var{Si} is a subtype of @var{Ti},
-according to visible subtype definitions
+if @var{Si} is a subtype of @var{Ti}
+by the relation below
 
 @item
 @samp{Ti < Si}
-if @var{Ti} is a subtype of @var{Si},
-according to visible subtype definitions
+if @var{Ti} is a subtype of @var{Si}
+by the relation below
 @end itemize
 
 Otherwise, the @code{coerce} expression is not type-correct.
@@ -8508,6 +8512,19 @@ in a discriminated union type,
 other than a recursive type of the exact form @samp{base(B1, ..., Bn)}
 @end itemize
 
+The relation @samp{S < T} is true when @samp{S != T} and either:
+ at itemize
+ at item
+ at samp{S} and @samp{T} are both discriminated union types,
+and @samp{S} is a subtype of @samp{T} by visible subtype definitions;
+or
+
+ at item
+ at samp{S} and @samp{T} are both tuple types of the same arity,
+and for each pair of corresponding argument types @samp{Si} and @samp{Ti},
+ at samp{Si < Ti} is true.
+ at end itemize
+
 @heading Mode checking
 
 Type conversion expressions must also be mode-correct.
-- 
2.44.0