[m-rev.] for review: Parse and check coerce expressions.
Peter Wang
novalazy at gmail.com
Thu Mar 11 11:17:51 AEDT 2021
On Wed, 10 Mar 2021 14:40:33 +1100 Peter Wang <novalazy at gmail.com> wrote:
> 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.
>
Consider the following diff to be part of the previous change.
It allows the predicates in the coerce_unify_tvars.m test case (below)
to typecheck, and prevents an abort in the mode checker.
Peter
diff --git a/compiler/modecheck_coerce.m b/compiler/modecheck_coerce.m
index 1fba5db9f..f445003a0 100644
--- a/compiler/modecheck_coerce.m
+++ b/compiler/modecheck_coerce.m
@@ -196,7 +196,8 @@ make_bound_inst_for_type(ModuleInfo, Seen0, Type, Inst) :-
),
Inst = bound(shared, InstResults, BoundInsts)
else
- unexpected($pred, "type_constructors fail")
+ % Type with no definition, e.g. void
+ Inst = ground_inst
)
else
% Does typed_ground help?
diff --git a/compiler/typecheck.m b/compiler/typecheck.m
index ee1f7cb6f..ef5bf2280 100644
--- a/compiler/typecheck.m
+++ b/compiler/typecheck.m
@@ -2907,9 +2907,9 @@ typecheck_coerce_2(Context, FromVar, ToVar, TypeAssign0,
typecheck_info_get_type_table(!.Info, TypeTable),
( if
typecheck_coerce_between_types(TypeTable, TVarSet,
- FromType, ToType)
+ FromType, ToType, TypeAssign0, TypeAssign1)
then
- TypeAssign = TypeAssign0
+ TypeAssign = TypeAssign1
else
type_assign_get_coerce_constraints(TypeAssign0, Coercions0),
Coercion = coerce_constraint(FromType, ToType, Context,
@@ -3725,9 +3725,11 @@ convert_cons_defn(Info, GoalId, Action, HLDS_ConsDefn, ConsTypeInfo) :-
%---------------------------------------------------------------------------%
:- pred typecheck_coerce_between_types(type_table::in, tvarset::in,
- mer_type::in, mer_type::in) is semidet.
+ mer_type::in, mer_type::in, type_assign::in, type_assign::out)
+ is semidet.
-typecheck_coerce_between_types(TypeTable, TVarSet, FromType, ToType) :-
+typecheck_coerce_between_types(TypeTable, TVarSet, FromType, ToType,
+ !TypeAssign) :-
% Type bindings must have been aplpied to FromType and ToType already.
replace_principal_type_ctor_with_base(TypeTable, TVarSet,
FromType, FromBaseType),
@@ -3745,8 +3747,8 @@ typecheck_coerce_between_types(TypeTable, TVarSet, FromType, ToType) :-
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).
+ check_coerce_type_params(TypeTable, TVarSet, InvariantSet,
+ BaseTypeParams, FromBaseTypeArgs, ToBaseTypeArgs, !TypeAssign).
:- pred replace_principal_type_ctor_with_base(type_table::in, tvarset::in,
mer_type::in, mer_type::out) is det.
@@ -3898,12 +3900,12 @@ build_type_param_variance_restrictions_in_ctor_arg_type(TypeTable, CurTypeCtor,
%---------------------%
-:- 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.
+:- pred check_coerce_type_params(type_table::in, tvarset::in,
+ invariant_set::in, list(tvar)::in, list(mer_type)::in, list(mer_type)::in,
+ type_assign::in, type_assign::out) is semidet.
-check_type_param_variance_restrictions(TypeTable, TVarSet, InvariantSet,
- TypeParams, FromTypeArgs, ToTypeArgs) :-
+check_coerce_type_params(TypeTable, TVarSet, InvariantSet,
+ TypeParams, FromTypeArgs, ToTypeArgs, !TypeAssign) :-
(
TypeParams = [],
FromTypeArgs = [],
@@ -3912,26 +3914,30 @@ check_type_param_variance_restrictions(TypeTable, TVarSet, InvariantSet,
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)
+ check_coerce_type_param(TypeTable, TVarSet, InvariantSet,
+ TypeVar, FromType, ToType, !TypeAssign),
+ check_coerce_type_params(TypeTable, TVarSet, InvariantSet,
+ TailTypeParams, TailFromTypes, TailToTypes, !TypeAssign)
).
-:- 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.
+:- pred check_coerce_type_param(type_table::in, tvarset::in, invariant_set::in,
+ tvar::in, mer_type::in, mer_type::in, type_assign::in, type_assign::out)
+ is semidet.
-check_one_type_param_variance_restriction(TypeTable, TVarSet, InvariantSet,
- TypeVar, FromType, ToType) :-
+check_coerce_type_param(TypeTable, TVarSet, InvariantSet,
+ TypeVar, FromType, ToType, !TypeAssign) :-
( if set.contains(InvariantSet, TypeVar) then
- compare_types(TypeTable, TVarSet, compare_equal, FromType, ToType)
+ compare_types(TypeTable, TVarSet, compare_equal, FromType, ToType,
+ !TypeAssign)
else
- (
+ ( if
compare_types(TypeTable, TVarSet, compare_equal_lt,
- FromType, ToType)
- ;
+ FromType, ToType, !TypeAssign)
+ then
+ true
+ else
compare_types(TypeTable, TVarSet, compare_equal_lt,
- ToType, FromType)
+ ToType, FromType, !TypeAssign)
)
).
@@ -3941,64 +3947,87 @@ check_one_type_param_variance_restriction(TypeTable, TVarSet, InvariantSet,
---> compare_equal
; compare_equal_lt.
- % Succeed if TypeA is the same type as TypeB.
+ % Succeed if TypeA unifies with TypeB (possibly binding type vars).
% 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.
+:- pred compare_types(type_table::in, tvarset::in,
+ types_comparison::in, mer_type::in, mer_type::in,
+ type_assign::in, type_assign::out) is semidet.
-compare_types(TypeTable, TVarSet, Comparison, TypeA, TypeB) :-
+compare_types(TypeTable, TVarSet, Comparison, TypeA, TypeB,
+ !TypeAssign) :-
+ ( if
+ ( TypeA = type_variable(_, _)
+ ; TypeB = type_variable(_, _)
+ )
+ then
+ type_assign_unify_type(TypeA, TypeB, !TypeAssign)
+ else
+ compare_types_nonvar(TypeTable, TVarSet, Comparison, TypeA, TypeB,
+ !TypeAssign)
+ ).
+
+:- pred compare_types_nonvar(type_table::in, tvarset::in, types_comparison::in,
+ mer_type::in, mer_type::in, type_assign::in, type_assign::out) is semidet.
+
+compare_types_nonvar(TypeTable, TVarSet, Comparison, TypeA, TypeB,
+ !TypeAssign) :-
require_complete_switch [TypeA]
(
TypeA = builtin_type(BuiltinType),
TypeB = builtin_type(BuiltinType)
;
- TypeA = type_variable(TypeVar, Kind),
- TypeB = type_variable(TypeVar, Kind)
+ TypeA = type_variable(_, _),
+ TypeB = type_variable(_, _),
+ unexpected($pred, "type_variable")
;
TypeA = defined_type(_, _, _),
type_to_ctor_and_args(TypeA, TypeCtorA, ArgsA),
type_to_ctor_and_args(TypeB, TypeCtorB, ArgsB),
( if TypeCtorA = TypeCtorB then
- compare_corresponding_types(TypeTable, TVarSet, Comparison,
- ArgsA, ArgsB)
+ compare_types_corresponding(TypeTable, TVarSet, Comparison,
+ ArgsA, ArgsB, !TypeAssign)
else
Comparison = compare_equal_lt,
get_supertype(TypeTable, TVarSet, TypeCtorA, ArgsA, SuperTypeA),
- compare_types(TypeTable, TVarSet, Comparison, SuperTypeA, TypeB)
+ compare_types(TypeTable, TVarSet, Comparison, SuperTypeA, TypeB,
+ !TypeAssign)
)
;
TypeA = tuple_type(ArgsA, Kind),
TypeB = tuple_type(ArgsB, Kind),
- compare_corresponding_types(TypeTable, TVarSet, Comparison,
- ArgsA, ArgsB)
+ compare_types_corresponding(TypeTable, TVarSet, Comparison,
+ ArgsA, ArgsB, !TypeAssign)
;
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)
+ compare_types_corresponding(TypeTable, TVarSet, compare_equal,
+ ArgsA, ArgsB, !TypeAssign)
;
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)
+ compare_types(TypeTable, TVarSet, Comparison, TypeA1, TypeB1,
+ !TypeAssign)
).
-:- pred compare_corresponding_types(type_table::in, tvarset::in,
- types_comparison::in, list(mer_type)::in, list(mer_type)::in) is semidet.
+:- pred compare_types_corresponding(type_table::in, tvarset::in,
+ types_comparison::in, list(mer_type)::in, list(mer_type)::in,
+ type_assign::in, type_assign::out) 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).
+compare_types_corresponding(_TypeTable, _TVarSet, _Comparison,
+ [], [], !TypeAssign).
+compare_types_corresponding(TypeTable, TVarSet, Comparison,
+ [TypeA | TypesA], [TypeB | TypesB], !TypeAssign) :-
+ compare_types(TypeTable, TVarSet, Comparison, TypeA, TypeB, !TypeAssign),
+ compare_types_corresponding(TypeTable, TVarSet, Comparison, TypesA, TypesB,
+ !TypeAssign).
%---------------------------------------------------------------------------%
@@ -4027,41 +4056,52 @@ typecheck_prune_coerce_constraints(TypeAssignSet0, TypeAssignSet, !Info) :-
:- 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),
+type_assign_prune_coerce_constraints(TypeTable, !TypeAssign) :-
+ type_assign_get_coerce_constraints(!.TypeAssign, Coercions0),
(
- Coercions0 = [],
- TypeAssign = TypeAssign0
+ Coercions0 = []
;
Coercions0 = [_ | _],
- list.filter(coerce_constraint_is_not_satisfied(TypeTable, TypeAssign0),
- Coercions0, Coercions),
- type_assign_set_coerce_constraints(Coercions, TypeAssign0, TypeAssign)
+ check_and_drop_coerce_constraints(TypeTable, Coercions0, Coercions,
+ !TypeAssign),
+ type_assign_set_coerce_constraints(Coercions, !TypeAssign)
).
-:- pred coerce_constraint_is_not_satisfied(type_table::in, type_assign::in,
- coerce_constraint::in) is semidet.
+:- pred check_and_drop_coerce_constraints(type_table::in,
+ list(coerce_constraint)::in, list(coerce_constraint)::out,
+ type_assign::in, type_assign::out) is det.
-coerce_constraint_is_not_satisfied(TypeTable, TypeAssign, Coercion) :-
- check_coerce_constraint(TypeTable, TypeAssign, Coercion, Satisfied),
- Satisfied = no.
+check_and_drop_coerce_constraints(_TypeTable, [], [], !TypeAssign).
+check_and_drop_coerce_constraints(TypeTable, [Coercion0 | Coercions0],
+ KeepCoercions, !TypeAssign) :-
+ check_coerce_constraint(TypeTable, Coercion0, !.TypeAssign, Satisfied),
+ (
+ Satisfied = yes(!:TypeAssign),
+ check_and_drop_coerce_constraints(TypeTable, Coercions0,
+ KeepCoercions, !TypeAssign)
+ ;
+ Satisfied = no,
+ check_and_drop_coerce_constraints(TypeTable, Coercions0,
+ TailKeepCoercions, !TypeAssign),
+ KeepCoercions = [Coercion0 | TailKeepCoercions]
+ ).
-:- pred check_coerce_constraint(type_table::in, type_assign::in,
- coerce_constraint::in, bool::out) is det.
+:- pred check_coerce_constraint(type_table::in, coerce_constraint::in,
+ type_assign::in, maybe(type_assign)::out) is det.
-check_coerce_constraint(TypeTable, TypeAssign, Coercion, Satisfied) :-
+check_coerce_constraint(TypeTable, Coercion, TypeAssign0, 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),
+ type_assign_get_type_bindings(TypeAssign0, TypeBindings),
+ type_assign_get_typevarset(TypeAssign0, 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)
+ FromType, ToType, TypeAssign0, TypeAssign)
then
- Satisfied = yes
+ Satisfied = yes(TypeAssign)
else
Satisfied = no
)
diff --git a/tests/invalid/Mercury.options b/tests/invalid/Mercury.options
index 749c9906f..a0c5957aa 100644
--- a/tests/invalid/Mercury.options
+++ b/tests/invalid/Mercury.options
@@ -21,6 +21,7 @@ MCFLAGS-bug238 = --constraint-propagation
MCFLAGS-children = --no-intermodule-optimization
MCFLAGS-coerce_implied_mode = --halt-at-warn
MCFLAGS-coerce_infer = --infer-all
+MCFLAGS-coerce_void = --halt-at-warn
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 bfb45c679..a44eb7bdd 100644
--- a/tests/invalid/Mmakefile
+++ b/tests/invalid/Mmakefile
@@ -125,7 +125,9 @@ SINGLEMODULE= \
coerce_non_du \
coerce_syntax \
coerce_type_error \
+ coerce_unify_tvars \
coerce_uniq \
+ coerce_void \
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
index 3c45572d9..c2982376e 100644
--- a/tests/invalid/coerce_ambig.err_exp
+++ b/tests/invalid/coerce_ambig.err_exp
@@ -6,7 +6,4 @@ 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
index 3bd2b5874..d8456f7d9 100644
--- a/tests/invalid/coerce_ambig.m
+++ b/tests/invalid/coerce_ambig.m
@@ -40,6 +40,7 @@ ambig2 :-
:- pred ambig3(list(fruit)::out) is det.
ambig3(Xs) :-
+ % Not ambiguous after we unify list(_T) with list(fruit).
Xs = coerce([]).
%---------------------------------------------------------------------------%
diff --git a/tests/invalid/coerce_unify_tvars.err_exp b/tests/invalid/coerce_unify_tvars.err_exp
new file mode 100644
index 000000000..a7c72387f
--- /dev/null
+++ b/tests/invalid/coerce_unify_tvars.err_exp
@@ -0,0 +1,3 @@
+coerce_unify_tvars.m:061: In clause for predicate `head_type_params'/2:
+coerce_unify_tvars.m:061: cannot coerce from `list.list(V_1)' to
+coerce_unify_tvars.m:061: `list.list(V_2)'.
diff --git a/tests/invalid/coerce_unify_tvars.m b/tests/invalid/coerce_unify_tvars.m
new file mode 100644
index 000000000..a64a805aa
--- /dev/null
+++ b/tests/invalid/coerce_unify_tvars.m
@@ -0,0 +1,61 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module coerce_unify_tvars.
+:- interface.
+
+:- import_module list.
+
+:- type one_or_more(T) =< list(T)
+ ---> [T | list(T)].
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module require.
+
+:- pred append(one_or_more(T), one_or_more(T), one_or_more(T)).
+:- mode append(in, in, out) is det.
+
+append(OoMA, OoMB, OoMC) :-
+ LA = coerce(OoMA),
+ LB = coerce(OoMB),
+ list.append(LA, LB, LC),
+ (
+ LC = [],
+ unexpected($pred, "empty list")
+ ;
+ LC = [_ | _],
+ OoMC = coerce(LC)
+ ).
+
+:- pred length(one_or_more(T)::in, int::out) is det.
+
+length(OoM, Length) :-
+ L = coerce(OoM),
+ list.length(L, Length).
+
+:- pred same_length(one_or_more(T1)::in, one_or_more(T2)::in) is semidet.
+
+same_length(A, B) :-
+ LA = coerce(A),
+ LB = coerce(B),
+ list.same_length(LA, LB).
+
+:- pred same_length2(one_or_more(T1)::in, one_or_more({T2})::in) is semidet.
+
+same_length2(A, B) :-
+ LA = coerce(A),
+ LB = coerce(B),
+ list.same_length(LA, LB).
+
+%---------------------------------------------------------------------------%
+
+ % Obviously the two head type parameters cannot be unified.
+ % This test is mainly just to force an error in this module.
+ %
+:- pred head_type_params(list(T1)::in, list(T2)::in) is semidet.
+
+head_type_params(X, coerce(X)).
diff --git a/tests/invalid/coerce_void.err_exp b/tests/invalid/coerce_void.err_exp
new file mode 100644
index 000000000..d7945c636
--- /dev/null
+++ b/tests/invalid/coerce_void.err_exp
@@ -0,0 +1,8 @@
+coerce_void.m:010: In predicate `main'/2:
+coerce_void.m:010: warning: unresolved polymorphism.
+coerce_void.m:010: The variables with unbound types were:
+coerce_void.m:010: V_8: list.list(T)
+coerce_void.m:010: List: list.list(T)
+coerce_void.m:010: The unbound type variables will be implicitly bound to the
+coerce_void.m:010: builtin type `void'.
+For more information, recompile with `-E'.
diff --git a/tests/invalid/coerce_void.m b/tests/invalid/coerce_void.m
new file mode 100644
index 000000000..75b85ea18
--- /dev/null
+++ b/tests/invalid/coerce_void.m
@@ -0,0 +1,20 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+
+:- module coerce_void.
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module list.
+
+main(!IO) :-
+ List = coerce([]) : list(T),
+ io.print_line(List, !IO).
More information about the reviews
mailing list