diff --git a/compiler/type_assign.m b/compiler/type_assign.m index b5cf49081..1f45bb4d6 100644 --- a/compiler/type_assign.m +++ b/compiler/type_assign.m @@ -141,10 +141,13 @@ dta_type_a :: arity, dta_type_b :: 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 + ; no_common_base_type( + ncbt_base_tc :: type_ctor, + ncbt_base_tc_arg_num :: uint, + % Both types are du types, but they do not have a common + % base type. + ncbt_type_a :: mer_type, + ncbt_type_b :: mer_type ) ; cannot_unify_type_vars( % One or both of these will be a type_variable. diff --git a/compiler/typecheck_coerce.m b/compiler/typecheck_coerce.m index cca6377c4..62b0c9582 100644 --- a/compiler/typecheck_coerce.m +++ b/compiler/typecheck_coerce.m @@ -401,21 +401,19 @@ typecheck_coerce_between_types(TypeTable, TVarSet, ; MaybeBoth = ok2(FromDuTypeInfo, ToDuTypeInfo), compute_base_type_of_du_type(TypeTable, TVarSet, - FromDuTypeInfo, FromBaseTypeInfo), + FromDuTypeInfo, FromBaseDuTypeInfo), compute_base_type_of_du_type(TypeTable, TVarSet, - ToDuTypeInfo, ToBaseTypeInfo), - FromBaseTypeInfo = du_type_info(FromBaseTypeCtor, FromBaseTypeArgTypes, - FromBaseTypeDefn, FromBaseTypeBodyDu), - ToBaseTypeInfo = du_type_info(ToBaseTypeCtor, ToBaseTypeArgTypes, - _ToBaseTypeDefn, _ToBaseTypeBodyDu), - ( if - % Coercion can work only if the from-type and to-type - % have the same base type constructor. - BaseTypeCtor = FromBaseTypeCtor, - BaseTypeCtor = ToBaseTypeCtor - then + ToDuTypeInfo, ToBaseDuTypeInfo), + FromBaseDuTypeInfo = du_type_info(FromBaseTypeCtor, + FromBaseTypeArgTypes, FromBaseTypeDefn, FromBaseTypeBodyDu), + ToBaseDuTypeInfo = du_type_info(ToBaseTypeCtor, + ToBaseTypeArgTypes, _ToBaseTypeDefn, _ToBaseTypeBodyDu), + % Coercion can work only if the from-type and to-type + % have the same base type constructor. + ( if FromBaseTypeCtor = ToBaseTypeCtor then % Since FromBaseTypeCtor = ToBaseTypeCtor, the two type % definitions and their bodies must be the same as well. + BaseTypeCtor = FromBaseTypeCtor, BaseTypeDefn = FromBaseTypeDefn, BaseTypeBodyDu = FromBaseTypeBodyDu, hlds_data.get_type_defn_tparams(BaseTypeDefn, BaseTypeCtorParams), @@ -759,44 +757,19 @@ are_actual_param_type_pair_as_related_as_needed(TypeTable, TVarSet, InvariantTVars, BaseTypeCtor, BaseTypeCtorParam, FromType, ToType, !ArgNum, !TypeAssign, !CoerceFails) :- ( if map.search(InvariantTVars, BaseTypeCtorParam, OoMCtorArgPosn) then - Comparison = compare_equal(ir_base_type_ctor(OoMCtorArgPosn)), - types_compare_as_given(TypeTable, TVarSet, BaseTypeCtor, !.ArgNum, - Comparison, FromType, ToType, !TypeAssign, !CoerceFails) + Comparison = must_be_invariant(ir_base_type_ctor(OoMCtorArgPosn)) else - types_compare_as_given(TypeTable, TVarSet, BaseTypeCtor, !.ArgNum, - compare_equal_lt, FromType, ToType, - !.TypeAssign, FromToTypeAssign, [], FromToCoerceFails), - ( - FromToCoerceFails = [], - !:TypeAssign = FromToTypeAssign - ; - FromToCoerceFails = [_ | _], - types_compare_as_given(TypeTable, TVarSet, BaseTypeCtor, !.ArgNum, - compare_equal_lt, 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 - ) - ) + Comparison = need_not_be_invariant ), + types_compare_as_given(TypeTable, TVarSet, BaseTypeCtor, !.ArgNum, + Comparison, FromType, ToType, !TypeAssign, !CoerceFails), !:ArgNum = !.ArgNum + 1u. %---------------------------------------------------------------------------% :- type types_comparison - ---> compare_equal(invariant_reason) - ; compare_equal_lt. + ---> must_be_invariant(invariant_reason) + ; need_not_be_invariant. % Succeed if TypeA unifies with TypeB (possibly binding type vars). % If Comparison is compare_equal_lt, then also succeed if TypeA =< TypeB @@ -921,9 +894,9 @@ types_compare_as_given(TypeTable, TVarSet, BaseTypeCtor, ArgNum, PurityA = PurityB then % We do not allow subtyping in higher order argument types, - % so we pass compare_equal here EVEN IF Comparison is - % compare_equal_lt. - SubComparison = compare_equal(ir_higher_order), + % so we pass must_be_invariant here EVEN IF Comparison is + % need_not_be_invariant. + SubComparison = must_be_invariant(ir_higher_order), corresponding_types_compare_as_given(TypeTable, TVarSet, BaseTypeCtor, ArgNum, SubComparison, ArgTypesA, ArgTypesB, !TypeAssign, !CoerceFails) @@ -1050,43 +1023,58 @@ defined_types_compare_as_given(TypeTable, TVarSet, BaseTypeCtor, ArgNum, MaybeBoth = ok2(DuTypenfoA, DuTypenfoB), du_types_compare_as_given(TypeTable, TVarSet, BaseTypeCtor, ArgNum, Comparison, - TypeA, TypeCtorA, ArgTypesA, DuTypenfoA, - TypeB, TypeCtorB, ArgTypesB, DuTypenfoB, + TypeA, DuTypenfoA, TypeB, DuTypenfoB, !TypeAssign, !CoerceFails) ) ). + % du_types_compare_as_given(TypeTable, TVarSet, BaseTypeCtor, ArgNum, + % Comparison, TypeA, DuTypeInfoA, TypeB, DuTypeInfoB, + % !TypeAssign, !CoerceFails): + % + % Our caller guarantees that TypeCtorA \= TypeCtorB. + % :- pred du_types_compare_as_given(type_table::in, tvarset::in, type_ctor::in, uint::in, types_comparison::in, - mer_type::in, type_ctor::in, list(mer_type)::in, du_type_info::in, - mer_type::in, type_ctor::in, list(mer_type)::in, du_type_info::in, + mer_type::in, du_type_info::in, mer_type::in, du_type_info::in, type_assign::in, type_assign::out, list(coerce_fail)::in, list(coerce_fail)::out) is det. du_types_compare_as_given(TypeTable, TVarSet, BaseTypeCtor, ArgNum, Comparison, - TypeA, TypeCtorA, ArgTypesA, DuTypeInfoA, - TypeB, _TypeCtorB, _ArgTypesB, _DuTypeInfoB, + TypeA, DuTypeInfoA, TypeB, DuTypeInfoB, !TypeAssign, !CoerceFails) :- ( - Comparison = compare_equal(Reason), - CoerceFail = should_be_invariant_arg(BaseTypeCtor, - ArgNum, Reason, TypeA, TypeB), + Comparison = must_be_invariant(Reason), + % Even if TypeA and/or TypeB contain type variables, + % no possible types being bound to those variables + % can fix the mismatch between TypeCtorA amd TypeCtorB. + CoerceFail = should_be_invariant_arg(BaseTypeCtor, ArgNum, + Reason, 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 = need_not_be_invariant, + % XXX If TypeA and TypeB have a common "ancestor" that is + % NOT their common supertype, we could use the nearest + % such common ancestor instead of the base type. + % This would allow us to check the coercability of + % any phantom type parameters that don't make it + % all the way up to the common base type. + compute_base_type_of_du_type(TypeTable, TVarSet, + DuTypeInfoA, BaseDuTypeInfoA), + compute_base_type_of_du_type(TypeTable, TVarSet, + DuTypeInfoB, BaseDuTypeInfoB), + BaseDuTypeInfoA = du_type_info(BaseTypeCtorA, + BaseTypeArgTypesA, _BaseTypeDefnA, _BaseTypeBodyDuA), + BaseDuTypeInfoB = du_type_info(BaseTypeCtorB, + BaseTypeArgTypesB, _BaseTypeDefnB, _BaseTypeBodyDuB), + ( if BaseTypeCtorA = BaseTypeCtorB then + corresponding_types_compare_as_given(TypeTable, TVarSet, BaseTypeCtor, ArgNum, Comparison, - SuperTypeA, TypeB, !TypeAssign, !CoerceFails) - ; - MaybeSuperTypeA = not_a_subtype, - CoerceFail = du_type_is_not_subtype(TypeCtorA), + BaseTypeArgTypesA, BaseTypeArgTypesB, + !TypeAssign, !CoerceFails) + else + CoerceFail = no_common_base_type(BaseTypeCtor, ArgNum, + TypeA, TypeB), !:CoerceFails = [CoerceFail | !.CoerceFails] ) ). diff --git a/compiler/typecheck_errors.m b/compiler/typecheck_errors.m index 397ede16d..cd43f6bc3 100644 --- a/compiler/typecheck_errors.m +++ b/compiler/typecheck_errors.m @@ -60,7 +60,6 @@ :- import_module parse_tree.prog_type_subst. :- import_module parse_tree.prog_type_test. -:- import_module int. :- import_module one_or_more. :- import_module require. :- import_module set. @@ -179,15 +178,10 @@ wrap_quote(Str) = [quote(Str)]. report_invalid_coerce_from_to(ClauseContext, Context, FromVar, TVarSet, FromType0, ToType0, Fails0) = Spec :- - % XXX TYPECHECK_ERRORS % This code can generate some less-than-helpful diagnostics. % % - For tests/invalid/coerce_unify_tvars.m and some others, it says that % you cannot coerce from one anonymous type variable to another. - % - % In most cases, we will report that the coerced argument type is - % unresolved. For the remaining cases, is there something we can report - % that would be more helpful? InClauseForPieces = in_clause_for_pieces(ClauseContext), VarSet = ClauseContext ^ tecc_varset, FromVarStr = mercury_var_to_name_only_vs(VarSet, FromVar), @@ -196,34 +190,18 @@ report_invalid_coerce_from_to(ClauseContext, Context, FromVar, TVarSet, 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), + list.sort_and_remove_dups(Fails0, Fails), CausePieceLists = list.map(describe_coerce_fail(TVarSet), Fails), - list.condense(CausePieceLists, CausePieces), + ( if strip_kind_annotation(FromType) = strip_kind_annotation(ToType) then RedundantPieces = - [words("Also, the type conversion would be redundant anyway.")] + [words("Also, the type conversion would be redundant anyway."), + nl] else RedundantPieces = [] ), + ErrorPieces = [words("error: cannot coerce")] ++ color_as_subject([quote(FromVarStr)]) ++ [words("from")] ++ color_as_inconsistent([quote(FromTypeStr)]) ++ [words("to")] ++ @@ -234,66 +212,6 @@ report_invalid_coerce_from_to(ClauseContext, Context, FromVar, TVarSet, %---------------------------------------------------------------------------% -:- func standardize_coerce_fail(coerce_fail) = coerce_fail. - -standardize_coerce_fail(Fail0) = Fail :- - ( - Fail0 = different_base_types(_, _, _, _), - Fail = Fail0 - ; - Fail0 = 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(BaseTypeCtor, ArgNum, Reason, - FromType, ToType), - ( if compare((>), FromType, ToType) then - Fail = should_be_invariant_arg(BaseTypeCtor, ArgNum, Reason, - ToType, FromType) - else - Fail = Fail0 - ) - ). - -%---------------------------------------------------------------------------% - :- func describe_coerce_fail(tvarset, coerce_fail) = list(format_piece). describe_coerce_fail(TVarSet, Fail) = Pieces :- @@ -320,8 +238,9 @@ describe_coerce_fail(TVarSet, Fail) = Pieces :- 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 = no_common_base_type(BaseTypeCtor, ArgNum, FromType, ToType), + Pieces = describe_coerce_fail_no_common_base_type(TVarSet, + BaseTypeCtor, ArgNum, FromType, ToType) ; Fail = cannot_unify_type_vars(FromType, ToType), Pieces = describe_coerce_fail_cannot_unify_type_vars(TVarSet, @@ -457,12 +376,21 @@ describe_coerce_fail_different_tuple_arities(FromArity, ToArity) = Pieces :- %---------------------% -:- func describe_coerce_fail_du_type_is_not_subtype(type_ctor) - = list(format_piece). +:- func describe_coerce_fail_no_common_base_type(tvarset, type_ctor, uint, + mer_type, mer_type) = 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]. +describe_coerce_fail_no_common_base_type(TVarSet, _BaseTypeCtor, _ArgNum, + FromType0, ToType0) = Pieces :- + delete_identical_qualifications(FromType0, ToType0, FromType, ToType), + FromTypeStr = mercury_type_to_string(TVarSet, print_num_only, FromType), + ToTypeStr = mercury_type_to_string(TVarSet, print_num_only, ToType), + Pieces = [words("Coercion between the types")] ++ + color_as_subject([words(FromTypeStr)]) ++ + [words("and")] ++ + color_as_subject([words(ToTypeStr)]) ++ + [words("is not possible, because they")] ++ + color_as_incorrect([words("do not have a common base type.")]) ++ + [nl]. %---------------------% @@ -584,7 +512,7 @@ describe_coerce_fail_should_be_invariant_arg(_TVarSet, BaseTypeCtor, ArgNum, words("occurs in a higher order type."), words("Normally, it would be ok for the input arguments"), words("of higher order types to be contra-variant,"), - words("the Mercury type checker does not know"), + words("but the Mercury type checker does not know"), words("which arguments are input."), words("It ensures soundness by requiring all arguments"), words("of higher order types to be invariant,"), diff --git a/tests/invalid/coerce_type_error.err_exp b/tests/invalid/coerce_type_error.err_exp index 358def8a8..92a31919d 100644 --- a/tests/invalid/coerce_type_error.err_exp +++ b/tests/invalid/coerce_type_error.err_exp @@ -39,6 +39,6 @@ coerce_type_error.m:118: constructor, which is an abstract type. coerce_type_error.m:125: In clause for predicate `non_subtypes'/2: coerce_type_error.m:125: error: cannot coerce `Fruits' from `list(fruit)' to coerce_type_error.m:125: `list(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. +coerce_type_error.m:125: Coercion between the types fruit and +coerce_type_error.m:125: orange_non_fruit is not possible, because they do +coerce_type_error.m:125: not have a common base type.