[m-rev.] for review: Implement modechecking of coerce more efficiently.
Peter Wang
novalazy at gmail.com
Mon Apr 26 14:13:51 AEST 2021
Implement modechecking of coerce in a direct and efficient way.
The old implementation worked by generating a 'bound' inst node for each
node in the type tree (recursively, as far as possible),
calling abstractly_unify_inst, then checking the resulting inst is valid
for the result type. The insts could explode in size for large types.
The new implementation works by simultaneously traversing the input inst
tree, the input type tree, and the result type tree, and producing the
result inst tree for a valid conversion or rejecting the coercion.
Where the input and result types are equal, the result inst can just be
'ground' instead of expanding to a 'bound' inst. Therefore the
result inst does not explode in size compared to the input inst.
While testing, I discovered a couple of cases where the old
implementation would accept coercions that it should not have,
which are rejected by the new implementation.
compiler/modecheck_coerce.m:
Implement the new algorithm.
compiler/mode_errors.m:
Change how we report coerce mode errors as we cannot generate the
same messages as before.
compiler/typecheck.m:
compiler/type_util.m:
Move get_supertype into type_util.m.
doc/reference_manual.texi:
Describe how coerce is mode checked now.
tests/invalid/Mmakefile:
tests/invalid/coerce_int.err_exp:
tests/invalid/coerce_int.m:
tests/invalid/coerce_recursive_inst.err_exp:
tests/invalid/coerce_recursive_inst.m:
tests/invalid/coerce_recursive_type.err_exp:
tests/invalid/coerce_recursive_type.m:
Add new test cases.
tests/invalid/coerce_mode_error.m:
tests/invalid/coerce_mode_error.err_exp:
tests/invalid/coerce_instvar.err_exp:
tests/invalid/coerce_uniq.err_exp:
tests/invalid/coerce_unreachable.err_exp:
Update expected error messages.
diff --git a/compiler/mode_errors.m b/compiler/mode_errors.m
index b91267361..e8b38713f 100644
--- a/compiler/mode_errors.m
+++ b/compiler/mode_errors.m
@@ -165,9 +165,9 @@
; mode_error_coerce_input_not_ground(prog_var, mer_inst)
% The argument in a coerce expression has a non-ground inst.
- ; mode_error_coerce_bad_result_inst(mer_inst, mer_type)
- % The result of a coercion would have an inst that is not valid
- % for the type.
+ ; mode_error_coerce_invalid(mer_inst, mer_type)
+ % The argument in a coerce expression has a ground inst
+ % that is not valid for the result type.
% Mode errors that can happen in more than one kind of goal.
@@ -472,10 +472,11 @@ mode_error_to_spec(ModeInfo, ModeError) = Spec :-
MergeErrors)
;
ModeError = mode_error_coerce_input_not_ground(Var, VarInst),
- Spec = mode_error_coerce_input_not_ground(ModeInfo, Var, VarInst)
+ Spec = mode_error_coerce_input_not_ground_to_spec(ModeInfo, Var,
+ VarInst)
;
- ModeError = mode_error_coerce_bad_result_inst(Inst, Type),
- Spec = mode_error_coerce_bad_result_inst_to_spec(ModeInfo, Inst, Type)
+ ModeError = mode_error_coerce_invalid(Inst, Type),
+ Spec = mode_error_coerce_invalid_to_spec(ModeInfo, Inst, Type)
;
ModeError = mode_error_bind_locked_var(Reason, Var, InstA, InstB),
Spec = mode_error_bind_locked_var_to_spec(ModeInfo, Reason, Var,
@@ -1307,10 +1308,10 @@ merge_context_to_string(merge_stm_atomic) = "atomic".
%---------------------------------------------------------------------------%
-:- func mode_error_coerce_input_not_ground(mode_info, prog_var, mer_inst) =
- error_spec.
+:- func mode_error_coerce_input_not_ground_to_spec(mode_info, prog_var,
+ mer_inst) = error_spec.
-mode_error_coerce_input_not_ground(ModeInfo, Var, VarInst) = Spec :-
+mode_error_coerce_input_not_ground_to_spec(ModeInfo, Var, VarInst) = Spec :-
Preamble = mode_info_context_preamble(ModeInfo),
mode_info_get_context(ModeInfo, Context),
mode_info_get_varset(ModeInfo, VarSet),
@@ -1323,18 +1324,18 @@ mode_error_coerce_input_not_ground(ModeInfo, Var, VarInst) = Spec :-
%---------------------------------------------------------------------------%
-:- func mode_error_coerce_bad_result_inst_to_spec(mode_info, mer_inst,
- mer_type) = error_spec.
+:- func mode_error_coerce_invalid_to_spec(mode_info, mer_inst, mer_type) =
+ error_spec.
-mode_error_coerce_bad_result_inst_to_spec(ModeInfo, Inst, Type) = Spec :-
+mode_error_coerce_invalid_to_spec(ModeInfo, Inst, Type) = Spec :-
Preamble = mode_info_context_preamble(ModeInfo),
mode_info_get_context(ModeInfo, Context),
varset.init(TypeVarSet),
- Pieces = [words("mode error: the result would have instantiatedness")] ++
+ Pieces = [words("mode error: the input term has instantiatedness")] ++
report_inst(ModeInfo, quote_short_inst, [suffix(","), nl],
[nl_indent_delta(1)], [suffix(","), nl_indent_delta(-1)],
Inst) ++
- [words("which is not valid for the type"),
+ [words("and cannot be converted to the type"),
quote(mercury_type_to_string(TypeVarSet, print_name_only, Type)),
suffix("."), nl],
Spec = simplest_spec($pred, severity_error,
diff --git a/compiler/modecheck_coerce.m b/compiler/modecheck_coerce.m
index 4e5253d37..1c7cf6525 100644
--- a/compiler/modecheck_coerce.m
+++ b/compiler/modecheck_coerce.m
@@ -35,19 +35,27 @@
:- import_module check_hlds.inst_test.
:- import_module check_hlds.inst_util.
:- import_module check_hlds.mode_errors.
+:- import_module check_hlds.mode_util.
:- import_module check_hlds.modecheck_unify.
:- import_module check_hlds.type_util.
:- import_module hlds.
+:- import_module hlds.hlds_cons.
+:- import_module hlds.hlds_data.
:- import_module hlds.hlds_module.
+:- import_module hlds.hlds_pred.
:- import_module hlds.instmap.
:- import_module hlds.vartypes.
:- import_module mdbcomp.
:- import_module mdbcomp.sym_name.
+:- import_module parse_tree.builtin_lib_types.
:- import_module parse_tree.prog_mode.
:- import_module parse_tree.prog_type.
+:- import_module parse_tree.prog_type_subst.
:- import_module parse_tree.set_of_var.
+:- import_module map.
:- import_module maybe.
+:- import_module pair.
:- import_module require.
:- import_module set.
:- import_module term.
@@ -61,6 +69,9 @@
)
; coerce_mode_error.
+:- inst cons for cons_id/0
+ ---> cons(ground, ground, ground).
+
%---------------------------------------------------------------------------%
modecheck_coerce(Args0, Args, Modes0, Modes, Det, ExtraGoals, !ModeInfo) :-
@@ -110,6 +121,10 @@ modecheck_coerce(Args0, Args, Modes0, Modes, Det, ExtraGoals, !ModeInfo) :-
mode_info::in, mode_info::out) is det.
modecheck_coerce_vars(ModuleInfo0, X, Y, InstX, InstY, Res, !ModeInfo) :-
+ mode_info_get_pred_id(!.ModeInfo, PredId),
+ module_info_pred_info(ModuleInfo0, PredId, PredInfo),
+ pred_info_get_typevarset(PredInfo, TVarSet),
+
mode_info_get_var_types(!.ModeInfo, VarTypes),
lookup_var_type(VarTypes, X, TypeX),
lookup_var_type(VarTypes, Y, TypeY),
@@ -117,392 +132,52 @@ modecheck_coerce_vars(ModuleInfo0, X, Y, InstX, InstY, Res, !ModeInfo) :-
mode_info_var_is_live(!.ModeInfo, X, LiveX),
mode_info_var_is_live(!.ModeInfo, Y, LiveY),
( if LiveX = is_live, LiveY = is_live then
- BothLive = is_live,
- Uniq = shared
+ BothLive = is_live
else
- BothLive = is_dead,
- Uniq = unique
+ BothLive = is_dead
),
- set.init(Seen0),
- make_bound_inst_for_type(ModuleInfo0, Seen0, Uniq, TypeX,
- BoundInstForTypeX),
- ( if
- abstractly_unify_inst(BothLive, BoundInstForTypeX, InstX, real_unify,
- UnifyInstForTypeX, _Det, ModuleInfo0, ModuleInfo)
- then
+ set.init(ExpandedInsts0),
+ modecheck_coerce_make_inst(ModuleInfo0, TVarSet, LiveX, TypeX, TypeY,
+ ExpandedInsts0, InstX, MaybeFinalInstY),
+ (
+ MaybeFinalInstY = yes(FinalInstY),
( if
- check_bound_functors_in_type(ModuleInfo, TypeY,
- UnifyInstForTypeX, UnifyInstForTypeY)
+ abstractly_unify_inst(BothLive, InstX, ground_inst, real_unify,
+ UnifyInstX, _Det, ModuleInfo0, ModuleInfo1)
then
- mode_info_set_module_info(ModuleInfo, !ModeInfo),
- modecheck_set_var_inst(X, UnifyInstForTypeX, no, !ModeInfo),
- ModeX = from_to_mode(InstX, UnifyInstForTypeX),
- ( if inst_is_free(ModuleInfo0, InstY) then
- % Y is free so bind the coercion result to Y.
- modecheck_set_var_inst(Y, UnifyInstForTypeY, no, !ModeInfo),
- ModeY = from_to_mode(InstY, UnifyInstForTypeY),
- Res = coerce_mode_ok([X, Y], [ModeX, ModeY], no_extra_goals)
- else
- % Y is bound so bind the coercion result to a fresh
- % variable YPrime, then unify Y = YPrime.
- create_fresh_var(TypeY, YPrime, !ModeInfo),
- create_var_var_unification(Y, YPrime, TypeY,
- !.ModeInfo, ExtraGoal),
- ExtraGoals = extra_goals([], [ExtraGoal]),
- modecheck_set_var_inst(YPrime, UnifyInstForTypeY, no,
- !ModeInfo),
- ModeYPrime = from_to_mode(free_inst, UnifyInstForTypeY),
- Res = coerce_mode_ok([X, YPrime], [ModeX, ModeYPrime],
- ExtraGoals)
- )
+ ModuleInfo = ModuleInfo1,
+ FinalInstX = UnifyInstX
else
- set_of_var.init(WaitingVars),
- ModeError =
- mode_error_coerce_bad_result_inst(UnifyInstForTypeX, TypeY),
- mode_info_error(WaitingVars, ModeError, !ModeInfo),
- Res = coerce_mode_error
- )
- else
- unexpected($pred, "abstractly_unify_inst failed")
- ).
-
-%---------------------------------------------------------------------------%
-
- % Produce a bound() inst covering all constructors of the du type, and
- % recursively produce bound() insts for constructor arguments. To prevent
- % infinite recursion, return ground for recursive nodes in the type tree.
- %
- % If the given type is not a du or tuple type, simply return ground.
- %
-:- pred make_bound_inst_for_type(module_info::in, set(type_ctor)::in,
- uniqueness::in, mer_type::in, mer_inst::out) is det.
-
-make_bound_inst_for_type(ModuleInfo, Seen0, Uniq, Type, Inst) :-
- (
- Type = type_variable(_, _),
- Inst = ground_or_unique_inst(Uniq)
- ;
- Type = builtin_type(_),
- Inst = ground_or_unique_inst(Uniq)
- ;
- Type = defined_type(_SymName, _ArgTypes, _Kind),
- % XXX the seen set should probably include type arguments, not only the
- % type_ctor
- type_to_ctor_det(Type, TypeCtor),
- ( if set.insert_new(TypeCtor, Seen0, Seen) then
- % type_constructors substitutes type args into constructors.
- ( if type_constructors(ModuleInfo, Type, Constructors) then
- constructors_to_bound_insts_rec(ModuleInfo, Seen, TypeCtor,
- Uniq, Constructors, BoundInsts0),
- list.sort_and_remove_dups(BoundInsts0, BoundInsts),
- % XXX A better approximation of InstResults is probably
- % possible.
- InstResults = inst_test_results(
- inst_result_is_ground,
- inst_result_does_not_contain_any,
- inst_result_contains_inst_names_unknown,
- inst_result_contains_inst_vars_unknown,
- inst_result_contains_types_unknown,
- inst_result_no_type_ctor_propagated
- ),
- Inst = bound(Uniq, InstResults, BoundInsts)
- else
- % Type with no definition, e.g. void
- Inst = ground_or_unique_inst(Uniq)
- )
+ unexpected($pred, "abstractly_unify_inst failed")
+ ),
+ mode_info_set_module_info(ModuleInfo, !ModeInfo),
+ modecheck_set_var_inst(X, FinalInstX, no, !ModeInfo),
+ ModeX = from_to_mode(InstX, FinalInstX),
+ ( if inst_is_free(ModuleInfo, InstY) then
+ % Y is free so bind the coercion result to Y.
+ modecheck_set_var_inst(Y, FinalInstY, no, !ModeInfo),
+ ModeY = from_to_mode(InstY, FinalInstY),
+ Res = coerce_mode_ok([X, Y], [ModeX, ModeY], no_extra_goals)
else
- % Does typed_ground help?
- Inst = defined_inst(typed_ground(Uniq, Type))
+ % Y is bound so bind the coercion result to a fresh variable
+ % YPrime, then unify Y = YPrime.
+ create_fresh_var(TypeY, YPrime, !ModeInfo),
+ create_var_var_unification(Y, YPrime, TypeY, !.ModeInfo,
+ ExtraGoal),
+ ExtraGoals = extra_goals([], [ExtraGoal]),
+ modecheck_set_var_inst(YPrime, FinalInstY, no, !ModeInfo),
+ ModeYPrime = from_to_mode(free_inst, FinalInstY),
+ Res = coerce_mode_ok([X, YPrime], [ModeX, ModeYPrime], ExtraGoals)
)
;
- Type = tuple_type(ArgTypes, _Kind),
- list.length(ArgTypes, Arity),
- ConsId = tuple_cons(Arity),
- list.map(make_bound_inst_for_type(ModuleInfo, Seen0, Uniq),
- ArgTypes, ArgInsts),
- BoundInst = bound_functor(ConsId, ArgInsts),
- % XXX A better approximation of InstResults is probably possible.
- InstResults = inst_test_results(
- inst_result_is_ground,
- inst_result_does_not_contain_any,
- inst_result_contains_inst_names_unknown,
- inst_result_contains_inst_vars_unknown,
- inst_result_contains_types_unknown,
- inst_result_no_type_ctor_propagated
- ),
- Inst = bound(Uniq, InstResults, [BoundInst])
- ;
- Type = higher_order_type(_PredOrFunc, _ArgTypes, _HOInstInfo, _Purity,
- _EvalMethod),
- Inst = ground_or_unique_inst(Uniq)
- ;
- Type = apply_n_type(_, _, _),
- sorry($pred, "apply_n_type")
- ;
- Type = kinded_type(Type1, _),
- make_bound_inst_for_type(ModuleInfo, Seen0, Uniq, Type1, Inst)
- ).
-
- % Similar to mode_util.constructors_to_bound_insts but also produces
- % bound() insts for the constructor arguments, recursively.
- %
-:- pred constructors_to_bound_insts_rec(module_info::in, set(type_ctor)::in,
- type_ctor::in, uniqueness::in, list(constructor)::in,
- list(bound_inst)::out) is det.
-
-constructors_to_bound_insts_rec(ModuleInfo, Seen, TypeCtor, Uniq,
- Constructors, BoundInsts) :-
- constructors_to_bound_insts_loop_over_ctors(ModuleInfo, Seen, TypeCtor,
- Uniq, Constructors, BoundInsts).
-
-:- pred constructors_to_bound_insts_loop_over_ctors(module_info::in,
- set(type_ctor)::in, type_ctor::in, uniqueness::in, list(constructor)::in,
- list(bound_inst)::out) is det.
-
-constructors_to_bound_insts_loop_over_ctors(_ModuleInfo, _Seen, _TypeCtor,
- _Uniq, [], []).
-constructors_to_bound_insts_loop_over_ctors(ModuleInfo, Seen, TypeCtor,
- Uniq, [Ctor | Ctors], [BoundInst | BoundInsts]) :-
- Ctor = ctor(_Ordinal, _MaybeExistConstraints, Name, Args, _Arity, _Ctxt),
- ctor_arg_list_to_inst_list(ModuleInfo, Seen, Uniq, Args, ArgInsts),
- list.length(ArgInsts, Arity),
- BoundInst = bound_functor(cons(Name, Arity, TypeCtor), ArgInsts),
- constructors_to_bound_insts_loop_over_ctors(ModuleInfo, Seen, TypeCtor,
- Uniq, Ctors, BoundInsts).
-
-:- pred ctor_arg_list_to_inst_list(module_info::in, set(type_ctor)::in,
- uniqueness::in, list(constructor_arg)::in, list(mer_inst)::out) is det.
-
-ctor_arg_list_to_inst_list(_ModuleInfo, _Seen, _Uniq, [], []).
-ctor_arg_list_to_inst_list(ModuleInfo, Seen, Uniq,
- [Arg | Args], [ArgInst | ArgInsts]) :-
- Arg = ctor_arg(_MaybeFieldName, ArgType, _Context),
- make_bound_inst_for_type(ModuleInfo, Seen, Uniq, ArgType, ArgInst),
- ctor_arg_list_to_inst_list(ModuleInfo, Seen, Uniq, Args, ArgInsts).
-
-:- func ground_or_unique_inst(uniqueness) = mer_inst.
-
-ground_or_unique_inst(Uniq) =
- ( if Uniq = shared then
- ground_inst
- else
- ground(Uniq, none_or_default_func)
- ).
-
-%---------------------------------------------------------------------------%
-
- % Check that a bound() inst only includes functors that are constructors of
- % the given type, recursively. Insts are otherwise assumed to be valid for
- % the type, and not checked to be valid for the type in other respects.
- %
- % On success, Inst is Inst0 (possibly expanded), with the type_ctors in
- % cons_ids replaced by the type_ctor of Type.
- %
-:- pred check_bound_functors_in_type(module_info::in, mer_type::in,
- mer_inst::in, mer_inst::out) is semidet.
-
-check_bound_functors_in_type(ModuleInfo, Type, Inst0, Inst) :-
- inst_expand(ModuleInfo, Inst0, Inst1),
- require_complete_switch [Type]
- (
- Type = type_variable(_, _),
- Inst = Inst1
- ;
- Type = builtin_type(_),
- Inst = Inst1
- ;
- Type = defined_type(_, _, _),
- check_bound_functors_in_defined_type(ModuleInfo, Type, Inst1, Inst)
- ;
- Type = tuple_type(ArgTypes, _Kind),
- check_bound_functors_in_tuple(ModuleInfo, ArgTypes, Inst1, Inst)
- ;
- Type = higher_order_type(_PredOrFunc, ArgTypes, _HOInstInfo, _Purity,
- _EvalMethod),
- check_bound_functors_in_higher_order_type(ModuleInfo, ArgTypes,
- Inst1, Inst)
- ;
- Type = apply_n_type(_, _, _),
- fail
- ;
- Type = kinded_type(Type1, _Kind),
- check_bound_functors_in_type(ModuleInfo, Type1, Inst1, Inst)
- ).
-
-%---------------------%
-
-:- pred check_bound_functors_in_defined_type(module_info::in, mer_type::in,
- mer_inst::in, mer_inst::out) is semidet.
-
-check_bound_functors_in_defined_type(ModuleInfo, Type, Inst0, Inst) :-
- require_complete_switch [Inst0]
- (
- Inst0 = bound(Uniq, _InstResults0, BoundInsts0),
- type_to_ctor(Type, TypeCtor),
- % type_constructors substitutes type args into constructors.
- type_constructors(ModuleInfo, Type, Constructors),
- list.map(
- check_bound_functor_in_du_type(ModuleInfo, TypeCtor, Constructors),
- BoundInsts0, BoundInsts),
- % XXX A better approximation of InstResults is probably possible.
- Inst = bound(Uniq, inst_test_no_results, BoundInsts)
- ;
- Inst0 = ground(_Uniq, _HOInstInfo),
- Inst = Inst0
- ;
- Inst0 = constrained_inst_vars(InstVars, SubInst0),
- check_bound_functors_in_defined_type(ModuleInfo, Type,
- SubInst0, SubInst),
- Inst = constrained_inst_vars(InstVars, SubInst)
- ;
- ( Inst0 = free
- ; Inst0 = free(_)
- ; Inst0 = any(_, _)
- ; Inst0 = not_reached
- ; Inst0 = inst_var(_)
- ; Inst0 = abstract_inst(_, _)
- ),
- fail
- ;
- Inst0 = defined_inst(_),
- unexpected($pred, "unexpanded inst")
- ).
-
-:- pred check_bound_functor_in_du_type(module_info::in, type_ctor::in,
- list(constructor)::in, bound_inst::in, bound_inst::out) is semidet.
-
-check_bound_functor_in_du_type(ModuleInfo, TypeCtor, Ctors,
- BoundInst0, BoundInst) :-
- BoundInst0 = bound_functor(ConsId0, ArgInsts0),
- ConsId0 = cons(SymName0, Arity, _TypeCtor0),
- Name = unqualify_name(SymName0),
- find_first_matching_constructor_unqual(Name, Arity, Ctors, MatchingCtor),
- MatchingCtor = ctor(_, _, SymName, CtorArgs, _, _),
- ConsId = cons(SymName, Arity, TypeCtor),
- check_bound_functors_in_ctor_args(ModuleInfo, CtorArgs,
- ArgInsts0, ArgInsts),
- BoundInst = bound_functor(ConsId, ArgInsts).
-
-:- pred find_first_matching_constructor_unqual(string::in, int::in,
- list(constructor)::in, constructor::out) is semidet.
-
-find_first_matching_constructor_unqual(Name, Arity, [Ctor | Ctors],
- MatchingCtor) :-
- ( if
- Ctor = ctor(_, _, ConsName, _, Arity, _),
- unqualify_name(ConsName) = Name
- then
- MatchingCtor = Ctor
- else
- find_first_matching_constructor_unqual(Name, Arity, Ctors, MatchingCtor)
- ).
-
-:- pred check_bound_functors_in_ctor_args(module_info::in,
- list(constructor_arg)::in, list(mer_inst)::in, list(mer_inst)::out)
- is semidet.
-
-check_bound_functors_in_ctor_args(_, [], [], []).
-check_bound_functors_in_ctor_args(ModuleInfo, [CtorArg | CtorArgs],
- [ArgInst0 | ArgInsts0], [ArgInst | ArgInsts]) :-
- check_bound_functors_in_ctor_arg(ModuleInfo, CtorArg, ArgInst0, ArgInst),
- check_bound_functors_in_ctor_args(ModuleInfo, CtorArgs,
- ArgInsts0, ArgInsts).
-
-:- pred check_bound_functors_in_ctor_arg(module_info::in, constructor_arg::in,
- mer_inst::in, mer_inst::out) is semidet.
-
-check_bound_functors_in_ctor_arg(ModuleInfo, CtorArg, ArgInst0, ArgInst) :-
- CtorArg = ctor_arg(_MaybeFieldName, ArgType, _Context),
- check_bound_functors_in_type(ModuleInfo, ArgType, ArgInst0, ArgInst).
-
-%---------------------%
-
-:- pred check_bound_functors_in_tuple(module_info::in, list(mer_type)::in,
- mer_inst::in, mer_inst::out) is semidet.
-
-check_bound_functors_in_tuple(ModuleInfo, ArgTypes, Inst0, Inst) :-
- require_complete_switch [Inst0]
- (
- Inst0 = bound(Uniq, _InstTestsResults, BoundInsts0),
- list.map(bound_check_bound_functors_in_tuple(ModuleInfo, ArgTypes),
- BoundInsts0, BoundInsts),
- Inst = bound(Uniq, inst_test_no_results, BoundInsts)
- ;
- Inst0 = ground(_Uniq, _HOInstInfo),
- Inst = Inst0
- ;
- Inst0 = constrained_inst_vars(_, _),
- sorry($pred, "constrained_inst_vars")
- ;
- ( Inst0 = free
- ; Inst0 = free(_)
- ; Inst0 = any(_, _)
- ; Inst0 = not_reached
- ; Inst0 = inst_var(_)
- ; Inst0 = abstract_inst(_, _)
- ),
- fail
- ;
- Inst0 = defined_inst(_),
- unexpected($pred, "unexpanded inst")
- ).
-
-:- pred bound_check_bound_functors_in_tuple(module_info::in,
- list(mer_type)::in, bound_inst::in, bound_inst::out) is semidet.
-
-bound_check_bound_functors_in_tuple(ModuleInfo, ArgTypes,
- BoundInst0, BoundInst) :-
- BoundInst0 = bound_functor(ConsId, ArgInsts0),
- list.length(ArgTypes, Arity),
- ConsId = tuple_cons(Arity),
- check_bound_functors_in_tuple_args(ModuleInfo, ArgTypes,
- ArgInsts0, ArgInsts),
- BoundInst = bound_functor(ConsId, ArgInsts).
-
-:- pred check_bound_functors_in_tuple_args(module_info::in, list(mer_type)::in,
- list(mer_inst)::in, list(mer_inst)::out) is semidet.
-
-check_bound_functors_in_tuple_args(_ModuleInfo, [], [], []).
-check_bound_functors_in_tuple_args(ModuleInfo,
- [Type | Types], [Inst0 | Insts0], [Inst | Insts]) :-
- check_bound_functors_in_type(ModuleInfo, Type, Inst0, Inst),
- check_bound_functors_in_tuple_args(ModuleInfo, Types, Insts0, Insts).
-
-%---------------------%
-
-:- pred check_bound_functors_in_higher_order_type(module_info::in,
- list(mer_type)::in, mer_inst::in, mer_inst::out) is semidet.
-
-check_bound_functors_in_higher_order_type(_ModuleInfo, _ArgTypes,
- Inst0, Inst) :-
- require_complete_switch [Inst0]
- (
- Inst0 = ground(_Uniq, _HOInstInfo),
- Inst = Inst0
- ;
- Inst0 = bound(_Uniq, _InstTestsResults, _BoundInsts),
- % XXX is this reachable?
- sorry($pred, "bound inst")
- ;
- Inst0 = constrained_inst_vars(_, _),
- sorry($pred, "constrained_inst_vars")
- ;
- ( Inst0 = free
- ; Inst0 = free(_)
- ; Inst0 = any(_, _)
- ; Inst0 = not_reached
- ; Inst0 = inst_var(_)
- ; Inst0 = abstract_inst(_, _)
- ),
- fail
- ;
- Inst0 = defined_inst(_),
- unexpected($pred, "unexpanded inst")
+ MaybeFinalInstY = no,
+ ModeError = mode_error_coerce_invalid(InstX, TypeY),
+ set_of_var.init(WaitingVars),
+ mode_info_error(WaitingVars, ModeError, !ModeInfo),
+ Res = coerce_mode_error
).
-%---------------------------------------------------------------------------%
-
:- pred create_fresh_var(mer_type::in, prog_var::out,
mode_info::in, mode_info::out) is det.
@@ -514,6 +189,628 @@ create_fresh_var(VarType, Var, !ModeInfo) :-
mode_info_set_varset(VarSet, !ModeInfo),
mode_info_set_var_types(VarTypes, !ModeInfo).
+%---------------------------------------------------------------------------%
+
+:- type expanded_insts == set(pair(inst_name, mer_type)).
+
+ % Try to produce the resulting inst of a coercion from TypeX to TypeY.
+ % InstX is the initial inst of the input term,
+ % InstY is the final inst of the result term.
+ %
+:- pred modecheck_coerce_make_inst(module_info::in, tvarset::in, is_live::in,
+ mer_type::in, mer_type::in, expanded_insts::in,
+ mer_inst::in, maybe(mer_inst)::out) is det.
+
+modecheck_coerce_make_inst(ModuleInfo, TVarSet, LiveX, TypeX, TypeY,
+ ExpandedInsts0, InstX, Res) :-
+ (
+ ( InstX = free
+ ; InstX = free(_)
+ ),
+ unexpected($pred, "free inst")
+ ;
+ InstX = any(_, _),
+ unexpected($pred, "any inst")
+ ;
+ InstX = bound(UniqX, _InstResultsX, FunctorsX),
+ modecheck_coerce_make_bound_inst(ModuleInfo, TVarSet, LiveX, UniqX,
+ TypeX, TypeY, ExpandedInsts0, FunctorsX, Res)
+ ;
+ InstX = ground(UniqX, HOInstInfoX),
+ (
+ HOInstInfoX = none_or_default_func,
+ modecheck_coerce_from_ground_make_inst(ModuleInfo, TVarSet,
+ LiveX, UniqX, TypeX, TypeY, Res)
+ ;
+ HOInstInfoX = higher_order(_PredInstInfoX),
+ UniqY = make_result_uniq(LiveX, UniqX),
+ % Coerce cannot change the calling convention.
+ InstY = ground(UniqY, HOInstInfoX),
+ Res = yes(InstY)
+ )
+ ;
+ InstX = not_reached,
+ InstY = not_reached,
+ Res = yes(InstY)
+ ;
+ InstX = inst_var(_),
+ unexpected($pred, "uninstantiated inst parameter")
+ ;
+ InstX = constrained_inst_vars(InstVars, SubInstX),
+ % The term of TypeX is approximated by a ground inst SubInstX.
+ % After conversion, the term of TypeY must be approximated by
+ % a ground inst SubInstY.
+ modecheck_coerce_make_inst(ModuleInfo, TVarSet, LiveX, TypeX, TypeY,
+ ExpandedInsts0, SubInstX, SubRes),
+ (
+ SubRes = yes(SubInstY),
+ InstY = constrained_inst_vars(InstVars, SubInstY),
+ Res = yes(InstY)
+ ;
+ SubRes = no,
+ Res = no
+ )
+ ;
+ InstX = defined_inst(InstNameX),
+ % Avoid infinite loops. We track inst-type pairs because a user-defined
+ % inst can be used with different types.
+ ( if
+ set.insert_new(InstNameX - TypeX, ExpandedInsts0, ExpandedInsts1)
+ then
+ inst_lookup(ModuleInfo, InstNameX, InstX1),
+ modecheck_coerce_make_inst(ModuleInfo, TVarSet, LiveX,
+ TypeX, TypeY, ExpandedInsts1, InstX1, Res)
+ else
+ % If we would enter an infinite loop, return the inst unexpanded.
+ % Just in case, ensure that we are definitely dealing with
+ % user-defined inst; and TypeX =< TypeY so an inst valid for
+ % TypeX must be valid for TypeY.
+ % The sanity checks might not be strictly necessary.
+ ( if
+ is_user_inst(InstNameX),
+ check_is_subtype(ModuleInfo, TVarSet, TypeX, TypeY)
+ then
+ InstY = defined_inst(InstNameX),
+ Res = yes(InstY)
+ else
+ Res = no
+ )
+ )
+ ;
+ InstX = abstract_inst(_, _),
+ unexpected($pred, "abstract inst")
+ ).
+
+:- func make_result_uniq(is_live, uniqueness) = uniqueness.
+
+make_result_uniq(LiveX, UniqX) = UniqY :-
+ (
+ UniqX = shared,
+ UniqY = shared
+ ;
+ ( UniqX = unique
+ ; UniqX = mostly_unique
+ ),
+ (
+ LiveX = is_live,
+ UniqY = shared
+ ;
+ LiveX = is_dead,
+ UniqY = UniqX
+ )
+ ;
+ ( UniqX = clobbered
+ ; UniqX = mostly_clobbered
+ ),
+ % We know that the input must not be clobbered.
+ unexpected($pred, "clobbered")
+ ).
+
+:- pred is_user_inst(inst_name::in) is semidet.
+
+is_user_inst(InstName) :-
+ require_complete_switch [InstName]
+ (
+ InstName = user_inst(_, _)
+ ;
+ InstName = typed_inst(_, InstName1),
+ is_user_inst(InstName1)
+ ;
+ ( InstName = unify_inst(_, _, _, _)
+ ; InstName = merge_inst(_, _)
+ ; InstName = ground_inst(_, _, _, _)
+ ; InstName = any_inst(_, _, _, _)
+ ; InstName = shared_inst(_)
+ ; InstName = mostly_uniq_inst(_)
+ ; InstName = typed_ground(_, _)
+ ),
+ sorry($pred, "unexpected compiler generated inst_name")
+ ).
+
+%---------------------------------------------------------------------------%
+
+:- pred modecheck_coerce_make_bound_inst(module_info::in, tvarset::in,
+ is_live::in, uniqueness::in, mer_type::in, mer_type::in,
+ expanded_insts::in, list(bound_inst)::in, maybe(mer_inst)::out) is det.
+
+modecheck_coerce_make_bound_inst(ModuleInfo, TVarSet, LiveX, UniqX,
+ TypeX, TypeY, ExpandedInsts0, FunctorsX, Res) :-
+ ( if
+ modecheck_coerce_make_bound_functors(ModuleInfo, TVarSet, LiveX,
+ TypeX, TypeY, ExpandedInsts0, FunctorsX, FunctorsY)
+ then
+ UniqY = make_result_uniq(LiveX, UniqX),
+ % XXX A better approximation of InstResults is probably possible.
+ InstResults = inst_test_results(
+ inst_result_is_ground,
+ inst_result_does_not_contain_any,
+ inst_result_contains_inst_names_unknown,
+ inst_result_contains_inst_vars_unknown,
+ inst_result_contains_types_unknown,
+ inst_result_no_type_ctor_propagated
+ ),
+ InstY = bound(UniqY, InstResults, FunctorsY),
+ Res = yes(InstY)
+ else
+ Res = no
+ ).
+
+:- pred modecheck_coerce_make_bound_functors(module_info::in, tvarset::in,
+ is_live::in, mer_type::in, mer_type::in, expanded_insts::in,
+ list(bound_inst)::in, list(bound_inst)::out) is semidet.
+
+modecheck_coerce_make_bound_functors(ModuleInfo, TVarSet, LiveX,
+ TypeX, TypeY, ExpandedInsts0, FunctorsX, FunctorsY) :-
+ (
+ FunctorsX = [],
+ FunctorsY = []
+ ;
+ FunctorsX = [HeadFunctorX | TailFunctorsX],
+ modecheck_coerce_make_bound_functor(ModuleInfo, TVarSet, LiveX,
+ TypeX, TypeY, ExpandedInsts0, HeadFunctorX, yes(HeadFunctorY)),
+ modecheck_coerce_make_bound_functors(ModuleInfo, TVarSet, LiveX,
+ TypeX, TypeY, ExpandedInsts0, TailFunctorsX, TailFunctorsY),
+ FunctorsY = [HeadFunctorY | TailFunctorsY]
+ ).
+
+:- pred modecheck_coerce_make_bound_functor(module_info::in, tvarset::in,
+ is_live::in, mer_type::in, mer_type::in, expanded_insts::in,
+ bound_inst::in, maybe(bound_inst)::out) is det.
+
+modecheck_coerce_make_bound_functor(ModuleInfo, TVarSet, LiveX,
+ TypeX, TypeY, ExpandedInsts0, FunctorX, Res) :-
+ FunctorX = bound_functor(ConsIdX, ArgInstsX),
+ % The user may have provided an inst that does not make sense for the type.
+ % The compiler does not check for that elsewhere (probably it should)
+ % so we try to be careful about that here.
+ (
+ ConsIdX = cons(_, _, _),
+ ( if
+ get_bound_functor_cons_and_arg_types(ModuleInfo, TypeX, TypeY,
+ ConsIdX, ConsIdY, ArgTypesX, ArgTypesY, Arity),
+ list.length(ArgInstsX, Arity)
+ then
+ ( if
+ modecheck_coerce_from_bound_make_bound_functor_arg_insts(
+ ModuleInfo, TVarSet, LiveX, ExpandedInsts0,
+ ArgTypesX, ArgTypesY, ArgInstsX, ArgInstsY)
+ then
+ FunctorY = bound_functor(ConsIdY, ArgInstsY),
+ Res = yes(FunctorY)
+ else
+ Res = no
+ )
+ else
+ Res = no
+ )
+ ;
+ ConsIdX = tuple_cons(_),
+ % XXX post-typecheck does not replace occurences of
+ % cons(unqualified("{}"), ...) with tuple_cons yet.
+ sorry($pred, "tuple_cons")
+ ;
+ ( ConsIdX = int_const(_)
+ ; ConsIdX = uint_const(_)
+ ; ConsIdX = int8_const(_)
+ ; ConsIdX = uint8_const(_)
+ ; ConsIdX = int16_const(_)
+ ; ConsIdX = uint16_const(_)
+ ; ConsIdX = int32_const(_)
+ ; ConsIdX = uint32_const(_)
+ ; ConsIdX = int64_const(_)
+ ; ConsIdX = uint64_const(_)
+ ; ConsIdX = float_const(_)
+ ; ConsIdX = char_const(_)
+ ; ConsIdX = string_const(_)
+ ),
+ ( if
+ cons_id_matches_builtin_type(ConsIdX, TypeX),
+ TypeX = TypeY,
+ ArgInstsX = []
+ then
+ FunctorY = FunctorX,
+ Res = yes(FunctorY)
+ else
+ Res = no
+ )
+ ;
+ ( ConsIdX = closure_cons(_, _)
+ ; ConsIdX = impl_defined_const(_)
+ ; ConsIdX = type_ctor_info_const(_, _, _)
+ ; ConsIdX = base_typeclass_info_const(_, _, _, _)
+ ; ConsIdX = type_info_cell_constructor(_)
+ ; ConsIdX = type_info_const(_)
+ ; ConsIdX = typeclass_info_cell_constructor
+ ; ConsIdX = typeclass_info_const(_)
+ ; ConsIdX = ground_term_const(_, _)
+ ; ConsIdX = tabling_info_const(_)
+ ; ConsIdX = table_io_entry_desc(_)
+ ; ConsIdX = deep_profiling_proc_layout(_)
+ ),
+ unexpected($pred, "unsupported cons_id")
+ ).
+
+:- pred get_bound_functor_cons_and_arg_types(module_info::in,
+ mer_type::in, mer_type::in, cons_id::in(cons), cons_id::out(cons),
+ list(mer_type)::out, list(mer_type)::out, int::out) is semidet.
+
+get_bound_functor_cons_and_arg_types(ModuleInfo, TypeX, TypeY,
+ ConsIdX, ConsIdY, ArgTypesX, ArgTypesY, Arity) :-
+ type_to_ctor(TypeY, TypeCtorY),
+ make_cons_id_for_type_ctor(TypeCtorY, ConsIdX, ConsIdY),
+ require_complete_switch [TypeX]
+ (
+ TypeX = defined_type(_, _, _),
+ TypeY = defined_type(_, _, _),
+ % This fails if the input type does not actually have the
+ % functor given in a `bound' inst.
+ get_ctor_arg_types_do_subst(ModuleInfo, TypeX, ConsIdX,
+ ArgTypesX),
+ % This fails if the result type does not have a constructor
+ % matching that of the input type.
+ get_ctor_arg_types_do_subst(ModuleInfo, TypeY, ConsIdY,
+ ArgTypesY),
+ list.length(ArgTypesX, Arity),
+ list.length(ArgTypesY, Arity)
+ ;
+ TypeX = tuple_type(ArgTypesX, _),
+ TypeY = tuple_type(ArgTypesY, _),
+ ConsIdX = cons(unqualified("{}"), Arity, _),
+ list.length(ArgTypesX, Arity),
+ list.length(ArgTypesY, Arity)
+ ;
+ TypeX = builtin_type(BuiltinType),
+ TypeY = builtin_type(BuiltinType),
+ % `cons' is used for char.
+ BuiltinType = builtin_type_char,
+ ConsIdX = cons(_SymName, Arity, _),
+ Arity = 0,
+ ArgTypesX = [],
+ ArgTypesY = []
+ ;
+ TypeX = kinded_type(TypeX1, Kind),
+ TypeY = kinded_type(TypeY1, Kind),
+ get_bound_functor_cons_and_arg_types(ModuleInfo, TypeX1, TypeY1,
+ ConsIdX, ConsIdY, ArgTypesX, ArgTypesY, Arity)
+ ;
+ ( TypeX = type_variable(_, _)
+ ; TypeX = higher_order_type(_, _, _, _, _)
+ ; TypeX = apply_n_type(_, _, _)
+ ),
+ fail
+ ).
+
+:- pred modecheck_coerce_from_bound_make_bound_functor_arg_insts(
+ module_info::in, tvarset::in, is_live::in, expanded_insts::in,
+ list(mer_type)::in, list(mer_type)::in,
+ list(mer_inst)::in, list(mer_inst)::out) is semidet.
+
+modecheck_coerce_from_bound_make_bound_functor_arg_insts(ModuleInfo, TVarSet,
+ LiveX, ExpandedInsts0, ArgTypesX, ArgTypesY, ArgInstsX, ArgInstsY) :-
+ ( if
+ ArgTypesX = [],
+ ArgTypesY = [],
+ ArgInstsX = []
+ then
+ ArgInstsY = []
+ else if
+ ArgTypesX = [HeadArgTypeX | TailArgTypesX],
+ ArgTypesY = [HeadArgTypeY | TailArgTypesY],
+ ArgInstsX = [HeadArgInstX | TailArgInstsX]
+ then
+ modecheck_coerce_make_inst(ModuleInfo, TVarSet, LiveX,
+ HeadArgTypeX, HeadArgTypeY, ExpandedInsts0,
+ HeadArgInstX, yes(HeadArgInstY)),
+ modecheck_coerce_from_bound_make_bound_functor_arg_insts(ModuleInfo,
+ TVarSet, LiveX, ExpandedInsts0,
+ TailArgTypesX, TailArgTypesY,
+ TailArgInstsX, TailArgInstsY),
+ ArgInstsY = [HeadArgInstY | TailArgInstsY]
+ else
+ unexpected($pred, "length mismatch")
+ ).
+
+:- pred cons_id_matches_builtin_type(cons_id::in, mer_type::in) is semidet.
+
+cons_id_matches_builtin_type(ConsId, Type) :-
+ ( ConsId = int_const(_), Type = int_type
+ ; ConsId = uint_const(_), Type = uint_type
+ ; ConsId = int8_const(_), Type = int8_type
+ ; ConsId = uint8_const(_), Type = uint8_type
+ ; ConsId = int16_const(_), Type = int16_type
+ ; ConsId = uint16_const(_), Type = uint16_type
+ ; ConsId = int32_const(_), Type = int32_type
+ ; ConsId = uint32_const(_), Type = uint32_type
+ ; ConsId = int64_const(_), Type = int64_type
+ ; ConsId = uint64_const(_), Type = uint64_type
+ ; ConsId = float_const(_), Type = float_type
+ ; ConsId = char_const(_), Type = char_type
+ ; ConsId = string_const(_), Type = string_type
+ ).
+
+%---------------------------------------------------------------------------%
+
+:- pred modecheck_coerce_from_ground_make_inst(module_info::in, tvarset::in,
+ is_live::in, uniqueness::in, mer_type::in, mer_type::in,
+ maybe(mer_inst)::out) is det.
+
+modecheck_coerce_from_ground_make_inst(ModuleInfo, TVarSet, LiveX, UniqX,
+ TypeX, TypeY, MaybeInstY) :-
+ ( if TypeX = TypeY then
+ % This should be a common case.
+ UniqY = make_result_uniq(LiveX, UniqX),
+ InstY = ground(UniqY, none_or_default_func),
+ MaybeInstY = yes(InstY)
+ else if check_is_subtype(ModuleInfo, TVarSet, TypeX, TypeY) then
+ set.init(SeenTypes0),
+ modecheck_coerce_from_ground_make_inst_2(ModuleInfo, TVarSet,
+ LiveX, UniqX, SeenTypes0, TypeX, TypeY, InstY),
+ MaybeInstY = yes(InstY)
+ else
+ MaybeInstY = no
+ ).
+
+ % Precondition: TypeX =< TypeY.
+ %
+:- pred modecheck_coerce_from_ground_make_inst_2(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.
+
+modecheck_coerce_from_ground_make_inst_2(ModuleInfo, TVarSet, LiveX, UniqX,
+ SeenTypes0, TypeX, TypeY, InstY) :-
+ % We can preserve more information by creating a `bound' inst from the
+ % constructors in TypeX. This is only worth doing if the types differ,
+ % and if it would not lead to an infinite loop.
+ ( if
+ TypeX \= TypeY,
+ set.insert_new(TypeX, SeenTypes0, SeenTypes1)
+ then
+ modecheck_coerce_from_ground_make_bound_inst(ModuleInfo, TVarSet,
+ LiveX, UniqX, SeenTypes1, TypeX, TypeY, InstY)
+ else
+ UniqY = make_result_uniq(LiveX, UniqX),
+ InstY = ground_or_unique_inst(UniqY)
+ ).
+
+:- 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.
+
+modecheck_coerce_from_ground_make_bound_inst(ModuleInfo, TVarSet,
+ LiveX, UniqX, SeenTypes, TypeX, TypeY, InstY) :-
+ ( if type_constructors(ModuleInfo, TypeX, CtorsX) then
+ list.map(
+ modecheck_coerce_from_ground_make_bound_functor(ModuleInfo,
+ TVarSet, LiveX, UniqX, SeenTypes, TypeX, TypeY),
+ CtorsX, FunctorsY),
+ UniqY = make_result_uniq(LiveX, UniqX),
+ % XXX A better approximation of InstResults is probably possible.
+ InstResults = inst_test_results(
+ inst_result_is_ground,
+ inst_result_does_not_contain_any,
+ inst_result_contains_inst_names_unknown,
+ inst_result_contains_inst_vars_unknown,
+ inst_result_contains_types_unknown,
+ inst_result_no_type_ctor_propagated
+ ),
+ InstY = bound(UniqY, InstResults, FunctorsY)
+ else
+ unexpected($pred, "missing constructors")
+ ).
+
+:- pred modecheck_coerce_from_ground_make_bound_functor(module_info::in,
+ tvarset::in, is_live::in, uniqueness::in, set(mer_type)::in,
+ mer_type::in, mer_type::in, constructor::in, bound_inst::out) is det.
+
+modecheck_coerce_from_ground_make_bound_functor(ModuleInfo, TVarSet,
+ LiveX, UniqX, SeenTypes, _TypeX, TypeY, CtorX, FunctorY) :-
+ CtorX = ctor(_OrdinalX, _MaybeExistConstraintsX, CtorNameX, CtorArgsX,
+ CtorArity, _ContextX),
+
+ % Make the corresponding cons_id for TypeCtorY.
+ type_to_ctor_det(TypeY, TypeCtorY),
+ ModuleNameY = type_ctor_module(TypeCtorY),
+ maybe_change_module_qualifier(ModuleNameY, CtorNameX, CtorNameY),
+ ConsIdY = cons(CtorNameY, CtorArity, TypeCtorY),
+
+ % Get the argument types for the constructors of both types,
+ % with type arguments substituted in.
+ % type_constructors already substituted type args into CtorArgsX.
+ list.map(get_ctor_arg_type, CtorArgsX, ArgTypesX),
+ ( if
+ get_ctor_arg_types_do_subst(ModuleInfo, TypeY, ConsIdY, ArgTypesY0)
+ then
+ ArgTypesY = ArgTypesY0
+ else
+ % The constructor should exist in TypeY since TypeX =< TypeY.
+ unexpected($pred, "missing constructor for result type")
+ ),
+
+ % Make the argument insts for the bound functor.
+ list.map_corresponding(
+ modecheck_coerce_from_ground_make_inst_2(ModuleInfo, TVarSet,
+ LiveX, UniqX, SeenTypes),
+ ArgTypesX, ArgTypesY, ArgInstsY),
+
+ FunctorY = bound_functor(ConsIdY, ArgInstsY).
+
+:- func ground_or_unique_inst(uniqueness) = mer_inst.
+
+ground_or_unique_inst(Uniq) =
+ ( if Uniq = shared then
+ ground_inst
+ else
+ ground(Uniq, none_or_default_func)
+ ).
+
+%---------------------------------------------------------------------------%
+
+:- pred make_cons_id_for_type_ctor(type_ctor::in, cons_id::in(cons),
+ cons_id::out(cons)) is det.
+
+make_cons_id_for_type_ctor(TypeCtor, ConsId0, ConsId) :-
+ ConsId0 = cons(SymName0, Arity, TypeCtor0),
+ ModuleName = type_ctor_module(TypeCtor),
+ maybe_change_module_qualifier(ModuleName, SymName0, SymName),
+ ( if TypeCtor0 = cons_id_dummy_type_ctor then
+ % Keep the dummy type_ctor from the original cons_id.
+ % This probably makes no difference.
+ ConsId = cons(SymName, Arity, TypeCtor0)
+ else
+ ConsId = cons(SymName, Arity, TypeCtor)
+ ).
+
+:- pred maybe_change_module_qualifier(sym_name::in, sym_name::in,
+ sym_name::out) is det.
+
+maybe_change_module_qualifier(ModuleName, SymName0, SymName) :-
+ (
+ SymName0 = unqualified(_),
+ SymName = SymName0
+ ;
+ SymName0 = qualified(_ModuleName0, Name),
+ SymName = qualified(ModuleName, Name)
+ ).
+
+%---------------------------------------------------------------------------%
+
+:- pred get_ctor_arg_types_do_subst(module_info::in, mer_type::in, cons_id::in,
+ list(mer_type)::out) is semidet.
+
+get_ctor_arg_types_do_subst(ModuleInfo, Type, ConsId, CtorArgTypes) :-
+ type_to_ctor_and_args(Type, TypeCtor, TypeArgs),
+ module_info_get_cons_table(ModuleInfo, ConsTable),
+ search_cons_table_of_type_ctor(ConsTable, TypeCtor, ConsId, ConsDefn),
+ ConsDefn = hlds_cons_defn(_TypeCtor, _TVarSet, TypeParams, _KindMap,
+ _MaybeExistConstraints, CtorArgs, _Context),
+ list.map(get_ctor_arg_type, CtorArgs, CtorArgTypes0),
+ (
+ TypeParams = [],
+ CtorArgTypes = CtorArgTypes0
+ ;
+ TypeParams = [_ | _],
+ map.from_corresponding_lists(TypeParams, TypeArgs, Subst),
+ apply_subst_to_type_list(Subst, CtorArgTypes0, CtorArgTypes)
+ ).
+
+:- pred get_ctor_arg_type(constructor_arg::in, mer_type::out) is det.
+
+get_ctor_arg_type(ctor_arg(_, Type, _), Type).
+
+%---------------------------------------------------------------------------%
+
+:- type types_comparison
+ ---> compare_equal
+ ; compare_equal_lt.
+
+:- pred check_is_subtype(module_info::in, tvarset::in,
+ mer_type::in, mer_type::in) is semidet.
+
+check_is_subtype(ModuleInfo, TVarSet, TypeA, TypeB) :-
+ module_info_get_type_table(ModuleInfo, TypeTable),
+ compare_types(TypeTable, TVarSet, compare_equal_lt, TypeA, TypeB).
+
+ % Succeed if TypeA unifies with TypeB.
+ % If Comparison is compare_equal_lt, then also succeed if TypeA =< TypeB
+ % by subtype definitions.
+ %
+ % Note: this code is almost identical to compare_types in typecheck.m
+ % but since it is not part of the type checker, does not maintain
+ % type assignments.
+ %
+:- pred compare_types(type_table::in, tvarset::in, types_comparison::in,
+ mer_type::in, mer_type::in) is semidet.
+
+compare_types(TypeTable, TVarSet, Comparison, TypeA, TypeB) :-
+ ( if
+ ( TypeA = type_variable(_, _)
+ ; TypeB = type_variable(_, _)
+ )
+ then
+ % Unlike typecheck.compare_types which unifies two type variables,
+ % here we simply test for equality.
+ TypeA = TypeB
+ else
+ compare_types_nonvar(TypeTable, TVarSet, Comparison, TypeA, TypeB)
+ ).
+
+:- pred compare_types_nonvar(type_table::in, tvarset::in, types_comparison::in,
+ mer_type::in, mer_type::in) is semidet.
+
+compare_types_nonvar(TypeTable, TVarSet, Comparison, TypeA, TypeB) :-
+ require_complete_switch [TypeA]
+ (
+ TypeA = builtin_type(BuiltinType),
+ TypeB = builtin_type(BuiltinType)
+ ;
+ TypeA = type_variable(_, _),
+ TypeB = type_variable(_, _),
+ unexpected($pred, "type_variable")
+ ;
+ TypeA = defined_type(_, _, _),
+ type_to_ctor_and_args(TypeA, TypeCtorA, ArgsA),
+ type_to_ctor_and_args(TypeB, TypeCtorB, ArgsB),
+ ( if TypeCtorA = TypeCtorB then
+ compare_types_corresponding(TypeTable, TVarSet, Comparison,
+ ArgsA, ArgsB)
+ else
+ Comparison = compare_equal_lt,
+ get_supertype(TypeTable, TVarSet, TypeCtorA, ArgsA, SuperTypeA),
+ compare_types(TypeTable, TVarSet, Comparison, SuperTypeA, TypeB)
+ )
+ ;
+ TypeA = tuple_type(ArgsA, Kind),
+ TypeB = tuple_type(ArgsB, Kind),
+ compare_types_corresponding(TypeTable, TVarSet, Comparison,
+ ArgsA, ArgsB)
+ ;
+ TypeA = higher_order_type(PredOrFunc, ArgsA, _HOInstInfoA,
+ Purity, EvalMethod),
+ TypeB = higher_order_type(PredOrFunc, ArgsB, _HOInstInfoB,
+ Purity, EvalMethod),
+ % We do not allow subtyping in higher order argument types.
+ compare_types_corresponding(TypeTable, TVarSet, compare_equal,
+ ArgsA, ArgsB)
+ ;
+ TypeA = apply_n_type(_, _, _),
+ sorry($pred, "apply_n_type")
+ ;
+ TypeA = kinded_type(TypeA1, Kind),
+ TypeB = kinded_type(TypeB1, Kind),
+ compare_types(TypeTable, TVarSet, Comparison, TypeA1, TypeB1)
+ ).
+
+:- pred compare_types_corresponding(type_table::in, tvarset::in,
+ types_comparison::in, list(mer_type)::in, list(mer_type)::in) is semidet.
+
+compare_types_corresponding(_TypeTable, _TVarSet, _Comparison,
+ [], []).
+compare_types_corresponding(TypeTable, TVarSet, Comparison,
+ [TypeA | TypesA], [TypeB | TypesB]) :-
+ compare_types(TypeTable, TVarSet, Comparison, TypeA, TypeB),
+ compare_types_corresponding(TypeTable, TVarSet, Comparison,
+ TypesA, TypesB).
+
%---------------------------------------------------------------------------%
:- end_module check_hlds.modecheck_coerce.
%---------------------------------------------------------------------------%
diff --git a/compiler/type_util.m b/compiler/type_util.m
index 32defbaa0..73cdf2828 100644
--- a/compiler/type_util.m
+++ b/compiler/type_util.m
@@ -188,13 +188,20 @@
:- pred type_ctor_has_hand_defined_rtti(type_ctor::in, hlds_type_body::in)
is semidet.
- % Return the base type ctor for a given type ctor.
- % This predicate must only be called with a type ctor that is known
- % to be a subtype or supertype type ctor, not with arbitrary type ctors.
+ % Return the base type constructor for a given type constructor.
+ % This predicate must only be called with a type constructor that is known
+ % to be a subtype or supertype type constructor, not with arbitrary type
+ % constructors.
%
:- pred get_base_type_ctor(type_table::in, type_ctor::in, type_ctor::out)
is semidet.
+ % Return the supertype of a type, if any.
+ % This will substitute the type's arguments into its declared supertype.
+ %
+:- pred get_supertype(type_table::in, tvarset::in, type_ctor::in,
+ list(mer_type)::in, mer_type::out) is semidet.
+
% Given a type, determine what category its principal constructor
% falls into.
%
@@ -976,6 +983,26 @@ get_base_type_ctor(TypeTable, TypeCtor, BaseTypeCtor) :-
%-----------------------------------------------------------------------------%
+get_supertype(TypeTable, TVarSet, TypeCtor, Args, SuperType) :-
+ hlds_data.search_type_ctor_defn(TypeTable, TypeCtor, TypeDefn),
+ hlds_data.get_type_defn_body(TypeDefn, TypeBody),
+ TypeBody = hlds_du_type(_, yes(SuperType0), _, _, _),
+ require_det (
+ % Create substitution from type parameters to Args.
+ hlds_data.get_type_defn_tvarset(TypeDefn, TVarSet0),
+ hlds_data.get_type_defn_tparams(TypeDefn, TypeParams0),
+ tvarset_merge_renaming(TVarSet, TVarSet0, _NewTVarSet, Renaming),
+ apply_variable_renaming_to_tvar_list(Renaming,
+ TypeParams0, TypeParams),
+ map.from_corresponding_lists(TypeParams, Args, TSubst),
+
+ % Apply substitution to the declared supertype.
+ apply_variable_renaming_to_type(Renaming, SuperType0, SuperType1),
+ apply_rec_subst_to_type(TSubst, SuperType1, SuperType)
+ ).
+
+%-----------------------------------------------------------------------------%
+
classify_type(ModuleInfo, VarType) = TypeCategory :-
( if type_to_ctor(VarType, TypeCtor) then
TypeCategory = classify_type_ctor(ModuleInfo, TypeCtor)
diff --git a/compiler/typecheck.m b/compiler/typecheck.m
index a1ce39e67..97e5ea79d 100644
--- a/compiler/typecheck.m
+++ b/compiler/typecheck.m
@@ -3775,27 +3775,6 @@ replace_principal_type_ctor_with_base(TypeTable, TVarSet, Type0, Type) :-
Type = Type0
).
-:- pred get_supertype(type_table::in, tvarset::in, type_ctor::in,
- list(mer_type)::in, mer_type::out) is semidet.
-
-get_supertype(TypeTable, TVarSet, TypeCtor, Args, SuperType) :-
- hlds_data.search_type_ctor_defn(TypeTable, TypeCtor, TypeDefn),
- hlds_data.get_type_defn_body(TypeDefn, TypeBody),
- TypeBody = hlds_du_type(_, yes(SuperType0), _, _, _),
- require_det (
- % Create substitution from type parameters to Args.
- hlds_data.get_type_defn_tvarset(TypeDefn, TVarSet0),
- hlds_data.get_type_defn_tparams(TypeDefn, TypeParams0),
- tvarset_merge_renaming(TVarSet, TVarSet0, _NewTVarSet, Renaming),
- apply_variable_renaming_to_tvar_list(Renaming,
- TypeParams0, TypeParams),
- map.from_corresponding_lists(TypeParams, Args, TSubst),
-
- % Apply substitution to the declared supertype.
- apply_variable_renaming_to_type(Renaming, SuperType0, SuperType1),
- apply_rec_subst_to_type(TSubst, SuperType1, SuperType)
- ).
-
%---------------------%
:- type invariant_set == set(tvar).
@@ -3962,9 +3941,11 @@ check_coerce_type_param(TypeTable, TVarSet, InvariantSet,
% If Comparison is compare_equal_lt, then also succeed if TypeA =< TypeB
% by subtype definitions.
%
-:- pred compare_types(type_table::in, tvarset::in,
- types_comparison::in, mer_type::in, mer_type::in,
- type_assign::in, type_assign::out) is semidet.
+ % Note: changes here may need to be made to compare_types in
+ % modecheck_coerce.m
+ %
+:- pred compare_types(type_table::in, tvarset::in, types_comparison::in,
+ mer_type::in, mer_type::in, type_assign::in, type_assign::out) is semidet.
compare_types(TypeTable, TVarSet, Comparison, TypeA, TypeB,
!TypeAssign) :-
diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
index 9070e119f..9dc21f4f6 100644
--- a/doc/reference_manual.texi
+++ b/doc/reference_manual.texi
@@ -7147,7 +7147,7 @@ if @var{Ti} is a subtype of @var{Si},
according to visible subtype definitions
@end itemize
-Otherwise, the coerce expression is not type-correct.
+Otherwise, the @code{coerce} expression is not type-correct.
@c NOTE: we deliberately disallow coercion between arbitrary phantom types.
Furthermore,
@@ -7176,63 +7176,87 @@ other than a recursive type of the exact form @samp{base(B1, ..., Bn)}
@heading Mode checking
Type conversion expressions must also be mode-correct.
-For an expression where:
+Intuitively, conversion from a subtype to supertype is safe,
+but a conversion from a supertype to subtype is safe only if
+the inst approximating the input term
+indicates that the result would also be valid in the subtype.
- at itemize @bullet
+Mode checking proceeds by simultaneously traversing
+the inst tree of the input term,
+the type tree of the input term,
+and the type tree of the result term,
+and producing the inst tree of the result term
+if the conversion is valid.
+Let
+ at itemize
@item
-the input has type @samp{s},
-initial inst @var{InitialX},
-and final inst @var{FinalX}
-
+ at var{InstX} be the current node in the input inst tree,
+ at item
+ at var{InstY} be the current node in the result inst tree,
+ at item
+ at var{TypeX} be the current node in the input type tree,
@item
-the result has type @samp{t},
-initial inst @var{InitialY},
-and final inst @var{FinalY}
+ at var{TypeY} be the current node in the result type tree,
+ at item
+ at var{TypeCtorX} be the principal type constructor of @var{TypeX},
+ at item
+ at var{TypeCtorY} be the principal type constructor of @var{TypeY}.
@end itemize
- at noindent
-the type conversion expression is mode-correct iff:
+In the following, @var{X} < @var{Y} means
+ at var{X} is a subtype of @var{Y}
+by visible subtype definitions.
+
+For each node @var{InstX}:
+ at itemize
+ at item
+If @var{InstX} is a recursive node in the inst tree
+(i.e. it is its own ancestor),
+then we require @var{TypeX} =< @var{TypeY}.
+Let @var{InstY} = @var{InstX}.
- at itemize @bullet
@item
- at var{InitialX} is a ground inst
+Otherwise, if @var{InstX} is a @code{bound} node,
+then each of the function symbols listed in the @code{bound} inst
+must name a constructor in @var{TypeCtorY}.
+Let @var{InstY} be a @code{bound} inst containing the same
+function symbols;
+the insts for the arguments of each function symbol
+are then checked and constructed recursively.
@item
- at var{InitialY} is free
+Otherwise, if @var{InstX} is a @code{ground} node
+and @var{TypeX} = @var{TypeY},
+then @var{InstY} = @var{InstX}.
+ at c This includes higher-order types.
@item
- at var{FinalX} is @var{InitialX}
+Otherwise, if @var{InstX} is a @code{ground} node
+and @var{TypeX} < @var{TypeY}, then
+let @var{InstY} be the @code{bound} node constructed
+using the process below.
@item
- at var{FinalY} is
-the abstract unification of
- at var{InitialX} and the
- at code{bound} instantiatedness tree derived from @samp{t},
-and @var{FinalY} does not approximate any term
-that is invalid in @samp{t}.
+Otherwise,
+the @code{coerce} expression is not mode-correct.
@end itemize
-The @code{bound} instantiatedness tree for @samp{t}
-is derived by producing a @code{bound} node
-containing each possible constructor of @samp{t},
-where the arguments of each bound functor
-are also @code{bound} instantiatedness trees.
-Where a constructor argument type is not a discriminated union or tuple type,
-or if the argument is a recursive node in the type tree,
-the inst of the argument is replaced with @code{ground}.
-
-The abstract unification of two instantiation states
-is the abstract equivalent of the unification on terms.
-It is defined in
- at cite{Precise and Expressive Mode Systems for Typed Logic Programming
-Languages} by David Overton. @xref{[6]}.
-
-Intuitively,
-coercing a ground term from a subtype to a supertype is safe,
-but coercing a term from a supertype to a subtype
-is safe only if
-the inst of the term being coerced
-indicates that the term would also be valid in the subtype.
+To construct a @samp{bound} node @var{InstY}
+from a @samp{ground} node @var{InstX}:
+
+ at itemize
+ at item
+If @var{TypeX} = @var{TypeY}
+or if @var{TypeX} is a recursive node in the type tree
+(i.e. it is its own ancestor),
+then let @var{InstY} be @code{ground}.
+
+ at item
+Otherwise, let @var{InstY} be a @code{bound} inst
+containing all of the constructors in @var{TypeCtorX};
+the insts for the arguments of each function symbol
+are constructed recursively.
+ at end itemize
@heading Examples
@@ -12440,8 +12464,6 @@ typedef struct @{
* [4]:: Sagonas, @cite{The SLG-WAM: A Search-Efficient Engine
for Well-Founded Evaluation of Normal Logic Programs}.
* [5]:: Demoen and Sagonas, @cite{CAT: the copying approach to tabling}.
-* [6]:: Overton, @cite{Precise and Expressive Mode Systems for
- Typed Logic Programming Languages}.
@end menu
@node [1]
@@ -12481,11 +12503,4 @@ In C. Palamidessi, H. Glaser and K. Meinke, editors, @cite{Principles of
Declarative Programming, 10th International Symposium, PLILP'98},
Lecture Notes in Computer Science, Springer, 1998.
Available form @uref{http://user.it.uu.se/~kostis/Papers/cat.ps.gz}.
-
- at node [6]
- at unnumberedsec [6]
-David Overton, @cite{Precise and Expressive Mode Systems for
-Typed Logic Programming Languages},
-PhD thesis, The University of Melbourne, 2003. Available from
- at uref{http://mercurylang.org/documentation/papers/dmo-thesis.ps.gz}
@bye
diff --git a/tests/invalid/Mmakefile b/tests/invalid/Mmakefile
index 71e1e898d..59a44c1a7 100644
--- a/tests/invalid/Mmakefile
+++ b/tests/invalid/Mmakefile
@@ -122,8 +122,11 @@ SINGLEMODULE= \
coerce_implied_mode \
coerce_infer \
coerce_instvar \
+ coerce_int \
coerce_mode_error \
coerce_non_du \
+ coerce_recursive_inst \
+ coerce_recursive_type \
coerce_syntax \
coerce_type_error \
coerce_unify_tvars \
diff --git a/tests/invalid/coerce_instvar.err_exp b/tests/invalid/coerce_instvar.err_exp
index 3de661e6c..292f9a29d 100644
--- a/tests/invalid/coerce_instvar.err_exp
+++ b/tests/invalid/coerce_instvar.err_exp
@@ -1,19 +1,7 @@
coerce_instvar.m:043: In clause for `bad(in((I =< ground)), out((I =<
coerce_instvar.m:043: ground)))':
coerce_instvar.m:043: in coerce:
-coerce_instvar.m:043: mode error: the result would have instantiatedness
-coerce_instvar.m:043: ( I =< bound(
-coerce_instvar.m:043: apple
-coerce_instvar.m:043: ;
-coerce_instvar.m:043: lemon(
-coerce_instvar.m:043: bound(
-coerce_instvar.m:043: bar
-coerce_instvar.m:043: ;
-coerce_instvar.m:043: foo
-coerce_instvar.m:043: )
-coerce_instvar.m:043: )
-coerce_instvar.m:043: ;
-coerce_instvar.m:043: orange
-coerce_instvar.m:043: ) ),
-coerce_instvar.m:043: which is not valid for the type
+coerce_instvar.m:043: mode error: the input term has instantiatedness
+coerce_instvar.m:043: `( I =< ground )',
+coerce_instvar.m:043: and cannot be converted to the type
coerce_instvar.m:043: `coerce_instvar.citrus'.
diff --git a/tests/invalid/coerce_int.err_exp b/tests/invalid/coerce_int.err_exp
new file mode 100644
index 000000000..197c8bc8d
--- /dev/null
+++ b/tests/invalid/coerce_int.err_exp
@@ -0,0 +1,46 @@
+coerce_int.m:026: In clause for `bad(in(coerce_int.wrap(bound(1 ; 2)))) =
+coerce_int.m:026: out(coerce_int.wrap(bound(1 ; 3)))':
+coerce_int.m:026: mode error: argument 2 had the wrong instantiatedness.
+coerce_int.m:026: Final instantiatedness of `HeadVar__2' was
+coerce_int.m:026: `bound(wrap(bound(1 ; 2)))',
+coerce_int.m:026: expected final instantiatedness was
+coerce_int.m:026: named inst wrap(
+coerce_int.m:026: bound(
+coerce_int.m:026: 1
+coerce_int.m:026: ;
+coerce_int.m:026: 3
+coerce_int.m:026: )
+coerce_int.m:026: ),
+coerce_int.m:026: which expands to
+coerce_int.m:026: bound(
+coerce_int.m:026: wrap(
+coerce_int.m:026: bound(
+coerce_int.m:026: 1
+coerce_int.m:026: ;
+coerce_int.m:026: 3
+coerce_int.m:026: )
+coerce_int.m:026: )
+coerce_int.m:026: ).
+coerce_int.m:032: In clause for `bad_wrong_type(in(coerce_int.wrap(bound(1 ;
+coerce_int.m:032: 2)))) = out(coerce_int.wrap(bound(1 ; 2)))':
+coerce_int.m:032: in coerce:
+coerce_int.m:032: mode error: the input term has instantiatedness
+coerce_int.m:032: named inst wrap(
+coerce_int.m:032: bound(
+coerce_int.m:032: 1
+coerce_int.m:032: ;
+coerce_int.m:032: 2
+coerce_int.m:032: )
+coerce_int.m:032: ),
+coerce_int.m:032: which expands to
+coerce_int.m:032: bound(
+coerce_int.m:032: wrap(
+coerce_int.m:032: bound(
+coerce_int.m:032: 1
+coerce_int.m:032: ;
+coerce_int.m:032: 2
+coerce_int.m:032: )
+coerce_int.m:032: )
+coerce_int.m:032: ),
+coerce_int.m:032: and cannot be converted to the type
+coerce_int.m:032: `coerce_int.wrap(uint)'.
diff --git a/tests/invalid/coerce_int.m b/tests/invalid/coerce_int.m
new file mode 100644
index 000000000..b92105ec4
--- /dev/null
+++ b/tests/invalid/coerce_int.m
@@ -0,0 +1,32 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module coerce_int.
+:- interface.
+
+:- type wrap(T)
+ ---> wrap(T).
+
+:- inst wrap(I)
+ ---> wrap(I).
+
+:- implementation.
+
+:- func ok(wrap(int)) = wrap(int).
+:- mode ok(in(wrap(bound(1 ; 2 ; 3)))) = out(wrap(bound(3 ; 1 ; 2)))
+ is det.
+
+ok(X) = coerce(X).
+
+:- func bad(wrap(int)) = wrap(int).
+:- mode bad(in(wrap(bound(1 ; 2)))) = out(wrap(bound(1 ; 3)))
+ is det.
+
+bad(X) = coerce(X).
+
+:- func bad_wrong_type(wrap(uint)) = wrap(uint).
+:- mode bad_wrong_type(in(wrap(bound(1 ; 2)))) = out(wrap(bound(1 ; 2)))
+ is det.
+
+bad_wrong_type(X) = coerce(X).
diff --git a/tests/invalid/coerce_mode_error.err_exp b/tests/invalid/coerce_mode_error.err_exp
index 8105fbbe1..0899016bb 100644
--- a/tests/invalid/coerce_mode_error.err_exp
+++ b/tests/invalid/coerce_mode_error.err_exp
@@ -4,37 +4,25 @@ coerce_mode_error.m:035: mode error: `X' has instantiatedness `free',
coerce_mode_error.m:035: but it must be ground.
coerce_mode_error.m:046: In clause for `bad_fruit_to_citrus(in, out)':
coerce_mode_error.m:046: in coerce:
-coerce_mode_error.m:046: mode error: the result would have instantiatedness
-coerce_mode_error.m:046: `bound(apple ; lemon ; orange)',
-coerce_mode_error.m:046: which is not valid for the type
+coerce_mode_error.m:046: mode error: the input term has instantiatedness
+coerce_mode_error.m:046: `ground',
+coerce_mode_error.m:046: and cannot be converted to the type
coerce_mode_error.m:046: `coerce_mode_error.citrus'.
coerce_mode_error.m:052: In clause for `bad_nelist_f_to_list_c(in, out)':
coerce_mode_error.m:052: in coerce:
-coerce_mode_error.m:052: mode error: the result would have instantiatedness
-coerce_mode_error.m:052: bound(
-coerce_mode_error.m:052: '[|]'(
-coerce_mode_error.m:052: bound(
-coerce_mode_error.m:052: apple
-coerce_mode_error.m:052: ;
-coerce_mode_error.m:052: lemon
-coerce_mode_error.m:052: ;
-coerce_mode_error.m:052: orange
-coerce_mode_error.m:052: ),
-coerce_mode_error.m:052: bound(
-coerce_mode_error.m:052: []
-coerce_mode_error.m:052: ;
-coerce_mode_error.m:052: '[|]'(
-coerce_mode_error.m:052: bound(
-coerce_mode_error.m:052: apple
-coerce_mode_error.m:052: ;
-coerce_mode_error.m:052: lemon
-coerce_mode_error.m:052: ;
-coerce_mode_error.m:052: orange
-coerce_mode_error.m:052: ),
-coerce_mode_error.m:052: ground
-coerce_mode_error.m:052: )
-coerce_mode_error.m:052: )
-coerce_mode_error.m:052: )
-coerce_mode_error.m:052: ),
-coerce_mode_error.m:052: which is not valid for the type
+coerce_mode_error.m:052: mode error: the input term has instantiatedness
+coerce_mode_error.m:052: `ground',
+coerce_mode_error.m:052: and cannot be converted to the type
coerce_mode_error.m:052: `coerce_mode_error.list(coerce_mode_error.citrus)'.
+coerce_mode_error.m:064: In clause for `bad_from_list_to_least2(in, out)':
+coerce_mode_error.m:064: in coerce:
+coerce_mode_error.m:064: mode error: the input term has instantiatedness
+coerce_mode_error.m:064: `bound('[|]'(ground, ground))',
+coerce_mode_error.m:064: and cannot be converted to the type
+coerce_mode_error.m:064: `coerce_mode_error.least2(V_1)'.
+coerce_mode_error.m:073: In clause for `from_list_to_least2(in, out)':
+coerce_mode_error.m:073: in coerce:
+coerce_mode_error.m:073: mode error: the input term has instantiatedness
+coerce_mode_error.m:073: `bound('[|]'(ground, ground))',
+coerce_mode_error.m:073: and cannot be converted to the type
+coerce_mode_error.m:073: `coerce_mode_error.least2(V_1)'.
diff --git a/tests/invalid/coerce_mode_error.m b/tests/invalid/coerce_mode_error.m
index 37e4fa2d4..93a6138d0 100644
--- a/tests/invalid/coerce_mode_error.m
+++ b/tests/invalid/coerce_mode_error.m
@@ -52,3 +52,24 @@ bad_nelist_f_to_list_c(X, Y) :-
Y = coerce(X).
%---------------------------------------------------------------------------%
+
+:- type least2(T) =< list(T)
+ ---> [T | non_empty_list(T)].
+
+:- pred bad_from_list_to_least2(list(T), least2(T)).
+:- mode bad_from_list_to_least2(in, out) is semidet.
+
+bad_from_list_to_least2(List, Xs) :-
+ List = [_ | _],
+ Xs = coerce(List).
+
+:- pred from_list_to_least2(list(T), least2(T)).
+:- mode from_list_to_least2(in, out) is semidet.
+
+from_list_to_least2(List, Xs) :-
+ % Unfortunately the mode checker does not assign a precise enough inst
+ % to List for the coerce expression to be accepted.
+ List = [_, _ | _],
+ Xs = coerce(List).
+
+%---------------------------------------------------------------------------%
diff --git a/tests/invalid/coerce_recursive_inst.err_exp b/tests/invalid/coerce_recursive_inst.err_exp
new file mode 100644
index 000000000..7b279c40b
--- /dev/null
+++ b/tests/invalid/coerce_recursive_inst.err_exp
@@ -0,0 +1,47 @@
+coerce_recursive_inst.m:042: In clause for
+coerce_recursive_inst.m:042: `bad1(in((coerce_recursive_inst.cons))) =
+coerce_recursive_inst.m:042: out((coerce_recursive_inst.cons))':
+coerce_recursive_inst.m:042: in coerce:
+coerce_recursive_inst.m:042: mode error: the input term has instantiatedness
+coerce_recursive_inst.m:042: named inst cons,
+coerce_recursive_inst.m:042: which expands to
+coerce_recursive_inst.m:042: bound(
+coerce_recursive_inst.m:042: cons(
+coerce_recursive_inst.m:042: ground,
+coerce_recursive_inst.m:042: named inst rec,
+coerce_recursive_inst.m:042: which expands to
+coerce_recursive_inst.m:042: bound(
+coerce_recursive_inst.m:042: cons(
+coerce_recursive_inst.m:042: ground,
+coerce_recursive_inst.m:042: named inst rec
+coerce_recursive_inst.m:042: )
+coerce_recursive_inst.m:042: ;
+coerce_recursive_inst.m:042: nil
+coerce_recursive_inst.m:042: )
+coerce_recursive_inst.m:042: )
+coerce_recursive_inst.m:042: ),
+coerce_recursive_inst.m:042: and cannot be converted to the type
+coerce_recursive_inst.m:042: `coerce_recursive_inst.rec(coerce_recursive_inst.citrus)'.
+coerce_recursive_inst.m:048: In clause for
+coerce_recursive_inst.m:048: `bad2(in((coerce_recursive_inst.cons))) = out':
+coerce_recursive_inst.m:048: in coerce:
+coerce_recursive_inst.m:048: mode error: the input term has instantiatedness
+coerce_recursive_inst.m:048: named inst cons,
+coerce_recursive_inst.m:048: which expands to
+coerce_recursive_inst.m:048: bound(
+coerce_recursive_inst.m:048: cons(
+coerce_recursive_inst.m:048: ground,
+coerce_recursive_inst.m:048: named inst rec,
+coerce_recursive_inst.m:048: which expands to
+coerce_recursive_inst.m:048: bound(
+coerce_recursive_inst.m:048: cons(
+coerce_recursive_inst.m:048: ground,
+coerce_recursive_inst.m:048: named inst rec
+coerce_recursive_inst.m:048: )
+coerce_recursive_inst.m:048: ;
+coerce_recursive_inst.m:048: nil
+coerce_recursive_inst.m:048: )
+coerce_recursive_inst.m:048: )
+coerce_recursive_inst.m:048: ),
+coerce_recursive_inst.m:048: and cannot be converted to the type
+coerce_recursive_inst.m:048: `coerce_recursive_inst.rec(coerce_recursive_inst.citrus)'.
diff --git a/tests/invalid/coerce_recursive_inst.m b/tests/invalid/coerce_recursive_inst.m
new file mode 100644
index 000000000..4f89ce083
--- /dev/null
+++ b/tests/invalid/coerce_recursive_inst.m
@@ -0,0 +1,50 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module coerce_recursive_inst.
+:- interface.
+
+:- type rec(T)
+ ---> nil
+ ; cons(T, rec(T)).
+
+:- inst rec for rec/1
+ ---> nil
+ ; cons(ground, rec).
+
+:- inst cons for rec/1
+ ---> cons(ground, rec).
+
+:- type fruit
+ ---> apple
+ ; orange
+ ; lemon.
+
+:- type citrus =< fruit
+ ---> orange
+ ; lemon.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+ % convert subtype to supertype
+:- func good(rec(citrus)) = rec(fruit).
+:- mode good(in(cons)) = out(cons) is det.
+
+good(X) = coerce(X).
+
+ % cannot convert supertype to subtype
+:- func bad1(rec(fruit)) = rec(citrus).
+:- mode bad1(in(cons)) = out(cons) is det.
+
+bad1(X) = coerce(X).
+
+ % cannot convert supertype to subtype
+:- func bad2(rec(fruit)) = rec(citrus).
+:- mode bad2(in(cons)) = out is det.
+
+bad2(X) = coerce(X).
+
+%---------------------------------------------------------------------------%
diff --git a/tests/invalid/coerce_recursive_type.err_exp b/tests/invalid/coerce_recursive_type.err_exp
new file mode 100644
index 000000000..7cb64f357
--- /dev/null
+++ b/tests/invalid/coerce_recursive_type.err_exp
@@ -0,0 +1,72 @@
+coerce_recursive_type.m:045: In clause for `bad(in) = out':
+coerce_recursive_type.m:045: in coerce:
+coerce_recursive_type.m:045: mode error: the input term has instantiatedness
+coerce_recursive_type.m:045: `ground',
+coerce_recursive_type.m:045: and cannot be converted to the type
+coerce_recursive_type.m:045: `coerce_recursive_type.rec(coerce_recursive_type.citrus)'.
+coerce_recursive_type.m:051: In clause for
+coerce_recursive_type.m:051: `bad2(in((coerce_recursive_type.cons_apple3))) =
+coerce_recursive_type.m:051: out':
+coerce_recursive_type.m:051: in coerce:
+coerce_recursive_type.m:051: mode error: the input term has instantiatedness
+coerce_recursive_type.m:051: named inst cons_apple3,
+coerce_recursive_type.m:051: which expands to
+coerce_recursive_type.m:051: bound(
+coerce_recursive_type.m:051: cons(
+coerce_recursive_type.m:051: ground,
+coerce_recursive_type.m:051: named inst cons_apple2,
+coerce_recursive_type.m:051: which expands to
+coerce_recursive_type.m:051: bound(
+coerce_recursive_type.m:051: cons(
+coerce_recursive_type.m:051: ground,
+coerce_recursive_type.m:051: named inst cons_apple,
+coerce_recursive_type.m:051: which expands to
+coerce_recursive_type.m:051: bound(
+coerce_recursive_type.m:051: cons(
+coerce_recursive_type.m:051: named inst apple,
+coerce_recursive_type.m:051: which expands to
+coerce_recursive_type.m:051: bound(
+coerce_recursive_type.m:051: apple
+coerce_recursive_type.m:051: ),
+coerce_recursive_type.m:051: ground
+coerce_recursive_type.m:051: )
+coerce_recursive_type.m:051: )
+coerce_recursive_type.m:051: )
+coerce_recursive_type.m:051: )
+coerce_recursive_type.m:051: )
+coerce_recursive_type.m:051: ),
+coerce_recursive_type.m:051: and cannot be converted to the type
+coerce_recursive_type.m:051: `coerce_recursive_type.rec(coerce_recursive_type.citrus)'.
+coerce_recursive_type.m:058: In clause for
+coerce_recursive_type.m:058: `bad3(in((coerce_recursive_type.cons_apple3))) =
+coerce_recursive_type.m:058: out':
+coerce_recursive_type.m:058: in coerce:
+coerce_recursive_type.m:058: mode error: the input term has instantiatedness
+coerce_recursive_type.m:058: named inst cons_apple3,
+coerce_recursive_type.m:058: which expands to
+coerce_recursive_type.m:058: bound(
+coerce_recursive_type.m:058: cons(
+coerce_recursive_type.m:058: ground,
+coerce_recursive_type.m:058: named inst cons_apple2,
+coerce_recursive_type.m:058: which expands to
+coerce_recursive_type.m:058: bound(
+coerce_recursive_type.m:058: cons(
+coerce_recursive_type.m:058: ground,
+coerce_recursive_type.m:058: named inst cons_apple,
+coerce_recursive_type.m:058: which expands to
+coerce_recursive_type.m:058: bound(
+coerce_recursive_type.m:058: cons(
+coerce_recursive_type.m:058: named inst apple,
+coerce_recursive_type.m:058: which expands to
+coerce_recursive_type.m:058: bound(
+coerce_recursive_type.m:058: apple
+coerce_recursive_type.m:058: ),
+coerce_recursive_type.m:058: ground
+coerce_recursive_type.m:058: )
+coerce_recursive_type.m:058: )
+coerce_recursive_type.m:058: )
+coerce_recursive_type.m:058: )
+coerce_recursive_type.m:058: )
+coerce_recursive_type.m:058: ),
+coerce_recursive_type.m:058: and cannot be converted to the type
+coerce_recursive_type.m:058: `coerce_recursive_type.rec(coerce_recursive_type.fruit)'.
diff --git a/tests/invalid/coerce_recursive_type.m b/tests/invalid/coerce_recursive_type.m
new file mode 100644
index 000000000..38467fa90
--- /dev/null
+++ b/tests/invalid/coerce_recursive_type.m
@@ -0,0 +1,58 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module coerce_recursive_type.
+:- interface.
+
+:- type rec(T)
+ ---> nil
+ ; cons(T, rec(T)).
+
+:- type fruit
+ ---> apple
+ ; orange
+ ; lemon.
+
+:- type citrus =< fruit
+ ---> orange
+ ; lemon.
+
+:- inst apple
+ ---> apple.
+
+:- inst cons_apple for rec/1
+ ---> cons(apple, ground).
+
+:- inst cons_apple2 for rec/1
+ ---> cons(ground, cons_apple).
+
+:- inst cons_apple3 for rec/1
+ ---> cons(ground, cons_apple2).
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+ % convert subtype to supertype
+:- func good(rec(citrus)) = rec(fruit).
+
+good(X) = coerce(X).
+
+ % cannot convert supertype to subtype
+:- func bad(rec(fruit)) = rec(citrus).
+
+bad(X) = coerce(X).
+
+ % cannot convert supertype to subtype
+:- func bad2(rec(fruit)) = rec(citrus).
+:- mode bad2(in(cons_apple3)) = out is det.
+
+bad2(X) = coerce(X).
+
+ % convert subtype to supertype
+ % But, the bound inst is wrong for the input type.
+:- func bad3(rec(citrus)) = rec(fruit).
+:- mode bad3(in(cons_apple3)) = out is det.
+
+bad3(X) = coerce(X).
diff --git a/tests/invalid/coerce_uniq.err_exp b/tests/invalid/coerce_uniq.err_exp
index 897ddb2bd..1c168628d 100644
--- a/tests/invalid/coerce_uniq.err_exp
+++ b/tests/invalid/coerce_uniq.err_exp
@@ -1,6 +1,5 @@
coerce_uniq.m:024: In clause for `coerce_ui(ui, out)':
coerce_uniq.m:024: mode error: argument 1 did not get sufficiently
coerce_uniq.m:024: instantiated.
-coerce_uniq.m:024: Final instantiatedness of `X' was
-coerce_uniq.m:024: `bound(apple ; lemon ; orange)',
+coerce_uniq.m:024: Final instantiatedness of `X' was `ground',
coerce_uniq.m:024: expected final instantiatedness was `unique'.
diff --git a/tests/invalid/coerce_unreachable.err_exp b/tests/invalid/coerce_unreachable.err_exp
index 55c0cac24..559537314 100644
--- a/tests/invalid/coerce_unreachable.err_exp
+++ b/tests/invalid/coerce_unreachable.err_exp
@@ -1,7 +1,7 @@
coerce_unreachable.m:027: In clause for `p1(in, out)':
coerce_unreachable.m:027: in coerce:
-coerce_unreachable.m:027: mode error: the result would have instantiatedness
-coerce_unreachable.m:027: `bound(apple ; lemon ; orange)',
-coerce_unreachable.m:027: which is not valid for the type
+coerce_unreachable.m:027: mode error: the input term has instantiatedness
+coerce_unreachable.m:027: `ground',
+coerce_unreachable.m:027: and cannot be converted to the type
coerce_unreachable.m:027: `coerce_unreachable.citrus'.
For more information, recompile with `-E'.
--
2.30.0
More information about the reviews
mailing list