diff --git a/compiler/type_assign.m b/compiler/type_assign.m index 309d618e3..fc5d85e7c 100644 --- a/compiler/type_assign.m +++ b/compiler/type_assign.m @@ -142,6 +142,11 @@ dta_from_type :: arity, dta_to_type :: arity ) + ; du_type_is_not_subtype( + % The type is a du type with this type_ctor, but this type + % is not a subtype of anything. + ns_type_ctor :: type_ctor + ) ; cannot_unify_type_vars( % One or both of these will be a type_variable. cutv_from_type :: mer_type, diff --git a/compiler/typecheck_coerce.m b/compiler/typecheck_coerce.m index 3d656e2a6..4c0a9ab5c 100644 --- a/compiler/typecheck_coerce.m +++ b/compiler/typecheck_coerce.m @@ -65,6 +65,7 @@ :- import_module mdbcomp. :- import_module mdbcomp.prim_data. :- import_module mdbcomp.sym_name. +:- import_module parse_tree.maybe_error. :- import_module parse_tree.prog_type. :- import_module parse_tree.prog_type_scan. :- import_module parse_tree.prog_type_subst. @@ -380,25 +381,13 @@ typecheck_coerce_between_types(TypeTable, TVarSet, FromType, ToType, % Type bindings must have been applied to FromType and ToType already. classify_is_du_type(TypeTable, FromType, FromMaybeDuType), classify_is_du_type(TypeTable, ToType, ToMaybeDuType), + are_both_types_du(FromType, ToType, FromMaybeDuType, ToMaybeDuType, + MaybeBoth), ( - FromMaybeDuType = is_not_du_type(FromTypeDesc), - ToMaybeDuType = is_not_du_type(ToTypeDesc), - CoerceFail = non_du_type_ctor(FromType, FromTypeDesc, - ToType, ToTypeDesc), + MaybeBoth = error2(CoerceFail), CoerceFails = [CoerceFail] ; - FromMaybeDuType = is_not_du_type(FromTypeDesc), - ToMaybeDuType = is_du_type(_), - CoerceFail = non_du_type_ctor(FromType, FromTypeDesc, ToType, ""), - CoerceFails = [CoerceFail] - ; - FromMaybeDuType = is_du_type(_), - ToMaybeDuType = is_not_du_type(ToTypeDesc), - CoerceFail = non_du_type_ctor(FromType, "", ToType, ToTypeDesc), - CoerceFails = [CoerceFail] - ; - FromMaybeDuType = is_du_type(FromDuTypeInfo), - ToMaybeDuType = is_du_type(ToDuTypeInfo), + MaybeBoth = ok2(FromDuTypeInfo, ToDuTypeInfo), compute_base_type_of_du_type(TypeTable, TVarSet, FromDuTypeInfo, FromBaseTypeInfo), compute_base_type_of_du_type(TypeTable, TVarSet, @@ -434,6 +423,34 @@ typecheck_coerce_between_types(TypeTable, TVarSet, FromType, ToType, ) ). +:- pred are_both_types_du(mer_type::in, mer_type::in, + maybe_du_type::in, maybe_du_type::in, + maybe2(du_type_info, du_type_info, coerce_fail)::out) is det. + +are_both_types_du(FromType, ToType, FromMaybeDuType, ToMaybeDuType, + MaybeBoth) :- + ( + FromMaybeDuType = is_not_du_type(FromTypeDesc), + ToMaybeDuType = is_not_du_type(ToTypeDesc), + CoerceFail = non_du_type_ctor(FromType, FromTypeDesc, + ToType, ToTypeDesc), + MaybeBoth = error2(CoerceFail) + ; + FromMaybeDuType = is_not_du_type(FromTypeDesc), + ToMaybeDuType = is_du_type(_), + CoerceFail = non_du_type_ctor(FromType, FromTypeDesc, ToType, ""), + MaybeBoth = error2(CoerceFail) + ; + FromMaybeDuType = is_du_type(_), + ToMaybeDuType = is_not_du_type(ToTypeDesc), + CoerceFail = non_du_type_ctor(FromType, "", ToType, ToTypeDesc), + MaybeBoth = error2(CoerceFail) + ; + FromMaybeDuType = is_du_type(FromDuTypeInfo), + ToMaybeDuType = is_du_type(ToDuTypeInfo), + MaybeBoth = ok2(FromDuTypeInfo, ToDuTypeInfo) + ). + %---------------------------------------------------------------------------% :- pred compute_base_type_of_du_type(type_table::in, tvarset::in, @@ -710,7 +727,22 @@ are_actual_param_type_pair_as_related_as_needed(TypeTable, TVarSet, ; FromToCoerceFails = [_ | _], types_compare_as_given(TypeTable, TVarSet, compare_equal_lt, - ToType, FromType, !TypeAssign, !CoerceFails) + ToType, FromType, !.TypeAssign, ToFromTypeAssign, + [], ToFromCoerceFails), + ( + ToFromCoerceFails = [], + !:TypeAssign = ToFromTypeAssign + ; + ToFromCoerceFails = [_ | _], + % NOTE Adding both FromToCoerceFails and ToFromCoerceFails + % to !CoerceFails can report the same issue twice, with + % the roles of coerce-from type and coerce-to type reversed + % for any symmetrical problem that types_compare_as_given + % can report. This is ok, because report_invalid_coerce_from_to + % will ensure that we report just one copy in each such pair. + !:CoerceFails = FromToCoerceFails ++ ToFromCoerceFails + ++ !.CoerceFails + ) ) ). @@ -757,6 +789,8 @@ types_compare_as_given(TypeTable, TVarSet, Comparison, TypeA, TypeB, types_compare_as_given_nonvar(TypeTable, TVarSet, Comparison, TypeA, TypeB, !TypeAssign, !CoerceFails) :- + % Several of the kinds of coerce_fails that the code below can generate + % are NOT TESTED by any test case in the test suite. require_complete_switch [TypeA] ( TypeA = builtin_type(BuiltinTypeA), @@ -780,31 +814,68 @@ types_compare_as_given_nonvar(TypeTable, TVarSet, Comparison, defined_type_to_ctor_and_args(TypeA, TypeCtorA, ArgTypesA), defined_type_to_ctor_and_args(TypeB, TypeCtorB, ArgTypesB), ( if TypeCtorA = TypeCtorB then + % Checking for TypeCtorA = TypeCtorB before checking whether + % TypeA and TypeB are du types allows this code to succeed for + % + % - equivalence type + % - foreign types + % - solver types + % - abstract types + % - undefned type_ctors (ones that are not in the type table) + % + % Equivalence types should have been expanded out by now, + % so they pose no problem. (If they did appear here, we + % would have to expand them out, because without that, + % we cannot check for co- versus contra-variance.) + % + % The other kinds of types can all occur in the input + % of ths code. Most of the time, their argument lists + % are the empty list, but they can contain type parameters, + % such as the ones we use to distinguish e.g. prog_vars + % from tvars. XXX If anyone knows the technical name + % of such "ghost" type parameters, please write it here. + % + % I (zs) do not know whether type parameters on solver types + % (a) are ever useful, or (b) can cause issues with respect to + % co- versus contra-variance. corresponding_types_compare_as_given(TypeTable, TVarSet, Comparison, ArgTypesA, ArgTypesB, !TypeAssign, !CoerceFails) else + classify_defined_type_is_du_type(TypeTable, + TypeCtorA, ArgTypesA, MaybeDuTypeA), + classify_defined_type_is_du_type(TypeTable, + TypeCtorB, ArgTypesB, MaybeDuTypeB), + are_both_types_du(TypeA, TypeB, MaybeDuTypeA, MaybeDuTypeB, + MaybeBoth), ( - Comparison = compare_equal, - CoerceFail = should_be_invariant_arg(TypeA, TypeB), + MaybeBoth = error2(CoerceFail), + % A non-du type constructor cannot be a subtype. !:CoerceFails = [CoerceFail | !.CoerceFails] ; - Comparison = compare_equal_lt, - ( if - get_supertype(TypeTable, TVarSet, TypeCtorA, ArgTypesA, - SuperTypeA) - then - types_compare_as_given(TypeTable, TVarSet, Comparison, - SuperTypeA, TypeB, !TypeAssign, !CoerceFails) - else - % get_supertype fails only if TypeCtorA's definition - % is either - % - not a du type definition, or - % - it is a du type, but not a subtype type definition. - % XXX We should return a different fail for each. - CoerceFail = different_type_categories(TypeTable, - TypeA, TypeB), + MaybeBoth = ok2(DuTypeInfoA, _DuTypeInfoB), + ( + Comparison = compare_equal, + CoerceFail = should_be_invariant_arg(TypeA, TypeB), !:CoerceFails = [CoerceFail | !.CoerceFails] + ; + Comparison = compare_equal_lt, + DuTypeInfoA = + du_type_info(_, _, TypeDefnA, TypeBodyDuA), + MaybeSuperTypeA = TypeBodyDuA ^ du_type_supertype, + ( + MaybeSuperTypeA = subtype_of(SuperTypeA0), + get_supertype_of_subtype(TVarSet, + TypeCtorA, ArgTypesA, TypeDefnA, + SuperTypeA0, SuperTypeA), + types_compare_as_given(TypeTable, TVarSet, + Comparison, SuperTypeA, TypeB, + !TypeAssign, !CoerceFails) + ; + MaybeSuperTypeA = not_a_subtype, + CoerceFail = du_type_is_not_subtype(TypeCtorA), + !:CoerceFails = [CoerceFail | !.CoerceFails] + ) ) ) ) diff --git a/compiler/typecheck_errors.m b/compiler/typecheck_errors.m index dcc16916a..c52b46326 100644 --- a/compiler/typecheck_errors.m +++ b/compiler/typecheck_errors.m @@ -60,6 +60,7 @@ :- import_module parse_tree.prog_type_subst. :- import_module parse_tree.prog_type_test. +:- import_module int. :- import_module require. :- import_module set. :- import_module term. @@ -176,7 +177,7 @@ wrap_quote(Str) = [quote(Str)]. %---------------------------------------------------------------------------% report_invalid_coerce_from_to(ClauseContext, Context, FromVar, TVarSet, - FromType, ToType, Fails) = Spec :- + FromType, ToType, Fails0) = Spec :- % XXX TYPECHECK_ERRORS % This code can generate some less-than-helpful diagnostics. % @@ -191,7 +192,28 @@ report_invalid_coerce_from_to(ClauseContext, Context, FromVar, TVarSet, FromVarStr = mercury_var_to_name_only_vs(VarSet, FromVar), FromTypeStr = mercury_type_to_string(TVarSet, print_num_only, FromType), ToTypeStr = mercury_type_to_string(TVarSet, print_num_only, ToType), + + % The code of are_actual_param_type_pair_as_related_as_needed, + % when given a pair of types in an argument position that does not + % have to be invariant, tries out coercions in *both* directions. + % This means that if are_actual_param_type_pair_as_related_as_needed + % can return a specific coerce_fail, it can also return its mirror + % image, meaning it can also return a coerce_fail that is identical + % except for the exchange of roles between the from-type and the to-type. + % + % By imposing a standard order on each coerce_fails, we allow the + % call to sort_and_remove_dups to replace each mirror image + % with just coerce_fail. + % + % XXX are_actual_param_type_pair_as_related_as_needed could instead + % just arbitrarily always return either + % - the coerce_fails from the original comparison direction, or + % - the coerce_fails from the reverse comparison direction. + % Neither this nor that method seems universally superior. + Fails1 = list.map(standardize_coerce_fail, Fails0), + list.sort_and_remove_dups(Fails1, Fails), CausePieceLists = list.map(describe_coerce_fail(TVarSet), Fails), + list.condense(CausePieceLists, CausePieces), ( if strip_kind_annotation(FromType) = strip_kind_annotation(ToType) then RedundantPieces = @@ -207,6 +229,62 @@ report_invalid_coerce_from_to(ClauseContext, Context, FromVar, TVarSet, Spec = spec($pred, severity_error, phase_type_check, Context, InClauseForPieces ++ ErrorPieces). +:- func standardize_coerce_fail(coerce_fail) = coerce_fail. + +standardize_coerce_fail(Fail0) = Fail :- + ( + Fail0 = different_base_types(_, _, _, _), + Fail = Fail0 + ; + Fail0 = unknown_or_nonground_type(_, _, _), + Fail = Fail0 + ; + Fail0 = different_type_categories(TypeTable, FromType, ToType), + ( if compare((>), FromType, ToType) then + Fail = different_type_categories(TypeTable, ToType, FromType) + else + Fail = Fail0 + ) + ; + Fail0 = different_builtin_types(FromBuiltinType, ToBuiltinType), + ( if compare((>), FromBuiltinType, ToBuiltinType) then + Fail = different_builtin_types(ToBuiltinType, FromBuiltinType) + else + Fail = Fail0 + ) + ; + Fail0 = different_tuple_arities(FromArity, ToArity), + ( if FromArity > ToArity then + Fail = different_tuple_arities(ToArity, FromArity) + else + Fail = Fail0 + ) + ; + Fail0 = du_type_is_not_subtype(_), + Fail = Fail0 + ; + Fail0 = cannot_unify_type_vars(FromType, ToType), + ( if compare((>), FromType, ToType) then + Fail = cannot_unify_type_vars(ToType, FromType) + else + Fail = Fail0 + ) + ; + Fail0 = non_du_type_ctor(FromType, FromTypeDesc, ToType, ToTypeDesc), + ( if compare((>), FromTypeDesc, ToTypeDesc) then + Fail = non_du_type_ctor(ToType, ToTypeDesc, FromType, FromTypeDesc) + else + Fail = Fail0 + ) + ; + Fail0 = should_be_invariant_arg(FromType, ToType), + ( if compare((>), FromType, ToType) then + Fail = should_be_invariant_arg(ToType, FromType) + else + Fail = Fail0 + ) + ). + :- func describe_coerce_fail(tvarset, coerce_fail) = list(format_piece). describe_coerce_fail(TVarSet, Fail) = Pieces :- @@ -218,20 +296,6 @@ describe_coerce_fail(TVarSet, Fail) = Pieces :- FromType, FromBaseTypeCtor, ToType, ToBaseTypeCtor) ; Fail = unknown_or_nonground_type(_, _, _), - % We can and do generate this kind of coerce_fail during typechecking, - % but as of 2026 jul 26, I (zs) cannot - % - % - either construct a test case in which one of these coerce_fails - % survives the final prune coerce constraints pass, - % - % - or construct a correctness argument for the proposition that - % these coerce_fails *cannot* survive the final prune coerce - % constraints pass. - % - % In the absence of the former, which could serve as motivating - % example, I cannot design a good error message, and in the absence - % of the latter, I cannot replace the next line with a call to - % "unexpected". Pieces = [] ; Fail = different_type_categories(TypeTable, FromType, ToType), @@ -245,6 +309,9 @@ describe_coerce_fail(TVarSet, Fail) = Pieces :- Fail = different_tuple_arities(FromArity, ToArity), Pieces = describe_coerce_fail_different_tuple_arities( FromArity, ToArity) + ; + Fail = du_type_is_not_subtype(TypeCtor), + Pieces = describe_coerce_fail_du_type_is_not_subtype(TypeCtor) ; Fail = cannot_unify_type_vars(FromType, ToType), Pieces = describe_coerce_fail_cannot_unify_type_vars(TVarSet, @@ -276,6 +343,10 @@ describe_coerce_fail_different_base_types(_TVarSet, FromBaseCtorPiece = qual_type_ctor(FromBaseTypeCtor), ToBaseCtorPiece = qual_type_ctor(ToBaseTypeCtor) ), + % The use of coerce-from and coerce-to terminology here works + % because the comparison of base types is NOT subject to reversal + % by are_actual_param_type_pair_as_related_as_needed, since it happens + % above that predicate in the call tree. Pieces = [words("The base type constructor of the coerce-from type is")] ++ color_as_inconsistent([FromBaseCtorPiece, suffix(",")]) ++ [words("while for the coerce-to type it is")] ++ @@ -357,13 +428,20 @@ describe_coerce_fail_different_builtin_types(TVarSet, = list(format_piece). describe_coerce_fail_different_tuple_arities(FromArity, ToArity) = Pieces :- - Pieces = [words("You cannot coerce from a tuple type of")] ++ + Pieces = [words("You cannot coerce between a tuple type of")] ++ color_as_inconsistent([words("arity"), int_fixed(FromArity)]) ++ - [words("to a tuple type of")] ++ + [words("and a tuple type of")] ++ color_as_inconsistent([words("arity"), int_fixed(ToArity), suffix(".")]) ++ [nl]. +:- func describe_coerce_fail_du_type_is_not_subtype(type_ctor) + = list(format_piece). + +describe_coerce_fail_du_type_is_not_subtype(TypeCtor) = Pieces :- + Pieces = [qual_type_ctor(TypeCtor), words("is")] ++ + color_as_incorrect([words("not a subtype.")]) ++ [nl]. + :- func describe_coerce_fail_cannot_unify_type_vars(tvarset, mer_type, mer_type) = list(format_piece). diff --git a/compiler/typecheck_util.m b/compiler/typecheck_util.m index 89c188923..b11f82de9 100644 --- a/compiler/typecheck_util.m +++ b/compiler/typecheck_util.m @@ -109,6 +109,12 @@ :- pred classify_is_du_type(type_table::in, mer_type::in, maybe_du_type::out) is det. + % Do the same job as above, but for a type that is known to be + % a defined_type. + % +:- pred classify_defined_type_is_du_type(type_table::in, + type_ctor::in, list(mer_type)::in, maybe_du_type::out) is det. + %---------------------------------------------------------------------------% %---------------------------------------------------------------------------% @@ -224,29 +230,8 @@ classify_is_du_type(TypeTable, Type, MaybeDuType) :- Type = defined_type(SymName, ArgTypes, _Kind), list.length(ArgTypes, Arity), TypeCtor = type_ctor(SymName, Arity), - ( if search_type_ctor_defn(TypeTable, TypeCtor, TypeDefn) then - get_type_defn_body(TypeDefn, TypeBody), - ( - TypeBody = hlds_du_type(TypeBodyDu), - DuType = du_type_info(TypeCtor, ArgTypes, - TypeDefn, TypeBodyDu), - MaybeDuType = is_du_type(DuType) - ; - TypeBody = hlds_eqv_type(_), - MaybeDuType = is_not_du_type("equivalence type") - ; - TypeBody = hlds_foreign_type(_), - MaybeDuType = is_not_du_type("foreign type") - ; - TypeBody = hlds_solver_type(_), - MaybeDuType = is_not_du_type("solver type") - ; - TypeBody = hlds_abstract_type(_), - MaybeDuType = is_not_du_type("abstract type") - ) - else - MaybeDuType = is_not_du_type("unknown type") - ) + classify_defined_type_is_du_type(TypeTable, TypeCtor, ArgTypes, + MaybeDuType) ; Type = builtin_type(_), MaybeDuType = is_not_du_type("builtin type") @@ -273,6 +258,29 @@ classify_is_du_type(TypeTable, Type, MaybeDuType) :- classify_is_du_type(TypeTable, SubType, MaybeDuType) ). +classify_defined_type_is_du_type(TypeTable, TypeCtor, ArgTypes, MaybeDuType) :- + ( if search_type_ctor_defn(TypeTable, TypeCtor, TypeDefn) then + get_type_defn_body(TypeDefn, TypeBody), + ( + TypeBody = hlds_du_type(TypeBodyDu), + DuType = du_type_info(TypeCtor, ArgTypes, TypeDefn, TypeBodyDu), + MaybeDuType = is_du_type(DuType) + ; + TypeBody = hlds_eqv_type(_), + MaybeDuType = is_not_du_type("equivalence type") + ; + TypeBody = hlds_foreign_type(_), + MaybeDuType = is_not_du_type("foreign type") + ; + TypeBody = hlds_solver_type(_), + MaybeDuType = is_not_du_type("solver type") + ; + TypeBody = hlds_abstract_type(_), + MaybeDuType = is_not_du_type("abstract type") + ) + else + MaybeDuType = is_not_du_type("unknown type") + ). %---------------------------------------------------------------------------% :- end_module check_hlds.typecheck_util. diff --git a/tests/invalid/coerce_type_error.err_exp b/tests/invalid/coerce_type_error.err_exp index 0e4ee85e7..5c9604566 100644 --- a/tests/invalid/coerce_type_error.err_exp +++ b/tests/invalid/coerce_type_error.err_exp @@ -9,7 +9,7 @@ coerce_type_error.m:070: In clause for predicate `bad_phantom'/2: coerce_type_error.m:070: error: cannot coerce `X' from coerce_type_error.m:070: `coerce_type_error.phantom(int)' to coerce_type_error.m:070: `coerce_type_error.phantom(float)'. -coerce_type_error.m:070: Builtin types such as float and int cannot be either +coerce_type_error.m:070: Builtin types such as int and float cannot be either coerce_type_error.m:070: coerced from, or coerced to. coerce_type_error.m:091: In clause for predicate `bad_higher_order'/2: coerce_type_error.m:091: error: cannot coerce `X' from @@ -26,3 +26,10 @@ coerce_type_error.m:118: error: cannot coerce `X' 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)'. +coerce_type_error.m:125: In clause for predicate `non_subtypes'/2: +coerce_type_error.m:125: error: cannot coerce `Fruits' from +coerce_type_error.m:125: `list.list(coerce_type_error.fruit)' to +coerce_type_error.m:125: `list.list(coerce_type_error.orange_non_fruit)'. +coerce_type_error.m:125: `coerce_type_error.fruit'/0 is not a subtype. +coerce_type_error.m:125: `coerce_type_error.orange_non_fruit'/0 is not a +coerce_type_error.m:125: subtype. diff --git a/tests/invalid/coerce_type_error.m b/tests/invalid/coerce_type_error.m index 2da9b77af..859c3e308 100644 --- a/tests/invalid/coerce_type_error.m +++ b/tests/invalid/coerce_type_error.m @@ -118,3 +118,10 @@ bad_abs_type(X, Y) :- Y = coerce(X). %---------------------------------------------------------------------------% + +:- pred non_subtypes(list(fruit)::in, list(orange_non_fruit)::out) is det. + +non_subtypes(Fruits, Oranges) :- + Oranges = coerce(Fruits). + +%---------------------------------------------------------------------------% diff --git a/tests/invalid/coerce_unify_tvars.err_exp b/tests/invalid/coerce_unify_tvars.err_exp index ef2d295c2..9d475bee3 100644 --- a/tests/invalid/coerce_unify_tvars.err_exp +++ b/tests/invalid/coerce_unify_tvars.err_exp @@ -1,5 +1,5 @@ coerce_unify_tvars.m:063: In clause for predicate `head_type_params'/2: coerce_unify_tvars.m:063: error: cannot coerce `X' from `list.list(V_1)' to coerce_unify_tvars.m:063: `list.list(V_2)'. -coerce_unify_tvars.m:063: Type variables such as T2 and T1 cannot be either +coerce_unify_tvars.m:063: Type variables such as T1 and T2 cannot be either coerce_unify_tvars.m:063: coerced from, or coerced to.