[m-rev.] for review: Parse and check subtype definitions.

Peter Wang novalazy at gmail.com
Mon Feb 15 17:57:25 AEDT 2021


(Note that I changed the documentation a fair bit since I originally
posted it.)

-----

This is the first step towards implementing a subtypes feature.
It introduces type definitions of the form

    :- type subtype =< supertype ---> body.

Later, terms of a subtype should share a data representation with their
supertype, and it will be possible to convert terms between two types
that share "base types" using a coerce operation.

doc/reference_manual.texi:
    Add documentation for subtypes.

    Add documentation for a proposed `coerce' operation, commented out
    for now.

    Add "=<" to the list of reserved type names.

compiler/hlds_data.m:
    Add supertype field to hlds_du_type.

compiler/prog_data.m:
    Add du_supertype field to type_details_du.

    Add comment for future work.

compiler/parse_type_defn.m:
    Parse subtype definitions.

    Check that variables which occur in the "=< supertype" part
    also occur on the left hand side of the subtype definition.

compiler/parse_type_name.m:
    Add a new context for why_no_ho_inst_info.

    Add "=<" to is_known_type_name, i.e. prevent the user from defining
    a type of that name (any longer).

compiler/add_type.m:
    Rename add_du_ctors_check_foreign_type_for_cur_backend to
    add_du_ctors_check_subtype_check_foreign_type.

    In add_du_ctors_check_subtype_check_foreign_type, check that
    subtype definitions satisfy the conditions documented in the
    reference manual.

compiler/make_hlds_passes.m:
    Conform to previous renaming.

compiler/comp_unit_interface.m:
    Follow supertypes when computing the required type constructors
    whose definitions need to be kept in the implementation section
    of a .int file.

compiler/equiv_type.m:
compiler/equiv_type_hlds.m:
    Replace equivalence types in supertypes.

compiler/module_qual.qualify_items.m:
    Perform module qualification in supertypes.

compiler/hlds_out_module.m:
    Write out the "=< supertype" part of subtype definitions.

compiler/parse_tree_out.m:
    Write out the "=< supertype" part of subtype definitions.

compiler/recompilation.usage.m:
    Follow supertypes when finding used items.

compiler/add_foreign_enum.m:
compiler/add_special_pred.m:
compiler/check_parse_tree_type_defns.m:
compiler/check_typeclass.m:
compiler/code_info.m:
compiler/dead_proc_elim.m:
compiler/decide_type_repn.m:
compiler/det_report.m:
compiler/direct_arg_in_out.m:
compiler/du_type_layout.m:
compiler/foreign.m:
compiler/inst_check.m:
compiler/intermod.m:
compiler/ml_type_gen.m:
compiler/ml_unify_gen_test.m:
compiler/ml_unify_gen_util.m:
compiler/post_term_analysis.m:
compiler/prog_type.m:
compiler/recompilation.check.m:
compiler/resolve_unify_functor.m:
compiler/simplify_goal_ite.m:
compiler/switch_util.m:
compiler/table_gen.m:
compiler/term_norm.m:
compiler/type_ctor_info.m:
compiler/type_util.m:
compiler/unify_proc.m:
compiler/unused_imports.m:
compiler/xml_documentation.m:
    Conform to HLDS changes.

    Add comments for future work.

tests/invalid/Mmakefile:
tests/invalid/subtype_abstract.err_exp:
tests/invalid/subtype_abstract.m:
tests/invalid/subtype_circular.err_exp:
tests/invalid/subtype_circular.m:
tests/invalid/subtype_ctor_arg.err_exp:
tests/invalid/subtype_ctor_arg.m:
tests/invalid/subtype_eqv.err_exp:
tests/invalid/subtype_eqv.m:
tests/invalid/subtype_exist_constraints.err_exp:
tests/invalid/subtype_exist_constraints.m:
tests/invalid/subtype_exist_vars.err_exp:
tests/invalid/subtype_exist_vars.m:
tests/invalid/subtype_foreign.err_exp:
tests/invalid/subtype_foreign.m:
tests/invalid/subtype_foreign_supertype.err_exp:
tests/invalid/subtype_foreign_supertype.m:
tests/invalid/subtype_foreign_supertype2.err_exp:
tests/invalid/subtype_foreign_supertype2.err_exp2:
tests/invalid/subtype_foreign_supertype2.m:
tests/invalid/subtype_ho.err_exp:
tests/invalid/subtype_ho.m:
tests/invalid/subtype_invalid_supertype.err_exp:
tests/invalid/subtype_invalid_supertype.m:
tests/invalid/subtype_not_subset.err_exp:
tests/invalid/subtype_not_subset.m:
tests/invalid/subtype_syntax.err_exp:
tests/invalid/subtype_syntax.m:
tests/invalid_submodules/Mercury.options:
tests/invalid_submodules/Mmakefile:
tests/invalid_submodules/subtype_submodule.err_exp:
tests/invalid_submodules/subtype_submodule.m:
tests/valid/Mmakefile:
tests/valid/subtype_basic.m:
    Add test cases.
---
 compiler/add_foreign_enum.m                   |  15 +-
 compiler/add_special_pred.m                   |   5 +-
 compiler/add_type.m                           | 822 +++++++++++++++++-
 compiler/check_parse_tree_type_defns.m        |   4 +-
 compiler/check_typeclass.m                    |   6 +-
 compiler/code_info.m                          |   2 +-
 compiler/comp_unit_interface.m                |  34 +-
 compiler/dead_proc_elim.m                     |   3 +-
 compiler/decide_type_repn.m                   |  10 +-
 compiler/det_report.m                         |   4 +-
 compiler/direct_arg_in_out.m                  |   5 +-
 compiler/du_type_layout.m                     |  22 +-
 compiler/equiv_type.m                         |  15 +-
 compiler/equiv_type_hlds.m                    |  24 +-
 compiler/foreign.m                            |   2 +-
 compiler/hlds_data.m                          |   5 +-
 compiler/hlds_out_module.m                    |  13 +-
 compiler/inst_check.m                         |   6 +-
 compiler/intermod.m                           |  17 +-
 compiler/make_hlds_passes.m                   |  12 +-
 compiler/ml_type_gen.m                        |   4 +-
 compiler/ml_unify_gen_test.m                  |   2 +-
 compiler/ml_unify_gen_util.m                  |   3 +-
 compiler/module_qual.qualify_items.m          |  19 +-
 compiler/parse_tree_out.m                     |  11 +-
 compiler/parse_type_defn.m                    | 174 +++-
 compiler/parse_type_name.m                    |   8 +-
 compiler/post_term_analysis.m                 |   2 +-
 compiler/prog_data.m                          |   7 +-
 compiler/prog_type.m                          |   7 +-
 compiler/recompilation.check.m                |   2 +-
 compiler/recompilation.usage.m                |   8 +-
 compiler/resolve_unify_functor.m              |   2 +-
 compiler/simplify_goal_ite.m                  |   4 +-
 compiler/switch_util.m                        |   4 +-
 compiler/table_gen.m                          |   5 +-
 compiler/term_norm.m                          |   2 +-
 compiler/type_ctor_info.m                     |   6 +-
 compiler/type_util.m                          |  22 +-
 compiler/unify_proc.m                         |   6 +-
 compiler/unused_imports.m                     |   2 +-
 compiler/xml_documentation.m                  |   4 +-
 doc/reference_manual.texi                     | 283 +++++-
 tests/invalid/Mmakefile                       |  13 +
 tests/invalid/subtype_abstract.err_exp        |   5 +
 tests/invalid/subtype_abstract.m              |  30 +
 tests/invalid/subtype_circular.err_exp        |   3 +
 tests/invalid/subtype_circular.m              |  18 +
 tests/invalid/subtype_ctor_arg.err_exp        |  10 +
 tests/invalid/subtype_ctor_arg.m              |  44 +
 tests/invalid/subtype_eqv.err_exp             |   4 +
 tests/invalid/subtype_eqv.m                   |  30 +
 .../invalid/subtype_exist_constraints.err_exp |   8 +
 tests/invalid/subtype_exist_constraints.m     |  26 +
 tests/invalid/subtype_exist_vars.err_exp      |   8 +
 tests/invalid/subtype_exist_vars.m            |  31 +
 tests/invalid/subtype_foreign.err_exp         |   9 +
 tests/invalid/subtype_foreign.m               |  19 +
 .../invalid/subtype_foreign_supertype.err_exp |   2 +
 tests/invalid/subtype_foreign_supertype.m     |  19 +
 .../subtype_foreign_supertype2.err_exp        |   2 +
 .../subtype_foreign_supertype2.err_exp2       |   2 +
 tests/invalid/subtype_foreign_supertype2.m    |  20 +
 tests/invalid/subtype_ho.err_exp              |  26 +
 tests/invalid/subtype_ho.m                    |  36 +
 .../invalid/subtype_invalid_supertype.err_exp |  15 +
 tests/invalid/subtype_invalid_supertype.m     |  24 +
 tests/invalid/subtype_not_subset.err_exp      |   6 +
 tests/invalid/subtype_not_subset.m            |  17 +
 tests/invalid/subtype_syntax.err_exp          |  28 +
 tests/invalid/subtype_syntax.m                |  42 +
 tests/invalid_submodules/Mercury.options      |   1 +
 tests/invalid_submodules/Mmakefile            |   1 +
 .../subtype_submodule.err_exp                 |   3 +
 tests/invalid_submodules/subtype_submodule.m  |  32 +
 tests/valid/Mmakefile                         |   1 +
 tests/valid/subtype_basic.m                   |  48 +
 77 files changed, 2024 insertions(+), 172 deletions(-)
 create mode 100644 tests/invalid/subtype_abstract.err_exp
 create mode 100644 tests/invalid/subtype_abstract.m
 create mode 100644 tests/invalid/subtype_circular.err_exp
 create mode 100644 tests/invalid/subtype_circular.m
 create mode 100644 tests/invalid/subtype_ctor_arg.err_exp
 create mode 100644 tests/invalid/subtype_ctor_arg.m
 create mode 100644 tests/invalid/subtype_eqv.err_exp
 create mode 100644 tests/invalid/subtype_eqv.m
 create mode 100644 tests/invalid/subtype_exist_constraints.err_exp
 create mode 100644 tests/invalid/subtype_exist_constraints.m
 create mode 100644 tests/invalid/subtype_exist_vars.err_exp
 create mode 100644 tests/invalid/subtype_exist_vars.m
 create mode 100644 tests/invalid/subtype_foreign.err_exp
 create mode 100644 tests/invalid/subtype_foreign.m
 create mode 100644 tests/invalid/subtype_foreign_supertype.err_exp
 create mode 100644 tests/invalid/subtype_foreign_supertype.m
 create mode 100644 tests/invalid/subtype_foreign_supertype2.err_exp
 create mode 100644 tests/invalid/subtype_foreign_supertype2.err_exp2
 create mode 100644 tests/invalid/subtype_foreign_supertype2.m
 create mode 100644 tests/invalid/subtype_ho.err_exp
 create mode 100644 tests/invalid/subtype_ho.m
 create mode 100644 tests/invalid/subtype_invalid_supertype.err_exp
 create mode 100644 tests/invalid/subtype_invalid_supertype.m
 create mode 100644 tests/invalid/subtype_not_subset.err_exp
 create mode 100644 tests/invalid/subtype_not_subset.m
 create mode 100644 tests/invalid/subtype_syntax.err_exp
 create mode 100644 tests/invalid/subtype_syntax.m
 create mode 100644 tests/invalid_submodules/subtype_submodule.err_exp
 create mode 100644 tests/invalid_submodules/subtype_submodule.m
 create mode 100644 tests/valid/subtype_basic.m

diff --git a/compiler/add_foreign_enum.m b/compiler/add_foreign_enum.m
index a3947425f..31b3d88e8 100644
--- a/compiler/add_foreign_enum.m
+++ b/compiler/add_foreign_enum.m
@@ -204,9 +204,12 @@ add_pragma_foreign_enum(ModuleInfo, ImsItem, !TypeCtorForeignEnumMap,
                 report_not_du_type(Context, ContextPieces,
                     TypeSymName, TypeArity, TypeBody, !Specs)
             ;
-                TypeBody = hlds_du_type(Ctors, _MaybeUserEq, MaybeRepn,
-                    _IsForeignType),
-                expect(unify(MaybeRepn, no), $pred, "MaybeRepn != no"),
+                TypeBody = hlds_du_type(Ctors, MaybeSuperType, _MaybeUserEq,
+                    MaybeRepn, _IsForeignType),
+                expect(unify(MaybeSuperType, no), $pred,
+                    "MaybeSuperType != no"),
+                expect(unify(MaybeRepn, no), $pred,
+                    "MaybeRepn != no"),
 
                 MercuryForeignTagPairs =
                     one_or_more_to_list(OoMMercuryForeignTagPairs),
@@ -339,8 +342,10 @@ add_pragma_foreign_export_enum(ItemForeignExportEnum, !ModuleInfo,
                 report_not_du_type(Context, ContextPieces,
                     TypeSymName, TypeArity, TypeBody, !Specs)
             ;
-                TypeBody = hlds_du_type(Ctors, _MaybeUserEq, MaybeRepn,
-                    _IsForeignType),
+                TypeBody = hlds_du_type(Ctors, MaybeSuperType, _MaybeUserEq,
+                    MaybeRepn, _IsForeignType),
+                expect(unify(MaybeSuperType, no), $pred,
+                    "MaybeSuperType != no"),
                 (
                     MaybeRepn = no,
                     unexpected($pred, "MaybeRepn = no")
diff --git a/compiler/add_special_pred.m b/compiler/add_special_pred.m
index 040f5e7ef..b681cbfc7 100644
--- a/compiler/add_special_pred.m
+++ b/compiler/add_special_pred.m
@@ -502,10 +502,11 @@ collect_type_defn_for_tuple(TypeCtor, Type, TVarSet, TypeBody, Context) :-
     DirectArgCtors = no,
     Repn = du_type_repn([CtorRepn], ConsCtorMap, no_cheaper_tag_test,
         du_type_kind_general, DirectArgCtors),
+    MaybeSuperType = no,
     MaybeCanonical = canon,
     IsForeign = no,
-    TypeBody = hlds_du_type(one_or_more(Ctor, []), MaybeCanonical,
-        yes(Repn), IsForeign),
+    TypeBody = hlds_du_type(one_or_more(Ctor, []), MaybeSuperType,
+        MaybeCanonical, yes(Repn), IsForeign),
     construct_type(TypeCtor, TupleArgTypes, Type),
 
     term.context_init(Context).
diff --git a/compiler/add_type.m b/compiler/add_type.m
index 1c84127b3..7e1508331 100644
--- a/compiler/add_type.m
+++ b/compiler/add_type.m
@@ -2,6 +2,7 @@
 % vim: ft=mercury ts=4 sw=4 et
 %---------------------------------------------------------------------------%
 % Copyright (C) 1993-2011 The University of Melbourne.
+% Copyright (C) 2013-2021 The Mercury team.
 % This file may only be copied under the terms of the GNU General
 % Public License - see the file COPYING in the Mercury distribution.
 %---------------------------------------------------------------------------%
@@ -36,11 +37,12 @@
     list(error_spec)::in, list(error_spec)::out) is det.
 
     % Add the constructors of du types to the constructor table of the HLDS,
-    % and check that Mercury types defined solely by foreign types
-    % have a definition that works for the target backend.
+    % check subtype definitions, and check that Mercury types defined solely
+    % by foreign types have a definition that works for the target backend.
     %
-:- pred add_du_ctors_check_foreign_type_for_cur_backend(type_ctor::in,
-    hlds_type_defn::in, found_invalid_type::in, found_invalid_type::out,
+:- pred add_du_ctors_check_subtype_check_foreign_type(type_table::in,
+    type_ctor::in, hlds_type_defn::in,
+    found_invalid_type::in, found_invalid_type::out,
     module_info::in, module_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
@@ -58,10 +60,13 @@
 :- import_module libs.globals.
 :- import_module libs.op_mode.
 :- import_module mdbcomp.
+:- import_module mdbcomp.builtin_modules.
 :- import_module mdbcomp.sym_name.
+:- import_module parse_tree.mercury_to_mercury.
 :- import_module parse_tree.module_qual.
 :- import_module parse_tree.prog_out.
 :- import_module parse_tree.prog_type.
+:- import_module parse_tree.prog_type_subst.
 
 :- import_module bool.
 :- import_module int.
@@ -70,8 +75,13 @@
 :- import_module multi_map.
 :- import_module one_or_more.
 :- import_module require.
+:- import_module set.
 :- import_module string.
 :- import_module term.
+:- import_module unit.
+
+:- inst hlds_type_body_du for hlds_type_body/0
+    --->    hlds_du_type(ground, ground, ground, ground, ground).
 
 %---------------------------------------------------------------------------%
 %
@@ -101,7 +111,7 @@ module_add_type_defn(TypeStatus0, NeedQual, ItemTypeDefnInfo,
         (
             Body = hlds_abstract_type(_)
         ;
-            Body = hlds_du_type(_, _, _, _),
+            Body = hlds_du_type(_, _, _, _, _),
             string.suffix(term.context_file(Context), ".int2")
             % If the type definition comes from a .int2 file then we must
             % treat it as abstract. The constructors may only be used
@@ -415,11 +425,12 @@ convert_type_defn_to_hlds(TypeDefn, TypeCtor, HLDSBody, !ModuleInfo) :-
     (
         TypeDefn = parse_tree_du_type(DetailsDu),
         DetailsDu =
-            type_details_du(Ctors, MaybeUserEqComp, MaybeDirectArgCtors),
+            type_details_du(MaybeSuperType, Ctors, MaybeUserEqComp,
+                MaybeDirectArgCtors),
         MaybeRepn = no,
         MaybeForeign = no,
-        HLDSBody = hlds_du_type(Ctors, MaybeUserEqComp, MaybeRepn,
-            MaybeForeign),
+        HLDSBody = hlds_du_type(Ctors, MaybeSuperType, MaybeUserEqComp,
+            MaybeRepn, MaybeForeign),
         (
             MaybeDirectArgCtors = no
         ;
@@ -531,11 +542,11 @@ combine_old_and_new_type_status(OldDefn, NewTypeStatus, CombinedTypeStatus,
 merge_maybe_foreign_type_bodies(Globals, BodyA, BodyB, Body) :-
     (
         BodyA = hlds_foreign_type(ForeignTypeBodyA),
-        BodyB = hlds_du_type(_, _, _, _),
+        BodyB = hlds_du_type(_, _, _, _, _),
         merge_foreign_and_du_type_bodies(Globals, ForeignTypeBodyA, BodyB,
             Body)
     ;
-        BodyA = hlds_du_type(_, _, _, _),
+        BodyA = hlds_du_type(_, _, _, _, _),
         BodyB = hlds_foreign_type(ForeignTypeBodyB),
         merge_foreign_and_du_type_bodies(Globals, ForeignTypeBodyB, BodyA,
             Body)
@@ -547,17 +558,15 @@ merge_maybe_foreign_type_bodies(Globals, BodyA, BodyB, Body) :-
         Body = hlds_foreign_type(ForeignTypeBody)
     ).
 
-:- inst hlds_type_body_du for hlds_type_body/0
-    --->    hlds_du_type(ground, ground, ground, ground).
-
 :- pred merge_foreign_and_du_type_bodies(globals::in,
     foreign_type_body::in, hlds_type_body::in(hlds_type_body_du),
     hlds_type_body::out) is semidet.
 
 merge_foreign_and_du_type_bodies(Globals, ForeignTypeBodyA, DuTypeBodyB,
         Body) :-
-    DuTypeBodyB = hlds_du_type(_Ctors, _MaybeUserEq, _MaybeRepn,
-        MaybeForeignTypeBodyB),
+    DuTypeBodyB = hlds_du_type(_Ctors, MaybeSuperTypeB, _MaybeUserEq,
+        _MaybeRepn, MaybeForeignTypeBodyB),
+    MaybeSuperTypeB = no,
     (
         MaybeForeignTypeBodyB = yes(ForeignTypeBodyB)
     ;
@@ -633,7 +642,11 @@ check_for_dummy_type_with_unify_compare(TypeStatus, TypeCtor, DetailsDu,
         % zero-arity constructor are dummy types. Dummy types are not allowed
         % to have user-defined equality or comparison.
 
-        DetailsDu = type_details_du(Ctors, MaybeCanonical, _MaybeDirectArg),
+        % XXX SUBTYPE Do not consider a subtype to be a dummy type
+        % unless the base type is a dummy type.
+
+        DetailsDu = type_details_du(_MaybeSuperType, Ctors, MaybeCanonical,
+            _MaybeDirectArg),
         Ctors = one_or_more(Ctor, []),
         Ctor ^ cons_args = [],
         MaybeCanonical = noncanon(_),
@@ -803,7 +816,7 @@ get_body_is_solver_type(Body, IsSolverType) :-
             IsSolverType = non_solver_type
         )
     ;
-        ( Body = hlds_du_type(_, _, _, _)
+        ( Body = hlds_du_type(_, _, _, _, _)
         ; Body = hlds_eqv_type(_)
         ; Body = hlds_foreign_type(_)
         ),
@@ -896,7 +909,7 @@ do_foreign_type_visibilities_match(OldStatus, NewStatus) :-
 %---------------------------------------------------------------------------%
 %---------------------------------------------------------------------------%
 
-add_du_ctors_check_foreign_type_for_cur_backend(TypeCtor, TypeDefn,
+add_du_ctors_check_subtype_check_foreign_type(TypeTable, TypeCtor, TypeDefn,
         !FoundInvalidType, !ModuleInfo, !Specs) :-
     get_type_defn_context(TypeDefn, Context),
     get_type_defn_tvarset(TypeDefn, TVarSet),
@@ -906,8 +919,20 @@ add_du_ctors_check_foreign_type_for_cur_backend(TypeCtor, TypeDefn,
     get_type_defn_status(TypeDefn, Status),
     get_type_defn_ctors_need_qualifier(TypeDefn, NeedQual),
     (
-        Body = hlds_du_type(OoMCtors, _MaybeUserEqCmp, _MaybeRepn,
-            _MaybeForeign),
+        Body = hlds_du_type(OoMCtors, MaybeSuperType, _MaybeUserEqCmp,
+            _MaybeRepn, _MaybeForeign),
+
+        % Check subtype conditions if this is a subtype definitions.
+        % There is no particular reason to do this here except to
+        % save a pass over the type table.
+        (
+            MaybeSuperType = yes(SuperType),
+            check_subtype_defn(TypeTable, TVarSet, TypeCtor, TypeDefn, Body,
+                SuperType, !FoundInvalidType, !Specs)
+        ;
+            MaybeSuperType = no
+        ),
+
         module_info_get_cons_table(!.ModuleInfo, CtorMap0),
         module_info_get_partial_qualifier_info(!.ModuleInfo, PQInfo),
         module_info_get_ctor_field_table(!.ModuleInfo, CtorFieldMap0),
@@ -1182,6 +1207,763 @@ check_foreign_type_for_current_target(TypeCtor, ForeignTypeBody, PrevErrors,
         FoundInvalidType = found_invalid_type
     ).
 
+%---------------------------------------------------------------------------%
+%---------------------------------------------------------------------------%
+
+:- pred check_subtype_defn(type_table::in, tvarset::in, type_ctor::in,
+    hlds_type_defn::in, hlds_type_body::in(hlds_type_body_du), mer_type::in,
+    found_invalid_type::in, found_invalid_type::out,
+    list(error_spec)::in, list(error_spec)::out) is det.
+
+check_subtype_defn(TypeTable, TVarSet, TypeCtor, TypeDefn, TypeBody, SuperType,
+        !FoundInvalidType, !Specs) :-
+    hlds_data.get_type_defn_status(TypeDefn, OrigTypeStatus),
+    hlds_data.get_type_defn_context(TypeDefn, Context),
+    ( if type_to_ctor_and_args(SuperType, SuperTypeCtor, SuperTypeArgs) then
+        Seen0 = set.make_singleton_set(TypeCtor),
+        search_super_type_ctor_defn(TypeTable, OrigTypeStatus, SuperTypeCtor,
+            SearchRes, Seen0, Seen1),
+        (
+            SearchRes = ok(SuperTypeDefn),
+            check_subtype_defn_2(TypeTable, TypeCtor, TypeDefn, TypeBody,
+                SuperTypeCtor, SuperTypeDefn, SuperTypeArgs, Seen1,
+                !FoundInvalidType, !Specs)
+        ;
+            SearchRes = error(Error),
+            Pieces = supertype_ctor_defn_error_pieces(SuperTypeCtor, Error),
+            Msg = simplest_msg(Context, Pieces),
+            Spec = error_spec($pred, severity_error, phase_parse_tree_to_hlds,
+                [Msg]),
+            !:Specs = [Spec | !.Specs],
+            !:FoundInvalidType = found_invalid_type
+        )
+    else
+        SuperTypeStr = mercury_type_to_string(TVarSet, print_name_only,
+            SuperType),
+        Pieces = [words("Error: expected type constructor in"),
+            words("supertype part of subtype definition, got"),
+            quote(SuperTypeStr), nl],
+        Msg = simplest_msg(Context, Pieces),
+        Spec = error_spec($pred, severity_error, phase_parse_tree_to_hlds,
+            [Msg]),
+        !:Specs = [Spec | !.Specs],
+        !:FoundInvalidType = found_invalid_type
+    ).
+
+:- pred check_subtype_defn_2(type_table::in,
+    type_ctor::in, hlds_type_defn::in, hlds_type_body::in(hlds_type_body_du),
+    type_ctor::in, hlds_type_defn::in, list(mer_type)::in, set(type_ctor)::in,
+    found_invalid_type::in, found_invalid_type::out,
+    list(error_spec)::in, list(error_spec)::out) is det.
+
+check_subtype_defn_2(TypeTable, TypeCtor, TypeDefn, TypeBody,
+        SuperTypeCtor, SuperTypeDefn, SuperTypeArgs, Seen0,
+        !FoundInvalidType, !Specs) :-
+    hlds_data.get_type_defn_context(TypeDefn, Context),
+    hlds_data.get_type_defn_body(SuperTypeDefn, SuperTypeBody),
+    (
+        SuperTypeBody = hlds_du_type(_, _, _, _, IsForeign),
+        (
+            IsForeign = no,
+            check_subtype_defn_3(TypeTable, TypeCtor, TypeDefn, TypeBody,
+                SuperTypeCtor, SuperTypeDefn, SuperTypeBody, SuperTypeArgs,
+                Seen0, !FoundInvalidType, !Specs)
+        ;
+            IsForeign = yes(_),
+            SuperTypeCtor = type_ctor(SymName, Arity),
+            Pieces = [words("Error:"),
+                unqual_sym_name_arity(sym_name_arity(SymName, Arity)),
+                words("cannot be a supertype because it has a"),
+                words("foreign type definition."), nl],
+            Msg = simplest_msg(Context, Pieces),
+            Spec = error_spec($pred, severity_error,
+                phase_parse_tree_to_hlds, [Msg]),
+            !:Specs = [Spec | !.Specs],
+            !:FoundInvalidType = found_invalid_type
+        )
+    ;
+        ( SuperTypeBody = hlds_eqv_type(_)
+        ; SuperTypeBody = hlds_foreign_type(_)
+        ; SuperTypeBody = hlds_solver_type(_)
+        ; SuperTypeBody = hlds_abstract_type(_)
+        ),
+        SuperTypeCtor = type_ctor(SymName, Arity),
+        SuperTypeDesc = describe_hlds_type_body(SuperTypeBody),
+        Pieces = [words("Error:"),
+            unqual_sym_name_arity(sym_name_arity(SymName, Arity)),
+            words("cannot be a supertype because it is"),
+            words(SuperTypeDesc), suffix("."), nl],
+        Msg = simplest_msg(Context, Pieces),
+        Spec = error_spec($pred, severity_error, phase_parse_tree_to_hlds,
+            [Msg]),
+        !:Specs = [Spec | !.Specs],
+        !:FoundInvalidType = found_invalid_type
+    ).
+
+:- pred check_subtype_defn_3(type_table::in,
+    type_ctor::in, hlds_type_defn::in, hlds_type_body::in(hlds_type_body_du),
+    type_ctor::in, hlds_type_defn::in, hlds_type_body::in(hlds_type_body_du),
+    list(mer_type)::in, set(type_ctor)::in,
+    found_invalid_type::in, found_invalid_type::out,
+    list(error_spec)::in, list(error_spec)::out) is det.
+
+check_subtype_defn_3(TypeTable, TypeCtor, TypeDefn, TypeBody,
+        SuperTypeCtor, SuperTypeDefn, SuperTypeBody, SuperTypeArgs,
+        Seen0, !FoundInvalidType, !Specs) :-
+    hlds_data.get_type_defn_status(TypeDefn, TypeStatus),
+    check_subtype_has_base_type(TypeTable, TypeStatus, SuperTypeCtor,
+        SuperTypeDefn, MaybeBaseTypeError, Seen0, _Seen),
+    (
+        MaybeBaseTypeError = ok(unit),
+        check_subtype_ctors(TypeTable, TypeCtor, TypeDefn, TypeBody,
+            SuperTypeCtor, SuperTypeDefn, SuperTypeBody, SuperTypeArgs,
+            !FoundInvalidType, !Specs)
+    ;
+        MaybeBaseTypeError = error(Pieces),
+        (
+            Pieces = []
+        ;
+            Pieces = [_ | _],
+            hlds_data.get_type_defn_context(TypeDefn, Context),
+            Msg = simplest_msg(Context, Pieces),
+            Spec = error_spec($pred, severity_error, phase_parse_tree_to_hlds,
+                [Msg]),
+            !:Specs = [Spec | !.Specs]
+        ),
+        !:FoundInvalidType = found_invalid_type
+    ).
+
+%---------------------%
+
+:- pred check_subtype_has_base_type(type_table::in, type_status::in,
+    type_ctor::in, hlds_type_defn::in,
+    maybe_error(unit, list(format_component))::out,
+    set(type_ctor)::in, set(type_ctor)::out) is det.
+
+check_subtype_has_base_type(TypeTable, OrigTypeStatus, CurTypeCtor,
+        CurTypeDefn, MaybeError, !Seen) :-
+    hlds_data.get_type_defn_body(CurTypeDefn, CurTypeBody),
+    (
+        CurTypeBody = hlds_du_type(_, MaybeSuperType, _, _, IsForeign),
+        (
+            IsForeign = no,
+            MaybeSuperType = no,
+            MaybeError = ok(unit)
+        ;
+            IsForeign = no,
+            MaybeSuperType = yes(SuperType),
+            ( if type_to_ctor_and_args(SuperType, SuperTypeCtor, _) then
+                search_super_type_ctor_defn(TypeTable, OrigTypeStatus,
+                    SuperTypeCtor, SearchRes, !Seen),
+                (
+                    SearchRes = ok(SuperTypeDefn),
+                    check_subtype_has_base_type(TypeTable, OrigTypeStatus,
+                        SuperTypeCtor, SuperTypeDefn, MaybeError, !Seen)
+                ;
+                    SearchRes = error(Error),
+                    Pieces = supertype_ctor_defn_error_pieces(SuperTypeCtor,
+                        Error),
+                    MaybeError = error(Pieces)
+                )
+            else
+                hlds_data.get_type_defn_tvarset(CurTypeDefn, TVarSet),
+                SuperTypeStr = mercury_type_to_string(TVarSet, print_name_only,
+                    SuperType),
+                Pieces = [words("Error:"), quote(SuperTypeStr),
+                    words("is not a discriminated union type."), nl],
+                MaybeError = error(Pieces)
+            )
+        ;
+            IsForeign = yes(_),
+            CurTypeCtor = type_ctor(SymName, Arity),
+            Pieces = [words("Error:"),
+                unqual_sym_name_arity(sym_name_arity(SymName, Arity)),
+                words("has a foreign type definition."), nl],
+            MaybeError = error(Pieces)
+        )
+    ;
+        ( CurTypeBody = hlds_eqv_type(_)
+        ; CurTypeBody = hlds_foreign_type(_)
+        ; CurTypeBody = hlds_solver_type(_)
+        ; CurTypeBody = hlds_abstract_type(_)
+        ),
+        CurTypeCtor = type_ctor(SymName, Arity),
+        CurTypeDesc = describe_hlds_type_body(CurTypeBody),
+        Pieces = [words("Error:"),
+            unqual_sym_name_arity(sym_name_arity(SymName, Arity)),
+            words("is"), words(CurTypeDesc), suffix("."), nl],
+        MaybeError = error(Pieces)
+    ).
+
+:- func describe_hlds_type_body(hlds_type_body) = string.
+
+describe_hlds_type_body(TypeBody) = Desc :-
+    (
+        TypeBody = hlds_du_type(_, _, _, _, _),
+        Desc = "a discriminated union type"
+    ;
+        TypeBody = hlds_eqv_type(_),
+        Desc = "an equivalence type"
+    ;
+        TypeBody = hlds_foreign_type(_),
+        Desc = "a foreign type"
+    ;
+        TypeBody = hlds_solver_type(_),
+        Desc = "a solver type"
+    ;
+        TypeBody = hlds_abstract_type(_),
+        Desc = "an abstract type"
+    ).
+
+%---------------------%
+
+:- type search_type_ctor_defn_error
+    --->    type_is_abstract
+    ;       not_defined
+    ;       circularity_detected.
+
+:- pred search_super_type_ctor_defn(type_table::in, type_status::in,
+    type_ctor::in,
+    maybe_error(hlds_type_defn, search_type_ctor_defn_error)::out,
+    set(type_ctor)::in, set(type_ctor)::out) is det.
+
+search_super_type_ctor_defn(TypeTable, OrigTypeStatus, TypeCtor, Res, !Seen) :-
+    ( if set.insert_new(TypeCtor, !Seen) then
+        ( if search_type_ctor_defn(TypeTable, TypeCtor, TypeDefn) then
+            hlds_data.get_type_defn_status(TypeDefn, TypeStatus),
+            ( if
+                subtype_defn_int_supertype_defn_impl(OrigTypeStatus,
+                    TypeStatus)
+            then
+                Res = error(type_is_abstract)
+            else
+                Res = ok(TypeDefn)
+            )
+        else
+            Res = error(not_defined)
+        )
+    else
+        Res = error(circularity_detected)
+    ).
+
+:- pred subtype_defn_int_supertype_defn_impl(type_status::in, type_status::in)
+    is semidet.
+
+subtype_defn_int_supertype_defn_impl(SubTypeStatus, SuperTypeStatus) :-
+    % If the subtype is defined in the interface section of this module,
+    % then its supertype(s) must not be defined in the implementation section,
+    % i.e. abstractly exported. Other visibility rules are enforced during
+    % module qualification.
+    type_status_defined_in_this_module(SubTypeStatus) = yes,
+    type_status_defined_in_impl_section(SubTypeStatus) = no,
+
+    type_status_defined_in_this_module(SuperTypeStatus) = yes,
+    type_status_defined_in_impl_section(SuperTypeStatus) = yes.
+
+:- func supertype_ctor_defn_error_pieces(type_ctor,
+    search_type_ctor_defn_error) = list(format_component).
+
+supertype_ctor_defn_error_pieces(SuperTypeCtor, Error) = Pieces :-
+    SuperTypeCtor = type_ctor(SymName, Arity),
+    SymNameArity = sym_name_arity(SymName, Arity),
+    (
+        Error = type_is_abstract,
+        Pieces = [words("Error: the type definition for"),
+            unqual_sym_name_arity(SymNameArity),
+            words("is not visible here."), nl]
+    ;
+        Error = not_defined,
+        ( if special_type_ctor_not_du(SuperTypeCtor) then
+            Pieces = [words("Error:"), unqual_sym_name_arity(SymNameArity),
+                words("is not a discriminated union type."), nl]
+        else
+            Pieces = [words("Error: undefined type"),
+                unqual_sym_name_arity(SymNameArity), suffix("."), nl]
+        )
+    ;
+        Error = circularity_detected,
+        Pieces = [words("Error: circularity in subtype definition."), nl]
+    ).
+
+:- pred special_type_ctor_not_du(type_ctor::in) is semidet.
+
+special_type_ctor_not_du(TypeCtor) :-
+    % XXX This could use classify_type_ctor_if_special but that predicate is
+    % currently in check_hlds.
+    (
+        TypeCtor = type_ctor(SymName, Arity),
+        Arity = 0,
+        (
+            SymName = unqualified(TypeName)
+        ;
+            SymName = qualified(mercury_public_builtin_module, TypeName)
+        ),
+        is_builtin_type_name(TypeName)
+    ;
+        type_ctor_is_higher_order(TypeCtor, _, _, _)
+    ;
+        type_ctor_is_tuple(TypeCtor)
+    ).
+
+%---------------------%
+
+:- pred check_subtype_ctors(type_table::in,
+    type_ctor::in, hlds_type_defn::in, hlds_type_body::in(hlds_type_body_du),
+    type_ctor::in, hlds_type_defn::in, hlds_type_body::in(hlds_type_body_du),
+    list(mer_type)::in, found_invalid_type::in, found_invalid_type::out,
+    list(error_spec)::in, list(error_spec)::out) is det.
+
+check_subtype_ctors(TypeTable, _TypeCtor, TypeDefn, TypeBody,
+        SuperTypeCtor, SuperTypeDefn, SuperTypeBody, SuperTypeArgs,
+        !FoundInvalidType, !Specs) :-
+    hlds_data.get_type_defn_tvarset(TypeDefn, TVarSet0),
+    hlds_data.get_type_defn_status(TypeDefn, TypeStatus),
+    hlds_data.get_type_defn_tvarset(SuperTypeDefn, SuperTVarSet),
+    hlds_data.get_type_defn_tparams(SuperTypeDefn, SuperTypeParams0),
+
+    % Merge type variables in the subtype and supertype definitions into a
+    % common tvarset.
+    tvarset_merge_renaming(TVarSet0, SuperTVarSet, NewTVarSet, Renaming),
+    apply_variable_renaming_to_tvar_list(Renaming, SuperTypeParams0,
+        SuperTypeParams),
+
+    % Create a substitution from the supertype's type parameters to the
+    % argument types in the declared supertype part of the subtype definition.
+    map.from_corresponding_lists(SuperTypeParams, SuperTypeArgs, TSubst),
+
+    % Apply the type substitution to the supertype constructors' arguments.
+    SuperTypeBody = hlds_du_type(OoMSuperCtors, _, _, _, _),
+    SuperCtors0 = one_or_more_to_list(OoMSuperCtors),
+    list.map(rename_and_rec_subst_in_constructor(Renaming, TSubst),
+        SuperCtors0, SuperCtors),
+
+    % Check each subtype constructor against the supertype's constructors.
+    TypeBody = hlds_du_type(OoMCtors, _, _, _, _),
+    Ctors = one_or_more_to_list(OoMCtors),
+    foldl2(
+        check_subtype_ctor(TypeTable, NewTVarSet, TypeStatus,
+            SuperTypeCtor, SuperCtors),
+        Ctors, !FoundInvalidType, !Specs).
+
+:- pred check_subtype_ctor(type_table::in, tvarset::in, type_status::in,
+    type_ctor::in, list(constructor)::in, constructor::in,
+    found_invalid_type::in, found_invalid_type::out,
+    list(error_spec)::in, list(error_spec)::out) is det.
+
+check_subtype_ctor(TypeTable, TVarSet, TypeStatus, SuperTypeCtor, SuperCtors,
+        Ctor, !FoundInvalidType, !Specs) :-
+    Ctor = ctor(_, _, CtorName, _, Arity, Context),
+    UnqualCtorName = unqualify_name(CtorName),
+    ( if
+        search_ctor_by_unqual_name(SuperCtors, UnqualCtorName, Arity,
+            SuperCtor)
+    then
+        check_subtype_ctor_2(TypeTable, TVarSet, TypeStatus, Ctor, SuperCtor,
+            !FoundInvalidType, !Specs)
+    else
+        SuperTypeCtor = type_ctor(SuperTypeCtorName, SuperTypeCtorArity),
+        Pieces = [words("Error:"),
+            unqual_sym_name_arity(sym_name_arity(CtorName, Arity)),
+            words("is not a constructor of the supertype"),
+            unqual_sym_name_arity(
+                sym_name_arity(SuperTypeCtorName, SuperTypeCtorArity)),
+            suffix("."), nl],
+        Msg = simplest_msg(Context, Pieces),
+        Spec = error_spec($pred, severity_error, phase_parse_tree_to_hlds,
+            [Msg]),
+        !:Specs = [Spec | !.Specs],
+        !:FoundInvalidType = found_invalid_type
+    ).
+
+:- pred search_ctor_by_unqual_name(list(constructor)::in, string::in, int::in,
+    constructor::out) is semidet.
+
+search_ctor_by_unqual_name([HeadCtor | TailCtors], UnqualName, Arity, Ctor) :-
+    ( if
+        HeadCtor = ctor(_, _, HeadName, _, Arity, _),
+        unqualify_name(HeadName) = UnqualName
+    then
+        Ctor = HeadCtor
+    else
+        search_ctor_by_unqual_name(TailCtors, UnqualName, Arity, Ctor)
+    ).
+
+:- pred check_subtype_ctor_2(type_table::in, tvarset::in, type_status::in,
+    constructor::in, constructor::in,
+    found_invalid_type::in, found_invalid_type::out,
+    list(error_spec)::in, list(error_spec)::out) is det.
+
+check_subtype_ctor_2(TypeTable, TVarSet, TypeStatus, Ctor, SuperCtor,
+        !FoundInvalidType, !Specs) :-
+    Ctor = ctor(_, MaybeExistConstraints, CtorName, Args, Arity, Context),
+    SuperCtor = ctor(_, MaybeSuperExistConstraints, _SuperCtorName, SuperArgs,
+        _SuperArity, _SuperContext),
+    list.foldl3_corresponding(
+        check_subtype_ctor_arg(TypeTable, TVarSet, TypeStatus,
+            MaybeExistConstraints, MaybeSuperExistConstraints),
+        Args, SuperArgs,
+        map.init, ExistQVarsMapping,
+        did_not_find_invalid_type, FoundInvalidType, !Specs),
+    (
+        FoundInvalidType = did_not_find_invalid_type,
+        (
+            MaybeExistConstraints = no_exist_constraints,
+            MaybeSuperExistConstraints = no_exist_constraints
+        ;
+            MaybeExistConstraints = exist_constraints(Constraints),
+            MaybeSuperExistConstraints = exist_constraints(SuperConstraints),
+            CtorSymNameArity = sym_name_arity(CtorName, Arity),
+            check_subtype_ctor_exist_constraints(CtorSymNameArity,
+                Constraints, SuperConstraints, ExistQVarsMapping, Context,
+                !FoundInvalidType, !Specs)
+        ;
+            MaybeExistConstraints = no_exist_constraints,
+            MaybeSuperExistConstraints = exist_constraints(_),
+            unexpected($pred, "exist_constraints mismatch")
+        ;
+            MaybeExistConstraints = exist_constraints(_),
+            MaybeSuperExistConstraints = no_exist_constraints,
+            unexpected($pred, "exist_constraints mismatch")
+        )
+    ;
+        FoundInvalidType = found_invalid_type,
+        !:FoundInvalidType = FoundInvalidType
+    ).
+
+%---------------------%
+
+    % A map from existential type variable in the supertype constructor
+    % to an existential type variable in the subtype constructor.
+    %
+:- type existq_tvar_mapping == map(tvar, tvar).
+
+:- pred check_subtype_ctor_arg(type_table::in, tvarset::in, type_status::in,
+    maybe_cons_exist_constraints::in, maybe_cons_exist_constraints::in,
+    constructor_arg::in, constructor_arg::in,
+    existq_tvar_mapping::in, existq_tvar_mapping::out,
+    found_invalid_type::in, found_invalid_type::out,
+    list(error_spec)::in, list(error_spec)::out) is det.
+
+check_subtype_ctor_arg(TypeTable, TVarSet, OrigTypeStatus,
+        MaybeExistConstraints, MaybeSuperExistConstraints,
+        CtorArg, SuperCtorArg,
+        !ExistQVarsMapping, !FoundInvalidType, !Specs) :-
+    CtorArg = ctor_arg(_FieldName, ArgType, Context),
+    SuperCtorArg = ctor_arg(_SuperFieldName, SuperArgType, _SuperContext),
+    ( if
+        check_is_subtype(TypeTable, TVarSet, OrigTypeStatus,
+            ArgType, SuperArgType,
+            MaybeExistConstraints, MaybeSuperExistConstraints,
+            !ExistQVarsMapping)
+    then
+        true
+    else
+        ArgTypeStr =
+            mercury_type_to_string(TVarSet, print_name_only, ArgType),
+        SuperArgTypeStr =
+            mercury_type_to_string(TVarSet, print_name_only, SuperArgType),
+        Pieces = [words("Error:"), quote(ArgTypeStr),
+            words("is not a subtype of the corresponding type"),
+            quote(SuperArgTypeStr), words("in the supertype."), nl],
+        Msg = simplest_msg(Context, Pieces),
+        Spec = error_spec($pred, severity_error, phase_parse_tree_to_hlds,
+            [Msg]),
+        !:Specs = [Spec | !.Specs],
+        !:FoundInvalidType = found_invalid_type
+    ).
+
+%---------------------%
+
+:- pred check_is_subtype(type_table::in, tvarset::in, type_status::in,
+    mer_type::in, mer_type::in,
+    maybe_cons_exist_constraints::in, maybe_cons_exist_constraints::in,
+    existq_tvar_mapping::in, existq_tvar_mapping::out) is semidet.
+
+check_is_subtype(TypeTable, TVarSet0, OrigTypeStatus, TypeA, TypeB,
+        MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping) :-
+    require_complete_switch [TypeA]
+    (
+        TypeA = builtin_type(BuiltinType),
+        TypeB = builtin_type(BuiltinType)
+    ;
+        TypeA = type_variable(VarA, Kind),
+        TypeB = type_variable(VarB, Kind),
+        check_is_subtype_var_var(VarA, VarB,
+            MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping)
+    ;
+        TypeA = defined_type(NameA, ArgTypesA, Kind),
+        TypeB = defined_type(NameB, ArgTypesB, Kind),
+        ( if
+            NameA = NameB,
+            list.length(ArgTypesA, Arity),
+            list.length(ArgTypesB, Arity)
+        then
+            % TypeA and TypeB have the same type constructor.
+            % Check their corresponding argument types.
+            check_corresponding_args_are_subtype(TypeTable, TVarSet0,
+                OrigTypeStatus, ArgTypesA, ArgTypesB,
+                MaybeExistConstraintsA, MaybeExistConstraintsB,
+                !ExistQVarsMapping)
+        else
+            % TypeA and TypeB have different type constructors.
+            % Find a subtype definition s(S1, ..., Sn) =< t(T1, ..., Tk)
+            % where s/n is the type constructor of TypeA.
+            list.length(ArgTypesA, ArityA),
+            TypeCtorA = type_ctor(NameA, ArityA),
+            search_type_ctor_defn(TypeTable, TypeCtorA, TypeDefnA),
+            hlds_data.get_type_defn_body(TypeDefnA, TypeBodyA),
+            TypeBodyA = hlds_du_type(_, yes(SuperTypeA), _, _, _),
+
+            hlds_data.get_type_defn_status(TypeDefnA, TypeStatusA),
+            not subtype_defn_int_supertype_defn_impl(OrigTypeStatus,
+                TypeStatusA),
+
+            % The variables S1, ..., Sn must be distinct.
+            % Create a substitution from S1, ..., Sn to the types in ArgTypesA.
+            hlds_data.get_type_defn_tvarset(TypeDefnA, TVarSetA),
+            hlds_data.get_type_defn_tparams(TypeDefnA, TypeParamsA0),
+            tvarset_merge_renaming(TVarSet0, TVarSetA, TVarSet, RenamingA),
+            apply_variable_renaming_to_tvar_list(RenamingA, TypeParamsA0,
+                TypeParamsA),
+            map.from_corresponding_lists(TypeParamsA, ArgTypesA, TSubstA),
+
+            % Apply the substitution to t(T1, ..., Tk) to give
+            % t(T1', ..., Tk').
+            rename_and_rec_subst_in_type(RenamingA, TSubstA, SuperTypeA,
+                NewTypeA),
+
+            % Check that t(T1', ..., Tk') =< TypeB.
+            check_is_subtype(TypeTable, TVarSet, OrigTypeStatus,
+                NewTypeA, TypeB,
+                MaybeExistConstraintsA, MaybeExistConstraintsB,
+                !ExistQVarsMapping)
+        )
+    ;
+        TypeA = tuple_type(ArgTypesA, Kind),
+        TypeB = tuple_type(ArgTypesB, Kind),
+        list.length(ArgTypesA, Arity),
+        list.length(ArgTypesB, Arity),
+        check_corresponding_args_are_subtype(TypeTable, TVarSet0,
+            OrigTypeStatus, ArgTypesA, ArgTypesB,
+            MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping)
+    ;
+        TypeA = higher_order_type(PredOrFunc, ArgTypesA, HOInstInfoA, Purity,
+            EvalMethod),
+        TypeB = higher_order_type(PredOrFunc, ArgTypesB, HOInstInfoB, Purity,
+            EvalMethod),
+        list.length(ArgTypesA, Arity),
+        list.length(ArgTypesB, Arity),
+        (
+            HOInstInfoA = higher_order(PredInfoInfoA),
+            HOInstInfoB = higher_order(PredInfoInfoB),
+            PredInfoInfoA = pred_inst_info(PredOrFunc, ArgModesA, _RegTypesA,
+                Detism),
+            PredInfoInfoB = pred_inst_info(PredOrFunc, ArgModesB, _RegTypesB,
+                Detism),
+            MaybeArgModesA = yes(ArgModesA),
+            MaybeArgModesB = yes(ArgModesB)
+        ;
+            HOInstInfoA = none_or_default_func,
+            HOInstInfoB = none_or_default_func,
+            MaybeArgModesA = no,
+            MaybeArgModesB = no
+        ),
+        check_is_subtype_higher_order(TypeTable, TVarSet0, OrigTypeStatus,
+            ArgTypesA, ArgTypesB, MaybeArgModesA, MaybeArgModesB,
+            MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping)
+    ;
+        TypeA = apply_n_type(_, _, _),
+        fail
+    ;
+        TypeA = kinded_type(TypeA1, Kind),
+        TypeB = kinded_type(TypeB1, Kind),
+        check_is_subtype(TypeTable, TVarSet0, OrigTypeStatus, TypeA1, TypeB1,
+            MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping)
+    ).
+
+:- pred check_is_subtype_var_var(tvar::in, tvar::in,
+    maybe_cons_exist_constraints::in, maybe_cons_exist_constraints::in,
+    existq_tvar_mapping::in, existq_tvar_mapping::out) is semidet.
+
+check_is_subtype_var_var(VarA, VarB,
+        MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping) :-
+    ( if VarA = VarB then
+        true
+    else if map.search(!.ExistQVarsMapping, VarB, VarB1) then
+        VarB1 = VarA
+    else
+        MaybeExistConstraintsA = exist_constraints(ExistConstraintsA),
+        MaybeExistConstraintsB = exist_constraints(ExistConstraintsB),
+        ExistConstraintsA = cons_exist_constraints(_ExistQVarsA,
+            _ConstraintsA, UnconstrainedExistQVarsA, ConstrainedExistQVarsA),
+        ExistConstraintsB = cons_exist_constraints(_ExistQVarsB,
+            _ConstraintsB, UnconstrainedExistQVarsB, ConstrainedExistQVarsB),
+        (
+            list.contains(UnconstrainedExistQVarsA, VarA),
+            list.contains(UnconstrainedExistQVarsB, VarB)
+        ;
+            list.contains(ConstrainedExistQVarsA, VarA),
+            list.contains(ConstrainedExistQVarsB, VarB)
+        ),
+        map.insert(VarB, VarA, !ExistQVarsMapping)
+    ).
+
+:- pred check_corresponding_args_are_subtype(type_table::in, tvarset::in,
+    type_status::in, list(mer_type)::in, list(mer_type)::in,
+    maybe_cons_exist_constraints::in, maybe_cons_exist_constraints::in,
+    existq_tvar_mapping::in, existq_tvar_mapping::out) is semidet.
+
+check_corresponding_args_are_subtype(_TypeTable, _TVarSet, _OrigTypeStatus,
+        [], [],
+        _MaybeExistConstraintsA, _MaybeExistConstraintsB, !ExistQVarsMapping).
+check_corresponding_args_are_subtype(TypeTable, TVarSet, OrigTypeStatus,
+        [TypeA | TypesA], [TypeB | TypesB],
+        MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping) :-
+    check_is_subtype(TypeTable, TVarSet, OrigTypeStatus, TypeA, TypeB,
+        MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping),
+    check_corresponding_args_are_subtype(TypeTable, TVarSet, OrigTypeStatus,
+        TypesA, TypesB, MaybeExistConstraintsA, MaybeExistConstraintsB,
+        !ExistQVarsMapping).
+
+:- pred check_is_subtype_higher_order(type_table::in, tvarset::in,
+    type_status::in, list(mer_type)::in, list(mer_type)::in,
+    maybe(list(mer_mode))::in, maybe(list(mer_mode))::in,
+    maybe_cons_exist_constraints::in, maybe_cons_exist_constraints::in,
+    existq_tvar_mapping::in, existq_tvar_mapping::out) is semidet.
+
+check_is_subtype_higher_order(_TypeTable, _TVarSet, _OrigTypeStatus,
+        [], [], MaybeModesA, MaybeModesB,
+        _MaybeExistConstraintsA, _MaybeExistConstraintsB, !ExistQVarsMapping)
+        :-
+    (
+        MaybeModesA = no,
+        MaybeModesB = no
+    ;
+        MaybeModesA = yes([]),
+        MaybeModesB = yes([])
+    ).
+check_is_subtype_higher_order(TypeTable, TVarSet, OrigTypeStatus,
+        [TypeA | TypesA], [TypeB | TypesB], MaybeModesA0, MaybeModesB0,
+        MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping) :-
+    % Check arguments of higher order term have the same type.
+    % This could be more efficient, but should be rare used anyway.
+    check_is_subtype(TypeTable, TVarSet, OrigTypeStatus, TypeA, TypeB,
+        MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping),
+    check_is_subtype(TypeTable, TVarSet, OrigTypeStatus, TypeB, TypeA,
+        MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping),
+
+    % Argument modes, if available, must match exactly.
+    (
+        MaybeModesA0 = no,
+        MaybeModesB0 = no,
+        MaybeModesA = no,
+        MaybeModesB = no
+    ;
+        MaybeModesA0 = yes([ModeA | ModesA]),
+        MaybeModesB0 = yes([ModeB | ModesB]),
+        % XXX Currently we require term equality.
+        ModeA = ModeB,
+        MaybeModesA = yes(ModesA),
+        MaybeModesB = yes(ModesB)
+    ),
+
+    check_is_subtype_higher_order(TypeTable, TVarSet, OrigTypeStatus,
+        TypesA, TypesB, MaybeModesA, MaybeModesB,
+        MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping).
+
+%---------------------%
+
+:- pred check_subtype_ctor_exist_constraints(sym_name_arity::in,
+    cons_exist_constraints::in, cons_exist_constraints::in,
+    existq_tvar_mapping::in, prog_context::in,
+    found_invalid_type::in, found_invalid_type::out,
+    list(error_spec)::in, list(error_spec)::out) is det.
+
+check_subtype_ctor_exist_constraints(CtorSymNameArity,
+        ExistConstraints, SuperExistConstraints, ExistQVarsMapping, Context,
+        !FoundInvalidType, !Specs) :-
+    ExistConstraints = cons_exist_constraints(_, Constraints, _, _),
+    SuperExistConstraints = cons_exist_constraints(_, SuperConstraints0, _, _),
+    apply_variable_renaming_to_prog_constraint_list(ExistQVarsMapping,
+        SuperConstraints0, SuperConstraints),
+    list.sort(Constraints, SortedConstraints),
+    list.sort(SuperConstraints, SortedSuperConstraints),
+    ( if SortedConstraints = SortedSuperConstraints then
+        true
+    else
+        Pieces = [words("Error: existential class constraints for"),
+            unqual_sym_name_arity(CtorSymNameArity),
+            words("differ in the subtype and supertype."), nl],
+        Msg = simplest_msg(Context, Pieces),
+        Spec = error_spec($pred, severity_error, phase_parse_tree_to_hlds,
+            [Msg]),
+        !:Specs = [Spec | !.Specs],
+        !:FoundInvalidType = found_invalid_type
+    ).
+
+%---------------------%
+
+:- pred rename_and_rec_subst_in_constructor(tvar_renaming::in, tsubst::in,
+    constructor::in, constructor::out) is det.
+
+rename_and_rec_subst_in_constructor(Renaming, TSubst, Ctor0, Ctor) :-
+    Ctor0 = ctor(Ordinal, MaybeExistConstraints0, Name, Args0, NumArgs,
+        Context),
+    (
+        MaybeExistConstraints0 = no_exist_constraints,
+        MaybeExistConstraints = no_exist_constraints
+    ;
+        MaybeExistConstraints0 = exist_constraints(ExistConstraints0),
+        rename_and_rec_subst_in_exist_constraints(Renaming, TSubst,
+            ExistConstraints0, ExistConstraints),
+        MaybeExistConstraints = exist_constraints(ExistConstraints)
+    ),
+    list.map(rename_and_rec_subst_in_constructor_arg(Renaming, TSubst),
+        Args0, Args),
+    Ctor = ctor(Ordinal, MaybeExistConstraints, Name, Args, NumArgs,
+        Context).
+
+:- pred rename_and_rec_subst_in_exist_constraints(tvar_renaming::in,
+    tsubst::in, cons_exist_constraints::in, cons_exist_constraints::out)
+    is det.
+
+rename_and_rec_subst_in_exist_constraints(Renaming, TSubst,
+        ExistConstraints0, ExistConstraints) :-
+    ExistConstraints0 = cons_exist_constraints(ExistQVars0, Constraints0,
+        UnconstrainedExistQVars0, ConstrainedExistQVars0),
+
+    apply_variable_renaming_to_tvar_list(Renaming,
+        ExistQVars0, ExistQVars),
+
+    apply_variable_renaming_to_prog_constraint_list(Renaming,
+        Constraints0, Constraints1),
+    apply_rec_subst_to_prog_constraint_list(TSubst,
+        Constraints1, Constraints),
+
+    apply_variable_renaming_to_tvar_list(Renaming,
+        UnconstrainedExistQVars0, UnconstrainedExistQVars),
+
+    apply_variable_renaming_to_tvar_list(Renaming,
+        ConstrainedExistQVars0, ConstrainedExistQVars),
+
+    ExistConstraints = cons_exist_constraints(ExistQVars, Constraints,
+        UnconstrainedExistQVars, ConstrainedExistQVars).
+
+:- pred rename_and_rec_subst_in_constructor_arg(tvar_renaming::in, tsubst::in,
+    constructor_arg::in, constructor_arg::out) is det.
+
+rename_and_rec_subst_in_constructor_arg(Renaming, TSubst, Arg0, Arg) :-
+    Arg0 = ctor_arg(MaybeFieldName, Type0, Context),
+    rename_and_rec_subst_in_type(Renaming, TSubst, Type0, Type),
+    Arg = ctor_arg(MaybeFieldName, Type, Context).
+
+:- pred rename_and_rec_subst_in_type(tvar_renaming::in, tsubst::in,
+    mer_type::in, mer_type::out) is det.
+
+rename_and_rec_subst_in_type(Renaming, TSubst, Type0, Type) :-
+    apply_variable_renaming_to_type(Renaming, Type0, Type1),
+    apply_rec_subst_to_type(TSubst, Type1, Type).
+
 %---------------------------------------------------------------------------%
 :- end_module hlds.make_hlds.add_type.
 %---------------------------------------------------------------------------%
diff --git a/compiler/check_parse_tree_type_defns.m b/compiler/check_parse_tree_type_defns.m
index 397cf6b10..38e5e2c16 100644
--- a/compiler/check_parse_tree_type_defns.m
+++ b/compiler/check_parse_tree_type_defns.m
@@ -531,7 +531,7 @@ check_type_ctor_defns(InsistOnDefn, ModuleName,
         % we will have to disable users' ability to specify MaybeDirectArgs
         % in source code.
         DetailsDu = DuDefn ^ td_ctor_defn,
-        DetailsDu = type_details_du(OoMCtors, _MaybeCanonical,
+        DetailsDu = type_details_du(_MaybeSuperType, OoMCtors, _MaybeCanonical,
             _MaybeDirectArgs),
         OoMCtors = one_or_more(HeadCtor, TailCtors),
         ( if
@@ -1577,7 +1577,7 @@ add_type_ctor_to_field_name_map(TypeCtor, CheckedDefn, !FieldNameMap) :-
             CheckedStdDefn = std_mer_type_du_not_all_plain_constants(_Status,
                 DuDefn, _MaybeDefnCJCs),
             DetailsDu = DuDefn ^ td_ctor_defn,
-            DetailsDu = type_details_du(OoMCtors,
+            DetailsDu = type_details_du(_MaybeSuperType, OoMCtors,
                 _MaybeCanonical, _MaybeDirectArgs),
             OoMCtors = one_or_more(HeadCtor, TailCtors),
             list.foldl(add_data_ctor_to_field_name_map(TypeCtor),
diff --git a/compiler/check_typeclass.m b/compiler/check_typeclass.m
index a33eb205d..aec7ecd7d 100644
--- a/compiler/check_typeclass.m
+++ b/compiler/check_typeclass.m
@@ -274,7 +274,7 @@ is_valid_instance_orig_type(ModuleInfo, ClassId, InstanceDefn, Type,
                     true
                 )
             ;
-                ( TypeBody = hlds_du_type(_, _, _, _)
+                ( TypeBody = hlds_du_type(_, _, _, _, _)
                 ; TypeBody = hlds_foreign_type(_)
                 ; TypeBody = hlds_solver_type(_)
                 ; TypeBody = hlds_abstract_type(_)
@@ -353,7 +353,7 @@ is_valid_instance_type(ModuleInfo, ClassId, InstanceDefn, Type,
                     is_valid_instance_type(ModuleInfo, ClassId, InstanceDefn,
                         EqvType, N, _, !Specs)
                 ;
-                    ( TypeBody = hlds_du_type(_, _, _, _)
+                    ( TypeBody = hlds_du_type(_, _, _, _, _)
                     ; TypeBody = hlds_foreign_type(_)
                     ; TypeBody = hlds_solver_type(_)
                     ; TypeBody = hlds_abstract_type(_)
@@ -1790,7 +1790,7 @@ check_typeclass_constraints_on_type_ctor(ModuleInfo, TypeCtor - TypeDefn,
         !Specs) :-
     get_type_defn_body(TypeDefn, Body),
     (
-        Body = hlds_du_type(Ctors, _, _, _),
+        Body = hlds_du_type(Ctors, _, _, _, _),
         list.foldl(
             check_typeclass_constraints_on_data_ctor(ModuleInfo, TypeCtor,
                 TypeDefn),
diff --git a/compiler/code_info.m b/compiler/code_info.m
index e5b4d9409..b1896289c 100644
--- a/compiler/code_info.m
+++ b/compiler/code_info.m
@@ -927,7 +927,7 @@ lookup_cheaper_tag_test(CI, Type) = CheaperTagTest :-
     ( if
         search_type_defn(CI, Type, TypeDefn),
         get_type_defn_body(TypeDefn, TypeBody),
-        TypeBody = hlds_du_type(_, _, MaybeRepn, _),
+        TypeBody = hlds_du_type(_, _, _, MaybeRepn, _),
         MaybeRepn = yes(Repn)
     then
         CheaperTagTest = Repn ^ dur_cheaper_tag_test
diff --git a/compiler/comp_unit_interface.m b/compiler/comp_unit_interface.m
index 4c80a1028..faf240fc2 100644
--- a/compiler/comp_unit_interface.m
+++ b/compiler/comp_unit_interface.m
@@ -1278,7 +1278,9 @@ accumulate_abs_imp_exported_type_lhs_in_defn(IntTypesMap, BothTypesMap,
         )
     ;
         ImpTypeDefn = parse_tree_du_type(DetailsDu),
-        DetailsDu = type_details_du(OoMCtors, MaybeEqCmp, MaybeDirectArgCtors),
+        DetailsDu = type_details_du(_MaybeSuperType, OoMCtors, MaybeEqCmp,
+            MaybeDirectArgCtors),
+        % XXX SUBTYPE Type representation of subtype depends on base type.
         ( if
             map.search(IntTypesMap, TypeCtor, _),
             du_type_is_enum(DetailsDu, _NumFunctors)
@@ -1292,6 +1294,8 @@ accumulate_abs_imp_exported_type_lhs_in_defn(IntTypesMap, BothTypesMap,
             % defined in another module, we will NOT include TypeCtor in
             % !DirectDummyTypeCtors, since we won't know enough about
             % the contents of the other module.
+            % XXX SUBTYPE Do not consider a subtype to be a dummy type
+            % unless the base type is a dummy type.
             constructor_list_represents_dummy_type(BothTypesMap, OoMCtors,
                 MaybeEqCmp, MaybeDirectArgCtors)
         then
@@ -1359,7 +1363,7 @@ accumulate_abs_eqv_type_rhs_in_defn(ImpTypesMap, ImpItemTypeDefnInfo,
             !AbsExpEqvRhsTypeCtors, set.init, _, !ModulesNeededByTypeDefns)
     ;
         ImpTypeDefn = parse_tree_du_type(DetailsDu),
-        DetailsDu = type_details_du(OoMCtors, _, _),
+        DetailsDu = type_details_du(MaybeSuperType, OoMCtors, _, _),
         % There must exist a foreign type alternative to this type.
         % XXX ITEM_LIST I (zs) would like to see a proof argument for that,
         % since I don't think it is true. Unfortunately, we cannot check it
@@ -1369,7 +1373,17 @@ accumulate_abs_eqv_type_rhs_in_defn(ImpTypesMap, ImpItemTypeDefnInfo,
         % inside all the argument types of all the data constructors, and the
         % modules that define them.
         ctors_to_user_type_ctor_set(one_or_more_to_list(OoMCtors),
-            set.init, RhsTypeCtors),
+            set.init, RhsTypeCtors0),
+        (
+            MaybeSuperType = no,
+            RhsTypeCtors = RhsTypeCtors0
+        ;
+            MaybeSuperType = yes(SuperType),
+            % If the type is a subtype then we also require the type_ctor of
+            % the supertype, and all the type_ctors inside the argument types
+            % of the supertype, and the modules that define them.
+            type_to_user_type_ctor_set(SuperType, RhsTypeCtors0, RhsTypeCtors)
+        ),
         set.union(RhsTypeCtors, !DuArgTypeCtors),
         set.fold(accumulate_modules_used_by_type_ctor, RhsTypeCtors,
             !ModulesNeededByTypeDefns)
@@ -1513,8 +1527,10 @@ ctor_arg_is_dummy_type(TypeDefnMap, Type, CoveredTypes0) = IsDummyType :-
                     one_or_more.member(ItemTypeDefnInfo, ItemTypeDefnInfos),
                     TypeDefn = ItemTypeDefnInfo ^ td_ctor_defn,
                     TypeDefn = parse_tree_du_type(DetailsDu),
-                    DetailsDu = type_details_du(OoMCtors, MaybeEqCmp,
-                        MaybeDirectArgCtors),
+                    % XXX SUBTYPE Do not consider a subtype to be a dummy type
+                    % unless the base type is a dummy type.
+                    DetailsDu = type_details_du(_MaybeSuperType, OoMCtors,
+                        MaybeEqCmp, MaybeDirectArgCtors),
                     constructor_list_represents_dummy_type_2(TypeDefnMap,
                         OoMCtors, MaybeEqCmp, MaybeDirectArgCtors,
                         [Type | CoveredTypes0])
@@ -1648,9 +1664,11 @@ make_imp_type_abstract(BothTypesMap, !ImpItemTypeDefnInfo) :-
     !.ImpItemTypeDefnInfo = item_type_defn_info(_, _, TypeDefn0, _, _, _),
     (
         TypeDefn0 = parse_tree_du_type(DetailsDu0),
-        DetailsDu0 = type_details_du(OoMCtors, MaybeEqCmp,
+        DetailsDu0 = type_details_du(_MaybeSuperType, OoMCtors, MaybeEqCmp,
             MaybeDirectArgCtors),
         ( if
+            % XXX SUBTYPE Do not consider a subtype to be a dummy type unless
+            % the base type is a dummy type.
             constructor_list_represents_dummy_type(BothTypesMap,
                 OoMCtors, MaybeEqCmp, MaybeDirectArgCtors)
         then
@@ -2263,7 +2281,9 @@ dummy_solver_type = DetailsSolver :-
     is det.
 
 make_du_type_abstract(DetailsDu, DetailsAbstract) :-
-    DetailsDu = type_details_du(Ctors, MaybeCanonical, _MaybeDirectArgCtors),
+    % XXX SUBTYPE Type representation of subtype depends on base type.
+    DetailsDu = type_details_du(_MaybeSuperType, Ctors, MaybeCanonical,
+        _MaybeDirectArgCtors),
     ( if du_type_is_enum(DetailsDu, NumFunctors) then
         num_bits_needed_for_n_values(NumFunctors, NumBits),
         DetailsAbstract = abstract_type_fits_in_n_bits(NumBits)
diff --git a/compiler/dead_proc_elim.m b/compiler/dead_proc_elim.m
index e60d89a25..5ce83e3d3 100644
--- a/compiler/dead_proc_elim.m
+++ b/compiler/dead_proc_elim.m
@@ -1373,7 +1373,8 @@ dead_pred_initialize_referred_preds(ModuleInfo, _TypeCtor - TypeDefn,
         !NeededPreds) :-
     get_type_defn_body(TypeDefn, TypeDefnBody),
     (
-        TypeDefnBody = hlds_du_type(_Ctors, MaybeCanon, _Repn, _IsForeign),
+        TypeDefnBody = hlds_du_type(_Ctors, _MaybeSuperType, MaybeCanon, _Repn,
+            _IsForeign),
         dead_pred_initialize_maybe_canonical(ModuleInfo, MaybeCanon,
             !NeededPreds)
     ;
diff --git a/compiler/decide_type_repn.m b/compiler/decide_type_repn.m
index 83f6c735f..b21828251 100644
--- a/compiler/decide_type_repn.m
+++ b/compiler/decide_type_repn.m
@@ -140,7 +140,7 @@
     % - figure out which type definitions define exported simple types,
     % - decide their representations, and
     % - generate items recording those decisions, for types that appear
-    %   in the interfac
+    %   in the interface
     %
 :- pred decide_repns_for_simple_types_for_int3(module_name::in,
     type_ctor_checked_map::in, type_ctor_repn_map::out) is det.
@@ -353,7 +353,9 @@ decide_type_repns_stage_1_du_not_all_plain_constants(TypeCtor, DuDefn,
     decide_type_repns_foreign_defns(MaybeDefnCJCsE, ForeignTypeRepns),
     DuDefn = item_type_defn_info(_TypeCtorSymName, TypeParams, DetailsDu,
         TVarSet, _Context, _SeqNum),
-    DetailsDu = type_details_du(OoMCtors, MaybeCanonical, _MaybeDirectArgs),
+    % XXX SUBTYPE Type representation of subtype depends on base type.
+    DetailsDu = type_details_du(_MaybeSuperType, OoMCtors, MaybeCanonical,
+        _MaybeDirectArgs),
     OoMCtors = one_or_more(HeadCtor, TailCtors),
     (
         TailCtors = [],
@@ -752,7 +754,9 @@ decide_type_repns_stage_2_du_gen(BaseParams, EqvMap,
     expect(unify(TypeCtorSymName, SymName), $pred, "sym_name mismatch"),
     expect(unify(NumTypeParams, Arity), $pred, "arity mismatch"),
 
-    DetailsDu = type_details_du(OoMCtors0, MaybeCanonical, _MaybeDirectArgs),
+    % XXX SUBTYPE Type representation of subtype depends on base type.
+    DetailsDu = type_details_du(_MaybeSuperType, OoMCtors0, MaybeCanonical,
+        _MaybeDirectArgs),
     OoMCtors0 = one_or_more(HeadCtor0, TailCtors0),
     expand_eqv_cnotag_types_in_constructor(EqvMap, SimpleDuMap, TVarSet,
         HeadCtor0, HeadCtor, !Specs),
diff --git a/compiler/det_report.m b/compiler/det_report.m
index 6f627afbb..2c9942218 100644
--- a/compiler/det_report.m
+++ b/compiler/det_report.m
@@ -1671,7 +1671,7 @@ find_missing_cons_ids(DetInfo, MaybeLimit, InstMap0, SwitchContexts,
             ( if
                 det_lookup_var_type(ModuleInfo, ProcInfo, Var, TypeDefn),
                 hlds_data.get_type_defn_body(TypeDefn, TypeBody),
-                TypeBody = hlds_du_type(TypeConstructors, _, _, _)
+                TypeBody = hlds_du_type(TypeConstructors, _, _, _, _)
             then
                 SortedTypeConsIds =
                     constructor_cons_ids(VarTypeCtor,
@@ -1686,7 +1686,7 @@ find_missing_cons_ids(DetInfo, MaybeLimit, InstMap0, SwitchContexts,
         else
             det_lookup_var_type(ModuleInfo, ProcInfo, Var, TypeDefn),
             hlds_data.get_type_defn_body(TypeDefn, TypeBody),
-            TypeBody = hlds_du_type(TypeConstructors, _, _, _),
+            TypeBody = hlds_du_type(TypeConstructors, _, _, _, _),
             SortedTypeConsIds =
                 constructor_cons_ids(VarTypeCtor,
                     one_or_more_to_list(TypeConstructors)),
diff --git a/compiler/direct_arg_in_out.m b/compiler/direct_arg_in_out.m
index 43a076a00..f7268cff7 100644
--- a/compiler/direct_arg_in_out.m
+++ b/compiler/direct_arg_in_out.m
@@ -335,7 +335,8 @@ is_direct_arg_in_out_posn(ModuleInfo, VarTypes, Var, Mode, IsDAIO) :-
     then
         get_type_defn_body(TypeDefn, TypeBody),
         (
-            TypeBody = hlds_du_type(_, _, MaybeRepn, _),
+            TypeBody = hlds_du_type(_, _MaybeSuperType, _, MaybeRepn, _),
+            % XXX SUBTYPE Type representation of subtype depends on base type.
             (
                 MaybeRepn = no,
                 unexpected($pred, "MaybeRepn = no")
@@ -1512,7 +1513,7 @@ expand_daio_in_unify(GoalInfo0, GoalExpr0, GoalExpr, InstMap0,
             module_info_get_type_table(ModuleInfo, TypeTable),
             search_type_ctor_defn(TypeTable, ConsIdTypeCtor, TypeDefn),
             get_type_defn_body(TypeDefn, TypeBody),
-            TypeBody = hlds_du_type(_, _, MaybeRepn, _),
+            TypeBody = hlds_du_type(_, _, _, MaybeRepn, _),
             (
                 MaybeRepn = no,
                 unexpected($pred, "MaybeRepn = no")
diff --git a/compiler/du_type_layout.m b/compiler/du_type_layout.m
index a5b7a2486..f80b1be0f 100644
--- a/compiler/du_type_layout.m
+++ b/compiler/du_type_layout.m
@@ -250,8 +250,9 @@ decide_if_simple_du_type(ModuleInfo, Params, TypeCtorToForeignEnumMap,
     TypeCtorTypeDefn0 = TypeCtor - TypeDefn0,
     get_type_defn_body(TypeDefn0, Body0),
     (
-        Body0 = hlds_du_type(OoMCtors, MaybeCanonical, MaybeRepn0,
-            MaybeForeign),
+        % XXX SUBTYPE Type representation of subtype depends on base type.
+        Body0 = hlds_du_type(OoMCtors, _MaybeSuperType, MaybeCanonical,
+            MaybeRepn0, MaybeForeign),
         OoMCtors = one_or_more(HeadCtor, TailCtors),
         expect(unify(MaybeRepn0, no), $pred, "MaybeRepn0 != no"),
         ( if
@@ -636,8 +637,9 @@ decide_if_complex_du_type(ModuleInfo, Params, ComponentTypeMap,
     TypeCtorTypeDefn0 = TypeCtor - TypeDefn0,
     get_type_defn_body(TypeDefn0, Body0),
     (
-        Body0 = hlds_du_type(Ctors, _MaybeCanonical, MaybeRepn0,
-            _MaybeForeign),
+        % XXX SUBTYPE Type representation of subtype depends on base type.
+        Body0 = hlds_du_type(Ctors, _MaybeSuperType, _MaybeCanonical,
+            MaybeRepn0, _MaybeForeign),
         (
             MaybeRepn0 = yes(_),
             % We have already decided this type's representation
@@ -1930,9 +1932,10 @@ is_direct_arg_ctor(ComponentTypeMap, TypeCtorModule, TypeStatus,
             % (mercury_deep_copy_body.h), and maybe during some other
             % operations.
 
+            % XXX SUBTYPE Type representation of subtype depends on base type.
             get_type_defn_body(ArgTypeDefn, ArgTypeDefnBody),
-            ArgTypeDefnBody = hlds_du_type(_ArgCtors, _ArgMaybeUserEqComp,
-                _ArgMaybeRepn, ArgMaybeForeign),
+            ArgTypeDefnBody = hlds_du_type(_ArgCtors, _ArgMaybeSuperType,
+                _ArgMaybeUserEqComp, _ArgMaybeRepn, ArgMaybeForeign),
 
             ArgMaybeForeign = no,
 
@@ -2416,7 +2419,7 @@ deref_eqv_types(ModuleInfo, Type0, Type) :-
 %---------------------%
 
 :- inst hlds_du_type for hlds_type_body/0
-    --->    hlds_du_type(ground, ground, ground, ground).
+    --->    hlds_du_type(ground, ground, ground, ground, ground).
 
 :- pred separate_out_constants(list(constructor)::in,
     list(constructor)::out, list(constructor)::out) is det.
@@ -2559,8 +2562,9 @@ show_decisions_if_du_type(Stream, MaybePrimaryTags, ShowWhichTypes,
             ; Body = hlds_solver_type(_)
             )
         ;
-            Body = hlds_du_type(_Ctors, _MaybeCanonical, MaybeRepn,
-                _MaybeForeign),
+            Body = hlds_du_type(_Ctors, _MaybeSuperType, _MaybeCanonical,
+                MaybeRepn, _MaybeForeign),
+            % XXX SUBTYPE Show supertype.
             (
                 MaybeRepn = no,
                 unexpected($pred, "MaybeRepn = no")
diff --git a/compiler/equiv_type.m b/compiler/equiv_type.m
index fce1c8199..96ccc8764 100644
--- a/compiler/equiv_type.m
+++ b/compiler/equiv_type.m
@@ -1642,10 +1642,21 @@ report_contains_circular_eqv_type(TVarSet, Type, Context,
 replace_in_type_defn_du(MaybeRecord, TypeEqvMap, _InstEqvMap,
         _TypeCtor, _Context, DetailsDu0, DetailsDu,
         !TVarSet, !EquivTypeInfo, !UsedModules, Specs) :-
-    DetailsDu0 = type_details_du(Ctors0, EqPred, DirectArgFunctors),
+    DetailsDu0 = type_details_du(MaybeSuperType0, Ctors0, EqPred,
+        DirectArgFunctors),
+    (
+        MaybeSuperType0 = yes(SuperType0),
+        replace_in_type_maybe_record_use(MaybeRecord, TypeEqvMap,
+            SuperType0, SuperType, _, !TVarSet, !EquivTypeInfo, !UsedModules),
+        MaybeSuperType = yes(SuperType)
+    ;
+        MaybeSuperType0 = no,
+        MaybeSuperType = no
+    ),
     replace_in_ctors_location(MaybeRecord, TypeEqvMap, Ctors0, Ctors,
         !TVarSet, !EquivTypeInfo, !UsedModules),
-    DetailsDu = type_details_du(Ctors, EqPred, DirectArgFunctors),
+    DetailsDu = type_details_du(MaybeSuperType, Ctors, EqPred,
+        DirectArgFunctors),
     Specs = [].
 
 :- pred replace_in_type_defn_solver(maybe_record_sym_name_use::in,
diff --git a/compiler/equiv_type_hlds.m b/compiler/equiv_type_hlds.m
index 33319dcbf..3066c5b79 100644
--- a/compiler/equiv_type_hlds.m
+++ b/compiler/equiv_type_hlds.m
@@ -120,7 +120,7 @@ add_type_to_eqv_map(TypeCtor, Defn, !TypeEqvMap, !EqvExportTypes) :-
             IsExported = no
         )
     ;
-        ( Body = hlds_du_type(_, _, _, _)
+        ( Body = hlds_du_type(_, _, _, _, _)
         ; Body = hlds_foreign_type(_)
         ; Body = hlds_solver_type(_)
         ; Body = hlds_abstract_type(_)
@@ -169,13 +169,24 @@ replace_in_type_defn(ModuleName, TypeEqvMap, TypeCtor, !Defn,
     maybe_start_recording_expanded_items(ModuleName, TypeCtorSymName,
         !.MaybeRecompInfo, EquivTypeInfo0),
     (
-        Body0 = hlds_du_type(Ctors0, MaybeCanonical, MaybeRepn0, MaybeForeign),
+        Body0 = hlds_du_type(Ctors0, MaybeSuperType0, MaybeCanonical,
+            MaybeRepn0, MaybeForeign),
+        (
+            MaybeSuperType0 = yes(SuperType0),
+            hlds_replace_in_type(TypeEqvMap, SuperType0, SuperType,
+                TVarSet0, TVarSet1),
+            MaybeSuperType = yes(SuperType)
+        ;
+            MaybeSuperType0 = no,
+            MaybeSuperType = no,
+            TVarSet1 = TVarSet0
+        ),
         equiv_type.replace_in_ctors(TypeEqvMap, Ctors0, Ctors,
-            TVarSet0, TVarSet1, EquivTypeInfo0, EquivTypeInfo1),
+            TVarSet1, TVarSet2, EquivTypeInfo0, EquivTypeInfo1),
         (
             MaybeRepn0 = no,
             MaybeRepn = no,
-            TVarSet = TVarSet1,
+            TVarSet = TVarSet2,
             EquivTypeInfo = EquivTypeInfo1
         ;
             MaybeRepn0 = yes(Repn0),
@@ -183,12 +194,13 @@ replace_in_type_defn(ModuleName, TypeEqvMap, TypeCtor, !Defn,
                 CheaperTagTest, DuKind, DirectArgCtors),
             list.map_foldl3(replace_in_ctor_repn(TypeEqvMap),
                 CtorRepns0, CtorRepns, map.init, CtorNameToRepnMap,
-                TVarSet1, TVarSet, EquivTypeInfo1, EquivTypeInfo),
+                TVarSet2, TVarSet, EquivTypeInfo1, EquivTypeInfo),
             Repn = du_type_repn(CtorRepns, CtorNameToRepnMap,
                 CheaperTagTest, DuKind, DirectArgCtors),
             MaybeRepn = yes(Repn)
         ),
-        Body = hlds_du_type(Ctors, MaybeCanonical, MaybeRepn, MaybeForeign)
+        Body = hlds_du_type(Ctors, MaybeSuperType, MaybeCanonical,
+            MaybeRepn, MaybeForeign)
     ;
         Body0 = hlds_eqv_type(Type0),
         equiv_type.replace_in_type(TypeEqvMap, Type0, Type, _,
diff --git a/compiler/foreign.m b/compiler/foreign.m
index 86f499093..bc7167921 100644
--- a/compiler/foreign.m
+++ b/compiler/foreign.m
@@ -175,7 +175,7 @@ is_this_a_foreign_type(ModuleInfo, Type) = MaybeForeignTypeAssertions :-
             MaybeForeignTypeAssertions =
                 yes(foreign_type_and_assertions(ForeignTypeName, Assertions))
         ;
-            ( TypeBody = hlds_du_type(_, _, _, _)
+            ( TypeBody = hlds_du_type(_, _, _, _, _)
             ; TypeBody = hlds_eqv_type(_)
             ; TypeBody = hlds_solver_type(_)
             ; TypeBody = hlds_abstract_type(_)
diff --git a/compiler/hlds_data.m b/compiler/hlds_data.m
index 4716c2b1e..3d0bb113f 100644
--- a/compiler/hlds_data.m
+++ b/compiler/hlds_data.m
@@ -740,6 +740,9 @@ map_foldl_over_type_ctor_defns_2(Pred, _Name, !TypeCtorTable, !Acc) :-
                 % The ctors for this type.
                 du_type_ctors               :: one_or_more(constructor),
 
+                % The declared supertype for a subtype definition.
+                du_type_supertype           :: maybe(mer_type),
+
                 % Does this type have user-defined equality and comparison
                 % predicates?
                 du_type_canonical           :: maybe_canonical,
@@ -1038,7 +1041,7 @@ set_type_defn_prev_errors(X, !Defn) :-
 
 get_maybe_cheaper_tag_test(TypeBody) = CheaperTagTest :-
     (
-        TypeBody = hlds_du_type(_, _, MaybeRepn, _),
+        TypeBody = hlds_du_type(_, _, _, MaybeRepn, _),
         (
             MaybeRepn = no,
             unexpected($pred, "MaybeRepn = no")
diff --git a/compiler/hlds_out_module.m b/compiler/hlds_out_module.m
index 0678bdd7b..44724adfc 100644
--- a/compiler/hlds_out_module.m
+++ b/compiler/hlds_out_module.m
@@ -362,8 +362,19 @@ write_type_params_loop(Stream, TVarSet, HeadParam, TailParams, !IO) :-
 
 write_type_body(Info, Stream, _TypeCtor, TypeBody, Indent, TVarSet, !IO) :-
     (
-        TypeBody = hlds_du_type(Ctors, MaybeUserEqComp, MaybeRepn, Foreign),
+        TypeBody = hlds_du_type(Ctors, MaybeSuperType, MaybeUserEqComp,
+            MaybeRepn, Foreign),
         io.nl(Stream, !IO),
+        (
+            MaybeSuperType = yes(SuperType),
+            write_indent(Stream, Indent, !IO),
+            io.write_string(Stream, "=< ", !IO),
+            mercury_output_type(TVarSet, print_name_only, SuperType,
+                Stream, !IO),
+            io.nl(Stream, !IO)
+        ;
+            MaybeSuperType = no
+        ),
         MaybeSolverTypeDetails = no,
         MercInfo = Info ^ hoi_merc_out_info,
         (
diff --git a/compiler/inst_check.m b/compiler/inst_check.m
index ce53c03f8..40c7561d7 100644
--- a/compiler/inst_check.m
+++ b/compiler/inst_check.m
@@ -185,7 +185,7 @@ status_implies_type_defn_is_user_visible(Section, TypeStatus) = Visible :-
 get_du_functors_for_type_def(TypeDefn, Functors) :-
     get_type_defn_body(TypeDefn, TypeDefnBody),
     (
-        TypeDefnBody = hlds_du_type(Constructors, _, _, _),
+        TypeDefnBody = hlds_du_type(Constructors, _, _, _, _),
         list.map(constructor_to_functor_name_and_arity,
             one_or_more_to_list(Constructors), Functors)
     ;
@@ -493,7 +493,7 @@ check_for_type_bound_insts(ForTypeKind, [BoundInst | BoundInsts],
             ForTypeKind = ftk_user(TypeCtor, TypeDefn),
             get_type_defn_body(TypeDefn, TypeDefnBody),
             (
-                TypeDefnBody = hlds_du_type(OoMConstructors, _, _, _),
+                TypeDefnBody = hlds_du_type(OoMConstructors, _, _, _, _),
                 Constructors = one_or_more_to_list(OoMConstructors),
                 (
                     ConsSymName = unqualified(ConsName),
@@ -1195,7 +1195,7 @@ diagnose_mismatches_from_type(BoundInsts, TypeDefnOrBuiltin,
         TypeCtorAndDefn = type_ctor_and_defn(_TypeCtor, TypeDefn),
         get_type_defn_body(TypeDefn, TypeDefnBody),
         (
-            TypeDefnBody = hlds_du_type(Constructors, _, _, _),
+            TypeDefnBody = hlds_du_type(Constructors, _, _, _, _),
             find_mismatches_from_user(one_or_more_to_list(Constructors), 1,
                 BoundInsts, 0, NumMismatches, cord.init, MismatchPiecesCord)
         ;
diff --git a/compiler/intermod.m b/compiler/intermod.m
index 5a5a3383a..d2c902d2d 100644
--- a/compiler/intermod.m
+++ b/compiler/intermod.m
@@ -1157,8 +1157,8 @@ gather_opt_export_types_in_type_defn(TypeCtor, TypeDefn0, !IntermodInfo) :-
     ( if should_opt_export_type_defn(ModuleName, TypeCtor, TypeDefn0) then
         hlds_data.get_type_defn_body(TypeDefn0, TypeBody0),
         (
-            TypeBody0 = hlds_du_type(Ctors, MaybeUserEqComp0, MaybeRepn,
-                MaybeForeign0),
+            TypeBody0 = hlds_du_type(Ctors, MaybeSuperType, MaybeUserEqComp0,
+                MaybeRepn, MaybeForeign0),
             module_info_get_globals(ModuleInfo, Globals),
             globals.get_target(Globals, Target),
 
@@ -1188,8 +1188,8 @@ gather_opt_export_types_in_type_defn(TypeCtor, TypeDefn0, !IntermodInfo) :-
                     MaybeUserEqComp0, MaybeUserEqComp, !IntermodInfo),
                 MaybeForeign = MaybeForeign0
             ),
-            TypeBody = hlds_du_type(Ctors, MaybeUserEqComp, MaybeRepn,
-                MaybeForeign),
+            TypeBody = hlds_du_type(Ctors, MaybeSuperType, MaybeUserEqComp,
+                MaybeRepn, MaybeForeign),
             hlds_data.set_type_defn_body(TypeBody, TypeDefn0, TypeDefn)
         ;
             TypeBody0 = hlds_foreign_type(ForeignTypeBody0),
@@ -1556,7 +1556,8 @@ intermod_write_type(OutInfo, Stream, TypeCtor - TypeDefn,
     hlds_data.get_type_defn_context(TypeDefn, Context),
     TypeCtor = type_ctor(Name, _Arity),
     (
-        Body = hlds_du_type(Ctors, MaybeUserEqComp, MaybeRepnA, _MaybeForeign),
+        Body = hlds_du_type(Ctors, MaybeSuperType, MaybeUserEqComp,
+            MaybeRepnA, _MaybeForeign),
         (
             MaybeRepnA = no,
             unexpected($pred, "MaybeRepnA = no")
@@ -1566,7 +1567,7 @@ intermod_write_type(OutInfo, Stream, TypeCtor - TypeDefn,
         ),
         % XXX TYPE_REPN We should output information about any direct args
         % as a separate type_repn item.
-        DetailsDu = type_details_du(Ctors, MaybeUserEqComp,
+        DetailsDu = type_details_du(MaybeSuperType, Ctors, MaybeUserEqComp,
             MaybeDirectArgCtors),
         TypeBody = parse_tree_du_type(DetailsDu)
     ;
@@ -1593,7 +1594,7 @@ intermod_write_type(OutInfo, Stream, TypeCtor - TypeDefn,
         (
             Body = hlds_foreign_type(ForeignTypeBody)
         ;
-            Body = hlds_du_type(_, _, _, MaybeForeignTypeBody),
+            Body = hlds_du_type(_, _, _, _, MaybeForeignTypeBody),
             MaybeForeignTypeBody = yes(ForeignTypeBody)
         ),
         ForeignTypeBody = foreign_type_body(MaybeC, MaybeJava,
@@ -1649,7 +1650,7 @@ intermod_write_type(OutInfo, Stream, TypeCtor - TypeDefn,
         true
     ),
     ( if
-        Body = hlds_du_type(_, _, MaybeRepnB, _),
+        Body = hlds_du_type(_, _, _, MaybeRepnB, _),
         MaybeRepnB = yes(RepnB),
         RepnB = du_type_repn(CtorRepns, _, _, DuTypeKind, _),
         DuTypeKind = du_type_kind_foreign_enum(Lang)
diff --git a/compiler/make_hlds_passes.m b/compiler/make_hlds_passes.m
index e79d716b7..8d44b0af6 100644
--- a/compiler/make_hlds_passes.m
+++ b/compiler/make_hlds_passes.m
@@ -90,7 +90,7 @@
 %---------------------------------------------------------------------------%
 
 do_parse_tree_to_hlds(AugCompUnit, Globals, DumpBaseFileName, MQInfo0,
-        TypeEqvMapMap, UsedModules, !:QualInfo,
+        TypeEqvMap, UsedModules, !:QualInfo,
         !:FoundInvalidType, !:FoundInvalidInstOrMode, !:ModuleInfo, !:Specs) :-
     AugCompUnit = aug_compilation_unit(ModuleName, ModuleNameContext,
         ModuleVersionNumbers, _, _, _, _, _, _, _),
@@ -307,9 +307,9 @@ do_parse_tree_to_hlds(AugCompUnit, Globals, DumpBaseFileName, MQInfo0,
     % would allow us to generate better error messages.
     (
         !.FoundInvalidType = did_not_find_invalid_type,
-        % Add constructors for du types to the HLDS, and check that
-        % Mercury types defined solely by foreign types have a definition
-        % that works for the target backend.
+        % Add constructors for du types to the HLDS, check subtype definitions,
+        % and check that Mercury types defined solely by foreign types have a
+        % definition that works for the target backend.
         %
         % This must be done after adding all type definitions and all
         % `:- pragma foreign_type' declarations. If there were errors
@@ -317,7 +317,7 @@ do_parse_tree_to_hlds(AugCompUnit, Globals, DumpBaseFileName, MQInfo0,
         % a compiler abort.
         module_info_get_type_table(!.ModuleInfo, TypeTable0),
         foldl3_over_type_ctor_defns(
-            add_du_ctors_check_foreign_type_for_cur_backend,
+            add_du_ctors_check_subtype_check_foreign_type(TypeTable0),
             TypeTable0, !FoundInvalidType, !ModuleInfo, !Specs)
     ;
         !.FoundInvalidType = found_invalid_type
@@ -339,7 +339,7 @@ do_parse_tree_to_hlds(AugCompUnit, Globals, DumpBaseFileName, MQInfo0,
     module_info_optimize(!ModuleInfo),
 
     % The old pass 3.
-    init_qual_info(MQInfo0, TypeEqvMapMap, !:QualInfo),
+    init_qual_info(MQInfo0, TypeEqvMap, !:QualInfo),
 
     % Add clauses to their predicates.
     list.foldl3(add_clause, ItemClauses,
diff --git a/compiler/ml_type_gen.m b/compiler/ml_type_gen.m
index ef5644bdc..1d7812b5d 100644
--- a/compiler/ml_type_gen.m
+++ b/compiler/ml_type_gen.m
@@ -201,7 +201,9 @@ ml_gen_hld_type_defn(ModuleInfo, Target, TypeCtor, TypeDefn, !ClassDefns) :-
         % see our BABEL'01 paper "Compiling Mercury to the .NET CLR".
         % The same issue arises for some of the other kinds of types.
     ;
-        TypeBody = hlds_du_type(_Ctors, MaybeUserEqComp, MaybeRepn, _Foreign),
+        TypeBody = hlds_du_type(_Ctors, _MaybeSuperType, MaybeUserEqComp,
+            MaybeRepn, _Foreign),
+        % XXX SUBTYPE
         (
             MaybeRepn = no,
             unexpected($pred, "MaybeRepn = no")
diff --git a/compiler/ml_unify_gen_test.m b/compiler/ml_unify_gen_test.m
index 8e34926e3..10b8764e5 100644
--- a/compiler/ml_unify_gen_test.m
+++ b/compiler/ml_unify_gen_test.m
@@ -371,7 +371,7 @@ ml_get_maybe_cheaper_tag_test(Info, Type, CheaperTagTest) :-
     ( if
         search_type_ctor_defn(TypeTable, TypeCtor, TypeDefn),
         get_type_defn_body(TypeDefn, TypeBody),
-        TypeBody = hlds_du_type(_, _, MaybeRepn, _),
+        TypeBody = hlds_du_type(_, _, _, MaybeRepn, _),
         MaybeRepn = yes(Repn)
     then
         CheaperTagTest = Repn ^ dur_cheaper_tag_test
diff --git a/compiler/ml_unify_gen_util.m b/compiler/ml_unify_gen_util.m
index 56bb46156..da49d1776 100644
--- a/compiler/ml_unify_gen_util.m
+++ b/compiler/ml_unify_gen_util.m
@@ -592,7 +592,8 @@ ml_gen_hl_tag_field_id(ModuleInfo, Target, Type) = FieldId :-
     lookup_type_ctor_defn(TypeTable, TypeCtor, TypeDefn),
     hlds_data.get_type_defn_body(TypeDefn, TypeDefnBody),
     (
-        TypeDefnBody = hlds_du_type(_, _, MaybeRepn, _),
+        TypeDefnBody = hlds_du_type(_, _MaybeSuperType, _, MaybeRepn, _),
+        % XXX SUBTYPE Type representation depends on base type.
         (
             MaybeRepn = no,
             unexpected($pred, "MaybeRepn = no")
diff --git a/compiler/module_qual.qualify_items.m b/compiler/module_qual.qualify_items.m
index 73c6b31a5..7e533d92d 100644
--- a/compiler/module_qual.qualify_items.m
+++ b/compiler/module_qual.qualify_items.m
@@ -648,10 +648,23 @@ qualify_type_defn_eqv(InInt, Context, TypeCtor, DetailsEqv0, DetailsEqv,
     mq_info::in, mq_info::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-qualify_type_defn_du(InInt, _Context, TypeCtor, DetailsDu0, DetailsDu,
+qualify_type_defn_du(InInt, Context, TypeCtor, DetailsDu0, DetailsDu,
         !Info, !Specs) :-
-    DetailsDu0 = type_details_du(OoMCtors0, MaybeUserEqComp0,
+    DetailsDu0 = type_details_du(MaybeSuperType0, OoMCtors0, MaybeUserEqComp0,
         MaybeDirectArgCtors0),
+    (
+        MaybeSuperType0 = yes(SuperType0),
+        ErrorContext = mqec_type_defn(Context, TypeCtor),
+        % Note that this will not prevent a subtype defined in an interface
+        % section from referring to an abstract type as its supertype.
+        % That will be checked while checking other subtype conditions.
+        qualify_type(InInt, ErrorContext, SuperType0, SuperType,
+            !Info, !Specs),
+        MaybeSuperType = yes(SuperType)
+    ;
+        MaybeSuperType0 = no,
+        MaybeSuperType = no
+    ),
     OoMCtors0 = one_or_more(HeadCtor0, TailCtors0),
     qualify_constructor(InInt, TypeCtor, HeadCtor0, HeadCtor, !Info, !Specs),
     qualify_constructors(InInt, TypeCtor, TailCtors0, TailCtors,
@@ -663,7 +676,7 @@ qualify_type_defn_du(InInt, _Context, TypeCtor, DetailsDu0, DetailsDu,
     % Thus we don't module-qualify them here.
     MaybeUserEqComp = MaybeUserEqComp0,
     MaybeDirectArgCtors = MaybeDirectArgCtors0,
-    DetailsDu = type_details_du(OoMCtors, MaybeUserEqComp,
+    DetailsDu = type_details_du(MaybeSuperType, OoMCtors, MaybeUserEqComp,
         MaybeDirectArgCtors).
 
 :- pred qualify_constructors(mq_in_interface::in, type_ctor::in,
diff --git a/compiler/parse_tree_out.m b/compiler/parse_tree_out.m
index 794d520d8..13c7f4bfd 100644
--- a/compiler/parse_tree_out.m
+++ b/compiler/parse_tree_out.m
@@ -1331,10 +1331,19 @@ mercury_output_item_type_defn(Info, Stream, ItemTypeDefn, !IO) :-
         io.write_string(Stream, ".\n", !IO)
     ;
         TypeDefn = parse_tree_du_type(DetailsDu),
-        DetailsDu = type_details_du(OoMCtors, MaybeCanonical, MaybeDirectArgs),
+        DetailsDu = type_details_du(MaybeSuperType, OoMCtors, MaybeCanonical,
+            MaybeDirectArgs),
         mercury_output_begin_type_decl(Stream, non_solver_type, !IO),
         mercury_output_term(TypeVarSet, print_name_only, TypeTerm,
             Stream, !IO),
+        (
+            MaybeSuperType = no
+        ;
+            MaybeSuperType = yes(SuperType),
+            io.write_string(Stream, " =< ", !IO),
+            mercury_output_type(TypeVarSet, print_name_only, SuperType,
+                Stream, !IO)
+        ),
         OoMCtors = one_or_more(HeadCtor, TailCtors),
         mercury_output_ctors(TypeVarSet, yes, HeadCtor, TailCtors,
             Stream, !IO),
diff --git a/compiler/parse_type_defn.m b/compiler/parse_type_defn.m
index 7b9486c9e..87e8adb55 100644
--- a/compiler/parse_type_defn.m
+++ b/compiler/parse_type_defn.m
@@ -169,8 +169,24 @@ parse_du_type_defn(ModuleName, VarSet, HeadTerm, BodyTerm, Context, SeqNum,
 
     ContextPieces =
         cord.from_list([words("On the left hand side of type definition:")]),
-    parse_type_defn_head(ContextPieces, ModuleName, VarSet, HeadTerm,
-        MaybeTypeCtorAndArgs),
+    ( if
+        HeadTerm = functor(atom("=<"), HeadArgs, _HeadContext),
+        HeadArgs = [SubTypeTerm, SuperTypeTerm]
+    then
+        parse_type_defn_head(ContextPieces, ModuleName, VarSet, SubTypeTerm,
+            MaybeTypeCtorAndArgs),
+        SuperTypeContextPieces =
+            cord.from_list([words("In the supertype part of a"),
+                words("subtype definition:")]),
+        parse_supertype(VarSet, SuperTypeContextPieces, SuperTypeTerm,
+            MaybeSuperType0),
+        SuperTypeContext = get_term_context(SuperTypeTerm)
+    else
+        parse_type_defn_head(ContextPieces, ModuleName, VarSet, HeadTerm,
+            MaybeTypeCtorAndArgs),
+        MaybeSuperType0 = ok1(no),
+        SuperTypeContext = term.dummy_context_init
+    ),
     du_type_rhs_ctors_and_where_terms(BodyTerm, CtorsTerm, MaybeWhereTerm),
     parse_maybe_exist_quant_constructors(ModuleName, VarSet, CtorsTerm,
         MaybeOneOrMoreCtors),
@@ -185,6 +201,7 @@ parse_du_type_defn(ModuleName, VarSet, HeadTerm, BodyTerm, Context, SeqNum,
     ( if
         SolverSpecs = [],
         MaybeTypeCtorAndArgs = ok2(Name, Params),
+        MaybeSuperType0 = ok1(MaybeSuperType),
         MaybeOneOrMoreCtors = ok1(OneOrMoreCtors),
         MaybeWhere = ok3(SolverTypeDetails, MaybeCanonical, MaybeDirectArgIs)
     then
@@ -193,22 +210,31 @@ parse_du_type_defn(ModuleName, VarSet, HeadTerm, BodyTerm, Context, SeqNum,
         % if SolverTypeDetails is yes(...).
         expect(unify(SolverTypeDetails, no), $pred,
             "discriminated union type has solver type details"),
+        (
+            MaybeSuperType = yes(SuperType),
+            check_supertype_vars(Params, VarSet, SuperType, SuperTypeContext,
+                [], ErrorSpecs0)
+        ;
+            MaybeSuperType = no,
+            ErrorSpecs0 = []
+        ),
         OneOrMoreCtors = one_or_more(HeadCtor, TailCtors),
         Ctors = [HeadCtor | TailCtors],
-        process_du_ctors(Params, VarSet, BodyTerm, Ctors, [], CtorsSpecs),
+        process_du_ctors(Params, VarSet, BodyTerm, Ctors,
+            ErrorSpecs0, ErrorSpecs1),
         (
             MaybeDirectArgIs = yes(DirectArgCtors),
             check_direct_arg_ctors(Ctors, DirectArgCtors, BodyTerm,
-                CtorsSpecs, ErrorSpecs)
+                ErrorSpecs1, ErrorSpecs)
         ;
             MaybeDirectArgIs = no,
-            ErrorSpecs = CtorsSpecs
+            ErrorSpecs = ErrorSpecs1
         ),
         (
             ErrorSpecs = [],
             varset.coerce(VarSet, TypeVarSet),
-            DetailsDu = type_details_du(OneOrMoreCtors, MaybeCanonical,
-                MaybeDirectArgIs),
+            DetailsDu = type_details_du(MaybeSuperType, OneOrMoreCtors,
+                MaybeCanonical, MaybeDirectArgIs),
             TypeDefn = parse_tree_du_type(DetailsDu),
             ItemTypeDefn = item_type_defn_info(Name, Params, TypeDefn,
                 TypeVarSet, Context, SeqNum),
@@ -221,6 +247,7 @@ parse_du_type_defn(ModuleName, VarSet, HeadTerm, BodyTerm, Context, SeqNum,
     else
         Specs = SolverSpecs ++
             get_any_errors2(MaybeTypeCtorAndArgs) ++
+            get_any_errors1(MaybeSuperType0) ++
             get_any_errors1(MaybeOneOrMoreCtors) ++
             get_any_errors3(MaybeWhere),
         MaybeIOM = error1(Specs)
@@ -496,6 +523,28 @@ convert_constructor_arg_list_2(ModuleName, VarSet, MaybeCtorFieldName,
         MaybeArgs = error1(Specs)
     ).
 
+:- pred check_supertype_vars(list(type_param)::in, varset::in, mer_type::in,
+    prog_context::in, list(error_spec)::in, list(error_spec)::out) is det.
+
+check_supertype_vars(Params, VarSet, SuperType, Context, !Specs) :-
+    type_vars(SuperType, VarsInSuperType0),
+    list.sort_and_remove_dups(VarsInSuperType0, VarsInSuperType),
+    list.delete_elems(VarsInSuperType, Params, FreeVars),
+    (
+        FreeVars = []
+    ;
+        FreeVars = [_ | _],
+        varset.coerce(VarSet, GenericVarSet),
+        FreeVarsStr = mercury_vars_to_name_only(GenericVarSet, FreeVars),
+        Pieces = [words("Error: free type"),
+            words(choose_number(FreeVars, "parameter", "parameters")),
+            words(FreeVarsStr),
+            words("in supertype part of subtype definition."), nl],
+        Spec = simplest_spec($pred, severity_error, phase_term_to_parse_tree,
+            Context, Pieces),
+        !:Specs = [Spec | !.Specs]
+    ).
+
 :- pred process_du_ctors(list(type_param)::in, varset::in, term::in,
     list(constructor)::in, list(error_spec)::in, list(error_spec)::out) is det.
 
@@ -1484,53 +1533,64 @@ parse_type_defn_head(ContextPieces, ModuleName, VarSet, Term,
             MaybeSymNameArgs = ok2(SymName, ArgTerms),
             % Check that SymName is allowed to be a type constructor name.
             check_user_type_name(SymName, Context, NameSpecs),
-            % Check that all the ArgTerms are variables.
-            term_list_to_var_list_and_nonvars(ArgTerms, ParamVars,
-                NonVarArgTerms),
-            (
-                NonVarArgTerms = [],
-                % Check that all the ParamVars are distinct.
-                bag.from_list(ParamVars, ParamsBag),
-                bag.to_list_only_duplicates(ParamsBag, DupParamVars),
+            ( if
+                unqualify_name(SymName) = "=<",
+                list.length(ArgTerms, 2)
+            then
+                % This looks like an incorrect subtype definition so do not
+                % suggest that the arguments must be variables.
+                MaybeTypeCtorAndArgs = error2(NameSpecs)
+            else
+                % Check that all the ArgTerms are variables.
+                term_list_to_var_list_and_nonvars(ArgTerms, ParamVars,
+                    NonVarArgTerms),
                 (
-                    DupParamVars = [],
+                    NonVarArgTerms = [],
+                    % Check that all the ParamVars are distinct.
+                    bag.from_list(ParamVars, ParamsBag),
+                    bag.to_list_only_duplicates(ParamsBag, DupParamVars),
                     (
-                        NameSpecs = [],
-                        list.map(term.coerce_var, ParamVars, PrgParamVars),
-                        MaybeTypeCtorAndArgs = ok2(SymName, PrgParamVars)
+                        DupParamVars = [],
+                        (
+                            NameSpecs = [],
+                            list.map(term.coerce_var, ParamVars, PrgParamVars),
+                            MaybeTypeCtorAndArgs = ok2(SymName, PrgParamVars)
+                        ;
+                            NameSpecs = [_ | _],
+                            MaybeTypeCtorAndArgs = error2(NameSpecs)
+                        )
                     ;
-                        NameSpecs = [_ | _],
-                        MaybeTypeCtorAndArgs = error2(NameSpecs)
+                        DupParamVars = [_ | _],
+                        DupParamVarNames = list.map(
+                            mercury_var_to_name_only(VarSet), DupParamVars),
+                        Params = choose_number(DupParamVars,
+                            "the parameter", "the parameters"),
+                        IsOrAre = is_or_are(DupParamVars),
+                        Pieces = cord.list(ContextPieces) ++
+                            [lower_case_next_if_not_first,
+                            words("Error: type parameters must be unique,"),
+                            words("but"), words(Params)] ++
+                            list_to_pieces(DupParamVarNames) ++
+                            [words(IsOrAre), words("duplicated."), nl],
+                        Spec = simplest_spec($pred, severity_error,
+                            phase_term_to_parse_tree, Context, Pieces),
+                        MaybeTypeCtorAndArgs = error2([Spec | NameSpecs])
                     )
                 ;
-                    DupParamVars = [_ | _],
-                    DupParamVarNames = list.map(
-                        mercury_var_to_name_only(VarSet), DupParamVars),
-                    Params = choose_number(DupParamVars,
-                        "the parameter", "the parameters"),
-                    IsOrAre = is_or_are(DupParamVars),
+                    NonVarArgTerms = [_ | _],
+                    NonVarArgTermStrs = list.map(describe_error_term(VarSet),
+                        NonVarArgTerms),
+                    IsOrAre = is_or_are(NonVarArgTermStrs),
                     Pieces = cord.list(ContextPieces) ++
                         [lower_case_next_if_not_first,
-                        words("Error: type parameters must be unique, but"),
-                        words(Params)] ++ list_to_pieces(DupParamVarNames) ++
-                        [words(IsOrAre), words("duplicated."), nl],
+                        words("Error: type parameters must be variables,"),
+                        words("but")] ++
+                        list_to_quoted_pieces(NonVarArgTermStrs) ++
+                        [words(IsOrAre), words("not."), nl],
                     Spec = simplest_spec($pred, severity_error,
                         phase_term_to_parse_tree, Context, Pieces),
                     MaybeTypeCtorAndArgs = error2([Spec | NameSpecs])
                 )
-            ;
-                NonVarArgTerms = [_ | _],
-                NonVarArgTermStrs = list.map(describe_error_term(VarSet),
-                    NonVarArgTerms),
-                IsOrAre = is_or_are(NonVarArgTermStrs),
-                Pieces = cord.list(ContextPieces) ++
-                    [lower_case_next_if_not_first,
-                    words("Error: type parameters must be variables, but")] ++
-                    list_to_quoted_pieces(NonVarArgTermStrs) ++
-                    [words(IsOrAre), words("not."), nl],
-                Spec = simplest_spec($pred, severity_error,
-                    phase_term_to_parse_tree, Context, Pieces),
-                MaybeTypeCtorAndArgs = error2([Spec | NameSpecs])
             )
         )
     ).
@@ -1602,6 +1662,34 @@ check_no_free_body_vars(TVarSet, ParamTVars, BodyType, BodyContext, Specs) :-
         Specs = [Spec]
     ).
 
+%-----------------------------------------------------------------------------e
+
+:- pred parse_supertype(varset::in, cord(format_component)::in, term::in,
+    maybe1(maybe(mer_type))::out) is det.
+
+parse_supertype(VarSet, ContextPieces, Term, Result) :-
+    parse_type(no_allow_ho_inst_info(wnhii_supertype), VarSet,
+        ContextPieces, Term, MaybeType),
+    (
+        MaybeType = ok1(Type),
+        ( if type_to_ctor_and_args(Type, _TypeCtor, _Args) then
+            Result = ok1(yes(Type))
+        else
+            Context = get_term_context(Term),
+            TermStr = describe_error_term(VarSet, Term),
+            Pieces = cord.list(ContextPieces) ++
+                [lower_case_next_if_not_first,
+                words("Error: expected a type constructor,"),
+                words("got"), quote(TermStr), suffix("."), nl],
+            Spec = simplest_spec($pred, severity_error,
+                phase_term_to_parse_tree, Context, Pieces),
+            Result = error1([Spec])
+        )
+    ;
+        MaybeType = error1(Specs),
+        Result = error1(Specs)
+    ).
+
 %-----------------------------------------------------------------------------e
 :- end_module parse_tree.parse_type_defn.
 %-----------------------------------------------------------------------------e
diff --git a/compiler/parse_type_name.m b/compiler/parse_type_name.m
index 216c4269e..2a94df871 100644
--- a/compiler/parse_type_name.m
+++ b/compiler/parse_type_name.m
@@ -40,6 +40,7 @@
     ;       wnhii_func_arg
     ;       wnhii_func_return_arg
     ;       wnhii_type_qual             % NYI
+    ;       wnhii_supertype
     ;       wnhii_eqv_type_defn_body
     ;       wnhii_solver_type_defn
     ;       wnhii_class_constraint
@@ -734,7 +735,9 @@ is_known_type_name_args(Name, Args, KnownType) :-
         Name = "{}",
         KnownType = known_type_compound(kctk_tuple(Args))
     ;
-        Name = "=",
+        ( Name = "="
+        ; Name = "=<"
+        ),
         (
             ( Args = []
             ; Args = [_]
@@ -808,6 +811,9 @@ no_ho_inst_allowed_result(ContextPieces, Why, VarSet, Term) = Result :-
     ;
         Why = wnhii_type_qual,
         Place = "a type used for type qualification"
+    ;
+        Why = wnhii_supertype,
+        Place = "a supertype of a subtype"
     ;
         Why = wnhii_eqv_type_defn_body,
         Place = "the definition of an equivalence type"
diff --git a/compiler/post_term_analysis.m b/compiler/post_term_analysis.m
index 1c7d7d090..7aae59f50 100644
--- a/compiler/post_term_analysis.m
+++ b/compiler/post_term_analysis.m
@@ -253,7 +253,7 @@ special_pred_needs_term_check(ModuleInfo, SpecialPredId, TypeDefn)
 
 get_user_unify_compare(ModuleInfo, TypeBody, MaybeCanonical) :-
     (
-        TypeBody = hlds_du_type(_, MaybeCanonical, _, _)
+        TypeBody = hlds_du_type(_, _, MaybeCanonical, _, _)
     ;
         TypeBody = hlds_solver_type(DetailsSolver),
         DetailsSolver = type_details_solver(_, MaybeCanonical)
diff --git a/compiler/prog_data.m b/compiler/prog_data.m
index c4ebe1f17..6c106fce0 100644
--- a/compiler/prog_data.m
+++ b/compiler/prog_data.m
@@ -294,6 +294,9 @@ cons_id_is_const_struct(ConsId, ConstNum) :-
 
 :- type type_details_du
     --->    type_details_du(
+                % The supertype for a subtype definition.
+                du_supertype        :: maybe(mer_type),
+
                 % The list of data constructors (function symbols) defined
                 % by the type constructor.
                 du_ctors            :: one_or_more(constructor),
@@ -416,6 +419,8 @@ cons_id_is_const_struct(ConsId, ConstNum) :-
     --->    ctor(
                 % The ordinal number of the functor. The first functor
                 % in a type definition has ordinal number 0.
+                % XXX SUBTYPE For subtypes, the ordinal number needs to be
+                % retrieved from the base type.
                 cons_ordinal        :: uint32,
 
                 % Existential constraints, if any.
@@ -694,7 +699,7 @@ cons_id_is_const_struct(ConsId, ConstNum) :-
 :- type maybe_canonical
     --->    canon
     ;       noncanon(noncanonical).
-    
+
 :- type noncanonical
     --->    noncanon_uni_cmp(equality_pred, comparison_pred)
     ;       noncanon_uni_only(equality_pred)
diff --git a/compiler/prog_type.m b/compiler/prog_type.m
index 9d44a8d11..1d66c0794 100644
--- a/compiler/prog_type.m
+++ b/compiler/prog_type.m
@@ -994,7 +994,8 @@ du_type_is_notag(OoMCtors, MaybeCanonical) :-
     MaybeCanonical = canon.
 
 du_type_is_enum(DuDetails, NumFunctors) :-
-    DuDetails = type_details_du(OoMCtors, _MaybeCanonical,
+    % XXX SUBTYPE Whether a subtype is an enum depends on the base type.
+    DuDetails = type_details_du(_MaybeSuperType, OoMCtors, _MaybeCanonical,
         _MaybeDirectArgCtors),
     Ctors = one_or_more_to_list(OoMCtors),
     Ctors = [_, _ | _],
@@ -1016,7 +1017,9 @@ all_functors_are_enum([Ctor | Ctors], !NumFunctors) :-
     all_functors_are_enum(Ctors, !NumFunctors).
 
 du_type_is_dummy(DuDetails) :-
-    DuDetails = type_details_du(Ctors, MaybeCanonical, MaybeDirectArgCtors),
+    % XXX SUBTYPE Whether a subtype is a dummy type depends on the base type.
+    DuDetails = type_details_du(_MaybeSuperType, Ctors, MaybeCanonical,
+        MaybeDirectArgCtors),
     Ctors = one_or_more(Ctor, []),
     Ctor = ctor(_Ordinal, MaybeExistConstraints, _FunctorName, [], 0,
         _Context),
diff --git a/compiler/recompilation.check.m b/compiler/recompilation.check.m
index 6e1fdd120..467d730b3 100644
--- a/compiler/recompilation.check.m
+++ b/compiler/recompilation.check.m
@@ -1265,7 +1265,7 @@ check_type_defn_ambiguity_with_functor(RecompAvail, TypeCtor, TypeDefn,
         )
     ;
         TypeDefn = parse_tree_du_type(DetailsDu),
-        DetailsDu = type_details_du(Ctors, _, _),
+        DetailsDu = type_details_du(_MaybeSuperType, Ctors, _, _),
         list.foldl(check_functor_ambiguities(RecompAvail, TypeCtor),
             one_or_more_to_list(Ctors), !Info)
     ).
diff --git a/compiler/recompilation.usage.m b/compiler/recompilation.usage.m
index 33bdbce66..19b335f86 100644
--- a/compiler/recompilation.usage.m
+++ b/compiler/recompilation.usage.m
@@ -1097,7 +1097,13 @@ find_items_used_by_type_and_mode(TypeAndMode, !Info) :-
 
 find_items_used_by_type_body(TypeBody, !Info) :-
     (
-        TypeBody = hlds_du_type(Ctors, _, _, _),
+        TypeBody = hlds_du_type(Ctors, MaybeSuperType, _, _, _),
+        (
+            MaybeSuperType = yes(SuperType),
+            find_items_used_by_type(SuperType, !Info)
+        ;
+            MaybeSuperType = no
+        ),
         list.foldl(find_items_used_by_ctor, one_or_more_to_list(Ctors), !Info)
     ;
         TypeBody = hlds_eqv_type(EqvType),
diff --git a/compiler/resolve_unify_functor.m b/compiler/resolve_unify_functor.m
index 75d0aef0a..fe7bba7b6 100644
--- a/compiler/resolve_unify_functor.m
+++ b/compiler/resolve_unify_functor.m
@@ -585,7 +585,7 @@ get_constructor_containing_field(ModuleInfo, TermType, FieldSymName,
     lookup_type_ctor_defn(TypeTable, TermTypeCtor, TermTypeDefn),
     hlds_data.get_type_defn_body(TermTypeDefn, TermTypeBody),
     (
-        TermTypeBody = hlds_du_type(Ctors, _, _, _),
+        TermTypeBody = hlds_du_type(Ctors, _, _, _, _),
         FieldName = unqualify_name(FieldSymName),
         get_constructor_containing_field_loop(TermTypeCtor,
             one_or_more_to_list(Ctors), FieldName, ConsId, FieldNumber)
diff --git a/compiler/simplify_goal_ite.m b/compiler/simplify_goal_ite.m
index daadb5e2e..5dcb8f05e 100644
--- a/compiler/simplify_goal_ite.m
+++ b/compiler/simplify_goal_ite.m
@@ -419,8 +419,8 @@ warn_switch_for_ite_cond(ModuleInfo, VarTypes, Cond, !CondCanSwitch) :-
 
 can_switch_on_type(TypeBody) = CanSwitchOnType :-
     (
-        TypeBody = hlds_du_type(Ctors, _MaybeUserEq, _MaybeRepn,
-            _MaybeForeignType),
+        TypeBody = hlds_du_type(Ctors, _MaybeSuperType, _MaybeUserEq,
+            _MaybeRepn, _MaybeForeignType),
         % We don't care about _MaybeUserEq, since the unification with *any*
         % functor of the type indicates that we are deconstructing the physical
         % representation, not the logical value.
diff --git a/compiler/switch_util.m b/compiler/switch_util.m
index 6c05506cf..720fc9241 100644
--- a/compiler/switch_util.m
+++ b/compiler/switch_util.m
@@ -932,7 +932,7 @@ type_range(ModuleInfo, TypeCtorCat, Type, Min, Max, NumValues) :-
         lookup_type_ctor_defn(TypeTable, TypeCtor, TypeDefn),
         hlds_data.get_type_defn_body(TypeDefn, TypeBody),
         (
-            TypeBody = hlds_du_type(Constructors, _, _, _),
+            TypeBody = hlds_du_type(Constructors, _, _, _, _),
             Constructors = one_or_more(_HeadCtor, TailCtors),
             list.length(TailCtors, NumTailConstructors),
             % NumConstructors = 1 + NumTailConstructors
@@ -1416,7 +1416,7 @@ get_ptag_counts(Type, ModuleInfo, MaxPrimary, PtagCountMap) :-
     lookup_type_ctor_defn(TypeTable, TypeCtor, TypeDefn),
     hlds_data.get_type_defn_body(TypeDefn, TypeBody),
     (
-        TypeBody = hlds_du_type(_, _, MaybeRepn, _),
+        TypeBody = hlds_du_type(_, _, _, MaybeRepn, _),
         (
             MaybeRepn = no,
             unexpected($pred, "MaybeRepn = no")
diff --git a/compiler/table_gen.m b/compiler/table_gen.m
index cc9ae2df4..f3bc21670 100644
--- a/compiler/table_gen.m
+++ b/compiler/table_gen.m
@@ -2509,8 +2509,9 @@ gen_lookup_call_for_type(ArgTablingMethod0, CtorCat, Type, ArgVar, VarSeqNum,
             lookup_type_ctor_defn(TypeTable, TypeCtor, TypeDefn),
             hlds_data.get_type_defn_body(TypeDefn, TypeBody),
             ( if
-                TypeBody = hlds_du_type(Ctors, MaybeCanonical, MaybeRepn,
-                    _MaybeForeign),
+                TypeBody = hlds_du_type(Ctors, _MaybeSuperType, MaybeCanonical,
+                    MaybeRepn, _MaybeForeign),
+                % XXX SUBTYPE Anything to do?
                 MaybeCanonical = canon,
                 MaybeRepn = yes(Repn),
                 Repn ^ dur_kind = du_type_kind_mercury_enum
diff --git a/compiler/term_norm.m b/compiler/term_norm.m
index fb10e585e..2748c783e 100644
--- a/compiler/term_norm.m
+++ b/compiler/term_norm.m
@@ -152,7 +152,7 @@ find_weights(ModuleInfo, Weights) :-
 find_weights_for_type(TypeCtor - TypeDefn, !Weights) :-
     hlds_data.get_type_defn_body(TypeDefn, TypeBody),
     (
-        TypeBody = hlds_du_type(Constructors, _, _, _),
+        TypeBody = hlds_du_type(Constructors, _, _, _, _),
         hlds_data.get_type_defn_tparams(TypeDefn, TypeParams),
         list.foldl(find_weights_for_cons(TypeCtor, TypeParams),
             one_or_more_to_list(Constructors), !Weights)
diff --git a/compiler/type_ctor_info.m b/compiler/type_ctor_info.m
index 899cde0f0..7eb88393a 100644
--- a/compiler/type_ctor_info.m
+++ b/compiler/type_ctor_info.m
@@ -359,8 +359,8 @@ construct_type_ctor_info(TypeCtorGenInfo, ModuleInfo, RttiData) :-
                 UnivTVars, ExistTVars, MaybePseudoTypeInfo),
             Details = tcd_eqv(MaybePseudoTypeInfo)
         ;
-            TypeBody = hlds_du_type(_Ctors, MaybeCanonical, MaybeRepn,
-                _IsForeignType),
+            TypeBody = hlds_du_type(_Ctors, _MaybeSuperType, MaybeCanonical,
+                MaybeRepn, _IsForeignType),
             (
                 MaybeRepn = no,
                 unexpected($pred, "MaybeRepn = no")
@@ -403,7 +403,7 @@ construct_type_ctor_info(TypeCtorGenInfo, ModuleInfo, RttiData) :-
     some [!Flags] (
         !:Flags = set.init,
         (
-            TypeBody = hlds_du_type(_, _, _, _),
+            TypeBody = hlds_du_type(_, _, _, _, _),
             set.insert(kind_of_du_flag, !Flags)
         ;
             ( TypeBody = hlds_eqv_type(_)
diff --git a/compiler/type_util.m b/compiler/type_util.m
index 202f4a8cd..015f0dfdb 100644
--- a/compiler/type_util.m
+++ b/compiler/type_util.m
@@ -527,7 +527,7 @@ type_has_user_defined_equality_pred(ModuleInfo, Type, UserEqComp) :-
 type_body_has_user_defined_equality_pred(ModuleInfo, TypeBody, NonCanonical) :-
     require_complete_switch [TypeBody]
     (
-        TypeBody = hlds_du_type(_, _, _, MaybeForeignType),
+        TypeBody = hlds_du_type(_, _, _, _, MaybeForeignType),
         ( if
             MaybeForeignType = yes(ForeignTypeBody),
             module_info_get_globals(ModuleInfo, Globals),
@@ -608,7 +608,7 @@ type_body_definitely_has_no_user_defined_equality_pred(ModuleInfo, Type,
     module_info_get_globals(ModuleInfo, Globals),
     globals.get_target(Globals, Target),
     (
-        TypeBody = hlds_du_type(_, _, _, _),
+        TypeBody = hlds_du_type(_, _, _, _, _),
         ( if
             TypeBody ^ du_type_is_foreign_type = yes(ForeignTypeBody),
             have_foreign_type_for_backend(Target, ForeignTypeBody, yes)
@@ -683,7 +683,7 @@ type_body_has_solver_type_details(ModuleInfo, Type, SolverTypeDetails) :-
         Type = hlds_eqv_type(EqvType),
         type_has_solver_type_details(ModuleInfo, EqvType, SolverTypeDetails)
     ;
-        ( Type = hlds_du_type(_, _, _, _)
+        ( Type = hlds_du_type(_, _, _, _, _)
         ; Type = hlds_foreign_type(_)
         ; Type = hlds_abstract_type(_)
         ),
@@ -739,7 +739,7 @@ type_body_is_solver_type(ModuleInfo, TypeBody) :-
             IsSolverType = non_solver_type
         )
     ;
-        ( TypeBody = hlds_du_type(_, _, _, _)
+        ( TypeBody = hlds_du_type(_, _, _, _, _)
         ; TypeBody = hlds_foreign_type(_)
         ),
         IsSolverType = non_solver_type
@@ -773,7 +773,7 @@ type_body_is_solver_type_from_type_table(TypeTable, TypeBody) :-
             IsSolverType = no
         )
     ;
-        ( TypeBody = hlds_du_type(_, _, _, _)
+        ( TypeBody = hlds_du_type(_, _, _, _, _)
         ; TypeBody = hlds_foreign_type(_)
         ),
         IsSolverType = no
@@ -832,7 +832,7 @@ is_type_a_dummy_loop(TypeTable, Type, CoveredTypes) = IsDummy :-
             ( if search_type_ctor_defn(TypeTable, TypeCtor, TypeDefn) then
                 get_type_defn_body(TypeDefn, TypeBody),
                 (
-                    TypeBody = hlds_du_type(_, _, MaybeTypeRepn, _),
+                    TypeBody = hlds_du_type(_, _, _, MaybeTypeRepn, _),
                     (
                         MaybeTypeRepn = no,
                         unexpected($pred, "MaybeTypeRepn = no")
@@ -885,7 +885,7 @@ type_ctor_has_hand_defined_rtti(Type, Body) :-
     ),
     require_complete_switch [Body]
     (
-        Body = hlds_du_type(_, _, _, IsForeignType),
+        Body = hlds_du_type(_, _, _, _, IsForeignType),
         (
             IsForeignType = yes(_),
             HasHandDefinedRtti = no
@@ -1080,7 +1080,7 @@ classify_type_defn_body(TypeBody) = TypeCategory :-
     % XXX Why don't we have a category for solver types?
     % XXX Why do we classify abstract_enum_types as general?
     (
-        TypeBody = hlds_du_type(_, _, MaybeTypeRepn, _),
+        TypeBody = hlds_du_type(_, _, _, MaybeTypeRepn, _),
         (
             MaybeTypeRepn = no,
             unexpected($pred, "MaybeTypeRepn = no")
@@ -1295,7 +1295,7 @@ switch_type_num_functors(ModuleInfo, Type, NumFunctors) :-
         module_info_get_type_table(ModuleInfo, TypeTable),
         search_type_ctor_defn(TypeTable, TypeCtor, TypeDefn),
         hlds_data.get_type_defn_body(TypeDefn, TypeBody),
-        TypeBody = hlds_du_type(OoMConstructors, _, _, _),
+        TypeBody = hlds_du_type(OoMConstructors, _, _, _, _),
         OoMConstructors = one_or_more(_HeadCtor, TailCtors),
         NumFunctors = 1 + list.length(TailCtors)
     ).
@@ -1364,7 +1364,7 @@ cons_id_arg_types(ModuleInfo, VarType, ConsId, ArgTypes) :-
     module_info_get_type_table(ModuleInfo, TypeTable),
     search_type_ctor_defn(TypeTable, TypeCtor, TypeDefn),
     hlds_data.get_type_defn_body(TypeDefn, TypeDefnBody),
-    TypeDefnBody = hlds_du_type(OoMCtors, _, _, _),
+    TypeDefnBody = hlds_du_type(OoMCtors, _, _, _, _),
     OoMCtors = one_or_more(HeadCtor, TailCtors),
     ( Ctor = HeadCtor
     ; list.member(Ctor, TailCtors)
@@ -1402,7 +1402,7 @@ get_cons_repn_defn(ModuleInfo, ConsId, ConsIdConsRepn) :-
     module_info_get_type_table(ModuleInfo, TypeTable),
     search_type_ctor_defn(TypeTable, TypeCtor, TypeDefn),
     get_type_defn_body(TypeDefn, TypeBody),
-    TypeBody = hlds_du_type(_, _, MaybeRepn, _),
+    TypeBody = hlds_du_type(_, _, _, MaybeRepn, _),
     MaybeRepn = yes(Repn),
     Repn = du_type_repn(_, ConsRepnMap, _, _, _),
     ConsName = unqualify_name(ConsSymName),
diff --git a/compiler/unify_proc.m b/compiler/unify_proc.m
index 85118a0f2..24b8d7700 100644
--- a/compiler/unify_proc.m
+++ b/compiler/unify_proc.m
@@ -232,7 +232,7 @@ generate_unify_proc_body(SpecDefnInfo, X, Y, Clauses, !Info) :-
                 Clause, !Info),
             Clauses = [Clause]
         ;
-            TypeBody = hlds_du_type(_, _, MaybeRepn, _),
+            TypeBody = hlds_du_type(_, _, _, MaybeRepn, _),
             (
                 MaybeRepn = no,
                 unexpected($pred, "MaybeRepn = no")
@@ -974,7 +974,7 @@ generate_compare_proc_body(SpecDefnInfo, Res, X, Y, Clause, !Info) :-
             generate_compare_proc_body_solver(Context,
                 Res, X, Y, Clause, !Info)
         ;
-            TypeBody = hlds_du_type(_, _, MaybeRepn, _),
+            TypeBody = hlds_du_type(_, _, _, MaybeRepn, _),
             (
                 MaybeRepn = no,
                 unexpected($pred, "MaybeRepn = no")
@@ -2438,7 +2438,7 @@ generate_index_proc_body(SpecDefnInfo, X, Index, Clause, !Info) :-
         TypeBody = hlds_solver_type(_),
         unexpected($pred, "trying to create index proc for a solver type")
     ;
-        TypeBody = hlds_du_type(_, _, MaybeRepn, _),
+        TypeBody = hlds_du_type(_, _, _, MaybeRepn, _),
         (
             MaybeRepn = no,
             unexpected($pred, "MaybeRepn = no")
diff --git a/compiler/unused_imports.m b/compiler/unused_imports.m
index cefe7d556..d3aed3182 100644
--- a/compiler/unused_imports.m
+++ b/compiler/unused_imports.m
@@ -433,7 +433,7 @@ type_used_modules(_TypeCtor, TypeDefn, !UsedModules) :-
         DefinedInThisModule = yes,
         Visibility = type_visibility(TypeStatus),
         (
-            TypeBody = hlds_du_type(Ctors, _, _, _),
+            TypeBody = hlds_du_type(Ctors, _, _, _, _),
             list.foldl(ctor_used_modules(Visibility),
                 one_or_more_to_list(Ctors), !UsedModules)
         ;
diff --git a/compiler/xml_documentation.m b/compiler/xml_documentation.m
index b6df34e84..30c53692a 100644
--- a/compiler/xml_documentation.m
+++ b/compiler/xml_documentation.m
@@ -398,7 +398,7 @@ type_documentation(C, type_ctor(TypeName, TypeArity), TypeDefn, !Xmls) :-
 
 :- func type_xml_tag(hlds_type_body) = string.
 
-type_xml_tag(hlds_du_type(_, _, _, _)) = "du_type".
+type_xml_tag(hlds_du_type(_, _, _, _, _)) = "du_type".
 type_xml_tag(hlds_eqv_type(_)) = "eqv_type".
 type_xml_tag(hlds_foreign_type(_)) = "foreign_type".
 type_xml_tag(hlds_solver_type(_)) = "solver_type".
@@ -414,7 +414,7 @@ type_param_to_xml(TVarset, TVar) = Xml :-
 
 type_body_to_xml(C, TVarSet, TypeDefnBody) = Xmls :-
     (
-        TypeDefnBody = hlds_du_type(OoMCtors, _, _, _),
+        TypeDefnBody = hlds_du_type(OoMCtors, _, _, _, _),
         Ctors = one_or_more_to_list(OoMCtors),
         Xmls =
             [xml_list("constructors", constructor_to_xml(C, TVarSet), Ctors)]
diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
index 2c3ad70f9..894707b39 100644
--- a/doc/reference_manual.texi
+++ b/doc/reference_manual.texi
@@ -99,6 +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.
 * Exception handling:: Catching exceptions to recover from exceptional
                       situations.
 * Semantics::         Declarative and operational semantics of Mercury
@@ -1638,6 +1639,7 @@ or an explicit type qualification.
 * Lambda expressions::
 * Higher-order function applications::
 * Explicit type qualification::
+ at c * Type conversion expressions::
 @end menu
 
 @node Data-functors
@@ -1968,6 +1970,19 @@ 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 c A type conversion expression is a term of the form:
+
+ at c @example
+ at c coerce(Term)
+ at c @end example
+
+ at c @var{Term} must be a valid data-term.
+
+ at c @xref{Type conversions}.
+
 @node Variable scoping
 @section Variable scoping
 
@@ -2274,6 +2289,7 @@ There are several categories of derived types:
 * Discriminated unions::
 * Equivalence types::
 * Abstract types::
+* Subtypes::
 @end menu
 
 @node Discriminated unions
@@ -2379,6 +2395,7 @@ with the same name, arity, and result type in the same module.
 (There is no particularly good reason for this restriction;
 in the future we may allow several such functors
 as long as they have different argument types.)
+ at c That would likely conflict with subtypes.
 Note that excessive overloading of constructors
 can slow down type checking
 and can make the program confusing for human readers,
@@ -2437,6 +2454,7 @@ character
 string
 @{@}
 =
+=<
 pred
 func
 pure
@@ -2492,6 +2510,143 @@ named in the interface section of the module.
 Abstract types may be defined as either discriminated union types
 or as equivalence types.
 
+ at c -----------------------------------------------------------------------
+
+ at node Subtypes
+ at subsection Subtypes
+
+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}).
+
+A subtype is defined using the form
+ at example
+:- type @var{subtype} =< @var{supertype} ---> @var{body}.
+ at end example
+
+ at var{subtype} must be a name term
+whose arguments (if any) are distinct variables.
+
+ at var{supertype} must be a type (that may contain variables).
+After expanding out equivalences,
+the principal constructor must specify a discriminated union type
+whose @emph{definition} is in scope where the subtype definition occurs,
+by normal module visibility rules.
+
+The discriminated union type specified by @var{supertype}
+may itself be a subtype.
+Following a chain of visible subtype definitions,
+it must be possible to arrive at a @emph{base type},
+which is not a subtype.
+
+Any variable that occurs in @var{supertype} must occur in @var{subtype}.
+
+The @var{body} term is defined as
+a sequence of constructor definitions separated by semicolons.
+Any universally quantified type variable that occurs in @var{body}
+must occur in @var{subtype}.
+
+The constructor definitions must be a
+subset of the constructors of the supertype.
+If the supertype @samp{t} has constructor @samp{f(T1, ..., Tn)} then
+a subtype @samp{s =< t} may have a constructor @samp{f(S1, ..., Sn)}.
+For each @var{Si}, it must be that @samp{Si =< Ti}.
+
+(In the following discussion,
+assume that equivalence types are expanded out
+as required.)
+
+ at samp{S =< T} holds
+if @samp{S = f(S1, ..., Sn)}
+and @samp{T = f(T1, ..., Tn)} and
+for each pair of corresponding arguments @samp{Si =< Ti}.
+
+Otherwise, @samp{S =< T} holds
+if @samp{S = f(S1, ..., Sn)}
+and there is a visible definition @w{@samp{:- type f(R1, ..., Rn) =< U}},
+and for each pair of corresponding arguments @w{@samp{Si = Ri}} (unification),
+and @samp{U =< T}.
+In other words,
+any occurrences of @var{Ri} in @var{U} are substituted for @var{Si}
+to give @var{Usub},
+and @samp{Usub =< T} must hold.
+
+ at samp{P =< Q} holds for two higher order types @var{P} and @var{Q}
+iff @var{P} and @var{Q} are both @samp{pred} types or both @samp{func} types
+with the same arity,
+and @var{P} and @var{Q} have the same argument types.
+In addition,
+if either of @var{P} and @var{Q} has higher order inst information,
+then @var{P} and @var{Q} must have the same argument modes, determinism,
+and purity.
+(The current implementation does not admit subtyping in
+higher order arguments.)
+
+ at samp{P =< Q} holds if @var{P} and @var{Q} are both
+existentially quantified type variables, and @samp{P = Q}.
+
+There must be a one-to-one mapping between
+existentially quantified type variables
+for a constructor in the subtype definition
+and the same constructor in the supertype definition.
+The subtype constructor must repeat exactly the same set of
+existential class constraints on its existentially quantified type variables
+as in the supertype; the subtype constructor cannot add or remove any
+existential class constraints.
+
+Examples:
+
+ at example
+:- type list(T)
+    --->    []
+    ;       [T | list(T)].
+
+:- type non_empty_list(T) =< list(T)
+    --->    [T | list(T)].
+
+:- type non_empty_list_of_foo =< list(foo)
+    --->    [foo | list(foo)].
+
+:- type maybe_foo
+    --->    none
+    ;       some [T] foo(T) => fooable(T).
+
+:- type foo =< maybe_foo
+    --->    some [T] foo(T) => fooable(T).
+
+:- type task
+   --->     create(pred(int::in, io::di, uo::uo) is det)
+   ;        delete(pred(int::in, io::di, io::uo) is det).
+
+:- type create_task =< task
+   --->     create(pred(int::in, io::di, uo::uo) is det).
+ at end example
+
+A subtype may be exported as an abstract type
+by declaring only the name of the subtype in the
+interface section of a module (without the @samp{=< @var{supertype}} part).
+Then the subtype definition must be given in the implementation section of
+the same module.
+
+Example:
+
+ at example
+:- interface.
+
+:- type non_empty_list(T).  % abstract type
+
+:- implementation.
+
+:- import list.
+
+:- type non_empty_list(T) =< list(T)
+    --->    [T | list(T)].
+ at end example
+
+ at c -----------------------------------------------------------------------
+
 @node Predicate and function type declarations
 @section Predicate and function type declarations
 
@@ -6918,6 +7073,122 @@ good_example3_univ("foo"::in(bound("foo")), univ(42)::out).
 good_example3_univ("bar"::in(bound("bar")), univ("blah")::out).
 @end example
 
+ at c -----------------------------------------------------------------------
+
+ at c @node Type conversions
+ at c @chapter Type conversions
+
+ at c A term of type @samp{T1} may be converted to type @samp{T2}
+ at c using a type conversion expression:
+
+ at c @example
+ at c coerce(Term)
+ at c @end example
+
+ at c XXX disallow coerce/1 as a constructor name?
+
+ at c If @var{Term} has type @samp{T1} and the expression has type @samp{T2},
+ at c the coercion is type-correct iff
+ at c @samp{T1} and @samp{T2} are equivalent after
+ at c expanding out equivalence types
+ at c and replacing any subtypes with their base types
+ at c (@pxref{Subtypes}).
+
+ at c For example, if there is a subtype @samp{s =< t} and
+ at c a subtype @samp{non_empty_list(T) =< list(T)}
+ at c then coercions between these pairs of types are type-correct:
+
+ at c @example
+ at c s <-> t
+ at c list(s) <-> list(t)
+ at c non_empty_list(s) <-> non_empty_list(t)
+ at c list(s) <-> non_empty_list(s)
+ at c list(s) <-> non_empty_list(t)
+ at c @end example
+
+ at c If a subtype definition is not visible in the module
+ at c in which a @samp{coerce} operation occurs,
+ at c then the coercion is type-incorrect.
+
+ at c Coercions must also be mode-correct.
+ at c For a coercion where:
+
+ at c @itemize @bullet
+ at c @item
+ at c the input is @samp{X} with type @samp{s}
+
+ at c @item
+ at c the result is @samp{Y} with type @samp{t}
+
+ at c @item
+ at c @samp{Xi}, @samp{Xf} are the initial and final insts of @samp{X}
+
+ at c @item
+ at c @samp{Yi}, @samp{Yf} are the initial and final insts of @samp{Y}
+ at c @end itemize
+
+ at c @noindent
+ at c the coercion is mode-correct iff:
+
+ at c @itemize @bullet
+ at c @item
+ at c @samp{Xi} is a ground inst
+
+ at c @item
+ at c @samp{Xf = Xi}
+
+ at c @item
+ at c @samp{Yi} is free
+
+ at c @item
+ at c Yf is the greatest lower bound (glb) of @samp{Xi} and
+ at c the instantiatedness tree derived from @samp{t}
+ at c where all nodes are bound.
+ at c The glb must exist,
+ at c @samp{Yf} must be be ground,
+ at c and @samp{Yf} must be a valid inst of @samp{t}.
+ at c @end itemize
+
+ at c XXX partial order of insts not used elsewhere in reference manual
+
+ at c Intuitively,
+ at c coercing a ground term from subtype to supertype is always allowed,
+ at c but coercion from supertype to subtype is allowed only if
+ at c the term is approximated by an inst that indicates
+ at c the term would be a valid in the subtype.
+
+ at c Examples:
+
+ 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
+ at c :- inst citrus for fruit/0
+ at c     --->    lemon
+ at c     ;       orange.
+ at c
+ at c :- func f1(citrus) = fruit.
+ at c
+ at c f1(X) = coerce(X).  % correct
+ at c
+ at c :- func f2(fruit) = citrus.
+ at c
+ at c f2(X) = coerce(X).  % not mode-correct
+ 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).  % correct
+ at c @end example
+
+ at c -----------------------------------------------------------------------
+
 @node Exception handling
 @chapter Exception handling
 
@@ -8101,13 +8372,21 @@ using a declaration of the form
 This defines @var{MercuryTypeName}
 as a synonym for type @var{ForeignTypeDescriptor}
 defined in the foreign language @var{Lang}.
-You must declare @var{MercuryTypeName}
-using a (possibly abstract) @samp{:- type} declaration as usual.
+ at c You must declare @var{MercuryTypeName}
+ at c using a (possibly abstract) @samp{:- type} declaration as usual.
+ at var{MercuryTypeName} must be the name of an abstract type,
+or the name of a discriminated union type that is not a subtype.
+In both cases,
+ at var{MercuryTypeName} must be declared with @samp{:- type} as usual.
 The @samp{pragma foreign_type} must not have wider visibility
 than the type declaration
 (if the @samp{pragma foreign_type} declaration is in the interface,
 the @samp{:- type} declaration must be also).
 
+The type named by @var{MercuryTypeName}
+cannot be the base type of any subtypes (@pxref{Subtypes}).
+ at c XXX how can we check this?
+
 @var{ForeignTypeDescriptor} defines
 how the Mercury type is mapped for a particular foreign language.
 Specific syntax is given in the language specific information below.
diff --git a/tests/invalid/Mmakefile b/tests/invalid/Mmakefile
index f89f9d977..0a94257c7 100644
--- a/tests/invalid/Mmakefile
+++ b/tests/invalid/Mmakefile
@@ -287,6 +287,19 @@ SINGLEMODULE= \
 	state_vars_test3 \
 	state_vars_test4 \
 	state_vars_test5 \
+	subtype_abstract \
+	subtype_circular \
+	subtype_ctor_arg \
+	subtype_eqv \
+	subtype_exist_constraints \
+	subtype_exist_vars \
+	subtype_foreign \
+	subtype_foreign_supertype \
+	subtype_foreign_supertype2 \
+	subtype_ho \
+	subtype_invalid_supertype \
+	subtype_not_subset \
+	subtype_syntax \
 	switch_arm_multi_not_det \
 	tc_err1 \
 	tc_err2 \
diff --git a/tests/invalid/subtype_abstract.err_exp b/tests/invalid/subtype_abstract.err_exp
new file mode 100644
index 000000000..daf90e683
--- /dev/null
+++ b/tests/invalid/subtype_abstract.err_exp
@@ -0,0 +1,5 @@
+subtype_abstract.m:012: Error: the type definition for `citrus'/0 is not
+subtype_abstract.m:012:   visible here.
+subtype_abstract.m:019: Error: `subtype_abstract.lemon' is not a subtype of the
+subtype_abstract.m:019:   corresponding type `subtype_abstract.fruit' in the
+subtype_abstract.m:019:   supertype.
diff --git a/tests/invalid/subtype_abstract.m b/tests/invalid/subtype_abstract.m
new file mode 100644
index 000000000..296b70445
--- /dev/null
+++ b/tests/invalid/subtype_abstract.m
@@ -0,0 +1,30 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module subtype_abstract.
+:- interface.
+
+:- type fruit.
+
+:- type citrus.
+
+:- type lemon =< citrus         % abstract type as supertype
+    --->    lemon.
+
+:- type basket
+    --->    basket(fruit).
+
+:- type lemons_only =< basket
+    --->    basket(lemon).      % cannot determine lemon =< fruit
+
+:- implementation.
+
+:- type fruit
+    --->    apple
+    ;       orange
+    ;       lemon.
+
+:- type citrus =< fruit
+    --->    orange
+    ;       lemon.
diff --git a/tests/invalid/subtype_circular.err_exp b/tests/invalid/subtype_circular.err_exp
new file mode 100644
index 000000000..c732bdf4d
--- /dev/null
+++ b/tests/invalid/subtype_circular.err_exp
@@ -0,0 +1,3 @@
+subtype_circular.m:008: Error: circularity in subtype definition.
+subtype_circular.m:011: Error: circularity in subtype definition.
+subtype_circular.m:014: Error: circularity in subtype definition.
diff --git a/tests/invalid/subtype_circular.m b/tests/invalid/subtype_circular.m
new file mode 100644
index 000000000..4fba7a145
--- /dev/null
+++ b/tests/invalid/subtype_circular.m
@@ -0,0 +1,18 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module subtype_circular.
+:- interface.
+
+:- type loop =< loop
+    --->    loop.
+
+:- type loop1 =< loop2_eqv
+    --->    loop.
+
+:- type loop2 =< loop1_eqv
+    --->    loop.
+
+:- type loop1_eqv == loop1.
+:- type loop2_eqv == loop2.
diff --git a/tests/invalid/subtype_ctor_arg.err_exp b/tests/invalid/subtype_ctor_arg.err_exp
new file mode 100644
index 000000000..eb8700bd7
--- /dev/null
+++ b/tests/invalid/subtype_ctor_arg.err_exp
@@ -0,0 +1,10 @@
+subtype_ctor_arg.m:021: Error:
+subtype_ctor_arg.m:021:   `subtype_ctor_arg.nonempty_list(subtype_ctor_arg.foo)'
+subtype_ctor_arg.m:021:   is not a subtype of the corresponding type
+subtype_ctor_arg.m:021:   `subtype_ctor_arg.list(O)' in the supertype.
+subtype_ctor_arg.m:037: Error: `T' is not a subtype of the corresponding type
+subtype_ctor_arg.m:037:   `U' in the supertype.
+subtype_ctor_arg.m:040: Error: `subtype_ctor_arg.fruit(subtype_ctor_arg.foo)'
+subtype_ctor_arg.m:040:   is not a subtype of the corresponding type
+subtype_ctor_arg.m:040:   `subtype_ctor_arg.citrus(subtype_ctor_arg.foo)' in
+subtype_ctor_arg.m:040:   the supertype.
diff --git a/tests/invalid/subtype_ctor_arg.m b/tests/invalid/subtype_ctor_arg.m
new file mode 100644
index 000000000..c6b3fdf97
--- /dev/null
+++ b/tests/invalid/subtype_ctor_arg.m
@@ -0,0 +1,44 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module subtype_ctor_arg.
+:- interface.
+
+:- type list(T)
+    --->    []
+    ;       [T | list(T)].
+
+:- type nonempty_list(T) =< list(T)
+    --->    [T | list(T)].                      % ok
+
+:- type fruit(O)
+    --->    apple
+    ;       orange(list(O))
+    ;       lemon(list(foo_bar)).
+
+:- type citrus(O) =< fruit(O)
+    --->    orange(nonempty_list(foo))          % bad
+    ;       lemon(nonempty_list(foo)).          % ok
+
+:- type foo_bar
+    --->    foo
+    ;       bar.
+
+:- type foo =< foo_bar
+    --->    foo.
+
+%---------------------------------------------------------------------------%
+
+:- type pair(T)
+    --->    pair(T, T).
+
+:- type bad_pair1(T, U) =< pair(U)
+    --->    pair(T, U).                         % bad
+
+:- type bad_pair2 =< pair(citrus(foo))
+    --->    pair(citrus(foo), fruit(foo)).      % bad
+
+%---------------------------------------------------------------------------%
+
+
diff --git a/tests/invalid/subtype_eqv.err_exp b/tests/invalid/subtype_eqv.err_exp
new file mode 100644
index 000000000..bf9600086
--- /dev/null
+++ b/tests/invalid/subtype_eqv.err_exp
@@ -0,0 +1,4 @@
+subtype_eqv.m:020: Error: `O' is not a subtype of the corresponding type `L' in
+subtype_eqv.m:020:   the supertype.
+subtype_eqv.m:021: Error: `L' is not a subtype of the corresponding type `O' in
+subtype_eqv.m:021:   the supertype.
diff --git a/tests/invalid/subtype_eqv.m b/tests/invalid/subtype_eqv.m
new file mode 100644
index 000000000..2df9ad500
--- /dev/null
+++ b/tests/invalid/subtype_eqv.m
@@ -0,0 +1,30 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module subtype_eqv.
+:- interface.
+
+:- type fruit(A, O, L)
+    --->    apple(A)
+    ;       orange(O)
+    ;       lemon(L).
+
+:- type fruit_rev(L, O, A) == fruit(A, O, L).
+
+:- type citrus(O, L) =< fruit_rev(L, O, apples)
+    --->    orange(O)
+    ;       lemon(L).
+
+:- type citrus_bad(O, L) =< fruit_rev(O, L, apples)
+    --->    orange(O)
+    ;       lemon(L).
+
+:- type apples
+    --->    apples.
+
+:- type oranges
+    --->    oranges.
+
+:- type lemons
+    --->    lemons.
diff --git a/tests/invalid/subtype_exist_constraints.err_exp b/tests/invalid/subtype_exist_constraints.err_exp
new file mode 100644
index 000000000..727bec104
--- /dev/null
+++ b/tests/invalid/subtype_exist_constraints.err_exp
@@ -0,0 +1,8 @@
+subtype_exist_constraints.m:020: Error: `L' is not a subtype of the
+subtype_exist_constraints.m:020:   corresponding type `L' in the supertype.
+subtype_exist_constraints.m:023: Error: existential class constraints for
+subtype_exist_constraints.m:023:   `lemon'/1 differ in the subtype and
+subtype_exist_constraints.m:023:   supertype.
+subtype_exist_constraints.m:026: Error: existential class constraints for
+subtype_exist_constraints.m:026:   `lemon'/1 differ in the subtype and
+subtype_exist_constraints.m:026:   supertype.
diff --git a/tests/invalid/subtype_exist_constraints.m b/tests/invalid/subtype_exist_constraints.m
new file mode 100644
index 000000000..94b4c98f5
--- /dev/null
+++ b/tests/invalid/subtype_exist_constraints.m
@@ -0,0 +1,26 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module subtype_exist_constraints.
+:- interface.
+
+:- typeclass sweet(T) where [].
+:- typeclass sour(T) where [].
+
+:- type fruit
+    --->    apple
+    ;       orange
+    ;       some [L] lemon(L) => sour(L).
+
+:- type lemon =< fruit
+    --->    some [L] lemon(L) => sour(L).
+
+:- type missing_constraint =< fruit
+    --->    some [L] lemon(L).
+
+:- type wrong_constraint =< fruit
+    --->    some [L] lemon(L) => sweet(L).
+
+:- type extra_constraint =< fruit
+    --->    some [L] lemon(L) => (sour(L), sweet(L)).
diff --git a/tests/invalid/subtype_exist_vars.err_exp b/tests/invalid/subtype_exist_vars.err_exp
new file mode 100644
index 000000000..255d45eb4
--- /dev/null
+++ b/tests/invalid/subtype_exist_vars.err_exp
@@ -0,0 +1,8 @@
+subtype_exist_vars.m:019: Error: `T' is not a subtype of the corresponding type
+subtype_exist_vars.m:019:   `O' in the supertype.
+subtype_exist_vars.m:022: Error: `T' is not a subtype of the corresponding type
+subtype_exist_vars.m:022:   `int' in the supertype.
+subtype_exist_vars.m:028: Error: `B' is not a subtype of the corresponding type
+subtype_exist_vars.m:028:   `T' in the supertype.
+subtype_exist_vars.m:031: Error: `A' is not a subtype of the corresponding type
+subtype_exist_vars.m:031:   `T' in the supertype.
diff --git a/tests/invalid/subtype_exist_vars.m b/tests/invalid/subtype_exist_vars.m
new file mode 100644
index 000000000..43e2560ea
--- /dev/null
+++ b/tests/invalid/subtype_exist_vars.m
@@ -0,0 +1,31 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module subtype_exist_vars.
+:- interface.
+
+:- type fruit == fruit(int).
+
+:- type fruit(A)
+    --->    apple(A)
+    ;       some [O] orange(O)
+    ;       some [T, U] lemon(T, T, foo(U)).
+
+:- type foo(T)
+    --->    foo(T).
+
+:- type univ_vs_exist_mismatch(T) =< fruit(T)
+    --->    orange(T).
+
+:- type exist_vs_univ_mismatch =< fruit
+    --->    some [T] apple(T).
+
+:- type exist_vars_match =< fruit
+    --->    some [A, B] lemon(A, A, foo(B)).
+
+:- type exist_vars_mismatch1 =< fruit
+    --->    some [A, B] lemon(A, B, foo(B)).
+
+:- type exist_vars_mismatch2 =< fruit
+    --->    some [A, B] lemon(B, A, foo(A)).
diff --git a/tests/invalid/subtype_foreign.err_exp b/tests/invalid/subtype_foreign.err_exp
new file mode 100644
index 000000000..3d56df9a0
--- /dev/null
+++ b/tests/invalid/subtype_foreign.err_exp
@@ -0,0 +1,9 @@
+subtype_foreign.m:017: Error: type `subtype_foreign.citrus'/0 multiply defined.
+subtype_foreign.m:013: Here is the previous definition of type
+subtype_foreign.m:013:   `subtype_foreign.citrus'/0.
+subtype_foreign.m:018: Error: type `subtype_foreign.citrus'/0 multiply defined.
+subtype_foreign.m:013: Here is the previous definition of type
+subtype_foreign.m:013:   `subtype_foreign.citrus'/0.
+subtype_foreign.m:019: Error: type `subtype_foreign.citrus'/0 multiply defined.
+subtype_foreign.m:013: Here is the previous definition of type
+subtype_foreign.m:013:   `subtype_foreign.citrus'/0.
diff --git a/tests/invalid/subtype_foreign.m b/tests/invalid/subtype_foreign.m
new file mode 100644
index 000000000..25a3446db
--- /dev/null
+++ b/tests/invalid/subtype_foreign.m
@@ -0,0 +1,19 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module subtype_foreign.
+:- interface.
+
+:- type fruit
+    --->    apple
+    ;       orange
+    ;       lemon.
+
+:- type citrus =< fruit
+    --->    orange
+    ;       lemon.
+
+:- pragma foreign_type("C", citrus, "int").
+:- pragma foreign_type("Java", citrus, "int").
+:- pragma foreign_type("C#", citrus, "int").
diff --git a/tests/invalid/subtype_foreign_supertype.err_exp b/tests/invalid/subtype_foreign_supertype.err_exp
new file mode 100644
index 000000000..ebc15378f
--- /dev/null
+++ b/tests/invalid/subtype_foreign_supertype.err_exp
@@ -0,0 +1,2 @@
+subtype_foreign_supertype.m:013: Error: `fruit'/0 cannot be a supertype because
+subtype_foreign_supertype.m:013:   it is a foreign type.
diff --git a/tests/invalid/subtype_foreign_supertype.m b/tests/invalid/subtype_foreign_supertype.m
new file mode 100644
index 000000000..2f9fc0389
--- /dev/null
+++ b/tests/invalid/subtype_foreign_supertype.m
@@ -0,0 +1,19 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module subtype_foreign_supertype.
+:- interface.
+
+:- type fruit
+    --->    apple
+    ;       orange
+    ;       lemon.
+
+:- type citrus =< fruit
+    --->    orange
+    ;       lemon.
+
+:- pragma foreign_type("C", fruit, "int").
+:- pragma foreign_type("Java", fruit, "int").
+:- pragma foreign_type("C#", fruit, "int").
diff --git a/tests/invalid/subtype_foreign_supertype2.err_exp b/tests/invalid/subtype_foreign_supertype2.err_exp
new file mode 100644
index 000000000..27e55b6c9
--- /dev/null
+++ b/tests/invalid/subtype_foreign_supertype2.err_exp
@@ -0,0 +1,2 @@
+subtype_foreign_supertype2.m:016: Error: `fruit'/0 cannot be a supertype
+subtype_foreign_supertype2.m:016:   because it has a foreign type definition.
diff --git a/tests/invalid/subtype_foreign_supertype2.err_exp2 b/tests/invalid/subtype_foreign_supertype2.err_exp2
new file mode 100644
index 000000000..e948796e2
--- /dev/null
+++ b/tests/invalid/subtype_foreign_supertype2.err_exp2
@@ -0,0 +1,2 @@
+subtype_foreign_supertype2.m:016: Error: `fruit'/0 cannot be a supertype
+subtype_foreign_supertype2.m:016:   because it is a foreign type.
diff --git a/tests/invalid/subtype_foreign_supertype2.m b/tests/invalid/subtype_foreign_supertype2.m
new file mode 100644
index 000000000..20d2b1e99
--- /dev/null
+++ b/tests/invalid/subtype_foreign_supertype2.m
@@ -0,0 +1,20 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+%
+% The .err_exp file is for non-Java grades.
+% The .err_exp2 file is for Java grades.
+
+:- module subtype_foreign_supertype2.
+:- interface.
+
+:- type fruit
+    --->    apple
+    ;       orange
+    ;       lemon.
+
+:- type citrus =< fruit
+    --->    orange
+    ;       lemon.
+
+:- pragma foreign_type("Java", fruit, "int").
diff --git a/tests/invalid/subtype_ho.err_exp b/tests/invalid/subtype_ho.err_exp
new file mode 100644
index 000000000..b022ee809
--- /dev/null
+++ b/tests/invalid/subtype_ho.err_exp
@@ -0,0 +1,26 @@
+subtype_ho.m:023: Error:
+subtype_ho.m:023:   `(pred((T :: builtin.in), (io.state :: builtin.di), (io.state :: builtin.uo)) is det)'
+subtype_ho.m:023:   is not a subtype of the corresponding type
+subtype_ho.m:023:   `pred(T, io.state, io.state)' in the supertype.
+subtype_ho.m:026: Error: `pred(T, io.state, io.state)' is not a subtype of the
+subtype_ho.m:026:   corresponding type
+subtype_ho.m:026:   `(pred((T :: builtin.in), (io.state :: builtin.di), (io.state :: builtin.uo)) is det)'
+subtype_ho.m:026:   in the supertype.
+subtype_ho.m:029: Error:
+subtype_ho.m:029:   `(pred((T :: builtin.out), (io.state :: builtin.di), (io.state :: builtin.uo)) is det)'
+subtype_ho.m:029:   is not a subtype of the corresponding type
+subtype_ho.m:029:   `(pred((T :: builtin.in), (io.state :: builtin.di), (io.state :: builtin.uo)) is det)'
+subtype_ho.m:029:   in the supertype.
+subtype_ho.m:032: Error:
+subtype_ho.m:032:   `(pred((T :: builtin.in), (io.state :: builtin.di), (io.state :: builtin.uo)) is cc_multi)'
+subtype_ho.m:032:   is not a subtype of the corresponding type
+subtype_ho.m:032:   `(pred((T :: builtin.in), (io.state :: builtin.di), (io.state :: builtin.uo)) is det)'
+subtype_ho.m:032:   in the supertype.
+subtype_ho.m:035: Error: `(impure pred(T, io.state, io.state))' is not a
+subtype_ho.m:035:   subtype of the corresponding type
+subtype_ho.m:035:   `pred(T, io.state, io.state)' in the supertype.
+subtype_ho.m:036: Error:
+subtype_ho.m:036:   `((impure pred((T :: builtin.in), (io.state :: builtin.di), (io.state :: builtin.uo))) is det)'
+subtype_ho.m:036:   is not a subtype of the corresponding type
+subtype_ho.m:036:   `(pred((T :: builtin.in), (io.state :: builtin.di), (io.state :: builtin.uo)) is det)'
+subtype_ho.m:036:   in the supertype.
diff --git a/tests/invalid/subtype_ho.m b/tests/invalid/subtype_ho.m
new file mode 100644
index 000000000..8ca3d453d
--- /dev/null
+++ b/tests/invalid/subtype_ho.m
@@ -0,0 +1,36 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module subtype_ho.
+:- interface.
+
+:- import_module io.
+
+:- type tasks(T)
+    --->    task1(pred(T, io, io))
+    ;       task2(pred(T::in, io::di, io::uo) is det)
+    ;       fun(func(int) = int).
+
+:- type task1(T) =< tasks(T)
+    --->    task1(pred(T, io, io)).
+
+:- type task2_or_fun(T) =< tasks(T)
+    --->    task2(pred(T::in, io::di, io::uo) is det)
+    ;       fun(func(int) = int).
+
+:- type extra_mode_info(T) =< tasks(T)
+    --->    task1(pred(T::in, io::di, io::uo) is det).
+
+:- type missing_mode_info(T) =< tasks(T)
+    --->    task2(pred(T, io, io)).
+
+:- type mismatch_arg_mode(T) =< tasks(T)
+    --->    task2(pred(T::out, io::di, io::uo) is det).
+
+:- type mismatch_detism(T) =< tasks(T)
+    --->    task2(pred(T::in, io::di, io::uo) is cc_multi).
+
+:- type mismatch_purity(T) =< tasks(T)
+    --->    task1(impure pred(T, io, io))
+    ;       task2(impure pred(T::in, io::di, io::uo) is det).
diff --git a/tests/invalid/subtype_invalid_supertype.err_exp b/tests/invalid/subtype_invalid_supertype.err_exp
new file mode 100644
index 000000000..61f26427f
--- /dev/null
+++ b/tests/invalid/subtype_invalid_supertype.err_exp
@@ -0,0 +1,15 @@
+subtype_invalid_supertype.m:008: Error: `int'/0 is not a discriminated union
+subtype_invalid_supertype.m:008:   type.
+subtype_invalid_supertype.m:011: Error: `{}'/0 is not a discriminated union
+subtype_invalid_supertype.m:011:   type.
+subtype_invalid_supertype.m:014: Error: `func'/1 is not a discriminated union
+subtype_invalid_supertype.m:014:   type.
+subtype_invalid_supertype.m:017: Error: `pred'/0 is not a discriminated union
+subtype_invalid_supertype.m:017:   type.
+subtype_invalid_supertype.m:020: Error: undefined type `undefined'/0.
+subtype_invalid_supertype.m:020: In definition of type `s5'/0:
+subtype_invalid_supertype.m:020:   error: undefined type `undefined'/0.
+subtype_invalid_supertype.m:023: In the supertype part of a subtype definition:
+subtype_invalid_supertype.m:023:   error: `1' is not a type.
+subtype_invalid_supertype.m:023: In the supertype part of a subtype definition:
+subtype_invalid_supertype.m:023:   error: `2' is not a type.
diff --git a/tests/invalid/subtype_invalid_supertype.m b/tests/invalid/subtype_invalid_supertype.m
new file mode 100644
index 000000000..3e8a1cb5b
--- /dev/null
+++ b/tests/invalid/subtype_invalid_supertype.m
@@ -0,0 +1,24 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module subtype_invalid_supertype.
+:- interface.
+
+:- type s1 =< int
+    --->    s.
+
+:- type s2 =< {}
+    --->    s.
+
+:- type s3 =< (func(int) = int)
+    --->    s.
+
+:- type s4 =< (pred)
+    --->    s.
+
+:- type s5 =< undefined
+    --->    s.
+
+:- type s6 =< t(1, 2)
+    --->    s.
diff --git a/tests/invalid/subtype_not_subset.err_exp b/tests/invalid/subtype_not_subset.err_exp
new file mode 100644
index 000000000..19c9cc950
--- /dev/null
+++ b/tests/invalid/subtype_not_subset.err_exp
@@ -0,0 +1,6 @@
+subtype_not_subset.m:015: Error: `lemon'/1 is not a constructor of the
+subtype_not_subset.m:015:   supertype `fruit'/0.
+subtype_not_subset.m:016: Error: `pomelo'/0 is not a constructor of the
+subtype_not_subset.m:016:   supertype `fruit'/0.
+subtype_not_subset.m:017: Error: `grapefruit'/0 is not a constructor of the
+subtype_not_subset.m:017:   supertype `fruit'/0.
diff --git a/tests/invalid/subtype_not_subset.m b/tests/invalid/subtype_not_subset.m
new file mode 100644
index 000000000..3a374dead
--- /dev/null
+++ b/tests/invalid/subtype_not_subset.m
@@ -0,0 +1,17 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module subtype_not_subset.
+:- interface.
+
+:- type fruit
+    --->    apple
+    ;       orange
+    ;       lemon.
+
+:- type citrus =< fruit
+    --->    orange
+    ;       lemon(int)
+    ;       pomelo
+    ;       grapefruit.
diff --git a/tests/invalid/subtype_syntax.err_exp b/tests/invalid/subtype_syntax.err_exp
new file mode 100644
index 000000000..3def083f4
--- /dev/null
+++ b/tests/invalid/subtype_syntax.err_exp
@@ -0,0 +1,28 @@
+subtype_syntax.m:008: Error: the type name `=<' is reserved for the Mercury
+subtype_syntax.m:008:   implementation.
+subtype_syntax.m:009: Error: the type name `=<' is reserved for the Mercury
+subtype_syntax.m:009:   implementation.
+subtype_syntax.m:011: In the supertype part of a subtype definition: error:
+subtype_syntax.m:011:   `123' is not a type.
+subtype_syntax.m:014: In the supertype part of a subtype definition: error:
+subtype_syntax.m:014:   expected a type constructor, got `T'.
+subtype_syntax.m:017: In the supertype part of a subtype definition: error:
+subtype_syntax.m:017:   `123' is not a type.
+subtype_syntax.m:020: On the left hand side of type definition: error: expected
+subtype_syntax.m:020:   a symbol name, got `123'.
+subtype_syntax.m:021: In constructor definition: error: expected a symbol name,
+subtype_syntax.m:021:   got `1'.
+subtype_syntax.m:022: In constructor definition: error: expected a symbol name,
+subtype_syntax.m:022:   got `Two'.
+subtype_syntax.m:024: On the left hand side of type definition: error: expected
+subtype_syntax.m:024:   a type constructor and zero or more type variables as
+subtype_syntax.m:024:   arguments, got `T'.
+subtype_syntax.m:027: On the left hand side of type definition: error: type
+subtype_syntax.m:027:   parameters must be variables, but `int' is not.
+subtype_syntax.m:030: On the left hand side of type definition: error: type
+subtype_syntax.m:030:   parameters must be unique, but the parameter T is
+subtype_syntax.m:030:   duplicated.
+subtype_syntax.m:033: Error: free type parameters U, _V in supertype part of
+subtype_syntax.m:033:   subtype definition.
+subtype_syntax.m:037: Error: free type parameter U in right hand side of type
+subtype_syntax.m:037:   definition.
diff --git a/tests/invalid/subtype_syntax.m b/tests/invalid/subtype_syntax.m
new file mode 100644
index 000000000..43eff0f8a
--- /dev/null
+++ b/tests/invalid/subtype_syntax.m
@@ -0,0 +1,42 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module subtype_syntax.
+:- interface.
+
+:- type s =< t.             % =< is reserved
+:- type S =< T.             % =< is reserved
+
+:- type s =< 123            % supertype must be type
+    --->    s.
+
+:- type s =< T              % supertype cannot be var
+    --->    s.
+
+:- type s =< t(123)         % supertype args must be types
+    --->    s.
+
+:- type 123 =< t            % subtype must be symbol
+    --->    1               % constructors must be symbols
+    ;       Two.
+
+:- type T =< t              % subtype must be symbol
+    --->    s.
+
+:- type s(int) =< t         % subtype args must be variables
+    --->    s.
+
+:- type s(T, T) =< t        % subtype vars must be distinct
+    --->    s.
+
+:- type s(T) =< t(U, _V)    % vars in supertype must not be free
+    --->    s.
+
+:- type s =< t
+    --->    s(U).           % vars in body must not be free
+
+%---------------------------------------------------------------------------%
+
+:- type dummy_export
+    --->    dummy_export.
diff --git a/tests/invalid_submodules/Mercury.options b/tests/invalid_submodules/Mercury.options
index f5e9b137d..38d014207 100644
--- a/tests/invalid_submodules/Mercury.options
+++ b/tests/invalid_submodules/Mercury.options
@@ -11,5 +11,6 @@ MCFLAGS-import_in_parent.sub    = --no-intermodule-optimization
 MCFLAGS-missing_parent_import   = --no-intermodule-optimization
 MCFLAGS-sub_c                   = --verbose-error-messages \
                                     --no-intermodule-optimization
+MCFLAGS-subtype_submodule       = --no-intermodule-optimization
 MCFLAGS-undef_mod_qual          = --no-intermodule-optimization
 MCFLAGS-unresolved_overloading  = --no-intermodule-optimization
diff --git a/tests/invalid_submodules/Mmakefile b/tests/invalid_submodules/Mmakefile
index df378ac9b..2f8738682 100644
--- a/tests/invalid_submodules/Mmakefile
+++ b/tests/invalid_submodules/Mmakefile
@@ -24,6 +24,7 @@ MAKE_DEP_PROGS = \
 	import_in_parent \
 	missing_parent_import \
 	sub_c \
+	subtype_submodule \
 	undef_mod_qual \
 	unresolved_overloading
 
diff --git a/tests/invalid_submodules/subtype_submodule.err_exp b/tests/invalid_submodules/subtype_submodule.err_exp
new file mode 100644
index 000000000..2cfe41460
--- /dev/null
+++ b/tests/invalid_submodules/subtype_submodule.err_exp
@@ -0,0 +1,3 @@
+subtype_submodule.m:024: Error: undefined type `fruit2'/0.
+subtype_submodule.m:024: In definition of type `citrus2'/0:
+subtype_submodule.m:024:   error: undefined type `fruit2'/0.
diff --git a/tests/invalid_submodules/subtype_submodule.m b/tests/invalid_submodules/subtype_submodule.m
new file mode 100644
index 000000000..a74d7db26
--- /dev/null
+++ b/tests/invalid_submodules/subtype_submodule.m
@@ -0,0 +1,32 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module subtype_submodule.
+:- interface.
+
+:- type fruit
+    --->    apple
+    ;       orange
+    ;       lemon.
+
+:- implementation.
+
+%---------------------------------------------------------------------------%
+
+:- module child.
+:- interface.
+
+:- type citrus =< fruit     % ok
+    --->    orange
+    ;       lemon.
+
+:- type citrus2 =< fruit2   % bad
+    --->    orange
+    ;       lemon.
+
+:- end_module child.
+
+%---------------------------------------------------------------------------%
+
+:- end_module subtype_submodule.
diff --git a/tests/valid/Mmakefile b/tests/valid/Mmakefile
index da1b9d647..1ad251af7 100644
--- a/tests/valid/Mmakefile
+++ b/tests/valid/Mmakefile
@@ -237,6 +237,7 @@ OTHER_PROGS = \
 	state_var_mode_bug \
 	state_var_mode_bug2 \
 	static \
+	subtype_basic \
 	subtype_switch \
 	switch_detection_bug \
 	switch_detection_bug2 \
diff --git a/tests/valid/subtype_basic.m b/tests/valid/subtype_basic.m
new file mode 100644
index 000000000..fe243792a
--- /dev/null
+++ b/tests/valid/subtype_basic.m
@@ -0,0 +1,48 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module subtype_basic.
+:- interface.
+
+:- type fruit
+    --->    apple
+    ;       orange
+    ;       lemon.
+
+:- type citrus =< fruit
+    --->    orange
+    ;       lemon.
+
+:- type citrus(C) =< fruit
+    --->    orange
+    ;       lemon.
+
+:- type lemon.  % abstract
+
+:- type lemon_eqv == lemon.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- type lemon =< citrus
+    --->    lemon.
+
+:- type list(T)
+    --->    []
+    ;       [T | list(T)].
+
+:- type nonempty_list(T) =< list(T)
+    --->    [T | list(T)].
+
+:- type nonempty_list_of_fruit =< list(fruit)
+    --->    [fruit | list(fruit)].
+
+:- type nonempty_list_of_fruit_eqv == nonempty_list(fruit).
+
+:- type nonempty_list_of_citrus =< nonempty_list_of_fruit_eqv
+    --->    [citrus | list(citrus)].
+
+:- type nonempty_list_of_lemon =< nonempty_list_of_citrus
+    --->    [lemon | list(lemon_eqv)].
-- 
2.30.0



More information about the reviews mailing list