[m-rev.] for review: combined higher-order types and insts

Mark Brown mark at mercurylang.org
Sun Jan 31 17:50:38 AEDT 2016


Hi,

This implements the new language feature that I proposed recently
under the heading of subtypes.

Part of the change is that I've moved some code to a new module and
also modified it. This doesn't show up in a full diff very well, so
I've also attached the diff of just these modifications to the new
module.

For review by anyone.

Mark.
-------------- next part --------------
Implement combined higher-order types and insts.

These allow types to be defined in the following manner:

    :- type job ---> job(pred(int::out, io::di, io::uo) is det).

For any construction unification using this functor the argument must
have the required higher-order inst; it is a mode error if it does not.
When terms of type job with inst ground are deconstructed, the argument
is inferred to have the given inst, allowing a higher-order call in that
mode.

The new type syntax is currently only permitted as the direct argument of
a functor in a du type definition. In future it would be meaningful to
support this syntax in other locations, but that is left for a separate
change.

In order to correctly implement the construct/3 library predicate, we
need to be able to dynamically check that arguments do not violate
any constraints on the argument insts. At the moment, we conservatively
abort if any such constraints are present irrespective of whether they
are satisfied or not. Since these constraints are a new feature, no
existing code will abort in this way.

The implementation refers to the inst information associated with types
as "subtype information". This is because, generally, we think of the
combination of a type with a fully bound inst (i.e., one that describes
terms that contain no unbound variables) describes a subtype of that type.

compiler/inst_util.m:
	Ensure that arguments have the necessary insts in construction
	unifications.

	Where available, propagate the insts into arguments rather than
	using ground(shared, none).

compiler/prog_io_type_name.m:
	Parse the new form of types.

	Move code for unparsing types into the new unparse module.

compiler/hlds_out_mode.m:
compiler/parse_tree.m:
compiler/unparse.m:
	Move code for unparsing types, modes and insts into a new
	unparse module. These are better together than split across
	both parse_tree and hlds, as they were before.

	Unparse the new form of types.

compiler/prog_io_type_defn.m:
	Allow the new form of types in functor arguments.

compiler/prog_ctgc.m:
compiler/prog_io_item.m:
compiler/prog_io_mutable.m:
compiler/prog_io_pragma.m:
compiler/prog_io_typeclass.m:
compiler/superhomogeneous.m:
	Disallow the new form of types in places other than functor
	arguments.

compiler/prog_data.m:
	Go back to representing function types with result type appended
	to the arguments. In most case this now results in simpler code.

compiler/prog_type.m:
	Abstract away the representation of predicate vs function arguments
	by using a predicate to construct these types.

compiler/rtti.m:
compiler/type_ctor_info.m:
	Include subtype information about the arguments of a du functor
	and about the argument of a notag functor. Generate this
	information from the argument types.

	Currently, the information is one bit which says whether or not
	any subtypes exist in the arguments.

	Bump the RTTI version number from the compiler side.

compiler/rtti_out.m:
	Output functor subtype information for the low-level C backend.

compiler/rtti_to_mlds.m:
	Include functor subtype information in the MLDS.

compiler/mlds_to_cs.m:
	Add the new runtime type to the special cases.

compiler/erl_rtti.m:
compiler/erlang_rtti.m:
library/erlang_rtti_implementation.m:
	Include functor subtype info in the erlang RTTI.

java/runtime/DuFunctorDesc.java:
java/runtime/FunctorSubtypeInfo.java:
	Include functor subtype information in the Java runtime.

runtime/mercury_dotnet.cs.in:
	Include functor subtype information in the C# runtime.

runtime/mercury_type_info.h:
	Include functor subtype information in the C runtime.

	Bump the RTTI version number in the runtime.

	Define macros to access the new field. These macros can correctly
	handle the previous RTTI version, therefore we do not need to
	change the minimum version at this time.

library/private_builtin.m:
	Define constants for use by the Java backend.

library/construct.m:
library/rtti_implementation.m:
	Use the new RTTI to ensure we don't attempt to construct terms
	that violate the new insts.

compiler/prog_rep_tables.m:
	Ignore the new inst info for now.

compiler/*.m:
	Changes to conform to above.

doc/refernce_manual.texi:
	Document the new feature.

tests/hard_coded/functor_ho_inst.{m,exp}:
tests/hard_coded/functor_ho_inst_2.{m,exp}:
tests/hard_coded/functor_ho_inst_excp.{m,exp}:
tests/hard_coded/functor_ho_inst_excp_2.{m,exp}:
	Test the new functionality.

tests/invalid/combined_ho_type_inst.{m,err_exp}:
	Test that we don't allow the new types where they are not permitted.

tests/invalid/functor_ho_inst_bad.{m,err_exp}:
tests/invalid/functor_ho_inst_bad_2.{m,err_exp}:
tests/invalid/functor_ho_inst_bad_3.{m,err_exp}:
	Test that the argument inst information is enforced as required.

tests/hard_coded/Mmakefile:
tests/invalid/Mmakefile:
	Run the new test cases.

-------------- next part --------------
diff --git a/compiler/check_typeclass.m b/compiler/check_typeclass.m
index aefc898..170d943 100644
--- a/compiler/check_typeclass.m
+++ b/compiler/check_typeclass.m
@@ -282,7 +282,7 @@ is_valid_instance_orig_type(ModuleInfo, ClassId, InstanceDefn, Type,
         )
     ;
         ( Type = builtin_type(_)
-        ; Type = higher_order_type(_, _, _, _)
+        ; Type = higher_order_type(_, _, _, _, _)
         ; Type = apply_n_type(_, _, _)
         ; Type = type_variable(_, _)
         ; Type = tuple_type(_, _)
@@ -307,7 +307,7 @@ is_valid_instance_type(ModuleInfo, ClassId, InstanceDefn, Type,
         Type = builtin_type(_)
     ;
         (
-            Type = higher_order_type(_, _, _, _),
+            Type = higher_order_type(_, _, _, _, _),
             EndPieces = [words("is a higher order type.")]
         ;
             Type = apply_n_type(_, _, _),
@@ -383,7 +383,7 @@ each_arg_is_a_type_variable(SeenTypes, [Type | Types], N, Result) :-
     ;
         ( Type = defined_type(_, _, _)
         ; Type = builtin_type(_)
-        ; Type = higher_order_type(_, _, _, _)
+        ; Type = higher_order_type(_, _, _, _, _)
         ; Type = tuple_type(_, _)
         ; Type = apply_n_type(_, _, _)
         ; Type = kinded_type(_, _)
diff --git a/compiler/common.m b/compiler/common.m
index 788dbae..aa9bb13 100644
--- a/compiler/common.m
+++ b/compiler/common.m
@@ -873,17 +873,9 @@ types_match_exactly(type_variable(TVar, _), type_variable(TVar, _)).
 types_match_exactly(defined_type(Name, As, _), defined_type(Name, Bs, _)) :-
     types_match_exactly_list(As, Bs).
 types_match_exactly(builtin_type(BuiltinType), builtin_type(BuiltinType)).
-types_match_exactly(higher_order_type(As, AR, P, E),
-        higher_order_type(Bs, BR, P, E)) :-
-    types_match_exactly_list(As, Bs),
-    (
-        AR = yes(A),
-        BR = yes(B),
-        types_match_exactly(A, B)
-    ;
-        AR = no,
-        BR = no
-    ).
+types_match_exactly(higher_order_type(PorF, As, H, P, E),
+        higher_order_type(PorF, Bs, H, P, E)) :-
+    types_match_exactly_list(As, Bs).
 types_match_exactly(tuple_type(As, _), tuple_type(Bs, _)) :-
     types_match_exactly_list(As, Bs).
 types_match_exactly(apply_n_type(TVar, As, _), apply_n_type(TVar, Bs, _)) :-
diff --git a/compiler/equiv_type.m b/compiler/equiv_type.m
index f6beb67..0d039e7 100644
--- a/compiler/equiv_type.m
+++ b/compiler/equiv_type.m
@@ -1140,27 +1140,13 @@ replace_in_type_maybe_record_use_2(MaybeRecord, TypeEqvMap,
         Changed = no,
         Circ = no
     ;
-        Type0 = higher_order_type(Args0, MaybeRet0, Purity, EvalMethod),
+        Type0 = higher_order_type(PorF, Args0, HOInstInfo, Purity, EvalMethod),
         replace_in_type_list_location_circ_2(MaybeRecord, TypeEqvMap,
-            TypeCtorsAlreadyExpanded, Args0, Args, ArgsChanged, no, ArgsCirc,
+            TypeCtorsAlreadyExpanded, Args0, Args, Changed, no, Circ,
             !VarSet, !EquivTypeInfo, !UsedModules),
         (
-            MaybeRet0 = yes(Ret0),
-            replace_in_type_maybe_record_use_2(MaybeRecord, TypeEqvMap,
-                TypeCtorsAlreadyExpanded, Ret0, Ret, RetChanged, RetCirc,
-                !VarSet, !EquivTypeInfo, !UsedModules),
-            MaybeRet = yes(Ret),
-            Changed = bool.or(ArgsChanged, RetChanged),
-            Circ = bool.or(ArgsCirc, RetCirc)
-        ;
-            MaybeRet0 = no,
-            MaybeRet = no,
-            Changed = ArgsChanged,
-            Circ = ArgsCirc
-        ),
-        (
             Changed = yes,
-            Type = higher_order_type(Args, MaybeRet, Purity, EvalMethod)
+            Type = higher_order_type(PorF, Args, HOInstInfo, Purity, EvalMethod)
         ;
             Changed = no,
             Type = Type0
diff --git a/compiler/equiv_type_hlds.m b/compiler/equiv_type_hlds.m
index c469322..c9774e6 100644
--- a/compiler/equiv_type_hlds.m
+++ b/compiler/equiv_type_hlds.m
@@ -650,23 +650,15 @@ hlds_replace_in_type_2(TypeEqvMap, TypeCtorsAlreadyExpanded,
         hlds_replace_type_ctor(TypeEqvMap, TypeCtorsAlreadyExpanded, Type0,
             TypeCtor, TypeArgs, Kind, Type, ArgsChanged, Changed, !VarSet)
     ;
-        Type0 = higher_order_type(ArgTypes0, MaybeRetType0, Purity,
+        Type0 = higher_order_type(PorF, ArgTypes0, HOInstInfo, Purity,
             EvalMethod),
-        (
-            MaybeRetType0 = yes(RetType0),
-            hlds_replace_in_type_2(TypeEqvMap, TypeCtorsAlreadyExpanded,
-                RetType0, RetType, RetChanged, !VarSet),
-            MaybeRetType = yes(RetType)
-        ;
-            MaybeRetType0 = no,
-            MaybeRetType = no,
-            RetChanged = no
-        ),
+        % XXX replace in HOInstInfo
+        HOInstInfoChanged = no,
         hlds_replace_in_type_list_2(TypeEqvMap, TypeCtorsAlreadyExpanded,
-            ArgTypes0, ArgTypes, RetChanged, Changed, !VarSet),
+            ArgTypes0, ArgTypes, HOInstInfoChanged, Changed, !VarSet),
         (
             Changed = yes,
-            Type = higher_order_type(ArgTypes, MaybeRetType, Purity,
+            Type = higher_order_type(PorF, ArgTypes, HOInstInfo, Purity,
                 EvalMethod)
         ;
             Changed = no,
diff --git a/compiler/erl_rtti.m b/compiler/erl_rtti.m
index c6aa636..3d16a95 100644
--- a/compiler/erl_rtti.m
+++ b/compiler/erl_rtti.m
@@ -155,14 +155,14 @@ erlang_type_ctor_details_2(CtorDetails) = Details :-
         unexpected($module, $pred, "reserved")
     ;
         CtorDetails = tcd_notag(_, NoTagFunctor),
-        NoTagFunctor = notag_functor(Name, TypeInfo, ArgName),
+        NoTagFunctor = notag_functor(Name, TypeInfo, ArgName, SubtypeInfo),
         OrigArity = 1,
         Ordinal = 0,
         FunctorNum = 0,
         ArgTypeInfo = convert_to_rtti_maybe_pseudo_type_info_or_self(TypeInfo),
         ArgInfos = [du_arg_info(ArgName, ArgTypeInfo, full_word)],
         DUFunctor = erlang_du_functor(Name, OrigArity, Ordinal, FunctorNum,
-            erlang_atom_raw(Name), ArgInfos, no),
+            erlang_atom_raw(Name), ArgInfos, no, SubtypeInfo),
         Details = erlang_du([DUFunctor])
     ;
         CtorDetails = tcd_eqv(Type),
@@ -186,7 +186,7 @@ erlang_type_ctor_details_2(CtorDetails) = Details :-
 convert_enum_functor(EnumFunctor, FunctorNum, ErlangFunctor) :-
     EnumFunctor = enum_functor(Name, Ordinal),
     ErlangFunctor = erlang_du_functor(Name, 0, Ordinal, FunctorNum,
-        erlang_atom_raw(Name), [], no).
+        erlang_atom_raw(Name), [], no, functor_subtype_none).
 
     % Convert a du_functor into the equivalent erlang_du_functor
     %
@@ -194,9 +194,9 @@ convert_enum_functor(EnumFunctor, FunctorNum, ErlangFunctor) :-
     is det.
 
 convert_du_functor(Functor, FunctorNum, ErlangFunctor) :-
-    Functor = du_functor(Name, Arity, Ordinal, _, ArgInfos, Exist),
+    Functor = du_functor(Name, Arity, Ordinal, _, ArgInfos, Exist, SubtypeInfo),
     ErlangFunctor = erlang_du_functor(Name, Arity, Ordinal, FunctorNum,
-        erlang_atom_raw(Name), ArgInfos, Exist).
+        erlang_atom_raw(Name), ArgInfos, Exist, SubtypeInfo).
 
 :- func convert_to_rtti_maybe_pseudo_type_info_or_self(
     rtti_maybe_pseudo_type_info) = rtti_maybe_pseudo_type_info_or_self.
diff --git a/compiler/erlang_rtti.m b/compiler/erlang_rtti.m
index 6b986f9..a0e41f0 100644
--- a/compiler/erlang_rtti.m
+++ b/compiler/erlang_rtti.m
@@ -121,7 +121,8 @@
                     % in the future maybe name_arity
                 edu_rep             :: erlang_atom_raw,
                 edu_arg_infos       :: list(du_arg_info),
-                edu_exist_info      :: maybe(exist_info)
+                edu_exist_info      :: maybe(exist_info),
+                edu_subtype_info    :: functor_subtype_info
             ).
 
 :- type erlang_atom_raw
diff --git a/compiler/export.m b/compiler/export.m
index eaf34cd..9199db5 100644
--- a/compiler/export.m
+++ b/compiler/export.m
@@ -661,7 +661,7 @@ convert_type_to_mercury(Rval, Type, TargetArgLoc, ConvertedRval) :-
     ;
         ( Type = type_variable(_, _)
         ; Type = defined_type(_, _, _)
-        ; Type = higher_order_type(_, _, _, _)
+        ; Type = higher_order_type(_, _, _, _, _)
         ; Type = tuple_type(_, _)
         ; Type = apply_n_type(_, _, _)
         ; Type = kinded_type(_, _)
@@ -693,7 +693,7 @@ convert_type_from_mercury(SourceArgLoc, Rval, Type, ConvertedRval) :-
     ;
         ( Type = type_variable(_, _)
         ; Type = defined_type(_, _, _)
-        ; Type = higher_order_type(_, _, _, _)
+        ; Type = higher_order_type(_, _, _, _, _)
         ; Type = tuple_type(_, _)
         ; Type = apply_n_type(_, _, _)
         ; Type = kinded_type(_, _)
diff --git a/compiler/foreign.m b/compiler/foreign.m
index fdf6a3c..9c84faf 100644
--- a/compiler/foreign.m
+++ b/compiler/foreign.m
@@ -422,7 +422,7 @@ exported_type_to_string(Lang, ExportedType) = Result :-
                 % XXX Is MR_Word the right thing for any of these kinds of
                 % types for high level code, with or without high level data?
                 ( Type = defined_type(_, _, _)
-                ; Type = higher_order_type(_, _, _, _)
+                ; Type = higher_order_type(_, _, _, _, _)
                 ; Type = apply_n_type(_, _, _)
                 ),
                 Result = "MR_Word"
@@ -453,7 +453,7 @@ exported_type_to_string(Lang, ExportedType) = Result :-
             ;
                 ( Type = tuple_type(_, _)
                 ; Type = defined_type(_, _, _)
-                ; Type = higher_order_type(_, _, _, _)
+                ; Type = higher_order_type(_, _, _, _, _)
                 ; Type = apply_n_type(_, _, _)
                 ; Type = type_variable(_, _)
                 ; Type = kinded_type(_, _)
@@ -482,7 +482,7 @@ exported_type_to_string(Lang, ExportedType) = Result :-
             ;
                 ( Type = tuple_type(_, _)
                 ; Type = defined_type(_, _, _)
-                ; Type = higher_order_type(_, _, _, _)
+                ; Type = higher_order_type(_, _, _, _, _)
                 ; Type = apply_n_type(_, _, _)
                 ; Type = type_variable(_, _)
                 ; Type = kinded_type(_, _)
diff --git a/compiler/hhf.m b/compiler/hhf.m
index 9b7bfc0..2172b61 100644
--- a/compiler/hhf.m
+++ b/compiler/hhf.m
@@ -493,13 +493,9 @@ same_type_2(type_variable(_, _), type_variable(_, _)).
 same_type_2(defined_type(Name, ArgsA, _), defined_type(Name, ArgsB, _)) :-
     same_type_list(ArgsA, ArgsB).
 same_type_2(builtin_type(BuiltinType), builtin_type(BuiltinType)).
-same_type_2(higher_order_type(ArgsA, no, Purity, EvalMethod),
-        higher_order_type(ArgsB, no, Purity, EvalMethod)) :-
+same_type_2(higher_order_type(PorF, ArgsA, HOInstInfo, Purity, EvalMethod),
+        higher_order_type(PorF, ArgsB, HOInstInfo, Purity, EvalMethod)) :-
     same_type_list(ArgsA, ArgsB).
-same_type_2(higher_order_type(ArgsA, yes(RetA), Purity, EvalMethod),
-        higher_order_type(ArgsB, yes(RetB), Purity, EvalMethod)) :-
-    same_type_list(ArgsA, ArgsB),
-    same_type(RetA, RetB).
 same_type_2(tuple_type(ArgsA, _), tuple_type(ArgsB, _)) :-
     same_type_list(ArgsA, ArgsB).
 same_type_2(apply_n_type(_, ArgsA, _), apply_n_type(_, ArgsB, _)) :-
diff --git a/compiler/higher_order.m b/compiler/higher_order.m
index aea253f..2231f53 100644
--- a/compiler/higher_order.m
+++ b/compiler/higher_order.m
@@ -3374,7 +3374,7 @@ update_type_info_locn(Var, ConstraintType, Index, Index + 1, !RttiVarMaps) :-
         ( ConstraintType = defined_type(_, _, _)
         ; ConstraintType = builtin_type(_)
         ; ConstraintType = tuple_type(_, _)
-        ; ConstraintType = higher_order_type(_, _, _, _)
+        ; ConstraintType = higher_order_type(_, _, _, _, _)
         ; ConstraintType = apply_n_type(_, _, _)
         ; ConstraintType = kinded_type(_, _)
         )
diff --git a/compiler/hlds_out_mode.m b/compiler/hlds_out_mode.m
index caf4e1c..a1da480 100644
--- a/compiler/hlds_out_mode.m
+++ b/compiler/hlds_out_mode.m
@@ -35,16 +35,6 @@
 
 %-----------------------------------------------------------------------------%
 
-    % Convert a mode or inst to a term representation.
-    %
-:- func mode_to_term(output_lang, mer_mode) = prog_term.
-:- func mode_to_term_with_context(output_lang, prog_context, mer_mode)
-    = prog_term.
-:- func inst_to_term(output_lang, mer_inst) = prog_term.
-:- func inst_name_to_term(output_lang, inst_name) = prog_term.
-
-%-----------------------------------------------------------------------------%
-
 :- type incl_addr
     --->    do_not_incl_addr
     ;       do_incl_addr.
@@ -91,19 +81,17 @@
 
 :- implementation.
 
-:- import_module mdbcomp.
-:- import_module mdbcomp.prim_data.
-:- import_module mdbcomp.sym_name.
+:- import_module check_hlds.
+:- import_module check_hlds.mode_util.
 :- import_module parse_tree.mercury_to_mercury.
 :- import_module parse_tree.parse_tree_out_inst.
 :- import_module parse_tree.parse_tree_out_term.
-:- import_module parse_tree.prog_io_type_name.
+:- import_module parse_tree.unparse.
 :- import_module parse_tree.prog_util.
 
 :- import_module bool.
 :- import_module int.
 :- import_module pair.
-:- import_module require.
 :- import_module set.
 :- import_module string.
 :- import_module term.
@@ -111,13 +99,6 @@
 
 %-----------------------------------------------------------------------------%
 
-:- func make_atom(prog_context, string) = prog_term.
-
-make_atom(Context, Name) =
-    term.functor(term.atom(Name), [], Context).
-
-%-----------------------------------------------------------------------------%
-
 write_instmap(VarSet, AppendVarNums, Indent, InstMap, !IO) :-
     ( if instmap_is_unreachable(InstMap) then
         io.write_string("unreachable", !IO)
@@ -144,580 +125,6 @@ write_var_inst_list(VarSet, AppendVarNums, Indent, [Var - Inst | VarsInsts],
 
 %-----------------------------------------------------------------------------%
 
-mode_to_term(Lang, Mode) =
-    mode_to_term_with_context(Lang, term.context_init, Mode).
-
-mode_to_term_with_context(Lang, Context, Mode) = Term :-
-    (
-        Mode = (InstA -> InstB),
-        ( if
-            % Check for higher-order pred or func modes, and output them
-            % in a nice format.
-            InstA = ground(_Uniq, higher_order(_)),
-            InstB = InstA
-        then
-            Term = inst_to_term_with_context(Lang, Context, InstA)
-        else
-            construct_qualified_term_with_context(unqualified(">>"),
-                [inst_to_term_with_context(Lang, Context, InstA),
-                inst_to_term_with_context(Lang, Context, InstB)],
-                Context, Term)
-        )
-    ;
-        Mode = user_defined_mode(Name, Args),
-        construct_qualified_term_with_context(Name,
-            list.map(inst_to_term_with_context(Lang, Context), Args),
-            Context, Term)
-    ).
-
-inst_to_term(Lang, Inst) =
-    inst_to_term_with_context(Lang, term.context_init, Inst).
-
-:- func inst_to_term_with_context(output_lang, prog_context, mer_inst)
-    = prog_term.
-
-inst_to_term_with_context(Lang, Context, Inst) = Term :-
-    (
-        Inst = any(Uniq, HOInstInfo),
-        (
-            HOInstInfo = higher_order(PredInstInfo),
-            Term = any_pred_inst_info_to_term(Lang, Context, Uniq,
-                PredInstInfo)
-        ;
-            HOInstInfo = none_or_default_func,
-            Term = make_atom(Context, any_inst_uniqueness(Uniq))
-        )
-    ;
-        Inst = free,
-        Term = make_atom(Context, "free")
-    ;
-        Inst = free(Type),
-        unparse_type(Type, Term0),
-        Term1 = term.coerce(Term0),
-        Term = term.functor(term.atom("free"), [Term1], Context)
-    ;
-        Inst = bound(Uniq, InstResults, BoundInsts),
-        (
-            Lang = output_mercury,
-            ArgTerms = [bound_insts_to_term(Lang, Context, BoundInsts)]
-        ;
-            Lang = output_debug,
-            ArgTerms =
-                [inst_test_results_to_term(Context, InstResults),
-                bound_insts_to_term(Lang, Context, BoundInsts)]
-        ),
-        construct_qualified_term_with_context(
-            unqualified(inst_uniqueness(Uniq, "bound")),
-            ArgTerms, Context, Term)
-    ;
-        Inst = ground(Uniq, HOInstInfo),
-        (
-            HOInstInfo = higher_order(PredInstInfo),
-            Term = ground_pred_inst_info_to_term(Lang, Context, Uniq,
-                PredInstInfo)
-        ;
-            HOInstInfo = none_or_default_func,
-            Term = make_atom(Context, inst_uniqueness(Uniq, "ground"))
-        )
-    ;
-        Inst = inst_var(Var),
-        Term = term.coerce(term.variable(Var, context_init))
-    ;
-        Inst = constrained_inst_vars(Vars, SubInst),
-        Term = set.fold(func(Var, VarTerm) =
-                term.functor(term.atom("=<"),
-                    [term.coerce(term.variable(Var, context_init)), VarTerm],
-                    Context),
-            Vars, inst_to_term_with_context(Lang, Context, SubInst))
-    ;
-        Inst = abstract_inst(Name, Args),
-        Term = inst_name_to_term_with_context(Lang, Context,
-            user_inst(Name, Args))
-    ;
-        Inst = defined_inst(InstName),
-        Term = inst_name_to_term_with_context(Lang, Context, InstName)
-    ;
-        Inst = not_reached,
-        Term = make_atom(Context, "not_reached")
-    ).
-
-:- func inst_test_results_to_term(prog_context, inst_test_results) = prog_term.
-
-inst_test_results_to_term(Context, InstResults) = Term :-
-    (
-        InstResults = inst_test_results(GroundnessResult, AnyResult,
-            InstNamesResult, InstVarsResult, TypeResult, PropagatedResult),
-        SubTerm1 = inst_result_groundness_to_term(Context, GroundnessResult),
-        SubTerm2 = inst_result_contains_any_to_term(Context, AnyResult),
-        SubTerm3 = inst_result_contains_inst_names_to_term(Context,
-            InstNamesResult),
-        SubTerm4 = inst_result_contains_inst_vars_to_term(Context,
-            InstVarsResult),
-        SubTerm5 = inst_result_contains_types_to_term(Context, TypeResult),
-        SubTerm6 = inst_result_type_ctor_propagated_to_term(Context,
-            PropagatedResult),
-        Term = term.functor(term.atom("results"),
-            [SubTerm1, SubTerm2, SubTerm3, SubTerm4, SubTerm5, SubTerm6],
-            Context)
-    ;
-        InstResults = inst_test_no_results,
-        Term = term.functor(term.atom("no_results"), [], Context)
-    ;
-        InstResults = inst_test_results_fgtc,
-        Term = term.functor(term.atom("fgtc"), [], Context)
-    ).
-
-:- func inst_result_groundness_to_term(prog_context, inst_result_groundness)
-    = prog_term.
-
-inst_result_groundness_to_term(Context, Groundness) = Term :-
-    (
-        Groundness = inst_result_is_not_ground,
-        Term = term.functor(term.atom("is_not_ground"), [], Context)
-    ;
-        Groundness = inst_result_is_ground,
-        Term = term.functor(term.atom("is_ground"), [], Context)
-    ;
-        Groundness = inst_result_groundness_unknown,
-        Term = term.functor(term.atom("groundness_unknown"), [], Context)
-    ).
-
-:- func inst_result_contains_any_to_term(prog_context,
-    inst_result_contains_any) = prog_term.
-
-inst_result_contains_any_to_term(Context, ContainsAny) = Term :-
-    (
-        ContainsAny = inst_result_does_not_contain_any,
-        Term = term.functor(term.atom("does_not_contain_any"), [], Context)
-    ;
-        ContainsAny = inst_result_does_contain_any,
-        Term = term.functor(term.atom("does_contain_any"), [], Context)
-    ;
-        ContainsAny = inst_result_contains_any_unknown,
-        Term = term.functor(term.atom("contains_any_unknown"), [], Context)
-    ).
-
-:- func inst_result_contains_inst_names_to_term(prog_context,
-    inst_result_contains_inst_names) = prog_term.
-
-inst_result_contains_inst_names_to_term(Context, ContainsInstNames) = Term :-
-    (
-        ContainsInstNames = inst_result_contains_inst_names_unknown,
-        Term = term.functor(term.atom("contains_inst_names_unknown"),
-            [], Context)
-    ;
-        ContainsInstNames = inst_result_contains_inst_names_known(InstNameSet),
-        % Inst names can be pretty big, so we print only a count.
-        % If necessary, we can later modify this code to actually print them.
-        set.count(InstNameSet, NumInstNames),
-        CountTerm = term.functor(term.integer(NumInstNames), [], Context),
-        Term = term.functor(term.atom("contains_inst_names_known"),
-            [CountTerm], Context)
-    ).
-
-:- func inst_result_contains_inst_vars_to_term(prog_context,
-    inst_result_contains_inst_vars) = prog_term.
-
-inst_result_contains_inst_vars_to_term(Context, ContainsInstVars) = Term :-
-    (
-        ContainsInstVars = inst_result_contains_inst_vars_unknown,
-        Term = term.functor(term.atom("contains_inst_vars_unknown"),
-            [], Context)
-    ;
-        ContainsInstVars = inst_result_contains_inst_vars_known(InstVarSet),
-        set.to_sorted_list(InstVarSet, InstVars),
-        InstVarTerms = list.map(inst_var_to_term(Context), InstVars),
-        Term = term.functor(term.atom("contains_inst_vars_known"),
-            InstVarTerms, Context)
-    ).
-
-:- func inst_var_to_term(prog_context, inst_var) = prog_term.
-
-inst_var_to_term(Context, InstVar) = Term :-
-    InstVarNum = term.var_to_int(InstVar),
-    InstVarNumStr = string.int_to_string(InstVarNum),
-    Term = term.functor(string("inst_var_" ++ InstVarNumStr), [], Context).
-
-:- func inst_result_contains_types_to_term(prog_context,
-    inst_result_contains_types) = prog_term.
-
-inst_result_contains_types_to_term(Context, ContainsTypes) = Term :-
-    (
-        ContainsTypes = inst_result_contains_types_unknown,
-        Term = term.functor(term.atom("contains_types_unknown"), [], Context)
-    ;
-        ContainsTypes = inst_result_contains_types_known(TypeCtorSet),
-        set.to_sorted_list(TypeCtorSet, TypeCtors),
-        TypeCtorTerms = list.map(type_ctor_to_term(Context), TypeCtors),
-        Term = term.functor(term.atom("contains_types_known"),
-            TypeCtorTerms, Context)
-    ).
-
-:- func inst_result_type_ctor_propagated_to_term(prog_context,
-    inst_result_type_ctor_propagated) = prog_term.
-
-inst_result_type_ctor_propagated_to_term(Context, PropagatedResult) = Term :-
-    (
-        PropagatedResult = inst_result_no_type_ctor_propagated,
-        Term = term.functor(term.atom("no_type_ctor_propagated"), [], Context)
-    ;
-        PropagatedResult = inst_result_type_ctor_propagated(TypeCtor),
-        Term = term.functor(term.atom("type_ctor_propagated"),
-            [type_ctor_to_term(Context, TypeCtor)], Context)
-    ).
-
-:- func type_ctor_to_term(prog_context, type_ctor) = prog_term.
-
-type_ctor_to_term(Context, TypeCtor) = Term :-
-    TypeCtor = type_ctor(SymName, Arity),
-    string.format("%s/%d", [s(sym_name_to_string(SymName)), i(Arity)],
-        ConsName),
-    Term = term.functor(term.atom(ConsName), [], Context).
-
-:- func ground_pred_inst_info_to_term(output_lang, prog_context, uniqueness,
-    pred_inst_info) = prog_term.
-
-ground_pred_inst_info_to_term(Lang, Context, _Uniq, PredInstInfo) = Term :-
-    % XXX we ignore Uniq
-    PredInstInfo = pred_inst_info(PredOrFunc, Modes, _, Det),
-    (
-        PredOrFunc = pf_predicate,
-        construct_qualified_term_with_context(unqualified("pred"),
-            list.map(mode_to_term_with_context(Lang, Context), Modes),
-            Context, ModesTerm)
-    ;
-        PredOrFunc = pf_function,
-        pred_args_to_func_args(Modes, ArgModes, RetMode),
-        construct_qualified_term_with_context(unqualified("func"),
-            list.map(mode_to_term_with_context(Lang, Context), ArgModes),
-            Context, ArgModesTerm),
-        construct_qualified_term_with_context(unqualified("="),
-            [ArgModesTerm, mode_to_term_with_context(Lang, Context, RetMode)],
-            Context, ModesTerm)
-    ),
-    construct_qualified_term_with_context(unqualified("is"),
-        [ModesTerm, det_to_term(Context, Det)], Context, Term).
-
-:- func any_pred_inst_info_to_term(output_lang, prog_context, uniqueness,
-    pred_inst_info) = prog_term.
-
-any_pred_inst_info_to_term(Lang, Context, _Uniq, PredInstInfo) = Term :-
-    % XXX we ignore Uniq
-    PredInstInfo = pred_inst_info(PredOrFunc, Modes, _, Det),
-    (
-        PredOrFunc = pf_predicate,
-        construct_qualified_term_with_context(unqualified("any_pred"),
-            list.map(mode_to_term_with_context(Lang, Context), Modes),
-            Context, ModesTerm)
-    ;
-        PredOrFunc = pf_function,
-        pred_args_to_func_args(Modes, ArgModes, RetMode),
-        construct_qualified_term_with_context(unqualified("any_func"),
-            list.map(mode_to_term_with_context(Lang, Context), ArgModes),
-            Context, ArgModesTerm),
-        construct_qualified_term_with_context(unqualified("="),
-            [ArgModesTerm, mode_to_term_with_context(Lang, Context, RetMode)],
-            Context, ModesTerm)
-    ),
-    construct_qualified_term_with_context(unqualified("is"),
-        [ModesTerm, det_to_term(Context, Det)], Context, Term).
-
-inst_name_to_term(Lang, InstName) =
-    inst_name_to_term_with_context(Lang, term.context_init, InstName).
-
-:- func inst_name_to_term_with_context(output_lang, prog_context, inst_name)
-    = prog_term.
-
-inst_name_to_term_with_context(Lang, Context, InstName) = Term :-
-    (
-        InstName = user_inst(Name, Args),
-        construct_qualified_term_with_context(Name,
-            list.map(inst_to_term_with_context(Lang, Context), Args),
-            Context, Term)
-    ;
-        InstName = unify_inst(Liveness, Real, InstA, InstB),
-        (
-            Lang = output_mercury,
-            unexpected($module, $pred, "unify_inst")
-        ;
-            Lang = output_debug,
-            construct_qualified_term_with_context(unqualified("$unify"),
-                [make_atom(Context, is_live_to_str(Liveness)),
-                make_atom(Context, unify_is_real_to_str(Real)),
-                inst_to_term_with_context(Lang, Context, InstA),
-                inst_to_term_with_context(Lang, Context, InstB)],
-                Context, Term)
-        )
-    ;
-        InstName = merge_inst(InstA, InstB),
-        (
-            Lang = output_mercury,
-            unexpected($module, $pred, "merge_inst")
-        ;
-            Lang = output_debug,
-            construct_qualified_term_with_context(unqualified("$merge_inst"),
-                list.map(inst_to_term_with_context(Lang, Context),
-                [InstA, InstB]),
-                Context, Term)
-        )
-    ;
-        InstName = ground_inst(SubInstName, Uniq, IsLive, Real),
-        (
-            Lang = output_mercury,
-            unexpected($module, $pred, "ground_inst")
-        ;
-            Lang = output_debug,
-            construct_qualified_term_with_context(unqualified("$ground"),
-                [inst_name_to_term_with_context(Lang, Context, SubInstName),
-                make_atom(Context, inst_uniqueness(Uniq, "shared")),
-                make_atom(Context, is_live_to_str(IsLive)),
-                make_atom(Context, unify_is_real_to_str(Real))],
-                Context, Term)
-        )
-    ;
-        InstName = any_inst(SubInstName, Uniq, IsLive, Real),
-        (
-            Lang = output_mercury,
-            unexpected($module, $pred, "any_inst")
-        ;
-            Lang = output_debug,
-            construct_qualified_term_with_context(unqualified("$any"),
-                [inst_name_to_term_with_context(Lang, Context, SubInstName),
-                make_atom(Context, inst_uniqueness(Uniq, "shared")),
-                make_atom(Context, is_live_to_str(IsLive)),
-                make_atom(Context, unify_is_real_to_str(Real))],
-                Context, Term)
-        )
-    ;
-        InstName = shared_inst(SubInstName),
-        (
-            Lang = output_mercury,
-            unexpected($module, $pred, "shared_inst")
-        ;
-            Lang = output_debug,
-            construct_qualified_term_with_context(unqualified("$shared_inst"),
-                [inst_name_to_term_with_context(Lang, Context, SubInstName)],
-                Context, Term)
-        )
-    ;
-        InstName = mostly_uniq_inst(SubInstName),
-        (
-            Lang = output_mercury,
-            unexpected($module, $pred, "mostly_uniq_inst")
-        ;
-            Lang = output_debug,
-            construct_qualified_term_with_context(
-                unqualified("$mostly_uniq_inst"),
-                [inst_name_to_term_with_context(Lang, Context, SubInstName)],
-                Context, Term)
-        )
-    ;
-        InstName = typed_ground(Uniq, Type),
-        (
-            Lang = output_mercury,
-            unexpected($module, $pred, "typed_ground")
-        ;
-            Lang = output_debug,
-            unparse_type(Type, Term0),
-            construct_qualified_term_with_context(unqualified("$typed_ground"),
-                [make_atom(Context, inst_uniqueness(Uniq, "shared")),
-                term.coerce(Term0)],
-                Context, Term)
-        )
-    ;
-        InstName = typed_inst(Type, SubInstName),
-        (
-            Lang = output_mercury,
-            % Inst names in the inst tables can (and often do) have the types
-            % they apply pushed into them by inst_user.m. However, the typed
-            % nature of such inst names cannot (yet) be expressed in Mercury
-            % source code.
-            Term = inst_name_to_term_with_context(Lang, Context, SubInstName)
-        ;
-            Lang = output_debug,
-            unparse_type(Type, Term0),
-            construct_qualified_term_with_context(unqualified("$typed_inst"),
-                [term.coerce(Term0),
-                inst_name_to_term_with_context(Lang, Context, SubInstName)],
-                Context, Term)
-        )
-    ).
-
-:- func is_live_to_str(is_live) = string.
-
-is_live_to_str(is_live) = "live".
-is_live_to_str(is_dead) = "dead".
-
-:- func unify_is_real_to_str(unify_is_real) = string.
-
-unify_is_real_to_str(real_unify) = "real".
-unify_is_real_to_str(fake_unify) = "fake".
-
-:- func any_inst_uniqueness(uniqueness) = string.
-
-any_inst_uniqueness(shared) = "any".
-any_inst_uniqueness(unique) = "unique_any".
-any_inst_uniqueness(mostly_unique) = "mostly_unique_any".
-any_inst_uniqueness(clobbered) = "clobbered_any".
-any_inst_uniqueness(mostly_clobbered) = "mostly_clobbered_any".
-
-:- func inst_uniqueness(uniqueness, string) = string.
-
-inst_uniqueness(shared, SharedName) = SharedName.
-inst_uniqueness(unique, _) = "unique".
-inst_uniqueness(mostly_unique, _) = "mostly_unique".
-inst_uniqueness(clobbered, _) = "clobbered".
-inst_uniqueness(mostly_clobbered, _) = "mostly_clobbered".
-
-:- func bound_insts_to_term(output_lang, prog_context, list(bound_inst))
-    = prog_term.
-
-bound_insts_to_term(_, Context, []) =
-    % This shouldn't happen, but when it does, the problem is a LOT easier
-    % to debug if there is a HLDS dump you can read.
-    term.functor(term.atom("EMPTY_BOUND_INSTS"), [], Context).
-bound_insts_to_term(Lang, Context, [BoundInst | BoundInsts]) =
-    bound_insts_to_term_2(Lang, Context, BoundInst, BoundInsts).
-
-:- func bound_insts_to_term_2(output_lang, prog_context,
-    bound_inst, list(bound_inst)) = prog_term.
-
-bound_insts_to_term_2(Lang, Context, BoundInst, BoundInsts) = Term :-
-    BoundInst = bound_functor(ConsId, Args),
-    ArgTerms = list.map(inst_to_term_with_context(Lang, Context), Args),
-    cons_id_and_args_to_term_full(ConsId, ArgTerms, FirstTerm),
-    (
-        BoundInsts = [],
-        Term = FirstTerm
-    ;
-        BoundInsts = [HeadBoundInst | TailBoundInsts],
-        SecondTerm = bound_insts_to_term_2(Lang, Context,
-            HeadBoundInst, TailBoundInsts),
-        construct_qualified_term_with_context(unqualified(";"),
-            [FirstTerm, SecondTerm], Context, Term)
-    ).
-
-:- pred cons_id_and_args_to_term_full(cons_id::in, list(prog_term)::in,
-    prog_term::out) is det.
-
-cons_id_and_args_to_term_full(ConsId, ArgTerms, Term) :-
-    (
-        ConsId = cons(SymName, _Arity, _TypeCtor),
-        construct_qualified_term(SymName, ArgTerms, Term)
-    ;
-        ConsId = tuple_cons(_Arity),
-        SymName = unqualified("{}"),
-        construct_qualified_term(SymName, ArgTerms, Term)
-    ;
-        ConsId = closure_cons(_, _),
-        term.context_init(Context),
-        FunctorName = "closure_cons",
-        Term = term.functor(term.string(FunctorName), [], Context)
-    ;
-        ConsId = int_const(Int),
-        term.context_init(Context),
-        Term = term.functor(term.integer(Int), [], Context)
-    ;
-        ConsId = float_const(Float),
-        term.context_init(Context),
-        Term = term.functor(term.float(Float), [], Context)
-    ;
-        ConsId = string_const(String),
-        term.context_init(Context),
-        Term = term.functor(term.string(String), [], Context)
-    ;
-        ConsId = char_const(Char),
-        SymName = unqualified(string.from_char(Char)),
-        construct_qualified_term(SymName, [], Term)
-    ;
-        ConsId = impl_defined_const(String),
-        term.context_init(Context),
-        FunctorName = "ImplDefinedConst: " ++ String,
-        Term = term.functor(term.string(FunctorName), [], Context)
-    ;
-        ConsId = type_ctor_info_const(ModuleName, TypeCtorName, Arity),
-        term.context_init(Context),
-        string.format("TypeCtorInfo for %s.%s/%d",
-            [s(sym_name_to_string(ModuleName)), s(TypeCtorName), i(Arity)],
-            FunctorName),
-        Term = term.functor(term.string(FunctorName), [], Context)
-    ;
-        ConsId = base_typeclass_info_const(_, _, _, _),
-        term.context_init(Context),
-        FunctorName = "base_typeclass_info_const",
-        Term = term.functor(term.string(FunctorName), [], Context)
-    ;
-        ConsId = type_info_cell_constructor(TypeCtor),
-        TypeCtor = type_ctor(TypeCtorName, Arity),
-        term.context_init(Context),
-        string.format("type_info_cell_constructor for %s/%d",
-            [s(sym_name_to_string(TypeCtorName)), i(Arity)], FunctorName),
-        Term = term.functor(term.string(FunctorName), [], Context)
-    ;
-        ConsId = typeclass_info_cell_constructor,
-        term.context_init(Context),
-        FunctorName = "typeclass_info_cell_constructor",
-        Term = term.functor(term.string(FunctorName), [], Context)
-    ;
-        ConsId = type_info_const(TIConstNum),
-        expect(unify(ArgTerms, []), $module, $pred,
-            "type_info_const arity != 0"),
-        term.context_init(Context),
-        FunctorName = "type_info_const",
-        Arg = term.functor(term.integer(TIConstNum), [], Context),
-        Term = term.functor(term.string(FunctorName), [Arg], Context)
-    ;
-        ConsId = typeclass_info_const(TCIConstNum),
-        expect(unify(ArgTerms, []), $module, $pred,
-            "typeclass_info_const arity != 0"),
-        term.context_init(Context),
-        FunctorName = "typeclass_info_const",
-        Arg = term.functor(term.integer(TCIConstNum), [], Context),
-        Term = term.functor(term.string(FunctorName), [Arg], Context)
-    ;
-        ConsId = ground_term_const(TCIConstNum, SubConsId),
-        expect(unify(ArgTerms, []), $module, $pred,
-            "ground_term_const arity != 0"),
-        cons_id_and_args_to_term_full(SubConsId, [], SubArg),
-        term.context_init(Context),
-        FunctorName = "ground_term_const",
-        NumArg = term.functor(term.integer(TCIConstNum), [], Context),
-        Term = term.functor(term.string(FunctorName), [NumArg, SubArg],
-            Context)
-    ;
-        ConsId = tabling_info_const(_),
-        term.context_init(Context),
-        FunctorName = "tabling_info_const",
-        Term = term.functor(term.string(FunctorName), [], Context)
-    ;
-        ConsId = table_io_entry_desc(_),
-        term.context_init(Context),
-        FunctorName = "table_io_entry_desc",
-        Term = term.functor(term.string(FunctorName), [], Context)
-    ;
-        ConsId = deep_profiling_proc_layout(_),
-        term.context_init(Context),
-        FunctorName = "deep_profiling_proc_layout",
-        Term = term.functor(term.string(FunctorName), [], Context)
-    ).
-
-:- func det_to_term(prog_context, determinism) = prog_term.
-
-det_to_term(Context, Det) = make_atom(Context, det_to_string(Det)).
-
-:- func det_to_string(determinism) = string.
-
-det_to_string(detism_erroneous) = "erroneous".
-det_to_string(detism_failure) = "failure".
-det_to_string(detism_det) = "det".
-det_to_string(detism_semi) = "semidet".
-det_to_string(detism_cc_multi) = "cc_multi".
-det_to_string(detism_cc_non) = "cc_nondet".
-det_to_string(detism_multi) = "multi".
-det_to_string(detism_non) = "nondet".
-
-%-----------------------------------------------------------------------------%
-
 mercury_output_structured_uni_mode_list(Insts, Indent, Lang, InclAddr,
         InstVarSet, !IO) :-
     mercury_format_structured_uni_mode_list(Insts, 1, Indent, Lang, InclAddr,
diff --git a/compiler/hlds_out_module.m b/compiler/hlds_out_module.m
index 3cdbdbe..83506c5 100644
--- a/compiler/hlds_out_module.m
+++ b/compiler/hlds_out_module.m
@@ -60,6 +60,7 @@
 :- import_module parse_tree.parse_tree_out_term.
 :- import_module parse_tree.prog_item.
 :- import_module parse_tree.prog_out.
+:- import_module parse_tree.unparse.
 
 :- import_module assoc_list.
 :- import_module bool.
diff --git a/compiler/hlds_out_pred.m b/compiler/hlds_out_pred.m
index f802d3b..0fd80ff 100644
--- a/compiler/hlds_out_pred.m
+++ b/compiler/hlds_out_pred.m
@@ -82,7 +82,6 @@
 :- import_module hlds.hlds_goal.
 :- import_module hlds.hlds_llds.
 :- import_module hlds.hlds_out.hlds_out_goal.
-:- import_module hlds.hlds_out.hlds_out_mode.
 :- import_module hlds.hlds_rtti.
 :- import_module mdbcomp.goal_path.
 :- import_module mdbcomp.program_representation.
@@ -95,6 +94,7 @@
 :- import_module parse_tree.prog_out.
 :- import_module parse_tree.prog_util.
 :- import_module parse_tree.set_of_var.
+:- import_module parse_tree.unparse.
 
 :- import_module assoc_list.
 :- import_module bool.
diff --git a/compiler/hlds_rtti.m b/compiler/hlds_rtti.m
index 45daf31..912e4f5 100644
--- a/compiler/hlds_rtti.m
+++ b/compiler/hlds_rtti.m
@@ -772,7 +772,7 @@ apply_substs_to_ti_map(TRenaming, TSubst, Subst, TVar, Locn, !Map) :-
         ( NewType = builtin_type(_)
         ; NewType = defined_type(_, _, _)
         ; NewType = tuple_type(_, _)
-        ; NewType = higher_order_type(_, _, _, _)
+        ; NewType = higher_order_type(_, _, _, _, _)
         ; NewType = apply_n_type(_, _, _)
         ; NewType = kinded_type(_, _)
         )
diff --git a/compiler/inst_util.m b/compiler/inst_util.m
index bb417df..ba5db73 100644
--- a/compiler/inst_util.m
+++ b/compiler/inst_util.m
@@ -484,7 +484,8 @@ abstractly_unify_inst_3(Live, InstA, InstB, Real, Inst, Detism, !ModuleInfo) :-
                 InstB = ground(UniqB, _HOInstInfoB),
                 % It is an error to unify higher-order preds,
                 % so if Real \= fake_unify, then we must fail.
-                Real = fake_unify,
+                % XXX but this results in mode errors in unify procs
+                % Real = fake_unify,
                 % In theory we should choose take the union of the information
                 % specified by PredInstA and _HOInstInfoB. However, since
                 % our data representation provides no way of doing that, and
@@ -726,6 +727,7 @@ abstractly_unify_inst_functor_2(Live, InstA, ConsIdB, ArgInstsB, ArgLives,
             Live = is_dead,
             ArgInsts = ArgInstsB
         ),
+        arg_insts_match_ctor_subtypes(ArgInsts, ConsIdB, Type, !.ModuleInfo),
         % XXX A better approximation of InstResults is probably possible.
         Inst = bound(unique, inst_test_no_results,
             [bound_functor(ConsIdB, ArgInsts)]),
@@ -766,12 +768,14 @@ abstractly_unify_inst_functor_2(Live, InstA, ConsIdB, ArgInstsB, ArgLives,
         (
             Live = is_live,
             make_ground_inst_list_lives(ArgInstsB, Live, ArgLives, UniqA, Real,
-                ArgInsts, Detism, !ModuleInfo)
+                ArgInsts0, Detism, !ModuleInfo)
         ;
             Live = is_dead,
             make_ground_inst_list(ArgInstsB, Live, UniqA, Real,
-                ArgInsts, Detism, !ModuleInfo)
+                ArgInsts0, Detism, !ModuleInfo)
         ),
+        propagate_ctor_subtypes_into_arg_insts(ConsIdB, Type,
+            ArgInsts0, ArgInsts, !.ModuleInfo),
         % XXX A better approximation of InstResults is probably possible.
         Inst = bound(UniqA, inst_test_no_results,
             [bound_functor(ConsIdB, ArgInsts)])
@@ -961,6 +965,101 @@ abstractly_unify_constrained_inst_vars(Live, InstVarsA, SubInstA, InstB,
     ).
 
 %---------------------------------------------------------------------------%
+
+:- pred arg_insts_match_ctor_subtypes(list(mer_inst)::in, cons_id::in,
+    mer_type::in, module_info::in) is semidet.
+
+arg_insts_match_ctor_subtypes(ArgInsts, ConsId, Type, ModuleInfo) :-
+    ( if
+        type_to_ctor(Type, TypeCtor),
+        get_cons_defn(ModuleInfo, TypeCtor, ConsId, ConsDefn),
+        ConsDefn = hlds_cons_defn(_, _, _, _, ExistQVars, _, ConsArgs, _),
+        % Some builtin types have constructors with arguments that are not
+        % reflected in the constructor definition, and which return an
+        % empty list.
+        ConsArgs = [_ | _],
+        % XXX Handle existentially quantified constructors.
+        ExistQVars = []
+    then
+        arg_insts_match_ctor_subtypes_2(ArgInsts, ConsArgs, ModuleInfo)
+    else
+        true
+    ).
+
+:- pred arg_insts_match_ctor_subtypes_2(list(mer_inst)::in,
+    list(constructor_arg)::in, module_info::in) is semidet.
+
+arg_insts_match_ctor_subtypes_2([], [], _).
+arg_insts_match_ctor_subtypes_2([Inst | Insts], [ConsArg | ConsArgs],
+        ModuleInfo) :-
+    ( if
+        ( Inst = ground(_, HOInstInfo)
+        ; Inst = any(_, HOInstInfo)
+        ),
+        ConsArg ^ arg_type = higher_order_type(_, _, TypeHOInstInfo, _, _),
+        TypeHOInstInfo = higher_order(TypePredInst)
+    then
+        HOInstInfo = higher_order(PredInst),
+        pred_inst_matches(PredInst, TypePredInst, ModuleInfo)
+    else
+        true
+    ),
+    arg_insts_match_ctor_subtypes_2(Insts, ConsArgs, ModuleInfo).
+arg_insts_match_ctor_subtypes_2([], [_ | _], _) :-
+    unexpected($module, $pred, "length mismatch").
+arg_insts_match_ctor_subtypes_2([_ | _], [], _) :-
+    unexpected($module, $pred, "length mismatch").
+
+%---------------------------------------------------------------------------%
+
+:- pred propagate_ctor_subtypes_into_arg_insts(cons_id::in, mer_type::in,
+    list(mer_inst)::in, list(mer_inst)::out, module_info::in) is det.
+
+propagate_ctor_subtypes_into_arg_insts(ConsId, Type, !ArgInsts, ModuleInfo) :-
+    ( if
+        type_to_ctor(Type, TypeCtor),
+        get_cons_defn(ModuleInfo, TypeCtor, ConsId, ConsDefn),
+        ConsDefn = hlds_cons_defn(_, _, _, _, ExistQVars, _, ConsArgs, _),
+        % Some builtin types have constructors with arguments that are not
+        % reflected in the constructor definition, and which return an
+        % empty list.
+        ConsArgs = [_ | _],
+        % XXX Handle existentially quantified constructors.
+        ExistQVars = []
+    then
+        propagate_ctor_subtypes_into_arg_insts_2(ConsArgs, !ArgInsts)
+    else
+        true
+    ).
+
+:- pred propagate_ctor_subtypes_into_arg_insts_2(list(constructor_arg)::in,
+    list(mer_inst)::in, list(mer_inst)::out) is det.
+
+propagate_ctor_subtypes_into_arg_insts_2([], [], []).
+propagate_ctor_subtypes_into_arg_insts_2([ConsArg | ConsArgs],
+        [Inst0 | Insts0], [Inst | Insts]) :-
+    ( if
+        ConsArg ^ arg_type = higher_order_type(_, _, TypeHOInstInfo, _, _),
+        TypeHOInstInfo = higher_order(_),
+        (
+            Inst0 = ground(Uniq, _),
+            Inst1 = ground(Uniq, TypeHOInstInfo)
+        ;
+            Inst0 = any(Uniq, _),
+            Inst1 = any(Uniq, TypeHOInstInfo)
+        )
+    then
+        Inst = Inst1
+    else
+        Inst = Inst0
+    ),
+    propagate_ctor_subtypes_into_arg_insts_2(ConsArgs, Insts0, Insts).
+propagate_ctor_subtypes_into_arg_insts_2([], [_ | _], _) :-
+    unexpected($module, $pred, "length mismatch").
+propagate_ctor_subtypes_into_arg_insts_2([_ | _], [], _) :-
+    unexpected($module, $pred, "length mismatch").
+
+%---------------------------------------------------------------------------%
 %---------------------------------------------------------------------------%
 
     % Unifying shared with either shared or unique gives shared.
diff --git a/compiler/mercury_to_mercury.m b/compiler/mercury_to_mercury.m
index f02c06f..3dbbc10 100644
--- a/compiler/mercury_to_mercury.m
+++ b/compiler/mercury_to_mercury.m
@@ -152,7 +152,7 @@
 
 :- implementation.
 
-:- import_module parse_tree.prog_io_type_name.
+:- import_module parse_tree.unparse.
 
 :- import_module bool.
 :- import_module char.
diff --git a/compiler/ml_unify_gen.m b/compiler/ml_unify_gen.m
index 1b445cb..3da0b6a 100644
--- a/compiler/ml_unify_gen.m
+++ b/compiler/ml_unify_gen.m
@@ -1245,7 +1245,7 @@ ml_gen_box_or_unbox_const_rval_hld(ModuleInfo, ArgType, FieldType, ArgRval,
         ( FieldType = defined_type(_, _, _)
         ; FieldType = builtin_type(_)
         ; FieldType = tuple_type(_, _)
-        ; FieldType = higher_order_type(_, _, _, _)
+        ; FieldType = higher_order_type(_, _, _, _, _)
         ; FieldType = apply_n_type(_, _, _)
         ; FieldType = kinded_type(_, _)
         ),
diff --git a/compiler/mlds_to_cs.m b/compiler/mlds_to_cs.m
index c0a810b..ce30a43 100644
--- a/compiler/mlds_to_cs.m
+++ b/compiler/mlds_to_cs.m
@@ -3347,6 +3347,9 @@ output_lval(Info, Lval, !IO) :-
             else if string.prefix(NameStr, "MR_SECTAG_") then
                 io.write_string("runtime.Sectag_Locn.", !IO),
                 io.write_string(NameStr, !IO)
+            else if string.prefix(NameStr, "MR_FUNCTOR_SUBTYPE_") then
+                io.write_string("runtime.FunctorSubtypeInfo.", !IO),
+                io.write_string(NameStr, !IO)
             else if NameStr = "MR_PREDICATE" then
                 io.write_string("runtime.Constants.MR_PREDICATE", !IO)
             else if NameStr = "MR_FUNCTION" then
diff --git a/compiler/modecheck_unify.m b/compiler/modecheck_unify.m
index da6c102..5bdeb20 100644
--- a/compiler/modecheck_unify.m
+++ b/compiler/modecheck_unify.m
@@ -1304,12 +1304,12 @@ categorize_unify_var_lambda(ModeOfX, ArgModes0, X, ArgVars, PredOrFunc,
                 PredName = pred_info_name(PredInfo),
                 mode_info_get_var_types(!.ModeInfo, VarTypes),
                 lookup_var_type(VarTypes, X, Type),
-                ( if Type = higher_order_type(_, MaybeReturnType, _, _) then
+                ( if Type = higher_order_type(PorF, _, _, _, _) then
                     (
-                        MaybeReturnType = no,
+                        PorF = pf_predicate,
                         RHSTypeCtor = type_ctor(unqualified("pred"), 0)
                     ;
-                        MaybeReturnType = yes(_),
+                        PorF = pf_function,
                         RHSTypeCtor = type_ctor(unqualified("func"), 0)
                     )
                 else
diff --git a/compiler/module_qual.qualify_items.m b/compiler/module_qual.qualify_items.m
index 24eb71a..2eaf617 100644
--- a/compiler/module_qual.qualify_items.m
+++ b/compiler/module_qual.qualify_items.m
@@ -484,13 +484,13 @@ qualify_type(InInt, ErrorContext, Type0, Type, !Info, !Specs) :-
         ),
         Type = Type0
     ;
-        Type0 = higher_order_type(Args0, MaybeRet0, Purity, EvalMethod),
+        Type0 = higher_order_type(PorF, Args0, HOInstInfo0, Purity, EvalMethod),
         % XXX We could pass a more specific error context.
         qualify_type_list(InInt, ErrorContext, Args0, Args, !Info, !Specs),
         % XXX We could pass a more specific error context.
-        qualify_maybe_type(InInt, ErrorContext, MaybeRet0, MaybeRet,
+        qualify_ho_inst_info(InInt, ErrorContext, HOInstInfo0, HOInstInfo,
             !Info, !Specs),
-        Type = higher_order_type(Args, MaybeRet, Purity, EvalMethod)
+        Type = higher_order_type(PorF, Args, HOInstInfo, Purity, EvalMethod)
     ;
         Type0 = tuple_type(Args0, Kind),
         % XXX We could pass a more specific error context.
diff --git a/compiler/parse_tree.m b/compiler/parse_tree.m
index d8eacaf..3974942 100644
--- a/compiler/parse_tree.m
+++ b/compiler/parse_tree.m
@@ -56,6 +56,7 @@
 :- include_module parse_tree_out_term.
 :- include_module parse_tree_out_info.
 :- include_module prog_out.
+:- include_module unparse.
 
 % Utility data structures.
 :- include_module set_of_var.
diff --git a/compiler/polymorphism.m b/compiler/polymorphism.m
index 93d49bd..2dc8338 100644
--- a/compiler/polymorphism.m
+++ b/compiler/polymorphism.m
@@ -3256,7 +3256,7 @@ polymorphism_do_make_type_info_var(Type, Context, VarMCA, ExtraGoals, !Info) :-
             ( Type = defined_type(_, _, _)
             ; Type = builtin_type(_)
             ; Type = tuple_type(_, _)
-            ; Type = higher_order_type(_,_, _, _)
+            ; Type = higher_order_type(_,_, _, _, _)
             ; Type = apply_n_type(_, _, _)
             ; Type = kinded_type(_, _)
             ),
diff --git a/compiler/prog_ctgc.m b/compiler/prog_ctgc.m
index 05ff417..cbb4123 100644
--- a/compiler/prog_ctgc.m
+++ b/compiler/prog_ctgc.m
@@ -229,7 +229,8 @@ parse_unit_selector(Term) = UnitSelector :-
             Args = [TypeSelectorTerm]
         then
             ( if
-                maybe_parse_type(term.coerce(TypeSelectorTerm), TypeSelector)
+                maybe_parse_type(no_allow_ho_inst_info,
+                    term.coerce(TypeSelectorTerm), TypeSelector)
             then
                 UnitSelector = typesel(TypeSelector)
             else
@@ -430,7 +431,7 @@ parse_user_annotated_sharing(!.Varset, Term, UserSharing) :-
             [TypesTerm, UserSharingTerm], _),
         (
             TypesTerm = term.functor(term.atom("yes"), ListTypeTerms, _),
-            maybe_parse_types(ListTypeTerms, Types),
+            maybe_parse_types(no_allow_ho_inst_info, ListTypeTerms, Types),
             term.vars_list(ListTypeTerms, TypeVars),
             varset.select(set.list_to_set(TypeVars), !Varset),
             MaybeUserTypes = yes(user_type_info(Types,
@@ -489,7 +490,7 @@ parse_user_annotated_datastruct_term(Term, Datastruct) :-
     VarTerm = term.variable(GenericVar, _),
     term.coerce_var(GenericVar, ProgVar),
     get_list_term_arguments(TypesTerm, TypeTermsList),
-    maybe_parse_types(TypeTermsList, Types),
+    maybe_parse_types(no_allow_ho_inst_info, TypeTermsList, Types),
     list.map(mer_type_to_typesel, Types, Selector),
     Datastruct = selected_cel(ProgVar, Selector).
 
diff --git a/compiler/prog_data.m b/compiler/prog_data.m
index 8118355..666fb0d 100644
--- a/compiler/prog_data.m
+++ b/compiler/prog_data.m
@@ -1849,12 +1849,12 @@ cons_id_is_const_struct(ConsId, ConstNum) :-
             % Tuple types.
 
     ;       higher_order_type(
-                % A type for higher-order values. If the second argument
-                % is yes(T) then the values are functions returning T,
-                % otherwise they are predicates. The kind is always `star'.
-
+                % A type for higher-order values. The kind is always `star'.
+                % For functions the return type is at the end of the list
+                % of argument types.
+                pred_or_func,
                 list(mer_type),
-                maybe(mer_type),
+                ho_inst_info,
                 purity,
                 lambda_eval_method
             )
@@ -1978,7 +1978,7 @@ get_tvar_kind(Map, TVar, Kind) :-
 get_type_kind(type_variable(_, Kind)) = Kind.
 get_type_kind(defined_type(_, _, Kind)) = Kind.
 get_type_kind(builtin_type(_)) = kind_star.
-get_type_kind(higher_order_type(_, _, _, _)) = kind_star.
+get_type_kind(higher_order_type(_, _, _, _, _)) = kind_star.
 get_type_kind(tuple_type(_, Kind)) = Kind.
 get_type_kind(apply_n_type(_, _, Kind)) = Kind.
 get_type_kind(kinded_type(_, Kind)) = Kind.
diff --git a/compiler/prog_event.m b/compiler/prog_event.m
index 6d6e8c1..ef066c8 100644
--- a/compiler/prog_event.m
+++ b/compiler/prog_event.m
@@ -59,10 +59,12 @@
 
 :- implementation.
 
+:- import_module mdbcomp.prim_data.
 :- import_module mdbcomp.sym_name.
 :- import_module parse_tree.builtin_lib_types.
 :- import_module parse_tree.prog_mode.
 :- import_module parse_tree.prog_out.
+:- import_module parse_tree.prog_type.
 
 :- import_module assoc_list.
 :- import_module bimap.
@@ -541,8 +543,8 @@ build_dep_map(EventName, FileName, AttrNameMap, KeyMap, [AttrTerm | AttrTerms],
                         FuncAttrPurity = event_attr_impure_function,
                         FuncPurity = purity_impure
                     ),
-                    FuncAttrType = higher_order_type(ArgTypes, yes(AttrType),
-                        FuncPurity, lambda_normal),
+                    construct_higher_order_func_type(FuncPurity, lambda_normal,
+                        ArgTypes, AttrType, FuncAttrType),
                     ( if
                         map.search(!.AttrTypeMap, FuncAttrName,
                             OldFuncAttrType)
@@ -817,7 +819,7 @@ describe_attr_type(Type) = Desc :-
         Type = builtin_type(BuiltinType),
         builtin_type_to_string(BuiltinType, Desc)
     ;
-        Type = higher_order_type(_, _, _, _),
+        Type = higher_order_type(_, _, _, _, _),
         Desc = "function"
     ;
         ( Type = type_variable(_, _)
diff --git a/compiler/prog_io_item.m b/compiler/prog_io_item.m
index af39f78..cb2d612 100644
--- a/compiler/prog_io_item.m
+++ b/compiler/prog_io_item.m
@@ -1224,12 +1224,12 @@ parse_type_and_mode(InstConstraints, Term, MaybeTypeAndMode) :-
     ( if
         Term = term.functor(term.atom("::"), [TypeTerm, ModeTerm], _Context)
     then
-        maybe_parse_type(TypeTerm, Type),
+        maybe_parse_type(no_allow_ho_inst_info, TypeTerm, Type),
         convert_mode(allow_constrained_inst_var, ModeTerm, Mode0),
         constrain_inst_vars_in_mode_sub(InstConstraints, Mode0, Mode),
         MaybeTypeAndMode = type_and_mode(Type, Mode)
     else
-        maybe_parse_type(Term, Type),
+        maybe_parse_type(no_allow_ho_inst_info, Term, Type),
         MaybeTypeAndMode = type_only(Type)
     ).
 
@@ -1846,7 +1846,8 @@ parse_with_type_suffix(VarSet, Term, BeforeWithTypeTerm, MaybeWithType) :-
         BeforeWithTypeTerm = BeforeWithTypeTermPrime,
         ContextPieces = cord.from_list([words("In"), quote("with_type"),
             words("annotation:")]),
-        parse_type(TypeTerm, VarSet, ContextPieces, MaybeType),
+        parse_type(no_allow_ho_inst_info, TypeTerm, VarSet, ContextPieces,
+            MaybeType),
         (
             MaybeType = ok1(Type),
             MaybeWithType = ok1(yes(Type))
diff --git a/compiler/prog_io_mutable.m b/compiler/prog_io_mutable.m
index 4586bdd..a7925d8 100644
--- a/compiler/prog_io_mutable.m
+++ b/compiler/prog_io_mutable.m
@@ -267,7 +267,8 @@ parse_mutable_type(VarSet, TypeTerm, MaybeType) :-
         MaybeType = error1([Spec])
     else
         ContextPieces = cord.init,
-        parse_type(TypeTerm, VarSet, ContextPieces, MaybeType)
+        parse_type(no_allow_ho_inst_info, TypeTerm, VarSet, ContextPieces,
+            MaybeType)
     ).
 
 :- pred parse_mutable_inst(varset::in, term::in, maybe1(mer_inst)::out) is det.
diff --git a/compiler/prog_io_pragma.m b/compiler/prog_io_pragma.m
index b16b403..48a4d33 100644
--- a/compiler/prog_io_pragma.m
+++ b/compiler/prog_io_pragma.m
@@ -1509,7 +1509,7 @@ parse_pragma_structure_sharing(ModuleName, VarSet, ErrorTerm, PragmaTerms,
 
         % Parse the types:
         HeadVarTypesTerm = term.functor(term.atom("types"), ListTypeTerms, _),
-        maybe_parse_types(ListTypeTerms, Types),
+        maybe_parse_types(no_allow_ho_inst_info, ListTypeTerms, Types),
 
         % Parse the actual structure sharing information.
 
@@ -1565,7 +1565,7 @@ parse_pragma_structure_reuse(ModuleName, VarSet, ErrorTerm, PragmaTerms,
 
         % Parse the types:
         HeadVarTypesTerm = term.functor(term.atom("types"), ListTypeTerms, _),
-        maybe_parse_types(ListTypeTerms, Types),
+        maybe_parse_types(no_allow_ho_inst_info, ListTypeTerms, Types),
 
         % Parse the actual structure reuse information.
         MaybeStructureReuseTerm = term.functor(term.atom(ReuseFunctor),
@@ -3416,7 +3416,7 @@ convert_type_spec_pair(Term, TypeSpec) :-
     Term = term.functor(term.atom("="), [TypeVarTerm, SpecTypeTerm0], _),
     TypeVarTerm = term.variable(TypeVar0, _),
     term.coerce_var(TypeVar0, TypeVar),
-    maybe_parse_type(SpecTypeTerm0, SpecType),
+    maybe_parse_type(no_allow_ho_inst_info, SpecTypeTerm0, SpecType),
     TypeSpec = TypeVar - SpecType.
 
 %---------------------------------------------------------------------------%
diff --git a/compiler/prog_io_type_defn.m b/compiler/prog_io_type_defn.m
index a8939a5..83a5dce 100644
--- a/compiler/prog_io_type_defn.m
+++ b/compiler/prog_io_type_defn.m
@@ -418,7 +418,7 @@ convert_constructor_arg_list(ModuleName, VarSet, [Term | Terms])
 convert_constructor_arg_list_2(ModuleName, VarSet, MaybeCtorFieldName,
         TypeTerm, Terms) = MaybeArgs :-
     ContextPieces = cord.singleton(words("In type definition:")),
-    parse_type(TypeTerm, VarSet, ContextPieces, MaybeType),
+    parse_type(allow_ho_inst_info, TypeTerm, VarSet, ContextPieces, MaybeType),
     (
         MaybeType = ok1(Type),
         Context = get_term_context(TypeTerm),
@@ -634,7 +634,8 @@ parse_eqv_type_defn(ModuleName, VarSet, HeadTerm, BodyTerm, Context, SeqNum,
     parse_type_defn_head(ModuleName, VarSet, HeadTerm, MaybeNameAndParams),
     % XXX Should pass more correct ContextPieces.
     ContextPieces = cord.init,
-    parse_type(BodyTerm, VarSet, ContextPieces, MaybeType),
+    parse_type(no_allow_ho_inst_info, BodyTerm, VarSet, ContextPieces,
+        MaybeType),
     ( if
         SolverSpecs = [],
         MaybeNameAndParams = ok2(Name, ParamTVars),
@@ -1076,7 +1077,7 @@ parse_where_inst_is(_ModuleName, Term) = MaybeInst :-
 parse_where_type_is(_ModuleName, VarSet, Term) = MaybeType :-
     % XXX We should pass meaningful ContextPieces.
     ContextPieces = cord.init,
-    parse_type(Term, VarSet, ContextPieces, MaybeType).
+    parse_type(no_allow_ho_inst_info, Term, VarSet, ContextPieces, MaybeType).
 
 :- func parse_where_mutable_is(module_name, term) =
     maybe1(list(item_mutable_info)).
diff --git a/compiler/prog_io_type_name.m b/compiler/prog_io_type_name.m
index 1df24cc..fdd5388 100644
--- a/compiler/prog_io_type_name.m
+++ b/compiler/prog_io_type_name.m
@@ -25,29 +25,36 @@
 
 %---------------------------------------------------------------------------%
 
-:- pred maybe_parse_type(term::in, mer_type::out) is semidet.
+:- type allow_ho_inst_info
+    --->    allow_ho_inst_info
+    ;       no_allow_ho_inst_info.
 
-:- pred parse_type(term::in, varset::in, cord(format_component)::in,
-    maybe1(mer_type)::out) is det.
+:- pred maybe_parse_type(allow_ho_inst_info::in, term::in, mer_type::out)
+    is semidet.
 
-:- pred maybe_parse_types(list(term)::in, list(mer_type)::out) is semidet.
+:- pred parse_type(allow_ho_inst_info::in, term::in, varset::in,
+    cord(format_component)::in, maybe1(mer_type)::out) is det.
 
-:- pred parse_types(list(term)::in, varset::in, cord(format_component)::in,
-    maybe1(list(mer_type))::out) is det.
+:- pred maybe_parse_types(allow_ho_inst_info::in, list(term)::in,
+    list(mer_type)::out) is semidet.
 
-:- pred is_known_type_name(string::in) is semidet.
+:- pred parse_types(allow_ho_inst_info::in, list(term)::in, varset::in,
+    cord(format_component)::in, maybe1(list(mer_type))::out) is det.
 
-:- pred unparse_type(mer_type::in, term::out) is det.
+:- pred is_known_type_name(string::in) is semidet.
 
 %---------------------------------------------------------------------------%
 %---------------------------------------------------------------------------%
 
 :- implementation.
 
+:- import_module mdbcomp.prim_data.
 :- import_module mdbcomp.sym_name.
 :- import_module parse_tree.parse_tree_out_term.
+:- import_module parse_tree.prog_io_inst_mode_name.
 :- import_module parse_tree.prog_io_sym_name.
 :- import_module parse_tree.prog_out.
+:- import_module parse_tree.prog_type.
 
 :- import_module bool.
 :- import_module maybe.
@@ -55,14 +62,14 @@
 
 %---------------------------------------------------------------------------%
 
-maybe_parse_type(Term, Type) :-
+maybe_parse_type(AllowHOInstInfo, Term, Type) :-
     % The values of VarSet and ContextPieces do not matter since we succeed
     % only if they aren't used.
     VarSet = varset.init,
     ContextPieces = cord.init,
-    parse_type(Term, VarSet, ContextPieces, ok1(Type)).
+    parse_type(AllowHOInstInfo, Term, VarSet, ContextPieces, ok1(Type)).
 
-parse_type(Term, VarSet, ContextPieces, Result) :-
+parse_type(AllowHOInstInfo, Term, VarSet, ContextPieces, Result) :-
     % XXX kind inference: We currently give all types kind `star'.
     % This will be different when we have a kind system.
     (
@@ -89,8 +96,8 @@ parse_type(Term, VarSet, ContextPieces, Result) :-
                     Result = ok1(Type)
                 ;
                     KnownTypeKind = known_type_compound(CompoundTypeKind),
-                    parse_compound_type(Term, VarSet, ContextPieces,
-                        CompoundTypeKind, Result)
+                    parse_compound_type(AllowHOInstInfo, Term, VarSet,
+                        ContextPieces, CompoundTypeKind, Result)
                 ;
                     KnownTypeKind = known_type_bad_arity,
                     Result = ill_formed_type_result(ContextPieces, VarSet,
@@ -103,8 +110,8 @@ parse_type(Term, VarSet, ContextPieces, Result) :-
                     NameResult),
                 (
                     NameResult = ok2(SymName, SymNameArgTerms),
-                    parse_types(SymNameArgTerms, VarSet, ContextPieces,
-                        SymNameArgsResult),
+                    parse_types(no_allow_ho_inst_info, SymNameArgTerms, VarSet,
+                        ContextPieces, SymNameArgsResult),
                     (
                         SymNameArgsResult = ok1(ArgTypes),
                         Result = ok1(defined_type(SymName, ArgTypes,
@@ -121,13 +128,16 @@ parse_type(Term, VarSet, ContextPieces, Result) :-
         )
     ).
 
-:- pred parse_compound_type(term::in, varset::in, cord(format_component)::in,
-    known_compound_type_kind(term)::in, maybe1(mer_type)::out) is det.
+:- pred parse_compound_type(allow_ho_inst_info::in, term::in, varset::in,
+    cord(format_component)::in, known_compound_type_kind(term)::in,
+    maybe1(mer_type)::out) is det.
 
-parse_compound_type(Term, VarSet, ContextPieces, CompoundTypeKind, Result) :-
+parse_compound_type(AllowHOInstInfo, Term, VarSet, ContextPieces,
+        CompoundTypeKind, Result) :-
     (
         CompoundTypeKind = kctk_tuple(Args),
-        parse_types(Args, VarSet, ContextPieces, ArgsResult),
+        parse_types(no_allow_ho_inst_info, Args, VarSet, ContextPieces,
+            ArgsResult),
         (
             ArgsResult = ok1(ArgTypes),
             Result = ok1(tuple_type(ArgTypes, kind_star))
@@ -148,10 +158,11 @@ parse_compound_type(Term, VarSet, ContextPieces, CompoundTypeKind, Result) :-
     ;
         CompoundTypeKind = kctk_pure_pred(Args),
         ( if
-            maybe_parse_types(Args, ArgTypes)
+            maybe_parse_types(no_allow_ho_inst_info, Args, ArgTypes)
         then
-            Result = ok1(higher_order_type(ArgTypes, no, purity_pure,
-                lambda_normal))
+            construct_higher_order_pred_type(purity_pure, lambda_normal,
+                ArgTypes, PredType),
+            Result = ok1(PredType)
         else
             Result = ill_formed_type_result(ContextPieces, VarSet, Term)
         )
@@ -159,11 +170,22 @@ parse_compound_type(Term, VarSet, ContextPieces, CompoundTypeKind, Result) :-
         CompoundTypeKind = kctk_pure_func(Arg1, Arg2),
         ( if
             Arg1 = term.functor(term.atom("func"), FuncArgs, _),
-            maybe_parse_types(FuncArgs, ArgTypes),
-            maybe_parse_type(Arg2, RetType)
+            maybe_parse_types(no_allow_ho_inst_info, FuncArgs, ArgTypes),
+            maybe_parse_type(no_allow_ho_inst_info, Arg2, RetType)
         then
-            Result = ok1(higher_order_type(ArgTypes,
-                yes(RetType), purity_pure, lambda_normal))
+            construct_higher_order_func_type(purity_pure, lambda_normal,
+                ArgTypes, RetType, FuncType),
+            Result = ok1(FuncType)
+        else
+            Result = ill_formed_type_result(ContextPieces, VarSet, Term)
+        )
+    ;
+        CompoundTypeKind = kctk_is(Arg1, Arg2),
+        ( if
+            AllowHOInstInfo = allow_ho_inst_info,
+            maybe_parse_ho_type_and_inst(Arg1, Arg2, purity_pure, Type)
+        then
+            Result = ok1(Type)
         else
             Result = ill_formed_type_result(ContextPieces, VarSet, Term)
         )
@@ -175,23 +197,74 @@ parse_compound_type(Term, VarSet, ContextPieces, CompoundTypeKind, Result) :-
                 Name = "=",
                 Args = [Arg1, Arg2],
                 Arg1 = term.functor(term.atom("func"), FuncArgs, _),
-                maybe_parse_types(FuncArgs, ArgTypes),
-                maybe_parse_type(Arg2, RetType),
-                ResultPrime = ok1(higher_order_type(ArgTypes,
-                    yes(RetType), Purity, lambda_normal))
+                maybe_parse_types(no_allow_ho_inst_info, FuncArgs, ArgTypes),
+                maybe_parse_type(no_allow_ho_inst_info, Arg2, RetType),
+                construct_higher_order_func_type(Purity, lambda_normal,
+                    ArgTypes, RetType, Type)
             ;
                 Name = "pred",
-                maybe_parse_types(Args, ArgTypes),
-                ResultPrime = ok1(higher_order_type(ArgTypes, no, Purity,
-                    lambda_normal))
+                maybe_parse_types(no_allow_ho_inst_info, Args, ArgTypes),
+                construct_higher_order_pred_type(Purity, lambda_normal,
+                    ArgTypes, Type)
+            ;
+                Name = "is",
+                AllowHOInstInfo = allow_ho_inst_info,
+                Args = [Arg1, Arg2],
+                maybe_parse_ho_type_and_inst(Arg1, Arg2, Purity, Type)
             )
         then
-            Result = ResultPrime
+            Result = ok1(Type)
         else
             Result = ill_formed_type_result(ContextPieces, VarSet, Term)
         )
     ).
 
+:- pred maybe_parse_ho_type_and_inst(term::in, term::in, purity::in,
+    mer_type::out) is semidet.
+
+maybe_parse_ho_type_and_inst(Arg1, Arg2, Purity, Type) :-
+    Arg2 = term.functor(term.atom(DetString), [], _),
+    standard_det(DetString, Detism),
+    (
+        Arg1 = term.functor(term.atom("="), [FuncTerm, RetTerm], _),
+        FuncTerm = term.functor(term.atom("func"), ArgTerms, _),
+        maybe_parse_types_and_modes(ArgTerms, ArgTypes, ArgModes),
+        maybe_parse_type_and_mode(RetTerm, RetType, RetMode),
+        construct_higher_order_func_type(Purity, lambda_normal, ArgTypes,
+            RetType, ArgModes, RetMode, Detism, Type)
+    ;
+        Arg1 = term.functor(term.atom("pred"), ArgTerms, _),
+        maybe_parse_types_and_modes(ArgTerms, ArgTypes, ArgModes),
+        construct_higher_order_pred_type(Purity, lambda_normal, ArgTypes,
+            ArgModes, Detism, Type)
+    ).
+
+:- pred maybe_parse_types_and_modes(list(term)::in, list(mer_type)::out,
+    list(mer_mode)::out) is semidet.
+
+maybe_parse_types_and_modes(ArgTerms, ArgTypes, ArgModes) :-
+    list.reverse(ArgTerms, RevArgTerms),
+    maybe_parse_types_and_modes_acc(RevArgTerms, [], ArgTypes, [], ArgModes).
+
+:- pred maybe_parse_types_and_modes_acc(list(term)::in,
+    list(mer_type)::in, list(mer_type)::out,
+    list(mer_mode)::in, list(mer_mode)::out) is semidet.
+
+maybe_parse_types_and_modes_acc([], !ArgTypes, !ArgModes).
+maybe_parse_types_and_modes_acc([ArgTerm | ArgTerms], ArgTypes0, ArgTypes,
+        ArgModes0, ArgModes) :-
+    maybe_parse_type_and_mode(ArgTerm, ArgType, ArgMode),
+    maybe_parse_types_and_modes_acc(ArgTerms, [ArgType | ArgTypes0], ArgTypes,
+        [ArgMode | ArgModes0], ArgModes).
+
+:- pred maybe_parse_type_and_mode(term::in, mer_type::out, mer_mode::out)
+    is semidet.
+
+maybe_parse_type_and_mode(Term, Type, Mode) :-
+    Term = term.functor(term.atom("::"), [TypeTerm, ModeTerm], _),
+    maybe_parse_type(no_allow_ho_inst_info, TypeTerm, Type),
+    convert_mode(no_allow_constrained_inst_var, ModeTerm, Mode).
+
 is_known_type_name(Name) :-
     (
         is_known_type_name_args(Name, [] : list(mer_type), _)
@@ -208,6 +281,7 @@ is_known_type_name(Name) :-
     --->    kctk_tuple(list(T))
     ;       kctk_pure_func(T, T)
     ;       kctk_pure_pred(list(T))
+    ;       kctk_is(T, T)
     ;       kctk_purity(purity, T)
     ;       kctk_apply(list(T)).
 
@@ -277,6 +351,18 @@ is_known_type_name_args(Name, Args, KnownType) :-
         Name = "pred",
         KnownType = known_type_compound(kctk_pure_pred(Args))
     ;
+        Name = "is",
+        (
+            ( Args = []
+            ; Args = [_]
+            ; Args = [_, _, _ | _]
+            ),
+            KnownType = known_type_bad_arity
+        ;
+            Args = [Arg1, Arg2],
+            KnownType = known_type_compound(kctk_is(Arg1, Arg2))
+        )
+    ;
         (
             Name = "pure",
             Purity = purity_pure
@@ -314,15 +400,16 @@ ill_formed_type_result(ContextPieces, VarSet, Term) = Result :-
 
 %---------------------------------------------------------------------------%
 
-maybe_parse_types(Term, Types) :-
+maybe_parse_types(AllowHOInstInfo, Term, Types) :-
     % The values of VarSet and ContextPieces do not matter since we succeed
     % only if they aren't used.
     VarSet = varset.init,
     ContextPieces = cord.init,
-    parse_types(Term, VarSet, ContextPieces, ok1(Types)).
+    parse_types(AllowHOInstInfo, Term, VarSet, ContextPieces, ok1(Types)).
 
-parse_types(Terms, VarSet, ContextPieces, Result) :-
-    parse_types_acc(Terms, VarSet, ContextPieces, [], RevTypes, [], Specs),
+parse_types(AllowHOInstInfo, Terms, VarSet, ContextPieces, Result) :-
+    parse_types_acc(AllowHOInstInfo, Terms, VarSet, ContextPieces,
+        [], RevTypes, [], Specs),
     (
         Specs = [],
         Result = ok1(list.reverse(RevTypes))
@@ -331,14 +418,15 @@ parse_types(Terms, VarSet, ContextPieces, Result) :-
         Result = error1(Specs)
     ).
 
-:- pred parse_types_acc(list(term)::in, varset::in, cord(format_component)::in,
-    list(mer_type)::in, list(mer_type)::out,
+:- pred parse_types_acc(allow_ho_inst_info::in, list(term)::in, varset::in,
+    cord(format_component)::in, list(mer_type)::in, list(mer_type)::out,
     list(error_spec)::in, list(error_spec)::out) is det.
 
-parse_types_acc([], _, _, !RevTypes, !Specs).
-parse_types_acc([Term | Terms], VarSet, ContextPieces, !RevTypes, !Specs) :-
+parse_types_acc(_, [], _, _, !RevTypes, !Specs).
+parse_types_acc(AllowHOInstInfo, [Term | Terms], VarSet, ContextPieces,
+        !RevTypes, !Specs) :-
     % XXX We should pass a ContextPieces updated as the "nth type in ...".
-    parse_type(Term, VarSet, ContextPieces, TermResult),
+    parse_type(AllowHOInstInfo, Term, VarSet, ContextPieces, TermResult),
     (
         TermResult = ok1(Type),
         !:RevTypes = [Type | !.RevTypes]
@@ -346,84 +434,8 @@ parse_types_acc([Term | Terms], VarSet, ContextPieces, !RevTypes, !Specs) :-
         TermResult = error1(TermSpecs),
         !:Specs = TermSpecs ++ !.Specs
     ),
-    parse_types_acc(Terms, VarSet, ContextPieces, !RevTypes, !Specs).
-
-%---------------------------------------------------------------------------%
-
-unparse_type(Type, Term) :-
-    Context = term.context_init,
-    (
-        Type = type_variable(TVar, _),
-        Var = term.coerce_var(TVar),
-        Term = term.variable(Var, Context)
-    ;
-        Type = defined_type(SymName, Args, _),
-        unparse_type_list(Args, ArgTerms),
-        unparse_qualified_term(SymName, ArgTerms, Term)
-    ;
-        Type = builtin_type(BuiltinType),
-        builtin_type_to_string(BuiltinType, Name),
-        Term = term.functor(term.atom(Name), [], Context)
-    ;
-        Type = higher_order_type(Args, MaybeRet, Purity, EvalMethod),
-        unparse_type_list(Args, ArgTerms),
-        (
-            MaybeRet = yes(Ret),
-            Term0 = term.functor(term.atom("func"), ArgTerms, Context),
-            maybe_add_lambda_eval_method(EvalMethod, Term0, Term1),
-            unparse_type(Ret, RetTerm),
-            Term2 = term.functor(term.atom("="), [Term1, RetTerm], Context)
-        ;
-            MaybeRet = no,
-            Term0 = term.functor(term.atom("pred"), ArgTerms, Context),
-            maybe_add_lambda_eval_method(EvalMethod, Term0, Term2)
-        ),
-        maybe_add_purity_annotation(Purity, Term2, Term)
-    ;
-        Type = tuple_type(Args, _),
-        unparse_type_list(Args, ArgTerms),
-        Term = term.functor(term.atom("{}"), ArgTerms, Context)
-    ;
-        Type = apply_n_type(TVar, Args, _),
-        Var = term.coerce_var(TVar),
-        unparse_type_list(Args, ArgTerms),
-        Term = term.functor(term.atom(""),
-            [term.variable(Var, Context) | ArgTerms], Context)
-    ;
-        Type = kinded_type(_, _),
-        unexpected($module, $pred, "kind annotation")
-    ).
-
-:- pred unparse_type_list(list(mer_type)::in, list(term)::out) is det.
-
-unparse_type_list(Types, Terms) :-
-    list.map(unparse_type, Types, Terms).
-
-:- pred unparse_qualified_term(sym_name::in, list(term)::in, term::out) is det.
-
-unparse_qualified_term(unqualified(Name), Args, Term) :-
-    Context = term.context_init,
-    Term = term.functor(term.atom(Name), Args, Context).
-unparse_qualified_term(qualified(Qualifier, Name), Args, Term) :-
-    Context = term.context_init,
-    unparse_qualified_term(Qualifier, [], QualTerm),
-    Term0 = term.functor(term.atom(Name), Args, Context),
-    Term = term.functor(term.atom("."), [QualTerm, Term0], Context).
-
-:- pred maybe_add_lambda_eval_method(lambda_eval_method::in, term::in,
-    term::out) is det.
-
-maybe_add_lambda_eval_method(lambda_normal, Term, Term).
-
-:- pred maybe_add_purity_annotation(purity::in, term::in, term::out) is det.
-
-maybe_add_purity_annotation(purity_pure, Term, Term).
-maybe_add_purity_annotation(purity_semipure, Term0, Term) :-
-    Context = term.context_init,
-    Term = term.functor(term.atom("semipure"), [Term0], Context).
-maybe_add_purity_annotation(purity_impure, Term0, Term) :-
-    Context = term.context_init,
-    Term = term.functor(term.atom("impure"), [Term0], Context).
+    parse_types_acc(AllowHOInstInfo, Terms, VarSet, ContextPieces,
+        !RevTypes, !Specs).
 
 %---------------------------------------------------------------------------%
 :- end_module parse_tree.prog_io_type_name.
diff --git a/compiler/prog_io_typeclass.m b/compiler/prog_io_typeclass.m
index 570a8f6..6fe65d3 100644
--- a/compiler/prog_io_typeclass.m
+++ b/compiler/prog_io_typeclass.m
@@ -579,7 +579,8 @@ parse_arbitrary_constraint(VarSet, ConstraintTerm, Result) :-
     then
         ArgsResultContextPieces =
             cord.singleton(words("In class or inst constraint:")),
-        parse_types(Args0, VarSet, ArgsResultContextPieces, ArgsResult),
+        parse_types(no_allow_ho_inst_info, Args0, VarSet,
+            ArgsResultContextPieces, ArgsResult),
         (
             ArgsResult = ok1(Args),
             Constraint = constraint(ClassName, Args),
@@ -742,7 +743,8 @@ parse_underived_instance(ModuleName, TVarSet, NameTerm, Context, SeqNum,
     (
         MaybeClassName = ok2(ClassName, TypeTerms),
         TypesContextPieces = NameContextPieces,
-        parse_types(TypeTerms, VarSet, TypesContextPieces, MaybeTypes),
+        parse_types(no_allow_ho_inst_info, TypeTerms, VarSet,
+            TypesContextPieces, MaybeTypes),
         (
             MaybeTypes = ok1(Types),
             ItemInstanceInfo = item_instance_info(ClassName, Types, Types, [],
diff --git a/compiler/prog_rep_tables.m b/compiler/prog_rep_tables.m
index e82a97f..36e6d72 100644
--- a/compiler/prog_rep_tables.m
+++ b/compiler/prog_rep_tables.m
@@ -53,6 +53,7 @@
 :- implementation.
 
 :- import_module mdbcomp.
+:- import_module mdbcomp.prim_data.
 :- import_module mdbcomp.rtti_access.
 :- import_module mdbcomp.sym_name.
 
@@ -347,26 +348,19 @@ add_type_to_table(Type, TypeCode, !StringTable, !TypeTable) :-
         encode_arg_type_codes(ArgTypeCodes, ArgTypeBytesCord),
         TypeBytesCord = cord.singleton(Selector) ++ ArgTypeBytesCord
     ;
-        Type = higher_order_type(ArgTypes, MaybeReturnType,
-            _Purity, _EvalMethod),
+        Type = higher_order_type(PorF, ArgTypes, _HOInstInfo, _Purity,
+            _EvalMethod),
         list.map_foldl2(lookup_type_in_table, ArgTypes, ArgTypeCodes,
             !StringTable, !TypeTable),
         encode_arg_type_codes(ArgTypeCodes, ArgTypeBytesCord),
         (
-            MaybeReturnType = no,
-            Selector = 10,
-            TypeBytesCord = cord.singleton(Selector)
-                ++ ArgTypeBytesCord
+            PorF = pf_predicate,
+            Selector = 10
         ;
-            MaybeReturnType = yes(ReturnType),
-            Selector = 11,
-            lookup_type_in_table(ReturnType, ReturnTypeCode,
-                !StringTable, !TypeTable),
-            encode_num_det(ReturnTypeCode, ReturnTypeBytes),
-            TypeBytesCord = cord.singleton(Selector)
-                ++ ArgTypeBytesCord
-                ++ cord.from_list(ReturnTypeBytes)
-        )
+            PorF = pf_function,
+            Selector = 11
+        ),
+        TypeBytesCord = cord.singleton(Selector) ++ ArgTypeBytesCord
     ;
         Type = apply_n_type(_TVar, _ArgTypes, _Kind),
         unexpected($module, $pred, "apply_n_type")
diff --git a/compiler/prog_type.m b/compiler/prog_type.m
index 2d8f81d..8cf7bfe 100644
--- a/compiler/prog_type.m
+++ b/compiler/prog_type.m
@@ -181,9 +181,17 @@
 :- pred construct_higher_order_pred_type(purity::in, lambda_eval_method::in,
     list(mer_type)::in, mer_type::out) is det.
 
+:- pred construct_higher_order_pred_type(purity::in, lambda_eval_method::in,
+    list(mer_type)::in, list(mer_mode)::in, determinism::in, mer_type::out)
+    is det.
+
 :- pred construct_higher_order_func_type(purity::in, lambda_eval_method::in,
     list(mer_type)::in, mer_type::in, mer_type::out) is det.
 
+:- pred construct_higher_order_func_type(purity::in, lambda_eval_method::in,
+    list(mer_type)::in, mer_type::in, list(mer_mode)::in, mer_mode::in,
+    determinism::in, mer_type::out) is det.
+
     % Make error messages more readable by removing "builtin."
     % qualifiers.
     %
@@ -434,21 +442,12 @@ type_is_nonvar(Type) :-
     not type_is_var(Type).
 
 type_is_higher_order(Type) :-
-    strip_kind_annotation(Type) = higher_order_type(_, _, _, _).
+    strip_kind_annotation(Type) = higher_order_type(_, _, _, _, _).
 
-type_is_higher_order_details(Type, Purity, PredOrFunc, EvalMethod,
-        PredArgTypes) :-
+type_is_higher_order_details(Type, Purity, PredOrFunc, EvalMethod, ArgTypes) :-
     strip_kind_annotation(Type) =
-        higher_order_type(ArgTypes, MaybeRetType, Purity, EvalMethod),
-    (
-        MaybeRetType = yes(RetType),
-        PredOrFunc = pf_function,
-        PredArgTypes = list.append(ArgTypes, [RetType])
-    ;
-        MaybeRetType = no,
-        PredOrFunc = pf_predicate,
-        PredArgTypes = ArgTypes
-    ).
+        higher_order_type(PredOrFunc, ArgTypes, _HOInstInfo, Purity,
+            EvalMethod).
 
 type_is_higher_order_details_det(Type, !:Purity, !:PredOrFunc, !:EvalMethod,
         !:PredArgTypes) :-
@@ -520,16 +519,15 @@ type_to_ctor_and_args(Type, TypeCtor, Args) :-
         Args = [],
         TypeCtor = type_ctor(SymName, Arity)
     ;
-        Type = higher_order_type(Args0, MaybeRet, Purity, _EvalMethod),
-        Arity = list.length(Args0),
+        Type = higher_order_type(PorF, Args, _HOInstInfo, Purity, _EvalMethod),
         (
-            MaybeRet = yes(Ret),
+            PorF = pf_predicate,
             PorFStr = "func",
-            Args = list.append(Args0, [Ret])
+            Arity = list.length(Args)
         ;
-            MaybeRet = no,
+            PorF = pf_function,
             PorFStr = "pred",
-            Args = Args0
+            Arity = list.length(Args) - 1
         ),
         SymName0 = unqualified(PorFStr),
         (
@@ -629,14 +627,8 @@ type_vars_2(type_variable(Var, _), Vs, [Var | Vs]).
 type_vars_2(defined_type(_, Args, _), !V) :-
     type_vars_list_2(Args, !V).
 type_vars_2(builtin_type(_), !V).
-type_vars_2(higher_order_type(Args, MaybeRet, _, _), !V) :-
-    type_vars_list_2(Args, !V),
-    (
-        MaybeRet = yes(Ret),
-        type_vars_2(Ret, !V)
-    ;
-        MaybeRet = no
-    ).
+type_vars_2(higher_order_type(_, Args, _, _, _), !V) :-
+    type_vars_list_2(Args, !V).
 type_vars_2(tuple_type(Args, _), !V) :-
     type_vars_list_2(Args, !V).
 type_vars_2(apply_n_type(Var, Args, _), !V) :-
@@ -661,10 +653,8 @@ type_vars_list_2([Type | Types], !V) :-
 type_contains_var(type_variable(Var, _), Var).
 type_contains_var(defined_type(_, Args, _), Var) :-
     type_list_contains_var(Args, Var).
-type_contains_var(higher_order_type(Args, _, _, _), Var) :-
+type_contains_var(higher_order_type(_, Args, _, _, _), Var) :-
     type_list_contains_var(Args, Var).
-type_contains_var(higher_order_type(_, yes(Ret), _, _), Var) :-
-    type_contains_var(Ret, Var).
 type_contains_var(tuple_type(Args, _), Var) :-
     type_list_contains_var(Args, Var).
 type_contains_var(apply_n_type(Var, _, _), Var).
@@ -711,11 +701,27 @@ construct_higher_order_type(Purity, PredOrFunc, EvalMethod, ArgTypes, Type) :-
     ).
 
 construct_higher_order_pred_type(Purity, EvalMethod, ArgTypes, Type) :-
-    Type = higher_order_type(ArgTypes, no, Purity, EvalMethod).
+    Type = higher_order_type(pf_predicate, ArgTypes, none_or_default_func,
+        Purity, EvalMethod).
+
+construct_higher_order_pred_type(Purity, EvalMethod, ArgTypes, ArgModes,
+        Detism, Type) :-
+    PredInstInfo = pred_inst_info(pf_predicate, ArgModes, arg_reg_types_unset,
+        Detism),
+    Type = higher_order_type(pf_predicate, ArgTypes, higher_order(PredInstInfo),
+        Purity, EvalMethod).
 
 construct_higher_order_func_type(Purity, EvalMethod, ArgTypes, RetType,
         Type) :-
-    Type = higher_order_type(ArgTypes, yes(RetType), Purity, EvalMethod).
+    Type = higher_order_type(pf_function, ArgTypes ++ [RetType],
+        none_or_default_func, Purity, EvalMethod).
+
+construct_higher_order_func_type(Purity, EvalMethod, ArgTypes, RetType,
+        ArgModes, RetMode, Detism, Type) :-
+    PredInstInfo = pred_inst_info(pf_function, ArgModes ++ [RetMode],
+        arg_reg_types_unset, Detism),
+    Type = higher_order_type(pf_function, ArgTypes ++ [RetType],
+        higher_order(PredInstInfo), Purity, EvalMethod).
 
 strip_builtin_qualifiers_from_type(type_variable(Var, Kind),
         type_variable(Var, Kind)).
@@ -733,17 +739,9 @@ strip_builtin_qualifiers_from_type(defined_type(Name0, Args0, Kind),
 strip_builtin_qualifiers_from_type(builtin_type(BuiltinType),
         builtin_type(BuiltinType)).
 strip_builtin_qualifiers_from_type(
-        higher_order_type(Args0, MaybeRet0, Purity, EvalMethod),
-        higher_order_type(Args, MaybeRet, Purity, EvalMethod)) :-
-    strip_builtin_qualifiers_from_type_list(Args0, Args),
-    (
-        MaybeRet0 = yes(Ret0),
-        strip_builtin_qualifiers_from_type(Ret0, Ret),
-        MaybeRet = yes(Ret)
-    ;
-        MaybeRet0 = no,
-        MaybeRet = no
-    ).
+        higher_order_type(PorF, Args0, HOInstInfo, Purity, EvalMethod),
+        higher_order_type(PorF, Args, HOInstInfo, Purity, EvalMethod)) :-
+    strip_builtin_qualifiers_from_type_list(Args0, Args).
 strip_builtin_qualifiers_from_type(tuple_type(Args0, Kind),
         tuple_type(Args, Kind)) :-
     strip_builtin_qualifiers_from_type_list(Args0, Args).
@@ -1127,15 +1125,10 @@ type_unify_nonvar(TypeX, TypeY, HeadTypeParams, !Bindings) :-
         TypeX = builtin_type(BuiltinType),
         TypeY = builtin_type(BuiltinType)
     ;
-        TypeX = higher_order_type(ArgsX, no, Purity, EvalMethod),
-        TypeY = higher_order_type(ArgsY, no, Purity, EvalMethod),
+        TypeX = higher_order_type(PorF, ArgsX, _, Purity, EvalMethod),
+        TypeY = higher_order_type(PorF, ArgsY, _, Purity, EvalMethod),
         type_unify_list(ArgsX, ArgsY, HeadTypeParams, !Bindings)
     ;
-        TypeX = higher_order_type(ArgsX, yes(RetX), Purity, EvalMethod),
-        TypeY = higher_order_type(ArgsY, yes(RetY), Purity, EvalMethod),
-        type_unify_list(ArgsX, ArgsY, HeadTypeParams, !Bindings),
-        type_unify(RetX, RetY, HeadTypeParams, !Bindings)
-    ;
         TypeX = tuple_type(ArgsX, _),
         TypeY = tuple_type(ArgsY, _),
         type_unify_list(ArgsX, ArgsY, HeadTypeParams, !Bindings)
@@ -1189,7 +1182,7 @@ type_unify_apply(TypeY, VarX, ArgsX0, HeadTypeParams, !Bindings) :-
         ArgsX0 = [],
         type_unify_var(VarX, TypeY, HeadTypeParams, !Bindings)
     ;
-        TypeY = higher_order_type(_, _, _, _),
+        TypeY = higher_order_type(_, _, _, _, _),
         ArgsX0 = [],
         type_unify_var(VarX, TypeY, HeadTypeParams, !Bindings)
     ;
@@ -1275,13 +1268,8 @@ type_occurs(TypeX, Y, Bindings) :-
         TypeX = defined_type(_, Args, _),
         type_occurs_list(Args, Y, Bindings)
     ;
-        TypeX = higher_order_type(Args, MaybeRet, _, _),
-        (
-            type_occurs_list(Args, Y, Bindings)
-        ;
-            MaybeRet = yes(Ret),
-            type_occurs(Ret, Y, Bindings)
-        )
+        TypeX = higher_order_type(_, Args, _, _, _),
+        type_occurs_list(Args, Y, Bindings)
     ;
         TypeX = tuple_type(Args, _),
         type_occurs_list(Args, Y, Bindings)
diff --git a/compiler/prog_type_subst.m b/compiler/prog_type_subst.m
index 1aaed2d..818ac97 100644
--- a/compiler/prog_type_subst.m
+++ b/compiler/prog_type_subst.m
@@ -178,17 +178,9 @@ apply_variable_renaming_to_type(Renaming, Type0, Type) :-
         Type0 = builtin_type(_),
         Type = Type0
     ;
-        Type0 = higher_order_type(Args0, MaybeReturn0, Purity, EvalMethod),
+        Type0 = higher_order_type(PorF, Args0, HOInstInfo, Purity, EvalMethod),
         apply_variable_renaming_to_type_list(Renaming, Args0, Args),
-        (
-            MaybeReturn0 = yes(Return0),
-            apply_variable_renaming_to_type(Renaming, Return0, Return),
-            MaybeReturn = yes(Return)
-        ;
-            MaybeReturn0 = no,
-            MaybeReturn = no
-        ),
-        Type = higher_order_type(Args, MaybeReturn, Purity, EvalMethod)
+        Type = higher_order_type(PorF, Args, HOInstInfo, Purity, EvalMethod)
     ;
         Type0 = tuple_type(Args0, Kind),
         apply_variable_renaming_to_type_list(Renaming, Args0, Args),
@@ -220,17 +212,9 @@ apply_subst_to_type(Subst, Type0, Type) :-
         Type0 = builtin_type(_),
         Type = Type0
     ;
-        Type0 = higher_order_type(Args0, MaybeReturn0, Purity, EvalMethod),
+        Type0 = higher_order_type(PorF, Args0, HOInstInfo, Purity, EvalMethod),
         apply_subst_to_type_list(Subst, Args0, Args),
-        (
-            MaybeReturn0 = yes(Return0),
-            apply_subst_to_type(Subst, Return0, Return),
-            MaybeReturn = yes(Return)
-        ;
-            MaybeReturn0 = no,
-            MaybeReturn = no
-        ),
-        Type = higher_order_type(Args, MaybeReturn, Purity, EvalMethod)
+        Type = higher_order_type(PorF, Args, HOInstInfo, Purity, EvalMethod)
     ;
         Type0 = tuple_type(Args0, Kind),
         apply_subst_to_type_list(Subst, Args0, Args),
@@ -266,17 +250,9 @@ apply_rec_subst_to_type(Subst, Type0, Type) :-
         Type0 = builtin_type(_),
         Type = Type0
     ;
-        Type0 = higher_order_type(Args0, MaybeReturn0, Purity, EvalMethod),
+        Type0 = higher_order_type(PorF, Args0, HOInstInfo, Purity, EvalMethod),
         apply_rec_subst_to_type_list(Subst, Args0, Args),
-        (
-            MaybeReturn0 = yes(Return0),
-            apply_rec_subst_to_type(Subst, Return0, Return),
-            MaybeReturn = yes(Return)
-        ;
-            MaybeReturn0 = no,
-            MaybeReturn = no
-        ),
-        Type = higher_order_type(Args, MaybeReturn, Purity, EvalMethod)
+        Type = higher_order_type(PorF, Args, HOInstInfo, Purity, EvalMethod)
     ;
         Type0 = tuple_type(Args0, Kind),
         apply_rec_subst_to_type_list(Subst, Args0, Args),
@@ -323,7 +299,7 @@ apply_type_args(Type0, Args, Type) :-
         Type = defined_type(Name, Args0 ++ Args, Kind)
     ;
         ( Type0 = builtin_type(_)
-        ; Type0 = higher_order_type(_, _, _, _)
+        ; Type0 = higher_order_type(_, _, _, _, _)
         ),
         (
             Args = []
diff --git a/compiler/pseudo_type_info.m b/compiler/pseudo_type_info.m
index ae642a0..a6b8950 100644
--- a/compiler/pseudo_type_info.m
+++ b/compiler/pseudo_type_info.m
@@ -91,7 +91,7 @@ construct_pseudo_type_info(Type, NumUnivQTvars, ExistQTvars, PseudoTypeInfo) :-
         ( Type = defined_type(_, _, _)
         ; Type = builtin_type(_)
         ; Type = tuple_type(_, _)
-        ; Type = higher_order_type(_, _, _, _)
+        ; Type = higher_order_type(_, _, _, _, _)
         ; Type = apply_n_type(_, _, _)
         ; Type = kinded_type(_, _)
         ),
diff --git a/compiler/recompilation.version.m b/compiler/recompilation.version.m
index dd4d420..44631a9 100644
--- a/compiler/recompilation.version.m
+++ b/compiler/recompilation.version.m
@@ -72,7 +72,6 @@
 :- implementation.
 
 :- import_module hlds.hlds_out.
-:- import_module hlds.hlds_out.hlds_out_mode.
 :- import_module parse_tree.error_util.
 :- import_module parse_tree.mercury_to_mercury.
 :- import_module parse_tree.parse_tree_out_info.
@@ -81,6 +80,7 @@
 :- import_module parse_tree.prog_io_util.
 :- import_module parse_tree.prog_type.
 :- import_module parse_tree.prog_type_subst.
+:- import_module parse_tree.unparse.
 
 :- import_module assoc_list.
 :- import_module bool.
diff --git a/compiler/rtti.m b/compiler/rtti.m
index c415af6..059a8f9 100644
--- a/compiler/rtti.m
+++ b/compiler/rtti.m
@@ -268,7 +268,8 @@
     --->    notag_functor(
                 nt_name             :: string,
                 nt_arg_type         :: rtti_maybe_pseudo_type_info,
-                nt_arg_name         :: maybe(string)
+                nt_arg_name         :: maybe(string),
+                nt_subtype_info     :: functor_subtype_info
             ).
 
     % Descriptor for a functor in a du type. Also used for functors in
@@ -284,7 +285,8 @@
                 du_ordinal          :: int,
                 du_rep              :: du_rep,
                 du_arg_infos        :: list(du_arg_info),
-                du_exist_info       :: maybe(exist_info)
+                du_exist_info       :: maybe(exist_info),
+                du_subtype_info     :: functor_subtype_info
             ).
 
     % Descriptor for a functor represented by a reserved address.
@@ -409,6 +411,12 @@
                 du_arg_width        :: arg_width
             ).
 
+    % Information about subtypes in the arguments of a functor.
+    %
+:- type functor_subtype_info
+    --->    functor_subtype_none
+    ;       functor_subtype_exists.
+
     % An rtti_maybe_pseudo_type_info identifies the type of a function
     % symbol's argument. If the type of the argument is the same as the
     % type of the whole term, it should be bound to self. Otherwise, if
@@ -761,6 +769,11 @@
 :- pred sectag_and_locn_to_locn_string(sectag_and_locn::in, string::out)
     is det.
 
+    % Return the C representation of a functor's subtype info.
+    %
+:- pred functor_subtype_info_to_string(functor_subtype_info::in, string::out)
+    is det.
+
     % Return the C representation of the type_ctor_rep value of the given
     % type_ctor.
     %
@@ -1590,6 +1603,15 @@ sectag_and_locn_to_locn_string(SecTag, String) :-
         String = "MR_SECTAG_REMOTE"
     ).
 
+functor_subtype_info_to_string(FunctorSubtypeInfo, String) :-
+    (
+        FunctorSubtypeInfo = functor_subtype_none,
+        String = "MR_FUNCTOR_SUBTYPE_NONE"
+    ;
+        FunctorSubtypeInfo = functor_subtype_exists,
+        String = "MR_FUNCTOR_SUBTYPE_EXISTS"
+    ).
+
 type_ctor_rep_to_string(TypeCtorData, RepStr) :-
     TypeCtorDetails = TypeCtorData ^ tcr_rep_details,
     (
diff --git a/compiler/rtti_out.m b/compiler/rtti_out.m
index 2cb9da8..9a58084 100644
--- a/compiler/rtti_out.m
+++ b/compiler/rtti_out.m
@@ -839,7 +839,8 @@ output_foreign_enum_functor_defn(Info, RttiTypeCtor, ForeignEnumFunctor,
     notag_functor::in, decl_set::in, decl_set::out, io::di, io::uo) is det.
 
 output_notag_functor_defn(Info, RttiTypeCtor, NotagFunctor, !DeclSet, !IO) :-
-    NotagFunctor = notag_functor(FunctorName, ArgType, MaybeArgName),
+    NotagFunctor = notag_functor(FunctorName, ArgType, MaybeArgName,
+        FunctorSubtypeInfo),
     output_maybe_pseudo_type_info_defn(Info, ArgType, !DeclSet, !IO),
     ArgTypeData = maybe_pseudo_type_info_to_rtti_data(ArgType),
     output_record_rtti_data_decls(Info, ArgTypeData, "", "", 0, _,
@@ -871,6 +872,8 @@ output_notag_functor_defn(Info, RttiTypeCtor, NotagFunctor, !DeclSet, !IO) :-
         MaybeArgName = no,
         io.write_string("NULL", !IO)
     ),
+    io.write_string(",\n\t", !IO),
+    output_functor_subtype_info(FunctorSubtypeInfo, !IO),
     io.write_string("\n};\n", !IO).
 
 :- pred output_du_functor_defn(llds_out_info::in, rtti_type_ctor::in,
@@ -878,7 +881,7 @@ output_notag_functor_defn(Info, RttiTypeCtor, NotagFunctor, !DeclSet, !IO) :-
 
 output_du_functor_defn(Info, RttiTypeCtor, DuFunctor, !DeclSet, !IO) :-
     DuFunctor = du_functor(FunctorName, OrigArity, Ordinal, Rep,
-        ArgInfos, MaybeExistInfo),
+        ArgInfos, MaybeExistInfo, FunctorSubtypeInfo),
     ArgTypes = list.map(du_arg_info_type, ArgInfos),
     MaybeArgNames = list.map(du_arg_info_name, ArgInfos),
     HaveArgNames = (if list.member(yes(_), MaybeArgNames) then yes else no),
@@ -981,8 +984,22 @@ output_du_functor_defn(Info, RttiTypeCtor, DuFunctor, !DeclSet, !IO) :-
         MaybeExistInfo = no,
         io.write_string("NULL", !IO)
     ),
+    io.write_string(",\n\t", !IO),
+    output_functor_subtype_info(FunctorSubtypeInfo, !IO),
     io.write_string("\n};\n", !IO).
 
+:- pred output_functor_subtype_info(functor_subtype_info::in, io::di, io::uo)
+    is det.
+
+output_functor_subtype_info(FunctorSubtypeInfo, !IO) :-
+    (
+        FunctorSubtypeInfo = functor_subtype_none,
+        io.write_string("MR_FUNCTOR_SUBTYPE_NONE", !IO)
+    ;
+        FunctorSubtypeInfo = functor_subtype_exists,
+        io.write_string("MR_FUNCTOR_SUBTYPE_EXISTS", !IO)
+    ).
+
 :- pred output_res_functor_defn(llds_out_info::in, rtti_type_ctor::in,
     reserved_functor::in, decl_set::in, decl_set::out, io::di, io::uo) is det.
 
diff --git a/compiler/rtti_to_mlds.m b/compiler/rtti_to_mlds.m
index 2cb3702..fc1a741 100644
--- a/compiler/rtti_to_mlds.m
+++ b/compiler/rtti_to_mlds.m
@@ -737,7 +737,8 @@ gen_foreign_enum_functor_desc(_ModuleInfo, Lang, RttiTypeCtor,
 
 gen_notag_functor_desc(ModuleInfo, RttiTypeCtor, NotagFunctorDesc,
         !GlobalData) :-
-    NotagFunctorDesc = notag_functor(FunctorName, ArgType, MaybeArgName),
+    NotagFunctorDesc = notag_functor(FunctorName, ArgType, MaybeArgName,
+        FunctorSubtypeInfo),
     ArgTypeRttiData = maybe_pseudo_type_info_to_rtti_data(ArgType),
     gen_pseudo_type_info(ModuleInfo, ArgTypeRttiData, PTIInitializer,
         !GlobalData),
@@ -746,7 +747,8 @@ gen_notag_functor_desc(ModuleInfo, RttiTypeCtor, NotagFunctorDesc,
     Initializer = init_struct(mlds_rtti_type(item_type(RttiId)), [
         gen_init_string(FunctorName),
         PTIInitializer,
-        gen_init_maybe(ml_string_type, gen_init_string, MaybeArgName)
+        gen_init_maybe(ml_string_type, gen_init_string, MaybeArgName),
+        gen_init_functor_subtype_info(FunctorSubtypeInfo)
     ]),
     rtti_id_and_init_to_defn(RttiId, Initializer, !GlobalData).
 
@@ -755,7 +757,7 @@ gen_notag_functor_desc(ModuleInfo, RttiTypeCtor, NotagFunctorDesc,
 
 gen_du_functor_desc(ModuleInfo, RttiTypeCtor, DuFunctor, !GlobalData) :-
     DuFunctor = du_functor(FunctorName, Arity, Ordinal, Rep, ArgInfos,
-        MaybeExistInfo),
+        MaybeExistInfo, FunctorSubtypeInfo),
     ArgTypes = list.map(du_arg_info_type, ArgInfos),
     MaybeArgNames = list.map(du_arg_info_name, ArgInfos),
     HaveArgNames = (if list.member(yes(_), MaybeArgNames) then yes else no),
@@ -843,7 +845,8 @@ gen_du_functor_desc(ModuleInfo, RttiTypeCtor, DuFunctor, !GlobalData) :-
         ArgTypeInitializer,
         ArgNameInitializer,
         ArgLocnsInitializer,
-        ExistInfoInitializer
+        ExistInfoInitializer,
+        gen_init_functor_subtype_info(FunctorSubtypeInfo)
     ]),
     rtti_id_and_init_to_defn(RttiId, Initializer, !GlobalData).
 
@@ -1722,9 +1725,9 @@ real_rtti_data(RttiData) :-
 %
 % Conversion functions for builtin enumeration types.
 %
-% This handles sectag_locn and type_ctor_rep. The rvals generated are just
-% named constants in the private_builtin module, which the Mercury runtime
-% is expected to define.
+% This handles sectag_locn, functor_subtype_info and type_ctor_rep. The rvals
+% generated are just named constants in the private_builtin module, which the
+% Mercury runtime is expected to define.
 
 :- func gen_init_pred_or_func(pred_or_func) = mlds_initializer.
 
@@ -1736,6 +1739,12 @@ gen_init_pred_or_func(PredOrFunc) = gen_init_builtin_const(Name) :-
 gen_init_sectag_locn(Locn) = gen_init_builtin_const(Name) :-
     rtti.sectag_locn_to_string(Locn, Name).
 
+:- func gen_init_functor_subtype_info(functor_subtype_info) = mlds_initializer.
+
+gen_init_functor_subtype_info(FunctorSubtypeInfo) = Initializer :-
+    rtti.functor_subtype_info_to_string(FunctorSubtypeInfo, Name),
+    Initializer = gen_init_builtin_const(Name).
+
 :- func gen_init_type_ctor_rep(type_ctor_data) = mlds_initializer.
 
 gen_init_type_ctor_rep(TypeCtorData) = gen_init_builtin_const(Name) :-
diff --git a/compiler/superhomogeneous.m b/compiler/superhomogeneous.m
index 1d2f000..6e05230 100644
--- a/compiler/superhomogeneous.m
+++ b/compiler/superhomogeneous.m
@@ -803,8 +803,8 @@ maybe_unravel_special_var_functor_unification(XVar, YAtom, YArgs,
             ContextPieces =
                 cord.singleton(words("In explicit type qualification:")),
             varset.coerce(!.VarSet, GenericVarSet),
-            parse_type(DeclType1, GenericVarSet, ContextPieces,
-                DeclTypeResult),
+            parse_type(no_allow_ho_inst_info, DeclType1, GenericVarSet,
+                ContextPieces, DeclTypeResult),
             (
                 DeclTypeResult = ok1(DeclType),
                 varset.coerce(!.VarSet, DeclVarSet),
diff --git a/compiler/try_expand.m b/compiler/try_expand.m
index 49b39a9..ed145fc 100644
--- a/compiler/try_expand.m
+++ b/compiler/try_expand.m
@@ -829,8 +829,8 @@ make_try_lambda(Body0, OutputVarsSet, OutputTupleType, MaybeIO,
         LambdaParamModes = [out_mode],
         NonLocals = NonLocals0
     ),
-    LambdaType = higher_order_type(LambdaParamTypes, no, purity_pure,
-        lambda_normal),
+    LambdaType = higher_order_type(pf_predicate, LambdaParamTypes,
+        none_or_default_func, purity_pure, lambda_normal),
     proc_info_create_var_from_type(LambdaType, yes("TryLambda"), LambdaVar,
         !ProcInfo),
 
diff --git a/compiler/type_constraints.m b/compiler/type_constraints.m
index f6cbe6e..7ae63fd 100644
--- a/compiler/type_constraints.m
+++ b/compiler/type_constraints.m
@@ -888,10 +888,10 @@ simple_find_domain(stconstr(TVarA, TypeA), !DomainMap) :-
         NewTypeA = tuple_type(ArgTypes, Kind),
         restrict_domain(TVarA, NewTypeA, !DomainMap)
     ;
-        TypeA = higher_order_type(ArgTypes0, ReturnType0, Purity, Lambda),
+        TypeA = higher_order_type(PorF, ArgTypes0, HOInstInfo, Purity, Lambda),
         list.map(find_type_of_tvar(!.DomainMap), ArgTypes0, ArgTypes),
-        map_maybe(find_type_of_tvar(!.DomainMap), ReturnType0, ReturnType),
-        NewTypeA = higher_order_type(ArgTypes, ReturnType, Purity, Lambda),
+        NewTypeA = higher_order_type(PorF, ArgTypes, HOInstInfo, Purity,
+            Lambda),
         restrict_domain(TVarA, NewTypeA, !DomainMap)
     ;
         TypeA = apply_n_type(Return, ArgTypes0, Kind),
@@ -1158,21 +1158,11 @@ unify_types(A, B, Type) :-
                 fail
             )
         ;
-            A = higher_order_type(ArgsA, ResultA, Purity, Lambda),
-            B = higher_order_type(ArgsB, ResultB, Purity, Lambda),
+            A = higher_order_type(PorF, ArgsA, HOInstInfo, Purity, Lambda),
+            B = higher_order_type(PorF, ArgsB, HOInstInfo, Purity, Lambda),
             ( if list.same_length(ArgsA, ArgsB) then
                 list.map_corresponding(unify_types, ArgsA, ArgsB, Args),
-                (
-                    ResultA = yes(ResultA1),
-                    ResultB = yes(ResultB1),
-                    unify_types(ResultA1, ResultB1, Result1),
-                    Result = yes(Result1)
-                ;
-                    ResultA = no,
-                    ResultB = no,
-                    Result = no
-                ),
-                Type = higher_order_type(Args, Result, Purity, Lambda)
+                Type = higher_order_type(PorF, Args, HOInstInfo, Purity, Lambda)
             else
                 fail
             )
@@ -1814,17 +1804,9 @@ generic_call_goal_to_constraint(Environment, GoalExpr, GoalInfo, !TCInfo) :-
     list.map_foldl(get_var_type, Vars, ArgTVars, !TCInfo),
     ArgTypes = list.map(tvar_to_type, ArgTVars),
     (
-        Details = higher_order(CallVar, Purity, Kind, _),
-        (
-            Kind = pf_predicate,
-            HOType = higher_order_type(ArgTypes, no, Purity, lambda_normal)
-        ;
-            Kind = pf_function,
-            varset.new_var(FunctionTVar, !.TCInfo ^ tconstr_tvarset,
-                NewTVarSet),
-            !TCInfo ^ tconstr_tvarset := NewTVarSet,
-            HOType = apply_n_type(FunctionTVar, ArgTypes, kind_star)
-        ),
+        Details = higher_order(CallVar, Purity, PredOrFunc, _),
+        HOType = higher_order_type(PredOrFunc, ArgTypes, none_or_default_func,
+            Purity, lambda_normal),
         variable_assignment_constraint(Context, CallVar, HOType, !TCInfo)
     ;
         % Class methods are handled by looking up the method number in the
@@ -2026,23 +2008,16 @@ ho_pred_unif_constraint(PredTable, Info, LHSTVar, ArgTVars, PredId, Constraint,
         then
             ArgConstraints = list.map_corresponding(create_stconstr,
                 ArgTVars, HOArgTypes),
-            (
-                PredOrFunc = pf_predicate,
-                LHSConstraint = stconstr(LHSTVar, higher_order_type(
-                    LambdaTypes, no, Purity, lambda_normal))
-            ;
+            ( if
                 PredOrFunc = pf_function,
-                list.split_list(list.length(LambdaTypes) - 1, LambdaTypes,
-                    LambdaTypes1, [ReturnType]),
-                (
-                    LambdaTypes1 = [],
-                    LHSConstraint = stconstr(LHSTVar, ReturnType)
-                ;
-                    LambdaTypes1 = [_ | _],
-                    LHSConstraint = stconstr(LHSTVar, higher_order_type(
-                        LambdaTypes1, yes(ReturnType), Purity, lambda_normal))
-                )
+                LambdaTypes = [ReturnType]
+            then
+                Type = ReturnType
+            else
+                Type = higher_order_type(PredOrFunc, LambdaTypes,
+                    none_or_default_func, Purity, lambda_normal)
             ),
+            LHSConstraint = stconstr(LHSTVar, Type),
             Constraints = [LHSConstraint | ArgConstraints]
         else
             fail
@@ -2463,15 +2438,17 @@ type_to_string(TVarSet, Type, Name) :-
         list.map(type_to_string(TVarSet), Subtypes, SubtypeNames),
         Name = "{" ++  string.join_list(", ", SubtypeNames) ++ "}"
     ;
-        Type = higher_order_type(Subtypes, no, _, _),
-        list.map(type_to_string(TVarSet), Subtypes, SubtypeNames),
-        Name = "pred(" ++  string.join_list(", ", SubtypeNames) ++ ")"
-    ;
-        Type = higher_order_type(Subtypes, yes(ReturnType), _, _),
-        list.map(type_to_string(TVarSet), Subtypes, SubtypeNames),
-        type_to_string(TVarSet, ReturnType, ReturnTypeName),
-        Name = "func(" ++  string.join_list(", ", SubtypeNames) ++ ") = "
-            ++ ReturnTypeName
+        Type = higher_order_type(PorF, Types, _, _, _),
+        list.map(type_to_string(TVarSet), Types, TypeNames),
+        (
+            PorF = pf_predicate,
+            Name = "pred(" ++  string.join_list(", ", TypeNames) ++ ")"
+        ;
+            PorF = pf_function,
+            list.det_split_last(TypeNames, ArgTypeNames, ReturnTypeName),
+            Name = "func(" ++  string.join_list(", ", ArgTypeNames) ++ ") = "
+                ++ ReturnTypeName
+        )
     ;
         Type = apply_n_type(_, Subtypes, _),
         list.map(type_to_string(TVarSet), Subtypes, SubtypeNames),
diff --git a/compiler/type_ctor_info.m b/compiler/type_ctor_info.m
index 42994ed..c532b07 100644
--- a/compiler/type_ctor_info.m
+++ b/compiler/type_ctor_info.m
@@ -488,7 +488,7 @@ impl_type_ctor("table_builtin", "ml_subgoal", 0, impl_ctor_subgoal).
     %
 :- func type_ctor_info_rtti_version = int.
 
-type_ctor_info_rtti_version = 15.
+type_ctor_info_rtti_version = 16.
 
 %---------------------------------------------------------------------------%
 
@@ -505,7 +505,13 @@ make_notag_details(TypeArity, SymName, ArgType, MaybeArgName, EqualityAxioms,
     ExistTvars = [],
     pseudo_type_info.construct_maybe_pseudo_type_info(ArgType,
         NumUnivTvars, ExistTvars, MaybePseudoTypeInfo),
-    Functor = notag_functor(FunctorName, MaybePseudoTypeInfo, MaybeArgName),
+    ( if ArgType = higher_order_type(_, _, higher_order(_), _, _) then
+        FunctorSubtypeInfo = functor_subtype_exists
+    else
+        FunctorSubtypeInfo = functor_subtype_none
+    ),
+    Functor = notag_functor(FunctorName, MaybePseudoTypeInfo, MaybeArgName,
+        FunctorSubtypeInfo),
     Details = tcd_notag(EqualityAxioms, Functor).
 
 %---------------------------------------------------------------------------%
@@ -765,8 +771,8 @@ make_maybe_res_functors(TypeCtor, [Functor | Functors], NextOrdinal,
     ConsId = cons(SymName, list.length(ConstructorArgs), TypeCtor),
     map.lookup(ConsTagMap, ConsId, ConsTag),
     get_maybe_reserved_rep(ConsTag, ConsRep),
-    list.map(generate_du_arg_info(TypeArity, ExistTvars),
-        ConstructorArgs, ArgInfos),
+    list.map_foldl(generate_du_arg_info(TypeArity, ExistTvars),
+        ConstructorArgs, ArgInfos, functor_subtype_none, FunctorSubtypeInfo),
     (
         ExistTvars = [],
         MaybeExistInfo = no
@@ -779,7 +785,7 @@ make_maybe_res_functors(TypeCtor, [Functor | Functors], NextOrdinal,
     (
         ConsRep = du_rep(DuRep),
         DuFunctor = du_functor(FunctorName, Arity, NextOrdinal, DuRep,
-            ArgInfos, MaybeExistInfo),
+            ArgInfos, MaybeExistInfo, FunctorSubtypeInfo),
         MaybeResFunctor = du_func(DuFunctor)
     ;
         ConsRep = reserved_rep(ResRep),
@@ -842,9 +848,11 @@ get_maybe_reserved_rep(ConsTag, ConsRep) :-
     ).
 
 :- pred generate_du_arg_info(int::in, existq_tvars::in, constructor_arg::in,
-    du_arg_info::out) is det.
+    du_arg_info::out, functor_subtype_info::in, functor_subtype_info::out)
+    is det.
 
-generate_du_arg_info(NumUnivTvars, ExistTvars, ConstructorArg, ArgInfo) :-
+generate_du_arg_info(NumUnivTvars, ExistTvars, ConstructorArg, ArgInfo,
+        !FunctorSubtypeInfo) :-
     ConstructorArg = ctor_arg(MaybeCtorFieldName, ArgType, ArgWidth, _Ctxt),
     (
         MaybeCtorFieldName = yes(ctor_field_name(SymName, _)),
@@ -865,7 +873,12 @@ generate_du_arg_info(NumUnivTvars, ExistTvars, ConstructorArg, ArgInfo) :-
         MaybePseudoTypeInfo = pseudo(PseudoTypeInfo),
         MaybePseudoTypeInfoOrSelf = pseudo(PseudoTypeInfo)
     ),
-    ArgInfo = du_arg_info(MaybeArgName, MaybePseudoTypeInfoOrSelf, ArgWidth).
+    ArgInfo = du_arg_info(MaybeArgName, MaybePseudoTypeInfoOrSelf, ArgWidth),
+    ( if ArgType = higher_order_type(_, _, higher_order(_), _, _) then
+        !:FunctorSubtypeInfo = functor_subtype_exists
+    else
+        true
+    ).
 
     % This function gives the size of the MR_du_functor_arg_type_contains_var
     % field of the C type MR_DuFunctorDesc in bits.
diff --git a/compiler/type_util.m b/compiler/type_util.m
index e230e92..9e2f74b 100644
--- a/compiler/type_util.m
+++ b/compiler/type_util.m
@@ -508,7 +508,7 @@ type_definitely_has_no_user_defined_eq_pred_2(ModuleInfo, Type, !SeenTypes) :-
                 Args, !SeenTypes)
         ;
             ( Type = defined_type(_, _, _)
-            ; Type = higher_order_type(_, _, _, _)
+            ; Type = higher_order_type(_, _, _, _, _)
             ; Type = apply_n_type(_, _, _)
             ; Type = kinded_type(_, _)
             ),
diff --git a/compiler/typecheck_errors.m b/compiler/typecheck_errors.m
index e6c6046..8839ff3 100644
--- a/compiler/typecheck_errors.m
+++ b/compiler/typecheck_errors.m
@@ -190,11 +190,11 @@
 :- import_module libs.options.
 :- import_module parse_tree.mercury_to_mercury.
 :- import_module parse_tree.parse_tree_out_term.
-:- import_module parse_tree.prog_io_type_name.
 :- import_module parse_tree.prog_out.
 :- import_module parse_tree.prog_type.
 :- import_module parse_tree.prog_type_subst.
 :- import_module parse_tree.prog_util.
+:- import_module parse_tree.unparse.
 
 :- import_module assoc_list.
 :- import_module bool.
diff --git a/compiler/unparse.m b/compiler/unparse.m
new file mode 100644
index 0000000..64b9b7b
--- /dev/null
+++ b/compiler/unparse.m
@@ -0,0 +1,754 @@
+%-----------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sw=4 et
+%-----------------------------------------------------------------------------%
+% Copyright (C) 2009-2012 The University of Melbourne.
+% Copyright (C) 2015-2016 The Mercury team.
+% This file may only be copied under the terms of the GNU General
+% Public License - see the file COPYING in the Mercury distribution.
+%-----------------------------------------------------------------------------%
+%
+% File: unparse.m.
+% Main authors: conway, fjh.
+%
+%-----------------------------------------------------------------------------%
+
+:- module parse_tree.unparse.
+:- interface.
+
+:- import_module parse_tree.parse_tree_out_info.
+:- import_module parse_tree.prog_data.
+
+:- import_module term.
+
+%-----------------------------------------------------------------------------%
+
+    % Convert a type back to a term.
+    %
+:- pred unparse_type(mer_type::in, term::out) is det.
+
+    % Convert a mode or inst to a term representation.
+    %
+:- func mode_to_term(output_lang, mer_mode) = prog_term.
+:- func mode_to_term_with_context(output_lang, prog_context, mer_mode)
+    = prog_term.
+:- func inst_to_term(output_lang, mer_inst) = prog_term.
+:- func inst_name_to_term(output_lang, inst_name) = prog_term.
+:- func inst_test_results_to_term(prog_context, inst_test_results) = prog_term.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module mdbcomp.
+:- import_module mdbcomp.prim_data.
+:- import_module mdbcomp.sym_name.
+:- import_module parse_tree.prog_out.
+:- import_module parse_tree.prog_util.
+:- import_module parse_tree.prog_io_util.
+
+:- import_module list.
+:- import_module require.
+:- import_module set.
+:- import_module string.
+
+%-----------------------------------------------------------------------------%
+
+:- func make_atom(prog_context, string) = prog_term.
+
+make_atom(Context, Name) =
+    term.functor(term.atom(Name), [], Context).
+
+%-----------------------------------------------------------------------------%
+
+unparse_type(Type, Term) :-
+    Context = term.context_init,
+    (
+        Type = type_variable(TVar, _),
+        Var = term.coerce_var(TVar),
+        Term = term.variable(Var, Context)
+    ;
+        Type = defined_type(SymName, Args, _),
+        unparse_type_list(Args, ArgTerms),
+        unparse_qualified_term(SymName, ArgTerms, Term)
+    ;
+        Type = builtin_type(BuiltinType),
+        builtin_type_to_string(BuiltinType, Name),
+        Term = term.functor(term.atom(Name), [], Context)
+    ;
+        Type = higher_order_type(PorF, PredArgTypes, HOInstInfo, Purity,
+            EvalMethod),
+        unparse_type_list(PredArgTypes, PredArgTypeTerms),
+        (
+            HOInstInfo = higher_order(pred_inst_info(_, PredArgModes, _, _)),
+            unparse_mode_list(PredArgModes, PredArgModeTerms),
+            combine_type_and_mode_terms(PredArgTypeTerms, PredArgModeTerms,
+                PredArgTerms)
+        ;
+            HOInstInfo = none_or_default_func,
+            PredArgTerms = PredArgTypeTerms
+        ),
+        (
+            PorF = pf_predicate,
+            Term0 = term.functor(term.atom("pred"), PredArgTerms, Context),
+            maybe_add_lambda_eval_method(EvalMethod, Term0, Term2)
+        ;
+            PorF = pf_function,
+            list.det_split_last(PredArgTerms, ArgTerms, RetTerm),
+            Term0 = term.functor(term.atom("func"), ArgTerms, Context),
+            maybe_add_lambda_eval_method(EvalMethod, Term0, Term1),
+            Term2 = term.functor(term.atom("="), [Term1, RetTerm], Context)
+        ),
+        maybe_add_purity_annotation(Purity, Term2, Term3),
+        maybe_add_detism(HOInstInfo, Term3, Term)
+    ;
+        Type = tuple_type(Args, _),
+        unparse_type_list(Args, ArgTerms),
+        Term = term.functor(term.atom("{}"), ArgTerms, Context)
+    ;
+        Type = apply_n_type(TVar, Args, _),
+        Var = term.coerce_var(TVar),
+        unparse_type_list(Args, ArgTerms),
+        Term = term.functor(term.atom(""),
+            [term.variable(Var, Context) | ArgTerms], Context)
+    ;
+        Type = kinded_type(_, _),
+        unexpected($module, $pred, "kind annotation")
+    ).
+
+:- pred unparse_type_list(list(mer_type)::in, list(term)::out) is det.
+
+unparse_type_list(Types, Terms) :-
+    list.map(unparse_type, Types, Terms).
+
+:- pred unparse_qualified_term(sym_name::in, list(term)::in, term::out) is det.
+
+unparse_qualified_term(unqualified(Name), Args, Term) :-
+    Context = term.context_init,
+    Term = term.functor(term.atom(Name), Args, Context).
+unparse_qualified_term(qualified(Qualifier, Name), Args, Term) :-
+    Context = term.context_init,
+    unparse_qualified_term(Qualifier, [], QualTerm),
+    Term0 = term.functor(term.atom(Name), Args, Context),
+    Term = term.functor(term.atom("."), [QualTerm, Term0], Context).
+
+:- pred combine_type_and_mode_terms(list(term)::in, list(term)::in,
+    list(term)::out) is det.
+
+combine_type_and_mode_terms([], [], []).
+combine_type_and_mode_terms([], [_ | _], _) :-
+    unexpected($module, $pred, "argument length mismatch").
+combine_type_and_mode_terms([_ | _], [], _) :-
+    unexpected($module, $pred, "argument length mismatch").
+combine_type_and_mode_terms([Type | Types], [Mode | Modes], [Term | Terms]) :-
+    Term = term.functor(term.atom("::"), [Type, Mode], term.context_init),
+    combine_type_and_mode_terms(Types, Modes, Terms).
+
+:- pred maybe_add_lambda_eval_method(lambda_eval_method::in, term::in,
+    term::out) is det.
+
+maybe_add_lambda_eval_method(lambda_normal, Term, Term).
+
+:- pred maybe_add_purity_annotation(purity::in, term::in, term::out) is det.
+
+maybe_add_purity_annotation(purity_pure, Term, Term).
+maybe_add_purity_annotation(purity_semipure, Term0, Term) :-
+    Context = term.context_init,
+    Term = term.functor(term.atom("semipure"), [Term0], Context).
+maybe_add_purity_annotation(purity_impure, Term0, Term) :-
+    Context = term.context_init,
+    Term = term.functor(term.atom("impure"), [Term0], Context).
+
+:- pred maybe_add_detism(ho_inst_info::in, term::in, term::out) is det.
+
+maybe_add_detism(none_or_default_func, Term, Term).
+maybe_add_detism(higher_order(pred_inst_info(_, _, _, Detism)), Term0, Term) :-
+    Context = term.context_init,
+    DetismTerm0 = det_to_term(Context, Detism),
+    term.coerce(DetismTerm0, DetismTerm),
+    Term = term.functor(term.atom("is"), [Term0, DetismTerm], Context).
+
+%-----------------------------------------------------------------------------%
+
+:- pred unparse_mode_list(list(mer_mode)::in, list(term)::out) is det.
+
+unparse_mode_list([], []).
+unparse_mode_list([Mode | Modes], [Term | Terms]) :-
+    Term0 = mode_to_term(output_mercury, Mode),
+    term.coerce(Term0, Term),
+    unparse_mode_list(Modes, Terms).
+
+mode_to_term(Lang, Mode) =
+    mode_to_term_with_context(Lang, term.context_init, Mode).
+
+mode_to_term_with_context(Lang, Context, Mode) = Term :-
+    (
+        Mode = (InstA -> InstB),
+        ( if
+            % Check for higher-order pred or func modes, and output them
+            % in a nice format.
+            InstA = ground(_Uniq, higher_order(_)),
+            InstB = InstA
+        then
+            Term = inst_to_term_with_context(Lang, Context, InstA)
+        else
+            construct_qualified_term_with_context(unqualified(">>"),
+                [inst_to_term_with_context(Lang, Context, InstA),
+                inst_to_term_with_context(Lang, Context, InstB)],
+                Context, Term)
+        )
+    ;
+        Mode = user_defined_mode(Name, Args),
+        construct_qualified_term_with_context(Name,
+            list.map(inst_to_term_with_context(Lang, Context), Args),
+            Context, Term)
+    ).
+
+inst_to_term(Lang, Inst) =
+    inst_to_term_with_context(Lang, term.context_init, Inst).
+
+:- func inst_to_term_with_context(output_lang, prog_context, mer_inst)
+    = prog_term.
+
+inst_to_term_with_context(Lang, Context, Inst) = Term :-
+    (
+        Inst = any(Uniq, HOInstInfo),
+        (
+            HOInstInfo = higher_order(PredInstInfo),
+            Term = any_pred_inst_info_to_term(Lang, Context, Uniq,
+                PredInstInfo)
+        ;
+            HOInstInfo = none_or_default_func,
+            Term = make_atom(Context, any_inst_uniqueness(Uniq))
+        )
+    ;
+        Inst = free,
+        Term = make_atom(Context, "free")
+    ;
+        Inst = free(Type),
+        unparse_type(Type, Term0),
+        Term1 = term.coerce(Term0),
+        Term = term.functor(term.atom("free"), [Term1], Context)
+    ;
+        Inst = bound(Uniq, InstResults, BoundInsts),
+        (
+            Lang = output_mercury,
+            ArgTerms = [bound_insts_to_term(Lang, Context, BoundInsts)]
+        ;
+            Lang = output_debug,
+            ArgTerms =
+                [inst_test_results_to_term(Context, InstResults),
+                bound_insts_to_term(Lang, Context, BoundInsts)]
+        ),
+        construct_qualified_term_with_context(
+            unqualified(inst_uniqueness(Uniq, "bound")),
+            ArgTerms, Context, Term)
+    ;
+        Inst = ground(Uniq, HOInstInfo),
+        (
+            HOInstInfo = higher_order(PredInstInfo),
+            Term = ground_pred_inst_info_to_term(Lang, Context, Uniq,
+                PredInstInfo)
+        ;
+            HOInstInfo = none_or_default_func,
+            Term = make_atom(Context, inst_uniqueness(Uniq, "ground"))
+        )
+    ;
+        Inst = inst_var(Var),
+        Term = term.coerce(term.variable(Var, context_init))
+    ;
+        Inst = constrained_inst_vars(Vars, SubInst),
+        Term = set.fold(func(Var, VarTerm) =
+                term.functor(term.atom("=<"),
+                    [term.coerce(term.variable(Var, context_init)), VarTerm],
+                    Context),
+            Vars, inst_to_term_with_context(Lang, Context, SubInst))
+    ;
+        Inst = abstract_inst(Name, Args),
+        Term = inst_name_to_term_with_context(Lang, Context,
+            user_inst(Name, Args))
+    ;
+        Inst = defined_inst(InstName),
+        Term = inst_name_to_term_with_context(Lang, Context, InstName)
+    ;
+        Inst = not_reached,
+        Term = make_atom(Context, "not_reached")
+    ).
+
+inst_test_results_to_term(Context, InstResults) = Term :-
+    (
+        InstResults = inst_test_results(GroundnessResult, AnyResult,
+            InstNamesResult, InstVarsResult, TypeResult, PropagatedResult),
+        SubTerm1 = inst_result_groundness_to_term(Context, GroundnessResult),
+        SubTerm2 = inst_result_contains_any_to_term(Context, AnyResult),
+        SubTerm3 = inst_result_contains_inst_names_to_term(Context,
+            InstNamesResult),
+        SubTerm4 = inst_result_contains_inst_vars_to_term(Context,
+            InstVarsResult),
+        SubTerm5 = inst_result_contains_types_to_term(Context, TypeResult),
+        SubTerm6 = inst_result_type_ctor_propagated_to_term(Context,
+            PropagatedResult),
+        Term = term.functor(term.atom("results"),
+            [SubTerm1, SubTerm2, SubTerm3, SubTerm4, SubTerm5, SubTerm6],
+            Context)
+    ;
+        InstResults = inst_test_no_results,
+        Term = term.functor(term.atom("no_results"), [], Context)
+    ;
+        InstResults = inst_test_results_fgtc,
+        Term = term.functor(term.atom("fgtc"), [], Context)
+    ).
+
+:- func inst_result_groundness_to_term(prog_context, inst_result_groundness)
+    = prog_term.
+
+inst_result_groundness_to_term(Context, Groundness) = Term :-
+    (
+        Groundness = inst_result_is_not_ground,
+        Term = term.functor(term.atom("is_not_ground"), [], Context)
+    ;
+        Groundness = inst_result_is_ground,
+        Term = term.functor(term.atom("is_ground"), [], Context)
+    ;
+        Groundness = inst_result_groundness_unknown,
+        Term = term.functor(term.atom("groundness_unknown"), [], Context)
+    ).
+
+:- func inst_result_contains_any_to_term(prog_context,
+    inst_result_contains_any) = prog_term.
+
+inst_result_contains_any_to_term(Context, ContainsAny) = Term :-
+    (
+        ContainsAny = inst_result_does_not_contain_any,
+        Term = term.functor(term.atom("does_not_contain_any"), [], Context)
+    ;
+        ContainsAny = inst_result_does_contain_any,
+        Term = term.functor(term.atom("does_contain_any"), [], Context)
+    ;
+        ContainsAny = inst_result_contains_any_unknown,
+        Term = term.functor(term.atom("contains_any_unknown"), [], Context)
+    ).
+
+:- func inst_result_contains_inst_names_to_term(prog_context,
+    inst_result_contains_inst_names) = prog_term.
+
+inst_result_contains_inst_names_to_term(Context, ContainsInstNames) = Term :-
+    (
+        ContainsInstNames = inst_result_contains_inst_names_unknown,
+        Term = term.functor(term.atom("contains_inst_names_unknown"),
+            [], Context)
+    ;
+        ContainsInstNames = inst_result_contains_inst_names_known(InstNameSet),
+        % Inst names can be pretty big, so we print only a count.
+        % If necessary, we can later modify this code to actually print them.
+        set.count(InstNameSet, NumInstNames),
+        CountTerm = term.functor(term.integer(NumInstNames), [], Context),
+        Term = term.functor(term.atom("contains_inst_names_known"),
+            [CountTerm], Context)
+    ).
+
+:- func inst_result_contains_inst_vars_to_term(prog_context,
+    inst_result_contains_inst_vars) = prog_term.
+
+inst_result_contains_inst_vars_to_term(Context, ContainsInstVars) = Term :-
+    (
+        ContainsInstVars = inst_result_contains_inst_vars_unknown,
+        Term = term.functor(term.atom("contains_inst_vars_unknown"),
+            [], Context)
+    ;
+        ContainsInstVars = inst_result_contains_inst_vars_known(InstVarSet),
+        set.to_sorted_list(InstVarSet, InstVars),
+        InstVarTerms = list.map(inst_var_to_term(Context), InstVars),
+        Term = term.functor(term.atom("contains_inst_vars_known"),
+            InstVarTerms, Context)
+    ).
+
+:- func inst_var_to_term(prog_context, inst_var) = prog_term.
+
+inst_var_to_term(Context, InstVar) = Term :-
+    InstVarNum = term.var_to_int(InstVar),
+    InstVarNumStr = string.int_to_string(InstVarNum),
+    Term = term.functor(string("inst_var_" ++ InstVarNumStr), [], Context).
+
+:- func inst_result_contains_types_to_term(prog_context,
+    inst_result_contains_types) = prog_term.
+
+inst_result_contains_types_to_term(Context, ContainsTypes) = Term :-
+    (
+        ContainsTypes = inst_result_contains_types_unknown,
+        Term = term.functor(term.atom("contains_types_unknown"), [], Context)
+    ;
+        ContainsTypes = inst_result_contains_types_known(TypeCtorSet),
+        set.to_sorted_list(TypeCtorSet, TypeCtors),
+        TypeCtorTerms = list.map(type_ctor_to_term(Context), TypeCtors),
+        Term = term.functor(term.atom("contains_types_known"),
+            TypeCtorTerms, Context)
+    ).
+
+:- func inst_result_type_ctor_propagated_to_term(prog_context,
+    inst_result_type_ctor_propagated) = prog_term.
+
+inst_result_type_ctor_propagated_to_term(Context, PropagatedResult) = Term :-
+    (
+        PropagatedResult = inst_result_no_type_ctor_propagated,
+        Term = term.functor(term.atom("no_type_ctor_propagated"), [], Context)
+    ;
+        PropagatedResult = inst_result_type_ctor_propagated(TypeCtor),
+        Term = term.functor(term.atom("type_ctor_propagated"),
+            [type_ctor_to_term(Context, TypeCtor)], Context)
+    ).
+
+:- func type_ctor_to_term(prog_context, type_ctor) = prog_term.
+
+type_ctor_to_term(Context, TypeCtor) = Term :-
+    TypeCtor = type_ctor(SymName, Arity),
+    string.format("%s/%d", [s(sym_name_to_string(SymName)), i(Arity)],
+        ConsName),
+    Term = term.functor(term.atom(ConsName), [], Context).
+
+:- func ground_pred_inst_info_to_term(output_lang, prog_context, uniqueness,
+    pred_inst_info) = prog_term.
+
+ground_pred_inst_info_to_term(Lang, Context, _Uniq, PredInstInfo) = Term :-
+    % XXX we ignore Uniq
+    PredInstInfo = pred_inst_info(PredOrFunc, Modes, _, Det),
+    (
+        PredOrFunc = pf_predicate,
+        construct_qualified_term_with_context(unqualified("pred"),
+            list.map(mode_to_term_with_context(Lang, Context), Modes),
+            Context, ModesTerm)
+    ;
+        PredOrFunc = pf_function,
+        pred_args_to_func_args(Modes, ArgModes, RetMode),
+        construct_qualified_term_with_context(unqualified("func"),
+            list.map(mode_to_term_with_context(Lang, Context), ArgModes),
+            Context, ArgModesTerm),
+        construct_qualified_term_with_context(unqualified("="),
+            [ArgModesTerm, mode_to_term_with_context(Lang, Context, RetMode)],
+            Context, ModesTerm)
+    ),
+    construct_qualified_term_with_context(unqualified("is"),
+        [ModesTerm, det_to_term(Context, Det)], Context, Term).
+
+:- func any_pred_inst_info_to_term(output_lang, prog_context, uniqueness,
+    pred_inst_info) = prog_term.
+
+any_pred_inst_info_to_term(Lang, Context, _Uniq, PredInstInfo) = Term :-
+    % XXX we ignore Uniq
+    PredInstInfo = pred_inst_info(PredOrFunc, Modes, _, Det),
+    (
+        PredOrFunc = pf_predicate,
+        construct_qualified_term_with_context(unqualified("any_pred"),
+            list.map(mode_to_term_with_context(Lang, Context), Modes),
+            Context, ModesTerm)
+    ;
+        PredOrFunc = pf_function,
+        pred_args_to_func_args(Modes, ArgModes, RetMode),
+        construct_qualified_term_with_context(unqualified("any_func"),
+            list.map(mode_to_term_with_context(Lang, Context), ArgModes),
+            Context, ArgModesTerm),
+        construct_qualified_term_with_context(unqualified("="),
+            [ArgModesTerm, mode_to_term_with_context(Lang, Context, RetMode)],
+            Context, ModesTerm)
+    ),
+    construct_qualified_term_with_context(unqualified("is"),
+        [ModesTerm, det_to_term(Context, Det)], Context, Term).
+
+inst_name_to_term(Lang, InstName) =
+    inst_name_to_term_with_context(Lang, term.context_init, InstName).
+
+:- func inst_name_to_term_with_context(output_lang, prog_context, inst_name)
+    = prog_term.
+
+inst_name_to_term_with_context(Lang, Context, InstName) = Term :-
+    (
+        InstName = user_inst(Name, Args),
+        construct_qualified_term_with_context(Name,
+            list.map(inst_to_term_with_context(Lang, Context), Args),
+            Context, Term)
+    ;
+        InstName = unify_inst(Liveness, Real, InstA, InstB),
+        (
+            Lang = output_mercury,
+            unexpected($module, $pred, "unify_inst")
+        ;
+            Lang = output_debug,
+            construct_qualified_term_with_context(unqualified("$unify"),
+                [make_atom(Context, is_live_to_str(Liveness)),
+                make_atom(Context, unify_is_real_to_str(Real)),
+                inst_to_term_with_context(Lang, Context, InstA),
+                inst_to_term_with_context(Lang, Context, InstB)],
+                Context, Term)
+        )
+    ;
+        InstName = merge_inst(InstA, InstB),
+        (
+            Lang = output_mercury,
+            unexpected($module, $pred, "merge_inst")
+        ;
+            Lang = output_debug,
+            construct_qualified_term_with_context(unqualified("$merge_inst"),
+                list.map(inst_to_term_with_context(Lang, Context),
+                [InstA, InstB]),
+                Context, Term)
+        )
+    ;
+        InstName = ground_inst(SubInstName, Uniq, IsLive, Real),
+        (
+            Lang = output_mercury,
+            unexpected($module, $pred, "ground_inst")
+        ;
+            Lang = output_debug,
+            construct_qualified_term_with_context(unqualified("$ground"),
+                [inst_name_to_term_with_context(Lang, Context, SubInstName),
+                make_atom(Context, inst_uniqueness(Uniq, "shared")),
+                make_atom(Context, is_live_to_str(IsLive)),
+                make_atom(Context, unify_is_real_to_str(Real))],
+                Context, Term)
+        )
+    ;
+        InstName = any_inst(SubInstName, Uniq, IsLive, Real),
+        (
+            Lang = output_mercury,
+            unexpected($module, $pred, "any_inst")
+        ;
+            Lang = output_debug,
+            construct_qualified_term_with_context(unqualified("$any"),
+                [inst_name_to_term_with_context(Lang, Context, SubInstName),
+                make_atom(Context, inst_uniqueness(Uniq, "shared")),
+                make_atom(Context, is_live_to_str(IsLive)),
+                make_atom(Context, unify_is_real_to_str(Real))],
+                Context, Term)
+        )
+    ;
+        InstName = shared_inst(SubInstName),
+        (
+            Lang = output_mercury,
+            unexpected($module, $pred, "shared_inst")
+        ;
+            Lang = output_debug,
+            construct_qualified_term_with_context(unqualified("$shared_inst"),
+                [inst_name_to_term_with_context(Lang, Context, SubInstName)],
+                Context, Term)
+        )
+    ;
+        InstName = mostly_uniq_inst(SubInstName),
+        (
+            Lang = output_mercury,
+            unexpected($module, $pred, "mostly_uniq_inst")
+        ;
+            Lang = output_debug,
+            construct_qualified_term_with_context(
+                unqualified("$mostly_uniq_inst"),
+                [inst_name_to_term_with_context(Lang, Context, SubInstName)],
+                Context, Term)
+        )
+    ;
+        InstName = typed_ground(Uniq, Type),
+        (
+            Lang = output_mercury,
+            unexpected($module, $pred, "typed_ground")
+        ;
+            Lang = output_debug,
+            unparse_type(Type, Term0),
+            construct_qualified_term_with_context(unqualified("$typed_ground"),
+                [make_atom(Context, inst_uniqueness(Uniq, "shared")),
+                term.coerce(Term0)],
+                Context, Term)
+        )
+    ;
+        InstName = typed_inst(Type, SubInstName),
+        (
+            Lang = output_mercury,
+            % Inst names in the inst tables can (and often do) have the types
+            % they apply pushed into them by inst_user.m. However, the typed
+            % nature of such inst names cannot (yet) be expressed in Mercury
+            % source code.
+            Term = inst_name_to_term_with_context(Lang, Context, SubInstName)
+        ;
+            Lang = output_debug,
+            unparse_type(Type, Term0),
+            construct_qualified_term_with_context(unqualified("$typed_inst"),
+                [term.coerce(Term0),
+                inst_name_to_term_with_context(Lang, Context, SubInstName)],
+                Context, Term)
+        )
+    ).
+
+:- func is_live_to_str(is_live) = string.
+
+is_live_to_str(is_live) = "live".
+is_live_to_str(is_dead) = "dead".
+
+:- func unify_is_real_to_str(unify_is_real) = string.
+
+unify_is_real_to_str(real_unify) = "real".
+unify_is_real_to_str(fake_unify) = "fake".
+
+:- func any_inst_uniqueness(uniqueness) = string.
+
+any_inst_uniqueness(shared) = "any".
+any_inst_uniqueness(unique) = "unique_any".
+any_inst_uniqueness(mostly_unique) = "mostly_unique_any".
+any_inst_uniqueness(clobbered) = "clobbered_any".
+any_inst_uniqueness(mostly_clobbered) = "mostly_clobbered_any".
+
+:- func inst_uniqueness(uniqueness, string) = string.
+
+inst_uniqueness(shared, SharedName) = SharedName.
+inst_uniqueness(unique, _) = "unique".
+inst_uniqueness(mostly_unique, _) = "mostly_unique".
+inst_uniqueness(clobbered, _) = "clobbered".
+inst_uniqueness(mostly_clobbered, _) = "mostly_clobbered".
+
+:- func bound_insts_to_term(output_lang, prog_context, list(bound_inst))
+    = prog_term.
+
+bound_insts_to_term(_, Context, []) =
+    % This shouldn't happen, but when it does, the problem is a LOT easier
+    % to debug if there is a HLDS dump you can read.
+    term.functor(term.atom("EMPTY_BOUND_INSTS"), [], Context).
+bound_insts_to_term(Lang, Context, [BoundInst | BoundInsts]) =
+    bound_insts_to_term_2(Lang, Context, BoundInst, BoundInsts).
+
+:- func bound_insts_to_term_2(output_lang, prog_context,
+    bound_inst, list(bound_inst)) = prog_term.
+
+bound_insts_to_term_2(Lang, Context, BoundInst, BoundInsts) = Term :-
+    BoundInst = bound_functor(ConsId, Args),
+    ArgTerms = list.map(inst_to_term_with_context(Lang, Context), Args),
+    cons_id_and_args_to_term_full(ConsId, ArgTerms, FirstTerm),
+    (
+        BoundInsts = [],
+        Term = FirstTerm
+    ;
+        BoundInsts = [HeadBoundInst | TailBoundInsts],
+        SecondTerm = bound_insts_to_term_2(Lang, Context,
+            HeadBoundInst, TailBoundInsts),
+        construct_qualified_term_with_context(unqualified(";"),
+            [FirstTerm, SecondTerm], Context, Term)
+    ).
+
+:- pred cons_id_and_args_to_term_full(cons_id::in, list(prog_term)::in,
+    prog_term::out) is det.
+
+cons_id_and_args_to_term_full(ConsId, ArgTerms, Term) :-
+    (
+        ConsId = cons(SymName, _Arity, _TypeCtor),
+        construct_qualified_term(SymName, ArgTerms, Term)
+    ;
+        ConsId = tuple_cons(_Arity),
+        SymName = unqualified("{}"),
+        construct_qualified_term(SymName, ArgTerms, Term)
+    ;
+        ConsId = closure_cons(_, _),
+        term.context_init(Context),
+        FunctorName = "closure_cons",
+        Term = term.functor(term.string(FunctorName), [], Context)
+    ;
+        ConsId = int_const(Int),
+        term.context_init(Context),
+        Term = term.functor(term.integer(Int), [], Context)
+    ;
+        ConsId = float_const(Float),
+        term.context_init(Context),
+        Term = term.functor(term.float(Float), [], Context)
+    ;
+        ConsId = string_const(String),
+        term.context_init(Context),
+        Term = term.functor(term.string(String), [], Context)
+    ;
+        ConsId = char_const(Char),
+        SymName = unqualified(string.from_char(Char)),
+        construct_qualified_term(SymName, [], Term)
+    ;
+        ConsId = impl_defined_const(String),
+        term.context_init(Context),
+        FunctorName = "ImplDefinedConst: " ++ String,
+        Term = term.functor(term.string(FunctorName), [], Context)
+    ;
+        ConsId = type_ctor_info_const(ModuleName, TypeCtorName, Arity),
+        term.context_init(Context),
+        string.format("TypeCtorInfo for %s.%s/%d",
+            [s(sym_name_to_string(ModuleName)), s(TypeCtorName), i(Arity)],
+            FunctorName),
+        Term = term.functor(term.string(FunctorName), [], Context)
+    ;
+        ConsId = base_typeclass_info_const(_, _, _, _),
+        term.context_init(Context),
+        FunctorName = "base_typeclass_info_const",
+        Term = term.functor(term.string(FunctorName), [], Context)
+    ;
+        ConsId = type_info_cell_constructor(TypeCtor),
+        TypeCtor = type_ctor(TypeCtorName, Arity),
+        term.context_init(Context),
+        string.format("type_info_cell_constructor for %s/%d",
+            [s(sym_name_to_string(TypeCtorName)), i(Arity)], FunctorName),
+        Term = term.functor(term.string(FunctorName), [], Context)
+    ;
+        ConsId = typeclass_info_cell_constructor,
+        term.context_init(Context),
+        FunctorName = "typeclass_info_cell_constructor",
+        Term = term.functor(term.string(FunctorName), [], Context)
+    ;
+        ConsId = type_info_const(TIConstNum),
+        expect(unify(ArgTerms, []), $module, $pred,
+            "type_info_const arity != 0"),
+        term.context_init(Context),
+        FunctorName = "type_info_const",
+        Arg = term.functor(term.integer(TIConstNum), [], Context),
+        Term = term.functor(term.string(FunctorName), [Arg], Context)
+    ;
+        ConsId = typeclass_info_const(TCIConstNum),
+        expect(unify(ArgTerms, []), $module, $pred,
+            "typeclass_info_const arity != 0"),
+        term.context_init(Context),
+        FunctorName = "typeclass_info_const",
+        Arg = term.functor(term.integer(TCIConstNum), [], Context),
+        Term = term.functor(term.string(FunctorName), [Arg], Context)
+    ;
+        ConsId = ground_term_const(TCIConstNum, SubConsId),
+        expect(unify(ArgTerms, []), $module, $pred,
+            "ground_term_const arity != 0"),
+        cons_id_and_args_to_term_full(SubConsId, [], SubArg),
+        term.context_init(Context),
+        FunctorName = "ground_term_const",
+        NumArg = term.functor(term.integer(TCIConstNum), [], Context),
+        Term = term.functor(term.string(FunctorName), [NumArg, SubArg],
+            Context)
+    ;
+        ConsId = tabling_info_const(_),
+        term.context_init(Context),
+        FunctorName = "tabling_info_const",
+        Term = term.functor(term.string(FunctorName), [], Context)
+    ;
+        ConsId = table_io_entry_desc(_),
+        term.context_init(Context),
+        FunctorName = "table_io_entry_desc",
+        Term = term.functor(term.string(FunctorName), [], Context)
+    ;
+        ConsId = deep_profiling_proc_layout(_),
+        term.context_init(Context),
+        FunctorName = "deep_profiling_proc_layout",
+        Term = term.functor(term.string(FunctorName), [], Context)
+    ).
+
+:- func det_to_term(prog_context, determinism) = prog_term.
+
+det_to_term(Context, Det) = make_atom(Context, det_to_string(Det)).
+
+:- func det_to_string(determinism) = string.
+
+det_to_string(detism_erroneous) = "erroneous".
+det_to_string(detism_failure) = "failure".
+det_to_string(detism_det) = "det".
+det_to_string(detism_semi) = "semidet".
+det_to_string(detism_cc_multi) = "cc_multi".
+det_to_string(detism_cc_non) = "cc_nondet".
+det_to_string(detism_multi) = "multi".
+det_to_string(detism_non) = "nondet".
+
+
+%-----------------------------------------------------------------------------%
+:- end_module parse_tree.unparse.
+%-----------------------------------------------------------------------------%
diff --git a/compiler/unused_imports.m b/compiler/unused_imports.m
index 06afd79..0f79f86 100644
--- a/compiler/unused_imports.m
+++ b/compiler/unused_imports.m
@@ -751,14 +751,9 @@ mer_type_used_modules(Visibility, Type, !UsedModules) :-
                 !UsedModules)
         )
     ;
-        Type = higher_order_type(Args, MaybeReturn, _, _),
+        Type = higher_order_type(_, Args, HOInstInfo, _, _),
         list.foldl(mer_type_used_modules(Visibility), Args, !UsedModules),
-        (
-            MaybeReturn = yes(Return),
-            mer_type_used_modules(Visibility, Return, !UsedModules)
-        ;
-            MaybeReturn = no
-        )
+        ho_inst_info_used_modules(Visibility, HOInstInfo, !UsedModules)
     ;
         Type = tuple_type(ArgTypes, _),
         list.foldl(mer_type_used_modules(Visibility), ArgTypes, !UsedModules)
diff --git a/compiler/write_module_interface_files.m b/compiler/write_module_interface_files.m
index e938b99..a010088 100644
--- a/compiler/write_module_interface_files.m
+++ b/compiler/write_module_interface_files.m
@@ -1023,7 +1023,7 @@ ctor_arg_is_dummy_type(TypeDefnMap, Type, CoveredTypes0) = IsDummyType :-
         ( Type = type_variable(_, _)
         ; Type = builtin_type(_)
         ; Type = tuple_type(_, _)
-        ; Type = higher_order_type(_, _, _, _)
+        ; Type = higher_order_type(_, _, _, _, _)
         ; Type = apply_n_type(_, _, _)
         ; Type = kinded_type(_, _)
         ),
@@ -1356,14 +1356,8 @@ accumulate_modules_from_constraint_arg_type(ArgType, !Modules) :-
         ;
             ArgType = kinded_type(KindedType, _), Args = [KindedType]
         ;
-            ArgType = higher_order_type(Args0, MaybeRetType, _, _),
-            (
-                MaybeRetType = yes(RetType),
-                Args = [RetType  | Args0]
-            ;
-                MaybeRetType = no,
-                Args = Args0
-            )
+            ArgType = higher_order_type(_, Args, _HOInstInfo, _, _)
+            % XXX accumulate modules from ho_inst_info
         ),
         accumulate_modules_from_constraint_arg_types(Args, !Modules)
     ).
diff --git a/compiler/xml_documentation.m b/compiler/xml_documentation.m
index 6ae17bf..338f070 100644
--- a/compiler/xml_documentation.m
+++ b/compiler/xml_documentation.m
@@ -460,17 +460,20 @@ mer_type_to_xml(_, builtin_type(builtin_type_float)) = elem("float", [], []).
 mer_type_to_xml(_, builtin_type(builtin_type_string)) = elem("string", [], []).
 mer_type_to_xml(_, builtin_type(builtin_type_char)) =
     elem("character", [], []).
-mer_type_to_xml(TVarset, higher_order_type(Types, MaybeResult, _, _)) = Xml :-
-    XmlTypes = xml_list("higher_order_type_args", mer_type_to_xml(TVarset),
-        Types),
+mer_type_to_xml(TVarset, higher_order_type(PorF, Types, _, _, _)) = Xml :-
     (
-        MaybeResult = yes(ResultType),
+        PorF = pf_predicate,
+        XmlTypes = xml_list("higher_order_type_args", mer_type_to_xml(TVarset),
+            Types),
+        XmlChildren = [XmlTypes]
+    ;
+        PorF = pf_function,
+        list.det_split_last(Types, ArgTypes, ResultType),
+        XmlTypes = xml_list("higher_order_type_args", mer_type_to_xml(TVarset),
+            ArgTypes),
         XmlReturn = elem("return_type", [],
             [mer_type_to_xml(TVarset, ResultType)]),
         XmlChildren = [XmlTypes, XmlReturn]
-    ;
-        MaybeResult = no,
-        XmlChildren = [XmlTypes]
     ),
     Xml = elem("higher_order_type", [], XmlChildren).
 mer_type_to_xml(TVarset, tuple_type(Types, _)) = Xml :-
diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
index 283cc4a..4cd5c1e 100644
--- a/doc/reference_manual.texi
+++ b/doc/reference_manual.texi
@@ -2839,8 +2839,8 @@ the standard library modes @samp{in/1} and @samp{out/1}:
 @end example
 
 As for type declarations, a predicate or function can be defined
-to have a given higher-order inst (@pxref{Higher-order modes}) by using
- at code{`with_inst`} in the mode declaration.
+to have a given higher-order inst (@pxref{Higher-order insts and modes})
+by using @code{`with_inst`} in the mode declaration.
 
 For example,
 
@@ -4192,7 +4192,7 @@ higher-order procedures.)
 @menu
 * Creating higher-order terms::
 * Calling higher-order terms::
-* Higher-order modes::
+* Higher-order insts and modes::
 @end menu
 
 @node Creating higher-order terms
@@ -4469,15 +4469,24 @@ See also @samp{unsorted_solutions/2} and @samp{solutions_set/2}, which
 are defined in the standard library module @samp{solutions} and documented
 in the Mercury Library Reference Manual.
 
- at node Higher-order modes
- at section Higher-order modes
+ at node Higher-order insts and modes
+ at section Higher-order insts and modes
 
 In Mercury, the mode and determinism of a higher-order predicate or function
-term are part of that term's @emph{inst}, not its @emph{type}.
+term are generally part of that term's @emph{inst}, not its @emph{type}.
 This allows a single higher-order predicate to work on argument
 predicates of different modes and determinism, which is particularly
 useful for library predicates such as @samp{list.map} and @samp{list.foldl}.
 
+ at menu
+* Builtin higher-order insts and modes::
+* Default insts for functions::
+* Combined higher-order types and insts::
+ at end menu
+
+ at node Builtin higher-order insts and modes
+ at subsection Builtin higher-order insts and modes
+
 The language contains builtin @samp{inst} values
 
 @example
@@ -4554,6 +4563,24 @@ unifications; indirect attempts (via polymorphic predicates, for
 example @samp{(list.append([], [P], [Q])} may result in an error at
 run-time rather than at compile-time.
 
+Mercury also provides builtin @samp{inst} values for use with solver types:
+
+ at example
+any_pred is @var{Determinism}
+any_pred(@var{Mode}) is @var{Determinism}
+any_pred(@var{Mode1}, @var{Mode2}) is @var{Determinism}
+ at dots{}
+any_func = @var{Mode} is @var{Determinism}
+any_func(@var{Mode1}) = @var{Mode} is @var{Determinism}
+any_func(@var{Mode1}, @var{Mode2}) = @var{Mode} is @var{Determinism}
+ at dots{}
+ at end example
+
+See @ref{Solver types} for more details.
+
+ at node Default insts for functions
+ at subsection Default insts for functions
+
 In order to call a higher-order term, the compiler must know its higher-order
 inst.  This can cause problems when higher-order terms are placed into a
 polymorphic collection type and then extracted, since the declared mode for the
@@ -4575,20 +4602,63 @@ but note that there is little value in doing so because there is no
 default higher-order inst for predicates
 therefore it will not be possible to call those terms.
 
-Mercury also provides builtin @samp{inst} values for use with solver types:
+ at node Combined higher-order types and insts
+ at subsection Combined higher-order types and insts
+
+A higher-order type may optionally specify an inst in the following manner:
 
 @example
-any_pred is @var{Determinism}
-any_pred(@var{Mode}) is @var{Determinism}
-any_pred(@var{Mode1}, @var{Mode2}) is @var{Determinism}
+(pred) is @var{Determinism}
+pred(@var{Type}::@var{Mode}) is @var{Determinism}
+pred(@var{Type1}::@var{Mode1}, @var{Type2}::@var{Mode2}) is @var{Determinism}
 @dots{}
-any_func = @var{Mode} is @var{Determinism}
-any_func(@var{Mode1}) = @var{Mode} is @var{Determinism}
-any_func(@var{Mode1}, @var{Mode2}) = @var{Mode} is @var{Determinism}
+(func) = (@var{Type}::@var{Mode}) is @var{Determinism}
+func(@var{Type1}::@var{Mode1}) = (@var{Type}::@var{Mode}) is @var{Determinism}
+func(@var{Type1}::@var{Mode1}, @var{Type2}::@var{Mode2}) = (@var{Type}::@var{Mode}) is @var{Determinism}
 @dots{}
 @end example
 
-See @ref{Solver types} for more details.
+When used as argument types of functors in type declarations,
+types of this form have two effects.
+First, for any unification that constructs a term using such an argument,
+there is an additional mode constraint that
+the argument must be approximated by the inst.
+In other words, to be mode correct a program must not construct any term
+where a functor has an argument that does not have the declared inst,
+if present.
+
+The second effect is that when a unification deconstructs a ground term
+to extract an argument with such a declared inst,
+the extracted argument may then be used as if it had that inst.
+
+For example, given this type declaration:
+
+ at example
+:- type job ---> job(pred(int::out, io::di, io::uo) is det).
+ at end example
+
+the following goal is correct:
+
+ at example
+:- pred run(job::in, io::di, io::uo) is det.
+run(Job, !IO) :-
+    Job = job(Pred),
+    Pred(Result, !IO),          % Pred has the necessary inst
+    write_line(Result, !IO).
+ at end example
+
+However, the following would be a mode error:
+
+ at example
+:- pred bad(job::out) is det.
+bad(job(p)).                    % Error: p does not have required mode
+
+:- pred p(int::in, io::di, io::out) is det.
+ at dots{}
+ at end example
+
+Combined higher-order types and insts are currently only permitted
+as direct arguments of functors in discriminated unions.
 
 @node Modules
 @chapter Modules
diff --git a/java/runtime/DuFunctorDesc.java b/java/runtime/DuFunctorDesc.java
index 5643107..edc4174 100644
--- a/java/runtime/DuFunctorDesc.java
+++ b/java/runtime/DuFunctorDesc.java
@@ -21,6 +21,7 @@ public class DuFunctorDesc implements java.io.Serializable {
 	public /*final*/ java.lang.String[] du_functor_arg_names;
 	public /*final*/ DuArgLocn[] du_functor_arg_locns;
 	public /*final*/ DuExistInfo du_functor_exist_info;
+	public FunctorSubtypeInfo du_functor_subtype_info;
 
 	public DuFunctorDesc()
 	{
@@ -33,7 +34,8 @@ public class DuFunctorDesc implements java.io.Serializable {
 		java.lang.Object arg_types,
 		java.lang.Object arg_names,
 		java.lang.Object arg_locns,
-		java.lang.Object exist_info)
+		java.lang.Object exist_info,
+		int functor_subtype_info)
 	{
 		du_functor_name = functor_name;
 		du_functor_orig_arity = orig_arity;
@@ -47,5 +49,7 @@ public class DuFunctorDesc implements java.io.Serializable {
 		du_functor_arg_names = (java.lang.String []) arg_names;
 		du_functor_arg_locns = (DuArgLocn []) arg_locns;
 		du_functor_exist_info = (DuExistInfo) exist_info;
+		du_functor_subtype_info =
+			new FunctorSubtypeInfo(functor_subtype_info);
 	}
 }
diff --git a/java/runtime/FunctorSubtypeInfo.java b/java/runtime/FunctorSubtypeInfo.java
new file mode 100644
index 0000000..c5b1e9c
--- /dev/null
+++ b/java/runtime/FunctorSubtypeInfo.java
@@ -0,0 +1,19 @@
+//
+// Copyright (C) 2016 The Mercury Team.
+// This file may only be copied under the terms of the GNU Library General
+// Public License - see the file COPYING.LIB in the Mercury distribution.
+//
+
+package jmercury.runtime;
+
+public class FunctorSubtypeInfo implements java.io.Serializable {
+
+	public int value;
+
+	public FunctorSubtypeInfo(int arg) {
+		this.value = arg;
+	}
+}
+
+
+
diff --git a/library/construct.m b/library/construct.m
index 84fa504..0e41840 100644
--- a/library/construct.m
+++ b/library/construct.m
@@ -613,6 +613,13 @@ find_functor_2(TypeInfo, Functor, Arity, Num0, FunctorNumber, ArgTypes) :-
                 MR_fatal_error(""notag arg list is too long"");
             }
 
+            if (!MR_notag_subtype_none(type_ctor_info,
+                construct_info.functor_info.notag_functor_desc))
+            {
+                MR_fatal_error(""not yet implemented: construction ""
+                    ""of terms containing subtype constraints"");
+            }
+
             new_data = MR_field(MR_UNIV_TAG, MR_list_head(ArgList),
                 MR_UNIV_OFFSET_FOR_DATA);
             break;
@@ -675,6 +682,11 @@ find_functor_2(TypeInfo, Functor, Arity, Num0, FunctorNumber, ArgTypes) :-
                         ""of terms containing existential types"");
                 }
 
+                if (!MR_du_subtype_none(type_ctor_info, functor_desc)) {
+                    MR_fatal_error(""not yet implemented: construction ""
+                        ""of terms containing subtype constraints"");
+                }
+
                 arg_list = ArgList;
                 ptag = functor_desc->MR_du_functor_primary;
                 switch (functor_desc->MR_du_functor_sectag_locn) {
diff --git a/library/erlang_rtti_implementation.m b/library/erlang_rtti_implementation.m
index 5e29d9e..0e102fe 100644
--- a/library/erlang_rtti_implementation.m
+++ b/library/erlang_rtti_implementation.m
@@ -1220,11 +1220,11 @@ get_functor_with_names(TypeDesc, FunctorNum, Name, Arity, ArgTypeDescs,
         ArgNames) :-
     TypeInfo = type_info_from_type_desc(TypeDesc),
     MaybeResult = get_functor_with_names(TypeInfo, FunctorNum),
-    MaybeResult = yes({Name, Arity, ArgTypeInfos, ArgNames}),
+    MaybeResult = yes({Name, Arity, ArgTypeInfos, ArgNames, _SubtypeInfo}),
     ArgTypeDescs = type_descs_from_type_infos(ArgTypeInfos).
 
 :- func get_functor_with_names(type_info, int) =
-    maybe({string, int, list(type_info), list(string)}).
+    maybe({string, int, list(type_info), list(string), functor_subtype_info}).
 
 get_functor_with_names(TypeInfo, NumFunctor) = Result :-
     TypeCtorInfo = TypeInfo ^ type_ctor_info_evaled,
@@ -1255,7 +1255,8 @@ get_functor_with_names(TypeInfo, NumFunctor) = Result :-
 
             Name = string.from_char_list(FunctorRep ^ edu_name),
             Arity = FunctorRep ^ edu_orig_arity,
-            Result = yes({Name, Arity, ArgTypes, ArgNames})
+            SubtypeInfo = FunctorRep ^ edu_subtype_info,
+            Result = yes({Name, Arity, ArgTypes, ArgNames, SubtypeInfo})
         else
             Result = no
         )
@@ -1265,14 +1266,14 @@ get_functor_with_names(TypeInfo, NumFunctor) = Result :-
         Arity = 0,
         ArgTypes = [],
         ArgNames = [],
-        Result = yes({Name, Arity, ArgTypes, ArgNames})
+        Result = yes({Name, Arity, ArgTypes, ArgNames, functor_subtype_none})
     ;
         TypeCtorRep = etcr_tuple,
         type_ctor_info_and_args(TypeInfo, _TypeCtorInfo, ArgTypes),
         Name = "{}",
         Arity = list.length(ArgTypes),
         ArgNames = list.duplicate(Arity, ""),
-        Result = yes({Name, Arity, ArgTypes, ArgNames})
+        Result = yes({Name, Arity, ArgTypes, ArgNames, functor_subtype_none})
     ;
         TypeCtorRep = etcr_list,
         ( if NumFunctor = 0 then
@@ -1280,14 +1281,16 @@ get_functor_with_names(TypeInfo, NumFunctor) = Result :-
             Arity = 0,
             ArgTypes = [],
             ArgNames = [],
-            Result = yes({Name, Arity, ArgTypes, ArgNames})
+            Result = yes({Name, Arity, ArgTypes, ArgNames,
+                functor_subtype_none})
         else if NumFunctor = 1 then
             ArgTypeInfo = TypeInfo ^ type_info_index(1),
             Name = "[|]",
             Arity = 2,
             ArgTypes = [ArgTypeInfo, TypeInfo],
             ArgNames = ["", ""],
-            Result = yes({Name, Arity, ArgTypes, ArgNames})
+            Result = yes({Name, Arity, ArgTypes, ArgNames,
+                functor_subtype_none})
         else
             Result = no
         )
@@ -1414,9 +1417,17 @@ construct(TypeDesc, Index, Args) = Term :-
     (
         TypeCtorRep = etcr_du,
         Result = get_functor_with_names(TypeInfo, Index),
-        Result = yes({FunctorName, _FunctorArity, ArgTypes, _ArgNames}),
-        check_arg_types(Args, ArgTypes),
-        Term = construct_univ(TypeInfo, FunctorName, Args)
+        Result = yes({FunctorName, _FunctorArity, ArgTypes, _ArgNames,
+            SubtypeInfo}),
+        (
+            SubtypeInfo = functor_subtype_exists,
+            unexpected($module, $pred,
+                "unable to construct term with subtype constraints")
+        ;
+            SubtypeInfo = functor_subtype_none,
+            check_arg_types(Args, ArgTypes),
+            Term = construct_univ(TypeInfo, FunctorName, Args)
+        )
     ;
         TypeCtorRep = etcr_dummy,
         Index = 0,
@@ -2106,7 +2117,8 @@ det_dynamic_cast(Term, Actual) :-
                 edu_lex             :: int,
                 edu_rep             :: erlang_atom,
                 edu_arg_infos       :: list(du_arg_info),
-                edu_exist_info      :: maybe(exist_info)
+                edu_exist_info      :: maybe(exist_info),
+                edu_subtype_info    :: functor_subtype_info
             ).
 
 :- type du_arg_info
@@ -2124,6 +2136,10 @@ det_dynamic_cast(Term, Actual) :-
                 exist_typeinfo_locns        :: list(exist_typeinfo_locn)
             ).
 
+:- type functor_subtype_info
+    --->    functor_subtype_none
+    ;       functor_subtype_exists.
+
 :- type tc_constraint
     --->    tc_constraint(
                 tcc_class_name          :: tc_name,
diff --git a/library/private_builtin.m b/library/private_builtin.m
index c8271bf..784f8b5 100644
--- a/library/private_builtin.m
+++ b/library/private_builtin.m
@@ -1753,6 +1753,9 @@ const MR_FA_TypeInfo_Struct1 ML_type_info_for_list_of_pseudo_type_info = {
     public static final int MR_SECTAG_REMOTE            = 3;
     public static final int MR_SECTAG_VARIABLE          = 4;
 
+    public static final int MR_FUNCTOR_SUBTYPE_NONE     = 0;
+    public static final int MR_FUNCTOR_SUBTYPE_EXISTS   = 1;
+
     public static final int MR_PREDICATE    = 0;
     public static final int MR_FUNCTION     = 1;
 
diff --git a/library/rtti_implementation.m b/library/rtti_implementation.m
index 5155d1e..40c4454 100644
--- a/library/rtti_implementation.m
+++ b/library/rtti_implementation.m
@@ -1639,12 +1639,19 @@ is_exist_pseudo_type_info(_, _) :-
 
             case runtime.TypeCtorRep.MR_TYPECTOR_REP_DU:
             case runtime.TypeCtorRep.MR_TYPECTOR_REP_DU_USEREQ:
-                runtime.DuFunctorDesc[] functor_desc =
+                runtime.DuFunctorDesc[] functor_descs =
                     tc.type_functors.functors_du();
-                if (FunctorNumber >= 0 && FunctorNumber < functor_desc.Length)
+                if (FunctorNumber >= 0 && FunctorNumber < functor_descs.Length)
                 {
-                    new_data = ML_construct_du(tc, functor_desc[FunctorNumber],
-                        ArgList);
+                    runtime.DuFunctorDesc functor_desc =
+                        functor_descs[FunctorNumber];
+                    if (functor_desc.du_functor_subtype_info !=
+                        runtime.FunctorSubtypeInfo.MR_FUNCTOR_SUBTYPE_NONE)
+                    {
+                        runtime.Errors.SORRY(""construction of terms "" +
+                            ""containing subtype constraints"");
+                    }
+                    new_data = ML_construct_du(tc, functor_desc, ArgList);
                 }
                 break;
 
@@ -2018,11 +2025,16 @@ is_exist_pseudo_type_info(_, _) :-
 
             case private_builtin.MR_TYPECTOR_REP_DU:
             case private_builtin.MR_TYPECTOR_REP_DU_USEREQ:
-                DuFunctorDesc[] functor_desc = tc.type_functors.functors_du();
-                if (FunctorNumber >= 0 && FunctorNumber < functor_desc.length)
+                DuFunctorDesc[] functor_descs = tc.type_functors.functors_du();
+                if (FunctorNumber >= 0 && FunctorNumber < functor_descs.length)
                 {
-                    new_data = ML_construct_du(tc, functor_desc[FunctorNumber],
-                        ArgList);
+                    DuFunctorDesc functor_desc = functor_descs[FunctorNumber];
+                    if (functor_desc.du_functor_subtype_info.value !=
+                        private_builtin.MR_FUNCTOR_SUBTYPE_NONE) {
+                        throw new Error(""not yet implemented: construction ""
+                            + ""of terms containing subtype constraints"");
+                    }
+                    new_data = ML_construct_du(tc, functor_desc, ArgList);
                 }
                 break;
 
diff --git a/runtime/mercury_dotnet.cs.in b/runtime/mercury_dotnet.cs.in
index 938c523..9e01c28 100644
--- a/runtime/mercury_dotnet.cs.in
+++ b/runtime/mercury_dotnet.cs.in
@@ -669,6 +669,7 @@ public class DuFunctorDesc {
     public string[]         du_functor_arg_names;
     public DuArgLocn[]      du_functor_arg_locns;
     public DuExistInfo      du_functor_exist_info;
+    public FunctorSubtypeInfo   du_functor_subtype_info;
 
     public DuFunctorDesc() {
     }
@@ -685,7 +686,8 @@ public class DuFunctorDesc {
         object arg_types,
         object arg_names,
         object arg_locns,
-        object exist_info)
+        object exist_info,
+        FunctorSubtypeInfo functor_subtype_info)
     {
         du_functor_name = functor_name;
         du_functor_orig_arity = orig_arity;
@@ -699,6 +701,7 @@ public class DuFunctorDesc {
         du_functor_arg_names = (string[]) arg_names;
         du_functor_arg_locns = (DuArgLocn[]) arg_locns;
         du_functor_exist_info = (DuExistInfo) exist_info;
+        du_functor_subtype_info = functor_subtype_info;
     }
 }
 
@@ -709,6 +712,11 @@ public enum Sectag_Locn {
     MR_SECTAG_REMOTE            = 3
 }
 
+public enum FunctorSubtypeInfo {
+    MR_FUNCTOR_SUBTYPE_NONE     = 0,
+    MR_FUNCTOR_SUBTYPE_EXISTS   = 1
+}
+
 public class DuPtagLayout {
     public int          sectag_sharers;
     public Sectag_Locn  sectag_locn;
diff --git a/runtime/mercury_type_info.h b/runtime/mercury_type_info.h
index 9c06c00..9ecf71a 100644
--- a/runtime/mercury_type_info.h
+++ b/runtime/mercury_type_info.h
@@ -76,7 +76,7 @@
 ** compiler/type_ctor_info.m.
 */
 
-#define MR_RTTI_VERSION                     MR_RTTI_VERSION__ARG_WIDTHS
+#define MR_RTTI_VERSION                     MR_RTTI_VERSION__FUNCTOR_SUBTYPE
 #define MR_RTTI_VERSION__INITIAL            2
 #define MR_RTTI_VERSION__USEREQ             3
 #define MR_RTTI_VERSION__CLEAN_LAYOUT       4
@@ -91,6 +91,7 @@
 #define MR_RTTI_VERSION__BITMAP             13
 #define MR_RTTI_VERSION__DIRECT_ARG         14
 #define MR_RTTI_VERSION__ARG_WIDTHS         15
+#define MR_RTTI_VERSION__FUNCTOR_SUBTYPE    16
 
 /*
 ** Check that the RTTI version is in a sensible range.
@@ -880,6 +881,10 @@ typedef struct {
 ** field will be NULL. Otherwise, it points to an array of MR_DuArgLocn
 ** structures, describing the location and packing scheme of each visible
 ** argument.
+**
+** If any argument contains subtype information (for example, higher order
+** mode information) then the subtype_info field will be
+** MR_DU_SUBTYPE_INFO_EXISTS, otherwise it will be MR_DU_SUBTYPE_INFO_NONE.
 */
 
 typedef enum {
@@ -903,6 +908,16 @@ typedef struct {
     */
 } MR_DuArgLocn;
 
+/*
+** This type describes the subtype constraints on the arguments of a functor.
+** Currently, we only record whether any such constraints exist.
+*/
+
+typedef enum {
+    MR_DEFINE_BUILTIN_ENUM_CONST(MR_FUNCTOR_SUBTYPE_NONE),
+    MR_DEFINE_BUILTIN_ENUM_CONST(MR_FUNCTOR_SUBTYPE_EXISTS)
+} MR_FunctorSubtype;
+
 typedef struct {
     MR_ConstString          MR_du_functor_name;
     MR_int_least16_t        MR_du_functor_orig_arity;
@@ -915,6 +930,7 @@ typedef struct {
     const MR_ConstString    *MR_du_functor_arg_names;
     const MR_DuArgLocn      *MR_du_functor_arg_locns;
     const MR_DuExistInfo    *MR_du_functor_exist_info;
+    MR_FunctorSubtype       MR_du_functor_subtype;
 } MR_DuFunctorDesc;
 
 typedef const MR_DuFunctorDesc              *MR_DuFunctorDescPtr;
@@ -947,6 +963,10 @@ typedef const MR_DuFunctorDesc              *MR_DuFunctorDescPtr;
 #define MR_some_arg_type_contains_var(functor_desc)                     \
     ((functor_desc)->MR_du_functor_arg_type_contains_var > 0)
 
+#define MR_du_subtype_none(tci, functor_desc)                           \
+    ((tci)->MR_type_ctor_version < MR_RTTI_VERSION__FUNCTOR_SUBTYPE ||  \
+        (functor_desc)->MR_du_functor_subtype == MR_FUNCTOR_SUBTYPE_NONE)
+
 /*---------------------------------------------------------------------------*/
 
 typedef struct {
@@ -972,10 +992,15 @@ typedef struct {
     MR_ConstString      MR_notag_functor_name;
     MR_PseudoTypeInfo   MR_notag_functor_arg_type;
     MR_ConstString      MR_notag_functor_arg_name;
+    MR_FunctorSubtype   MR_notag_functor_subtype;
 } MR_NotagFunctorDesc;
 
 typedef const MR_NotagFunctorDesc           *MR_NotagFunctorDescPtr;
 
+#define MR_notag_subtype_none(tci, functor_desc)                        \
+    ((tci)->MR_type_ctor_version < MR_RTTI_VERSION__FUNCTOR_SUBTYPE ||  \
+        (functor_desc)->MR_notag_functor_subtype == MR_FUNCTOR_SUBTYPE_NONE)
+
 /*---------------------------------------------------------------------------*/
 
 typedef struct {
diff --git a/tests/hard_coded/Mmakefile b/tests/hard_coded/Mmakefile
index 2d3e8bd..0b0a049 100644
--- a/tests/hard_coded/Mmakefile
+++ b/tests/hard_coded/Mmakefile
@@ -135,6 +135,10 @@ ORDINARY_PROGS =	\
 	func_and_pred \
 	func_ctor_ambig \
 	func_test \
+	functor_ho_inst \
+	functor_ho_inst_2 \
+	functor_ho_inst_excp \
+	functor_ho_inst_excp_2 \
 	getopt_test \
 	ground_dd \
 	ground_terms \
@@ -778,6 +782,30 @@ init_excp.out: init_excp
 		mv $@.tmp $@; \
 	fi
 
+# functor_ho_inst_excp.out is expected to throw an exception or cause
+# a runtime abort
+functor_ho_inst_excp.out: functor_ho_inst_excp
+	if MERCURY_SUPPRESS_STACK_TRACE=yes ./functor_ho_inst_excp \
+			> $@.tmp 2>&1; \
+	then \
+		grep  . $@.tmp; \
+		exit 1; \
+	else \
+		mv $@.tmp $@; \
+	fi
+
+# functor_ho_inst_excp_2.out is expected to throw an exception or cause
+# a runtime abort
+functor_ho_inst_excp_2.out: functor_ho_inst_excp_2
+	if MERCURY_SUPPRESS_STACK_TRACE=yes ./functor_ho_inst_excp_2 \
+			> $@.tmp 2>&1; \
+	then \
+		grep  . $@.tmp; \
+		exit 1; \
+	else \
+		mv $@.tmp $@; \
+	fi
+
 # mutable_excp.out is expected to fail (it calls throw/1).
 #
 mutable_excp.out: mutable_excp
diff --git a/tests/hard_coded/functor_ho_inst.exp b/tests/hard_coded/functor_ho_inst.exp
new file mode 100644
index 0000000..6ed7baa
--- /dev/null
+++ b/tests/hard_coded/functor_ho_inst.exp
@@ -0,0 +1,2 @@
+job_result_ok
+job_result_failed
diff --git a/tests/hard_coded/functor_ho_inst.m b/tests/hard_coded/functor_ho_inst.m
new file mode 100644
index 0000000..1246f04
--- /dev/null
+++ b/tests/hard_coded/functor_ho_inst.m
@@ -0,0 +1,44 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+%
+% Use a functor with a higher-order argument with an inst.
+%
+
+:- module functor_ho_inst.
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+:- implementation.
+
+:- import_module list.
+
+:- type job
+    --->    job(pred(job_result::out, io::di, io::uo) is det).
+
+:- type job_result
+    --->    job_result_ok
+    ;       job_result_failed.
+
+:- pred run(job::in, io::di, io::uo) is det.
+
+run(Job, !IO) :-
+    Job = job(Pred),
+    Pred(Result, !IO),
+    io.write_line(Result, !IO).
+
+:- pred j1(job_result::out, io::di, io::uo) is det.
+
+j1(job_result_ok, !IO).
+
+:- pred j2(job_result::out, io::di, io::uo) is det.
+
+j2(job_result_failed, !IO).
+
+main(!IO) :-
+    Jobs = [job(j1), job(j2)],
+    list.foldl(run, Jobs, !IO).
+
diff --git a/tests/hard_coded/functor_ho_inst_2.exp b/tests/hard_coded/functor_ho_inst_2.exp
new file mode 100644
index 0000000..6ed7baa
--- /dev/null
+++ b/tests/hard_coded/functor_ho_inst_2.exp
@@ -0,0 +1,2 @@
+job_result_ok
+job_result_failed
diff --git a/tests/hard_coded/functor_ho_inst_2.m b/tests/hard_coded/functor_ho_inst_2.m
new file mode 100644
index 0000000..5d6646a
--- /dev/null
+++ b/tests/hard_coded/functor_ho_inst_2.m
@@ -0,0 +1,45 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+%
+% Same as functor_ho_inst except the extra functor argument makes it a
+% proper du functor rather than a notag functor.
+%
+
+:- module functor_ho_inst_2.
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+:- implementation.
+
+:- import_module list.
+
+:- type job
+    --->    job(int, pred(job_result::out, io::di, io::uo) is det).
+
+:- type job_result
+    --->    job_result_ok
+    ;       job_result_failed.
+
+:- pred run(job::in, io::di, io::uo) is det.
+
+run(Job, !IO) :-
+    Job = job(_, Pred),
+    Pred(Result, !IO),
+    io.write_line(Result, !IO).
+
+:- pred j1(job_result::out, io::di, io::uo) is det.
+
+j1(job_result_ok, !IO).
+
+:- pred j2(job_result::out, io::di, io::uo) is det.
+
+j2(job_result_failed, !IO).
+
+main(!IO) :-
+    Jobs = [job(1, j1), job(2, j2)],
+    list.foldl(run, Jobs, !IO).
+
diff --git a/tests/hard_coded/functor_ho_inst_excp.exp b/tests/hard_coded/functor_ho_inst_excp.exp
new file mode 100644
index 0000000..8f6e097
--- /dev/null
+++ b/tests/hard_coded/functor_ho_inst_excp.exp
@@ -0,0 +1 @@
+Mercury runtime: not yet implemented: construction of terms containing subtype constraints
diff --git a/tests/hard_coded/functor_ho_inst_excp.m b/tests/hard_coded/functor_ho_inst_excp.m
new file mode 100644
index 0000000..79bbfe5
--- /dev/null
+++ b/tests/hard_coded/functor_ho_inst_excp.m
@@ -0,0 +1,51 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+%
+% Try to construct a term that violates a functor argument's higher-order inst.
+%
+
+:- module functor_ho_inst_excp.
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+:- implementation.
+
+:- import_module construct.
+:- import_module exception.
+:- import_module list.
+:- import_module type_desc.
+:- import_module univ.
+
+:- type job
+    ---> job(pred(int::in, string::out) is det).
+
+:- pred run(job::in, io::di, io::uo) is det.
+
+run(Job, !IO) :-
+    Job = job(Pred),
+    Pred(5, Result),
+    io.write_string("Printing result:\n", !IO),
+    io.write_string(Result, !IO),
+    io.write_string("\nEnd of result.\n", !IO).
+
+:- pred semi_job(int::in, string::out) is semidet.
+
+semi_job(1, "singular sensation").
+
+:- func bad_job = job.
+
+bad_job = Job :-
+    ( if univ_to_type(construct(type_of(Job), 0, [univ(semi_job)]), Job0) then
+        Job = Job0
+    else
+        throw("unable to create job")
+    ).
+
+main(!IO) :-
+    Jobs = [bad_job],
+    list.foldl(run, Jobs, !IO).
+
diff --git a/tests/hard_coded/functor_ho_inst_excp_2.exp b/tests/hard_coded/functor_ho_inst_excp_2.exp
new file mode 100644
index 0000000..8f6e097
--- /dev/null
+++ b/tests/hard_coded/functor_ho_inst_excp_2.exp
@@ -0,0 +1 @@
+Mercury runtime: not yet implemented: construction of terms containing subtype constraints
diff --git a/tests/hard_coded/functor_ho_inst_excp_2.m b/tests/hard_coded/functor_ho_inst_excp_2.m
new file mode 100644
index 0000000..e5db304
--- /dev/null
+++ b/tests/hard_coded/functor_ho_inst_excp_2.m
@@ -0,0 +1,53 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+%
+% Same as functor_ho_inst_excp except the extra functor argument makes it a
+% proper du functor rather than a notag functor.
+%
+
+:- module functor_ho_inst_excp_2.
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+:- implementation.
+
+:- import_module construct.
+:- import_module exception.
+:- import_module list.
+:- import_module type_desc.
+:- import_module univ.
+
+:- type job
+    ---> job(int, pred(int::in, string::out) is det).
+
+:- pred run(job::in, io::di, io::uo) is det.
+
+run(Job, !IO) :-
+    Job = job(_, Pred),
+    Pred(5, Result),
+    io.write_string("Printing result:\n", !IO),
+    io.write_string(Result, !IO),
+    io.write_string("\nEnd of result.\n", !IO).
+
+:- pred semi_job(int::in, string::out) is semidet.
+
+semi_job(1, "singular sensation").
+
+:- func bad_job = job.
+
+bad_job = Job :-
+    Args = [univ(1), univ(semi_job)],
+    ( if univ_to_type(construct(type_of(Job), 0, Args), Job0) then
+        Job = Job0
+    else
+        throw("unable to create job")
+    ).
+
+main(!IO) :-
+    Jobs = [bad_job],
+    list.foldl(run, Jobs, !IO).
+
diff --git a/tests/invalid/Mmakefile b/tests/invalid/Mmakefile
index 8d495ac..5af4259 100644
--- a/tests/invalid/Mmakefile
+++ b/tests/invalid/Mmakefile
@@ -87,6 +87,7 @@ SINGLEMODULE= \
 	circ_type2 \
 	circ_type3 \
 	circ_type5 \
+	combined_ho_type_inst \
 	comparison \
 	complex_constraint_err \
 	conflicting_fs \
@@ -130,6 +131,9 @@ SINGLEMODULE= \
 	func_class \
 	func_errors \
 	funcs_as_preds \
+	functor_ho_inst_bad \
+	functor_ho_inst_bad_2 \
+	functor_ho_inst_bad_3 \
 	fundeps_coverage \
 	fundeps_unbound_in_ctor \
 	fundeps_vars \
diff --git a/tests/invalid/combined_ho_type_inst.err_exp b/tests/invalid/combined_ho_type_inst.err_exp
new file mode 100644
index 0000000..21a69be
--- /dev/null
+++ b/tests/invalid/combined_ho_type_inst.err_exp
@@ -0,0 +1,23 @@
+combined_ho_type_inst.m:015: Error: ill-formed type (pred((int :: in), (int ::
+combined_ho_type_inst.m:015:   out)) is det).
+combined_ho_type_inst.m:016: Error: ill-formed type (((func (int :: in)) = (int
+combined_ho_type_inst.m:016:   :: out)) is semidet).
+combined_ho_type_inst.m:019: In type definition: error: ill-formed type
+combined_ho_type_inst.m:019:   (pred((int :: in), (int :: out)) is det).
+combined_ho_type_inst.m:021: In type definition: error: ill-formed type (((func
+combined_ho_type_inst.m:021:   (int :: in)) = (int :: out)) is semidet).
+combined_ho_type_inst.m:024: In type definition: error: ill-formed type (pred
+combined_ho_type_inst.m:024:   (pred((int :: in), (int :: out)) is det)).
+combined_ho_type_inst.m:026: In type definition: error: ill-formed type ((pred
+combined_ho_type_inst.m:026:   ((pred((int :: in), (int :: out)) is det) ::
+combined_ho_type_inst.m:026:   in)) is semidet).
+combined_ho_type_inst.m:028: In type definition: error: ill-formed type ((func
+combined_ho_type_inst.m:028:   (((func (int :: in)) = (int :: out)) is
+combined_ho_type_inst.m:028:   semidet)) = int).
+combined_ho_type_inst.m:032: In type definition: error: ill-formed type (is)/2.
+combined_ho_type_inst.m:035: Error: syntax error in `:- pred' declaration at
+combined_ho_type_inst.m:035:   bad_sig_p(((pred((int :: in), (int :: out)) is
+combined_ho_type_inst.m:035:   semiet) :: in)).
+combined_ho_type_inst.m:036: Error: syntax error in arguments of `:- func'
+combined_ho_type_inst.m:036:   declaration at bad_sig_f((((func (int :: in)) =
+combined_ho_type_inst.m:036:   (int :: out)) is semidet)).
diff --git a/tests/invalid/combined_ho_type_inst.m b/tests/invalid/combined_ho_type_inst.m
new file mode 100644
index 0000000..39364e9
--- /dev/null
+++ b/tests/invalid/combined_ho_type_inst.m
@@ -0,0 +1,39 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+%
+% Uses combined higher-order types and insts in places where
+% they are not currently permitted.
+%
+%---------------------------------------------------------------------------%
+
+:- module combined_ho_type_inst.
+:- interface.
+
+:- import_module list.
+
+:- type bad_eqv_p == (pred(int::in, int::out) is det).
+:- type bad_eqv_f == (func(int::in) = (int::out) is semidet).
+
+:- type bad_nested_p
+    --->    bad_nested_p(list(pred(int::in, int::out) is det)).
+:- type bad_nested_f
+    --->    bad_nested_p(list(func(int::in) = (int::out) is semidet)).
+
+:- type bad_arg_p
+    --->    bad_arg_p(pred((pred(int::in, int::out) is det))).
+:- type bad_arg_p2
+    --->    bad_arg_p2(pred((pred(int::in, int::out) is det)::in) is semidet).
+:- type bad_arg_f
+    --->    bad_arg_f(func((func(int::in) = (int::out) is semidet)) = int).
+:- type bad_arg_f2
+    --->    bad_arg_f2(
+        func((func(int::in) = (int::out) is semidet)::in)
+            = (int::out) is semidet
+    ).
+
+:- pred bad_sig_p((pred(int::in, int::out) is semiet)::in) is semidet.
+:- func bad_sig_f(func(int::in) = (int::out) is semidet) = int.
+
+:- type avoid_spurious_warning == list(int).
+
diff --git a/tests/invalid/functor_ho_inst_bad.err_exp b/tests/invalid/functor_ho_inst_bad.err_exp
new file mode 100644
index 0000000..baee731
--- /dev/null
+++ b/tests/invalid/functor_ho_inst_bad.err_exp
@@ -0,0 +1,11 @@
+functor_ho_inst_bad.m:039: In clause for `main(di, uo)':
+functor_ho_inst_bad.m:039:   in list element #0:
+functor_ho_inst_bad.m:039:   mode error in unification of `V_7' and
+functor_ho_inst_bad.m:039:   `functor_ho_inst_bad.job(V_8)'.
+functor_ho_inst_bad.m:039:   Variable `V_7' has instantiatedness `free',
+functor_ho_inst_bad.m:039:   term `functor_ho_inst_bad.job(V_8)' has
+functor_ho_inst_bad.m:039:   instantiatedness
+functor_ho_inst_bad.m:039:     named inst functor_ho_inst_bad.job(
+functor_ho_inst_bad.m:039:       /* unique */ (pred(in, di, uo) is det)
+functor_ho_inst_bad.m:039:     ).
+For more information, recompile with `-E'.
diff --git a/tests/invalid/functor_ho_inst_bad.m b/tests/invalid/functor_ho_inst_bad.m
new file mode 100644
index 0000000..b673852
--- /dev/null
+++ b/tests/invalid/functor_ho_inst_bad.m
@@ -0,0 +1,41 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+%
+% Try to use a functor with a higher-order argument with an inst that
+% doesn't match the supplied one.
+%
+
+:- module functor_ho_inst_bad.
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+:- implementation.
+
+:- import_module list.
+
+:- type job
+    --->    job(pred(job_result::out, io::di, io::uo) is det).
+
+:- type job_result
+    --->    job_result_ok
+    ;       job_result_failed.
+
+:- pred run(job::in, io::di, io::uo) is det.
+
+run(Job, !IO) :-
+    Job = job(Pred),
+    Pred(Result, !IO),
+    io.write_line(Result, !IO).
+
+:- pred jbad(job_result::in, io::di, io::uo) is det.
+
+jbad(_, !IO).
+
+main(!IO) :-
+    Jobs = [job(jbad)],
+    list.foldl(run, Jobs, !IO).
+
diff --git a/tests/invalid/functor_ho_inst_bad_2.err_exp b/tests/invalid/functor_ho_inst_bad_2.err_exp
new file mode 100644
index 0000000..19a6a8a
--- /dev/null
+++ b/tests/invalid/functor_ho_inst_bad_2.err_exp
@@ -0,0 +1,7 @@
+functor_ho_inst_bad_2.m:031: In clause for `run(in, di, uo)':
+functor_ho_inst_bad_2.m:031:   in argument 2 (i.e. argument 1 of the called
+functor_ho_inst_bad_2.m:031:   predicate) of higher-order predicate call:
+functor_ho_inst_bad_2.m:031:   mode error: variable `Result' has
+functor_ho_inst_bad_2.m:031:   instantiatedness `free',
+functor_ho_inst_bad_2.m:031:   expected instantiatedness was `ground'.
+For more information, recompile with `-E'.
diff --git a/tests/invalid/functor_ho_inst_bad_2.m b/tests/invalid/functor_ho_inst_bad_2.m
new file mode 100644
index 0000000..7bc63e5
--- /dev/null
+++ b/tests/invalid/functor_ho_inst_bad_2.m
@@ -0,0 +1,41 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+%
+% Try to use a functor with a higher-order argument with an inst that
+% doesn't match the supplied one.
+%
+
+:- module functor_ho_inst_bad_2.
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+:- implementation.
+
+:- import_module list.
+
+:- type job
+    --->    job(pred(job_result::in, io::di, io::uo) is det).
+
+:- type job_result
+    --->    job_result_ok
+    ;       job_result_failed.
+
+:- pred run(job::in, io::di, io::uo) is det.
+
+run(Job, !IO) :-
+    Job = job(Pred),
+    Pred(Result, !IO),
+    io.write_line(Result, !IO).
+
+:- pred jbad(job_result::in, io::di, io::uo) is det.
+
+jbad(_, !IO).
+
+main(!IO) :-
+    Jobs = [job(jbad)],
+    list.foldl(run, Jobs, !IO).
+
diff --git a/tests/invalid/functor_ho_inst_bad_3.err_exp b/tests/invalid/functor_ho_inst_bad_3.err_exp
new file mode 100644
index 0000000..5490c58
--- /dev/null
+++ b/tests/invalid/functor_ho_inst_bad_3.err_exp
@@ -0,0 +1,8 @@
+functor_ho_inst_bad_3.m:038: In clause for `main(di, uo)':
+functor_ho_inst_bad_3.m:038:   mode error in unification of `Job' and
+functor_ho_inst_bad_3.m:038:   `functor_ho_inst_bad_3.job(J)'.
+functor_ho_inst_bad_3.m:038:   Variable `Job' has instantiatedness `free',
+functor_ho_inst_bad_3.m:038:   term `functor_ho_inst_bad_3.job(J)' has
+functor_ho_inst_bad_3.m:038:   instantiatedness
+functor_ho_inst_bad_3.m:038:     named inst functor_ho_inst_bad_3.job(ground).
+For more information, recompile with `-E'.
diff --git a/tests/invalid/functor_ho_inst_bad_3.m b/tests/invalid/functor_ho_inst_bad_3.m
new file mode 100644
index 0000000..db61f7f
--- /dev/null
+++ b/tests/invalid/functor_ho_inst_bad_3.m
@@ -0,0 +1,44 @@
+%---------------------------------------------------------------------------%
+% vim: ts=4 sw=4 et ft=mercury
+%---------------------------------------------------------------------------%
+%
+% Try to use a functor with a higher-order argument with a term that has
+% lost its higher-order inst and become ground.
+%
+
+:- module functor_ho_inst_bad_3.
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+:- implementation.
+
+:- type job
+    ---> job(pred(job_result::out, io::di, io::uo) is det).
+
+:- type job_result
+    --->    job_result_ok
+    ;       job_result_failed.
+
+:- pred run(job::in, io::di, io::uo) is det.
+
+run(Job, !IO) :-
+    Job = job(Pred),
+    Pred(Result, !IO),
+    io.write_line(Result, !IO).
+
+:- pred j1(job_result::out, io::di, io::uo) is det.
+
+j1(job_result_ok, !IO).
+
+main(!IO) :-
+    get(J),
+    Job = job(J),
+    run(Job, !IO).
+
+:- pred get(pred(job_result, io, io)::out) is det.
+
+get(j1).
+
-------------- next part --------------
diff --git a/compiler/unparse.m b/compiler/unparse.m
index b93e71f..64b9b7b 100644
--- a/compiler/unparse.m
+++ b/compiler/unparse.m
@@ -76,9 +76,18 @@ unparse_type(Type, Term) :-
         builtin_type_to_string(BuiltinType, Name),
         Term = term.functor(term.atom(Name), [], Context)
     ;
-        Type = higher_order_type(PorF, PredArgs, _HOInstInfo, Purity,
+        Type = higher_order_type(PorF, PredArgTypes, HOInstInfo, Purity,
             EvalMethod),
-        unparse_type_list(PredArgs, PredArgTerms),
+        unparse_type_list(PredArgTypes, PredArgTypeTerms),
+        (
+            HOInstInfo = higher_order(pred_inst_info(_, PredArgModes, _, _)),
+            unparse_mode_list(PredArgModes, PredArgModeTerms),
+            combine_type_and_mode_terms(PredArgTypeTerms, PredArgModeTerms,
+                PredArgTerms)
+        ;
+            HOInstInfo = none_or_default_func,
+            PredArgTerms = PredArgTypeTerms
+        ),
         (
             PorF = pf_predicate,
             Term0 = term.functor(term.atom("pred"), PredArgTerms, Context),
@@ -90,7 +99,8 @@ unparse_type(Type, Term) :-
             maybe_add_lambda_eval_method(EvalMethod, Term0, Term1),
             Term2 = term.functor(term.atom("="), [Term1, RetTerm], Context)
         ),
-        maybe_add_purity_annotation(Purity, Term2, Term)
+        maybe_add_purity_annotation(Purity, Term2, Term3),
+        maybe_add_detism(HOInstInfo, Term3, Term)
     ;
         Type = tuple_type(Args, _),
         unparse_type_list(Args, ArgTerms),
@@ -122,6 +132,18 @@ unparse_qualified_term(qualified(Qualifier, Name), Args, Term) :-
     Term0 = term.functor(term.atom(Name), Args, Context),
     Term = term.functor(term.atom("."), [QualTerm, Term0], Context).
 
+:- pred combine_type_and_mode_terms(list(term)::in, list(term)::in,
+    list(term)::out) is det.
+
+combine_type_and_mode_terms([], [], []).
+combine_type_and_mode_terms([], [_ | _], _) :-
+    unexpected($module, $pred, "argument length mismatch").
+combine_type_and_mode_terms([_ | _], [], _) :-
+    unexpected($module, $pred, "argument length mismatch").
+combine_type_and_mode_terms([Type | Types], [Mode | Modes], [Term | Terms]) :-
+    Term = term.functor(term.atom("::"), [Type, Mode], term.context_init),
+    combine_type_and_mode_terms(Types, Modes, Terms).
+
 :- pred maybe_add_lambda_eval_method(lambda_eval_method::in, term::in,
     term::out) is det.
 
@@ -137,8 +159,25 @@ maybe_add_purity_annotation(purity_impure, Term0, Term) :-
     Context = term.context_init,
     Term = term.functor(term.atom("impure"), [Term0], Context).
 
+:- pred maybe_add_detism(ho_inst_info::in, term::in, term::out) is det.
+
+maybe_add_detism(none_or_default_func, Term, Term).
+maybe_add_detism(higher_order(pred_inst_info(_, _, _, Detism)), Term0, Term) :-
+    Context = term.context_init,
+    DetismTerm0 = det_to_term(Context, Detism),
+    term.coerce(DetismTerm0, DetismTerm),
+    Term = term.functor(term.atom("is"), [Term0, DetismTerm], Context).
+
 %-----------------------------------------------------------------------------%
 
+:- pred unparse_mode_list(list(mer_mode)::in, list(term)::out) is det.
+
+unparse_mode_list([], []).
+unparse_mode_list([Mode | Modes], [Term | Terms]) :-
+    Term0 = mode_to_term(output_mercury, Mode),
+    term.coerce(Term0, Term),
+    unparse_mode_list(Modes, Terms).
+
 mode_to_term(Lang, Mode) =
     mode_to_term_with_context(Lang, term.context_init, Mode).
 


More information about the reviews mailing list