diff --git a/compiler/prog_type.m b/compiler/prog_type.m index 1ea172719..0a4a96797 100644 --- a/compiler/prog_type.m +++ b/compiler/prog_type.m @@ -30,6 +30,9 @@ %---------------------------------------------------------------------------% +:- inst defined_type for mer_type/0 + ---> defined_type(ground, ground, ground). + % Given a non-variable type, return its type_ctor and argument types. % Fail if the type is a variable. % @@ -42,6 +45,11 @@ :- pred type_to_ctor_and_args_det(mer_type::in, type_ctor::out, list(mer_type)::out) is det. + % Given a defined type, return its type_ctor and argument types. + % +:- pred defined_type_to_ctor_and_args(mer_type::in(defined_type), + type_ctor::out, list(mer_type)::out) is det. + % Given a non-variable type, return its type_ctor. % Fail if the type is a variable. % @@ -231,9 +239,8 @@ type_to_ctor_and_args(Type, TypeCtor, ArgTypes) :- Type = type_variable(_, _), fail ; - Type = defined_type(SymName, ArgTypes, _), - Arity = list.length(ArgTypes), - TypeCtor = type_ctor(SymName, Arity) + Type = defined_type(_SymName, _ArgTypes, _), + defined_type_to_ctor_and_args(Type, TypeCtor, ArgTypes) ; Type = builtin_type(BuiltinType), builtin_type_name(BuiltinType, Name), @@ -286,6 +293,11 @@ type_to_ctor_and_args_det(Type, TypeCtor, ArgTypes) :- unexpected($pred, "type_to_ctor_and_args failed: " ++ string(Type)) ). +defined_type_to_ctor_and_args(Type, TypeCtor, ArgTypes) :- + Type = defined_type(SymName, ArgTypes, _), + Arity = list.length(ArgTypes), + TypeCtor = type_ctor(SymName, Arity). + type_to_ctor(Type, TypeCtor) :- % This should be subject to unused argument elimination. type_to_ctor_and_args(Type, TypeCtor, _ArgTypes). diff --git a/compiler/type_assign.m b/compiler/type_assign.m index 99c92000a..7d2d69443 100644 --- a/compiler/type_assign.m +++ b/compiler/type_assign.m @@ -26,6 +26,7 @@ :- import_module parse_tree.vartypes. :- import_module list. +:- import_module maybe. %---------------------------------------------------------------------------% % @@ -59,11 +60,14 @@ :- type coerce_constraint ---> coerce_constraint( % One or both sides should contain a type variable. - coerce_from :: mer_type, - coerce_to :: mer_type, - coerce_context :: prog_context, - coerce_var :: prog_var, - coerce_status :: coerce_constraint_status + coerce_from :: mer_type, + coerce_to :: mer_type, + coerce_context :: prog_context, + coerce_var :: prog_var, + coerce_status :: coerce_constraint_status, + % The list should be nonempty for all status values + % other than satisfied_but_redundant. ZZZ need_to_check? + coerce_fails :: list(coerce_fail) ). :- type coerce_constraint_status @@ -72,6 +76,86 @@ ; not_yet_resolved ; satisfied_but_redundant. + % The purpose of this type is let report_invalid_coerce_from_to + % describe *in specific detail* the cause of the coercion failure. + % + % Each function symbol in this list represents one point + % in the operation of the typecheck_coerce_between_types predicate + % and its subcontractors where it could fail. + % + % XXX While the current set of failure points works for typechecking + % I don't think this is the ideal set for explaining coercion failures + % to users. Specifically, at the moment we check whether both types + % are du types quite late; I think we should check this VERY early. + % + % NOTE: there is no point in discussing the details of what we + % record for each kind of failure until we decide on what set of failures + % we want. + % + % XXX I (zs) am not sure whether all these kinds of coerce fails + % can actually reach report_invalid_coerce_from_to. This is because + % I cannot rule out either of the following the possibilities. + % + % - A failure point lower down in the call tree will never be reached + % because some code higher up in the call tree will find a related + % but not identical failure point first, preventing execution from + % reaching the lower failure point. + % + % - Some coercion failures may occur during typechecking while the + % specific types bound to some type variables are not yet known, + % but they will go away once the bindings of those type variables + % become known. + % + % XXX Also, I am not sure that these names are the ones that + % best describe each kind of coercion failure. +:- type coerce_fail + ---> different_base_types( + % The two base type_ctors must be different. + dbt_from_type :: mer_type, + dbt_from_base_type_ctor :: type_ctor, + dbt_to_type :: mer_type, + dbt_to_base_type_ctor :: type_ctor + ) + ; unknown_or_nonground_type( + existq_tvars :: list(tvar), + % If both these arguments are yes(...), then + % type_is_ground_except_vars must fail for at least one + % of the wrapped types, when that predicate is passed + % the value in the existq_tvars field. + maybe_from_type :: maybe(mer_type), + maybe_to_type :: maybe(mer_type) + ) + ; incompatible_types( + % The two types have different principal function symbols. + it_from_type :: mer_type, + it_to_type :: mer_type + ) + ; cannot_coerce_type_vars( + % At least one of these must be a type_var. + cctv_from_type :: mer_type, + cctv_to_type :: mer_type + ) + ; cannot_unify_type_vars( + cutv_from_type :: mer_type, + cutv_to_type :: mer_type + ) + ; non_du_type_ctor( + % The from-type and the to-type have the same base type_ctor, + % but this base type_ctor is not a du type. + ndtc_from_type :: mer_type, + ndtc_to_type :: mer_type + ) + ; should_be_invariant_arg( + % The from-type and to-type are different, even though + % they should be identical. + % + % XXX We *really* need some extra info here + % that we use to explain to users the *reason* + % these should be identical. + sbia_from_type :: mer_type, + sbia_to_type :: mer_type + ). + :- pred type_assign_get_var_types(type_assign::in, vartypes::out) is det. :- pred type_assign_get_typevarset(type_assign::in, diff --git a/compiler/typecheck.m b/compiler/typecheck.m index 9f791463e..55c7252fa 100644 --- a/compiler/typecheck.m +++ b/compiler/typecheck.m @@ -1007,7 +1007,8 @@ report_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, FromVar, Status), + Coercion = coerce_constraint(FromType0, ToType0, Context, FromVar, + Status, Fails), type_assign_get_typevarset(TypeAssign, TVarSet), type_assign_get_type_bindings(TypeAssign, TypeBindings), apply_rec_subst_to_type(TypeBindings, FromType0, FromType), @@ -1019,7 +1020,7 @@ report_coercion(TypeAssign, Coercion, !Info) :- ; Status = unsatisfiable, Spec = report_invalid_coerce_from_to(ClauseContext, Context, FromVar, - TVarSet, FromType, ToType) + TVarSet, FromType, ToType, Fails) ; Status = not_yet_resolved, Spec = report_unresolved_coerce_from_to(ClauseContext, Context, diff --git a/compiler/typecheck_coerce.m b/compiler/typecheck_coerce.m index 5a31f794f..46b048791 100644 --- a/compiler/typecheck_coerce.m +++ b/compiler/typecheck_coerce.m @@ -122,21 +122,22 @@ typecheck_coerce_2(Info, Context, FromVar, ToVar, TypeAssign0, 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, TypeAssign0, TypeAssign1) - then + typecheck_coerce_between_types(TypeTable, TVarSet, + FromType, ToType, TypeAssign0, TypeAssign1, CoerceFails), + ( + CoerceFails = [], type_assign_get_type_bindings(TypeAssign1, TypeBindings1), ( if is_same_type_after_subst(TypeBindings1, FromType, ToType) then Coercion = coerce_constraint(FromType, ToType, Context, - FromVar, satisfied_but_redundant), + FromVar, satisfied_but_redundant, []), add_coerce_constraint(Coercion, TypeAssign1, TypeAssign) else TypeAssign = TypeAssign1 ) - else + ; + CoerceFails = [_HeadCoerceFail | _TailCoerceFails], Coercion = coerce_constraint(FromType, ToType, Context, FromVar, - unsatisfiable), + unsatisfiable, CoerceFails), add_coerce_constraint(Coercion, TypeAssign0, TypeAssign) ), !:TypeAssignSet = [TypeAssign | !.TypeAssignSet] @@ -165,8 +166,10 @@ typecheck_coerce_2(Info, Context, FromVar, ToVar, TypeAssign0, TypeAssign1, TypeAssign2) ) ), + CoerceFail = unknown_or_nonground_type(ExistQTVars, + MaybeFromType, MaybeToType), Coercion = coerce_constraint(FromType, ToType, Context, FromVar, - need_to_check), + need_to_check, [CoerceFail]), add_coerce_constraint(Coercion, TypeAssign2, TypeAssign), !:TypeAssignSet = [TypeAssign | !.TypeAssignSet] ). @@ -187,35 +190,57 @@ add_coerce_constraint(Coercion, !TypeAssign) :- Coercions = [Coercion | Coercions0], type_assign_set_coerce_constraints(Coercions, !TypeAssign). -%-------------% +%---------------------% :- pred typecheck_coerce_between_types(type_table::in, tvarset::in, - mer_type::in, mer_type::in, type_assign::in, type_assign::out) - is semidet. + mer_type::in, mer_type::in, type_assign::in, type_assign::out, + list(coerce_fail)::out) is det. typecheck_coerce_between_types(TypeTable, TVarSet, FromType, ToType, - !TypeAssign) :- + !TypeAssign, CoerceFails) :- % Type bindings must have been applied to FromType and ToType already. compute_base_type(TypeTable, TVarSet, FromType, FromBaseType), compute_base_type(TypeTable, TVarSet, ToType, ToBaseType), - type_to_ctor_and_args(FromBaseType, - FromBaseTypeCtor, FromBaseTypeArgTypes), - type_to_ctor_and_args(ToBaseType, - ToBaseTypeCtor, ToBaseTypeArgTypes), - - % 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_body(BaseTypeDefn, BaseTypeBody), - BaseTypeBody = hlds_du_type(BaseTypeBodyDu), - hlds_data.get_type_defn_tparams(BaseTypeDefn, BaseTypeParams), - compute_which_type_params_must_be_invariant(TypeTable, BaseTypeCtor, - BaseTypeBodyDu, BaseTypeParams, InvariantTVars), - are_type_params_as_related_as_needed(TypeTable, TVarSet, InvariantTVars, - BaseTypeParams, FromBaseTypeArgTypes, ToBaseTypeArgTypes, !TypeAssign). + ( if + type_to_ctor_and_args(FromBaseType, + FromBaseTypeCtor, FromBaseTypeArgTypes), + type_to_ctor_and_args(ToBaseType, + ToBaseTypeCtor, ToBaseTypeArgTypes) + then + ( if + % The input type and result type must have + % the same base type constructor. + BaseTypeCtor = FromBaseTypeCtor, + BaseTypeCtor = ToBaseTypeCtor + then + % Check the variance of type arguments. + ( if + hlds_data.search_type_ctor_defn(TypeTable, BaseTypeCtor, + BaseTypeDefn), + hlds_data.get_type_defn_body(BaseTypeDefn, BaseTypeBody), + BaseTypeBody = hlds_du_type(BaseTypeBodyDu) + then + hlds_data.get_type_defn_tparams(BaseTypeDefn, BaseTypeParams), + compute_which_type_params_must_be_invariant(TypeTable, + BaseTypeCtor, BaseTypeBodyDu, BaseTypeParams, + InvariantTVars), + are_type_params_as_related_as_needed(TypeTable, TVarSet, + InvariantTVars, BaseTypeParams, + FromBaseTypeArgTypes, ToBaseTypeArgTypes, + !TypeAssign, [], CoerceFails) + else + CoerceFail = non_du_type_ctor(FromBaseType, ToBaseType), + CoerceFails = [CoerceFail] + ) + else + CoerceFail = different_base_types(FromType, FromBaseTypeCtor, + ToType, ToBaseTypeCtor), + CoerceFails = [CoerceFail] + ) + else + CoerceFail = cannot_coerce_type_vars(FromType, ToType), + CoerceFails = [CoerceFail] + ). :- pred compute_base_type(type_table::in, tvarset::in, mer_type::in, mer_type::out) is det. @@ -315,6 +340,20 @@ acc_invariant_tvars_in_ctor_rhs_type(TypeTable, BaseTypeCtor, BaseTypeParams, require_complete_switch [TypeBody] ( TypeBody = hlds_du_type(_), + % Given a supertype t and a subtype ts, the condition + % and then-part allows programs to coerce from list(ts) + % to list(t). However, when trying to coerce from + % one_or_more(ts) to one_or_more(T), examining the + % one_or_more function symbol's second arg, whose type + % is list(ts), the condition fails, and the else-part + % prevents coercion from list(ts) to list(t). + % + % XXX If coercion from list(ts) to list(t) is allowed + % at the top level, why is it not allowed in an argument? + % + % It should be sufficient for TypeCtor and ArgTypes + % to match ONE of the types among our ancestors; + % the match shouldn't be restricted to the very top ancestor. ( if TypeCtor = BaseTypeCtor, type_list_to_var_list(ArgTypes, ArgTypeVars), @@ -405,10 +444,11 @@ acc_invariant_tvars_in_ctor_rhs_type(TypeTable, BaseTypeCtor, BaseTypeParams, :- pred are_type_params_as_related_as_needed(type_table::in, tvarset::in, invariant_tvars::in, list(tvar)::in, list(mer_type)::in, list(mer_type)::in, - type_assign::in, type_assign::out) is semidet. + type_assign::in, type_assign::out, + list(coerce_fail)::in, list(coerce_fail)::out) is det. are_type_params_as_related_as_needed(TypeTable, TVarSet, InvariantTVars, - TypeParams, FromArgTypes, ToArgTypes, !TypeAssign) :- + TypeParams, FromArgTypes, ToArgTypes, !TypeAssign, !CoerceFails) :- ( if TypeParams = [], FromArgTypes = [], @@ -422,10 +462,10 @@ are_type_params_as_related_as_needed(TypeTable, TVarSet, InvariantTVars, then is_type_param_pair_as_related_as_needed(TypeTable, TVarSet, InvariantTVars, HeadTypeParam, HeadFromArgType, HeadToArgType, - !TypeAssign), + !TypeAssign, !CoerceFails), are_type_params_as_related_as_needed(TypeTable, TVarSet, InvariantTVars, TailTypeParams, TailFromArgTypes, TailToArgTypes, - !TypeAssign) + !TypeAssign, !CoerceFails) else % FromArgTypes and ToArgTypes are the actual types bound to TypeParams % in the from-type and to-type of the coercion respectively. @@ -436,22 +476,25 @@ are_type_params_as_related_as_needed(TypeTable, TVarSet, InvariantTVars, :- pred is_type_param_pair_as_related_as_needed(type_table::in, tvarset::in, invariant_tvars::in, tvar::in, mer_type::in, mer_type::in, - type_assign::in, type_assign::out) is semidet. + type_assign::in, type_assign::out, + list(coerce_fail)::in, list(coerce_fail)::out) is det. is_type_param_pair_as_related_as_needed(TypeTable, TVarSet, InvariantTVars, - TypeVar, FromType, ToType, !TypeAssign) :- + TypeVar, FromType, ToType, !TypeAssign, !CoerceFails) :- ( if set.contains(InvariantTVars, TypeVar) then types_compare_as_given(TypeTable, TVarSet, compare_equal, - FromType, ToType, !TypeAssign) + FromType, ToType, !TypeAssign, !CoerceFails) else - ( if + types_compare_as_given(TypeTable, TVarSet, compare_equal_lt, + FromType, ToType, !.TypeAssign, FromToTypeAssign, + [], FromToCoerceFails), + ( + FromToCoerceFails = [], + !:TypeAssign = FromToTypeAssign + ; + FromToCoerceFails = [_ | _], types_compare_as_given(TypeTable, TVarSet, compare_equal_lt, - FromType, ToType, !TypeAssign) - then - true - else - types_compare_as_given(TypeTable, TVarSet, compare_equal_lt, - ToType, FromType, !TypeAssign) + ToType, FromType, !TypeAssign, !CoerceFails) ) ). @@ -470,82 +513,139 @@ is_type_param_pair_as_related_as_needed(TypeTable, TVarSet, InvariantTVars, % :- pred types_compare_as_given(type_table::in, tvarset::in, types_comparison::in, mer_type::in, mer_type::in, - type_assign::in, type_assign::out) is semidet. + type_assign::in, type_assign::out, + list(coerce_fail)::in, list(coerce_fail)::out) is det. types_compare_as_given(TypeTable, TVarSet, Comparison, TypeA, TypeB, - !TypeAssign) :- + !TypeAssign, !CoerceFails) :- ( if ( TypeA = type_variable(_, _) ; TypeB = type_variable(_, _) ) then - type_assign_unify_type(TypeA, TypeB, !TypeAssign) + ( if type_assign_unify_type(TypeA, TypeB, !TypeAssign) then + true + else + CoerceFail = cannot_unify_type_vars(TypeA, TypeB), + !:CoerceFails = [CoerceFail | !.CoerceFails] + ) else types_compare_as_given_nonvar(TypeTable, TVarSet, Comparison, - TypeA, TypeB, !TypeAssign) + TypeA, TypeB, !TypeAssign, !CoerceFails) ). :- pred types_compare_as_given_nonvar(type_table::in, tvarset::in, types_comparison::in, mer_type::in, mer_type::in, - type_assign::in, type_assign::out) is semidet. + type_assign::in, type_assign::out, + list(coerce_fail)::in, list(coerce_fail)::out) is det. types_compare_as_given_nonvar(TypeTable, TVarSet, Comparison, - TypeA, TypeB, !TypeAssign) :- + TypeA, TypeB, !TypeAssign, !CoerceFails) :- require_complete_switch [TypeA] ( TypeA = builtin_type(BuiltinType), - TypeB = builtin_type(BuiltinType) + ( if TypeB = builtin_type(BuiltinType) then + true + else + CoerceFail = incompatible_types(TypeA, TypeB), + !:CoerceFails = [CoerceFail | !.CoerceFails] + ) ; TypeA = type_variable(_, _), - TypeB = type_variable(_, _), unexpected($pred, "type_variable") ; TypeA = defined_type(_, _, _), - type_to_ctor_and_args(TypeA, TypeCtorA, ArgTypesA), - type_to_ctor_and_args(TypeB, TypeCtorB, ArgTypesB), - ( if TypeCtorA = TypeCtorB then - corresponding_types_compare_as_given(TypeTable, TVarSet, - Comparison, ArgTypesA, ArgTypesB, !TypeAssign) + ( if TypeB = defined_type(_, _, _) then + defined_type_to_ctor_and_args(TypeA, TypeCtorA, ArgTypesA), + defined_type_to_ctor_and_args(TypeB, TypeCtorB, ArgTypesB), + ( if TypeCtorA = TypeCtorB then + corresponding_types_compare_as_given(TypeTable, TVarSet, + Comparison, ArgTypesA, ArgTypesB, + !TypeAssign, !CoerceFails) + else + ( + Comparison = compare_equal, + CoerceFail = should_be_invariant_arg(TypeA, TypeB), + !: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. + % ZZZ We should return a differnt fail for each. + CoerceFail = incompatible_types(TypeA, TypeB), + !:CoerceFails = [CoerceFail | !.CoerceFails] + ) + ) + ) else - Comparison = compare_equal_lt, - get_supertype(TypeTable, TVarSet, TypeCtorA, ArgTypesA, - SuperTypeA), - types_compare_as_given(TypeTable, TVarSet, Comparison, - SuperTypeA, TypeB, !TypeAssign) + CoerceFail = incompatible_types(TypeA, TypeB), + !:CoerceFails = [CoerceFail | !.CoerceFails] ) ; TypeA = tuple_type(ArgTypesA, Kind), - TypeB = tuple_type(ArgTypesB, Kind), - corresponding_types_compare_as_given(TypeTable, TVarSet, Comparison, - ArgTypesA, ArgTypesB, !TypeAssign) + ( if TypeB = tuple_type(ArgTypesB, Kind) then + corresponding_types_compare_as_given(TypeTable, TVarSet, + Comparison, ArgTypesA, ArgTypesB, !TypeAssign, !CoerceFails) + else + CoerceFail = incompatible_types(TypeA, TypeB), + !:CoerceFails = [CoerceFail | !.CoerceFails] + ) ; TypeA = higher_order_type(PredOrFunc, ArgTypesA, _HOInstInfoA, Purity), - TypeB = higher_order_type(PredOrFunc, ArgTypesB, _HOInstInfoB, Purity), - % We do not allow subtyping in higher order argument types. - corresponding_types_compare_as_given(TypeTable, TVarSet, compare_equal, - ArgTypesA, ArgTypesB, !TypeAssign) + ( if TypeB = higher_order_type(PredOrFunc, ArgTypesB, _HO, Purity) then + % We do not allow subtyping in higher order argument types. + corresponding_types_compare_as_given(TypeTable, TVarSet, + compare_equal, ArgTypesA, ArgTypesB, !TypeAssign, !CoerceFails) + else + CoerceFail = incompatible_types(TypeA, TypeB), + !:CoerceFails = [CoerceFail | !.CoerceFails] + ) ; TypeA = apply_n_type(_, _, _), sorry($pred, "apply_n_type") ; TypeA = kinded_type(TypeA1, Kind), - TypeB = kinded_type(TypeB1, Kind), - types_compare_as_given(TypeTable, TVarSet, Comparison, - TypeA1, TypeB1, !TypeAssign) + % We require TypeB to be a kinded type of the SAME KIND as TypeA. + % XXX We should probably require it to have the same kind as TypeA, + % *without* requiring it to be a kinded type. However, that will matter + % only once we start using kinded types. + ( if TypeB = kinded_type(TypeB1, Kind) then + types_compare_as_given(TypeTable, TVarSet, Comparison, + TypeA1, TypeB1, !TypeAssign, !CoerceFails) + else + CoerceFail = incompatible_types(TypeA, TypeB), + !:CoerceFails = [CoerceFail | !.CoerceFails] + ) ). :- pred corresponding_types_compare_as_given(type_table::in, tvarset::in, types_comparison::in, list(mer_type)::in, list(mer_type)::in, - type_assign::in, type_assign::out) is semidet. + type_assign::in, type_assign::out, + list(coerce_fail)::in, list(coerce_fail)::out) is det. corresponding_types_compare_as_given(_TypeTable, _TVarSet, _Comparison, - [], [], !TypeAssign). + [], [], !TypeAssign, !CoerceFails). corresponding_types_compare_as_given(TypeTable, TVarSet, Comparison, - [TypeA | TypesA], [TypeB | TypesB], !TypeAssign) :- + [TypeA | TypesA], [TypeB | TypesB], !TypeAssign, !CoerceFails) :- types_compare_as_given(TypeTable, TVarSet, Comparison, - TypeA, TypeB, !TypeAssign), + TypeA, TypeB, !TypeAssign, !CoerceFails), corresponding_types_compare_as_given(TypeTable, TVarSet, Comparison, - TypesA, TypesB, !TypeAssign). + TypesA, TypesB, !TypeAssign, !CoerceFails). +corresponding_types_compare_as_given(_TypeTable, _TVarSet, _Comparison, + [_ | _], [], !TypeAssign, !CoerceFails) :- + unexpected($pred, "length mismatch"). +corresponding_types_compare_as_given(_TypeTable, _TVarSet, _Comparison, + [], [_ | _], !TypeAssign, !CoerceFails) :- + unexpected($pred, "length mismatch"). %---------------------------------------------------------------------------% %---------------------------------------------------------------------------% @@ -638,7 +738,7 @@ check_pending_coerce_constraints_loop(TypeTable, [Coercion0 | Coercions0], check_coerce_constraint_if_ready(TypeTable, Coercion0, Action, !TypeAssign) :- Coercion0 = coerce_constraint(FromType0, ToType0, Context, FromVar, - Status0), + Status0, _CoerceFails0), ( Status0 = need_to_check, TypeAssign0 = !.TypeAssign, @@ -648,24 +748,25 @@ check_coerce_constraint_if_ready(TypeTable, Coercion0, Action, !TypeAssign) :- apply_rec_subst_to_type(TypeBindings0, FromType0, FromType), apply_rec_subst_to_type(TypeBindings0, ToType0, ToType), ( if type_is_ground_except_vars(FromType, ExistQTVars) then - ( if - typecheck_coerce_between_types(TypeTable, TVarSet, - FromType, ToType, TypeAssign0, TypeAssign1) - then + typecheck_coerce_between_types(TypeTable, TVarSet, + FromType, ToType, TypeAssign0, TypeAssign1, CoerceFails), + ( + CoerceFails = [], type_assign_get_type_bindings(TypeAssign1, TypeBindings1), ( if is_same_type_after_subst(TypeBindings1, FromType, ToType) then - Coercion = coerce_constraint(FromType, ToType, - Context, FromVar, satisfied_but_redundant), + Coercion = coerce_constraint(FromType, ToType, Context, + FromVar, satisfied_but_redundant, []), Action = keep(Coercion) else Action = prune ), !:TypeAssign = TypeAssign1 - else - Coercion = coerce_constraint(FromType0, ToType0, - Context, FromVar, unsatisfiable), + ; + CoerceFails = [_HeadCoerceFail | _TailCoerceFails], + Coercion = coerce_constraint(FromType0, ToType0, Context, + FromVar, unsatisfiable, CoerceFails), Action = keep(Coercion) ) else @@ -696,7 +797,7 @@ type_assign_has_only_satisfied_coerce_constraints(TypeAssign) :- coerce_constraint_is_satisfied(Coercion) :- Coercion = coerce_constraint(_FromType, _ToType, _Context, _FromVar, - Status), + Status, _), require_complete_switch [Status] ( Status = satisfied_but_redundant diff --git a/compiler/typecheck_errors.m b/compiler/typecheck_errors.m index c3f6f292b..23aa6558b 100644 --- a/compiler/typecheck_errors.m +++ b/compiler/typecheck_errors.m @@ -23,13 +23,15 @@ :- import_module parse_tree.error_spec. :- import_module parse_tree.prog_data. +:- import_module list. + %---------------------------------------------------------------------------% :- func report_unsatisfiable_constraints(type_error_clause_context, prog_context, type_assign_set) = diag_spec. :- func report_invalid_coerce_from_to(type_error_clause_context, prog_context, - prog_var, tvarset, mer_type, mer_type) = diag_spec. + prog_var, tvarset, mer_type, mer_type, list(coerce_fail)) = diag_spec. :- func report_unresolved_coerce_from_to(type_error_clause_context, prog_context, prog_var, tvarset, mer_type, mer_type) = diag_spec. @@ -57,7 +59,6 @@ :- import_module parse_tree.prog_type_subst. :- import_module parse_tree.prog_type_test. -:- import_module list. :- import_module require. :- import_module set. :- import_module term. @@ -174,7 +175,7 @@ wrap_quote(Str) = [quote(Str)]. %---------------------------------------------------------------------------% report_invalid_coerce_from_to(ClauseContext, Context, FromVar, TVarSet, - FromType, ToType) = Spec :- + FromType, ToType, Fails) = Spec :- % XXX TYPECHECK_ERRORS % This code can generate some less-than-helpful diagnostics. % @@ -189,66 +190,8 @@ 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), - OnlyDuPieces = [words("You can only coerce"), - words("from one discriminated union type to another, and")], - ( if FromTypeStr = ToTypeStr then - describe_if_non_du_type(FromType, FromTypeNonDuPieces), - ( - FromTypeNonDuPieces = [], - % We shouldn't get here. FromType and ToType must be the same du - % type, but a coercion from one du type to the same du type must be - % type-correct. However, throwing an exception would only punish an - % innocent user. - CausePieces = [] - ; - FromTypeNonDuPieces = [_ | _], - CausePieces = OnlyDuPieces ++ - [quote(FromTypeStr), words("is a")] ++ - color_as_incorrect(FromTypeNonDuPieces ++ [suffix(".")]) - ) - else - describe_if_non_du_type(FromType, FromTypeNonDuPieces), - describe_if_non_du_type(ToType, ToTypeNonDuPieces), - ( - FromTypeNonDuPieces = [], - ( - ToTypeNonDuPieces = [], - % Either FromTypeNonDuPieces or ToTypeNonDuPieces should be - % nonempty, so we shouldn't get here. However, throwing - % an exception would only punish an innocent user. - CausePieces = [] - ; - ToTypeNonDuPieces = [_ | _], - CausePieces = OnlyDuPieces ++ - [quote(ToTypeStr), words("is a")] ++ - color_as_incorrect(ToTypeNonDuPieces ++ [suffix(".")]) - ) - ; - FromTypeNonDuPieces = [_ | _], - ( - ToTypeNonDuPieces = [], - CausePieces = OnlyDuPieces ++ - [quote(FromTypeStr), words("is a")] ++ - color_as_incorrect(FromTypeNonDuPieces ++ [suffix(".")]) - ; - ToTypeNonDuPieces = [_ | _], - ( if FromTypeNonDuPieces = ToTypeNonDuPieces then - CausePieces = OnlyDuPieces ++ - [quote(FromTypeStr), words("and"), quote(ToTypeStr), - words("are")] ++ - color_as_incorrect(FromTypeNonDuPieces ++ - [suffix("s.")]) - else - CausePieces = OnlyDuPieces ++ - [quote(FromTypeStr), words("is a")] ++ - color_as_incorrect(FromTypeNonDuPieces ++ - [suffix(",")]) ++ - [words("while"), quote(ToTypeStr), words("is a")] ++ - color_as_incorrect(ToTypeNonDuPieces ++ [suffix(".")]) - ) - ) - ) - ), + 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.")] @@ -263,6 +206,94 @@ report_invalid_coerce_from_to(ClauseContext, Context, FromVar, TVarSet, Spec = spec($pred, severity_error, phase_type_check, Context, InClauseForPieces ++ ErrorPieces). +:- func describe_coerce_fail(tvarset, coerce_fail) = list(format_piece). + +describe_coerce_fail(TVarSet, Fail) = Pieces :- + % XXX Generate descriptions for ALL kinds of coerce failures. + ( + Fail = different_base_types(_FromType, _FromBaseTypeCtor, + _ToType, _ToBaseTypeCtor), + Pieces = [] + ; + Fail = unknown_or_nonground_type(_, _, _), + Pieces = [] + ; + Fail = incompatible_types(_, _), + Pieces = [] + ; + Fail = cannot_coerce_type_vars(_, _), + Pieces = [] + ; + Fail = cannot_unify_type_vars(_, _), + Pieces = [] + ; + Fail = non_du_type_ctor(FromType, ToType), + Pieces = describe_coerce_fail_non_du_type_ctor(TVarSet, + FromType, ToType) + ; + Fail = should_be_invariant_arg(_, _), + Pieces = [] + ). + +:- func describe_coerce_fail_non_du_type_ctor(tvarset, mer_type, mer_type) + = list(format_piece). + +describe_coerce_fail_non_du_type_ctor(TVarSet, FromType, ToType) = Pieces :- + FromTypeStr = mercury_type_to_string(TVarSet, print_num_only, FromType), + ToTypeStr = mercury_type_to_string(TVarSet, print_num_only, ToType), + OnlyDuPieces = [words("You can only coerce"), + words("from one discriminated union type to another, and")], + describe_if_non_du_type(FromType, FromTypeNonDuPieces), + describe_if_non_du_type(ToType, ToTypeNonDuPieces), + ( + FromTypeNonDuPieces = [], + ( + ToTypeNonDuPieces = [], + % Either FromTypeNonDuPieces or ToTypeNonDuPieces should be + % nonempty, so we shouldn't get here. However, throwing + % an exception would only punish an innocent user. + Pieces = [] + ; + ToTypeNonDuPieces = [_ | _], + Pieces = OnlyDuPieces ++ + [quote(ToTypeStr), words("is a")] ++ + color_as_incorrect(ToTypeNonDuPieces ++ [suffix(".")]) + ) + ; + FromTypeNonDuPieces = [_ | _], + ( + ToTypeNonDuPieces = [], + Pieces = OnlyDuPieces ++ + [quote(FromTypeStr), words("is a")] ++ + color_as_incorrect(FromTypeNonDuPieces ++ [suffix(".")]) + ; + ToTypeNonDuPieces = [_ | _], + ( if FromTypeNonDuPieces = ToTypeNonDuPieces then + ( if FromTypeStr = ToTypeStr then + Pieces = OnlyDuPieces ++ + [quote(FromTypeStr), words("is a")] ++ + color_as_incorrect(FromTypeNonDuPieces ++ + [suffix(".")]) + else + Pieces = OnlyDuPieces ++ + [quote(FromTypeStr), words("and"), quote(ToTypeStr), + words("are")] ++ + color_as_incorrect(FromTypeNonDuPieces ++ + [suffix("s.")]) + ) + else + Pieces = OnlyDuPieces ++ + [quote(FromTypeStr), words("is a")] ++ + color_as_incorrect(FromTypeNonDuPieces ++ + [suffix(",")]) ++ + [words("while"), quote(ToTypeStr), words("is a")] ++ + color_as_incorrect(ToTypeNonDuPieces ++ [suffix(".")]) + ) + ) + ). + +%---------------------------------------------------------------------------% + report_unresolved_coerce_from_to(ClauseContext, Context, FromVar, TVarSet, FromType, ToType) = Spec :- InClauseForPieces = in_clause_for_pieces(ClauseContext), @@ -278,6 +309,8 @@ report_unresolved_coerce_from_to(ClauseContext, Context, FromVar, TVarSet, Spec = spec($pred, severity_error, phase_type_check, Context, InClauseForPieces ++ ErrorPieces). +%---------------------------------------------------------------------------% + report_redundant_coerce(ClauseContext, Context, FromVar, TVarSet, FromType) = Spec :- InClauseForPieces = in_clause_for_pieces(ClauseContext),