[m-rev.] for review: Parse and check coerce expressions.
Peter Wang
novalazy at gmail.com
Wed Mar 10 14:40:33 AEDT 2021
This change implements parsing, typechecking, and modechecking of
"coerce" expressions from my subtypes proposal, i.e. coerce(Term).
Backends currently will abort if asked to generate code for coercions,
as subtypes do not yet share data representations with their base types,
so most coercions would lead to crashes at runtime anyway.
----------------
compiler/hlds_goal.m:
Add new type of generic_call to represent coerce expressions.
compiler/hlds_pred.m:
Add new generic_call_id for coerce expressions.
compiler/superhomogeneous.m:
Treat var-functor unifications of the form "Var = coerce(Term)"
as special, producing coerce generic_calls.
----------------
compiler/type_assign.m:
Add a field to type_assign to hold coerce constraints to be checked,
or known to be unsatisfiable, in the given type assignment.
compiler/typecheck.m:
compiler/typecheck_errors.m:
Implement typechecking of coerce expressions.
compiler/prog_type.m:
Add a predicate type_is_ground_except_vars.
----------------
compiler/check_hlds.m:
Add new module modecheck_coerce.
compiler/modecheck_coerce.m:
Implement modechecking of coerce expressions.
compiler/modecheck_goal.m:
Call modecheck_coerce at a coerce generic call.
compiler/mode_errors.m:
Add two mode errors relating to coerce expressions.
----------------
compiler/arg_info.m:
compiler/build_mode_constraints.m:
compiler/bytecode_gen.m:
compiler/call_gen.m:
compiler/coverage_profiling.m:
compiler/deep_profiling.m:
compiler/exception_analysis.m:
compiler/float_regs.m:
compiler/follow_vars.m:
compiler/goal_util.m:
compiler/higher_order.m:
compiler/hlds_desc.m:
compiler/hlds_out_goal.m:
compiler/hlds_out_util.m:
compiler/intermod.m:
compiler/interval.m:
compiler/lambda.m:
compiler/live_vars.m:
compiler/ml_call_gen.m:
compiler/ml_code_gen.m:
compiler/mode_constraints.m:
compiler/old_type_constraints.m:
compiler/post_typecheck.m:
compiler/pre_quantification.m:
compiler/tabling_analysis.m:
compiler/term_traversal.m:
compiler/trailing_analysis.m:
compiler/tupling.m:
compiler/unique_modes.m:
compiler/unused_imports.m:
compiler/purity.m:
compiler/simplify_goal.m:
compiler/simplify_goal_call.m:
compiler/structure_reuse.direct.detect_garbage.m:
compiler/structure_reuse.indirect.m:
compiler/structure_sharing.analysis.m:
Conform to changes.
compiler/prog_rep.m:
Conform to changes. Reuse cast_rep for coercions for now.
compiler/hlds_statistics.m:
Count coercions in proc stats.
----------------
tests/invalid/Mercury.options:
tests/invalid/Mmakefile:
tests/invalid/coerce_ambig.err_exp:
tests/invalid/coerce_ambig.m:
tests/invalid/coerce_disambig.err_exp:
tests/invalid/coerce_disambig.m:
tests/invalid/coerce_implied_mode.err_exp:
tests/invalid/coerce_implied_mode.m:
tests/invalid/coerce_infer.err_exp:
tests/invalid/coerce_infer.m:
tests/invalid/coerce_instvar.err_exp:
tests/invalid/coerce_instvar.m:
tests/invalid/coerce_mode_error.err_exp:
tests/invalid/coerce_mode_error.m:
tests/invalid/coerce_non_du.err_exp:
tests/invalid/coerce_non_du.m:
tests/invalid/coerce_syntax.err_exp:
tests/invalid/coerce_syntax.m:
tests/invalid/coerce_type_error.err_exp:
tests/invalid/coerce_type_error.m:
tests/invalid/coerce_uniq.err_exp:
tests/invalid/coerce_uniq.m:
tests/invalid/coerce_unreachable.err_exp:
tests/invalid/coerce_unreachable.m:
Add test cases.
tests/typeclasses/arbitrary_constraint_class.m:
tests/typeclasses/arbitrary_constraint_pred_1.m:
tests/typeclasses/arbitrary_constraint_pred_2.m:
Wrap parentheses around calls to a coerce/1 method
to prevent them being treated as coerce expressions.
----------------
doc/reference_manual.texi:
Rewrite chapter on Type conversions (still commented out).
In particular, the typechecking rules that I had written
previously were insufficient.
NEWS:
Mention backwards incompatibility.
---
NEWS | 5 +
compiler/arg_info.m | 1 +
compiler/build_mode_constraints.m | 3 +
compiler/bytecode_gen.m | 1 +
compiler/call_gen.m | 10 +
compiler/check_hlds.m | 5 +-
compiler/coverage_profiling.m | 2 +
compiler/deep_profiling.m | 4 +
compiler/exception_analysis.m | 2 +
compiler/float_regs.m | 1 +
compiler/follow_vars.m | 4 +-
compiler/goal_util.m | 1 +
compiler/higher_order.m | 1 +
compiler/hlds_desc.m | 3 +
compiler/hlds_goal.m | 11 +-
compiler/hlds_out_goal.m | 9 +-
compiler/hlds_out_util.m | 9 +
compiler/hlds_pred.m | 3 +-
compiler/hlds_statistics.m | 12 +-
compiler/intermod.m | 4 +
compiler/interval.m | 5 +
compiler/lambda.m | 2 +
compiler/live_vars.m | 4 +-
compiler/ml_call_gen.m | 4 +
compiler/ml_code_gen.m | 8 +-
compiler/mode_constraints.m | 3 +
compiler/mode_errors.m | 52 ++
compiler/modecheck_coerce.m | 496 ++++++++++++++++
compiler/modecheck_goal.m | 11 +-
compiler/old_type_constraints.m | 3 +
compiler/post_typecheck.m | 5 +-
compiler/pre_quantification.m | 2 +
compiler/prog_rep.m | 8 +
compiler/prog_type.m | 12 +
compiler/purity.m | 1 +
compiler/simplify_goal.m | 3 +
compiler/simplify_goal_call.m | 1 +
.../structure_reuse.direct.detect_garbage.m | 1 +
compiler/structure_reuse.indirect.m | 1 +
compiler/structure_sharing.analysis.m | 1 +
compiler/superhomogeneous.m | 30 +-
compiler/tabling_analysis.m | 6 +
compiler/term_traversal.m | 2 +
compiler/trailing_analysis.m | 4 +
compiler/tupling.m | 4 +-
compiler/type_assign.m | 36 +-
compiler/typecheck.m | 531 +++++++++++++++++-
compiler/typecheck_errors.m | 15 +
compiler/unique_modes.m | 3 +
compiler/unused_imports.m | 1 +
doc/reference_manual.texi | 248 +++++---
tests/invalid/Mercury.options | 2 +
tests/invalid/Mmakefile | 10 +
tests/invalid/coerce_ambig.err_exp | 12 +
tests/invalid/coerce_ambig.m | 45 ++
tests/invalid/coerce_disambig.err_exp | 6 +
tests/invalid/coerce_disambig.m | 38 ++
tests/invalid/coerce_implied_mode.err_exp | 7 +
tests/invalid/coerce_implied_mode.m | 38 ++
tests/invalid/coerce_infer.err_exp | 2 +
tests/invalid/coerce_infer.m | 26 +
tests/invalid/coerce_instvar.err_exp | 19 +
tests/invalid/coerce_instvar.m | 43 ++
tests/invalid/coerce_mode_error.err_exp | 40 ++
tests/invalid/coerce_mode_error.m | 54 ++
tests/invalid/coerce_non_du.err_exp | 11 +
tests/invalid/coerce_non_du.m | 31 +
tests/invalid/coerce_syntax.err_exp | 8 +
tests/invalid/coerce_syntax.m | 50 ++
tests/invalid/coerce_type_error.err_exp | 22 +
tests/invalid/coerce_type_error.m | 120 ++++
tests/invalid/coerce_uniq.err_exp | 12 +
tests/invalid/coerce_uniq.m | 36 ++
tests/invalid/coerce_unreachable.err_exp | 7 +
tests/invalid/coerce_unreachable.m | 41 ++
.../typeclasses/arbitrary_constraint_class.m | 2 +-
.../typeclasses/arbitrary_constraint_pred_1.m | 2 +-
.../typeclasses/arbitrary_constraint_pred_2.m | 2 +-
78 files changed, 2164 insertions(+), 116 deletions(-)
create mode 100644 compiler/modecheck_coerce.m
create mode 100644 tests/invalid/coerce_ambig.err_exp
create mode 100644 tests/invalid/coerce_ambig.m
create mode 100644 tests/invalid/coerce_disambig.err_exp
create mode 100644 tests/invalid/coerce_disambig.m
create mode 100644 tests/invalid/coerce_implied_mode.err_exp
create mode 100644 tests/invalid/coerce_implied_mode.m
create mode 100644 tests/invalid/coerce_infer.err_exp
create mode 100644 tests/invalid/coerce_infer.m
create mode 100644 tests/invalid/coerce_instvar.err_exp
create mode 100644 tests/invalid/coerce_instvar.m
create mode 100644 tests/invalid/coerce_mode_error.err_exp
create mode 100644 tests/invalid/coerce_mode_error.m
create mode 100644 tests/invalid/coerce_non_du.err_exp
create mode 100644 tests/invalid/coerce_non_du.m
create mode 100644 tests/invalid/coerce_syntax.err_exp
create mode 100644 tests/invalid/coerce_syntax.m
create mode 100644 tests/invalid/coerce_type_error.err_exp
create mode 100644 tests/invalid/coerce_type_error.m
create mode 100644 tests/invalid/coerce_uniq.err_exp
create mode 100644 tests/invalid/coerce_uniq.m
create mode 100644 tests/invalid/coerce_unreachable.err_exp
create mode 100644 tests/invalid/coerce_unreachable.m
diff --git a/NEWS b/NEWS
index bc556a8a8..f5919d859 100644
--- a/NEWS
+++ b/NEWS
@@ -17,6 +17,11 @@ Changes that may break compatibility
* We have reserved `=<`/2 as a type name.
+* A term with a top level functor `coerce/1` is now treated as a
+ type conversion expression. To call a function named `coerce/1`,
+ you can module qualify the name at the call site,
+ or wrap parentheses around the name, e.g. `(coerce)(Arg)`.
+
Changes to the Mercury standard library
---------------------------------------
diff --git a/compiler/arg_info.m b/compiler/arg_info.m
index 1dba916c2..314b0318d 100644
--- a/compiler/arg_info.m
+++ b/compiler/arg_info.m
@@ -363,6 +363,7 @@ generic_call_arg_reg_types(ModuleInfo, _VarTypes, GenericCall, ArgVars,
( GenericCall = class_method(_, _, _, _)
; GenericCall = event_call(_)
; GenericCall = cast(_)
+ ; GenericCall = coerce
),
list.duplicate(length(ArgVars), reg_r, ArgRegTypes)
).
diff --git a/compiler/build_mode_constraints.m b/compiler/build_mode_constraints.m
index 14a5884e2..62fde63d8 100644
--- a/compiler/build_mode_constraints.m
+++ b/compiler/build_mode_constraints.m
@@ -478,6 +478,9 @@ add_goal_expr_constraints(ModuleInfo, ProgVarset, PredId, GoalExpr,
;
% No mode constraints
Details = cast(_)
+ ;
+ Details = coerce,
+ sorry($pred, "coerce generic_call")
)
;
GoalExpr = switch(_, _, _),
diff --git a/compiler/bytecode_gen.m b/compiler/bytecode_gen.m
index 1fac40c6f..132e99c1e 100644
--- a/compiler/bytecode_gen.m
+++ b/compiler/bytecode_gen.m
@@ -224,6 +224,7 @@ gen_goal_expr(GoalExpr, GoalInfo, !ByteInfo, Code) :-
( GenericCallType = class_method(_, _, _, _)
; GenericCallType = cast(_)
; GenericCallType = event_call(_)
+ ; GenericCallType = coerce
),
% XXX
% string.append_list([
diff --git a/compiler/call_gen.m b/compiler/call_gen.m
index cf930af76..1e147431e 100644
--- a/compiler/call_gen.m
+++ b/compiler/call_gen.m
@@ -212,6 +212,10 @@ generate_generic_call(OuterCodeModel, GenericCall, Args, Modes,
else
unexpected($pred, "invalid type/inst cast call")
)
+ ;
+ GenericCall = coerce,
+ % XXX SUBTYPE
+ sorry($pred, "coerce")
).
:- pred generate_main_generic_call(code_model::in, generic_call::in,
@@ -442,6 +446,10 @@ generic_call_info(Globals, GenericCall, NumInputArgsR, NumInputArgsF,
SpecifierArgInfos = [],
FirstImmediateInputReg = 1,
HoCallVariant = ho_call_unknown % dummy; not used
+ ;
+ GenericCall = coerce,
+ % XXX SUBTYPE
+ sorry($pred, "coerce")
).
% Some of the values that generic call passes to the dispatch routine
@@ -509,6 +517,8 @@ generic_call_nonvar_setup(event_call(_), _, _, _, _, !CLD) :-
unexpected($pred, "event_call").
generic_call_nonvar_setup(cast(_), _, _, _, _, !CLD) :-
unexpected($pred, "cast").
+generic_call_nonvar_setup(coerce, _, _, _, _, !CLD) :-
+ unexpected($pred, "coerce").
%---------------------------------------------------------------------------%
diff --git a/compiler/check_hlds.m b/compiler/check_hlds.m
index 89522fa11..1defdb851 100644
--- a/compiler/check_hlds.m
+++ b/compiler/check_hlds.m
@@ -59,9 +59,10 @@
:- include_module mode_errors.
:- include_module mode_info.
:- include_module mode_util.
- :- include_module modecheck_goal.
- :- include_module modecheck_conj.
:- include_module modecheck_call.
+ :- include_module modecheck_coerce.
+ :- include_module modecheck_conj.
+ :- include_module modecheck_goal.
:- include_module modecheck_unify.
:- include_module modecheck_util.
:- include_module modes.
diff --git a/compiler/coverage_profiling.m b/compiler/coverage_profiling.m
index 71d78d94e..93a711ea9 100644
--- a/compiler/coverage_profiling.m
+++ b/compiler/coverage_profiling.m
@@ -250,6 +250,7 @@ coverage_prof_second_pass_goal(Goal0, Goal,
GathersCoverageAfter = yes
;
( GenericCall = cast(_)
+ ; GenericCall = coerce
; GenericCall = event_call(_)
),
GathersCoverageAfter = no
@@ -912,6 +913,7 @@ coverage_prof_first_pass(CPOptions, Goal0, Goal, PortCountsCoverageAfterBefore,
PortCountsCoverageAfterDirect = port_counts_give_coverage_after
;
( GenericCall = cast(_)
+ ; GenericCall = coerce
; GenericCall = event_call(_)
),
Trivial0 = goal_is_trivial,
diff --git a/compiler/deep_profiling.m b/compiler/deep_profiling.m
index 8dc00d84c..a98dc77b1 100644
--- a/compiler/deep_profiling.m
+++ b/compiler/deep_profiling.m
@@ -1067,6 +1067,7 @@ deep_prof_transform_goal(Goal0, Goal, AddedImpurity, !DeepInfo) :-
;
( GenericCall = event_call(_)
; GenericCall = cast(_)
+ ; GenericCall = coerce
),
Goal = Goal1,
AddedImpurity = no
@@ -1347,6 +1348,9 @@ deep_prof_wrap_call(Goal0, Goal, !DeepInfo) :-
;
Generic = cast(_),
unexpected($pred, "cast")
+ ;
+ Generic = coerce,
+ unexpected($pred, "coerce")
),
GoalCodeModel = goal_info_get_code_model(GoalInfo0),
module_info_get_globals(ModuleInfo, Globals),
diff --git a/compiler/exception_analysis.m b/compiler/exception_analysis.m
index db9d9755c..6a162be73 100644
--- a/compiler/exception_analysis.m
+++ b/compiler/exception_analysis.m
@@ -558,6 +558,8 @@ check_goal_for_exceptions_generic_call(VarTypes, Details, Args, GoalInfo,
Details = event_call(_)
;
Details = cast(_)
+ ;
+ Details = coerce
).
:- pred check_goals_for_exceptions(scc::in, vartypes::in,
diff --git a/compiler/float_regs.m b/compiler/float_regs.m
index e1d08fae3..9c2487e41 100644
--- a/compiler/float_regs.m
+++ b/compiler/float_regs.m
@@ -711,6 +711,7 @@ insert_reg_wrappers_goal_2(Goal0, Goal, !InstMap, !Info, !Specs) :-
;
( GenericCall = event_call(_)
; GenericCall = cast(_)
+ ; GenericCall = coerce
),
Goal = Goal0,
update_instmap(Goal, !InstMap)
diff --git a/compiler/follow_vars.m b/compiler/follow_vars.m
index d3c4dc920..62d8ffb6d 100644
--- a/compiler/follow_vars.m
+++ b/compiler/follow_vars.m
@@ -253,7 +253,9 @@ find_follow_vars_in_goal_expr(GoalExpr0, GoalExpr, !GoalInfo,
GoalExpr0 = generic_call(GenericCall, Args, Modes, MaybeArgRegs, Det),
GoalExpr = GoalExpr0,
(
- GenericCall = cast(_)
+ ( GenericCall = cast(_)
+ ; GenericCall = coerce
+ )
% Casts are generated inline.
;
( GenericCall = higher_order(_, _, _, _)
diff --git a/compiler/goal_util.m b/compiler/goal_util.m
index 3f54cc3d6..eef694245 100644
--- a/compiler/goal_util.m
+++ b/compiler/goal_util.m
@@ -714,6 +714,7 @@ generic_call_vars(higher_order(Var, _, _, _), [Var]).
generic_call_vars(class_method(Var, _, _, _), [Var]).
generic_call_vars(event_call(_), []).
generic_call_vars(cast(_), []).
+generic_call_vars(coerce, []).
%-----------------------------------------------------------------------------%
diff --git a/compiler/higher_order.m b/compiler/higher_order.m
index b613892d6..043826566 100644
--- a/compiler/higher_order.m
+++ b/compiler/higher_order.m
@@ -596,6 +596,7 @@ ho_traverse_goal(Goal0, Goal, !Info) :-
;
( GenericCall = event_call(_)
; GenericCall = cast(_)
+ ; GenericCall = coerce
),
Goal = Goal0
)
diff --git a/compiler/hlds_desc.m b/compiler/hlds_desc.m
index 1b856ebee..1871b1c4c 100644
--- a/compiler/hlds_desc.m
+++ b/compiler/hlds_desc.m
@@ -113,6 +113,9 @@ describe_goal(ModuleInfo, VarSet, Goal) = FullDesc :-
;
GCall = cast(_),
Desc = "cast " ++ describe_args(VarSet, Args)
+ ;
+ GCall = coerce,
+ Desc = "coerce " ++ describe_args(VarSet, Args)
)
;
GoalExpr = call_foreign_proc(_, PredId, _, Args, ExtraArgs, _, _),
diff --git a/compiler/hlds_goal.m b/compiler/hlds_goal.m
index b59e8773e..f98d79628 100644
--- a/compiler/hlds_goal.m
+++ b/compiler/hlds_goal.m
@@ -700,7 +700,11 @@
% A cast generic_call with two arguments, Input and Output,
% assigns `Input' to `Output', performing a cast of this kind.
cast_kind :: cast_kind
- ).
+ )
+
+ ; coerce.
+ % A coerce expression with two arguments, Input and Output,
+ % assigns `Input' to `Output'.
% The various kinds of casts that we can do.
%
@@ -1926,6 +1930,9 @@ generic_call_to_id(GenericCall, GenericCallId) :-
;
GenericCall = cast(CastType),
GenericCallId = gcid_cast(CastType)
+ ;
+ GenericCall = coerce,
+ GenericCallId = gcid_coerce
).
generic_call_pred_or_func(GenericCall) = PredOrFunc :-
@@ -1937,6 +1944,7 @@ generic_call_pred_or_func(GenericCall) = PredOrFunc :-
;
( GenericCall = event_call(_)
; GenericCall = cast(_)
+ ; GenericCall = coerce
),
PredOrFunc = pf_predicate
).
@@ -3264,6 +3272,7 @@ rename_generic_call(Must, Subn, Call0, Call) :-
;
( Call0 = event_call(_EventName)
; Call0 = cast(_CastKind)
+ ; Call0 = coerce
),
Call = Call0
).
diff --git a/compiler/hlds_out_goal.m b/compiler/hlds_out_goal.m
index 6a34534b1..d534fab6b 100644
--- a/compiler/hlds_out_goal.m
+++ b/compiler/hlds_out_goal.m
@@ -1508,8 +1508,13 @@ write_goal_generic_call(Info, Stream, _ModuleInfo, VarSet, _TypeQual,
mercury_output_term(VarSet, VarNamePrint, Term, Stream, !IO),
io.write_string(Stream, Follow, !IO)
;
- GenericCall = cast(CastType),
- CastTypeString = cast_type_to_string(CastType),
+ (
+ GenericCall = cast(CastType),
+ CastTypeString = cast_type_to_string(CastType)
+ ;
+ GenericCall = coerce,
+ CastTypeString = "coerce"
+ ),
( if string.contains_char(DumpOptions, 'l') then
write_indent(Stream, Indent, !IO),
io.write_strings(Stream, ["% ", CastTypeString, "\n"], !IO),
diff --git a/compiler/hlds_out_util.m b/compiler/hlds_out_util.m
index d960d81a9..28b6b3413 100644
--- a/compiler/hlds_out_util.m
+++ b/compiler/hlds_out_util.m
@@ -515,6 +515,8 @@ generic_call_id_to_string(gcid_event_call(EventName)) =
"event " ++ EventName.
generic_call_id_to_string(gcid_cast(CastType)) =
cast_type_to_string(CastType).
+generic_call_id_to_string(gcid_coerce) =
+ "coerce".
cast_type_to_string(unsafe_type_cast) = "unsafe_type_cast".
cast_type_to_string(unsafe_type_inst_cast) = "unsafe_type_inst_cast".
@@ -599,6 +601,13 @@ arg_number_to_string(CallId, ArgNum) = Str :-
; GenericCallId = gcid_cast(_)
),
Str = "argument " ++ int_to_string(ArgNum)
+ ;
+ GenericCallId = gcid_coerce,
+ ( if ArgNum = 2 then
+ Str = "the result"
+ else
+ Str = "the argument"
+ )
)
).
diff --git a/compiler/hlds_pred.m b/compiler/hlds_pred.m
index 5efbea581..99c2bebef 100644
--- a/compiler/hlds_pred.m
+++ b/compiler/hlds_pred.m
@@ -171,7 +171,8 @@
---> gcid_higher_order(purity, pred_or_func, arity)
; gcid_class_method(class_id, pf_sym_name_arity)
; gcid_event_call(string)
- ; gcid_cast(cast_kind).
+ ; gcid_cast(cast_kind)
+ ; gcid_coerce.
:- type pred_proc_list == list(pred_proc_id).
diff --git a/compiler/hlds_statistics.m b/compiler/hlds_statistics.m
index 9f84d4932..f7296ab29 100644
--- a/compiler/hlds_statistics.m
+++ b/compiler/hlds_statistics.m
@@ -183,6 +183,9 @@ accumulate_proc_stats_in_goal(Goal, !UsedVars, !Stats) :-
;
CallKind = cast(_),
!Stats ^ ps_casts := !.Stats ^ ps_casts + 1
+ ;
+ CallKind = coerce,
+ !Stats ^ ps_coerces := !.Stats ^ ps_coerces + 1
)
;
GoalExpr = conj(ConjType, Conjs),
@@ -299,6 +302,7 @@ accumulate_proc_stats_in_switch([Case | Cases], !UsedVars, !Stats) :-
ps_method_calls :: int,
ps_event_calls :: int,
ps_casts :: int,
+ ps_coerces :: int,
ps_plain_conjs :: int,
ps_plain_conjuncts :: int,
@@ -325,7 +329,7 @@ accumulate_proc_stats_in_switch([Case | Cases], !UsedVars, !Stats) :-
:- func init_proc_stats = proc_stats.
init_proc_stats = Stats :-
- Stats = proc_stats(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
+ Stats = proc_stats(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0).
:- pred write_proc_stat_components(io.output_stream::in, string::in,
@@ -336,7 +340,7 @@ write_proc_stat_components(OutStream, Msg, Name, PredId, ProcId, Stats, !IO) :-
Stats = proc_stats(UnifyConstructs, UnifyDeconstructs,
UnifyAssigns, UnifyTests, UnifyComplicateds,
PlainCalls, ForeignCalls, HOCalls, MethodCalls, EventCalls, Casts,
- PlainConjs, PlainConjuncts, ParallelConjs, ParallelConjuncts,
+ Coerces, PlainConjs, PlainConjuncts, ParallelConjs, ParallelConjuncts,
Disjs, Disjuncts, Switches, SwitchArms,
IfThenElses, Negations, Scopes, BiImplications, AtomicGoals, TryGoals),
@@ -344,7 +348,7 @@ write_proc_stat_components(OutStream, Msg, Name, PredId, ProcId, Stats, !IO) :-
UnifyConstructs + UnifyDeconstructs +
UnifyAssigns + UnifyTests + UnifyComplicateds +
PlainCalls + ForeignCalls +
- HOCalls + MethodCalls + EventCalls + Casts +
+ HOCalls + MethodCalls + EventCalls + Casts + Coerces +
PlainConjs + ParallelConjs +
Disjs + Switches +
IfThenElses + Negations + Scopes +
@@ -373,6 +377,8 @@ write_proc_stat_components(OutStream, Msg, Name, PredId, ProcId, Stats, !IO) :-
"event_calls", EventCalls, !IO),
output_proc_stat_component(OutStream, Msg, Name, PredId, ProcId,
"casts", Casts, !IO),
+ output_proc_stat_component(OutStream, Msg, Name, PredId, ProcId,
+ "coerces", Coerces, !IO),
output_proc_stat_component(OutStream, Msg, Name, PredId, ProcId,
"plain_conjs", PlainConjs, !IO),
diff --git a/compiler/intermod.m b/compiler/intermod.m
index d2c902d2d..1955c4fc5 100644
--- a/compiler/intermod.m
+++ b/compiler/intermod.m
@@ -625,6 +625,10 @@ gather_entities_to_opt_export_in_goal_expr(GoalExpr, DoWrite,
; CallType = cast(_)
),
DoWrite = no
+ ;
+ CallType = coerce,
+ % XXX SUBTYPE consider this later
+ DoWrite = no
)
;
GoalExpr = call_foreign_proc(Attrs, _, _, _, _, _, _),
diff --git a/compiler/interval.m b/compiler/interval.m
index 87e1ec3d1..59e6ff896 100644
--- a/compiler/interval.m
+++ b/compiler/interval.m
@@ -313,6 +313,7 @@ build_interval_info_in_goal(hlds_goal(GoalExpr, GoalInfo), !IntervalInfo,
( GenericCall = higher_order(_, _, _, _)
; GenericCall = class_method(_, _, _, _)
; GenericCall = event_call(_)
+ ; GenericCall = coerce
),
module_info_get_globals(ModuleInfo, Globals),
call_gen.generic_call_info(Globals, GenericCall,
@@ -995,6 +996,10 @@ record_decisions_in_goal(Goal0, Goal, !VarInfo, !VarRename, InsertMap,
(
GenericCall = cast(_),
MustHaveMap = no
+ ;
+ GenericCall = coerce,
+ % XXX SUBTYPE
+ sorry($pred, "coerce")
;
( GenericCall = higher_order(_, _, _, _)
; GenericCall = class_method(_, _, _, _)
diff --git a/compiler/lambda.m b/compiler/lambda.m
index 7bf5b3103..eef1282f8 100644
--- a/compiler/lambda.m
+++ b/compiler/lambda.m
@@ -782,6 +782,8 @@ find_used_vars_in_goal(Goal, !VarUses) :-
GenericCall = event_call(_)
;
GenericCall = cast(_)
+ ;
+ GenericCall = coerce
),
mark_vars_as_used(ArgVars, !VarUses)
;
diff --git a/compiler/live_vars.m b/compiler/live_vars.m
index af1a140b8..2a2b1de3d 100644
--- a/compiler/live_vars.m
+++ b/compiler/live_vars.m
@@ -467,7 +467,9 @@ build_live_sets_in_goal_expr(GoalExpr0, GoalExpr, GoalInfo0, GoalInfo,
GoalExpr0 = generic_call(GenericCall, ArgVars, Modes, _, _),
GoalExpr = GoalExpr0,
(
- GenericCall = cast(_),
+ ( GenericCall = cast(_)
+ ; GenericCall = coerce
+ ),
GoalInfo = GoalInfo0
;
( GenericCall = higher_order(_, _, _, _)
diff --git a/compiler/ml_call_gen.m b/compiler/ml_call_gen.m
index 7349d07fc..1fc3bee4c 100644
--- a/compiler/ml_call_gen.m
+++ b/compiler/ml_call_gen.m
@@ -125,6 +125,10 @@ ml_gen_generic_call(GenericCall, ArgVars, ArgModes, Determinism, Context,
;
GenericCall = cast(_),
ml_gen_cast(Context, ArgVars, LocalVarDefns, FuncDefns, Stmts, !Info)
+ ;
+ GenericCall = coerce,
+ % XXX SUBTYPE
+ sorry($pred, "coerce")
).
:- inst main_generic_call for generic_call/0
diff --git a/compiler/ml_code_gen.m b/compiler/ml_code_gen.m
index 988cc2736..769f14df4 100644
--- a/compiler/ml_code_gen.m
+++ b/compiler/ml_code_gen.m
@@ -783,10 +783,10 @@ goal_expr_find_subgoal_nonlocals(GoalExpr, SubGoalNonLocals) :-
_Name),
SubGoalNonLocals = set_of_var.list_to_set([MethodVar | ArgVars])
;
- GenericCall = event_call(_Eventname),
- SubGoalNonLocals = set_of_var.list_to_set(ArgVars)
- ;
- GenericCall = cast(_CastKind),
+ ( GenericCall = event_call(_Eventname)
+ ; GenericCall = cast(_CastKind)
+ ; GenericCall = coerce
+ ),
SubGoalNonLocals = set_of_var.list_to_set(ArgVars)
)
;
diff --git a/compiler/mode_constraints.m b/compiler/mode_constraints.m
index e1dd3ed8d..442dfb203 100644
--- a/compiler/mode_constraints.m
+++ b/compiler/mode_constraints.m
@@ -1364,6 +1364,9 @@ goal_constraints_2(GoalId, NonLocals, Vars, CanSucceed, GoalExpr0, GoalExpr,
;
GenericCall = cast(_),
sorry($pred, "type/inst cast call NYI")
+ ;
+ GenericCall = coerce,
+ sorry($pred, "coerce NYI")
),
GoalExpr = GoalExpr0
;
diff --git a/compiler/mode_errors.m b/compiler/mode_errors.m
index 345005e3e..a3dd30426 100644
--- a/compiler/mode_errors.m
+++ b/compiler/mode_errors.m
@@ -2,6 +2,7 @@
% vim: ft=mercury ts=4 sw=4 et
%---------------------------------------------------------------------------%
% Copyright (C) 1994-2012 The University of Melbourne.
+% Copyright (C) 2014-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.
%---------------------------------------------------------------------------%
@@ -159,6 +160,15 @@
% Different arms of a disjunction result in different insts
% for some non-local variables.
+ % Mode errors in coerce expressions.
+
+ ; 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 errors that can happen in more than one kind of goal.
; mode_error_bind_locked_var(var_lock_reason, prog_var,
@@ -460,6 +470,12 @@ mode_error_to_spec(ModeInfo, ModeError) = Spec :-
ModeError = mode_error_merge_disj(MergeContext, MergeErrors),
Spec = mode_error_merge_disj_to_spec(ModeInfo, MergeContext,
MergeErrors)
+ ;
+ ModeError = mode_error_coerce_input_not_ground(Var, VarInst),
+ Spec = mode_error_coerce_input_not_ground(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_bind_locked_var(Reason, Var, InstA, InstB),
Spec = mode_error_bind_locked_var_to_spec(ModeInfo, Reason, Var,
@@ -815,6 +831,7 @@ mode_error_no_matching_mode_to_spec(ModeInfo, Vars, Insts, InitialInsts)
;
( GenericCallId = gcid_event_call(_)
; GenericCallId = gcid_cast(_)
+ ; GenericCallId = gcid_coerce
),
PredOrFunc = pf_predicate
),
@@ -1291,6 +1308,41 @@ merge_context_to_string(merge_stm_atomic) = "atomic".
%---------------------------------------------------------------------------%
+:- func mode_error_coerce_input_not_ground(mode_info, prog_var, mer_inst) =
+ error_spec.
+
+mode_error_coerce_input_not_ground(ModeInfo, Var, VarInst) = Spec :-
+ Preamble = mode_info_context_preamble(ModeInfo),
+ mode_info_get_context(ModeInfo, Context),
+ mode_info_get_varset(ModeInfo, VarSet),
+ Pieces = [words("mode error:"),
+ quote(mercury_var_to_name_only(VarSet, Var))] ++
+ has_instantiatedness(ModeInfo, VarInst, ",") ++
+ [words("but it must be ground."), nl],
+ Spec = simplest_spec($pred, severity_error,
+ phase_mode_check(report_in_any_mode), Context, Preamble ++ Pieces).
+
+%---------------------------------------------------------------------------%
+
+:- func mode_error_coerce_bad_result_inst_to_spec(mode_info, mer_inst,
+ mer_type) = error_spec.
+
+mode_error_coerce_bad_result_inst_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")] ++
+ 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"),
+ quote(mercury_type_to_string(TypeVarSet, print_name_only, Type)),
+ suffix("."), nl],
+ Spec = simplest_spec($pred, severity_error,
+ phase_mode_check(report_in_any_mode), Context, Preamble ++ Pieces).
+
+%---------------------------------------------------------------------------%
+
:- func mode_error_bind_locked_var_to_spec(mode_info, var_lock_reason,
prog_var, mer_inst, mer_inst) = error_spec.
diff --git a/compiler/modecheck_coerce.m b/compiler/modecheck_coerce.m
new file mode 100644
index 000000000..1fba5db9f
--- /dev/null
+++ b/compiler/modecheck_coerce.m
@@ -0,0 +1,496 @@
+%---------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sw=4 et
+%---------------------------------------------------------------------------%
+% Copyright (C) 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.
+%---------------------------------------------------------------------------%
+%
+% File: modecheck_coerce.m.
+% Main author: wangp.
+%
+% This file contains the code to modecheck a coerce expression.
+%
+%---------------------------------------------------------------------------%
+
+:- module check_hlds.modecheck_coerce.
+:- interface.
+
+:- import_module check_hlds.mode_info.
+:- import_module check_hlds.modecheck_util.
+:- import_module parse_tree.
+:- import_module parse_tree.prog_data.
+
+:- import_module list.
+
+:- pred modecheck_coerce(list(prog_var)::in, list(prog_var)::out,
+ list(mer_mode)::in, list(mer_mode)::out, determinism::out,
+ extra_goals::out, mode_info::in, mode_info::out) is det.
+
+%---------------------------------------------------------------------------%
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module check_hlds.inst_test.
+:- import_module check_hlds.inst_util.
+:- import_module check_hlds.mode_errors.
+:- import_module check_hlds.modecheck_unify.
+:- import_module check_hlds.type_util.
+:- import_module hlds.
+:- import_module hlds.hlds_module.
+:- import_module hlds.instmap.
+:- import_module hlds.vartypes.
+:- import_module mdbcomp.
+:- import_module mdbcomp.sym_name.
+:- import_module parse_tree.prog_mode.
+:- import_module parse_tree.prog_type.
+:- import_module parse_tree.set_of_var.
+
+:- import_module maybe.
+:- import_module require.
+:- import_module set.
+:- import_module term.
+:- import_module varset.
+
+:- type modecheck_coerce_result
+ ---> coerce_mode_ok(
+ list(prog_var),
+ list(mer_mode),
+ extra_goals
+ )
+ ; coerce_mode_error.
+
+%---------------------------------------------------------------------------%
+
+modecheck_coerce(Args0, Args, Modes0, Modes, Det, ExtraGoals, !ModeInfo) :-
+ ( if Args0 = [X, Y] then
+ mode_info_get_module_info(!.ModeInfo, ModuleInfo0),
+ mode_info_get_instmap(!.ModeInfo, InstMap),
+ ( if instmap_is_reachable(InstMap) then
+ instmap_lookup_var(InstMap, X, InstX),
+ instmap_lookup_var(InstMap, Y, InstY),
+ ( if inst_is_ground(ModuleInfo0, InstX) then
+ modecheck_coerce_vars(ModuleInfo0, X, Y, InstX, InstY, Res,
+ !ModeInfo),
+ (
+ Res = coerce_mode_ok(Args, Modes, ExtraGoals),
+ Det = detism_det
+ ;
+ Res = coerce_mode_error,
+ Args = [X, Y],
+ Modes = Modes0,
+ Det = detism_erroneous,
+ ExtraGoals = no_extra_goals
+ )
+ else
+ WaitingVars = set_of_var.make_singleton(X),
+ ModeError = mode_error_coerce_input_not_ground(X, InstX),
+ mode_info_error(WaitingVars, ModeError, !ModeInfo),
+ Args = [X, Y],
+ Modes = Modes0,
+ Det = detism_erroneous,
+ ExtraGoals = no_extra_goals
+ )
+ else
+ Args = Args0,
+ Modes = Modes0,
+ Det = detism_erroneous,
+ ExtraGoals = no_extra_goals
+ )
+ else
+ unexpected($pred, "bad coerce")
+ ).
+
+:- pred modecheck_coerce_vars(module_info::in, prog_var::in, prog_var::in,
+ mer_inst::in, mer_inst::in, modecheck_coerce_result::out,
+ mode_info::in, mode_info::out) is det.
+
+modecheck_coerce_vars(ModuleInfo0, X, Y, InstX, InstY, Res, !ModeInfo) :-
+ mode_info_get_var_types(!.ModeInfo, VarTypes),
+ lookup_var_type(VarTypes, X, TypeX),
+ lookup_var_type(VarTypes, Y, TypeY),
+ set.init(Seen0),
+ make_bound_inst_for_type(ModuleInfo0, Seen0, TypeX, BoundInstForTypeX),
+ ( if
+ % XXX would we ever want to pass is_dead here?
+ abstractly_unify_inst(is_live, BoundInstForTypeX, InstX, fake_unify,
+ UnifyInstForTypeX, _Det, ModuleInfo0, ModuleInfo)
+ then
+ ( if
+ check_bound_functors_in_type(ModuleInfo, TypeY,
+ UnifyInstForTypeX, UnifyInstForTypeY)
+ then
+ mode_info_set_module_info(ModuleInfo, !ModeInfo),
+ % Y aliases X, so X loses uniqueness.
+ % (but if X becomes dead, Y could be unique?)
+ 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)
+ )
+ 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,
+ mer_type::in, mer_inst::out) is det.
+
+make_bound_inst_for_type(ModuleInfo, Seen0, Type, Inst) :-
+ (
+ Type = type_variable(_, _),
+ Inst = ground_inst
+ ;
+ Type = builtin_type(_),
+ Inst = ground_inst
+ ;
+ 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,
+ 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(shared, InstResults, BoundInsts)
+ else
+ unexpected($pred, "type_constructors fail")
+ )
+ else
+ % Does typed_ground help?
+ Inst = defined_inst(typed_ground(shared, Type))
+ )
+ ;
+ Type = tuple_type(ArgTypes, _Kind),
+ list.length(ArgTypes, Arity),
+ ConsId = tuple_cons(Arity),
+ list.map(make_bound_inst_for_type(ModuleInfo, Seen0),
+ 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(shared, InstResults, [BoundInst])
+ ;
+ Type = higher_order_type(_PredOrFunc, _ArgTypes, _HOInstInfo, _Purity,
+ _EvalMethod),
+ Inst = ground_inst
+ ;
+ Type = apply_n_type(_, _, _),
+ sorry($pred, "apply_n_type")
+ ;
+ Type = kinded_type(Type1, _),
+ make_bound_inst_for_type(ModuleInfo, Seen0, 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, list(constructor)::in, list(bound_inst)::out) is det.
+
+constructors_to_bound_insts_rec(ModuleInfo, Seen, TypeCtor, Constructors,
+ BoundInsts) :-
+ constructors_to_bound_insts_loop_over_ctors(ModuleInfo, Seen, TypeCtor,
+ Constructors, BoundInsts).
+
+:- pred constructors_to_bound_insts_loop_over_ctors(module_info::in,
+ set(type_ctor)::in, type_ctor::in, list(constructor)::in,
+ list(bound_inst)::out) is det.
+
+constructors_to_bound_insts_loop_over_ctors(_ModuleInfo, _Seen, _TypeCtor,
+ [], []).
+constructors_to_bound_insts_loop_over_ctors(ModuleInfo, Seen, TypeCtor,
+ [Ctor | Ctors], [BoundInst | BoundInsts]) :-
+ Ctor = ctor(_Ordinal, _MaybeExistConstraints, Name, Args, _Arity, _Ctxt),
+ ctor_arg_list_to_inst_list(ModuleInfo, Seen, Args, ArgInsts),
+ list.length(ArgInsts, Arity),
+ BoundInst = bound_functor(cons(Name, Arity, TypeCtor), ArgInsts),
+ constructors_to_bound_insts_loop_over_ctors(ModuleInfo, Seen, TypeCtor,
+ Ctors, BoundInsts).
+
+:- pred ctor_arg_list_to_inst_list(module_info::in, set(type_ctor)::in,
+ list(constructor_arg)::in, list(mer_inst)::out) is det.
+
+ctor_arg_list_to_inst_list(_ModuleInfo, _Seen, [], []).
+ctor_arg_list_to_inst_list(ModuleInfo, Seen,
+ [Arg | Args], [ArgInst | ArgInsts]) :-
+ Arg = ctor_arg(_MaybeFieldName, ArgType, _Context),
+ make_bound_inst_for_type(ModuleInfo, Seen, ArgType, ArgInst),
+ ctor_arg_list_to_inst_list(ModuleInfo, Seen, Args, ArgInsts).
+
+%---------------------------------------------------------------------------%
+
+ % 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")
+ ).
+
+%---------------------------------------------------------------------------%
+
+:- pred create_fresh_var(mer_type::in, prog_var::out,
+ mode_info::in, mode_info::out) is det.
+
+create_fresh_var(VarType, Var, !ModeInfo) :-
+ mode_info_get_var_types(!.ModeInfo, VarTypes0),
+ mode_info_get_varset(!.ModeInfo, VarSet0),
+ varset.new_var(Var, VarSet0, VarSet),
+ add_var_type(Var, VarType, VarTypes0, VarTypes),
+ mode_info_set_varset(VarSet, !ModeInfo),
+ mode_info_set_var_types(VarTypes, !ModeInfo).
+
+%---------------------------------------------------------------------------%
+:- end_module check_hlds.modecheck_coerce.
+%---------------------------------------------------------------------------%
diff --git a/compiler/modecheck_goal.m b/compiler/modecheck_goal.m
index f4ca85ce2..9eaff161f 100644
--- a/compiler/modecheck_goal.m
+++ b/compiler/modecheck_goal.m
@@ -2,7 +2,7 @@
% vim: ft=mercury ts=4 sw=4 et
%-----------------------------------------------------------------------------%
% Copyright (C) 2009-2012 The University of Melbourne.
-% Copyright (C) 2015 The Mercury team.
+% Copyright (C) 2014-2019, 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.
%-----------------------------------------------------------------------------%
@@ -114,6 +114,7 @@
:- import_module check_hlds.mode_errors.
:- import_module check_hlds.mode_util.
:- import_module check_hlds.modecheck_call.
+:- import_module check_hlds.modecheck_coerce.
:- import_module check_hlds.modecheck_conj.
:- import_module check_hlds.modecheck_unify.
:- import_module check_hlds.modecheck_util.
@@ -1357,6 +1358,14 @@ modecheck_goal_generic_call(GenericCall, Args0, Modes0, GoalInfo0, GoalExpr,
Det),
handle_extra_goals(GoalExpr1, ExtraGoals, GoalInfo0, Args0, Args,
InstMap0, GoalExpr, !ModeInfo)
+ ;
+ GenericCall = coerce,
+ modecheck_coerce(Args0, Args, Modes0, Modes, Det, ExtraGoals,
+ !ModeInfo),
+ GoalExpr1 = generic_call(GenericCall, Args, Modes, arg_reg_types_unset,
+ Det),
+ handle_extra_goals(GoalExpr1, ExtraGoals, GoalInfo0, Args0, Args,
+ InstMap0, GoalExpr, !ModeInfo)
),
mode_info_unset_call_context(!ModeInfo),
diff --git a/compiler/old_type_constraints.m b/compiler/old_type_constraints.m
index 372eee956..b2239216d 100644
--- a/compiler/old_type_constraints.m
+++ b/compiler/old_type_constraints.m
@@ -854,6 +854,9 @@ generic_call_goal_to_constraint(Environment, GoalExpr, GoalInfo, !TCInfo) :-
;
% Casts do not contain any type information.
Details = cast(_)
+ ;
+ Details = coerce,
+ sorry($pred, "coerce")
).
% Creates a constraint from the information stored in a predicate
diff --git a/compiler/post_typecheck.m b/compiler/post_typecheck.m
index bc152551b..71352321a 100644
--- a/compiler/post_typecheck.m
+++ b/compiler/post_typecheck.m
@@ -181,8 +181,8 @@ find_unproven_body_constraints(ModuleInfo, PredId, PredInfo,
list.sort_and_remove_dups(UnprovenConstraints0, UnprovenConstraints),
report_unsatisfied_constraints(ModuleInfo, PredId, PredInfo,
UnprovenConstraints, !NoTypeErrorSpecs),
- list.length(UnprovenConstraints, NumUmprovenConstraints),
- !:NumBadErrors = !.NumBadErrors + NumUmprovenConstraints
+ list.length(UnprovenConstraints, NumUnprovenConstraints),
+ !:NumBadErrors = !.NumBadErrors + NumUnprovenConstraints
;
UnprovenConstraints0 = []
).
@@ -342,6 +342,7 @@ describe_constrained_goal(ModuleInfo, Goal) = Pieces :-
;
( GoalExpr = generic_call(event_call(_), _, _, _, _)
; GoalExpr = generic_call(cast(_), _, _, _, _)
+ ; GoalExpr = generic_call(coerce, _, _, _, _)
; GoalExpr = unify(_, _, _, _, _)
; GoalExpr = conj(_, _)
; GoalExpr = disj(_)
diff --git a/compiler/pre_quantification.m b/compiler/pre_quantification.m
index e80e30c52..6b4632357 100644
--- a/compiler/pre_quantification.m
+++ b/compiler/pre_quantification.m
@@ -202,6 +202,8 @@ build_vars_to_zones_in_goal(CurZone, Goal, !TraceCounter, !VarsToZones) :-
GenericCall = event_call(_)
;
GenericCall = cast(_)
+ ;
+ GenericCall = coerce
)
;
GoalExpr = call_foreign_proc(_Attrs, _PredId, _ProcId,
diff --git a/compiler/prog_rep.m b/compiler/prog_rep.m
index aa2f2c8df..e718820b0 100644
--- a/compiler/prog_rep.m
+++ b/compiler/prog_rep.m
@@ -573,6 +573,14 @@ goal_to_goal_rep(Info, Instmap0, hlds_goal(GoalExpr, GoalInfo), GoalRep) :-
else
unexpected($pred, "cast arity != 2")
)
+ ;
+ GenericCall = coerce,
+ ( if ArgsRep = [InputArgRep, OutputArgRep] then
+ % XXX SUBTYPE add coerce_rep
+ AtomicGoalRep = cast_rep(OutputArgRep, InputArgRep)
+ else
+ unexpected($pred, "coerce arity != 2")
+ )
)
;
GoalExpr = plain_call(PredId, _, Args, Builtin, _, _),
diff --git a/compiler/prog_type.m b/compiler/prog_type.m
index 1d66c0794..d6d30ae76 100644
--- a/compiler/prog_type.m
+++ b/compiler/prog_type.m
@@ -85,6 +85,11 @@
%
:- pred type_is_ground(mer_type::in) is semidet.
+ % Succeeds iff the given type contains no type variables except
+ % for those in the given list.
+ %
+:- pred type_is_ground_except_vars(mer_type::in, list(tvar)::in) is semidet.
+
% Succeeds iff the given type is not ground.
%
:- pred type_is_nonground(mer_type::in) is semidet.
@@ -477,6 +482,13 @@ strip_kind_annotation(Type0) = Type :-
type_is_ground(Type) :-
not type_contains_var(Type, _).
+type_is_ground_except_vars(Type, Except) :-
+ all [TVar] (
+ type_contains_var(Type, TVar)
+ =>
+ list.contains(Except, TVar)
+ ).
+
type_is_nonground(Type) :-
type_contains_var(Type, _).
diff --git a/compiler/purity.m b/compiler/purity.m
index 915e79c76..ac40b24ac 100644
--- a/compiler/purity.m
+++ b/compiler/purity.m
@@ -677,6 +677,7 @@ compute_expr_purity(GoalExpr0, GoalExpr, GoalInfo, Purity, ContainsTrace,
Purity = purity_pure % XXX this is wrong!
;
( GenericCall0 = cast(_)
+ ; GenericCall0 = coerce
; GenericCall0 = event_call(_)
),
Purity = purity_pure
diff --git a/compiler/simplify_goal.m b/compiler/simplify_goal.m
index 5a0c71001..5f24be106 100644
--- a/compiler/simplify_goal.m
+++ b/compiler/simplify_goal.m
@@ -434,6 +434,9 @@ will_flush(GoalExpr, BeforeAfter) = WillFlush :-
;
GenericCall = cast(_),
WillFlush0 = no
+ ;
+ GenericCall = coerce,
+ WillFlush0 = no
),
(
BeforeAfter = before,
diff --git a/compiler/simplify_goal_call.m b/compiler/simplify_goal_call.m
index 8b416ffbf..f7cff3195 100644
--- a/compiler/simplify_goal_call.m
+++ b/compiler/simplify_goal_call.m
@@ -262,6 +262,7 @@ simplify_goal_generic_call(GoalExpr0, GoalExpr, GoalInfo, GoalInfo,
;
( GenericCall = class_method(_, _, _, _)
; GenericCall = cast(_)
+ ; GenericCall = coerce
),
GoalExpr = GoalExpr0,
Common = Common0
diff --git a/compiler/structure_reuse.direct.detect_garbage.m b/compiler/structure_reuse.direct.detect_garbage.m
index f56a10d14..2e0dd945e 100644
--- a/compiler/structure_reuse.direct.detect_garbage.m
+++ b/compiler/structure_reuse.direct.detect_garbage.m
@@ -235,6 +235,7 @@ determine_dead_deconstructions_generic_call(ModuleInfo, ProcInfo,
;
( GenDetails = event_call(_) % XXX too conservative
; GenDetails = cast(_)
+ ; GenDetails = coerce
),
SetToTop = yes
),
diff --git a/compiler/structure_reuse.indirect.m b/compiler/structure_reuse.indirect.m
index 815011cc0..00b15f7ea 100644
--- a/compiler/structure_reuse.indirect.m
+++ b/compiler/structure_reuse.indirect.m
@@ -660,6 +660,7 @@ indirect_reuse_analyse_generic_call(BaseInfo, GenDetails, CallArgs, Modes,
;
( GenDetails = event_call(_) % XXX too conservative
; GenDetails = cast(_)
+ ; GenDetails = coerce
),
SetToTop = yes
),
diff --git a/compiler/structure_sharing.analysis.m b/compiler/structure_sharing.analysis.m
index a25a94abc..bd71c4d8c 100644
--- a/compiler/structure_sharing.analysis.m
+++ b/compiler/structure_sharing.analysis.m
@@ -770,6 +770,7 @@ analyse_generic_call(ModuleInfo, ProcInfo, GenDetails, CallArgs, Modes,
;
( GenDetails = event_call(_) % XXX too conservative
; GenDetails = cast(_)
+ ; GenDetails = coerce
),
SetToTop = yes
),
diff --git a/compiler/superhomogeneous.m b/compiler/superhomogeneous.m
index 51ecb3134..ff9d2a7c6 100644
--- a/compiler/superhomogeneous.m
+++ b/compiler/superhomogeneous.m
@@ -2,7 +2,7 @@
% vim: ft=mercury ts=4 sw=4 et
%-----------------------------------------------------------------------------%
% Copyright (C) 2005-2012 The University of Melbourne.
-% Copyright (C) 2014-2018 The Mercury team.
+% Copyright (C) 2014-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.
%-----------------------------------------------------------------------------%
@@ -1084,6 +1084,34 @@ maybe_unravel_special_var_functor_unification(XVar, YAtom, YArgTerms,
% qual_info_set_found_syntax_error(yes, !QualInfo),
% Expansion = expansion(not_fgti, cord.empty)
)
+ ;
+ % Handle coerce expressions.
+ YAtom = "coerce",
+ YArgTerms = [RValTerm0],
+ require_det (
+ (
+ RValTerm0 = term.variable(RValTermVar, _),
+ RValGoalCord = cord.empty
+ ;
+ RValTerm0 = term.functor(_, _, _),
+ substitute_state_var_mapping(RValTerm0, RValTerm,
+ !VarSet, !SVarState, !Specs),
+ make_fresh_arg_var_no_svar(RValTerm0, RValTermVar, [],
+ !VarSet),
+ do_unravel_var_unification(RValTermVar, RValTerm, Context,
+ MainContext, SubContext, Purity, Order, RValTermExpansion,
+ !SVarState, !SVarStore, !VarSet,
+ !ModuleInfo, !QualInfo, !Specs),
+ RValTermExpansion = expansion(_, RValGoalCord)
+ ),
+ CoerceGoalExpr = generic_call(coerce,
+ [RValTermVar, XVar], [in_mode, out_mode],
+ arg_reg_types_unset, detism_det),
+ goal_info_init(Context, CoerceGoalInfo),
+ CoerceGoal = hlds_goal(CoerceGoalExpr, CoerceGoalInfo),
+ CoerceGoalCord = cord.singleton(CoerceGoal),
+ Expansion = expansion(not_fgti, RValGoalCord ++ CoerceGoalCord)
+ )
;
% Handle if-then-else expressions.
(
diff --git a/compiler/tabling_analysis.m b/compiler/tabling_analysis.m
index 07d82b594..518247613 100644
--- a/compiler/tabling_analysis.m
+++ b/compiler/tabling_analysis.m
@@ -343,6 +343,9 @@ check_goal_for_mm_tabling(SCC, VarTypes, Goal, Result, MaybeAnalysisStatus,
;
Details = cast(_),
Result = mm_tabled_will_not_call
+ ;
+ Details = coerce,
+ Result = mm_tabled_will_not_call
),
MaybeAnalysisStatus = yes(optimal)
;
@@ -635,6 +638,9 @@ mm_tabling_annotate_goal_2(VarTypes, !GoalExpr, Status, !ModuleInfo) :-
;
GenericCall = cast(_),
Status = mm_tabled_will_not_call
+ ;
+ GenericCall = coerce,
+ Status = mm_tabled_will_not_call
)
;
!.GoalExpr = conj(ConjType, Conjuncts0),
diff --git a/compiler/term_traversal.m b/compiler/term_traversal.m
index a0d005de8..9626970a8 100644
--- a/compiler/term_traversal.m
+++ b/compiler/term_traversal.m
@@ -308,6 +308,8 @@ term_traverse_goal(ModuleInfo, Params, Goal, !Info) :-
Details = event_call(_)
;
Details = cast(_)
+ ;
+ Details = coerce
)
;
GoalExpr = conj(_, Goals),
diff --git a/compiler/trailing_analysis.m b/compiler/trailing_analysis.m
index 1b690a6a5..fb182d4fe 100644
--- a/compiler/trailing_analysis.m
+++ b/compiler/trailing_analysis.m
@@ -429,6 +429,7 @@ check_goal_for_trail_mods(SCC, VarTypes, Goal, Result, MaybeAnalysisStatus,
MaybeAnalysisStatus = yes(optimal)
;
( Details = cast(_)
+ ; Details = coerce
; Details = event_call(_)
),
Result = trail_will_not_modify,
@@ -955,6 +956,9 @@ trail_annotate_goal_2(VarTypes, GoalInfo, !GoalExpr, Status, !ModuleInfo) :-
;
GenericCall = cast(_),
Status = trail_will_not_modify
+ ;
+ GenericCall = coerce,
+ Status = trail_will_not_modify
)
;
!.GoalExpr = conj(ConjType, Conjuncts0),
diff --git a/compiler/tupling.m b/compiler/tupling.m
index c3fc527bd..43393059c 100644
--- a/compiler/tupling.m
+++ b/compiler/tupling.m
@@ -1110,7 +1110,9 @@ count_load_stores_in_goal(Goal, CountInfo, !CountState) :-
count_load_stores_for_call(CountInfo, Inputs, Outputs,
MaybeNeedAcrossCall, GoalInfo, !CountState)
;
- GenericCall = cast(_),
+ ( GenericCall = cast(_)
+ ; GenericCall = coerce
+ ),
% Casts are generated inline.
cls_require_in_regs(CountInfo, InputArgs, !CountState),
cls_put_in_regs(OutputArgs, !CountState)
diff --git a/compiler/type_assign.m b/compiler/type_assign.m
index 097fe3ff2..795a8e8aa 100644
--- a/compiler/type_assign.m
+++ b/compiler/type_assign.m
@@ -1,7 +1,7 @@
%-----------------------------------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et
%-----------------------------------------------------------------------------%
-% Copyright (C) 2014 The Mercury team.
+% Copyright (C) 2014-2015, 2018, 2020-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.
%-----------------------------------------------------------------------------%
@@ -46,6 +46,9 @@
% Type bindings.
ta_type_bindings :: tsubst,
+ % The list of coerce constraints collected so far.
+ ta_coerce_constraints :: list(coerce_constraint),
+
% The set of class constraints collected so far.
ta_class_constraints :: hlds_constraints,
@@ -56,6 +59,19 @@
ta_constraint_map :: constraint_map
).
+:- type coerce_constraint
+ ---> coerce_constraint(
+ % One or both sides should be a type_variable.
+ coerce_from :: mer_type,
+ coerce_to :: mer_type,
+ coerce_context :: prog_context,
+ coerce_status :: coerce_constraint_status
+ ).
+
+:- type coerce_constraint_status
+ ---> need_to_check
+ ; unsatisfiable.
+
:- pred type_assign_get_var_types(type_assign::in,
vartypes::out) is det.
:- pred type_assign_get_typevarset(type_assign::in,
@@ -64,6 +80,8 @@
external_type_params::out) is det.
:- pred type_assign_get_type_bindings(type_assign::in,
tsubst::out) is det.
+:- pred type_assign_get_coerce_constraints(type_assign::in,
+ list(coerce_constraint)::out) is det.
:- pred type_assign_get_typeclass_constraints(type_assign::in,
hlds_constraints::out) is det.
:- pred type_assign_get_constraint_proof_map(type_assign::in,
@@ -79,6 +97,8 @@
type_assign::in, type_assign::out) is det.
:- pred type_assign_set_type_bindings(tsubst::in,
type_assign::in, type_assign::out) is det.
+:- pred type_assign_set_coerce_constraints(list(coerce_constraint)::in,
+ type_assign::in, type_assign::out) is det.
:- pred type_assign_set_typeclass_constraints(hlds_constraints::in,
type_assign::in, type_assign::out) is det.
:- pred type_assign_set_constraint_proof_map(constraint_proof_map::in,
@@ -212,6 +232,8 @@ type_assign_get_external_type_params(TA, X) :-
X = TA ^ ta_external_type_params.
type_assign_get_type_bindings(TA, X) :-
X = TA ^ ta_type_bindings.
+type_assign_get_coerce_constraints(TA, X) :-
+ X = TA ^ ta_coerce_constraints.
type_assign_get_typeclass_constraints(TA, X) :-
X = TA ^ ta_class_constraints.
type_assign_get_constraint_proof_map(TA, X) :-
@@ -227,6 +249,8 @@ type_assign_set_external_type_params(X, !TA) :-
!TA ^ ta_external_type_params := X.
type_assign_set_type_bindings(X, !TA) :-
!TA ^ ta_type_bindings := X.
+type_assign_set_coerce_constraints(X, !TA) :-
+ !TA ^ ta_coerce_constraints := X.
type_assign_set_typeclass_constraints(X, !TA) :-
!TA ^ ta_class_constraints := X.
type_assign_set_constraint_proof_map(X, !TA) :-
@@ -236,19 +260,21 @@ type_assign_set_constraint_map(X, !TA) :-
type_assign_set_reduce_results(TVarSet, Bindings, Constraints, ProofMap,
ConstraintMap, TypeAssign0, TypeAssign) :-
- TypeAssign0 = type_assign(VarTypes, _, ExternalTypeParams, _, _, _, _),
+ TypeAssign0 = type_assign(VarTypes, _, ExternalTypeParams, _,
+ Coercions, _, _, _),
TypeAssign = type_assign(VarTypes, TVarSet, ExternalTypeParams, Bindings,
- Constraints, ProofMap, ConstraintMap).
+ Coercions, Constraints, ProofMap, ConstraintMap).
%-----------------------------------------------------------------------------%
type_assign_set_init(TypeVarSet, VarTypes, ExternalTypeParams, Constraints,
TypeAssignSet) :-
map.init(TypeBindings),
+ Coercions = [],
map.init(ProofMap),
map.init(ConstraintMap),
TypeAssignSet = [type_assign(VarTypes, TypeVarSet, ExternalTypeParams,
- TypeBindings, Constraints, ProofMap, ConstraintMap)].
+ TypeBindings, Coercions, Constraints, ProofMap, ConstraintMap)].
type_assign_set_get_final_info(TypeAssignSet,
OldExternalTypeParams, OldExistQVars,
@@ -264,7 +290,7 @@ type_assign_set_get_final_info(TypeAssignSet,
),
TypeAssign = type_assign(VarTypes0, OldTypeVarSet, ExternalTypeParams,
- TypeBindings, HLDSTypeConstraints, ConstraintProofMap0,
+ TypeBindings, _Coercions0, HLDSTypeConstraints, ConstraintProofMap0,
ConstraintMap0),
( if map.is_empty(TypeBindings) then
diff --git a/compiler/typecheck.m b/compiler/typecheck.m
index 34de4d121..ee1f7cb6f 100644
--- a/compiler/typecheck.m
+++ b/compiler/typecheck.m
@@ -2,7 +2,7 @@
% vim: ft=mercury ts=4 sw=4 et
%---------------------------------------------------------------------------%
% Copyright (C) 1993-2012 The University of Melbourne.
-% Copyright (C) 2014-2018 The Mercury team.
+% Copyright (C) 2014-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.
%---------------------------------------------------------------------------%
@@ -142,6 +142,7 @@
:- import_module int.
:- import_module map.
:- import_module maybe.
+:- import_module one_or_more.
:- import_module pair.
:- import_module require.
:- import_module set.
@@ -681,6 +682,7 @@ do_typecheck_pred(ModuleInfo, PredId, !PredInfo, !Specs, NextIteration) :-
perform_context_reduction(Context, !TypeAssignSet, !Info),
typecheck_check_for_ambiguity(Context, whole_pred, HeadVars,
!.TypeAssignSet, !Info),
+ typecheck_check_for_unsatisfied_coercions(!.TypeAssignSet, !Info),
type_assign_set_get_final_info(!.TypeAssignSet,
!.ExternalTypeParams, ExistQVars0, ExplicitVarTypes0, TypeVarSet,
!:ExternalTypeParams, InferredVarTypes0, InferredTypeConstraints0,
@@ -750,7 +752,7 @@ do_typecheck_pred(ModuleInfo, PredId, !PredInfo, !Specs, NextIteration) :-
pred_info_get_tvar_kind_map(!.PredInfo, TVarKindMap),
argtypes_identical_up_to_renaming(TVarKindMap, ExistQVars0,
ArgTypes0, OldTypeConstraints, ExistQVars, ArgTypes,
- InferredTypeConstraints)
+ InferredTypeConstraints)
;
% Promises cannot be called from anywhere. Therefore
% even if the types of their arguments have changed,
@@ -1161,6 +1163,7 @@ typecheck_clause(HeadVars, ArgTypes, !Clause, !TypeAssignSet, !Info) :-
type_checkpoint("end of clause", ModuleInfo, VarSet, !.TypeAssignSet,
!IO)
),
+ typecheck_prune_coerce_constraints(!TypeAssignSet, !Info),
!Clause ^ clause_body := Body,
typecheck_check_for_ambiguity(Context, clause_only, HeadVars,
!.TypeAssignSet, !Info).
@@ -1246,6 +1249,50 @@ typecheck_check_for_ambiguity(Context, StuffToCheck, HeadVars,
%---------------------------------------------------------------------------%
+:- pred typecheck_check_for_unsatisfied_coercions(type_assign_set::in,
+ typecheck_info::in, typecheck_info::out) is det.
+
+typecheck_check_for_unsatisfied_coercions(TypeAssignSet, !Info) :-
+ (
+ TypeAssignSet = [],
+ unexpected($pred, "no type-assignment")
+ ;
+ TypeAssignSet = [TypeAssign],
+ type_assign_get_coerce_constraints(TypeAssign, Coercions),
+ (
+ Coercions = []
+ ;
+ Coercions = [_ | _],
+ % All valid coercion constraints have been removed from the
+ % type assignment already.
+ list.foldl(report_invalid_coercion(TypeAssign), Coercions, !Info)
+ )
+ ;
+ TypeAssignSet = [_, _ | _]
+ % If there are multple type assignments then there is a type ambiguity
+ % error anyway. Reporting invalid coercions from different type
+ % assignments would be confusing.
+ ).
+
+:- pred report_invalid_coercion(type_assign::in, coerce_constraint::in,
+ typecheck_info::in, typecheck_info::out) is det.
+
+report_invalid_coercion(TypeAssign, Coercion, !Info) :-
+ % XXX When inferring types for a predicate/function with no declared type,
+ % we should not report coercions as invalid until the argument types have
+ % been inferred.
+ Coercion = coerce_constraint(FromType0, ToType0, Context, _Status),
+ type_assign_get_typevarset(TypeAssign, TVarSet),
+ type_assign_get_type_bindings(TypeAssign, TypeBindings),
+ apply_rec_subst_to_type(TypeBindings, FromType0, FromType),
+ apply_rec_subst_to_type(TypeBindings, ToType0, ToType),
+ typecheck_info_get_error_clause_context(!.Info, ClauseContext),
+ Spec = report_invalid_coerce_from_to(ClauseContext, Context, TVarSet,
+ FromType, ToType),
+ typecheck_info_add_error(Spec, !Info).
+
+%---------------------------------------------------------------------------%
+
:- pred typecheck_goal(hlds_goal::in, hlds_goal::out, prog_context::in,
type_assign_set::in, type_assign_set::out,
typecheck_info::in, typecheck_info::out) is det.
@@ -1411,8 +1458,7 @@ typecheck_goal_expr(GoalExpr0, GoalExpr, GoalInfo, !TypeAssignSet, !Info) :-
GenericCall = higher_order(PredVar, Purity, _, _),
trace [compiletime(flag("type_checkpoint")), io(!IO)] (
type_checkpoint("higher-order call", ModuleInfo, VarSet,
- !.TypeAssignSet,
- !IO)
+ !.TypeAssignSet, !IO)
),
hlds_goal.generic_call_to_id(GenericCall, GenericCallId),
typecheck_higher_order_call(GenericCallId, Context,
@@ -1432,6 +1478,13 @@ typecheck_goal_expr(GoalExpr0, GoalExpr, GoalInfo, !TypeAssignSet, !Info) :-
GenericCall = cast(_)
% A cast imposes no restrictions on its argument types,
% so nothing needs to be done here.
+ ;
+ GenericCall = coerce,
+ trace [compiletime(flag("type_checkpoint")), io(!IO)] (
+ type_checkpoint("coerce", ModuleInfo, VarSet,
+ !.TypeAssignSet, !IO)
+ ),
+ typecheck_coerce(Context, Args, !TypeAssignSet, !Info)
),
GoalExpr = GoalExpr0
;
@@ -2765,16 +2818,23 @@ type_assign_get_types_of_vars([Var | Vars], [Type | Types], !TypeAssign) :-
else
% Otherwise, introduce a fresh type variable with kind `star' to use
% as the type of that variable.
- type_assign_get_typevarset(!.TypeAssign, TypeVarSet0),
- varset.new_var(TypeVar, TypeVarSet0, TypeVarSet),
- type_assign_set_typevarset(TypeVarSet, !TypeAssign),
- Type = type_variable(TypeVar, kind_star),
- add_var_type(Var, Type, VarTypes0, VarTypes1),
- type_assign_set_var_types(VarTypes1, !TypeAssign)
+ type_assign_fresh_type_var(Var, Type, !TypeAssign)
),
% Recursively process the rest of the variables.
type_assign_get_types_of_vars(Vars, Types, !TypeAssign).
+:- pred type_assign_fresh_type_var(prog_var::in, mer_type::out,
+ type_assign::in, type_assign::out) is det.
+
+type_assign_fresh_type_var(Var, Type, !TypeAssign) :-
+ type_assign_get_var_types(!.TypeAssign, VarTypes0),
+ type_assign_get_typevarset(!.TypeAssign, TypeVarSet0),
+ varset.new_var(TypeVar, TypeVarSet0, TypeVarSet),
+ type_assign_set_typevarset(TypeVarSet, !TypeAssign),
+ Type = type_variable(TypeVar, kind_star),
+ add_var_type(Var, Type, VarTypes0, VarTypes1),
+ type_assign_set_var_types(VarTypes1, !TypeAssign).
+
%---------------------------------------------------------------------------%
% Unify (with occurs check) two types in a type assignment
@@ -2789,6 +2849,102 @@ type_assign_unify_type(X, Y, TypeAssign0, TypeAssign) :-
type_unify(X, Y, HeadTypeParams, TypeBindings0, TypeBindings),
type_assign_set_type_bindings(TypeBindings, TypeAssign0, TypeAssign).
+%---------------------------------------------------------------------------%
+
+:- pred typecheck_coerce(prog_context::in, list(prog_var)::in,
+ type_assign_set::in, type_assign_set::out,
+ typecheck_info::in, typecheck_info::out) is det.
+
+typecheck_coerce(Context, Args, TypeAssignSet0, TypeAssignSet, !Info) :-
+ ( if Args = [FromVar0, ToVar0] then
+ FromVar = FromVar0,
+ ToVar = ToVar0
+ else
+ unexpected($pred, "coerce requires two arguments")
+ ),
+ list.foldl2(typecheck_coerce_2(Context, FromVar, ToVar),
+ TypeAssignSet0, [], TypeAssignSet1, !Info),
+ ( if
+ TypeAssignSet1 = [],
+ TypeAssignSet0 = [_ | _]
+ then
+ TypeAssignSet = TypeAssignSet0
+ else
+ TypeAssignSet = TypeAssignSet1
+ ).
+
+:- pred typecheck_coerce_2(prog_context::in, prog_var::in, prog_var::in,
+ type_assign::in, type_assign_set::in, type_assign_set::out,
+ typecheck_info::in, typecheck_info::out) is det.
+
+typecheck_coerce_2(Context, FromVar, ToVar, TypeAssign0,
+ !TypeAssignSet, !Info) :-
+ type_assign_get_var_types(TypeAssign0, VarTypes),
+ type_assign_get_typevarset(TypeAssign0, TVarSet),
+ type_assign_get_external_type_params(TypeAssign0, ExternalTypeParams),
+ type_assign_get_type_bindings(TypeAssign0, TypeBindings),
+
+ ( if search_var_type(VarTypes, FromVar, FromType0) then
+ apply_rec_subst_to_type(TypeBindings, FromType0, FromType1),
+ MaybeFromType = yes(FromType1)
+ else
+ MaybeFromType = no
+ ),
+ ( if search_var_type(VarTypes, ToVar, ToType0) then
+ apply_rec_subst_to_type(TypeBindings, ToType0, ToType1),
+ MaybeToType = yes(ToType1)
+ else
+ MaybeToType = no
+ ),
+
+ ( if
+ MaybeFromType = yes(FromType),
+ MaybeToType = yes(ToType),
+ type_is_ground_except_vars(FromType, ExternalTypeParams),
+ type_is_ground_except_vars(ToType, ExternalTypeParams)
+ then
+ % We can compare the types on both sides immediately.
+ typecheck_info_get_type_table(!.Info, TypeTable),
+ ( if
+ typecheck_coerce_between_types(TypeTable, TVarSet,
+ FromType, ToType)
+ then
+ TypeAssign = TypeAssign0
+ else
+ type_assign_get_coerce_constraints(TypeAssign0, Coercions0),
+ Coercion = coerce_constraint(FromType, ToType, Context,
+ unsatisfiable),
+ Coercions = [Coercion | Coercions0],
+ type_assign_set_coerce_constraints(Coercions,
+ TypeAssign0, TypeAssign)
+ ),
+ !:TypeAssignSet = [TypeAssign | !.TypeAssignSet]
+ else
+ % One or both of the types is not known yet. Add a coercion constraint
+ % on the type assignment to be checked after typechecking the clause.
+ (
+ MaybeFromType = yes(FromType),
+ TypeAssign1 = TypeAssign0
+ ;
+ MaybeFromType = no,
+ type_assign_fresh_type_var(FromVar, FromType,
+ TypeAssign0, TypeAssign1)
+ ),
+ (
+ MaybeToType = yes(ToType),
+ TypeAssign2 = TypeAssign1
+ ;
+ MaybeToType = no,
+ type_assign_fresh_type_var(ToVar, ToType,
+ TypeAssign1, TypeAssign2)
+ ),
+ type_assign_get_coerce_constraints(TypeAssign2, Coercions0),
+ Coercion = coerce_constraint(FromType, ToType, Context, need_to_check),
+ Coercions = [Coercion | Coercions0],
+ type_assign_set_coerce_constraints(Coercions, TypeAssign2, TypeAssign),
+ !:TypeAssignSet = [TypeAssign | !.TypeAssignSet]
+ ).
+
%---------------------------------------------------------------------------%
%---------------------------------------------------------------------------%
@@ -3565,6 +3721,361 @@ convert_cons_defn(Info, GoalId, Action, HLDS_ConsDefn, ConsTypeInfo) :-
ConsType, ArgTypes, Constraints, source_type(TypeCtor)))
).
+%---------------------------------------------------------------------------%
+%---------------------------------------------------------------------------%
+
+:- pred typecheck_coerce_between_types(type_table::in, tvarset::in,
+ mer_type::in, mer_type::in) is semidet.
+
+typecheck_coerce_between_types(TypeTable, TVarSet, FromType, ToType) :-
+ % Type bindings must have been aplpied to FromType and ToType already.
+ replace_principal_type_ctor_with_base(TypeTable, TVarSet,
+ FromType, FromBaseType),
+ replace_principal_type_ctor_with_base(TypeTable, TVarSet,
+ ToType, ToBaseType),
+ type_to_ctor_and_args(FromBaseType, FromBaseTypeCtor, FromBaseTypeArgs),
+ type_to_ctor_and_args(ToBaseType, ToBaseTypeCtor, ToBaseTypeArgs),
+
+ % The input type and result type must share a base type constructor.
+ BaseTypeCtor = FromBaseTypeCtor,
+ BaseTypeCtor = ToBaseTypeCtor,
+
+ % Check the variance of type arguments.
+ hlds_data.search_type_ctor_defn(TypeTable, BaseTypeCtor, BaseTypeDefn),
+ hlds_data.get_type_defn_tparams(BaseTypeDefn, BaseTypeParams),
+ build_type_param_variance_restrictions(TypeTable, BaseTypeCtor,
+ InvariantSet),
+ check_type_param_variance_restrictions(TypeTable, TVarSet, InvariantSet,
+ BaseTypeParams, FromBaseTypeArgs, ToBaseTypeArgs).
+
+:- pred replace_principal_type_ctor_with_base(type_table::in, tvarset::in,
+ mer_type::in, mer_type::out) is det.
+
+replace_principal_type_ctor_with_base(TypeTable, TVarSet, Type0, Type) :-
+ ( if
+ type_to_ctor_and_args(Type0, TypeCtor, Args),
+ get_supertype(TypeTable, TVarSet, TypeCtor, Args, SuperType)
+ then
+ replace_principal_type_ctor_with_base(TypeTable, TVarSet,
+ SuperType, Type)
+ else
+ 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).
+
+:- pred build_type_param_variance_restrictions(type_table::in,
+ type_ctor::in, invariant_set::out) is det.
+
+build_type_param_variance_restrictions(TypeTable, TypeCtor, InvariantSet) :-
+ ( if
+ hlds_data.search_type_ctor_defn(TypeTable, TypeCtor, TypeDefn),
+ hlds_data.get_type_defn_tparams(TypeDefn, TypeParams),
+ hlds_data.get_type_defn_body(TypeDefn, TypeBody),
+ TypeBody = hlds_du_type(OoMCtors, _MaybeSuperType, _MaybeCanonical,
+ _MaybeTypeRepn, _IsForeignType)
+ then
+ Ctors = one_or_more_to_list(OoMCtors),
+ list.foldl(
+ build_type_param_variance_restrictions_in_ctor(TypeTable,
+ TypeCtor, TypeParams),
+ Ctors, set.init, InvariantSet)
+ else
+ unexpected($pred, "not du type")
+ ).
+
+:- pred build_type_param_variance_restrictions_in_ctor(type_table::in,
+ type_ctor::in, list(tvar)::in, constructor::in,
+ invariant_set::in, invariant_set::out) is det.
+
+build_type_param_variance_restrictions_in_ctor(TypeTable, CurTypeCtor,
+ CurTypeParams, Ctor, !InvariantSet) :-
+ Ctor = ctor(_Ordinal, _MaybeExistConstraints, _CtorName, CtorArgs, _Arity,
+ _Context),
+ list.foldl(
+ build_type_param_variance_restrictions_in_ctor_arg(TypeTable,
+ CurTypeCtor, CurTypeParams),
+ CtorArgs, !InvariantSet).
+
+:- pred build_type_param_variance_restrictions_in_ctor_arg(type_table::in,
+ type_ctor::in, list(tvar)::in, constructor_arg::in,
+ invariant_set::in, invariant_set::out) is det.
+
+build_type_param_variance_restrictions_in_ctor_arg(TypeTable, CurTypeCtor,
+ CurTypeParams, CtorArg, !InvariantSet) :-
+ CtorArg = ctor_arg(_MaybeFieldName, CtorArgType, _Context),
+ build_type_param_variance_restrictions_in_ctor_arg_type(TypeTable,
+ CurTypeCtor, CurTypeParams, CtorArgType, !InvariantSet).
+
+:- pred build_type_param_variance_restrictions_in_ctor_arg_type(type_table::in,
+ type_ctor::in, list(tvar)::in, mer_type::in,
+ invariant_set::in, invariant_set::out) is det.
+
+build_type_param_variance_restrictions_in_ctor_arg_type(TypeTable, CurTypeCtor,
+ CurTypeParams, CtorArgType, !InvariantSet) :-
+ (
+ CtorArgType = builtin_type(_)
+ ;
+ CtorArgType = type_variable(_TypeVar, _Kind)
+ ;
+ CtorArgType = defined_type(_SymName, ArgTypes, _Kind),
+ ( if
+ type_to_ctor_and_args(CtorArgType, TypeCtor, TypeArgs),
+ hlds_data.search_type_ctor_defn(TypeTable, TypeCtor, TypeDefn)
+ then
+ hlds_data.get_type_defn_body(TypeDefn, TypeBody),
+ require_complete_switch [TypeBody]
+ (
+ TypeBody = hlds_du_type(_, _, _, _, _),
+ ( if
+ TypeCtor = CurTypeCtor,
+ type_list_to_var_list(TypeArgs, CurTypeParams)
+ then
+ % A recursive type that matches exactly the current type
+ % head does not impose any restrictions on the type
+ % parameters.
+ true
+ else
+ type_vars_list(ArgTypes, TypeVars),
+ set.insert_list(TypeVars, !InvariantSet)
+ )
+ ;
+ ( TypeBody = hlds_foreign_type(_)
+ ; TypeBody = hlds_abstract_type(_)
+ ; TypeBody = hlds_solver_type(_)
+ ),
+ type_vars_list(ArgTypes, TypeVars),
+ set.insert_list(TypeVars, !InvariantSet)
+ ;
+ TypeBody = hlds_eqv_type(_),
+ unexpected($pred, "hlds_eqv_type")
+ )
+ else
+ unexpected($pred, "undefined type")
+ )
+ ;
+ CtorArgType = tuple_type(ArgTypes, _Kind),
+ list.foldl(
+ build_type_param_variance_restrictions_in_ctor_arg_type(TypeTable,
+ CurTypeCtor, CurTypeParams),
+ ArgTypes, !InvariantSet)
+ ;
+ CtorArgType = higher_order_type(_PredOrFunc, ArgTypes, _HOInstInfo,
+ _Purity, _EvalMethod),
+ type_vars_list(ArgTypes, TypeVars),
+ set.insert_list(TypeVars, !InvariantSet)
+ ;
+ CtorArgType = apply_n_type(_, _, _),
+ sorry($pred, "apply_n_type")
+ ;
+ CtorArgType = kinded_type(CtorArgType1, _Kind),
+ build_type_param_variance_restrictions_in_ctor_arg_type(TypeTable,
+ CurTypeCtor, CurTypeParams, CtorArgType1, !InvariantSet)
+ ).
+
+%---------------------%
+
+:- pred check_type_param_variance_restrictions(type_table::in, tvarset::in,
+ invariant_set::in, list(tvar)::in, list(mer_type)::in, list(mer_type)::in)
+ is semidet.
+
+check_type_param_variance_restrictions(TypeTable, TVarSet, InvariantSet,
+ TypeParams, FromTypeArgs, ToTypeArgs) :-
+ (
+ TypeParams = [],
+ FromTypeArgs = [],
+ ToTypeArgs = []
+ ;
+ TypeParams = [TypeVar | TailTypeParams],
+ FromTypeArgs = [FromType | TailFromTypes],
+ ToTypeArgs = [ToType | TailToTypes],
+ check_one_type_param_variance_restriction(TypeTable, TVarSet,
+ InvariantSet, TypeVar, FromType, ToType),
+ check_type_param_variance_restrictions(TypeTable, TVarSet,
+ InvariantSet, TailTypeParams, TailFromTypes, TailToTypes)
+ ).
+
+:- pred check_one_type_param_variance_restriction(type_table::in, tvarset::in,
+ invariant_set::in, tvar::in, mer_type::in, mer_type::in) is semidet.
+
+check_one_type_param_variance_restriction(TypeTable, TVarSet, InvariantSet,
+ TypeVar, FromType, ToType) :-
+ ( if set.contains(InvariantSet, TypeVar) then
+ compare_types(TypeTable, TVarSet, compare_equal, FromType, ToType)
+ else
+ (
+ compare_types(TypeTable, TVarSet, compare_equal_lt,
+ FromType, ToType)
+ ;
+ compare_types(TypeTable, TVarSet, compare_equal_lt,
+ ToType, FromType)
+ )
+ ).
+
+%---------------------%
+
+:- type types_comparison
+ ---> compare_equal
+ ; compare_equal_lt.
+
+ % Succeed if TypeA is the same type as TypeB.
+ % 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) is semidet.
+
+compare_types(TypeTable, TVarSet, Comparison, TypeA, TypeB) :-
+ require_complete_switch [TypeA]
+ (
+ TypeA = builtin_type(BuiltinType),
+ TypeB = builtin_type(BuiltinType)
+ ;
+ TypeA = type_variable(TypeVar, Kind),
+ TypeB = type_variable(TypeVar, Kind)
+ ;
+ TypeA = defined_type(_, _, _),
+ type_to_ctor_and_args(TypeA, TypeCtorA, ArgsA),
+ type_to_ctor_and_args(TypeB, TypeCtorB, ArgsB),
+ ( if TypeCtorA = TypeCtorB then
+ compare_corresponding_types(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_corresponding_types(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_corresponding_types(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_corresponding_types(type_table::in, tvarset::in,
+ types_comparison::in, list(mer_type)::in, list(mer_type)::in) is semidet.
+
+compare_corresponding_types(_TypeTable, _TVarSet, _Comparison, [], []).
+compare_corresponding_types(TypeTable, TVarSet, Comparison,
+ [TypeA | TypesA], [TypeB | TypesB]) :-
+ compare_types(TypeTable, TVarSet, Comparison, TypeA, TypeB),
+ compare_corresponding_types(TypeTable, TVarSet, Comparison,
+ TypesA, TypesB).
+
+%---------------------------------------------------------------------------%
+
+ % Remove satisfied coerce constraints from each type assignment,
+ % then drop any type assignments with unsatisfied coerce constraints
+ % if there is at least one type assignment that does satisfy coerce
+ % constraints.
+ %
+:- pred typecheck_prune_coerce_constraints(type_assign_set::in,
+ type_assign_set::out, typecheck_info::in, typecheck_info::out) is det.
+
+typecheck_prune_coerce_constraints(TypeAssignSet0, TypeAssignSet, !Info) :-
+ typecheck_info_get_type_table(!.Info, TypeTable),
+ list.map(type_assign_prune_coerce_constraints(TypeTable),
+ TypeAssignSet0, TypeAssignSet1),
+ list.filter(type_assign_has_no_coerce_constraints,
+ TypeAssignSet1, SatisfiedTypeAssignSet, UnsatisfiedTypeAssignSet),
+ (
+ SatisfiedTypeAssignSet = [_ | _],
+ TypeAssignSet = SatisfiedTypeAssignSet
+ ;
+ SatisfiedTypeAssignSet = [],
+ TypeAssignSet = UnsatisfiedTypeAssignSet
+ ).
+
+:- pred type_assign_prune_coerce_constraints(type_table::in,
+ type_assign::in, type_assign::out) is det.
+
+type_assign_prune_coerce_constraints(TypeTable, TypeAssign0, TypeAssign) :-
+ type_assign_get_coerce_constraints(TypeAssign0, Coercions0),
+ (
+ Coercions0 = [],
+ TypeAssign = TypeAssign0
+ ;
+ Coercions0 = [_ | _],
+ list.filter(coerce_constraint_is_not_satisfied(TypeTable, TypeAssign0),
+ Coercions0, Coercions),
+ type_assign_set_coerce_constraints(Coercions, TypeAssign0, TypeAssign)
+ ).
+
+:- pred coerce_constraint_is_not_satisfied(type_table::in, type_assign::in,
+ coerce_constraint::in) is semidet.
+
+coerce_constraint_is_not_satisfied(TypeTable, TypeAssign, Coercion) :-
+ check_coerce_constraint(TypeTable, TypeAssign, Coercion, Satisfied),
+ Satisfied = no.
+
+:- pred check_coerce_constraint(type_table::in, type_assign::in,
+ coerce_constraint::in, bool::out) is det.
+
+check_coerce_constraint(TypeTable, TypeAssign, Coercion, Satisfied) :-
+ Coercion = coerce_constraint(FromType0, ToType0, _Context, Status),
+ (
+ Status = need_to_check,
+ type_assign_get_type_bindings(TypeAssign, TypeBindings),
+ type_assign_get_typevarset(TypeAssign, TVarSet),
+ apply_rec_subst_to_type(TypeBindings, FromType0, FromType),
+ apply_rec_subst_to_type(TypeBindings, ToType0, ToType),
+ ( if
+ typecheck_coerce_between_types(TypeTable, TVarSet,
+ FromType, ToType)
+ then
+ Satisfied = yes
+ else
+ Satisfied = no
+ )
+ ;
+ Status = unsatisfiable,
+ Satisfied = no
+ ).
+
+:- pred type_assign_has_no_coerce_constraints(type_assign::in)
+ is semidet.
+
+type_assign_has_no_coerce_constraints(TypeAssign) :-
+ type_assign_get_coerce_constraints(TypeAssign, []).
+
%---------------------------------------------------------------------------%
:- end_module check_hlds.typecheck.
%---------------------------------------------------------------------------%
diff --git a/compiler/typecheck_errors.m b/compiler/typecheck_errors.m
index 8ce5e8bff..7341d99e5 100644
--- a/compiler/typecheck_errors.m
+++ b/compiler/typecheck_errors.m
@@ -179,6 +179,9 @@
:- func report_missing_tvar_in_foreign_code(type_error_clause_context,
prog_context, string) = error_spec.
+:- func report_invalid_coerce_from_to(type_error_clause_context, prog_context,
+ tvarset, mer_type, mer_type) = error_spec.
+
:- pred construct_pred_decl_diff(module_info::in,
list(mer_type)::in, maybe(mer_type)::in, pred_id::in,
list(format_component)::out) is det.
@@ -1989,6 +1992,18 @@ report_missing_tvar_in_foreign_code(ClauseContext, Context, VarName) = Spec :-
%---------------------------------------------------------------------------%
+report_invalid_coerce_from_to(ClauseContext, Context, TVarSet,
+ FromType, ToType) = Spec :-
+ InClauseForPieces = in_clause_for_pieces(ClauseContext),
+ FromTypeStr = mercury_type_to_string(TVarSet, print_num_only, FromType),
+ ToTypeStr = mercury_type_to_string(TVarSet, print_num_only, ToType),
+ Pieces = [words("cannot coerce from"), quote(FromTypeStr),
+ words("to"), quote(ToTypeStr), suffix("."), nl],
+ Msg = simplest_msg(Context, InClauseForPieces ++ Pieces),
+ Spec = error_spec($pred, severity_error, phase_type_check, [Msg]).
+
+%---------------------------------------------------------------------------%
+
:- func types_of_vars_to_pieces(prog_varset, inst_varset, list(prog_var),
type_assign_set) = list(format_component).
diff --git a/compiler/unique_modes.m b/compiler/unique_modes.m
index 4abb5942f..2c25a3025 100644
--- a/compiler/unique_modes.m
+++ b/compiler/unique_modes.m
@@ -610,6 +610,9 @@ unique_modes_check_goal_generic_call(GenericCall, ArgVars, Modes,
% Casts are introduced by the compiler and should be mode correct.
GenericCall = cast(_),
ArgOffset = 0
+ ;
+ GenericCall = coerce,
+ ArgOffset = 0
),
unique_modes_check_call_modes(ArgVars, Modes, ArgOffset, Detism,
CanProcSucceed, !ModeInfo),
diff --git a/compiler/unused_imports.m b/compiler/unused_imports.m
index d3aed3182..0b7b9dd22 100644
--- a/compiler/unused_imports.m
+++ b/compiler/unused_imports.m
@@ -794,6 +794,7 @@ hlds_goal_used_modules(Goal, !UsedModules) :-
( Call = higher_order(_, _, _, _)
; Call = event_call(_)
; Call = cast(_)
+ ; Call = coerce
)
)
;
diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
index 1e7a2557c..2f0a70198 100644
--- a/doc/reference_manual.texi
+++ b/doc/reference_manual.texi
@@ -7083,114 +7083,198 @@ good_example3_univ("bar"::in(bound("bar")), univ("blah")::out).
@c @node Type conversions
@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
+ at c A term may be converted from one type @var{FromType}
+ at c to another type @var{ToType}
+ at c using a type conversion expression of the form:
+ at c
@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 coerce(@var{Term})
@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
+ at c The expression is type-correct iff
+ at c @var{FromType} and @var{ToType} are both discriminated union types,
+ at c and after replacing the principal type constructors with base types
+ at c (@pxref{Subtypes})
+ at c the two types have the same type constructor,
+ at c and the arguments of the common type constructor
+ at c satisfy the type parameter variance restrictions below.
+ at c
+ at c Let @var{FromType} expand out to @samp{base(S1, ..., Sn)}
+ at c and @var{ToType} expand out to @samp{base(T1, ..., Tn)},
+ at c where @samp{base(B1, ..., Bn)} is the common base type,
+ at c and @var{Bi} is the i'th type parameter,
+ at c which is bound to @var{Si} in @var{FromType}
+ at c and @var{Ti} in @var{ToType}.
+ at c
+ at c For each pair of corresponding type arguments,
+ at c one of the following must be true:
+ at c @itemize
@c @item
- at c the input is @samp{X} with type @samp{s}
-
+ at c @samp{Si = Ti}
+ at c if the two types are the same
+ at c
@c @item
- at c the result is @samp{Y} with type @samp{t}
-
+ at c @samp{Si < Ti}
+ at c if @var{Si} is a subtype of @var{Ti},
+ at c according to visible subtype definitions
+ at c
@c @item
- at c @samp{Xi}, @samp{Xf} are the initial and final insts of @samp{X}
-
+ at c @samp{Ti < Si}
+ at c if @var{Ti} is a subtype of @var{Si},
+ at c according to visible subtype definitions
+ at c @end itemize
+ at c
+ at c Otherwise, the coerce expression is not type-correct.
+ at c @c NOTE: we deliberately disallow coercion between arbitrary phantom types.
+ at c
+ at c Furthermore,
+ at c @samp{Si = Ti} must be true
+ at c if @var{Bi} occurs in one or more of these locations
+ at c in the @samp{base/n} type definition:
+ at c
+ at c @itemize
+ at c @item
+ at c in a higher order type
+ at c
+ at c @item
+ at c in a foreign type
+ at c
+ at c @item
+ at c in an abstract type
+ at c
@c @item
- at c @samp{Yi}, @samp{Yf} are the initial and final insts of @samp{Y}
+ at c in a solver type
+ at c
+ at c @item
+ at c in a discriminated union type,
+ at c other than a recursive type of the exact form @samp{base(B1, ..., Bn)}
@c @end itemize
-
+ at c
+ at c @heading Mode checking
+ at c
+ at c Type conversion expressions must also be mode-correct.
+ at c For an expression where:
+ at c
+ at c @itemize @bullet
+ at c @item
+ at c the input has type @samp{s},
+ at c initial inst @var{InitialX},
+ at c and final inst @var{FinalX}
+ at c
+ at c @item
+ at c the result has type @samp{t},
+ at c initial inst @var{InitialY},
+ at c and final inst @var{FinalY}
+ at c @end itemize
+ at c
@c @noindent
- at c the coercion is mode-correct iff:
-
+ at c the type conversion expression is mode-correct iff:
+ at c
@c @itemize @bullet
@c @item
- at c @samp{Xi} is a ground inst
-
+ at c @var{InitialX} is a ground inst
+ at c
@c @item
- at c @samp{Xf = Xi}
-
+ at c @var{InitialY} is free
+ at c
@c @item
- at c @samp{Yi} is free
-
+ at c @var{FinalX} is @var{InitialX} but without uniqueness
+ at c
@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 @var{FinalY} is
+ at c the abstract unification of
+ at c @var{InitialX} and the
+ at c @code{bound} instantiatedness tree derived from @samp{t},
+ at c and @var{FinalY} does not approximate any term
+ at c that is invalid in @samp{t}.
@c @end itemize
-
- at c XXX partial order of insts not used elsewhere in reference manual
-
+ at c
+ at c The @code{bound} instantiatedness tree for @samp{t}
+ at c is derived by producing a @code{bound} node
+ at c containing each possible constructor of @samp{t},
+ at c where the arguments of each bound functor
+ at c are also @code{bound} instantiatedness trees.
+ at c Where a constructor argument type is not a discriminated union or tuple type,
+ at c or if the argument is a recursive node in the type tree,
+ at c the inst of the argument is replaced with @code{ground}.
+ at c
+ at c The abstract unification of two instantiation states
+ at c is the abstract equivalent of the unification on terms.
+ at c It is defined in
+ at c @cite{Precise and Expressive Mode Systems for Typed Logic Programming
+ at c Languages} by David Overton. @xref{[6]}.
+ at c
@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 coercing a ground term from a subtype to a supertype is safe,
+ at c but coercing a term from a supertype to a subtype
+ at c is safe only if
+ at c the inst of the term being coerced
+ at c indicates that the term would also be valid in the subtype.
+ at c
+ at c @heading Examples
+ at c
+ at c Assume we have:
+ at c
@c @example
@c :- type fruit
- at c ---> apple
- at c ; lemon
- at c ; orange.
+ at c ---> apple
+ at c ; lemon
+ at c ; orange.
@c
@c :- type citrus =< fruit
- at c ---> lemon
- at c ; orange.
+ at c ---> lemon
+ at c ; orange.
+ at c @end example
@c
- at c :- inst citrus for fruit/0
- at c ---> lemon
- at c ; orange.
+ at c This function is type and mode-correct:
@c
+ at c @example
@c :- func f1(citrus) = fruit.
@c
- at c f1(X) = coerce(X). % correct
+ at c f1(X) = coerce(X).
+ at c @end example
@c
+ at c This function is type-correct but not mode-correct
+ at c because some @code{fruit}s are not @code{citrus}:
+ at c
+ at c @example
@c :- func f2(fruit) = citrus.
@c
- at c f2(X) = coerce(X). % not mode-correct
+ at c f2(X) = coerce(X). % incorrect
+ at c @end example
+ at c
+ at c This function is mode-correct
+ at c because the initial inst of the input argument
+ at c limits the range of @code{fruit} values
+ at c to those that would also be valid in @code{citrus}:
+ at c
+ at c @example
+ at c :- inst citrus for fruit/0
+ at c ---> lemon
+ at c ; orange.
@c
@c :- func f3(fruit) = citrus.
@c :- mode f3(in(citrus)) = out is det.
@c
- at c f3(X) = coerce(X). % correct
+ at c f3(X) = coerce(X).
+ at c @end example
+ at c
+ at c Finally,
+ at c this function is type-incorrect because
+ at c in the coerce expression,
+ at c the type parameter @var{T} of @code{wrap/1}
+ at c is bound to @code{fruit} in the input type,
+ at c but @code{citrus} in the result type.
+ at c
+ at c @example
+ at c :- type wrap(T)
+ at c ---> wrap(T).
+ at c
+ at c :- func f4(func(fruit) = int) = (func(citrus) = int).
+ at c
+ at c f4(X) = Y :-
+ at c wrap(Y) = coerce(wrap(X)). % incorrect
@c @end example
@c -----------------------------------------------------------------------
@@ -12325,6 +12409,8 @@ 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]
@@ -12365,4 +12451,10 @@ 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/Mercury.options b/tests/invalid/Mercury.options
index 17ad80b89..749c9906f 100644
--- a/tests/invalid/Mercury.options
+++ b/tests/invalid/Mercury.options
@@ -19,6 +19,8 @@ MCFLAGS-bug214 = --allow-stubs --no-warn-stubs
# Mantis bug 238 shows up in bug238.m only with --constraint-propagation.
MCFLAGS-bug238 = --constraint-propagation
MCFLAGS-children = --no-intermodule-optimization
+MCFLAGS-coerce_implied_mode = --halt-at-warn
+MCFLAGS-coerce_infer = --infer-all
MCFLAGS-duplicate_modes = --verbose-error-messages
MCFLAGS-ee_invalid = --verbose-error-messages
MCFLAGS-empty_interface = --halt-at-warn -E
diff --git a/tests/invalid/Mmakefile b/tests/invalid/Mmakefile
index 0a94257c7..bfb45c679 100644
--- a/tests/invalid/Mmakefile
+++ b/tests/invalid/Mmakefile
@@ -116,6 +116,16 @@ SINGLEMODULE= \
circ_type2 \
circ_type3 \
circ_type5 \
+ coerce_ambig \
+ coerce_disambig \
+ coerce_implied_mode \
+ coerce_infer \
+ coerce_instvar \
+ coerce_mode_error \
+ coerce_non_du \
+ coerce_syntax \
+ coerce_type_error \
+ coerce_uniq \
combined_ho_type_inst \
combined_ho_type_inst_2 \
comparison \
diff --git a/tests/invalid/coerce_ambig.err_exp b/tests/invalid/coerce_ambig.err_exp
new file mode 100644
index 000000000..3c45572d9
--- /dev/null
+++ b/tests/invalid/coerce_ambig.err_exp
@@ -0,0 +1,12 @@
+coerce_ambig.m:030: In clause for predicate `ambig1'/0:
+coerce_ambig.m:030: error: ambiguous overloading causes type ambiguity.
+coerce_ambig.m:030: Possible type assignments include:
+coerce_ambig.m:030: X: `coerce_ambig.fruit' or `coerce_ambig.citrus'
+coerce_ambig.m:036: In clause for predicate `ambig2'/0:
+coerce_ambig.m:036: error: ambiguous overloading causes type ambiguity.
+coerce_ambig.m:036: Possible type assignments include:
+coerce_ambig.m:036: X: `coerce_ambig.fruit' or `coerce_ambig.another_fruit'
+coerce_ambig.m:043: In clause for predicate `ambig3'/1:
+coerce_ambig.m:043: cannot coerce from `coerce_ambig.list(V_1)' to
+coerce_ambig.m:043: `coerce_ambig.list(coerce_ambig.fruit)'.
+For more information, recompile with `-E'.
diff --git a/tests/invalid/coerce_ambig.m b/tests/invalid/coerce_ambig.m
new file mode 100644
index 000000000..3bd2b5874
--- /dev/null
+++ b/tests/invalid/coerce_ambig.m
@@ -0,0 +1,45 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module coerce_ambig.
+:- interface.
+
+:- type list(T)
+ ---> []
+ ; [T | list(T)].
+
+:- type fruit
+ ---> apple
+ ; orange
+ ; lemon.
+
+:- type citrus =< fruit
+ ---> orange
+ ; lemon.
+
+:- type another_fruit
+ ---> apple.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- pred ambig1 is semidet.
+
+ambig1 :-
+ X = orange,
+ _Y = coerce(X).
+
+:- pred ambig2 is semidet.
+
+ambig2 :-
+ X = apple,
+ _Y = coerce(X).
+
+:- pred ambig3(list(fruit)::out) is det.
+
+ambig3(Xs) :-
+ Xs = coerce([]).
+
+%---------------------------------------------------------------------------%
diff --git a/tests/invalid/coerce_disambig.err_exp b/tests/invalid/coerce_disambig.err_exp
new file mode 100644
index 000000000..bccd4c09a
--- /dev/null
+++ b/tests/invalid/coerce_disambig.err_exp
@@ -0,0 +1,6 @@
+coerce_disambig.m:037: In clause for `member(out, in)':
+coerce_disambig.m:037: mode mismatch in disjunction.
+coerce_disambig.m:037: The variable `X' is ground in some branches but not
+coerce_disambig.m:037: others.
+coerce_disambig.m:028: In this branch, `X' is free.
+coerce_disambig.m:032: In this branch, `X' is ground.
diff --git a/tests/invalid/coerce_disambig.m b/tests/invalid/coerce_disambig.m
new file mode 100644
index 000000000..5359e551a
--- /dev/null
+++ b/tests/invalid/coerce_disambig.m
@@ -0,0 +1,38 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module coerce_disambig.
+:- interface.
+
+:- type cord(T).
+
+:- pred member(T, cord(T)).
+:- mode member(out, in) is nondet.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module list. % includes list.member/2
+
+:- type nonempty_list(T) =< list(T)
+ ---> [T | list(T)].
+
+:- type cord(T)
+ ---> empty_node
+ ; list_node(nonempty_list(T)).
+
+member(X, Node) :-
+ (
+ Node = empty_node
+ % This branch deliberately does not bind X. We should get a mode
+ % mismatch error instead of any errors about coerce.
+ ;
+ Node = list_node(Xs),
+ % member/2 is ambiguous
+ % but coerce to list(T) is valid
+ % while coerce to cord(T) is invalid
+ % so the user should not need to disambiguate.
+ member(X, coerce(Xs))
+ ).
diff --git a/tests/invalid/coerce_implied_mode.err_exp b/tests/invalid/coerce_implied_mode.err_exp
new file mode 100644
index 000000000..2a9164aa7
--- /dev/null
+++ b/tests/invalid/coerce_implied_mode.err_exp
@@ -0,0 +1,7 @@
+coerce_implied_mode.m:036: In clause for
+coerce_implied_mode.m:036: `coerce_implied_mode3(in(bound(orange)))':
+coerce_implied_mode.m:036: in coerce:
+coerce_implied_mode.m:036: warning: unification of `Y' and `V_4' cannot
+coerce_implied_mode.m:036: succeed.
+coerce_implied_mode.m:036: `Y' has instantiatedness `bound(orange)',
+coerce_implied_mode.m:036: `V_4' has instantiatedness `bound(lemon)'.
diff --git a/tests/invalid/coerce_implied_mode.m b/tests/invalid/coerce_implied_mode.m
new file mode 100644
index 000000000..8dbfb32b8
--- /dev/null
+++ b/tests/invalid/coerce_implied_mode.m
@@ -0,0 +1,38 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module coerce_implied_mode.
+:- interface.
+
+:- type fruit
+ ---> apple
+ ; orange
+ ; lemon.
+
+:- type citrus =< fruit
+ ---> orange
+ ; lemon.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- pred coerce_implied_mode(fruit::in) is semidet.
+
+coerce_implied_mode(Y) :-
+ Y = coerce(orange : citrus).
+
+:- pred coerce_implied_mode2(fruit).
+:- mode coerce_implied_mode2(in(bound(orange))) is det.
+
+coerce_implied_mode2(Y) :-
+ Y = coerce(orange : citrus).
+
+:- pred coerce_implied_mode3(fruit).
+:- mode coerce_implied_mode3(in(bound(orange))) is failure.
+
+coerce_implied_mode3(Y) :-
+ Y = coerce(lemon : citrus).
+
+%---------------------------------------------------------------------------%
diff --git a/tests/invalid/coerce_infer.err_exp b/tests/invalid/coerce_infer.err_exp
new file mode 100644
index 000000000..fd9c0b6b3
--- /dev/null
+++ b/tests/invalid/coerce_infer.err_exp
@@ -0,0 +1,2 @@
+coerce_infer.m:026: In clause for function `f'/1:
+coerce_infer.m:026: cannot coerce from `V_1' to `V_2'.
diff --git a/tests/invalid/coerce_infer.m b/tests/invalid/coerce_infer.m
new file mode 100644
index 000000000..9225f5d97
--- /dev/null
+++ b/tests/invalid/coerce_infer.m
@@ -0,0 +1,26 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module coerce_infer.
+:- interface.
+
+:- type fruit
+ ---> apple
+ ; orange
+ ; lemon.
+
+:- type citrus =< fruit
+ ---> orange
+ ; lemon.
+
+:- func g(citrus) = fruit.
+
+:- implementation.
+
+g(X) = f(X).
+
+% We cannot infer this yet:
+%:- func f(citrus) = fruit.
+
+f(X) = coerce(X).
diff --git a/tests/invalid/coerce_instvar.err_exp b/tests/invalid/coerce_instvar.err_exp
new file mode 100644
index 000000000..3de661e6c
--- /dev/null
+++ b/tests/invalid/coerce_instvar.err_exp
@@ -0,0 +1,19 @@
+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: `coerce_instvar.citrus'.
diff --git a/tests/invalid/coerce_instvar.m b/tests/invalid/coerce_instvar.m
new file mode 100644
index 000000000..4b62b0318
--- /dev/null
+++ b/tests/invalid/coerce_instvar.m
@@ -0,0 +1,43 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module coerce_instvar.
+:- interface.
+
+:- type foobar
+ ---> foo
+ ; bar.
+
+:- type foo =< foobar
+ ---> foo.
+
+:- type fruit
+ ---> apple
+ ; orange
+ ; lemon(foobar).
+
+:- type citrus =< fruit
+ ---> orange
+ ; lemon(foo).
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- pred good(citrus, fruit).
+:- mode good(in(I), out(I)) is det.
+
+good(X, Y) :-
+ Y = coerce(X),
+ (
+ Y = orange
+ ;
+ Y = lemon(foo)
+ ).
+
+:- pred bad(fruit, citrus).
+:- mode bad(in(I), out(I)) is det.
+
+bad(X, Y) :-
+ Y = coerce(X).
diff --git a/tests/invalid/coerce_mode_error.err_exp b/tests/invalid/coerce_mode_error.err_exp
new file mode 100644
index 000000000..8105fbbe1
--- /dev/null
+++ b/tests/invalid/coerce_mode_error.err_exp
@@ -0,0 +1,40 @@
+coerce_mode_error.m:035: In clause for `bad_coerce_free_input(in(free), out)':
+coerce_mode_error.m:035: in coerce:
+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: `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: `coerce_mode_error.list(coerce_mode_error.citrus)'.
diff --git a/tests/invalid/coerce_mode_error.m b/tests/invalid/coerce_mode_error.m
new file mode 100644
index 000000000..37e4fa2d4
--- /dev/null
+++ b/tests/invalid/coerce_mode_error.m
@@ -0,0 +1,54 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module coerce_mode_error.
+:- interface.
+
+:- type list(T)
+ ---> []
+ ; [T | list(T)].
+
+:- type non_empty_list(T) =< list(T)
+ ---> [T | list(T)].
+
+:- type fruit
+ ---> apple
+ ; orange
+ ; lemon.
+
+:- type citrus =< fruit
+ ---> orange
+ ; lemon.
+
+:- inst citrus_fruit for fruit/0
+ ---> orange
+ ; lemon.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- pred bad_coerce_free_input(fruit::free>>free, fruit::out) is det.
+
+bad_coerce_free_input(X, Y) :-
+ Y = coerce(X).
+
+:- pred fruit_to_citrus(fruit, citrus).
+:- mode fruit_to_citrus(in(citrus_fruit), out) is det.
+
+fruit_to_citrus(X, Y) :-
+ Y = coerce(X).
+
+:- pred bad_fruit_to_citrus(fruit::in, citrus::out) is det.
+
+bad_fruit_to_citrus(X, Y) :-
+ Y = coerce(X).
+
+:- pred bad_nelist_f_to_list_c(non_empty_list(fruit), list(citrus)).
+:- mode bad_nelist_f_to_list_c(in, out) is det.
+
+bad_nelist_f_to_list_c(X, Y) :-
+ Y = coerce(X).
+
+%---------------------------------------------------------------------------%
diff --git a/tests/invalid/coerce_non_du.err_exp b/tests/invalid/coerce_non_du.err_exp
new file mode 100644
index 000000000..83e52a357
--- /dev/null
+++ b/tests/invalid/coerce_non_du.err_exp
@@ -0,0 +1,11 @@
+coerce_non_du.m:015: In clause for function `f1'/1:
+coerce_non_du.m:015: cannot coerce from `int' to `int'.
+coerce_non_du.m:019: In clause for function `f2'/1:
+coerce_non_du.m:019: cannot coerce from `float' to `float'.
+coerce_non_du.m:023: In clause for function `f3'/1:
+coerce_non_du.m:023: cannot coerce from `{}' to `{}'.
+coerce_non_du.m:027: In clause for function `f4'/1:
+coerce_non_du.m:027: cannot coerce from `((func int) = int)' to
+coerce_non_du.m:027: `((func int) = int)'.
+coerce_non_du.m:031: In clause for function `f5'/1:
+coerce_non_du.m:031: cannot coerce from `pred(int, int)' to `pred(int, int)'.
diff --git a/tests/invalid/coerce_non_du.m b/tests/invalid/coerce_non_du.m
new file mode 100644
index 000000000..2f6e4cbc4
--- /dev/null
+++ b/tests/invalid/coerce_non_du.m
@@ -0,0 +1,31 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module coerce_non_du.
+:- interface.
+
+:- type dummy_export
+ ---> dummy_export.
+
+:- implementation.
+
+:- func f1(int) = int.
+
+f1(X) = coerce(X).
+
+:- func f2(float) = float.
+
+f2(X) = coerce(X).
+
+:- func f3({}) = {}.
+
+f3(X) = coerce(X).
+
+:- func f4(func(int) = int) = (func(int) = int).
+
+f4(X) = coerce(X).
+
+:- func f5(pred(int, int)) = (pred(int, int)).
+
+f5(X) = coerce(X).
diff --git a/tests/invalid/coerce_syntax.err_exp b/tests/invalid/coerce_syntax.err_exp
new file mode 100644
index 000000000..e4b15d64b
--- /dev/null
+++ b/tests/invalid/coerce_syntax.err_exp
@@ -0,0 +1,8 @@
+coerce_syntax.m:024: In clause for predicate `module_qualify_coerce'/0:
+coerce_syntax.m:024: error: undefined symbol `coerce_syntax.coerce'/1.
+coerce_syntax.m:029: In clause for predicate `apply_coerce'/0:
+coerce_syntax.m:029: in argument 1 of functor `apply/2':
+coerce_syntax.m:029: error: undefined symbol `coerce'/0.
+coerce_syntax.m:034: In clause for predicate `empty_apply_coerce'/0:
+coerce_syntax.m:034: in argument 1 of functor `/2':
+coerce_syntax.m:034: error: undefined symbol `coerce'/0.
diff --git a/tests/invalid/coerce_syntax.m b/tests/invalid/coerce_syntax.m
new file mode 100644
index 000000000..e39c4e528
--- /dev/null
+++ b/tests/invalid/coerce_syntax.m
@@ -0,0 +1,50 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module coerce_syntax.
+:- interface.
+
+:- type fruit
+ ---> apple
+ ; orange
+ ; lemon.
+
+:- type citrus =< fruit
+ ---> orange
+ ; lemon.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- pred module_qualify_coerce is det.
+
+module_qualify_coerce :-
+ _ = coerce_syntax.coerce(1).
+
+:- pred apply_coerce is det.
+
+apply_coerce :-
+ _ = apply(coerce, 1).
+
+:- pred empty_apply_coerce is det.
+
+empty_apply_coerce :-
+ _ = (coerce)(1).
+
+:- pred coerce_in_head_var(citrus::in, fruit::out) is det.
+
+coerce_in_head_var(X, coerce(X)).
+
+:- pred coerce_in_head_functor(citrus::in, fruit::out) is det.
+
+coerce_in_head_functor(_, coerce(orange : citrus)).
+
+:- func coerce_in_function_arg(citrus) = fruit is semidet.
+
+coerce_in_function_arg(coerce(apple)) = orange.
+
+:- func coerce_in_function_result(citrus) = fruit.
+
+coerce_in_function_result(X) = coerce(X).
diff --git a/tests/invalid/coerce_type_error.err_exp b/tests/invalid/coerce_type_error.err_exp
new file mode 100644
index 000000000..bafabaa89
--- /dev/null
+++ b/tests/invalid/coerce_type_error.err_exp
@@ -0,0 +1,22 @@
+coerce_type_error.m:045: In clause for predicate `bad_unrelated'/2:
+coerce_type_error.m:045: cannot coerce from
+coerce_type_error.m:045: `coerce_type_error.orange_non_fruit' to
+coerce_type_error.m:045: `coerce_type_error.citrus'.
+coerce_type_error.m:070: In clause for predicate `bad_phantom'/2:
+coerce_type_error.m:070: cannot coerce from `coerce_type_error.phantom(int)'
+coerce_type_error.m:070: to `coerce_type_error.phantom(float)'.
+coerce_type_error.m:091: In clause for predicate `bad_higher_order'/2:
+coerce_type_error.m:091: cannot coerce from
+coerce_type_error.m:091: `coerce_type_error.wrap_ho(coerce_type_error.citrus)'
+coerce_type_error.m:091: to
+coerce_type_error.m:091: `coerce_type_error.wrap_ho(coerce_type_error.fruit)'.
+coerce_type_error.m:106: In clause for predicate `bad_foreign_type'/2:
+coerce_type_error.m:106: cannot coerce from
+coerce_type_error.m:106: `coerce_type_error.wrap_ft(coerce_type_error.citrus)'
+coerce_type_error.m:106: to
+coerce_type_error.m:106: `coerce_type_error.wrap_ft(coerce_type_error.fruit)'.
+coerce_type_error.m:118: In clause for predicate `bad_abs_type'/2:
+coerce_type_error.m:118: cannot coerce from
+coerce_type_error.m:118: `coerce_type_error.wrap_abs(coerce_type_error.citrus)'
+coerce_type_error.m:118: to
+coerce_type_error.m:118: `coerce_type_error.wrap_abs(coerce_type_error.fruit)'.
diff --git a/tests/invalid/coerce_type_error.m b/tests/invalid/coerce_type_error.m
new file mode 100644
index 000000000..2da9b77af
--- /dev/null
+++ b/tests/invalid/coerce_type_error.m
@@ -0,0 +1,120 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module coerce_type_error.
+:- interface.
+
+:- import_module list.
+
+:- type non_empty_list(T) =< list(T)
+ ---> [T | list(T)].
+
+:- type fruit
+ ---> apple
+ ; orange
+ ; lemon.
+
+:- type citrus =< fruit
+ ---> orange
+ ; lemon.
+
+:- type orange_fruit =< fruit
+ ---> orange.
+
+:- type orange_non_fruit
+ ---> orange.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- pred citrus_to_fruit(citrus::in, fruit::out) is det.
+
+citrus_to_fruit(X, Y) :-
+ Y = coerce(X).
+
+:- pred orange_fruit_to_citrus(orange_fruit::in, citrus::out) is det.
+
+orange_fruit_to_citrus(X, Y) :-
+ Y = coerce(X).
+
+:- pred bad_unrelated(orange_non_fruit::in, citrus::out) is det.
+
+bad_unrelated(X, Y) :-
+ Y = coerce(X).
+
+:- pred list_to_list(list(citrus)::in, list(fruit)::out) is det.
+
+list_to_list(X, Y) :-
+ Y = coerce(X).
+
+%---------------------------------------------------------------------------%
+
+:- type fruit2 == fruit.
+:- type citrus2 == citrus.
+
+:- pred citrus_to_fruit2(citrus2::in, fruit2::out) is det.
+
+citrus_to_fruit2(X, Y) :-
+ Y = coerce(X).
+
+%---------------------------------------------------------------------------%
+
+:- type phantom(T)
+ ---> phantom.
+
+:- pred bad_phantom(phantom(int)::in, phantom(float)::out) is det.
+
+bad_phantom(X, Y) :-
+ Y = coerce(X).
+
+%---------------------------------------------------------------------------%
+
+:- type wrap(T)
+ ---> nil
+ ; wrap(T, {T, wrap(T)}).
+
+:- pred wrap_to_wrap(wrap(citrus)::in, wrap(fruit)::out) is det.
+
+wrap_to_wrap(X, Y) :-
+ Y = coerce(X).
+
+%---------------------------------------------------------------------------%
+
+:- type wrap_ho(T)
+ ---> wrap_ho(pred(T)).
+
+:- pred bad_higher_order(wrap_ho(citrus)::in, wrap_ho(fruit)::out) is det.
+
+bad_higher_order(X, Y) :-
+ Y = coerce(X).
+
+%---------------------------------------------------------------------------%
+
+:- type wrap_ft(T)
+ ---> wrap_ft(ft(T)).
+
+:- type ft(T).
+:- pragma foreign_type("C", ft(T), "int").
+:- pragma foreign_type("C#", ft(T), "int").
+:- pragma foreign_type("Java", ft(T), "int").
+
+:- pred bad_foreign_type(wrap_ft(citrus)::in, wrap_ft(fruit)::out) is det.
+
+bad_foreign_type(X, Y) :-
+ Y = coerce(X).
+
+%---------------------------------------------------------------------------%
+
+:- import_module set.
+
+:- type wrap_abs(T)
+ ---> wrap_abs(set(T)).
+
+:- pred bad_abs_type(wrap_abs(citrus)::in, wrap_abs(fruit)::out) is det.
+
+bad_abs_type(X, Y) :-
+ Y = coerce(X).
+
+%---------------------------------------------------------------------------%
diff --git a/tests/invalid/coerce_uniq.err_exp b/tests/invalid/coerce_uniq.err_exp
new file mode 100644
index 000000000..94aa907e5
--- /dev/null
+++ b/tests/invalid/coerce_uniq.err_exp
@@ -0,0 +1,12 @@
+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: expected final instantiatedness was `unique'.
+coerce_uniq.m:029: In clause for `coerce_di(di, uo)':
+coerce_uniq.m:029: mode error: argument 2 did not get sufficiently
+coerce_uniq.m:029: instantiated.
+coerce_uniq.m:029: Final instantiatedness of `Y' was
+coerce_uniq.m:029: `bound(apple ; lemon ; orange)',
+coerce_uniq.m:029: expected final instantiatedness was `unique'.
diff --git a/tests/invalid/coerce_uniq.m b/tests/invalid/coerce_uniq.m
new file mode 100644
index 000000000..244afb859
--- /dev/null
+++ b/tests/invalid/coerce_uniq.m
@@ -0,0 +1,36 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module coerce_uniq.
+:- interface.
+
+:- type fruit
+ ---> apple
+ ; orange
+ ; lemon.
+
+:- type citrus =< fruit
+ ---> orange
+ ; lemon.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- pred coerce_ui(fruit::ui, fruit::out) is det.
+
+coerce_ui(X, Y) :-
+ Y = coerce(X).
+
+:- pred coerce_di(fruit::di, fruit::uo) is det.
+
+coerce_di(X, Y) :-
+ Y = coerce(X).
+
+:- pred coerce_become_shared(fruit::unique>>ground, fruit::out) is det.
+
+coerce_become_shared(X, Y) :-
+ Y = coerce(X).
+
+%---------------------------------------------------------------------------%
diff --git a/tests/invalid/coerce_unreachable.err_exp b/tests/invalid/coerce_unreachable.err_exp
new file mode 100644
index 000000000..55c0cac24
--- /dev/null
+++ b/tests/invalid/coerce_unreachable.err_exp
@@ -0,0 +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: `coerce_unreachable.citrus'.
+For more information, recompile with `-E'.
diff --git a/tests/invalid/coerce_unreachable.m b/tests/invalid/coerce_unreachable.m
new file mode 100644
index 000000000..b58678578
--- /dev/null
+++ b/tests/invalid/coerce_unreachable.m
@@ -0,0 +1,41 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module coerce_unreachable.
+:- interface.
+
+:- type fruit
+ ---> apple
+ ; orange
+ ; lemon.
+
+:- type citrus =< fruit
+ ---> orange
+ ; lemon.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module exception.
+
+:- pred p1(fruit::in, citrus::out) is det.
+
+p1(X, Y) :-
+ % This coercion is invalid.
+ Y = coerce(X),
+ ( if Y = orange then
+ true
+ else
+ throw(apple)
+ ).
+
+:- pred p2(fruit::in, citrus::out) is erroneous.
+
+p2(X, Y) :-
+ % This coercion is invalid, but can be moved after the exception is thrown.
+ Y = coerce(X),
+ throw(apple).
+
+%---------------------------------------------------------------------------%
diff --git a/tests/typeclasses/arbitrary_constraint_class.m b/tests/typeclasses/arbitrary_constraint_class.m
index ec54a703a..5985a9bca 100644
--- a/tests/typeclasses/arbitrary_constraint_class.m
+++ b/tests/typeclasses/arbitrary_constraint_class.m
@@ -31,7 +31,7 @@
mg(S0, S) :-
( semidet_succeed ->
- S = coerce(0.0)
+ S = (coerce)(0.0)
;
S = S0
).
diff --git a/tests/typeclasses/arbitrary_constraint_pred_1.m b/tests/typeclasses/arbitrary_constraint_pred_1.m
index 288172360..969292c31 100644
--- a/tests/typeclasses/arbitrary_constraint_pred_1.m
+++ b/tests/typeclasses/arbitrary_constraint_pred_1.m
@@ -27,7 +27,7 @@
mg(S0, S) :-
( semidet_succeed ->
- S = coerce(0.0)
+ S = (coerce)(0.0)
;
S = S0
).
diff --git a/tests/typeclasses/arbitrary_constraint_pred_2.m b/tests/typeclasses/arbitrary_constraint_pred_2.m
index 262f55ab9..9de69d9c4 100644
--- a/tests/typeclasses/arbitrary_constraint_pred_2.m
+++ b/tests/typeclasses/arbitrary_constraint_pred_2.m
@@ -27,7 +27,7 @@
mg(S0, S) :-
( semidet_succeed ->
- S = coerce([S0])
+ S = (coerce)([S0])
;
S = S0
).
--
2.30.0
More information about the reviews
mailing list