%---------------------------------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et
%---------------------------------------------------------------------------%
% Copyright (C) 1996-2012 The University of Melbourne.
% Copyright (C) 2015-2024 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: modecheck_unify.m.
% Main author: fjh.
%
% This module contains the code to modecheck unifications.
%
% Check that the unification doesn't attempt to unify two free variables
% unless one of them is dead.

% (Also we ought to split unifications up if necessary to avoid complicated
% subunifications.)
%
%---------------------------------------------------------------------------%

:- module check_hlds.modecheck_unify.
:- interface.

:- import_module check_hlds.mode_info.
:- import_module hlds.
:- import_module hlds.hlds_goal.
:- import_module parse_tree.
:- import_module parse_tree.prog_data.

    % Modecheck a unification.
    %
:- pred modecheck_unify(prog_var::in, unify_rhs::in, unification::in,
    unify_context::in, hlds_goal_info::in, hlds_goal_expr::out,
    mode_info::in, mode_info::out) is det.

%---------------------------------------------------------------------------%
%---------------------------------------------------------------------------%

:- implementation.

:- import_module check_hlds.inst_abstract_unify.
:- import_module check_hlds.inst_lookup.
:- import_module check_hlds.inst_match.
:- import_module check_hlds.inst_test.
:- import_module check_hlds.inst_util.
:- import_module check_hlds.mode_debug.
:- import_module check_hlds.mode_errors.
:- import_module check_hlds.mode_test.
:- import_module check_hlds.mode_top_functor.
:- import_module check_hlds.mode_util.
:- import_module check_hlds.modecheck_goal.
:- import_module check_hlds.modecheck_util.
:- import_module check_hlds.modes.
:- import_module check_hlds.polymorphism_lambda.
:- import_module check_hlds.proc_requests.
:- import_module check_hlds.type_util.
:- import_module check_hlds.unique_modes.
:- import_module hlds.const_struct.
:- import_module hlds.goal_util.
:- import_module hlds.hlds_module.
:- import_module hlds.hlds_pred.
:- import_module hlds.instmap.
:- import_module hlds.make_goal.
:- import_module libs.
:- import_module libs.globals.
:- import_module libs.options.
:- import_module mdbcomp.
:- import_module mdbcomp.builtin_modules.
:- import_module mdbcomp.prim_data.
:- import_module mdbcomp.sym_name.
:- import_module parse_tree.builtin_lib_types.
:- import_module parse_tree.maybe_error.
:- import_module parse_tree.prog_mode.
:- import_module parse_tree.prog_type.
:- import_module parse_tree.prog_type_test.
:- import_module parse_tree.set_of_var.
:- import_module parse_tree.var_table.

:- import_module assoc_list.
:- import_module bool.
:- import_module list.
:- import_module map.
:- import_module maybe.
:- import_module one_or_more.
:- import_module pair.
:- import_module require.
:- import_module string.
:- import_module term.
:- import_module varset.

%---------------------------------------------------------------------------%
%---------------------------------------------------------------------------%

modecheck_unify(LHSVar, RHS, Unification0, UnifyContext, UnifyGoalInfo0,
        Goal, !ModeInfo) :-
    % If a unification occurs in a negated context with an inst "any" argument
    % then it has an explicit `impure' annotation.
    %
    % With lambdas, the lambda itself has a higher-order any inst if it
    % includes any inst "any" nonlocals. The value of the lambda expression
    % does not become fixed until all of the nonlocals become fixed.
    % Executing such a lambda may constrain nonlocal solver variables,
    % which in turn constrains the higher-order value itself. Effectively,
    % call/N constrains the predicate value to be "some predicate that is
    % true for the given arguments", and apply/N constrains the function
    % value to be "some function that returns the given value for the given
    % arguments".
    %
    % But we also allow a ground higher-order inst to be used with non-ground
    % locals, provided the type of the higher-order value is impure.
    %
    (
        RHS = rhs_var(RHSVar),
        modecheck_unify_var(LHSVar, RHSVar,
            Unification0, UnifyContext, UnifyGoalInfo0, Goal, !ModeInfo)
    ;
        RHS = rhs_functor(ConsId, IsExistConstr, RHSVars),
        modecheck_unify_functor(LHSVar, ConsId, IsExistConstr, RHSVars,
            Unification0, UnifyContext, UnifyGoalInfo0, Goal, !ModeInfo)
    ;
        RHS = rhs_lambda_goal(Purity, HOGroundness, _PredOrFunc,
            LambdaNonLocals, _ArgVarsModes, _Detism, _LambdaGoal),
        ( if
            Purity \= purity_impure,
            HOGroundness = ho_ground,
            mode_info_get_module_info(!.ModeInfo, ModuleInfo),
            mode_info_get_instmap(!.ModeInfo, InstMap),
            AnyVars = list.filter(var_inst_contains_any(ModuleInfo, InstMap),
                LambdaNonLocals),
            AnyVars = [HeadAnyVar | TailAnyVars]
        then
            set_of_var.init(WaitingVars),
            OoMAnyVars = one_or_more(HeadAnyVar, TailAnyVars),
            mode_info_error(WaitingVars,
                purity_error_lambda_should_be_any(OoMAnyVars), !ModeInfo),
            Goal = conj(plain_conj, [])
        else
            ( if
                goal_info_has_feature(UnifyGoalInfo0,
                    feature_lambda_undetermined_mode)
            then
                modecheck_unify_rhs_undetermined_mode_lambda(LHSVar, RHS,
                    Unification0, UnifyContext, UnifyGoalInfo0, Goal,
                    !ModeInfo)
            else
                modecheck_unify_rhs_lambda(LHSVar, RHS,
                    Unification0, UnifyContext, UnifyGoalInfo0, Goal,
                    !ModeInfo)
            )
        )
    ).

%---------------------------------------------------------------------------%
%---------------------------------------------------------------------------%

:- pred modecheck_unify_var(prog_var::in, prog_var::in, unification::in,
    unify_context::in, hlds_goal_info::in, hlds_goal_expr::out,
    mode_info::in, mode_info::out) is det.

modecheck_unify_var(X, Y, Unification0, UnifyContext,
        UnifyGoalInfo0, UnifyGoalExpr, !ModeInfo) :-
    mode_info_get_module_info(!.ModeInfo, ModuleInfo0),
    mode_info_get_var_table(!.ModeInfo, VarTable),
    mode_info_get_instmap(!.ModeInfo, InstMap),
    instmap_lookup_var(InstMap, X, InstOfX),
    instmap_lookup_var(InstMap, Y, InstOfY),
    mode_info_var_is_live(!.ModeInfo, X, LiveX),
    mode_info_var_is_live(!.ModeInfo, Y, LiveY),
    ( if LiveX = is_live, LiveY = is_live then
        BothLive = is_live
    else
        BothLive = is_dead
    ),
    lookup_var_type(VarTable, X, TypeOfX),
    ( if
        abstractly_unify_inst(TypeOfX, BothLive, real_unify, InstOfX, InstOfY,
            UnifiedInst, Detism, ModuleInfo0, ModuleInfo1),
        % Do not allow free-free unifications if both variables are locked.
        % (Normally the checks for binding locked variables are done in
        % modecheck_set_var_inst, which is called below, but that won't catch
        % this case, because the inst of the variable will remain `free'.
        % XXX are there other cases like this one?)
        not (
            UnifiedInst = free,
            mode_info_var_is_locked(!.ModeInfo, X, _XLockedReason),
            mode_info_var_is_locked(!.ModeInfo, Y, _YLockedReason),
            % a unification of the form `X = X' doesn't bind X,
            % and thus should be allowed even if X is locked
            X \= Y
        )
    then
        mode_info_set_module_info(ModuleInfo1, !ModeInfo),
        modecheck_set_var_inst(X, UnifiedInst, yes(InstOfY), !ModeInfo),
        modecheck_set_var_inst(Y, UnifiedInst, yes(InstOfX), !ModeInfo),
        categorize_unify_var_var(InstOfX, InstOfY, UnifiedInst, LiveX, LiveY,
            X, Y, Detism, UnifyContext, UnifyGoalInfo0, VarTable, Unification0,
            UnifyGoalExpr, !ModeInfo)
    else
        set_of_var.list_to_set([X, Y], WaitingVars),
        % XXX This error should mean that abstractly_unify_inst has failed,
        % but the part of the condition above *after* that call may also fail.
        ModeError = mode_error_unify_var_var(X, Y, InstOfX, InstOfY),
        mode_info_error(WaitingVars, ModeError, !ModeInfo),
        % If we get an error, set the inst to not_reached to suppress
        % follow-on errors. But don't call categorize_unification, because
        % that could cause an invalid call to `unify_proc.request_unify'
        UnifiedInst = not_reached,
        modecheck_set_var_inst(X, UnifiedInst, no, !ModeInfo),
        modecheck_set_var_inst(Y, UnifiedInst, no, !ModeInfo),
        % Return any old garbage.
        Unification = assign(X, Y),
        UnifyMode = unify_modes_li_lf_ri_rf(InstOfX, UnifiedInst,
            InstOfY, UnifiedInst),
        UnifyGoalExpr = unify(X, rhs_var(Y), UnifyMode, Unification,
            UnifyContext)
    ).

    % categorize_unify_var_var works out which category a unification
    % between a variable and another variable expression is - whether it is
    % an assignment, a simple test or a complicated unify.
    %
:- pred categorize_unify_var_var(mer_inst::in, mer_inst::in, mer_inst::in,
    is_live::in, is_live::in, prog_var::in,
    prog_var::in, determinism::in, unify_context::in, hlds_goal_info::in,
    var_table::in, unification::in, hlds_goal_expr::out,
    mode_info::in, mode_info::out) is det.

categorize_unify_var_var(InitInstX, InitInstY, UnifiedInst, LiveX, LiveY, X, Y,
        Detism, UnifyContext, GoalInfo, VarTable, Unification0, Unify,
        !ModeInfo) :-
    mode_info_get_module_info(!.ModeInfo, ModuleInfo0),
    ( if
        init_final_insts_is_output(ModuleInfo0, InitInstX, UnifiedInst)
    then
        Unification = assign(X, Y)
    else if
        init_final_insts_is_output(ModuleInfo0, InitInstY, UnifiedInst)
    then
        Unification = assign(Y, X)
    else if
        init_final_insts_is_unused(ModuleInfo0, InitInstX, UnifiedInst),
        init_final_insts_is_unused(ModuleInfo0, InitInstY, UnifiedInst)
    then
        % For free-free unifications, we pretend for a moment that they are
        % an assignment to the dead variable - they will then be optimized
        % away.
        (
            LiveX = is_dead,
            Unification = assign(X, Y)
        ;
            LiveX = is_live,
            (
                LiveY = is_dead,
                Unification = assign(Y, X)
            ;
                LiveY = is_live,
                unexpected($pred, "free-free unify!")
            )
        )
    else if
        % Check for unreachable unifications.
        ( InitInstX = not_reached
        ; InitInstY = not_reached
        )
    then
        % For these, we can generate any old junk here --
        % we just need to avoid calling modecheck_complicated_unify,
        % since that might abort.
        Unification = simple_test(X, Y)
    else
        lookup_var_type(VarTable, X, Type),
        ( if
            type_is_atomic(ModuleInfo0, Type),
            not type_has_user_defined_equality_pred(ModuleInfo0, Type, _)
        then
            Unification = simple_test(X, Y)
        else if
            % Unification of c_pointers is a runtime error unless introduced by
            % the compiler.
            Type = c_pointer_type,
            goal_info_has_feature(GoalInfo, feature_pretest_equality_condition)
        then
            Unification = simple_test(X, Y)
        else
            modecheck_complicated_unify(X, Y, Type,
                InitInstX, InitInstY, UnifiedInst, Detism, UnifyContext,
                Unification0, Unification, !ModeInfo)
        )
    ),

    % Optimize away unifications with dead variables and simple tests that
    % cannot fail by replacing them with `true'. (The optimization of simple
    % tests is necessary because otherwise determinism analysis assumes they
    % can fail. The optimization of assignments to dead variables may be
    % necessary to stop the code generator from getting confused.)
    %
    % Optimize away unifications which always fail by replacing them with
    % `fail'.
    ( if
        Unification = assign(AssignTarget, AssignSource),
        mode_info_var_is_live(!.ModeInfo, AssignTarget, is_dead)
    then
        Unify = conj(plain_conj, []),
        record_optimize_away(GoalInfo, AssignTarget, AssignSource, !ModeInfo)
    else if
        Unification = simple_test(TestVar1, TestVar2),
        Detism = detism_det
    then
        Unify = conj(plain_conj, []),
        record_optimize_away(GoalInfo, TestVar1, TestVar2, !ModeInfo)
    else if
        Detism = detism_failure
    then
        % This optimisation is safe because the only way that we can analyse
        % a unification as having no solutions is that the unification
        % always fails.
        %
        % As far as the mode checker is concerned, unifying two preds
        % is not erroneous, but a mode *error*.
        Unify = disj([]),
        mode_info_get_module_info(!.ModeInfo, ModuleInfo),
        module_info_get_globals(ModuleInfo, Globals),
        globals.lookup_bool_option(Globals, warn_unification_cannot_succeed,
            WarnCannotSucceed),
        (
            WarnCannotSucceed = yes,
            mode_info_get_pred_id(!.ModeInfo, PredId),
            module_info_pred_info(ModuleInfo, PredId, PredInfo),
            pred_info_get_origin(PredInfo, Origin),
            ReportWarning = should_report_mode_warning_for_pred_origin(Origin),
            (
                ReportWarning = yes,
                Warning = cannot_succeed_var_var(X, Y, InitInstX, InitInstY),
                mode_info_warning(Warning, !ModeInfo)
            ;
                ReportWarning = no
            )
        ;
            WarnCannotSucceed = no
        )
    else
        UnifyModes = unify_modes_li_lf_ri_rf(InitInstX, UnifiedInst,
            InitInstY, UnifiedInst),
        Unify = unify(X, rhs_var(Y), UnifyModes, Unification, UnifyContext)
    ).

    % If we optimize away a singleton variable in a unification in one branch
    % of e.g. a switch, it is possible that the same variable is a singleton
    % in another branch, but cannot be optimized away because it is bound in
    % a call (which cannot be optimized away). In such cases, we must make sure
    % that we call requantification to delete the variable from the nonlocals
    % set of the switch, because otherwise, the arms of the switch would
    % disagree on which nonlocals are bound.
    %
:- pred record_optimize_away(hlds_goal_info::in, prog_var::in, prog_var::in,
    mode_info::in, mode_info::out) is det.

record_optimize_away(GoalInfo, Var1, Var2, !ModeInfo) :-
    NonLocals = goal_info_get_nonlocals(GoalInfo),
    ( if
        set_of_var.member(NonLocals, Var1),
        set_of_var.member(NonLocals, Var2)
    then
        true
    else
        mode_info_need_to_requantify(!ModeInfo)
    ).

    % Modecheck_complicated_unify does some extra checks that are needed
    % for mode-checking complicated unifications.
    %
:- pred modecheck_complicated_unify(prog_var::in, prog_var::in,
    mer_type::in, mer_inst::in, mer_inst::in, mer_inst::in, determinism::in,
    unify_context::in, unification::in, unification::out,
    mode_info::in, mode_info::out) is det.

modecheck_complicated_unify(X, Y, Type, InitInstX, InitInstY, UnifiedInst,
        Detism, UnifyContext, Unification0, Unification, !ModeInfo) :-
    % Build up the unification.
    UnifyMode = unify_modes_li_lf_ri_rf(InitInstX, UnifiedInst,
        InitInstY, UnifiedInst),
    determinism_components(Detism, CanFail, _),
    ( if Unification0 = complicated_unify(_, _, UnifyTypeInfoVars0) then
        UnifyTypeInfoVars = UnifyTypeInfoVars0
    else
        unexpected($pred, "non-complicated unify")
    ),
    Unification = complicated_unify(UnifyMode, CanFail, UnifyTypeInfoVars),

    % Check that all the type_info or type_class_info variables used
    % by the polymorphic unification are ground.
    (
        % Optimize common case.
        UnifyTypeInfoVars = []
    ;
        UnifyTypeInfoVars = [_ | _],
        list.length(UnifyTypeInfoVars, NumTypeInfoVars),
        list.duplicate(NumTypeInfoVars, ground(shared, none_or_default_func),
            ExpectedInsts),
        mode_info_set_call_context(call_context_unify(UnifyContext),
            !ModeInfo),
        ArgOffset = unify_method_event_cast_modecheck_arg_offset,
        modecheck_vars_have_insts_no_exact_match(match_unify, ArgOffset,
            UnifyTypeInfoVars, ExpectedInsts, _InstVarSub, _BadInstVars,
            !ModeInfo),
        % We can ignore _InstVarSub since type_info variables
        % should not have variable insts.
        mode_info_unset_call_context(!ModeInfo)
    ),
    mode_info_get_module_info(!.ModeInfo, ModuleInfo0),
    ( if
        mode_info_get_errors(!.ModeInfo, Errors),
        Errors = [_ | _]
    then
        true
    else if
        % Check that we are not trying to do a polymorphic unification
        % in a mode other than (in, in).
        % [Actually we also allow `any' insts, since the (in, in)
        % mode of unification for types which have `any' insts must
        % also be able to handle (in(any), in(any)) unifications.]
        Type = type_variable(_, _),
        not inst_is_ground_or_any(ModuleInfo0, InitInstX)
    then
        WaitingVars = set_of_var.make_singleton(X),
        ModeError = mode_error_unify_var_poly(X, InitInstX),
        mode_info_error(WaitingVars, ModeError, !ModeInfo)
    else if
        Type = type_variable(_, _),
        not inst_is_ground_or_any(ModuleInfo0, InitInstY)
    then
        WaitingVars = set_of_var.make_singleton(Y),
        ModeError = mode_error_unify_var_poly(Y, InitInstY),
        mode_info_error(WaitingVars, ModeError, !ModeInfo)
    else if
        % Check that we are not trying to do a higher-order unification.
        type_is_higher_order_details(Type, _, PredOrFunc, _)
    then
        % We do not want to report this as an error if it occurs in a
        % compiler-generated predicate. Instead, we delay the error until
        % runtime, so that it only occurs if the compiler-generated predicate
        % gets called. not_reached is considered bound, so the error message
        % would be spurious if the instmap is unreachable.
        mode_info_get_pred_id(!.ModeInfo, PredId),
        module_info_pred_info(ModuleInfo0, PredId, PredInfo),
        mode_info_get_instmap(!.ModeInfo, InstMap0),
        ( if
            ( is_unify_index_or_compare_pred(PredInfo)
            ; instmap_is_unreachable(InstMap0)
            )
        then
            true
        else
            set_of_var.init(WaitingVars),
            ModeError = mode_error_higher_order_unify(X, error_at_var(Y),
                Type, PredOrFunc),
            mode_info_error(WaitingVars, ModeError, !ModeInfo)
        )
    else if
        % Ensure that we will generate code for the unification procedure
        % that will be used to implement this complicated unification.
        type_to_ctor(Type, TypeCtor)
    then
        mode_info_get_context(!.ModeInfo, Context),
        mode_info_get_instvarset(!.ModeInfo, InstVarSet),
        UnifyProcId = unify_proc_id(TypeCtor, UnifyMode),
        request_unify(UnifyProcId, InstVarSet, Detism, Context,
            ModuleInfo0, ModuleInfo),
        mode_info_set_module_info(ModuleInfo, !ModeInfo)
    else
        true
    ).

%---------------------------------------------------------------------------%
%---------------------------------------------------------------------------%

:- pred modecheck_unify_functor(prog_var::in, cons_id::in, is_exist_constr::in,
    list(prog_var)::in, unification::in, unify_context::in,
    hlds_goal_info::in, hlds_goal_expr::out,
    mode_info::in, mode_info::out) is det.

modecheck_unify_functor(X, ConsId, IsExistConstruction, ArgVars0, Unification0,
        UnifyContext, GoalInfo0, GoalExpr, !ModeInfo) :-
    mode_info_get_var_table(!.ModeInfo, VarTable0),
    lookup_var_type(VarTable0, X, TypeOfX),

    ( if
        % We replace any unifications with higher-order pred constants
        % by lambda expressions. For example, we replace
        %
        %       X = list.append(Y)     % Y::in, X::out
        %
        % with
        %
        %       X = lambda [A1::in, A2::out] (list.append(Y, A1, A2))
        %
        % Normally this is done by polymorphism.process_unify_functor,
        % but if we are re-modechecking goals after lambda.m has been run
        % (e.g. for deforestation), then we may need to do it again here.
        % Note that any changes to this code here will probably need to be
        % duplicated there too.

        type_is_higher_order_details(TypeOfX, Purity, _, PredArgTypes),
        ConsId = closure_cons(ShroudedPredProcId)
    then
        % Convert the pred term to a lambda expression.
        mode_info_get_module_info(!.ModeInfo, ModuleInfo0),
        mode_info_get_context(!.ModeInfo, Context),
        proc(PredId, ProcId) = unshroud_pred_proc_id(ShroudedPredProcId),
        convert_pred_to_lambda_goal(ModuleInfo0, Purity, X, PredId, ProcId,
            ArgVars0, PredArgTypes, UnifyContext, GoalInfo0,
            Context, MaybeRHS0, VarTable0, VarTable),
        mode_info_set_var_table(VarTable, !ModeInfo),

        (
            MaybeRHS0 = ok1(RHS0),
            % Modecheck this unification in its new form.
            modecheck_unify(X, RHS0, Unification0, UnifyContext,
                GoalInfo0, GoalExpr, !ModeInfo)
        ;
            MaybeRHS0 = error1(_),
            unexpected($pred,
                "could not convert pred to lambda goal; " ++
                "polymorphism.m should have stopped us getting here")
        )
    else if
        % Right hand sides that represent constant structures need to be
        % handled specially, because the term is inherently shared.
        cons_id_is_const_struct(ConsId, ConstNum)
    then
        expect(unify(IsExistConstruction, is_not_exist_constr), $pred,
            "const struct construction is existential"),
        expect(unify(ArgVars0, []), $pred,
            "const struct construction has args"),
        modecheck_unify_functor_const_struct(X, ConsId, ConstNum, UnifyContext,
            GoalExpr, !ModeInfo)
    else
        % It is not a higher-order pred unification or a unification with a
        % constant structure, so just call modecheck_unify_functor to do
        % the ordinary thing.
        modecheck_unify_functor_std(X, TypeOfX, ConsId, IsExistConstruction,
            ArgVars0, Unification0, UnifyContext, GoalInfo0, GoalExpr,
            !ModeInfo)
    ).

%---------------------%

:- pred modecheck_unify_functor_const_struct(prog_var::in, cons_id::in,
    int::in, unify_context::in, hlds_goal_expr::out,
    mode_info::in, mode_info::out) is det.

modecheck_unify_functor_const_struct(X, ConsId, ConstNum, UnifyContext,
        UnifyGoalExpr, !ModeInfo) :-
    mode_info_get_instmap(!.ModeInfo, InstMap),
    instmap_lookup_var(InstMap, X, InstOfX),
    mode_info_get_module_info(!.ModeInfo, ModuleInfo0),
    module_info_get_const_struct_db(ModuleInfo0, ConstStructDb),
    lookup_const_struct_num(ConstStructDb, ConstNum, ConstStruct),
    ConstStruct = const_struct(_, _, _, InstOfY, _),
    ( if inst_is_free(ModuleInfo0, InstOfX) then
        Inst = InstOfY,
        modecheck_set_var_inst(X, Inst, yes(InstOfY), !ModeInfo),
        Unification = construct(X, ConsId, [], [],
            construct_statically(born_static), cell_is_shared,
            no_construct_sub_info),
        UnifyMode = unify_modes_li_lf_ri_rf(InstOfX, Inst, InstOfY, Inst),
        UnifyGoalExpr = unify(X, rhs_functor(ConsId, is_not_exist_constr, []),
            UnifyMode, Unification, UnifyContext)
%   else if
%       abstractly_unify_inst(LiveX, InstOfX, InstOfY, real_unify,
%           UnifyInst, Det1, ModuleInfo0, ModuleInfo1)
%   then
%       Inst = UnifyInst,
%       Detism = Detism1,
%       mode_info_set_module_info(ModuleInfo1, !ModeInfo),
%       modecheck_set_var_inst(Y, Inst, yes(InstOfX), !ModeInfo),
%       ModeOfX = (InstOfX -> Inst),
%       ModeOfY = (InstOfY -> Inst),
%       categorize_unify_var_const_struct(ModeOfX, ModeOfY, LiveX, X, ConsId,
%           Detism, UnifyContext, UnifyGoalInfo0, VarTable, Unification0,
%           UnifyGoalExpr0, !ModeInfo),
    else
        set_of_var.list_to_set([X], WaitingVars),
        ModeError = mode_error_unify_var_functor(X, ConsId, [], InstOfX, []),
        mode_info_error(WaitingVars, ModeError, !ModeInfo),
        % If we get an error, set the inst to not_reached to suppress
        % follow-on errors. But don't call categorize_unification, because
        % that could cause an invalid call to `unify_proc.request_unify'
        Inst = not_reached,
        modecheck_set_var_inst(X, Inst, no, !ModeInfo),
        % Return any old garbage.
        Unification = construct(X, ConsId, [], [],
            construct_statically(born_static), cell_is_shared,
            no_construct_sub_info),
        UnifyMode = unify_modes_li_lf_ri_rf(InstOfX, Inst, InstOfY, Inst),
        UnifyGoalExpr = unify(X, rhs_functor(ConsId, is_not_exist_constr, []),
            UnifyMode, Unification, UnifyContext)
    ).

%---------------------%

:- pred modecheck_unify_functor_std(prog_var::in, mer_type::in, cons_id::in,
    is_exist_constr::in, list(prog_var)::in, unification::in,
    unify_context::in, hlds_goal_info::in, hlds_goal_expr::out,
    mode_info::in, mode_info::out) is det.

modecheck_unify_functor_std(X0, TypeOfX, ConsId0, IsExistConstruction,
        ArgVars0, Unification0, UnifyContext, GoalInfo0, GoalExpr,
        !ModeInfo) :-
    mode_info_get_instmap(!.ModeInfo, InstMap0),
    ensure_exist_constr_is_construction(IsExistConstruction, X0, X,
        InitInstOfX, LiveX, ExtraGoalsExistConstruct, !ModeInfo),

    % The calls above may have changed the instmap.
    mode_info_get_instmap(!.ModeInfo, InstMap1),
    mode_info_get_how_to_check(!.ModeInfo, HowToCheckGoal),
    mode_info_get_module_info(!.ModeInfo, ModuleInfo0),
    mode_info_get_var_table(!.ModeInfo, VarTable),
    instmap_lookup_vars(InstMap1, ArgVars0, InitInstsOfArgVars),
    mode_info_var_list_is_live(!.ModeInfo, ArgVars0, LiveArgs),
    qualify_cons_id(ArgVars0, ConsId0, ConsId, InstConsId),
    InitInstOfY = bound(unique, inst_test_no_results,
        [bound_functor(InstConsId, InitInstsOfArgVars)]),
    % The occur check: is the unification of the form X = f(..., X, ...)?
    ( if list.member(X, ArgVars0) then
        handle_occur_check_failure(X, TypeOfX, InitInstOfX, ArgVars0,
            InitInstsOfArgVars, InstConsId, GoalExpr, !ModeInfo)
    else if
        % XXX We forbid the construction of partially instantiated
        % structures involving solver types. We would like to forbid all such
        % constructions, but that causes trouble with the current code of
        % term_conversion.term_to_univ_special_case, which does use partial
        % instantiation (in a rather horrible way).
        %
        % This is a hacky solution that gets us most of what we want
        % with respect to solver types.
        not would_construct_partial_term_with_solver_type(ModuleInfo0,
            VarTable, ArgVars0, InitInstOfX, InitInstsOfArgVars),
        abstractly_unify_inst_functor(TypeOfX, LiveX, real_unify, InitInstOfX,
            InstConsId, InitInstsOfArgVars, LiveArgs,
            UnifiedInst, Detism, ModuleInfo0, ModuleInfo1)
    then
        % This is the standard path through this predicate.
        mode_info_set_module_info(ModuleInfo1, !ModeInfo),
        UnifyMode = unify_modes_li_lf_ri_rf(InitInstOfX, UnifiedInst,
            InitInstOfY, UnifiedInst),
        get_mode_of_args(InitInstsOfArgVars, UnifiedInst, ArgFromToInsts),
        inst_expand_and_remove_constrained_inst_vars(ModuleInfo1,
            InitInstOfX, InitInstOfX1),
        list.length(ArgVars0, Arity),
        get_arg_insts_det(InitInstOfX1, InstConsId, Arity, InitInstOfXArgs),
        get_mode_of_args(InitInstOfXArgs, UnifiedInst, ModeOfXArgs),
        categorize_unify_var_functor(InitInstOfX, UnifiedInst, ModeOfXArgs,
            ArgFromToInsts, X, ConsId, ArgVars0, VarTable, UnifyContext,
            Unification0, Unification1, !ModeInfo),
        split_complicated_subunifies(Unification1, Unification,
            ArgVars0, ArgVars, ExtraGoalsSplitSubUnifies, !ModeInfo),
        modecheck_set_var_inst(X, UnifiedInst, yes(InitInstOfY), !ModeInfo),
        bind_args_if_needed(InitInstOfX, UnifiedInst, ArgVars, InitInstOfXArgs,
            !ModeInfo),

        % Construct the final goal expression.
        ( if
            Unification = construct(_, _, _, _, _, _, _),
            LiveX = is_dead
        then
            % Optimize away construction of unused terms by replacing
            % the unification with `true'.
            GoalExpr = conj(plain_conj, [])
        else if
            Detism = detism_failure
        then
            % Optimize away unifications which always fail by replacing
            % them with `fail'.
            GoalExpr = disj([]),
            maybe_generate_cannot_succeed_warning(X, InitInstOfX, ConsId,
                !ModeInfo)
        else
            Functor = rhs_functor(ConsId, IsExistConstruction, ArgVars),
            UnifyExpr = unify(X, Functor, UnifyMode, Unification,
                UnifyContext),

            % Modecheck_unification sometimes needs to introduce new goals
            % to handle complicated sub-unifications in deconstructions.
            % The only time this can happen during unique mode analysis is if
            % the instmap is unreachable, since inst_is_bound succeeds for
            % not_reached. (If it did in other cases, the code would be wrong,
            % since it wouldn't have the correct determinism annotations.)
            append_extra_goals(ExtraGoalsExistConstruct,
                ExtraGoalsSplitSubUnifies, ExtraGoals),
            ( if
                HowToCheckGoal = check_unique_modes,
                ExtraGoals = extra_goals(_, _),
                instmap_is_reachable(InstMap1)
            then
                unexpected($pred,
                    "re-modecheck of unification " ++
                    "encountered complicated sub-unifies")
            else
                true
            ),
            handle_extra_goals(UnifyExpr, ExtraGoals, GoalInfo0,
                [X0 | ArgVars0], [X | ArgVars], InstMap0, GoalExpr, !ModeInfo)
        )
    else
        % Including all ArgVars0 in the waiting_vars is a conservative
        % approximation.
        %
        % XXX This records a mode_error_unify_var_functor error,
        % which is documented to mean that abstractly_unify_inst_functor
        % has failed. However, we can also get here if the code before
        % that call has failed.
        handle_var_functor_mode_error(X, InstConsId, ArgVars0,
            InitInstOfX, InitInstsOfArgVars, [X | ArgVars0], GoalExpr,
            !ModeInfo)
    ).

%---------------------%

    % If a unification was originally of the form X0 = 'new f'(Ys),
    % then it must be classified as a construction. If it were classified
    % as a deconstruction, the argument unifications would be ill-typed.
    %
    % If X0 is already bound, then, to make sure the unification is classified
    % as a construction, we make a new variable X the target of the
    % construction, and unify this new left-hand-side variable with the old,
    % yielding code of the form X = 'new f'(Ys), X0 = X.
    %
:- pred ensure_exist_constr_is_construction(is_exist_constr::in,
    prog_var::in, prog_var::out, mer_inst::out, is_live::out, extra_goals::out,
    mode_info::in, mode_info::out) is det.

ensure_exist_constr_is_construction(IsExistConstruction, X0, X,
        InitInstX, LiveX, ExtraGoals, !ModeInfo) :-
    mode_info_get_instmap(!.ModeInfo, InstMap0),
    instmap_lookup_var(InstMap0, X0, InitInstX0),
    ( if
        IsExistConstruction = is_exist_constr,
        mode_info_get_module_info(!.ModeInfo, ModuleInfo0),
        not inst_is_free(ModuleInfo0, InitInstX0)
    then
        make_complicated_sub_unify(X0, X, ExtraGoals, !ModeInfo),
        InitInstX = free,
        LiveX = is_live
    else
        X = X0,
        InitInstX = InitInstX0,
        mode_info_var_is_live(!.ModeInfo, X, LiveX),
        ExtraGoals = no_extra_goals
    ).

:- pred would_construct_partial_term_with_solver_type(module_info::in,
    var_table::in, list(prog_var)::in,
    mer_inst::in, list(mer_inst)::in) is semidet.

would_construct_partial_term_with_solver_type(ModuleInfo, VarTable, ArgVars,
        InitInstOfX, InitInstsOfArgVars) :-
    inst_is_free(ModuleInfo, InitInstOfX),
    some [InitInstOfArgVar] (
        list.member(InitInstOfArgVar, InitInstsOfArgVars),
        inst_is_free(ModuleInfo, InitInstOfArgVar)
    ),
    some [ArgVar] (
        list.member(ArgVar, ArgVars),
        lookup_var_type(VarTable, ArgVar, ArgType),
        type_is_or_may_contain_solver_type(ModuleInfo, ArgType)
    ).

%---------------------%

    % Categorize_unify_var_functor works out which category a unification
    % between a variable and a functor is - whether it is a construction
    % unification or a deconstruction. It also works out whether it will be
    % deterministic or semideterministic.
    %
:- pred categorize_unify_var_functor(mer_inst::in, mer_inst::in,
    list(from_to_insts)::in, list(from_to_insts)::in,
    prog_var::in, cons_id::in, list(prog_var)::in, var_table::in,
    unify_context::in, unification::in, unification::out,
    mode_info::in, mode_info::out) is det.

categorize_unify_var_functor(InitInstOfX, FinalInstOfX, FromToInstsOfXArgs,
        ArgFromToInsts, X, NewConsId, ArgVars, VarTable, UnifyContext,
        Unification0, Unification, !ModeInfo) :-
    lookup_var_type(VarTable, X, TypeOfX),
    % If we are redoing mode analysis, preserve the existing cons_id.
    (
        Unification0 = construct(_, ConsIdPrime, _, _, _, _, SubInfo0),
        (
            SubInfo0 = construct_sub_info(MaybeTakeAddr, _MaybeSize0),
            expect(unify(MaybeTakeAddr, no), $pred, "take_addr")
        ;
            SubInfo0 = no_construct_sub_info
        ),
        SubInfo = SubInfo0,
        ConsId = ConsIdPrime
    ;
        Unification0 = deconstruct(_, ConsIdPrime, _, _, _, _),
        SubInfo = no_construct_sub_info,
        ConsId = ConsIdPrime
    ;
        ( Unification0 = assign(_, _)
        ; Unification0 = simple_test(_, _)
        ; Unification0 = complicated_unify(_, _, _)
        ),
        SubInfo = no_construct_sub_info,
        ConsId = NewConsId
    ),
    from_to_insts_to_unify_modes(FromToInstsOfXArgs, ArgFromToInsts,
        ArgModes),
    mode_info_get_module_info(!.ModeInfo, ModuleInfo),
    ( if init_final_insts_is_output(ModuleInfo, InitInstOfX, FinalInstOfX) then
        % It is a construction.
        Unification = construct(X, ConsId, ArgVars, ArgModes,
            construct_dynamically, cell_is_unique, SubInfo),
        % For existentially quantified data types, check that any type_info
        % or type_class_info variables in the construction are ground.
        mode_info_set_call_context(call_context_unify(UnifyContext),
            !ModeInfo),
        check_type_info_args_are_ground(ArgVars, VarTable, UnifyContext,
            !ModeInfo),
        mode_info_unset_call_context(!ModeInfo)
    else
        % It is a deconstruction.
        ( if
            % If the variable was already known to be bound to a single
            % particular functor, then the unification either always succeeds
            % or always fails. In the latter case, the final inst will be
            % `not_reached' or `bound([])'. So if both the initial and final
            % inst are `bound([_])', then the unification must be
            % deterministic.
            inst_expand(ModuleInfo, InitInstOfX, ExpandedInitInstOfX),
            ExpandedInitInstOfX = bound(_, _, [_]),
            inst_expand(ModuleInfo, FinalInstOfX, ExpandedFinalInstOfX),
            ExpandedFinalInstOfX = bound(_, _, [_])
        then
            CanFail = cannot_fail
        else if
            % If the type has only one constructor, then the unification
            % cannot fail.
            type_constructors(ModuleInfo, TypeOfX, Constructors),
            Constructors = [_]
        then
            CanFail = cannot_fail
        else
            % Otherwise, it can fail.
            CanFail = can_fail,
            mode_info_get_instmap(!.ModeInfo, InstMap0),
            ( if
                type_is_higher_order_details(TypeOfX, _, PredOrFunc, _),
                instmap_is_reachable(InstMap0)
            then
                set_of_var.init(WaitingVars),
                ModeError = mode_error_higher_order_unify(X,
                    error_at_functor(ConsId, ArgVars), TypeOfX, PredOrFunc),
                mode_info_error(WaitingVars, ModeError, !ModeInfo)
            else
                true
            )
        ),
        Unification = deconstruct(X, ConsId, ArgVars, ArgModes, CanFail,
            cannot_cgc)
    ).

    % Check that any type_info or type_class_info variables
    % in the argument list are ground.
    %
:- pred check_type_info_args_are_ground(list(prog_var)::in,
    var_table::in, unify_context::in, mode_info::in, mode_info::out) is det.

check_type_info_args_are_ground([], _VarTable, _UnifyContext, !ModeInfo).
check_type_info_args_are_ground([ArgVar | ArgVars], VarTable, UnifyContext,
        !ModeInfo) :-
    lookup_var_type(VarTable, ArgVar, ArgType),
    ( if is_introduced_type_info_type(ArgType) then
        mode_info_set_call_arg_context(1, !ModeInfo),
        modecheck_introduced_type_info_var_has_inst_no_exact_match(ArgVar,
            ArgType, ground(shared, none_or_default_func), !ModeInfo),
        check_type_info_args_are_ground(ArgVars, VarTable, UnifyContext,
            !ModeInfo)
    else
        true
    ).

%---------------------%

    % The argument unifications in a construction or deconstruction
    % unification must be simple assignments, they cannot be
    % complicated unifications. If they are, we split them out
    % into separate unifications by introducing fresh variables here.
    %
:- pred split_complicated_subunifies(unification::in, unification::out,
    list(prog_var)::in, list(prog_var)::out, extra_goals::out,
    mode_info::in, mode_info::out) is det.

split_complicated_subunifies(Unification0, Unification, ArgVars0, ArgVars,
        ExtraGoals, !ModeInfo) :-
    ( if
        Unification0 = deconstruct(X, ConsId, ArgVars0, ArgModes0, Det, CanCGC)
    then
        ( if
            split_complicated_subunifies_loop(ArgVars0, ArgModes0,
                ArgVars1, ExtraGoals1, !ModeInfo)
        then
            ExtraGoals = ExtraGoals1,
            ArgVars = ArgVars1,
            Unification = deconstruct(X, ConsId, ArgVars, ArgModes0, Det,
                CanCGC)
        else
            unexpected($pred, "split_complicated_subunifies_loop failed")
        )
    else
        Unification = Unification0,
        ArgVars = ArgVars0,
        ExtraGoals = no_extra_goals
    ).

:- pred split_complicated_subunifies_loop(list(prog_var)::in,
    list(unify_mode)::in, list(prog_var)::out, extra_goals::out,
    mode_info::in, mode_info::out) is semidet.

split_complicated_subunifies_loop([], [], [], no_extra_goals, !ModeInfo).
split_complicated_subunifies_loop([Var0 | Vars0], [ArgMode0 | ArgModes0],
        Vars, ExtraGoals, !ModeInfo) :-
    mode_info_get_module_info(!.ModeInfo, ModuleInfo),
    ArgMode0 = unify_modes_li_lf_ri_rf(InitInstX, FinalInstX,
        InitInstY, FinalInstY),
    mode_info_get_var_table(!.ModeInfo, VarTable0),
    lookup_var_type(VarTable0, Var0, VarType),
    ( if
        init_final_insts_to_top_functor_mode(ModuleInfo, InitInstX, FinalInstX,
            VarType, top_in),
        init_final_insts_to_top_functor_mode(ModuleInfo, InitInstY, FinalInstY,
            VarType, top_in)
    then
        make_complicated_sub_unify(Var0, Var, ExtraGoals0, !ModeInfo),
        % Recursive call to handle the remaining variables...
        split_complicated_subunifies_loop(Vars0, ArgModes0, Vars1,
            ExtraGoals1, !ModeInfo),
        Vars = [Var | Vars1],
        append_extra_goals(ExtraGoals0, ExtraGoals1, ExtraGoals)
    else
        split_complicated_subunifies_loop(Vars0, ArgModes0, Vars1,
            ExtraGoals, !ModeInfo),
        Vars = [Var0 | Vars1]
    ).

:- pred make_complicated_sub_unify(prog_var::in, prog_var::out,
    extra_goals::out, mode_info::in, mode_info::out) is det.

make_complicated_sub_unify(Var0, Var, ExtraGoals0, !ModeInfo) :-
    % Introduce a new variable `Var', which is a clone of Var0.
    mode_info_get_var_table(!.ModeInfo, VarTable0),
    lookup_var_entry(VarTable0, Var0, VarEntry0),
    VarEntry = VarEntry0 ^ vte_name := "",
    add_var_entry(VarEntry, Var, VarTable0, VarTable),
    mode_info_set_var_table(VarTable, !ModeInfo),
    VarType = VarEntry0 ^ vte_type,
    create_var_var_unification(Var0, Var, VarType, !.ModeInfo, ExtraGoal),
    % Insert the new unification at the start of the extra goals.
    ExtraGoals0 = extra_goals([], [ExtraGoal]).

%---------------------%

:- pred handle_occur_check_failure(prog_var::in, mer_type::in, mer_inst::in,
    list(prog_var)::in, list(mer_inst)::in, cons_id::in, hlds_goal_expr::out,
    mode_info::in, mode_info::out) is det.

handle_occur_check_failure(X, TypeOfX, InitInstOfX, ArgVars0,
        InitInstsOfArgVars, InstConsId, GoalExpr, !ModeInfo) :-
    mode_info_get_module_info(!.ModeInfo, ModuleInfo0),
    ( if inst_is_ground(ModuleInfo0, TypeOfX, InitInstOfX) then
        % If X is ground, then we don't consider X = f(..., X, ...)
        % to be a mode error, but it is a unification that can never
        % succeed, and thus it is very unlikely to be what the programmer
        % intended to write.
        %
        % We used to have the code
        %   Warning = cannot_succeed_ground_occur_check(X, ConsId),
        %   mode_info_warning(Warning, !ModeInfo)
        % here. However, it diagnose occur check problems *only*
        % if they took the form X = f(..., X, ...). This is because
        % if the unintended occurrence of X on the right hand side
        % has more than one function symbol above it, as in e.g.
        % X = f(g(X)), then the compiler will transform it into
        % superhomogeneous form as X = f(Y), Y = g(X), and the test
        % list.member(X, ArgVars0) above will succeed for neither
        % of those unifications.
        %
        % That code is now commented out because superhomogeneous.m
        % now has code to a warning for occurs check violations that works
        % regardless of the position of X inside the term that is
        % unified with it.
        modecheck_set_var_inst(X, not_reached, no, !ModeInfo),
        GoalExpr = disj([])
    else
        % If X is not ground, then X = f(..., X, ...) is a mode error.
        handle_var_functor_mode_error(X, InstConsId, ArgVars0,
            InitInstOfX, InitInstsOfArgVars, [X], GoalExpr, !ModeInfo)
    ).

:- pred handle_var_functor_mode_error(prog_var::in, cons_id::in,
    list(prog_var)::in, mer_inst::in, list(mer_inst)::in,
    list(prog_var)::in, hlds_goal_expr::out,
    mode_info::in, mode_info::out) is det.

handle_var_functor_mode_error(X, InstConsId, ArgVars0,
        InstOfX, InstArgs, WaitingVarsList, GoalExpr, !ModeInfo) :-
    set_of_var.list_to_set(WaitingVarsList, WaitingVars),
    ModeError = mode_error_unify_var_functor(X, InstConsId, ArgVars0,
        InstOfX, InstArgs),
    mode_info_error(WaitingVars, ModeError, !ModeInfo),
    % If we get an error, set the inst to not_reached to avoid cascading
    % errors. But don't call categorize_unification, because that could
    % cause an invalid call to `unify_proc.request_unify'.
    Inst = not_reached,
    modecheck_set_var_inst(X, Inst, no, !ModeInfo),
    NoArgInsts = list.duplicate(list.length(ArgVars0), no),
    bind_args(Inst, ArgVars0, NoArgInsts, !ModeInfo),
    % Return any old garbage.
    GoalExpr = disj([]).

    % Warn about unifications that always fail if the user has requested
    % such warnings, and they are reasonably certain not to be misleading.
    %
:- pred maybe_generate_cannot_succeed_warning(prog_var::in, mer_inst::in,
    cons_id::in, mode_info::in, mode_info::out) is det.

maybe_generate_cannot_succeed_warning(X, InstOfX, ConsId, !ModeInfo) :-
    mode_info_get_module_info(!.ModeInfo, ModuleInfo),
    module_info_get_globals(ModuleInfo, Globals),
    globals.lookup_bool_option(Globals, warn_unification_cannot_succeed,
        WarnCannotSucceed),
    (
        WarnCannotSucceed = yes,
        mode_info_get_in_dupl_for_switch(!.ModeInfo, InDuplForSwitch),
        (
            InDuplForSwitch = in_dupl_for_switch
            % Suppress the warning, since the unification may succeed
            % in another copy of this duplicated switch arm.
        ;
            InDuplForSwitch = not_in_dupl_for_switch,
            mode_info_get_pred_id(!.ModeInfo, PredId),
            module_info_pred_info(ModuleInfo, PredId, PredInfo),
            pred_info_get_origin(PredInfo, Origin),
            ReportWarning =
                should_report_mode_warning_for_pred_origin(Origin),
            (
                ReportWarning = yes,
                Warning = cannot_succeed_var_functor(X, InstOfX, ConsId),
                mode_info_warning(Warning, !ModeInfo)
            ;
                ReportWarning = no
            )
        )
    ;
        WarnCannotSucceed = no
    ).

%---------------------%

    % The call to bind_args below serves to update the insts of the
    % argument variables on the right hand side of the unification,
    % putting into them any information we can derive from the original
    % inst of the variable on the left hand side.
    %
    % Unfortunately, the update can be very expensive. For example,
    % for a ground list with N elements, there will be N variables
    % bound to the cons cells of the list. Since the average size of the
    % insts of these variables is proportional to N/2, the task
    % of recording all their insts is at least quadratic in N.
    % In practice, it can actually be worse, because of the way the code
    % called by bind_args works. It keeps track of sets of insts seen
    % so far, and checks new insts for membership of such sets.
    % If the initial elements of a list are repeated, then the membership
    % test can try to unify e.g. [a, a, a, a] with [], [a], [a, a]
    % and [a, a, a]. This means that each step of the quadratic algorithm
    % is itself quadratic, for an overall complexity of O(n^4).
    %
    % It is therefore crucial that we avoid calling bind_args if at all
    % possible.
    %
    % There are two cases in which we definitely know we can avoid
    % calling bind_args. First, if the variable on the left hand side, X,
    % is originally free, then it cannot change the already recorded insts
    % of the variables on the right hand side. Second, in from_ground_term
    % scopes, the variables on the right hand sides of construct
    % unifications are all local to the scope of the from_ground_term
    % scope. We can avoid updating their insts because no part of the
    % compiler will ever want to see their insts.
    %
    % We test for the first case first, because we expect it to be
    % much more common.
    %
:- pred bind_args_if_needed(mer_inst::in, mer_inst::in,
    list(prog_var)::in, list(mer_inst)::in,
    mode_info::in, mode_info::out) is det.

bind_args_if_needed(InstOfX, Inst, ArgVars, InstOfXArgs, !ModeInfo) :-
    mode_info_get_module_info(!.ModeInfo, ModuleInfo),
    ( if inst_is_free(ModuleInfo, InstOfX) then
        true
    else
        mode_info_get_in_from_ground_term(!.ModeInfo, InFromGroundTerm),
        (
            InFromGroundTerm = in_from_ground_term_scope
        ;
            InFromGroundTerm = not_in_from_ground_term_scope,
            UnifyArgInsts = list.map(func(I) = yes(I), InstOfXArgs),
            bind_args(Inst, ArgVars, UnifyArgInsts, !ModeInfo)
        )
    ).

:- pred bind_args(mer_inst::in, list(prog_var)::in, list(maybe(mer_inst))::in,
    mode_info::in, mode_info::out) is det.

bind_args(Inst, Args, UnifyArgInsts, !ModeInfo) :-
    ( if try_bind_args(Inst, Args, UnifyArgInsts, !ModeInfo) then
        true
    else
        unexpected($pred, "try_bind_args failed")
    ).

:- pred try_bind_args(mer_inst::in, list(prog_var)::in,
    list(maybe(mer_inst))::in, mode_info::in, mode_info::out) is semidet.

try_bind_args(Inst, ArgVars, UnifyArgInsts, !ModeInfo) :-
    (
        Inst = not_reached,
        instmap.init_unreachable(InstMap),
        mode_info_set_instmap(InstMap, !ModeInfo)
    ;
        Inst = ground(Uniq, none_or_default_func),
        ground_args(Uniq, ArgVars, UnifyArgInsts, !ModeInfo)
    ;
        Inst = bound(_Uniq, _InstResults, BoundInsts),
        (
            BoundInsts = [],
            % The code is unreachable.
            instmap.init_unreachable(InstMap),
            mode_info_set_instmap(InstMap, !ModeInfo)
        ;
            BoundInsts = [bound_functor(_, ArgInsts)],
            try_bind_arg_list(ArgVars, ArgInsts, UnifyArgInsts, !ModeInfo)
        )
    ;
        Inst = constrained_inst_vars(_, SubInst),
        try_bind_args(SubInst, ArgVars, UnifyArgInsts, !ModeInfo)
    ).

:- pred try_bind_arg_list(list(prog_var)::in, list(mer_inst)::in,
    list(maybe(mer_inst))::in, mode_info::in, mode_info::out) is semidet.

try_bind_arg_list([], [], [], !ModeInfo).
try_bind_arg_list([Arg | Args], [Inst | Insts], [UnifyArgInst | UnifyArgInsts],
        !ModeInfo) :-
    modecheck_set_var_inst(Arg, Inst, UnifyArgInst, !ModeInfo),
    try_bind_arg_list(Args, Insts, UnifyArgInsts, !ModeInfo).

:- pred ground_args(uniqueness::in, list(prog_var)::in,
    list(maybe(mer_inst))::in, mode_info::in, mode_info::out) is semidet.

ground_args(_Uniq, [], [], !ModeInfo).
ground_args(Uniq, [Arg | Args], [UnifyArgInst | UnifyArgInsts], !ModeInfo) :-
    Ground = ground(Uniq, none_or_default_func),
    modecheck_set_var_inst(Arg, Ground, UnifyArgInst, !ModeInfo),
    ground_args(Uniq, Args, UnifyArgInsts, !ModeInfo).

%---------------------%

    % get_mode_of_args(InitialArgInsts, FinalInst, ArgFromToInsts):
    %
    % For a var-functor unification, given the initial insts of the functor
    % arguments and the final inst of the var, compute the modes of the
    % functor arguments.
    %
:- pred get_mode_of_args(list(mer_inst)::in, mer_inst::in,
    list(from_to_insts)::out) is det.

get_mode_of_args(ArgInitInsts, FinalInst, ArgFromToInsts) :-
    ( if
        try_get_mode_of_args(ArgInitInsts, FinalInst, ArgFromToInstsPrime)
    then
        ArgFromToInsts = ArgFromToInstsPrime
    else
        unexpected($pred, "try_get_mode_of_args failed")
    ).

:- pred try_get_mode_of_args(list(mer_inst)::in, mer_inst::in,
    list(from_to_insts)::out) is semidet.

try_get_mode_of_args(ArgInitInsts, FinalInst, ArgFromToInsts) :-
    (
        FinalInst = not_reached,
        pair_with_final_inst(ArgInitInsts, FinalInst, ArgFromToInsts)
    ;
        FinalInst = any(_Uniq, none_or_default_func),
        pair_with_final_inst(ArgInitInsts, FinalInst, ArgFromToInsts)
    ;
        FinalInst = ground(_Uniq, none_or_default_func),
        pair_with_final_inst(ArgInitInsts, FinalInst, ArgFromToInsts)
    ;
        FinalInst = bound(_Uniq, _InstResults, BoundInsts),
        (
            BoundInsts = [],
            % The code is unreachable.
            pair_with_final_inst(ArgInitInsts, not_reached, ArgFromToInsts)
        ;
            BoundInsts = [bound_functor(_Name, FunctorArgInsts)],
            pair_up_insts(ArgInitInsts, FunctorArgInsts, ArgFromToInsts)
        )
    ;
        FinalInst = constrained_inst_vars(_, SubInst),
        try_get_mode_of_args(ArgInitInsts, SubInst, ArgFromToInsts)
    ).

:- pred pair_up_insts(list(mer_inst)::in, list(mer_inst)::in,
    list(from_to_insts)::out) is det.

pair_up_insts([], [], []).
pair_up_insts([], [_ | _], _) :-
    unexpected($pred, "mismatched list lengths").
pair_up_insts([_ | _], [], _) :-
    unexpected($pred, "mismatched list lengths").
pair_up_insts([InstA | InstsA], [InstB | InstsB],
        [FromToInst | FromToInsts]) :-
    FromToInst = from_to_insts(InstA, InstB),
    pair_up_insts(InstsA, InstsB, FromToInsts).

:- pred pair_with_final_inst(list(mer_inst)::in, mer_inst::in,
    list(from_to_insts)::out) is det.

pair_with_final_inst([], _, []).
pair_with_final_inst([InitInst | InitInsts], FinalInst,
        [FromToInst | FromToInsts]) :-
    FromToInst = from_to_insts(InitInst, FinalInst),
    pair_with_final_inst(InitInsts, FinalInst, FromToInsts).

%---------------------------------------------------------------------------%
%---------------------------------------------------------------------------%

:- pred modecheck_unify_rhs_lambda(prog_var::in,
    unify_rhs::in(rhs_lambda_goal), unification::in, unify_context::in,
    hlds_goal_info::in, hlds_goal_expr::out, mode_info::in, mode_info::out)
    is det.

modecheck_unify_rhs_lambda(X, LambdaRHS, Unification0, UnifyContext, _,
        UnifyGoalExpr, !ModeInfo) :-
    LambdaRHS = rhs_lambda_goal(Purity, Groundness, PredOrFunc,
        LambdaNonLocals, VarsModes, Det, Goal0),

    % First modecheck the lambda goal itself:
    %
    % initialize the initial insts of the lambda variables;
    % check that the non-local vars are ground or any;
    % mark the non-local vars as shared;
    % if the higher-order inst is ground lock the non-local vars,
    % otherwise if it is `any' lock the non-local vars that themselves
    % do not match_initial any;
    % mark the non-clobbered lambda variables as live;
    % modecheck the goal;
    % check that the final insts are correct;
    % unmark the live vars;
    % unlock the locked vars;
    % restore the original instmap.
    %
    % XXX or should we merge the original and the final instmaps???
    %
    % The reason that we need to merge the original and final instmaps is
    % as follows. The lambda goal will not have bound any variables (since
    % they were locked), but it may have added some information or lost some
    % uniqueness. We cannot use the final instmap, because that may have
    % too much information. If we use the initial instmap, variables will be
    % considered as unique even if they become shared or clobbered in the
    % lambda goal!
    %
    % However even this may not be enough. If a unique non-local variable
    % is used in its unique inst (e.g. it is used in a ui mode) and then shared
    % within the lambda body, this is unsound. This variable should be marked
    % as shared at the _top_ of the lambda goal. As for implementing this,
    % it probably means that the lambda goal should be re-modechecked,
    % or even modechecked to a fixpoint.
    %
    % For the moment, since doing all that properly seems too hard, we just
    % share all non-local variables at the top of the lambda goal. This is
    % safe, but perhaps too conservative.

    % Initialize the initial insts of the lambda variables.
    mode_info_get_module_info(!.ModeInfo, ModuleInfo0),
    assoc_list.keys_and_values(VarsModes, Vars, Modes),
    mode_list_get_initial_insts(ModuleInfo0, Modes, VarInitialInsts),
    assoc_list.from_corresponding_lists(Vars, VarInitialInsts, VarInstAL),
    VarInstMapDelta = instmap_delta_from_assoc_list(VarInstAL),
    mode_info_get_instmap(!.ModeInfo, InstMap0),
    apply_instmap_delta(VarInstMapDelta, InstMap0, InstMap1),
    mode_info_set_instmap(InstMap1, !ModeInfo),

    % Mark the non-clobbered lambda variables as live.
    get_arg_lives(ModuleInfo0, Modes, ArgLives),
    get_live_vars(Vars, ArgLives, LiveVarsList),
    set_of_var.list_to_set(LiveVarsList, LiveVars),
    mode_info_add_live_vars(LiveVars, !ModeInfo),

    % Lock the non-locals. A ground lambda goal is not allowed to bind any
    % of the non-local variables, since it could get called more than once,
    % or from inside a negation. So in this case we lock all non-locals
    % (not counting the lambda quantified vars).
    %
    % If the lambda goal is inst `any', we don't lock the non-locals which
    % match_initial any, since it is safe to bind these any time that it
    % is safe to bind the lambda goal itself.
    Goal0 = hlds_goal(_, GoalInfo0),
    NonLocals0 = goal_info_get_nonlocals(GoalInfo0),
    set_of_var.delete_list(Vars, NonLocals0, NonLocals1),
    mode_info_get_var_table(!.ModeInfo, VarTable),
    (
        Groundness = ho_ground,
        NonLocals = NonLocals1
    ;
        Groundness = ho_any,
        % XXX Give FilterPred a more descriptive name.
        FilterPred =
            ( pred(NonLocal::in) is semidet :-
                lookup_var_type(VarTable, NonLocal, NonLocalType),
                instmap_lookup_var(InstMap1, NonLocal, NonLocalInst),
                % XXX should filter other higher-order any vars, not just
                % functions with the default mode.
                not inst_matches_initial(ModuleInfo0, NonLocalType,
                    NonLocalInst, any(shared, none_or_default_func))
            ),
        set_of_var.filter(FilterPred, NonLocals1, NonLocals)
    ),
    set_of_var.to_sorted_list(NonLocals, NonLocalsList),
    lookup_var_types(VarTable, NonLocalsList, NonLocalTypes),
    instmap_lookup_vars(InstMap1, NonLocalsList, NonLocalInsts),
    mode_info_get_module_info(!.ModeInfo, ModuleInfo2),
    ( if
        % XXX This test is too conservative.
        %
        % We should allow non-local variables to be non-ground sometimes,
        % possibly dependent on whether or not they are dead after this
        % unification. In addition, we should not "share" a unique non-local
        % variable if these two conditions hold:
        %
        % - It is dead after this unification.
        % - It is not shared within the lambda body.
        %
        % Unfortunately, we can't test the latter condition until after
        % we have mode-checked the lambda body. (See the above comment on
        % merging the initial and final instmaps.)
        ( if
            Groundness = ho_ground,
            Purity \= purity_impure
        then
            inst_list_is_ground(ModuleInfo2, NonLocalTypes, NonLocalInsts)
        else
            inst_list_is_ground_or_any(ModuleInfo2, NonLocalInsts)
        )
    then
        make_shared_inst_list(NonLocalTypes, NonLocalInsts,
            SharedNonLocalInsts, ModuleInfo2, ModuleInfo3),
        instmap_set_vars_corresponding(NonLocalsList, SharedNonLocalInsts,
            InstMap1, InstMap2),
        mode_info_set_module_info(ModuleInfo3, !ModeInfo),
        mode_info_set_instmap(InstMap2, !ModeInfo),

        mode_info_lock_vars(var_lock_lambda(PredOrFunc), NonLocals, !ModeInfo),

        mode_checkpoint(enter, "lambda goal", !ModeInfo),
        mode_info_get_how_to_check(!.ModeInfo, HowToCheckGoal),
        (
            HowToCheckGoal = check_unique_modes,
            unique_modes_check_goal(Goal0, Goal, !ModeInfo)
        ;
            HowToCheckGoal = check_modes,
            modecheck_goal(Goal0, Goal, !ModeInfo)
        ),
        mode_list_get_final_insts(ModuleInfo0, Modes, FinalInsts),
        modecheck_lambda_final_insts(Vars, FinalInsts, !ModeInfo),
        mode_checkpoint(exit, "lambda goal", !ModeInfo),

        mode_info_remove_live_vars(LiveVars, !ModeInfo),
        mode_info_unlock_vars(var_lock_lambda(PredOrFunc), NonLocals,
            !ModeInfo),

        % Ensure that the non-local vars are shared OUTSIDE the
        % lambda unification as well as inside.
        instmap_set_vars_corresponding(NonLocalsList, SharedNonLocalInsts,
            InstMap0, InstMap11),
        mode_info_set_instmap(InstMap11, !ModeInfo),

        % Now modecheck the unification of X with the lambda-expression.
        RHS0 = rhs_lambda_goal(Purity, Groundness, PredOrFunc,
            LambdaNonLocals, VarsModes, Det, Goal),
        modecheck_unify_lambda(X, PredOrFunc, LambdaNonLocals, Modes, Det,
            RHS0, RHS, Unification0, Unification, UnifyMode, !ModeInfo)
    else
        acc_non_ground_vars(ModuleInfo2, VarTable, InstMap1, NonLocalsList,
            [], RevNonGroundVarsInsts),
        list.reverse(RevNonGroundVarsInsts, NonGroundVarsInsts),
        (
            NonGroundVarsInsts = [BadVar - BadInst | _],
            % XXX Why aren't we reporting the rest of NonGroundVarsInsts?
            WaitingVars = set_of_var.make_singleton(BadVar),
            ModeError = mode_error_non_ground_non_local_lambda_var(BadVar,
                BadInst),
            mode_info_error(WaitingVars, ModeError, !ModeInfo)
        ;
            NonGroundVarsInsts = [],
            unexpected($pred, "very strange var")
        ),
        % Return any old garbage.
        RHS = rhs_lambda_goal(Purity, Groundness, PredOrFunc,
            LambdaNonLocals, VarsModes, Det, Goal0),
        UnifyMode = unify_modes_li_lf_ri_rf(free, free, free, free),
        Unification = Unification0
    ),
    UnifyGoalExpr = unify(X, RHS, UnifyMode, Unification, UnifyContext).

:- pred acc_non_ground_vars(module_info::in, var_table::in, instmap::in,
    list(prog_var)::in,
    assoc_list(prog_var, mer_inst)::in,
    assoc_list(prog_var, mer_inst)::out) is det.

acc_non_ground_vars(_, _, _, [], !RevNonGroundVarsInsts).
acc_non_ground_vars(ModuleInfo, VarTable, InstMap, [Var | Vars],
        !RevNonGroundVarsInsts) :-
    lookup_var_type(VarTable, Var, Type),
    instmap_lookup_var(InstMap, Var, Inst),
    ( if inst_is_ground(ModuleInfo, Type, Inst) then
        true
    else
        !:RevNonGroundVarsInsts = [Var - Inst | !.RevNonGroundVarsInsts]
    ),
    acc_non_ground_vars(ModuleInfo, VarTable, InstMap, Vars,
        !RevNonGroundVarsInsts).

:- pred modecheck_unify_lambda(prog_var::in, pred_or_func::in,
    list(prog_var)::in, list(mer_mode)::in, determinism::in,
    unify_rhs::in, unify_rhs::out, unification::in, unification::out,
    unify_mode::out, mode_info::in, mode_info::out) is det.

modecheck_unify_lambda(X, PredOrFunc, ArgVars, LambdaModes, LambdaDetism,
        RHS0, RHS, Unification0, Unification, UnifyMode, !ModeInfo) :-
    mode_info_get_module_info(!.ModeInfo, ModuleInfo0),
    mode_info_get_instmap(!.ModeInfo, InstMap0),
    instmap_lookup_var(InstMap0, X, InstOfX),
    InstOfY = ground(unique, higher_order(LambdaPredInfo)),
    LambdaPredInfo = pred_inst_info(PredOrFunc, LambdaModes,
        arg_reg_types_unset, LambdaDetism),
    mode_info_get_var_table(!.ModeInfo, VarTable),
    lookup_var_type(VarTable, X, TypeOfX),
    ( if
        abstractly_unify_inst(TypeOfX, is_dead, real_unify, InstOfX, InstOfY,
            UnifyInst, _Detism, ModuleInfo0, ModuleInfo1)
    then
        Inst = UnifyInst,
        mode_info_set_module_info(ModuleInfo1, !ModeInfo),
        UnifyMode = unify_modes_li_lf_ri_rf(InstOfX, Inst, InstOfY, Inst),
        % The lambda expression just maps its argument variables
        % from their current insts to the same inst.
        instmap_lookup_vars(InstMap0, ArgVars, ArgInsts),
        categorize_unify_var_lambda(InstOfX, Inst, ArgInsts, X, ArgVars,
            PredOrFunc, RHS0, RHS, Unification0, Unification, !ModeInfo),
        modecheck_set_var_inst(X, Inst, no, !ModeInfo)
    else
        set_of_var.list_to_set([X], WaitingVars),
        ModeError = mode_error_unify_var_lambda(X, InstOfX, InstOfY),
        mode_info_error(WaitingVars, ModeError, !ModeInfo),
        % If we get an error, set the inst to not_reached to avoid cascading
        % errors. But don't call categorize_unification, because that could
        % cause an invalid call to `unify_proc.request_unify'
        Inst = not_reached,
        modecheck_set_var_inst(X, Inst, no, !ModeInfo),
        UnifyMode = unify_modes_li_lf_ri_rf(InstOfX, Inst, InstOfY, Inst),

        % Return any old garbage.
        Unification = Unification0,
        RHS = RHS0
    ).

    % Categorize_unify_var_lambda works out which category a unification
    % between a variable and a lambda expression is - whether it is a
    % construction unification or a deconstruction. It also works out
    % whether it will be det or semidet.
    %
:- pred categorize_unify_var_lambda(mer_inst::in, mer_inst::in,
    list(mer_inst)::in,
    prog_var::in, list(prog_var)::in, pred_or_func::in,
    unify_rhs::in, unify_rhs::out, unification::in, unification::out,
    mode_info::in, mode_info::out) is det.

categorize_unify_var_lambda(InitInstX, FinalInstX, ArgInsts, X, ArgVars,
        PredOrFunc, RHS0, RHS, Unification0, Unification, !ModeInfo) :-
    % If we are re-doing mode analysis, preserve the existing cons_id.
    list.length(ArgVars, Arity),
    (
        Unification0 = construct(_, ConsId, _, _, _, _, SubInfo),
        (
            SubInfo = construct_sub_info(MaybeTakeAddr, _MaybeSize),
            expect(unify(MaybeTakeAddr, no), $pred, "take_addr")
        ;
            SubInfo = no_construct_sub_info
        )
    ;
        Unification0 = deconstruct(_, ConsId, _, _, _, _),
        SubInfo = no_construct_sub_info
    ;
        ( Unification0 = assign(_, _)
        ; Unification0 = simple_test(_, _)
        ; Unification0 = complicated_unify(_, _, _)
        ),
        SubInfo = no_construct_sub_info,
        % The real cons_id will be computed by lambda.m;
        % we just put in a dummy one for now.
        TypeCtor = type_ctor(unqualified("int"), 0),
        DuCtor = du_ctor(unqualified("__LambdaGoal__"), Arity, TypeCtor),
        ConsId = du_data_ctor(DuCtor)
    ),
    ArgFromToInsts = list.map(func(I) = from_to_insts(I, I), ArgInsts),
    from_to_insts_to_unify_modes(ArgFromToInsts, ArgFromToInsts, ArgModes),
    mode_info_get_instmap(!.ModeInfo, InstMap),
    mode_info_get_module_info(!.ModeInfo, ModuleInfo),
    ( if init_final_insts_is_output(ModuleInfo, InitInstX, FinalInstX) then
        ( if
            % If pred_consts are present, lambda expansion has already been
            % done. Rerunning mode analysis should not produce a lambda_goal
            % which cannot be directly converted back into a higher-order
            % predicate constant. If the instmap is not reachable, the call
            % may have been handled as an implied mode, since not_reached
            % is considered to be bound. In this case the lambda_goal may
            % not be converted back to a predicate constant, but that does not
            % matter since the code will be pruned away later by simplify.m.
            ConsId = closure_cons(ShroudedPredProcId),
            instmap_is_reachable(InstMap)
        then
            proc(PredId, ProcId) = unshroud_pred_proc_id(ShroudedPredProcId),
            ( if
                RHS0 = rhs_lambda_goal(_, _, _, _, _, _, Goal),
                Goal = hlds_goal(plain_call(PredId, ProcId, _, _, _, _), _)
            then
                % XXX We used to construct RHS as a rhs_functor whose cons_id
                % is not ConsId, but cons(PredSymName, Arity, RHSTypeCtor).
                % This code was added by Simon Taylor in 1998 in commit
                % d0085d8119780aa922bec7bbbb2f97d8cd6be660, with the message
                % "Avoid aborting on higher-order predicate constants with
                % multiple modes if lambda expansion has already been run."
                %
                % We now keep the original ConsId, since the predicate
                % common_standardize_and_record_construct in common.m
                % relies the cons_ids in rhs and the construct being the same.
                RHS = rhs_functor(ConsId, is_not_exist_constr, ArgVars)
            else
                unexpected($pred, "reintroduced lambda goal")
            )
        else
            RHS = RHS0
        ),
        Unification = construct(X, ConsId, ArgVars, ArgModes,
            construct_dynamically, cell_is_unique, SubInfo)
    else if instmap_is_reachable(InstMap) then
        % If it is a deconstruction, it is a mode error.
        % The error message would be incorrect in unreachable code,
        % since not_reached is considered bound.
        set_of_var.init(WaitingVars),
        mode_info_get_var_table(!.ModeInfo, VarTable0),
        lookup_var_type(VarTable0, X, Type),
        ModeError = mode_error_higher_order_unify(X,
            error_at_lambda(ArgVars, ArgFromToInsts), Type, PredOrFunc),
        mode_info_error(WaitingVars, ModeError, !ModeInfo),
        % Return any old garbage.
        Unification = Unification0,
        RHS = RHS0
    else
        Unification = Unification0,
        RHS = RHS0
    ).

%---------------------------------------------------------------------------%
%---------------------------------------------------------------------------%

:- pred modecheck_unify_rhs_undetermined_mode_lambda(prog_var::in,
    unify_rhs::in(rhs_lambda_goal), unification::in, unify_context::in,
    hlds_goal_info::in, hlds_goal_expr::out, mode_info::in, mode_info::out)
    is det.

modecheck_unify_rhs_undetermined_mode_lambda(X, RHS0, Unification,
        UnifyContext, GoalInfo0, Goal, !ModeInfo) :-
    mode_info_get_module_info(!.ModeInfo, ModuleInfo),
    RHS0 = rhs_lambda_goal(_, _, _, _, _, _, Goal0),
    % Find out the predicate called in the lambda goal.
    ( if
        pred_ids_args_called_from_goal(Goal0, PredIdsArgs0),
        list.negated_filter(is_added_by_polymorphism(ModuleInfo),
            PredIdsArgs0, PredIdsArgs),
        PredIdsArgs = [{PredId, ArgVars}]
    then
        mode_info_get_proc_mode_error_map(!.ModeInfo, ProcModeErrorMap),
        mode_info_get_var_table(!.ModeInfo, VarTable),
        mode_info_get_instmap(!.ModeInfo, InstMap),
        match_modes_by_higher_order_insts(ModuleInfo, ProcModeErrorMap,
            VarTable, InstMap, ArgVars, PredId, MatchResult),
        (
            (
                MatchResult = some_ho_args_not_ground(NonGroundArgVars),
                MultiModeError = no_matching_mode(NonGroundArgVars)
            ;
                MatchResult = possible_modes([]),
                MultiModeError = no_matching_mode(ArgVars)
            ;
                MatchResult = possible_modes([ProcA, ProcB | ProcCs]),
                MultiModeError = more_than_one_matching_mode(ArgVars,
                    ProcA, ProcB, ProcCs)
            ),
            PredMultiModeError =
                pred_id_var_multimode_error(PredId, MultiModeError),
            WaitingVars = set_of_var.make_singleton(X),
            ModeError =
                mode_error_unify_var_multimode_pf(X, PredMultiModeError),
            mode_info_error(WaitingVars, ModeError, !ModeInfo),
            mode_info_get_pred_var_multimode_error_map(!.ModeInfo,
                MultiModeErrorMap0),
            map.set(X, PredMultiModeError,
                MultiModeErrorMap0, MultiModeErrorMap),
            mode_info_set_pred_var_multimode_error_map(MultiModeErrorMap,
                !ModeInfo),
            % Return any old garbage.
            Goal = true_goal_expr
        ;
            MatchResult = possible_modes([ProcId]),
            fix_undetermined_mode_lambda_goal(ModuleInfo, ProcId, RHS0,
                MaybeRHS),
            (
                MaybeRHS = ok1(RHS),
                goal_info_remove_feature(feature_lambda_undetermined_mode,
                    GoalInfo0, GoalInfo),
                % Modecheck this unification in its new form.
                modecheck_unify_rhs_lambda(X, RHS, Unification,
                    UnifyContext, GoalInfo, Goal, !ModeInfo)
            ;
                MaybeRHS = error1(_),
                unexpected($pred, "could not fix up lambda goal; " ++
                    "polymorphism.m should have stopped us getting here")
            )
        )
    else
        unexpected($pred, "expecting single call")
    ).

:- pred is_added_by_polymorphism(module_info::in, {pred_id, T}::in)
    is semidet.

is_added_by_polymorphism(ModuleInfo, {PredId, _}) :-
    module_info_pred_info(ModuleInfo, PredId, PredInfo),
    mercury_private_builtin_module = pred_info_module(PredInfo),
    PredName = pred_info_name(PredInfo),
    ( PredName = "type_info_from_typeclass_info"
    ; PredName = "superclass_from_typeclass_info"
    ).

%---------------------%

:- type match_modes_result
    --->    possible_modes(list(proc_id))
    ;       some_ho_args_not_ground(list(prog_var)).

:- pred match_modes_by_higher_order_insts(module_info::in,
    proc_mode_error_map::in, var_table::in, instmap::in, list(prog_var)::in,
    pred_id::in, match_modes_result::out) is det.

match_modes_by_higher_order_insts(ModuleInfo, ProcModeErrorMap, VarTable,
        InstMap, ArgVars, CalleePredId, Result) :-
    module_info_pred_info(ModuleInfo, CalleePredId, CalleePredInfo),
    ( if map.search(ProcModeErrorMap, CalleePredId, CalleeErrorMapPrime) then
        CalleeErrorMap = CalleeErrorMapPrime
    else
        map.init(CalleeErrorMap)
    ),
    CalleeProcIds = pred_info_all_procids(CalleePredInfo),
    match_modes_by_higher_order_insts_loop(ModuleInfo, VarTable, InstMap,
        ArgVars, CalleePredInfo, CalleeErrorMap, CalleeProcIds,
        [], [], Result).

:- pred match_modes_by_higher_order_insts_loop(module_info::in,
    var_table::in, instmap::in, list(prog_var)::in,
    pred_info::in, map(proc_id, list(mode_error_info))::in, list(proc_id)::in,
    list(proc_id)::in, list(prog_var)::in, match_modes_result::out) is det.

match_modes_by_higher_order_insts_loop(_, _, _, _, _, _, [],
        !.RevMatchedProcIds, !.NonGroundNonLocals, Result) :-
    (
        !.NonGroundNonLocals = [],
        Result = possible_modes(list.reverse(!.RevMatchedProcIds))
    ;
        !.NonGroundNonLocals = [_ | _],
        !:NonGroundNonLocals = list.sort_and_remove_dups(!.NonGroundNonLocals),
        Result = some_ho_args_not_ground(!.NonGroundNonLocals)
    ).
match_modes_by_higher_order_insts_loop(ModuleInfo, VarTable, InstMap,
        ArgVars, CalleePredInfo, CalleeErrorMap, [ProcId | ProcIds],
        !.RevMatchedProcIds, !.NonGroundNonLocals, Result) :-
    ( if
        map.search(CalleeErrorMap, ProcId, CalleeModeErrors),
        CalleeModeErrors = [_ | _]
    then
        % This mode of the callee is not valid.
        true
    else
        pred_info_proc_info(CalleePredInfo, ProcId, CalleeProcInfo),
        proc_info_get_argmodes(CalleeProcInfo, ArgModes),
        match_mode_by_higher_order_insts(ModuleInfo, VarTable, InstMap,
            ArgVars, ArgModes, ProcNonGroundNonLocals, ProcResult),
        !:NonGroundNonLocals = ProcNonGroundNonLocals ++ !.NonGroundNonLocals,
        (
            ProcResult = ho_insts_match,
            !:RevMatchedProcIds = [ProcId | !.RevMatchedProcIds]
        ;
            ProcResult = ho_insts_do_not_match
        )
    ),
    match_modes_by_higher_order_insts_loop(ModuleInfo, VarTable, InstMap,
        ArgVars, CalleePredInfo, CalleeErrorMap, ProcIds,
        !.RevMatchedProcIds, !.NonGroundNonLocals, Result).

:- type match_mode_result
    --->    ho_insts_match
    ;       ho_insts_do_not_match.

:- pred match_mode_by_higher_order_insts(module_info::in,
    var_table::in, instmap::in, list(prog_var)::in, list(mer_mode)::in,
    list(prog_var)::out, match_mode_result::out) is det.

match_mode_by_higher_order_insts(_ModuleInfo, _VarTable, _InstMap,
        [], _, [], ho_insts_match).
match_mode_by_higher_order_insts(ModuleInfo, VarTable, InstMap,
        [ArgVar | ArgVars], ArgModesList, NonGroundArgVars, Result) :-
    (
        ArgModesList = [ArgMode | ArgModes]
    ;
        ArgModesList = [],
        unexpected($pred, "too many arguments")
    ),
    match_mode_by_higher_order_insts(ModuleInfo, VarTable, InstMap,
        ArgVars, ArgModes, TailNonGroundArgVars, TailResult),

    % For arguments with higher order initial insts, check if the variable in
    % that position has a matching inst. If the variable is free, then we need
    % to delay the goal.
    Initial = mode_get_initial_inst(ModuleInfo, ArgMode),
    ( if Initial = ground(_, higher_order(_)) then
        instmap_lookup_var(InstMap, ArgVar, ArgInst),
        lookup_var_type(VarTable, ArgVar, ArgType),
        ( if inst_matches_initial(ModuleInfo, ArgType, ArgInst, Initial) then
            NonGroundArgVars = TailNonGroundArgVars,
            Result = TailResult
        else
            ( if inst_is_ground(ModuleInfo, ArgType, ArgInst) then
                NonGroundArgVars = TailNonGroundArgVars
            else
                NonGroundArgVars = [ArgVar | TailNonGroundArgVars]
            ),
            Result = ho_insts_do_not_match
        )
    else
        NonGroundArgVars = TailNonGroundArgVars,
        Result = TailResult
    ).

%---------------------------------------------------------------------------%
:- end_module check_hlds.modecheck_unify.
%---------------------------------------------------------------------------%
