diff --git a/compiler/type_assign.m b/compiler/type_assign.m
index fc5d85e7c..9d2db1c77 100644
--- a/compiler/type_assign.m
+++ b/compiler/type_assign.m
@@ -28,6 +28,7 @@
 
 :- import_module list.
 :- import_module maybe.
+:- import_module one_or_more.
 
 %---------------------------------------------------------------------------%
 %
@@ -163,16 +164,46 @@
                 ndtc_to_type_desc       :: string
             )
     ;       should_be_invariant_arg(
+                sbia_base_tc            :: type_ctor,
+                sbia_base_tc_arg_num    :: uint,
+                % The reason why this paramater must have the same type
+                % bound to it in the from-type and the to-type.
+                sbia_reason             :: invariant_reason,
                 % 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
             ).
 
+:- type invariant_reason
+    --->    ir_base_type_ctor(one_or_more(ctor_arg_posn))
+            % The reason for the invariance requirement lies in
+            % the nature of one or more data constructor arguments
+            % (in the base type_ctor's du type definition) in which
+            % the type parameter occurs.
+    ;       ir_higher_order.
+            % The reason for the invariance requirement lies in
+            % the fact that the type bound to the type parameter in either
+            % the from-type or the to-type is a higher order type.
+
+:- type ctor_arg_posn
+    --->    ctor_arg_posn(du_or_tuple_cons_id, uint, posn_invariant_reason).
+
+:- type du_or_tuple_cons_id =< cons_id
+    --->    du_data_ctor(du_ctor)
+    ;       tuple_cons(arity).
+
+:- type posn_invariant_reason
+    --->    pir_du_nonrec(type_ctor, type_ctor)
+            % The base type_ctor, and the type_ctor
+            % of the data constructor's argument type.
+    ;       pir_foreign
+    ;       pir_solver
+    ;       pir_abstract
+    ;       pir_higher_order.
+
+%---------------------------------------------------------------------------%
+
 :- 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_coerce.m b/compiler/typecheck_coerce.m
index 303afeb29..78e890b05 100644
--- a/compiler/typecheck_coerce.m
+++ b/compiler/typecheck_coerce.m
@@ -76,9 +76,10 @@
 :- import_module map.
 :- import_module maybe.
 :- import_module one_or_more.
+:- import_module one_or_more_map.
 :- import_module require.
-:- import_module set.
 :- import_module term_context.
+:- import_module uint.
 :- import_module varset.
 
 %---------------------------------------------------------------------------%
@@ -413,9 +414,9 @@ typecheck_coerce_between_types(TypeTable, TVarSet, FromType, ToType,
                 BaseTypeCtor, BaseTypeCtorParams, BaseTypeBodyDu,
                 InvariantTVars),
             are_actual_param_type_pairs_as_related_as_needed(TypeTable,
-                TVarSet, InvariantTVars, BaseTypeCtorParams,
-                FromBaseTypeArgTypes, ToBaseTypeArgTypes,
-                !TypeAssign, [], CoerceFails)
+                TVarSet, InvariantTVars, BaseTypeCtor,
+                BaseTypeCtorParams, FromBaseTypeArgTypes, ToBaseTypeArgTypes,
+                1u, _, !TypeAssign, [], CoerceFails)
         else
             CoerceFail = different_base_types(FromType, FromBaseTypeCtor,
                 ToType, ToBaseTypeCtor),
@@ -484,7 +485,7 @@ compute_base_type_of_du_type(TypeTable, TVarSet, DuTypeInfo, BaseDuTypeInfo) :-
 
 %---------------------------------------------------------------------------%
 
-:- type invariant_tvars == set(tvar).
+:- type invariant_tvars == one_or_more_map(tvar, ctor_arg_posn).
 
     % compute_which_type_params_must_be_invariant(TypeTable,
     %     BaseTypeCtor, BaseTypeDefn, BaseTypeParams, InvariantTVars):
@@ -514,7 +515,7 @@ compute_which_type_params_must_be_invariant(TypeTable,
         % the only thing we ever use InvariantTVars for is to test whether
         % an element of BaseTypeCtorParams occurs in it. This is what
         % justifies returning the empty set here.
-        set.init(InvariantTVars)
+        one_or_more_map.init(InvariantTVars)
     ;
         BaseTypeCtorParams = [_ | _],
         BaseTypeBodyDu = type_body_du(OoMCtors, _OoMAlphaSortedCtors,
@@ -523,7 +524,7 @@ compute_which_type_params_must_be_invariant(TypeTable,
         list.foldl(
             acc_invariant_tvars_in_ctor(TypeTable,
                 BaseTypeCtor, BaseTypeCtorParams),
-            Ctors, set.init, InvariantTVars)
+            Ctors, one_or_more_map.init, InvariantTVars)
     ).
 
 :- pred acc_invariant_tvars_in_ctor(type_table::in,
@@ -532,23 +533,27 @@ compute_which_type_params_must_be_invariant(TypeTable,
 
 acc_invariant_tvars_in_ctor(TypeTable, BaseTypeCtor, BaseTypeCtorParams, Ctor,
         !InvariantTVars) :-
-    Ctor = ctor(_Ordinal, _MaybeExist, _CtorName, CtorArgs, _Arity, _Context),
-    list.foldl(
+    Ctor = ctor(_Ordinal, _MaybeExist, CtorSymName, CtorArgs, Arity, _Context),
+    DuCtor = du_ctor(CtorSymName, Arity, BaseTypeCtor),
+    ConsId = du_data_ctor(DuCtor),
+    list.foldl2(
         acc_invariant_tvars_in_ctor_arg(TypeTable,
-            BaseTypeCtor, BaseTypeCtorParams),
-        CtorArgs, !InvariantTVars).
+            BaseTypeCtor, BaseTypeCtorParams, ConsId),
+        CtorArgs, 1u, _, !InvariantTVars).
 
 :- pred acc_invariant_tvars_in_ctor_arg(type_table::in,
-    type_ctor::in, list(tvar)::in, constructor_arg::in,
+    type_ctor::in, list(tvar)::in, du_or_tuple_cons_id::in,
+    constructor_arg::in, uint::in, uint::out,
     invariant_tvars::in, invariant_tvars::out) is det.
 
 acc_invariant_tvars_in_ctor_arg(TypeTable, BaseTypeCtor, BaseTypeCtorParams,
-        CtorArg, !InvariantTVars) :-
+        DuCtor, CtorArg, !ArgNum, !InvariantTVars) :-
     CtorArg = ctor_arg(_MaybeFieldName, CtorArgType, _Context),
     % Since acc_invariant_tvars_in_ctor_arg_type is recursive,
     % we cannot inline it here.
     acc_invariant_tvars_in_ctor_arg_type(TypeTable,
-        BaseTypeCtor, BaseTypeCtorParams, CtorArgType, !InvariantTVars).
+        BaseTypeCtor, BaseTypeCtorParams, DuCtor, CtorArgType,
+        !ArgNum, !InvariantTVars).
 
     % We have to scan pretty much all the types that occur
     % on the right hand side of BaseTypeCtor's definition, whether they occur
@@ -562,11 +567,12 @@ acc_invariant_tvars_in_ctor_arg(TypeTable, BaseTypeCtor, BaseTypeCtorParams,
     % - they definitely *will* be identical (as with recursive types).
     %
 :- pred acc_invariant_tvars_in_ctor_arg_type(type_table::in,
-    type_ctor::in, list(tvar)::in, mer_type::in,
-    invariant_tvars::in, invariant_tvars::out) is det.
+    type_ctor::in, list(tvar)::in, du_or_tuple_cons_id::in, mer_type::in,
+    uint::in, uint::out, invariant_tvars::in, invariant_tvars::out) is det.
 
 acc_invariant_tvars_in_ctor_arg_type(TypeTable,
-        BaseTypeCtor, BaseTypeCtorParams, CtorArgType, !InvariantTVars) :-
+        BaseTypeCtor, BaseTypeCtorParams, ConsId, CtorArgType,
+        !ArgNum, !InvariantTVars) :-
     (
         CtorArgType = builtin_type(_)
     ;
@@ -606,38 +612,47 @@ acc_invariant_tvars_in_ctor_arg_type(TypeTable,
                 % (i.e. outside CtorArgType) as well.
                 true
             else
+                PosnReason = pir_du_nonrec(BaseTypeCtor, TypeCtor),
+                CtorArgPosn = ctor_arg_posn(ConsId, !.ArgNum, PosnReason),
                 type_vars_in_types(ArgTypes, TypeVars),
-                set.insert_list(TypeVars, !InvariantTVars)
+                list.foldl(one_or_more_map.reverse_add(CtorArgPosn), TypeVars,
+                    !InvariantTVars)
             )
         ;
-            ( TypeBody = hlds_foreign_type(_)
-            ; TypeBody = hlds_abstract_type(_)
-            ; TypeBody = hlds_solver_type(_)
+            ( TypeBody = hlds_foreign_type(_),  PosnReason = pir_foreign
+            ; TypeBody = hlds_solver_type(_),   PosnReason = pir_solver
+            ; TypeBody = hlds_abstract_type(_), PosnReason = pir_abstract
             ),
+            CtorArgPosn = ctor_arg_posn(ConsId, !.ArgNum, PosnReason),
             type_vars_in_types(ArgTypes, TypeVars),
-            set.insert_list(TypeVars, !InvariantTVars)
+            list.foldl(one_or_more_map.reverse_add(CtorArgPosn), TypeVars,
+                !InvariantTVars)
         ;
             TypeBody = hlds_eqv_type(EqvType0),
-            % This a equivalence type was not expanded out by
-            % equiv_type.m, so the source of the equivalence must be
-            % outside the set of type definitions that equiv_type.m
-            % pays attention to, such as in the implementation section
-            % of an imported module.
+            % This equivalence type was not expanded out by equiv_type.m,
+            % so the source of the equivalence must be outside the set of
+            % type definitions that equiv_type.m pays attention to,
+            % such as in the implementation section of an imported module.
             %
             % In these cases, expand out the type and process the result
             % as if the equivalence *had* been expanded out.
             hlds_data.get_type_defn_tparams(TypeDefn, TypeParams),
             map.from_corresponding_lists(TypeParams, ArgTypes, TSubst),
             apply_subst_to_type(TSubst, EqvType0, EqvType),
+            % We ignore the updated !:ArgNum, because we do not want to
+            % increment !.ArgNum BOTH here AND at clause end.
             acc_invariant_tvars_in_ctor_arg_type(TypeTable,
-                BaseTypeCtor, BaseTypeCtorParams, EqvType, !InvariantTVars)
+                BaseTypeCtor, BaseTypeCtorParams, ConsId, EqvType,
+                !.ArgNum, _, !InvariantTVars)
         )
     ;
         CtorArgType = tuple_type(ArgTypes, _Kind),
-        list.foldl(
+        list.length(ArgTypes, Arity),
+        TupleCtor = tuple_cons(Arity),
+        list.foldl2(
             acc_invariant_tvars_in_ctor_arg_type(TypeTable,
-                BaseTypeCtor, BaseTypeCtorParams),
-            ArgTypes, !InvariantTVars)
+                BaseTypeCtor, BaseTypeCtorParams, TupleCtor),
+            ArgTypes, 1u, _, !InvariantTVars)
     ;
         CtorArgType = higher_order_type(_PoF, ArgTypes, _HOInstInfo, _Purity),
         % We do not support any subtyping of higher order types.
@@ -646,21 +661,26 @@ acc_invariant_tvars_in_ctor_arg_type(TypeTable,
         % which means that all type parameters that occur in such
         % higher order types must be bound to the exact same value
         % in the from-type and to-type.
+        CtorArgPosn = ctor_arg_posn(ConsId, !.ArgNum, pir_higher_order),
         type_vars_in_types(ArgTypes, TypeVars),
-        set.insert_list(TypeVars, !InvariantTVars)
+        list.foldl(one_or_more_map.reverse_add(CtorArgPosn), TypeVars,
+            !InvariantTVars)
     ;
         CtorArgType = apply_n_type(_, _, _),
         sorry($pred, "apply_n_type")
     ;
         CtorArgType = kinded_type(SubCtorArgType, _Kind),
         acc_invariant_tvars_in_ctor_arg_type(TypeTable,
-            BaseTypeCtor, BaseTypeCtorParams, SubCtorArgType, !InvariantTVars)
-    ).
+            BaseTypeCtor, BaseTypeCtorParams, ConsId, SubCtorArgType,
+            !ArgNum, !InvariantTVars)
+    ),
+    !:ArgNum = !.ArgNum + 1u.
 
 %---------------------------------------------------------------------------%
 
     % are_actual_param_type_pairs_as_related_as_needed(TypeTable, TVarSet,
-    %   InvariantTVars, TypeParams, FromArgTypes, ToArgTypes, !TypeAssign):
+    %   InvariantTVars, BaseTypeCtor, BaseTypeParams, FromArgTypes, ToArgTypes,
+    %   !ArgNume, !TypeAssign, !CoerceFails):
     %
     % FromArgTypes and ToArgTypes are the actual types bound to TypeParams
     % in the from-type and to-type of the coercion respectively.
@@ -679,31 +699,33 @@ acc_invariant_tvars_in_ctor_arg_type(TypeTable,
     % relationship.
     %
 :- pred are_actual_param_type_pairs_as_related_as_needed(type_table::in,
-    tvarset::in, invariant_tvars::in,
+    tvarset::in, invariant_tvars::in, type_ctor::in,
     list(tvar)::in, list(mer_type)::in, list(mer_type)::in,
-    type_assign::in, type_assign::out,
+    uint::in, uint::out, type_assign::in, type_assign::out,
     list(coerce_fail)::in, list(coerce_fail)::out) is det.
 
 are_actual_param_type_pairs_as_related_as_needed(TypeTable, TVarSet,
-        InvariantTVars, TypeParams, FromArgTypes, ToArgTypes,
-        !TypeAssign, !CoerceFails) :-
+        InvariantTVars, BaseTypeCtor, BaseTypeCtorParams,
+        FromArgTypes, ToArgTypes, !ArgNum, !TypeAssign, !CoerceFails) :-
     ( if
-        TypeParams = [],
+        BaseTypeCtorParams = [],
         FromArgTypes = [],
         ToArgTypes = []
     then
         true
     else if
-        TypeParams = [HeadTypeParam | TailTypeParams],
+        BaseTypeCtorParams = [HeadBaseTypeCtorParam | TailBaseTypeCtorParams],
         FromArgTypes = [HeadFromArgType | TailFromArgTypes],
         ToArgTypes = [HeadToArgType | TailToArgTypes]
     then
         are_actual_param_type_pair_as_related_as_needed(TypeTable, TVarSet,
-            InvariantTVars, HeadTypeParam, HeadFromArgType, HeadToArgType,
-            !TypeAssign, !CoerceFails),
+            InvariantTVars, BaseTypeCtor,
+            HeadBaseTypeCtorParam, HeadFromArgType, HeadToArgType,
+            !ArgNum, !TypeAssign, !CoerceFails),
         are_actual_param_type_pairs_as_related_as_needed(TypeTable, TVarSet,
-            InvariantTVars, TailTypeParams, TailFromArgTypes, TailToArgTypes,
-            !TypeAssign, !CoerceFails)
+            InvariantTVars, BaseTypeCtor,
+            TailBaseTypeCtorParams, TailFromArgTypes, TailToArgTypes,
+            !ArgNum, !TypeAssign, !CoerceFails)
     else
         % FromArgTypes and ToArgTypes are the actual types bound to TypeParams
         % in the from-type and to-type of the coercion respectively.
@@ -713,28 +735,30 @@ are_actual_param_type_pairs_as_related_as_needed(TypeTable, TVarSet,
     ).
 
 :- pred are_actual_param_type_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,
+    tvarset::in, invariant_tvars::in, type_ctor::in,
+    tvar::in, mer_type::in, mer_type::in,
+    uint::in, uint::out, type_assign::in, type_assign::out,
     list(coerce_fail)::in, list(coerce_fail)::out) is det.
 
 are_actual_param_type_pair_as_related_as_needed(TypeTable, TVarSet,
-        InvariantTVars, TypeParam, FromType, ToType,
-        !TypeAssign, !CoerceFails) :-
-    ( if set.contains(InvariantTVars, TypeParam) then
-        types_compare_as_given(TypeTable, TVarSet, compare_equal,
-            FromType, ToType, !TypeAssign, !CoerceFails)
+        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)
     else
-        types_compare_as_given(TypeTable, TVarSet, compare_equal_lt,
-            FromType, ToType, !.TypeAssign, FromToTypeAssign,
-            [], FromToCoerceFails),
+        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, compare_equal_lt,
-                ToType, FromType, !.TypeAssign, ToFromTypeAssign,
-                [], ToFromCoerceFails),
+            types_compare_as_given(TypeTable, TVarSet, BaseTypeCtor, !.ArgNum,
+                compare_equal_lt, ToType, FromType,
+                !.TypeAssign, ToFromTypeAssign, [], ToFromCoerceFails),
             (
                 ToFromCoerceFails = [],
                 !:TypeAssign = ToFromTypeAssign
@@ -750,12 +774,13 @@ are_actual_param_type_pair_as_related_as_needed(TypeTable, TVarSet,
                     ++ !.CoerceFails
             )
         )
-    ).
+    ),
+    !:ArgNum = !.ArgNum + 1u.
 
 %---------------------------------------------------------------------------%
 
 :- type types_comparison
-    --->    compare_equal
+    --->    compare_equal(invariant_reason)
     ;       compare_equal_lt.
 
     % Succeed if TypeA unifies with TypeB (possibly binding type vars).
@@ -770,12 +795,12 @@ are_actual_param_type_pair_as_related_as_needed(TypeTable, TVarSet,
     % in modecheck_coerce.m.
     %
 :- pred types_compare_as_given(type_table::in, tvarset::in,
-    types_comparison::in, mer_type::in, mer_type::in,
+    type_ctor::in, uint::in, types_comparison::in, mer_type::in, mer_type::in,
     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, !CoerceFails) :-
+types_compare_as_given(TypeTable, TVarSet, BaseTypeCtor, ArgNum,
+        Comparison, TypeA, TypeB, !TypeAssign, !CoerceFails) :-
     ( if
         ( TypeA = type_variable(_, _)
         ; TypeB = type_variable(_, _)
@@ -788,17 +813,17 @@ types_compare_as_given(TypeTable, TVarSet, Comparison, TypeA, TypeB,
             !:CoerceFails = [CoerceFail | !.CoerceFails]
         )
     else
-        types_compare_as_given_nonvar(TypeTable, TVarSet, Comparison,
-            TypeA, TypeB, !TypeAssign, !CoerceFails)
+        types_compare_as_given_nonvar(TypeTable, TVarSet, BaseTypeCtor, ArgNum,
+            Comparison, 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_ctor::in, uint::in, types_comparison::in, mer_type::in, mer_type::in,
     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, !CoerceFails) :-
+types_compare_as_given_nonvar(TypeTable, TVarSet, BaseTypeCtor, ArgNum,
+        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]
@@ -848,7 +873,7 @@ types_compare_as_given_nonvar(TypeTable, TVarSet, Comparison,
                 % (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,
+                    BaseTypeCtor, ArgNum, Comparison, ArgTypesA, ArgTypesB,
                     !TypeAssign, !CoerceFails)
             else
                 classify_defined_type_is_du_type(TypeTable,
@@ -864,8 +889,9 @@ types_compare_as_given_nonvar(TypeTable, TVarSet, Comparison,
                 ;
                     MaybeBoth = ok2(DuTypeInfoA, _DuTypeInfoB),
                     (
-                        Comparison = compare_equal,
-                        CoerceFail = should_be_invariant_arg(TypeA, TypeB),
+                        Comparison = compare_equal(Reason),
+                        CoerceFail = should_be_invariant_arg(BaseTypeCtor,
+                            ArgNum, Reason, TypeA, TypeB),
                         !:CoerceFails = [CoerceFail | !.CoerceFails]
                     ;
                         Comparison = compare_equal_lt,
@@ -878,8 +904,8 @@ types_compare_as_given_nonvar(TypeTable, TVarSet, Comparison,
                                 TypeCtorA, ArgTypesA, TypeDefnA,
                                 SuperTypeA0, SuperTypeA),
                             types_compare_as_given(TypeTable, TVarSet,
-                                Comparison, SuperTypeA, TypeB,
-                                !TypeAssign, !CoerceFails)
+                                BaseTypeCtor, ArgNum, Comparison,
+                                SuperTypeA, TypeB, !TypeAssign, !CoerceFails)
                         ;
                             MaybeSuperTypeA = not_a_subtype,
                             CoerceFail = du_type_is_not_subtype(TypeCtorA),
@@ -899,7 +925,8 @@ types_compare_as_given_nonvar(TypeTable, TVarSet, Comparison,
             list.length(ArgTypesB, NumArgTypesB),
             ( if NumArgTypesA = NumArgTypesB then
                 corresponding_types_compare_as_given(TypeTable, TVarSet,
-                    Comparison, ArgTypesA, ArgTypesB, !TypeAssign, !CoerceFails)
+                    BaseTypeCtor, ArgNum, Comparison, ArgTypesA, ArgTypesB,
+                    !TypeAssign, !CoerceFails)
             else
                 CoerceFail =
                     different_tuple_arities(NumArgTypesA, NumArgTypesB),
@@ -916,9 +943,10 @@ types_compare_as_given_nonvar(TypeTable, TVarSet, Comparison,
         ( if TypeB = higher_order_type(PredOrFunc, ArgTypesB, _IB, Purity) 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,
+            SubComparison = compare_equal(ir_higher_order),
             corresponding_types_compare_as_given(TypeTable, TVarSet,
-                SubComparison, ArgTypesA, ArgTypesB, !TypeAssign, !CoerceFails)
+                BaseTypeCtor, ArgNum, SubComparison, ArgTypesA, ArgTypesB,
+                !TypeAssign, !CoerceFails)
         else
             CoerceFail = different_type_categories(TypeTable, TypeA, TypeB),
             !:CoerceFails = [CoerceFail | !.CoerceFails]
@@ -933,8 +961,8 @@ types_compare_as_given_nonvar(TypeTable, TVarSet, Comparison,
         % *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)
+            types_compare_as_given(TypeTable, TVarSet, BaseTypeCtor, ArgNum,
+                Comparison, TypeA1, TypeB1, !TypeAssign, !CoerceFails)
         else
             CoerceFail = different_type_categories(TypeTable, TypeA, TypeB),
             !:CoerceFails = [CoerceFail | !.CoerceFails]
@@ -942,22 +970,25 @@ types_compare_as_given_nonvar(TypeTable, TVarSet, Comparison,
     ).
 
 :- 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,
+    type_ctor::in, uint::in, types_comparison::in,
+    list(mer_type)::in, list(mer_type)::in, type_assign::in, type_assign::out,
     list(coerce_fail)::in, list(coerce_fail)::out) is det.
 
-corresponding_types_compare_as_given(_TypeTable, _TVarSet, _Comparison,
+corresponding_types_compare_as_given(_, _, _, _, _,
         [], [], !TypeAssign, !CoerceFails).
-corresponding_types_compare_as_given(TypeTable, TVarSet, Comparison,
-        [TypeA | TypesA], [TypeB | TypesB], !TypeAssign, !CoerceFails) :-
-    types_compare_as_given(TypeTable, TVarSet, Comparison,
-        TypeA, TypeB, !TypeAssign, !CoerceFails),
-    corresponding_types_compare_as_given(TypeTable, TVarSet, Comparison,
-        TypesA, TypesB, !TypeAssign, !CoerceFails).
-corresponding_types_compare_as_given(_TypeTable, _TVarSet, _Comparison,
+corresponding_types_compare_as_given(TypeTable, TVarSet,
+        BaseTypeCtor, ArgNum, Comparison, [TypeA | TypesA], [TypeB | TypesB],
+        !TypeAssign, !CoerceFails) :-
+    types_compare_as_given(TypeTable, TVarSet,
+        BaseTypeCtor, ArgNum, Comparison, TypeA, TypeB,
+        !TypeAssign, !CoerceFails),
+    corresponding_types_compare_as_given(TypeTable, TVarSet,
+        BaseTypeCtor, ArgNum, Comparison, TypesA, TypesB,
+        !TypeAssign, !CoerceFails).
+corresponding_types_compare_as_given(_, _, _, _, _,
         [_ | _], [], !TypeAssign, !CoerceFails) :-
     unexpected($pred, "length mismatch").
-corresponding_types_compare_as_given(_TypeTable, _TVarSet, _Comparison,
+corresponding_types_compare_as_given(_, _, _, _, _,
         [], [_ | _], !TypeAssign, !CoerceFails) :-
     unexpected($pred, "length mismatch").
 
diff --git a/compiler/typecheck_errors.m b/compiler/typecheck_errors.m
index 84cf254d3..01936c42b 100644
--- a/compiler/typecheck_errors.m
+++ b/compiler/typecheck_errors.m
@@ -61,6 +61,7 @@
 :- import_module parse_tree.prog_type_test.
 
 :- import_module int.
+:- import_module one_or_more.
 :- import_module require.
 :- import_module set.
 :- import_module term.
@@ -229,6 +230,8 @@ 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 :-
@@ -277,14 +280,18 @@ standardize_coerce_fail(Fail0) = Fail :-
             Fail = Fail0
         )
     ;
-        Fail0 = should_be_invariant_arg(FromType, ToType),
+        Fail0 = should_be_invariant_arg(BaseTypeCtor, ArgNum, Reason,
+            FromType, ToType),
         ( if compare((>), FromType, ToType) then
-            Fail = should_be_invariant_arg(ToType, FromType)
+            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 :-
@@ -321,10 +328,14 @@ describe_coerce_fail(TVarSet, Fail) = Pieces :-
         Pieces = describe_coerce_fail_non_du_type_ctor(TVarSet,
             FromType, FromTypeDesc, ToType, ToTypeDesc)
     ;
-        Fail = should_be_invariant_arg(_, _),
-        Pieces = []
+        Fail = should_be_invariant_arg(BaseTypeCtor, ArgNum, Reason,
+            FromType, ToType),
+        Pieces = describe_coerce_fail_should_be_invariant_arg(TVarSet,
+            BaseTypeCtor, ArgNum, Reason, FromType, ToType)
     ).
 
+%---------------------%
+
 :- func describe_coerce_fail_different_base_types(tvarset,
     mer_type, type_ctor, mer_type, type_ctor) = list(format_piece).
 
@@ -372,6 +383,8 @@ describe_coerce_fail_different_base_types(_TVarSet,
 %       color_as_inconsistent([ToBaseCtorPiece, suffix(".")]) ++
 %       [nl].
 
+%---------------------%
+
 :- func describe_coerce_fail_different_type_categories(type_table,
     mer_type, mer_type) = list(format_piece).
 
@@ -410,6 +423,8 @@ describe_coerce_fail_different_type_categories(TypeTable,
         Pieces = []
     ).
 
+%---------------------%
+
 :- func describe_coerce_fail_different_builtin_types(tvarset,
     builtin_type, builtin_type) = list(format_piece).
 
@@ -424,6 +439,8 @@ describe_coerce_fail_different_builtin_types(TVarSet,
         color_as_subject([words(ToTypeStr)]) ++
         [words("cannot be either coerced from, or coerced to."), nl].
 
+%---------------------%
+
 :- func describe_coerce_fail_different_tuple_arities(arity, arity)
     = list(format_piece).
 
@@ -435,6 +452,8 @@ describe_coerce_fail_different_tuple_arities(FromArity, ToArity) = Pieces :-
             suffix(".")]) ++
         [nl].
 
+%---------------------%
+
 :- func describe_coerce_fail_du_type_is_not_subtype(type_ctor)
     = list(format_piece).
 
@@ -442,6 +461,8 @@ 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).
 
@@ -475,6 +496,8 @@ describe_coerce_fail_cannot_unify_type_vars(TVarSet, FromType, ToType)
         words("to be equal to any type, or to be in a"),
         words("subtype relationship with any type."), nl].
 
+%---------------------%
+
 :- func describe_coerce_fail_non_du_type_ctor(tvarset,
     mer_type, string, mer_type, string) = list(format_piece).
 
@@ -542,6 +565,115 @@ describe_if_non_du_type(NonDuDesc, DescPieces) :-
         DescPieces = [words(NonDuDesc)]
     ).
 
+%---------------------%
+
+:- func describe_coerce_fail_should_be_invariant_arg(tvarset, type_ctor, uint,
+    invariant_reason, mer_type, mer_type) = list(format_piece).
+
+describe_coerce_fail_should_be_invariant_arg(_TVarSet, BaseTypeCtor, ArgNum,
+        Reason, _FromType, _ToType) = Pieces :-
+    % XXX Should we print _FromType and _ToType?
+    % In the usual case where BaseTypeCtor has a low arity, they will be
+    % obvious from the names of the coerce-from and coerce-to types.
+    (
+        Reason = ir_higher_order,
+        Pieces = [words("The type parameter that these types are bound to"),
+            words("occurs in a higher order type."),
+            words("Normally, it would be ok for the input arguments"),
+            words("of higher order types to be co-variant,"),
+            words("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,"),
+            words("meaning they must be the same in the"),
+            words("coerced-from and coerced-to types.")]
+    ;
+        Reason = ir_base_type_ctor(OoMCtorArgPosns),
+        BaseTypeCtor = type_ctor(_, BaseTypeCtorArity),
+        ( if
+            BaseTypeCtorArity = 1,
+            ArgNum = 1u
+        then
+            ArgNumPieces = [words("only parameter")]
+        else
+            ArgNumPieces = [unth_fixed(ArgNum), words("parameter")]
+        ),
+        FrontPieces = [words("The")] ++ ArgNumPieces ++
+            [words("of the type constructor"), unqual_type_ctor(BaseTypeCtor),
+            words("must be")] ++ color_as_correct([words("invariant,")]) ++
+            [words("meaning that it must be bound to the same type"),
+            words("in the coerced-from and coerced-to types.")],
+        OoMCtorArgPosns = one_or_more(HeadCtorArgPosn, TailCtorArgPosns),
+        HeadCtorArgPosnPieces = ctor_arg_posn_to_pieces(HeadCtorArgPosn),
+        (
+            TailCtorArgPosns = [],
+            Pieces = FrontPieces ++
+                [words("The reason for this is that"),
+                words("this type parameter occurs in")] ++
+                HeadCtorArgPosnPieces ++ [suffix("."), nl]
+        ;
+            TailCtorArgPosns = [_ | _],
+            TailCtorArgPosnPieces =
+                list.map(ctor_arg_posn_to_pieces, TailCtorArgPosns),
+            CtorArgPosnPiecesLists =
+                [HeadCtorArgPosnPieces | TailCtorArgPosnPieces],
+            list.intersperse_list_last([[suffix(","), nl]],
+                [[suffix(","), words("and"), nl]], CtorArgPosnPiecesLists,
+                AllCtorArgPosnPiecesLists),
+            list.condense(AllCtorArgPosnPiecesLists, AllCtorArgPosnPieces),
+            Pieces = FrontPieces ++
+                [words("The reasons for this are that"),
+                words("this type parameter occurs in")] ++
+                [nl_indent_delta(1)] ++
+                AllCtorArgPosnPieces ++
+                [suffix("."), nl_indent_delta(-1)]
+        )
+    ).
+
+:- func ctor_arg_posn_to_pieces(ctor_arg_posn) = list(format_piece).
+
+ctor_arg_posn_to_pieces(CtorArgPosn) = Pieces :-
+    CtorArgPosn = ctor_arg_posn(DuOrTupleConsId, ArgNum, PosnReason),
+    Pieces = [words("the type of the"),
+        unth_fixed(ArgNum), words("argument of the"),
+        unqual_cons_id_and_maybe_arity(coerce(DuOrTupleConsId)),
+        % XXX Should we s/data constructor/functionl symbol/?
+        words("data constructor, which")] ++
+        posn_invariant_reason_to_pieces(PosnReason).
+
+:- func posn_invariant_reason_to_pieces(posn_invariant_reason)
+    = list(format_piece).
+
+posn_invariant_reason_to_pieces(PosnReason) = Pieces :-
+    % XXX These should be color_as_incorrect, but to be consistent,
+    % we could need the color to include any comma suffix.
+    (
+        PosnReason = pir_du_nonrec(BaseTypeCtor, TypeCtor),
+        ( if BaseTypeCtor = TypeCtor then
+            Pieces = [words("applies the base type constructor"),
+                unqual_type_ctor(BaseTypeCtor),
+                % XXX Should we s/different/nonrecursive/?
+                words("to a different list of type parameters")]
+        else
+            % This should be a temporary limitation.
+            Pieces = [words("has a type constructor other than"),
+                unqual_type_ctor(BaseTypeCtor), suffix(","),
+                words("namely"), unqual_type_ctor(TypeCtor)]
+        )
+    ;
+        PosnReason = pir_foreign,
+        Pieces = [words("is a foreign type")]
+    ;
+        PosnReason = pir_solver,
+        Pieces = [words("is a solver type")]
+    ;
+        PosnReason = pir_abstract,
+        Pieces = [words("is an abstract type")]
+    ;
+        PosnReason = pir_higher_order,
+        Pieces = [words("is a higher order type")]
+    ).
+
 %---------------------------------------------------------------------------%
 
 report_unresolved_coerce_from_to(ClauseContext, Context, FromVar, TVarSet,
diff --git a/tests/invalid/Mercury.options b/tests/invalid/Mercury.options
index 336a709d6..1c924195d 100644
--- a/tests/invalid/Mercury.options
+++ b/tests/invalid/Mercury.options
@@ -44,6 +44,7 @@ MCFLAGS-bug487                  += --no-warn-unneeded-final-statevars
 MCFLAGS-children                += --no-intermodule-optimization
 MCFLAGS-coerce_implied_mode     += --halt-at-warn
 MCFLAGS-coerce_infer            += --infer-all
+MCFLAGS-coerce_type_error       += --no-intermodule-optimization
 MCFLAGS-coerce_typecheck_eqv    += --no-intermodule-optimization
 MCFLAGS-coerce_typecheck_eqv_helper_1 += --no-intermodule-optimization
 MCFLAGS-coerce_void             += --halt-at-warn
diff --git a/tests/invalid/coerce_type_error.err_exp b/tests/invalid/coerce_type_error.err_exp
index 5c9604566..3e9892e7f 100644
--- a/tests/invalid/coerce_type_error.err_exp
+++ b/tests/invalid/coerce_type_error.err_exp
@@ -16,16 +16,37 @@ coerce_type_error.m:091:   error: cannot coerce `X' 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:091:   The only parameter of the type constructor
+coerce_type_error.m:091:   `wrap_ho'/1 must be invariant, meaning that it must
+coerce_type_error.m:091:   be bound to the same type in the coerced-from and
+coerce_type_error.m:091:   coerced-to types. The reason for this is that this
+coerce_type_error.m:091:   type parameter occurs in the type of the first
+coerce_type_error.m:091:   argument of the `wrap_ho'/1 data constructor, which
+coerce_type_error.m:091:   is a higher order type.
 coerce_type_error.m:106: In clause for predicate `bad_foreign_type'/2:
 coerce_type_error.m:106:   error: cannot coerce `X' 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:106:   The only parameter of the type constructor
+coerce_type_error.m:106:   `wrap_ft'/1 must be invariant, meaning that it must
+coerce_type_error.m:106:   be bound to the same type in the coerced-from and
+coerce_type_error.m:106:   coerced-to types. The reason for this is that this
+coerce_type_error.m:106:   type parameter occurs in the type of the first
+coerce_type_error.m:106:   argument of the `wrap_ft'/1 data constructor, which
+coerce_type_error.m:106:   is a foreign type.
 coerce_type_error.m:118: In clause for predicate `bad_abs_type'/2:
 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:118:   The only parameter of the type constructor
+coerce_type_error.m:118:   `wrap_abs'/1 must be invariant, meaning that it must
+coerce_type_error.m:118:   be bound to the same type in the coerced-from and
+coerce_type_error.m:118:   coerced-to types. The reason for this is that this
+coerce_type_error.m:118:   type parameter occurs in the type of the first
+coerce_type_error.m:118:   argument of the `wrap_abs'/1 data constructor, which
+coerce_type_error.m:118:   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
 coerce_type_error.m:125:   `list.list(coerce_type_error.fruit)' to
@@ -33,3 +54,16 @@ coerce_type_error.m:125:   `list.list(coerce_type_error.orange_non_fr
 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:135: In clause for predicate `nested_du_type'/2:
+coerce_type_error.m:135:   error: cannot coerce `OoMCitrus' from
+coerce_type_error.m:135:   `one_or_more.one_or_more(coerce_type_error.citrus)'
+coerce_type_error.m:135:   to
+coerce_type_error.m:135:   `one_or_more.one_or_more(coerce_type_error.fruit)'.
+coerce_type_error.m:135:   The only parameter of the type constructor
+coerce_type_error.m:135:   `one_or_more'/1 must be invariant, meaning that it
+coerce_type_error.m:135:   must be bound to the same type in the coerced-from
+coerce_type_error.m:135:   and coerced-to types. The reason for this is that
+coerce_type_error.m:135:   this type parameter occurs in the type of the second
+coerce_type_error.m:135:   argument of the `one_or_more'/2 data constructor,
+coerce_type_error.m:135:   which has a type constructor other than
+coerce_type_error.m:135:   `one_or_more'/1, namely `list'/1.
diff --git a/tests/invalid/coerce_type_error.m b/tests/invalid/coerce_type_error.m
index 859c3e308..3caa82c1d 100644
--- a/tests/invalid/coerce_type_error.m
+++ b/tests/invalid/coerce_type_error.m
@@ -110,7 +110,7 @@ bad_foreign_type(X, Y) :-
 :- import_module set.
 
 :- type wrap_abs(T)
-    --->    wrap_abs(set(T)).
+    --->    wrap_abs(set(T)). % We disable intermod opt to keep set abstract.
 
 :- pred bad_abs_type(wrap_abs(citrus)::in, wrap_abs(fruit)::out) is det.
 
@@ -125,3 +125,13 @@ non_subtypes(Fruits, Oranges) :-
     Oranges = coerce(Fruits).
 
 %---------------------------------------------------------------------------%
+
+:- import_module one_or_more.
+
+:- pred nested_du_type(one_or_more(citrus)::in, one_or_more(fruit)::out)
+    is det.
+
+nested_du_type(OoMCitrus, OoMFruit) :-
+    OoMFruit = coerce(OoMCitrus).
+
+%---------------------------------------------------------------------------%
diff --git a/tests/invalid/coerce_typecheck_eqv.err_exp b/tests/invalid/coerce_typecheck_eqv.err_exp
index ac7746edd..12b188c67 100644
--- a/tests/invalid/coerce_typecheck_eqv.err_exp
+++ b/tests/invalid/coerce_typecheck_eqv.err_exp
@@ -3,3 +3,11 @@ coerce_typecheck_eqv.m:039:   error: cannot coerce `X' from
 coerce_typecheck_eqv.m:039:   `coerce_typecheck_eqv.bad(coerce_typecheck_eqv.citrus)'
 coerce_typecheck_eqv.m:039:   to
 coerce_typecheck_eqv.m:039:   `coerce_typecheck_eqv.bad(coerce_typecheck_eqv.fruit)'.
+coerce_typecheck_eqv.m:039:   The only parameter of the type constructor
+coerce_typecheck_eqv.m:039:   `bad'/1 must be invariant, meaning that it must
+coerce_typecheck_eqv.m:039:   be bound to the same type in the coerced-from and
+coerce_typecheck_eqv.m:039:   coerced-to types. The reason for this is that
+coerce_typecheck_eqv.m:039:   this type parameter occurs in the type of the
+coerce_typecheck_eqv.m:039:   first argument of the `bad'/1 data constructor,
+coerce_typecheck_eqv.m:039:   which has a type constructor other than `bad'/1,
+coerce_typecheck_eqv.m:039:   namely `list'/1.