diff --git a/doc/mercury_reference_manual.texi b/doc/mercury_reference_manual.texi
index ebed23b19..0ae5fb1a4 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,
@@ -3309,7 +3309,8 @@ using type conversion expressions (@pxref{Type conversions}).
 As previously described,
 the syntax for non-subtype discriminated union types is
 @example
-:- type @var{type} ---> @var{body}.
+:- type @var{type}
+        --->    @var{body}
 @end example
 where @var{type} is the name of a type constructor
 applied to zero or more distinct type variables
@@ -3321,7 +3322,8 @@ must be among @var{type}'s parameters.
 
 The syntax for subtypes is similar but slightly different:
 @example
-:- type @var{subtype} =< @var{supertype} ---> @var{body}.
+:- type @var{subtype} =< @var{supertype}
+        --->    @var{body}.
 @end example
 Since a subtype is also a discriminated union type,
 the rules for discriminated union types apply to them as well:
@@ -3344,10 +3346,12 @@ 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.
 
+@heading Differences between subtype and supertype
+
 The body of the subtype may differ from the body of its supertype in two ways.
 @itemize @bullet
 @item
@@ -3421,86 +3425,221 @@ that does not occur in @var{supertype}.
 @c There should be some discussion here
 @c of the possible uses of this flexibility.
 
+@c I (zs) can't think of any such uses that wouldn't be better expressed
+@c using simple equivalence type definitions, such as
+@c
+@c :- type self_map(T) == map(T, T).
+@c
+@c for duplicating type parameters in the supertype, or
+@c
+@c :- type multi_map(K, V) == map(K, list(V)).
+@c
+@c for introducing type constructors into the supertype.
+@c
+@c As for phantom parameters in the subtype, adding them to the supertype
+@c should work as well.
+
+Subtypes must not have user-defined equality or comparison predicates.
+The base type of a subtype may have user-defined equality or comparison.
+In that case, values of the subtype will be tested for equality or
+compared using those predicates.
+
+There is no special interaction between subtypes and the type class system.
+
+@heading Lifting a subtype
+
+If type @samp{S} has the form @samp{S = tc(S1, ..., Sn)}
+and there is a visible subtype definition starting with
+@w{@samp{:- type tc(RP1, ..., RPn) =< U}},
+then we define @samp{lift(S)} as the type that results from
+replacing all occurrences of each type parameter @samp{RPi} in @samp{U}
+with the corresponding @samp{Si}.
+
+Since the sypertype @samp{U} in that subtype definition
+must have the form of a type constructor
+applied to zero or more argument types,
+the result of the substitution must also have the same form.
+If the supertype's type constructor is also a subtype,
+then lifting may be applied to it as well.
+
+We define @samp{lift_to_base(S)} as
+@itemize @bullet
+@item
+@samp{lift_to_base(lift(S))},
+if the principal type constructor of @samp{S}
+has a visible subtype definition; and
+@item
+@samp{S}, otherwise.
+@end itemize
+
+@samp{lift_to_base} effectively computes
+the fixpoint of the @samp{lift} operation.
+However, we can also stop lifting before we get to the fixpoint.
+
+We define @samp{lift_to(tc/n, S)} as
+@itemize @bullet
+@item
+@samp{S}, if the principal type constructor of @samp{S} is @samp{tc/n};
+@item
+@samp{lift_to(tc/n, lift(S))},
+if the principal type constructor of @samp{S} is not @samp{tc/n},
+but that principal type constructor does have a visible subtype definition; and
+@item
+@samp{S}, otherwise.
+@end itemize
+
+@heading The subtype relation
+
 (In the following discussion,
 we assume that all equivalence types have been expanded out.)
 
-The subtype relation @samp{S =< T} has four cases to consider:
+The subtype relation @samp{S =< T} has three 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.
 
-@c Manually numbered as @enumerate introduces another level of indentation
+@c Manually numbered, as @enumerate introduces another level of indentation
 @c and leaves too little space between the items.
 @noindent
-1. For discriminated union types @samp{S} and @samp{T}:
+1. For two discriminated union types
+@samp{S = tcs(S1, ..., Sm)} and @samp{T = tct(T1, ..., Tn)}:
+let @samp{LS} be @samp{lift_to(tct/n, S)}.
+Then @samp{S =< T} holds if and only if
+
 @itemize
 @item
-If @samp{S} and @samp{T} have the same principal type constructor,
-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}.
+the principal type constructor of @samp{LS} is also @samp{tct/n},
+meaning that @samp{LS = tct(LS1, ..., LSn)}, and
 @item
-If @samp{S} and @samp{T} have different principal type constructors,
-and if @samp{S = f(S1, ..., Sn)}, @samp{S =< T} holds if
-    @itemize @minus
-    @item
-    there is a visible subtype definition starting with
-    @w{@samp{:- type f(R1, ..., Rn) =< U}},
-    @item
-    for all @var{i} in @samp{1..n}, @w{@samp{Si = Ri}} (unification), and
-    @item
-    @samp{U =< T}.
-    @end itemize
-In other words, if all occurrences of @var{Ri} in @var{U}
-are replaced by the corresponding @var{Si} to give @var{Usub},
-then @samp{Usub =< T} must hold.
+for all @var{i} in @samp{1..n}, @samp{LSi =< Ti}.
 @end itemize
 
+@c @itemize
+@c @item
+@c If @samp{S} and @samp{T} have the same principal type constructor,
+@c say @samp{f/n}, which implies that
+@c @samp{S = f(S1, ..., Sn)} and @samp{T = f(T1, ..., Tn)},
+@c then @samp{S =< T} holds if and only if
+@c for all @var{i} in @samp{1..n}, @samp{Si =< Ti}.
+@c @item
+@c If @samp{S} and @samp{T} have different principal type constructors,
+@c and if @samp{S = f(S1, ..., Sn)}, @samp{S =< T} holds if
+@c     @itemize @minus
+@c     @item
+@c     there is a visible subtype definition starting with
+@c     @w{@samp{:- type f(R1, ..., Rn) =< U}},
+@c     @item
+@c     for all @var{i} in @samp{1..n}, @w{@samp{Si = Ri}} (unification), and
+@c     @item
+@c     @samp{U =< T}.
+@c     @end itemize
+@c In other words, if all occurrences of @var{Ri} in @var{U}
+@c are replaced by the corresponding @var{Si} to give @var{Usub},
+@c then @samp{Usub =< T} must hold.
+@c This is alternative 1.
+@c 
+@c XXX We could replace the second item @emph{either} with just:
+@c 
+@c If @samp{S} and @samp{T} have different principal type constructors,
+@c @samp{S =< T} holds if @samp{lift(S) =< T}.
+@c This is alternative 2.
+@c 
+@c @emph{or} with
+@c 
+@c If @samp{S} and @samp{T} have different principal type constructors,
+@c say @samp{s/n} and @samp{t/m} respectively,
+@c @samp{S =< T} holds if @samp{lift_to(t, m, S) =< T}.
+@c This is alternative 3.
+@c @end itemize
+
 @noindent
 2. For two tuple types
-@samp{S = @{S1, ..., Sn@}} and @samp{T = @{T1, ..., Tn@}},
+@samp{S = @{S1, ..., Sm@}} and @samp{T = @{T1, ..., Tn@}},
 @samp{S =< T} holds if and only if
-@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.
-
-@noindent
-3. 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 case for discriminated union types
-with the same principal type constructor.
 
 @itemize
 @item
-@samp{P =< Q} holds for two higher-order types @var{P} and @var{Q}
-if and only if all of the following conditions hold:
-    @itemize @minus
+@samp{m = n}, and
+@item
+for all @var{i} in @samp{1..n}, @samp{Si =< Ti}.
+@end itemize
+This is analogous to the case for discriminated union types.
+
+@noindent
+3. For all other types,
+@samp{S =< T} if and only if @samp{S = T},
+i.e.@: they are syntactically identical.
+
+Note that this last category includes higher order types.
+If @samp{S} and @samp{T} are both higher order types, then
+@samp{S =< T} can hold only if
+
+@itemize @minus
+@item
+@samp{S} and @samp{T} are either
+both @samp{pred} types, or both @samp{func} types,
+@item
+they have the same arity,
+@item
+@samp{S} and @samp{T} have identical argument types, and
+@item
+either
+    @itemize
     @item
-    @var{P} and @var{Q} are either
-    both @samp{pred} types, or both @samp{func} types,
+    neither @samp{S} and @samp{T} has any higher-order inst information, or
     @item
-    they have the same arity,
-    @item
-    @var{P} and @var{Q} have the same argument types
-    (the current implementation does not allow subtyping
-    in higher-order arguments), and
-    @item
-    if either of @var{P} and @var{Q} has higher-order inst information,
-    then @var{P} and @var{Q} must have
-    the @emph{same} higher-order inst information,
-    i.e.@: their higher-order inst information must specify
+    both @samp{S} and @samp{T} have the same higher-order inst information,
+    meaning that they both specify
     the same argument modes, determinism, and purity.
     @end itemize
 @end itemize
 
-@noindent
-4. For all other types,
-@samp{S =< T} if and only if @samp{S = T},
-i.e.@: they are syntactically identical.
+Subtyping theory allows @samp{S =< T} to hold for e.g. two predicates
+if their arguments are not invariant (meaning they are not identical),
+provided that their input arguments are contravariant and
+their output arguments are covariant.
+However, in Mercury, an argument of a predicate
+can be an input in one mode and an output in another mode.
+Requiring all arguments to be invariant
+is the simplest way for the Mercury typechecker
+to handle the fact that in many cases,
+it will not have access to such mode information.
+
+@c @noindent
+@c 3. A higher-order type @samp{S}
+@c can be a subtype of another higher-order type @samp{T}
+@c in only one way.
+@c this way is analogous to the case for discriminated union types
+@c with the same principal type constructor.
+@c 
+@c @samp{S =< T} holds for two higher-order types @samp{S} and @samp{T}
+@c only if @samp{S} and @samp{T} are identical.
+@c 
+@c In more detail, all of the following conditions must hold:
+@c @itemize @minus
+@c @item
+@c @samp{S} and @samp{T} are either
+@c both @samp{pred} types, or both @samp{func} types,
+@c @item
+@c they have the same arity,
+@c @item
+@c @samp{S} and @samp{T} have the same argument types
+@c (the current implementation does not allow subtyping
+@c in higher-order arguments), and
+@c @c XXX say why: which args are input will depend on modes
+@c @item
+@c either
+@c     @itemize
+@c     @item
+@c     neither @samp{S} and @samp{T} has any higher-order inst information, or
+@c     @item
+@c     both @samp{S} and @samp{T} have the same higher-order inst information,
+@c     meaning that they both specify
+@c     the same argument modes, determinism, and purity.
+@c     @end itemize
+@c @end itemize
+
+@heading Abstract subtypes
 
 A subtype may be exported as an abstract type
 by declaring only the name of the subtype in the
@@ -3523,12 +3662,7 @@ Example:
     --->    [T | list(T)].
 @end example
 
-Subtypes must not have user-defined equality or comparison predicates.
-The base type of a subtype may have user-defined equality or comparison.
-In that case, values of the subtype will be tested for equality or
-compared using those predicates.
-
-There is no special interaction between subtypes and the type class system.
+@heading More examples of subtypes
 
 Some more examples of subtypes:
 
@@ -8507,50 +8641,243 @@ 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}
+A term @samp{FromTerm} may be converted from its type @samp{FromType}
+to another type @samp{ToType}
 using a type conversion expression of the form:
 
 @example
-coerce(@var{Term})
+coerce(@var{FromTerm})
 @end example
 
+whose result it bound, either implicitly or explicitly,
+to another term that here we call @samp{ToTerm}
+(which is usually a variable).
+
+@c The expression is type-correct if and only if
+@c @var{FromType} and @var{ToType} are both discriminated union types,
+@c and, after replacing each of their principal type constructors
+@c with their base type constructors,
+@c @itemize @bullet
+@c @item
+@c the resulting types have the @emph{same} principal type constructor, and
+@c @item
+@c the arguments of that principal type constructor
+@c satisfy the type parameter variance restrictions below.
+@c @end itemize
+
 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
-(@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.
+@itemize @bullet
+@item
+@samp{FromType} and @samp{ToType} are both discriminated union types;
+@c XXX It should be possible to extend this to allow both to be tuples
+@c of equal arities, by simply requiring each tuple arg to be coercable.
+@item
+@samp{lift_to_base(FromType)} and @samp{lift_to_base(ToType)}
+have the same type constructor, being e.g.
+@samp{base_tc(BaseFromArgType1, ..., BaseFromArgTypen)} and
+@samp{base_tc(BaseToArgType1, ..., BaseToArgTypen)} respectively,
+with the type parameters of the type constructor
+@samp{base_tc} in its declaration being @samp{BP1, ..., BPn};
+@item
+for all @var{i} in @samp{1..n} where @samp{BPi} must be invariant,
+@samp{BaseFromArgTypei} is identical to @samp{BaseToArgTypei}; and
+@c XXX Should we instead phrase this as
+@c "where the i'th parameter of base_tc must be invariant"?
+@item
+for all @var{i} in @samp{1..n} where @samp{BPi} need not be invariant,
+@samp{BaseFromArgTypei} is coercable to @samp{BaseToArgTypei}.
+@c XXX "coercable" is probably not the best name for this concept.
+@c Alternatives may be phrases like "related by subtyping".
+@end itemize
+
+The last two conditions raise two new questions.
+Given a base type constructor, which of its parameters must be invariant?
+And what does it mean for one type to be coercable to another type?
+
+@heading Must-be-invariant type parameters
+
+A base type must be a discriminated union type,
+which means its definition must have the form
+
+@example
+:- type base_tc(BP1, ..., BPn)
+    --->    f1(T11, ...)
+    ;       ...
+    ;       fm(Tm1, ...).
+@end example
+
+The parameter types @samp{BP1} ... @samp{BPn} 
+will typically occur in one or more of the @samp{Tij},
+where @var{i} is in @samp{1..m}, and
+the value of @var{j} after a given value of @var{i}
+must be between 1 and the arity of @samp{fi}.
+(It is also possible, though rare, for some @samp{BPk}
+to occur in none of the @samp{Tij}.)
+
+Parameter @var{k} of @samp{base_tc} must be invariant
+if and only if @samp{BPk} occurs in one or more of the @samp{Tij}
+for which any of the following holds:
+
+@itemize @bullet
+
+@item
+@samp{Tij} is a higher order type;
+
+@item
+@samp{Tij} is a discriminated union type
+whose type constructor is @samp{base_tc},
+but whose arguments differ from the type constructor's parameter list,
+(meaning that it is any type other than
+@samp{base_tc(BP1, ..., BPn)});
+
+@item
+@samp{Tij} is a discriminated union type
+whose type constructor is not @samp{base_tc},
+but that type constructor is not known to have
+an empty list of must-be-invariant type parameters; or
+
+@item
+@samp{Tij} is a foreign type, a solver type, or an abstract type.
+@c XXX We should not mention solver types if they cannot occur
+@c in du types, but I (zs) don't know whether they can occur or not.
+@c XXX We currently make a type parameter must-be-invariant for a foreign type,
+@c but I (zs) don't know the justification for that.
+
+@end itemize
+
+Basically, the reason for requiring @emph{any}
+type paramaters to be invariant,
+and thus saying that the corresponding pairs of argument types
+in @samp{lift_to_base(FromType)} and @samp{lift_to_base(ToType)}
+must be identical, is that
+@itemize @minus
+@item
+the input and output arguments of predicates and functions
+have opposite variance requirements
+(inputs must be contravariant while outputs must be covariant);
+@item
+without guaranteed access to mode information,
+the Mercury typechecker must require all arguments to meet
+both requirements at the same time; and
+@item
+the only way to do so is to require all arguments to be invariant.
+@end itemize
+
+That is the reason for the first bullet point above.
+The reason for the second is that any data constructor argument
+whose type is recursive but does not meet the imposed condition
+(possibly because it includes the parameters in a different order)
+may create a link that says
+"if this specific parameter of @samp{base_tc} must be invariant,
+then another specific parameter must also be invariant",
+and the implications of such links are hard for humans to understand.
+In any case, in the vast majority of definitions of discriminated union types
+either have no recursively-typed arguments,
+or all their recursively-typed arguments
+exactly repeat the type constructor's parameter list.
+@c (Consider the definitions of pretty much all collection types,
+@c such as lists or maps.)
+Therefore in practice,
+the second bullet point rarely requires parameters to be invariant.
+
+The reason for the third bullet point is to allow coercions to happen
+when @samp{base_tc}'s definition includes data constructors with arguments
+whose types have definitions that cannot themselves require invariance.
+(The types bound to their type parameters are a separate question.)
+This rule means that
+e.g.@: an argument type of the form @samp{list(ElemType)} will never require
+any type parameters occurring inside @samp{ElemType} to be invariant,
+due to the @samp{list} type's one parameter not needing to be invariant:
+@example
+:- type list(T)
+    --->    []                  % nil
+    ;       [T | list(T)].      % cons(T, list(T))
+@end example
+
+This rule means that the @samp{one_or_more} type's one parameter
+also does not need to be invariant:
+@example
+:- type one_or_more(T)
+    --->    one_or_more(T, list(T)).
+@end example
+
+The main limitation that this bullet point imposes
+is on mutually recursive sets of type constructors
+that each have one or more parameters.
+(A type constructor obviously has no parameters that must be invariant
+if it has no parameters at all.)
+Consider two such types, say @samp{foo} and @samp{bar}.
+While computing which of @samp{foo}'s parameters must be invariant,
+we cannot already know whether any of @samp{bar}'s parameters must be invariant,
+and vice versa.
+Therefore in practice, this rule says that
+any type parameters that occur in mutually-recursive types
+must be invariant.
+
+The reason for the fourth bullet point,
+as applied to abstract type constructors, is simple.
+If the compiler does not have access to the definition of a type,
+it cannot know whether it contains any cause for requiring
+the type variables occurring in that type to be invariant.
+The only safe way to handle such situations
+is to assume that it does contain such causes.
+
+@c and after replacing the principal type constructors with base types
+@c (@pxref{Subtypes})
+@c the two types have the same type constructor,
+@c and the arguments of the common type constructor
+@c satisfy the type parameter variance restrictions below.
+
+@heading Which types can be coerced to which other types?
+
+ZZZ The rest is to be done once we agree on what to call this concept,
+but the approach I intend to take is
+- to view types as trees,
+- the non-du parts of the tree must be identical in the from-type and to-type,
+- while the du parts need only have a common base type.
+  (After the most recent change, we do not require either S =< T nor T =< S;
+  we require only S =< B and T =< B.)
 
 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.
 
 Furthermore,