[m-dev.] subtypes (was Re: [m-rev.] for review: don't allow nondefault mode functions in terms)

Mark Brown mark at mercurylang.org
Wed Dec 9 21:58:26 AEDT 2015


On Thu, Dec 3, 2015 at 3:13 AM, Mark Brown <mark at mercurylang.org> wrote:
> On Mon, Nov 2, 2015 at 2:08 AM, Zoltan Somogyi <zoltan.somogyi at runbox.com> wrote:
>> However, if it was
>> done correctly, it would guarantee that the information cannot
>> get lost. With that system, if you took a higher order value out
>> of a term, its type would tell you its signature, even if the term
>> was (at some intermediate point in time) polymorphic.
>>
>> Unfortunately, this proposal has been a "medium term solution"
>> for way more than a decade now :-(
>
> I posted one solution a couple of years ago, and also proposed an
> alternative. This worked by using the existing
> propagate_ctor_info_lazily code to push the relevant information from
> the types to the mode checker.
>
> If I understand what you're saying about the implementation,

I didn't. (As discussed in person.)

I have started implementing the language feature as follows:

 - A field is added to higher_order_type in mer_type to store any
pred_inst_info.
 - The extra field is ignored during type checking.
 - When mode checking a construction, if there is a pred_inst_info in
the type then the argument must match it (using pred_inst_matches).
 - When mode checking a deconstruction, if there is a pred_inst_info
in the type then propagate it into the argument inst.

The implementation will need to use typed_ground insts to propagate
more deeply nested information, for a list of predicates for example,
but that is not yet done. There's plenty of other holes too - this is
a work-in-progress. The current diff is attached in case anyone is
interested, although it is not ready for review.

The subtypes.m module, also attached, compiles and runs with the above
patch. The mode information in the type is crucial; if the first
argument was changed to 'in', for example, there would be mode errors
at both the place where the jobs are constructed as well as where they
are used.

Any feedback on what I am doing would be welcome.

>
> Regarding correctness, how are construct/3 and dynamic_cast/2 to be
> handled? It would be unsafe for the universal quantifiers in their
> signatures to range over all types, including subtypes, without some
> way of checking that the output values really are in the type in
> question.

The second example illustrates the problem. Construct/3 can in fact be
a problem even for higher order types, if some du type has a higher
order argument that is expected to match a particular mode, because
there is no way to check that the higher-order value inside the univ
matches this mode.

Any ideas on this yet?

Mark
-------------- next part --------------
diff --git a/compiler/check_typeclass.m b/compiler/check_typeclass.m
index 73dad1e..a79ee57 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 7e0353d..abcefb2 100644
--- a/compiler/equiv_type.m
+++ b/compiler/equiv_type.m
@@ -1148,27 +1148,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/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 0d6037e..cb2f142 100644
--- a/compiler/higher_order.m
+++ b/compiler/higher_order.m
@@ -3373,7 +3373,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_data.m b/compiler/hlds_data.m
index d5a53ab..d5d2cb9 100644
--- a/compiler/hlds_data.m
+++ b/compiler/hlds_data.m
@@ -431,6 +431,11 @@ cons_table_optimize(!ConsTable) :-
         in(pred(in, in, out, in, out) is det),
     type_table::in, type_table::out, T::in, T::out) is det.
 
+:- pred map_foldl2_over_type_ctor_defns(
+    pred(type_ctor, hlds_type_defn, hlds_type_defn, T, T, U, U)::
+        in(pred(in, in, out, in, out, in, out) is det),
+    type_table::in, type_table::out, T::in, T::out, U::in, U::out) is det.
+
 %---------------------------------------------------------------------------%
 
     % Have we reported an error for this type definition yet?
@@ -987,6 +992,19 @@ map_foldl_over_type_ctor_defns(Pred, !TypeTable, !Acc) :-
 map_foldl_over_type_ctor_defns_2(Pred, _Name, !TypeCtorTable, !Acc) :-
     map.map_foldl(Pred, !TypeCtorTable, !Acc).
 
+map_foldl2_over_type_ctor_defns(Pred, !TypeTable, !AccA, !AccB) :-
+    map.map_foldl2(map_foldl2_over_type_ctor_defns_2(Pred), !TypeTable,
+        !AccA, !AccB).
+
+:- pred map_foldl2_over_type_ctor_defns_2(
+    pred(type_ctor, hlds_type_defn, hlds_type_defn, T, T, U, U)::
+        in(pred(in, in, out, in, out, in, out) is det),
+    string::in, type_ctor_table::in, type_ctor_table::out,
+    T::in, T::out, U::in, U::out) is det.
+
+map_foldl2_over_type_ctor_defns_2(Pred, _Name, !TypeCtorTable, !AccA, !AccB) :-
+    map.map_foldl2(Pred, !TypeCtorTable, !AccA, !AccB).
+
 %---------------------------------------------------------------------------%
 
 :- type hlds_type_defn
diff --git a/compiler/hlds_rtti.m b/compiler/hlds_rtti.m
index b4f2624..34cfc54 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..fd83ddb 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,98 @@ abstractly_unify_constrained_inst_vars(Live, InstVarsA, SubInstA, InstB,
     ).
 
 %---------------------------------------------------------------------------%
+
+:- import_module io.
+:- 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
+        get_cons_id_non_existential_arg_types(ModuleInfo, Type, ConsId,
+            ArgTypes),
+        % Some builtin types have constructors with arguments that are not
+        % reflected in the constructor definition, and which return an
+        % empty list.
+        %
+        % XXX We shouldn't be applying the substitution anyway, since we
+        % only want to match against subtype information from the
+        % constructor's definition.
+        ArgTypes = [_ | _]
+    then
+        arg_insts_match_ctor_subtypes_2(ArgInsts, ArgTypes, ModuleInfo)
+    else
+        true
+    ).
+
+:- pred arg_insts_match_ctor_subtypes_2(list(mer_inst)::in, list(mer_type)::in,
+    module_info::in) is semidet.
+
+arg_insts_match_ctor_subtypes_2([], [], _).
+arg_insts_match_ctor_subtypes_2([Inst | Insts], [Type | Types], ModuleInfo) :-
+    ( if
+        ( Inst = ground(_, HOInstInfo)
+        ; Inst = any(_, HOInstInfo)
+        ),
+        Type = higher_order_type(_, _, TypeHOInstInfo, _, _),
+        HOInstInfo = higher_order(PredInst),
+        TypeHOInstInfo = higher_order(TypePredInst)
+    then
+        pred_inst_matches(PredInst, TypePredInst, ModuleInfo)
+    else
+        true
+    ),
+    arg_insts_match_ctor_subtypes_2(Insts, Types, 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
+        get_cons_id_non_existential_arg_types(ModuleInfo, Type, ConsId,
+            ArgTypes),
+        % XXX see comment above
+        ArgTypes = [_ | _]
+    then
+        propagate_ctor_subtypes_into_arg_insts_2(ArgTypes, !ArgInsts)
+    else
+        true
+    ).
+
+:- pred propagate_ctor_subtypes_into_arg_insts_2(list(mer_type)::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([Type | Types], [Inst0 | Insts0],
+        [Inst | Insts]) :-
+    ( if
+        Type = higher_order_type(_, _, TypeHOInstInfo, _, _),
+        TypeHOInstInfo = higher_order(_),
+        % XXX should abstractly unify this information
+        (
+            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(Types, 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/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/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 6040bfe..c4d89b2 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/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_data.m b/compiler/prog_data.m
index 8fa5126..fd7d9ee 100644
--- a/compiler/prog_data.m
+++ b/compiler/prog_data.m
@@ -1818,12 +1818,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
             )
@@ -1947,7 +1947,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 4c5ecb2..8bf37b5 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_util.m b/compiler/prog_io_util.m
index c632713..f6edf0a 100644
--- a/compiler/prog_io_util.m
+++ b/compiler/prog_io_util.m
@@ -190,6 +190,7 @@
 :- import_module parse_tree.parse_tree_out_term.
 :- import_module parse_tree.prog_io_sym_name.
 :- import_module parse_tree.prog_out.
+:- import_module parse_tree.prog_type.
 :- import_module parse_tree.prog_util.
 
 :- import_module bool.
@@ -356,8 +357,9 @@ parse_compound_type(Term, VarSet, ContextPieces, CompoundTypeKind, Result) :-
         ( if
             maybe_parse_types(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)
         )
@@ -368,8 +370,18 @@ parse_compound_type(Term, VarSet, ContextPieces, CompoundTypeKind, Result) :-
             maybe_parse_types(FuncArgs, ArgTypes),
             maybe_parse_type(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
+            maybe_parse_ho_type_and_inst(Arg1, Arg2, purity_pure, Type)
+        then
+            Result = ok1(Type)
         else
             Result = ill_formed_type_result(ContextPieces, VarSet, Term)
         )
@@ -383,21 +395,71 @@ parse_compound_type(Term, VarSet, ContextPieces, CompoundTypeKind, Result) :-
                 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))
+                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))
+                construct_higher_order_pred_type(Purity, lambda_normal,
+                    ArgTypes, Type)
+            ;
+                Name = "is",
+                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(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), _)
@@ -414,6 +476,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)).
 
@@ -483,6 +546,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
@@ -579,18 +654,19 @@ unparse_type(Type, Term) :-
         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),
+        Type = higher_order_type(PorF, PredArgs, _HOInstInfo, Purity,
+            EvalMethod),
+        unparse_type_list(PredArgs, PredArgTerms),
         (
-            MaybeRet = yes(Ret),
+            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),
-            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)
     ;
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/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 86315b8..20368d8 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
             )
@@ -1813,17 +1803,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
@@ -2025,23 +2007,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
@@ -2460,15 +2435,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_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/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 66cfc1a..a5118d4 100644
--- a/compiler/write_module_interface_files.m
+++ b/compiler/write_module_interface_files.m
@@ -1021,7 +1021,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(_, _)
         ),
@@ -1354,14 +1354,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 8806537..462151c 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 :-
-------------- next part --------------
A non-text attachment was scrubbed...
Name: subtypes.m
Type: text/x-objcsrc
Size: 666 bytes
Desc: not available
URL: <http://lists.mercurylang.org/archives/developers/attachments/20151209/b1a357de/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: subtypes_problem.m
Type: text/x-objcsrc
Size: 822 bytes
Desc: not available
URL: <http://lists.mercurylang.org/archives/developers/attachments/20151209/b1a357de/attachment-0001.bin>


More information about the developers mailing list