[m-rev.] for review: Fix aborts when checking coercions.
Peter Wang
novalazy at gmail.com
Thu Jul 10 15:54:37 AEST 2025
Fix some aborts that could happen while type- or modechecking type
conversion expressions.
compiler/typecheck_coerce.m:
When building the set of invariant type parameters, handle a
constructor argument that has a type which is an (unexpanded)
equivalence type.
This fixes GitHub issue #137.
compiler/modecheck_coerce.m:
In modecheck_coerce_from_ground_make_inst_for_subtype,
handle a non-du or tuple type instead of aborting.
In get_ctor_arg_types_do_subst, handle a tuple type
instead of failing (leading to an abort).
tests/invalid/Mmakefile:
tests/invalid/coerce_typecheck_eqv.err_exp:
tests/invalid/coerce_typecheck_eqv.m:
tests/invalid/coerce_typecheck_eqv_helper_1.m:
Add test case.
tests/valid/Mmakefile:
tests/valid/coerce_modecheck_eqv.err_exp:
tests/valid/coerce_modecheck_eqv.m:
tests/valid/coerce_modecheck_eqv_helper_1.m:
Add test case.
tests/valid/gh137.m:
tests/valid/gh137_helper_1.m:
Delete original test case for GitHub issue #137,
as it is subsumed by tests/invalid/coerce_typecheck_eqv.m
NEWS.md:
Add news item for this, and previous changes.
[The diff is created with -b]
diff --git a/NEWS.md b/NEWS.md
index 518cae42d..d86b64a0b 100644
--- a/NEWS.md
+++ b/NEWS.md
@@ -1455,6 +1455,9 @@ Changes to the Mercury compiler
C# and Java grades when a subtype type definition did not repeat the field
names of its base type.
+* We have improved the typechecking and modechecking of type conversion
+ expressions.
+
* We have fixed a bug where `--warn-unused-imports` did not warn about
unused modules that are also imported by an ancestor of the current module.
diff --git a/compiler/modecheck_coerce.m b/compiler/modecheck_coerce.m
index 8e3d462e6..c87c478d9 100644
--- a/compiler/modecheck_coerce.m
+++ b/compiler/modecheck_coerce.m
@@ -806,22 +806,22 @@ modecheck_coerce_from_ground_make_inst_for_subtype(ModuleInfo, TVarSet,
% and if it would not lead to an infinite loop.
( if
TypeX \= TypeY,
- set.insert_new(TypeX, SeenTypes0, SeenTypes1)
+ set.insert_new(TypeX, SeenTypes0, SeenTypes1),
+ type_constructors(ModuleInfo, TypeX, CtorsX)
then
- modecheck_coerce_from_ground_make_bound_functor(ModuleInfo, TVarSet,
- LiveX, UniqX, SeenTypes1, TypeX, TypeY, InstY)
+ modecheck_coerce_from_ground_make_bound_inst(ModuleInfo, TVarSet,
+ LiveX, UniqX, SeenTypes1, TypeX, TypeY, CtorsX, InstY)
else
UniqY = uniqueness_for_coerce_result(LiveX, UniqX),
InstY = ground(UniqY, none_or_default_func)
).
-:- pred modecheck_coerce_from_ground_make_bound_functor(module_info::in,
+:- pred modecheck_coerce_from_ground_make_bound_inst(module_info::in,
tvarset::in, is_live::in, uniqueness::in, set(mer_type)::in,
- mer_type::in, mer_type::in, mer_inst::out) is det.
+ mer_type::in, mer_type::in, list(constructor)::in, mer_inst::out) is det.
-modecheck_coerce_from_ground_make_bound_functor(ModuleInfo, TVarSet,
- LiveX, UniqX, SeenTypes, TypeX, TypeY, InstY) :-
- ( if type_constructors(ModuleInfo, TypeX, CtorsX) then
+modecheck_coerce_from_ground_make_bound_inst(ModuleInfo, TVarSet,
+ LiveX, UniqX, SeenTypes, TypeX, TypeY, CtorsX, InstY) :-
list.map(
modecheck_coerce_from_ground_make_bound_functor(ModuleInfo,
TVarSet, LiveX, UniqX, SeenTypes, TypeX, TypeY),
@@ -836,10 +836,7 @@ modecheck_coerce_from_ground_make_bound_functor(ModuleInfo, TVarSet,
inst_result_contains_types_unknown,
inst_result_no_type_ctor_propagated
),
- InstY = bound(UniqY, InstResults, BoundFunctorsY)
- else
- unexpected($pred, "missing constructors")
- ).
+ InstY = bound(UniqY, InstResults, BoundFunctorsY).
:- pred modecheck_coerce_from_ground_make_bound_functor(module_info::in,
tvarset::in, is_live::in, uniqueness::in, set(mer_type)::in,
@@ -910,13 +907,16 @@ maybe_change_module_qualifier(ModuleName, SymName0, SymName) :-
du_ctor::in, list(mer_type)::out) is semidet.
get_ctor_arg_types_do_subst(ModuleInfo, Type, DuCtor, CtorArgTypes) :-
+ ( if Type = tuple_type(TypeArgs, _Kind) then
+ % Assume DuCtor is correct.
+ CtorArgTypes = TypeArgs
+ else
type_to_ctor_and_args(Type, TypeCtor, TypeArgs),
module_info_get_cons_table(ModuleInfo, ConsTable),
- search_cons_table_of_type_ctor(ConsTable, TypeCtor, DuCtor,
- ConsDefn),
+ search_cons_table_of_type_ctor(ConsTable, TypeCtor, DuCtor, ConsDefn),
require_det (
- ConsDefn = hlds_cons_defn(_TypeCtor, _TVarSet, TypeParams, _KindMap,
- _MaybeExistConstraints, CtorArgs, _Context),
+ ConsDefn = hlds_cons_defn(_TypeCtor, _TVarSet, TypeParams,
+ _KindMap, _MaybeExistConstraints, CtorArgs, _Context),
get_ctor_arg_types(CtorArgs, CtorArgTypes0),
(
TypeParams = [],
@@ -926,6 +926,7 @@ get_ctor_arg_types_do_subst(ModuleInfo, Type, DuCtor, CtorArgTypes) :-
map.from_corresponding_lists(TypeParams, TypeArgs, Subst),
apply_subst_to_type_list(Subst, CtorArgTypes0, CtorArgTypes)
)
+ )
).
:- pred get_ctor_existq_tvars_det(module_info::in, mer_type::in, du_ctor::in,
diff --git a/compiler/typecheck_coerce.m b/compiler/typecheck_coerce.m
index 6ecfd6e34..e47e0c382 100644
--- a/compiler/typecheck_coerce.m
+++ b/compiler/typecheck_coerce.m
@@ -313,8 +313,12 @@ build_type_param_variance_restrictions_in_ctor_arg_type(TypeTable, CurTypeCtor,
type_vars_in_types(ArgTypes, TypeVars),
set.insert_list(TypeVars, !InvariantSet)
;
- TypeBody = hlds_eqv_type(_),
- unexpected($pred, "hlds_eqv_type")
+ TypeBody = hlds_eqv_type(EqvType0),
+ hlds_data.get_type_defn_tparams(TypeDefn, TypeParams),
+ map.from_corresponding_lists(TypeParams, TypeArgs, TSubst),
+ apply_subst_to_type(TSubst, EqvType0, EqvType),
+ build_type_param_variance_restrictions_in_ctor_arg_type(TypeTable,
+ CurTypeCtor, CurTypeParams, EqvType, !InvariantSet)
)
else
unexpected($pred, "undefined type")
diff --git a/tests/invalid/Mmakefile b/tests/invalid/Mmakefile
index f22f430b4..e1bd357c2 100644
--- a/tests/invalid/Mmakefile
+++ b/tests/invalid/Mmakefile
@@ -46,6 +46,7 @@ INTERMOD_SPECIAL_SINGLEMODULE_PROGS = \
BORING_MULTIMODULE_PROGS = \
bad_exported_mode \
+ coerce_typecheck_eqv \
exported_unify \
ho_default_func_2 \
instances_pc.instances_pc_helper_1 \
diff --git a/tests/invalid/coerce_typecheck_eqv.err_exp b/tests/invalid/coerce_typecheck_eqv.err_exp
new file mode 100644
index 000000000..ac7746edd
--- /dev/null
+++ b/tests/invalid/coerce_typecheck_eqv.err_exp
@@ -0,0 +1,5 @@
+coerce_typecheck_eqv.m:039: In clause for predicate `test2'/2:
+coerce_typecheck_eqv.m:039: error: cannot coerce [38;5;87m`X'[39;49m from
+coerce_typecheck_eqv.m:039: [38;5;171m`coerce_typecheck_eqv.bad(coerce_typecheck_eqv.citrus)'[39;49m
+coerce_typecheck_eqv.m:039: to
+coerce_typecheck_eqv.m:039: [38;5;171m`coerce_typecheck_eqv.bad(coerce_typecheck_eqv.fruit)'.[39;49m
diff --git a/tests/invalid/coerce_typecheck_eqv.m b/tests/invalid/coerce_typecheck_eqv.m
new file mode 100644
index 000000000..aa282707d
--- /dev/null
+++ b/tests/invalid/coerce_typecheck_eqv.m
@@ -0,0 +1,41 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module coerce_typecheck_eqv.
+:- interface.
+
+:- type fruit
+ ---> apple
+ ; lemon.
+
+:- type citrus =< fruit
+ ---> lemon.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module coerce_typecheck_eqv_helper_1.
+
+:- type good(T)
+ ---> good(first(int, T)). % == second(T, int) == list(int)
+
+:- type bad(T)
+ ---> bad(first(T, int)). % == second(int, T) == list(T)
+
+:- pred test1(good(citrus)::in, good(fruit)::out) is det.
+
+test1(X, Y) :-
+ Y = coerce(X).
+
+:- pred test2(bad(citrus)::in, bad(fruit)::out) is det.
+
+test2(X, Y) :-
+ % The type parameter T in bad(T), after expanding type equivalences,
+ % appears in the discriminated union type list(T), so it must be invariant.
+ % This coerce expression cannot be type-correct as T would be bound to
+ % 'citrus' in the from-type, but 'fruit' in the to-type.
+ Y = coerce(X).
+
+%---------------------------------------------------------------------------%
diff --git a/tests/invalid/coerce_typecheck_eqv_helper_1.m b/tests/invalid/coerce_typecheck_eqv_helper_1.m
new file mode 100644
index 000000000..868c180ff
--- /dev/null
+++ b/tests/invalid/coerce_typecheck_eqv_helper_1.m
@@ -0,0 +1,16 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module coerce_typecheck_eqv_helper_1.
+:- interface.
+
+:- type first(A, B) == second(B, A).
+
+:- type second(T, U).
+
+:- implementation.
+
+:- import_module list.
+
+:- type second(T, U) == list(U).
diff --git a/tests/valid/Mmakefile b/tests/valid/Mmakefile
index ed9f268dd..a40c120f3 100644
--- a/tests/valid/Mmakefile
+++ b/tests/valid/Mmakefile
@@ -143,6 +143,7 @@ OTHER_PROGS = \
bug85 \
builtin_false \
call_failure \
+ coerce_modecheck_eqv \
common_struct_bug \
compl_unify_bug \
complete_int8_switch \
@@ -184,7 +185,6 @@ OTHER_PROGS = \
func_in_head \
gh65 \
gh89 \
- gh137 \
github_50 \
hawkins_switch_bug \
headvar_not_found \
diff --git a/tests/valid/coerce_modecheck_eqv.m b/tests/valid/coerce_modecheck_eqv.m
new file mode 100644
index 000000000..8c2b9422e
--- /dev/null
+++ b/tests/valid/coerce_modecheck_eqv.m
@@ -0,0 +1,39 @@
+%---------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sw=4 et
+%---------------------------------------------------------------------------%
+
+:- module coerce_modecheck_eqv.
+:- interface.
+
+:- type fruit
+ ---> apple
+ ; orange
+ ; lemon.
+
+:- type citrus =< fruit
+ ---> orange
+ ; lemon.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module coerce_modecheck_eqv_helper_1.
+
+:- type wrap_foo(T)
+ ---> wrap_foo(foo(T)).
+
+:- type wrap_bar(T)
+ ---> wrap_bar({T, bar}).
+
+:- pred test1(wrap_foo(citrus)::in, wrap_foo(fruit)::out) is det.
+
+test1(X, Y) :-
+ Y = coerce(X).
+
+:- pred test2(wrap_bar(citrus)::in, wrap_bar(fruit)::out) is det.
+
+test2(X, Y) :-
+ Y = coerce(X).
+
+%---------------------------------------------------------------------------%
diff --git a/tests/valid/coerce_modecheck_eqv_helper_1.m b/tests/valid/coerce_modecheck_eqv_helper_1.m
new file mode 100644
index 000000000..ec6f1dedc
--- /dev/null
+++ b/tests/valid/coerce_modecheck_eqv_helper_1.m
@@ -0,0 +1,32 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module coerce_modecheck_eqv_helper_1.
+:- interface.
+
+% We really need foo(T) to be abstractly exported from this module,
+% with the type equivalence defined in the implementation section.
+% Then, we can run:
+%
+% mmc --make-int coerce_modecheck_eqv_helper_1.m
+% mmc --errorcheck-only coerce_modecheck_eqv.m
+%
+% If we try to include and run the test as part of the test suite,
+% the compiler reports:
+%
+% Error: the type `foo'/1 is a polymorphic equivalence type with a
+% monomorphic definition. The export of such types as abstract types
+% is not yet implemented.
+%
+% Therefore, we export the type definition in the interface section,
+% but it won't actually test the handling of an unexpanded equivalence type
+% in the modechecker for coercions.
+:- type foo(T).
+:- type foo(T) == int. % should be in the implementation section
+
+:- type bar.
+
+:- implementation.
+
+:- type bar == int.
diff --git a/tests/valid/gh137.m b/tests/valid/gh137.m
deleted file mode 100644
index 5d55c71fa..000000000
--- a/tests/valid/gh137.m
+++ /dev/null
@@ -1,70 +0,0 @@
-%-----------------------------------------------------------------------------%
-% vim: ft=mercury
-%-----------------------------------------------------------------------------%
-% Copyright (C) 2025 Charlie H. McGee IV.
-% This file may only be copied under the terms of the GNU Library General
-% Public License as described in the file LICENCE.
-%-----------------------------------------------------------------------------%
-%
-% File: mh_scope.m
-% Main author: C4Cypher.
-% Stability: low.
-%
-%-----------------------------------------------------------------------------%
-%
-% This is a regression test for github issue #137.
-%
-% The problem is a compiler crash with the error message:
-%
-% Software Error: predicate
-% `check_hlds.typecheck_coerce.
-% build_type_param_variance_restrictions_in_ctor_arg_type'/6:
-% Unexpected: hlds_eqv_type
-%
-% The crash occurs when the compiler typechecks the coerce on the
-% second last line, and its immediate cause is the fact that the
-% type table entry for the root_scope function symbol, for *both*
-% the supertype mh_scope and the subtype mh_root_scope, has an argument
-% whose type is an equivalence type. This type is exported as an abstract
-% type from gh137_helper_1.m, but gh137_helper_1.{int,int2} both contain
-% its definition as an equivalence type in their implementation section.
-
-%-----------------------------------------------------------------------------%
-
-:- module gh137.
-
-:- interface.
-
-:- type mh_scope.
-
-:- pred parent(mh_scope::in, mh_scope::out) is semidet.
-
-%-----------------------------------------------------------------------------%
-%-----------------------------------------------------------------------------%
-
-:- implementation.
-
-:- import_module gh137_helper_1.
-
-%-----------------------------------------------------------------------------%
-
-:- type mh_scope
- ---> root_scope(var_id_set)
- ; extended_scope(mh_root_scope)
- ; child_scope(mh_scope).
-
-:- type mh_root_scope =< mh_scope
- ---> root_scope(var_id_set)
- ; extended_scope(mh_root_scope).
-
-parent(Child, Parent) :-
- require_complete_switch [Child]
- (
- Child = root_scope(_),
- fail
- ;
- Child = child_scope(Parent)
- ;
- Child = extended_scope(Root),
- Parent = coerce(Root)
- ).
diff --git a/tests/valid/gh137_helper_1.m b/tests/valid/gh137_helper_1.m
deleted file mode 100644
index a04692d07..000000000
--- a/tests/valid/gh137_helper_1.m
+++ /dev/null
@@ -1,8 +0,0 @@
-:- module gh137_helper_1.
-:- interface.
-
-:- type var_id_set.
-
-:- implementation.
-
-:- type var_id_set == int.
--
2.49.0
More information about the reviews
mailing list