diff --git a/doc/mercury_reference_manual.texi b/doc/mercury_reference_manual.texi
index ebed23b19..b2286d571 100644
--- a/doc/mercury_reference_manual.texi
+++ b/doc/mercury_reference_manual.texi
@@ -3298,7 +3298,7 @@ or as equivalence types.
 @node Subtypes
 @subsection Subtypes
 
-(This is a new and experimental feature, subject to change.)
+(This is a relatively new feature, and is subject to change.)
 
 A subtype is a discriminated union type
 that is a subset of a supertype,
@@ -3311,6 +3311,8 @@ the syntax for non-subtype discriminated union types is
 @example
 :- type @var{type} ---> @var{body}.
 @end example
+@c XXX We should format our examples using our usual style,
+@c meaning the ---> body part should be on a separate line.
 where @var{type} is the name of a type constructor
 applied to zero or more distinct type variables
 (the @emph{parameters} of the type constructor),
@@ -3323,6 +3325,8 @@ The syntax for subtypes is similar but slightly different:
 @example
 :- type @var{subtype} =< @var{supertype} ---> @var{body}.
 @end example
+@c XXX We should format our examples using our usual style,
+@c meaning the ---> body part should be on a separate line.
 Since a subtype is also a discriminated union type,
 the rules for discriminated union types apply to them as well:
 @var{subtype} must be the name of a type constructor
@@ -3344,7 +3348,7 @@ by normal module visibility rules.
 
 The discriminated union type specified by @var{supertype}
 may itself be a subtype.
-Following the chain of subtype definitions,
+Following the chain of subtype-to-supertype links,
 it must be possible to arrive at a @emph{base type},
 which is a discriminated union type but @emph{not} a subtype.
 
@@ -8507,7 +8511,7 @@ good_example3_univ("bar"::in(bound("bar")), univ("blah")::out).
 @node Type conversions
 @chapter Type conversions
 
-(This is a new and experimental feature, subject to change.)
+(This is a relatively new feature, and is subject to change.)
 
 A term may be converted from one type @var{FromType}
 to another type @var{ToType}
@@ -8520,39 +8524,64 @@ coerce(@var{Term})
 The expression is type-correct if and only if
 @var{FromType} and @var{ToType} are both discriminated union types,
 and after replacing the principal type constructors with base types
+@c XXX This reads like a category error:
+@c you replace a type_ctor with another type_ctor,
+@c or a type_ctor with another type;
+@c you do not replace a type_ctor with a complete type.
 (@pxref{Subtypes})
 the two types have the same type constructor,
 and the arguments of the common type constructor
 satisfy the type parameter variance restrictions below.
 
 Let @var{FromType} expand out to @samp{base(S1, ..., Sn)}
+@c XXX In the subtype section, we use "expand" only in the sense of
+@c expanding out equivalence types. Here, we also include replacing each
+@c subtype with its supertype, using the head of the subtype's definition.
+@c Do we have a specific name for that operation?
+@c If not, *should* we give it a name?
 and @var{ToType} expand out to @samp{base(T1, ..., Tn)},
 where @samp{base(B1, ..., Bn)} is the common base type,
 and @var{Bi} is the i'th type parameter,
 which is bound to @var{Si} in @var{FromType}
 and @var{Ti} in @var{ToType}.
+@c XXX Wouldn't Fi be better notation than Si?
+@c Si would make sense if we talked about source types, but
+@c we call them about from-types.
+@c XXX And wouldn't BPi be better notation than just Bi?
+@c It would clarify that BPi are type parameters, i.e. type variables,
+@c while the Si/Fi/Ti are complete types.
 
 For each pair of corresponding type arguments,
 one of the following must be true:
 @itemize
 @item
-@samp{Si = Ti}
-if the two types are the same
+@samp{Si = Ti},
+meaning the two types are the same
 
 @item
-@samp{Si < Ti}
-if @var{Si} is a subtype of @var{Ti}
+@samp{Si < Ti},
+meaning @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}
+@samp{Ti < Si},
+meaning @var{Ti} is a subtype of @var{Si}
 by the relation below
 @end itemize
 
-Otherwise, the @code{coerce} expression is not type-correct.
+If none of the above is true, i.e.@: if @samp{Si} and @samp{Ti} are not related.
+then the @code{coerce} expression is not type-correct.
 @c NOTE: we deliberately disallow coercion between arbitrary phantom types.
 
+@c I wouild approach the above by
+@c - first defining the @samp{S =< T} relation,
+@c - defining four categories (2x2) based on whether S=<T and T=<S hold,
+@c - dividing the base type_ctor's parameters into
+@c   - the must-be-invariant parameters for which S=T must hold, and
+@c   - the need-not-be-invariant parameters for which one or both of
+@c     S=<T and T=<S must hold
+@c - and THEN saying which parameters must be invariant.
+
 Furthermore,
 @samp{Si = Ti} must be true
 if @var{Bi} occurs in one or more of these locations