[m-rev.] for review: Announce subtypes and coerce.

[Peter Wang]

NEWS:
    As above.

doc/reference_manual.texi:
    Uncomment documentation for coerce.

diff --git a/NEWS b/NEWS
index 058e00662..ead462b39 100644
--- a/NEWS
+++ b/NEWS
@@ -341,6 +341,9 @@ Changes to the Mercury standard library
 Changes to the Mercury language
 -------------------------------
 
+* The type system now supports subtypes, which work in tandem with
+  type conversion expressions ("coerce").
+
 * The compiler can implement tabling only when generating C code.
   When compiling a predicate that has a `pragma memo` specified for it
   in a non-C grade, it necessarily ignores the pragma, but normally
diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
index 47f1e0507..bf3717947 100644
--- a/doc/reference_manual.texi
+++ b/doc/reference_manual.texi
@@ -99,7 +99,7 @@ into another language, under the above conditions for modified versions.
 * Type classes::      Constrained polymorphism.
 * Existential types:: Support for data abstraction and heterogeneous
                       collections.
- at c * Type conversions::  Converting between subtypes and supertypes.
+* Type conversions::  Converting between subtypes and supertypes.
 * Exception handling:: Catching exceptions to recover from exceptional
                       situations.
 * Semantics::         Declarative and operational semantics of Mercury
@@ -1639,7 +1639,7 @@ or an explicit type qualification.
 * Lambda expressions::
 * Higher-order function applications::
 * Explicit type qualification::
- at c * Type conversion expressions::
+* Type conversion expressions::
 @end menu
 
 @node Data-functors
@@ -1970,18 +1970,18 @@ or equivalently, as it is more commonly written,
 @var{Term} `with_type` @var{Type}
 @end example
 
- at c @node Type conversion expressions
- at c @subsection Type conversion expressions
+ at node Type conversion expressions
+ at subsection Type conversion expressions
 
- at c A type conversion expression is a term of the form:
+A type conversion expression is a term of the form:
 
- at c @example
- at c coerce(Term)
- at c @end example
+ at example
+coerce(Term)
+ at end example
 
- at c @var{Term} must be a valid data-term.
+ at var{Term} must be a valid data-term.
 
- at c @xref{Type conversions}.
+ at xref{Type conversions}.
 
 @node Variable scoping
 @section Variable scoping
@@ -2520,8 +2520,8 @@ or as equivalence types.
 A subtype is a discriminated union type
 that is a subset of a supertype,
 in that every term of a subtype is a valid term in the supertype.
- at c It is possible to convert terms between subtype and supertype
- at c using type conversion expressions (@pxref{Type conversions}).
+It is possible to convert terms between subtype and supertype
+using type conversion expressions (@pxref{Type conversions}).
 
 A subtype is defined using the form
 @example
@@ -7083,201 +7083,203 @@ good_example3_univ("bar"::in(bound("bar")), univ("blah")::out).
 
 @c -----------------------------------------------------------------------
 
- at c @node Type conversions
- at c @chapter Type conversions
- at c
- at c A term may be converted from one type @var{FromType}
- at c to another type @var{ToType}
- at c using a type conversion expression of the form:
- at c
- at c @example
- at c coerce(@var{Term})
- at c @end example
- at c
- at c The expression is type-correct iff
- at c @var{FromType} and @var{ToType} are both discriminated union types,
- at c and after replacing the principal type constructors with base types
- at c (@pxref{Subtypes})
- at c the two types have the same type constructor,
- at c and the arguments of the common type constructor
- at c satisfy the type parameter variance restrictions below.
- at c
- at c Let @var{FromType} expand out to @samp{base(S1, ..., Sn)}
- at c and @var{ToType} expand out to @samp{base(T1, ..., Tn)},
- at c where @samp{base(B1, ..., Bn)} is the common base type,
- at c and @var{Bi} is the i'th type parameter,
- at c which is bound to @var{Si} in @var{FromType}
- at c and @var{Ti} in @var{ToType}.
- at c
- at c For each pair of corresponding type arguments,
- at c one of the following must be true:
- at c @itemize
- at c @item
- at c @samp{Si = Ti}
- at c if the two types are the same
- at c
- at c @item
- at c @samp{Si < Ti}
- at c if @var{Si} is a subtype of @var{Ti},
- at c according to visible subtype definitions
- at c
- at c @item
- at c @samp{Ti < Si}
- at c if @var{Ti} is a subtype of @var{Si},
- at c according to visible subtype definitions
- at c @end itemize
- at c
- at c Otherwise, the coerce expression is not type-correct.
- at c @c NOTE: we deliberately disallow coercion between arbitrary phantom types.
- at c
- at c Furthermore,
- at c @samp{Si = Ti} must be true
- at c if @var{Bi} occurs in one or more of these locations
- at c in the @samp{base/n} type definition:
- at c
- at c @itemize
- at c @item
- at c in a higher order type
- at c
- at c @item
- at c in a foreign type
- at c
- at c @item
- at c in an abstract type
- at c
- at c @item
- at c in a solver type
- at c
- at c @item
- at c in a discriminated union type,
- at c other than a recursive type of the exact form @samp{base(B1, ..., Bn)}
- at c @end itemize
- at c
- at c @heading Mode checking
- at c
- at c Type conversion expressions must also be mode-correct.
- at c For an expression where:
- at c
- at c @itemize @bullet
- at c @item
- at c the input has type @samp{s},
- at c initial inst @var{InitialX},
- at c and final inst @var{FinalX}
- at c
- at c @item
- at c the result has type @samp{t},
- at c initial inst @var{InitialY},
- at c and final inst @var{FinalY}
- at c @end itemize
- at c
- at c @noindent
- at c the type conversion expression is mode-correct iff:
- at c
- at c @itemize @bullet
- at c @item
- at c @var{InitialX} is a ground inst
- at c
- at c @item
- at c @var{InitialY} is free
- at c
- at c @item
- at c @var{FinalX} is @var{InitialX}
- at c
- at c @item
- at c @var{FinalY} is
- at c the abstract unification of
- at c @var{InitialX} and the
- at c @code{bound} instantiatedness tree derived from @samp{t},
- at c and @var{FinalY} does not approximate any term
- at c that is invalid in @samp{t}.
- at c @end itemize
- at c
- at c The @code{bound} instantiatedness tree for @samp{t}
- at c is derived by producing a @code{bound} node
- at c containing each possible constructor of @samp{t},
- at c where the arguments of each bound functor
- at c are also @code{bound} instantiatedness trees.
- at c Where a constructor argument type is not a discriminated union or tuple type,
- at c or if the argument is a recursive node in the type tree,
- at c the inst of the argument is replaced with @code{ground}.
- at c
- at c The abstract unification of two instantiation states
- at c is the abstract equivalent of the unification on terms.
- at c It is defined in
- at c @cite{Precise and Expressive Mode Systems for Typed Logic Programming
- at c Languages} by David Overton. @xref{[6]}.
- at c
- at c Intuitively,
- at c coercing a ground term from a subtype to a supertype is safe,
- at c but coercing a term from a supertype to a subtype
- at c is safe only if
- at c the inst of the term being coerced
- at c indicates that the term would also be valid in the subtype.
- at c
- at c @heading Examples
- at c
- at c Assume we have:
- at c
- at c @example
- at c :- type fruit
- at c    --->    apple
- at c    ;       lemon
- at c    ;       orange.
- at c
- at c :- type citrus =< fruit
- at c    --->    lemon
- at c    ;       orange.
- at c @end example
- at c
- at c This function is type and mode-correct:
- at c
- at c @example
- at c :- func f1(citrus) = fruit.
- at c
- at c f1(X) = coerce(X).
- at c @end example
- at c
- at c This function is type-correct but not mode-correct
- at c because some @code{fruit}s are not @code{citrus}:
- at c
- at c @example
- at c :- func f2(fruit) = citrus.
- at c
- at c f2(X) = coerce(X).  % incorrect
- at c @end example
- at c
- at c This function is mode-correct
- at c because the initial inst of the input argument
- at c limits the range of @code{fruit} values
- at c to those that would also be valid in @code{citrus}:
- at c
- at c @example
- at c :- inst citrus for fruit/0
- at c     --->    lemon
- at c     ;       orange.
- at c
- at c :- func f3(fruit) = citrus.
- at c :- mode f3(in(citrus)) = out is det.
- at c
- at c f3(X) = coerce(X).
- at c @end example
- at c
- at c Finally,
- at c this function is type-incorrect because
- at c in the coerce expression,
- at c the type parameter @var{T} of @code{wrap/1}
- at c is bound to @code{fruit} in the input type,
- at c but @code{citrus} in the result type.
- at c
- at c @example
- at c :- type wrap(T)
- at c     --->    wrap(T).
- at c
- at c :- func f4(func(fruit) = int) = (func(citrus) = int).
- at c
- at c f4(X) = Y :-
- at c     wrap(Y) = coerce(wrap(X)).  % incorrect
- at c @end example
+ at node Type conversions
+ at chapter Type conversions
+
+(This is a new and experimental feature, subject to change.)
+
+A term may be converted from one type @var{FromType}
+to another type @var{ToType}
+using a type conversion expression of the form:
+
+ at example
+coerce(@var{Term})
+ at end example
+
+The expression is type-correct iff
+ at 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.
+
+Let @var{FromType} expand out to @samp{base(S1, ..., Sn)}
+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}.
+
+For each pair of corresponding type arguments,
+one of the following must be true:
+ at itemize
+ at item
+ at samp{Si = Ti}
+if the two types are the same
+
+ at item
+ at samp{Si < Ti}
+if @var{Si} is a subtype of @var{Ti},
+according to visible subtype definitions
+
+ at item
+ at samp{Ti < Si}
+if @var{Ti} is a subtype of @var{Si},
+according to visible subtype definitions
+ at end itemize
+
+Otherwise, the coerce expression is not type-correct.
+ at c NOTE: we deliberately disallow coercion between arbitrary phantom types.
+
+Furthermore,
+ at samp{Si = Ti} must be true
+if @var{Bi} occurs in one or more of these locations
+in the @samp{base/n} type definition:
+
+ at itemize
+ at item
+in a higher order type
+
+ at item
+in a foreign type
+
+ at item
+in an abstract type
+
+ at item
+in a solver type
+
+ at item
+in a discriminated union type,
+other than a recursive type of the exact form @samp{base(B1, ..., Bn)}
+ at end itemize
+
+ at heading Mode checking
+
+Type conversion expressions must also be mode-correct.
+For an expression where:
+
+ at itemize @bullet
+ at item
+the input has type @samp{s},
+initial inst @var{InitialX},
+and final inst @var{FinalX}
+
+ at item
+the result has type @samp{t},
+initial inst @var{InitialY},
+and final inst @var{FinalY}
+ at end itemize
+
+ at noindent
+the type conversion expression is mode-correct iff:
+
+ at itemize @bullet
+ at item
+ at var{InitialX} is a ground inst
+
+ at item
+ at var{InitialY} is free
+
+ at item
+ at var{FinalX} is @var{InitialX}
+
+ at item
+ at var{FinalY} is
+the abstract unification of
+ at var{InitialX} and the
+ at code{bound} instantiatedness tree derived from @samp{t},
+and @var{FinalY} does not approximate any term
+that is invalid in @samp{t}.
+ at end itemize
+
+The @code{bound} instantiatedness tree for @samp{t}
+is derived by producing a @code{bound} node
+containing each possible constructor of @samp{t},
+where the arguments of each bound functor
+are also @code{bound} instantiatedness trees.
+Where a constructor argument type is not a discriminated union or tuple type,
+or if the argument is a recursive node in the type tree,
+the inst of the argument is replaced with @code{ground}.
+
+The abstract unification of two instantiation states
+is the abstract equivalent of the unification on terms.
+It is defined in
+ at cite{Precise and Expressive Mode Systems for Typed Logic Programming
+Languages} by David Overton. @xref{[6]}.
+
+Intuitively,
+coercing a ground term from a subtype to a supertype is safe,
+but coercing a term from a supertype to a subtype
+is safe only if
+the inst of the term being coerced
+indicates that the term would also be valid in the subtype.
+
+ at heading Examples
+
+Assume we have:
+
+ at example
+:- type fruit
+   --->    apple
+   ;       lemon
+   ;       orange.
+
+:- type citrus =< fruit
+   --->    lemon
+   ;       orange.
+ at end example
+
+This function is type and mode-correct:
+
+ at example
+:- func f1(citrus) = fruit.
+
+f1(X) = coerce(X).
+ at end example
+
+This function is type-correct but not mode-correct
+because some @code{fruit}s are not @code{citrus}:
+
+ at example
+:- func f2(fruit) = citrus.
+
+f2(X) = coerce(X).  % incorrect
+ at end example
+
+This function is mode-correct
+because the initial inst of the input argument
+limits the range of @code{fruit} values
+to those that would also be valid in @code{citrus}:
+
+ at example
+:- inst citrus for fruit/0
+    --->    lemon
+    ;       orange.
+
+:- func f3(fruit) = citrus.
+:- mode f3(in(citrus)) = out is det.
+
+f3(X) = coerce(X).
+ at end example
+
+Finally,
+this function is type-incorrect because
+in the coerce expression,
+the type parameter @var{T} of @code{wrap/1}
+is bound to @code{fruit} in the input type,
+but @code{citrus} in the result type.
+
+ at example
+:- type wrap(T)
+    --->    wrap(T).
+
+:- func f4(func(fruit) = int) = (func(citrus) = int).
+
+f4(X) = Y :-
+    wrap(Y) = coerce(wrap(X)).  % incorrect
+ at end example
 
 @c -----------------------------------------------------------------------
 
-- 
2.30.0