[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