[m-rev.] for review: improve checking of `any' in negated context

[David Overton]

Estimated hours taken: 5
Branches: main

Allow more precise (i.e. less conservative) mode checking in the case that an
`any' inst occurs in a negated context.  Normally we must disallow this
because we do not know whether the inst has become more instantiated over the
negated goal.  However, if the inst has simply been unified with `free' then
we know that it cannot have become more instantiated.  This change checks
for, and allows, that case.

This situation occurs quite frequently in code generated by the HAL compiler.

compiler/inst_match.m:
	Add a new inst comparison predicate
	`inst_is_at_least_as_instantiated' which is the same as
	`inst_matches_initial' except that it reverses the uniqueness
	comparison.

compiler/modecheck_unify.m:
	When mode checking a unification, in the call to
	`modecheck_set_var_inst' pass the initial inst of the other side of
	the unification.

compiler/modes.m:
	Modify `modecheck_set_var_inst' so that in the case that the inst to
	be set is the final inst in a unification goal and the initial inst
	of the other side of the unification is available then it can make
	use of that information to improve the precision of the analysis.

tests/hard_coded/Mmakefile:
tests/hard_coded/any_free_unify.exp:
tests/hard_coded/any_free_unify.m:
	Add a test case.

Index: compiler/inst_match.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/inst_match.m,v
retrieving revision 1.52
diff -u -r1.52 inst_match.m
--- compiler/inst_match.m	15 Mar 2003 03:08:53 -0000	1.52
+++ compiler/inst_match.m	28 May 2003 01:04:17 -0000
@@ -123,6 +123,18 @@
 	% inst_matches_final into a single predicate inst_matches(When, ...)
 	% where When is either `initial' or `final'.
 
+	% inst_is_at_least_as_instantiated(InstA, InstB, Type, ModuleInfo)
+	% 	succeeds iff InstA is at least as instantiated as InstB.  This
+	% 	defines a partial order which is the same as
+	% 	inst_matches_initial except that uniqueness comparisons are
+	% 	reversed.  This gives us the partial order of which
+	% 	abstractly_unify_inst(dead, ...) is the greatest lower bound.
+	% 	It describes the allowable changes in the inst of a variable
+	% 	over the forward execution of a goal.
+
+:- pred inst_is_at_least_as_instantiated(inst, inst, type, module_info).
+:- mode inst_is_at_least_as_instantiated(in, in, in, in) is semidet.
+
 :- pred unique_matches_initial(uniqueness, uniqueness).
 :- mode unique_matches_initial(in, in) is semidet.
 
@@ -323,11 +335,16 @@
 
 :- type expansions == set(pair(inst)).
 
+:- type uniqueness_comparison
+	--->	match
+	;	instantiated.
+
 :- type inst_match_info
 	--->	inst_match_info(
 			module_info	:: module_info,
 			expansions	:: expansions,
-			maybe_sub	:: maybe(inst_var_sub)
+			maybe_sub	:: maybe(inst_var_sub),
+			uniqueness_comparison	:: uniqueness_comparison
 		).
 
 :- func sub(inst_match_info) = inst_var_sub is semidet.
@@ -342,7 +359,8 @@
 
 :- func init_inst_match_info(module_info) = inst_match_info.
 
-init_inst_match_info(ModuleInfo) = inst_match_info(ModuleInfo, Exp, no) :-
+init_inst_match_info(ModuleInfo) = inst_match_info(ModuleInfo, Exp, no, match)
+		:-
 	set__init(Exp).
 
 :- pred inst_matches_initial_2(inst, inst, maybe(type), 
@@ -400,23 +418,25 @@
 	% occur in `Expansions'.
 
 inst_matches_initial_4(any(UniqA), any(UniqB), _, I, I) :-
-	unique_matches_initial(UniqA, UniqB).
+	compare_uniqueness(I ^ uniqueness_comparison, UniqA, UniqB).
 inst_matches_initial_4(any(_), free, _, I, I).
 inst_matches_initial_4(free, any(_), _, I, I).
 inst_matches_initial_4(free, free, _, I, I).
 inst_matches_initial_4(bound(UniqA, ListA), any(UniqB), _, Info, Info) :-
-	unique_matches_initial(UniqA, UniqB),
-	bound_inst_list_matches_uniq(ListA, UniqB, Info^module_info).
+	compare_uniqueness(Info ^ uniqueness_comparison, UniqA, UniqB),
+	compare_bound_inst_list_uniq(Info ^ uniqueness_comparison,
+		ListA, UniqB, Info^module_info).
 inst_matches_initial_4(bound(_Uniq, _List), free, _, I, I).
 inst_matches_initial_4(bound(UniqA, ListA), bound(UniqB, ListB), Type,
 		Info0, Info) :-
-	unique_matches_initial(UniqA, UniqB),
+	compare_uniqueness(Info0 ^ uniqueness_comparison, UniqA, UniqB),
 	bound_inst_list_matches_initial(ListA, ListB, Type, Info0, Info).
 inst_matches_initial_4(bound(UniqA, ListA), ground(UniqB, none), _,
 		Info, Info) :-
-	unique_matches_initial(UniqA, UniqB),
+	compare_uniqueness(Info ^ uniqueness_comparison, UniqA, UniqB),
 	bound_inst_list_is_ground(ListA, Info^module_info),
-	bound_inst_list_matches_uniq(ListA, UniqB, Info^module_info).
+	compare_bound_inst_list_uniq(Info ^ uniqueness_comparison,
+		ListA, UniqB, Info^module_info).
 inst_matches_initial_4(bound(Uniq, List), abstract_inst(_,_), _, Info, Info) :-
 	Uniq = unique,
 	bound_inst_list_is_ground(List, Info^module_info),
@@ -429,20 +449,20 @@
 		Info, Info) :-
 	\+ ground_inst_info_is_nonstandard_func_mode(GroundInstInfoA,
 		Info^module_info),
-	unique_matches_initial(UniqA, UniqB).
+	compare_uniqueness(Info ^ uniqueness_comparison, UniqA, UniqB).
 inst_matches_initial_4(ground(_Uniq, _PredInst), free, _, I, I).
 inst_matches_initial_4(ground(UniqA, _GII_A), bound(UniqB, ListB), MaybeType,
 		Info0, Info) :-
 	MaybeType = yes(Type),
 		% We can only check this case properly if the type is known.
-	unique_matches_initial(UniqA, UniqB),
+	compare_uniqueness(Info0 ^ uniqueness_comparison, UniqA, UniqB),
 	bound_inst_list_is_complete_for_type(set__init, Info0^module_info,
 		ListB, Type),
 	ground_matches_initial_bound_inst_list(UniqA, ListB, yes(Type),
 		Info0, Info).
 inst_matches_initial_4(ground(UniqA, GroundInstInfoA),
 		ground(UniqB, GroundInstInfoB), Type, Info0, Info) :-
-	unique_matches_initial(UniqA, UniqB),
+	compare_uniqueness(Info0 ^ uniqueness_comparison, UniqA, UniqB),
 	ground_inst_info_matches_initial(GroundInstInfoA, GroundInstInfoB,
 		UniqB, Type, Info0, Info).
 inst_matches_initial_4(ground(_UniqA, none), abstract_inst(_,_),_,_,_) :-
@@ -701,6 +721,22 @@
 
 %-----------------------------------------------------------------------------%
 
+	% Determine what kind of uniqueness comparison we are doing and then do
+	% it.
+	% If we are doing a "match" then call unique_matches_initial to do the
+	% comparison.
+	% If we are comparing "instantiatedness" then the uniqueness comparison
+	% is the reverse of when we are doing a match so call
+	% unique_matches_initial with the arguments reversed.
+
+:- pred compare_uniqueness(uniqueness_comparison, uniqueness, uniqueness).
+:- mode compare_uniqueness(in, in, in) is semidet.
+
+compare_uniqueness(match, InstA, InstB) :-
+	unique_matches_initial(InstA, InstB).
+compare_uniqueness(instantiated, InstA, InstB) :-
+	unique_matches_initial(InstB, InstA).
+
 unique_matches_initial(unique, _).
 unique_matches_initial(mostly_unique, mostly_unique).
 unique_matches_initial(mostly_unique, shared).
@@ -718,6 +754,15 @@
 
 %-----------------------------------------------------------------------------%
 
+:- pred compare_bound_inst_list_uniq(uniqueness_comparison, list(bound_inst),
+		uniqueness, module_info).
+:- mode compare_bound_inst_list_uniq(in, in, in, in) is semidet.
+
+compare_bound_inst_list_uniq(match, List, Uniq, ModuleInfo) :-
+	bound_inst_list_matches_uniq(List, Uniq, ModuleInfo).
+compare_bound_inst_list_uniq(instantiated, List, Uniq, ModuleInfo) :-
+	uniq_matches_bound_inst_list(Uniq, List, ModuleInfo).
+
 :- pred bound_inst_list_matches_uniq(list(bound_inst), uniqueness,
 					module_info).
 :- mode bound_inst_list_matches_uniq(in, in, in) is semidet.
@@ -970,6 +1015,11 @@
 			% check that [X|Xs] matches_final Ys.
 		bound_inst_list_matches_final([X|Xs], Ys, MaybeType)
 	).
+
+inst_is_at_least_as_instantiated(InstA, InstB, Type, ModuleInfo) :-
+	Info = init_inst_match_info(ModuleInfo) ^ 
+			uniqueness_comparison := instantiated,
+	inst_matches_initial_2(InstA, InstB, yes(Type), Info, _).
 
 inst_matches_binding(InstA, InstB, Type, ModuleInfo) :-
 	Info0 = init_inst_match_info(ModuleInfo),
Index: compiler/modecheck_unify.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modecheck_unify.m,v
retrieving revision 1.57
diff -u -r1.57 modecheck_unify.m
--- compiler/modecheck_unify.m	13 May 2003 23:56:17 -0000	1.57
+++ compiler/modecheck_unify.m	28 May 2003 01:04:17 -0000
@@ -93,8 +93,10 @@
 		Inst = UnifyInst,
 		Det = Det1,
 		mode_info_set_module_info(ModeInfo0, ModuleInfo1, ModeInfo1),
-		modecheck_set_var_inst(X, Inst, ModeInfo1, ModeInfo2),
-		modecheck_set_var_inst(Y, Inst, ModeInfo2, ModeInfo3),
+		modecheck_set_var_inst(X, Inst, yes(InstOfY),
+			ModeInfo1, ModeInfo2),
+		modecheck_set_var_inst(Y, Inst, yes(InstOfX),
+			ModeInfo2, ModeInfo3),
 		ModeOfX = (InstOfX -> Inst),
 		ModeOfY = (InstOfY -> Inst),
 		mode_info_get_var_types(ModeInfo3, VarTypes),
@@ -111,8 +113,8 @@
 			% that could cause an invalid call to
 			% `unify_proc__request_unify'
 		Inst = not_reached,
-		modecheck_set_var_inst(X, Inst, ModeInfo1, ModeInfo2),
-		modecheck_set_var_inst(Y, Inst, ModeInfo2, ModeInfo),
+		modecheck_set_var_inst(X, Inst, no, ModeInfo1, ModeInfo2),
+		modecheck_set_var_inst(Y, Inst, no, ModeInfo2, ModeInfo),
 			% return any old garbage
 		Unification = assign(X, Y),
 		ModeOfX = (InstOfX -> Inst),
@@ -386,7 +388,7 @@
 				X, ArgVars, PredOrFunc,
 				RHS0, Unification0, ModeInfo1,
 				RHS, Unification, ModeInfo2),
-		modecheck_set_var_inst(X, Inst, ModeInfo2, ModeInfo)
+		modecheck_set_var_inst(X, Inst, no, ModeInfo2, ModeInfo)
 	;
 		set__list_to_set([X], WaitingVars),
 		mode_info_error(WaitingVars,
@@ -399,7 +401,7 @@
 			% that could cause an invalid call to
 			% `unify_proc__request_unify'
 		Inst = not_reached,
-		modecheck_set_var_inst(X, Inst, ModeInfo1, ModeInfo),
+		modecheck_set_var_inst(X, Inst, no, ModeInfo1, ModeInfo),
 		ModeOfX = (InstOfX -> Inst),
 		ModeOfY = (InstOfY -> Inst),
 		Mode = ModeOfX - ModeOfY,
@@ -514,8 +516,10 @@
 		ModeOfX = (InstOfX -> Inst),
 		ModeOfY = (InstOfY -> Inst),
 		Mode = ModeOfX - ModeOfY,
-		modecheck_set_var_inst(X, Inst, ModeInfo2, ModeInfo3),
-		( bind_args(Inst, ArgVars0, ModeInfo3, ModeInfo4) ->
+		modecheck_set_var_inst(X, Inst, no,
+			ModeInfo2, ModeInfo3),
+		NoArgInsts = list__duplicate(length(ArgVars0), no),
+		( bind_args(Inst, ArgVars0, NoArgInsts, ModeInfo3, ModeInfo4) ->
 			ModeInfo = ModeInfo4
 		;
 			error("bind_args failed")
@@ -544,10 +548,12 @@
 			inst_expand_and_remove_constrained_inst_vars(
 				ModuleInfo1, InstOfX, InstOfX1),
 			list__length(ArgVars0, Arity),
-			get_arg_insts(InstOfX1, InstConsId, Arity, InstOfXArgs),
-			get_mode_of_args(Inst, InstOfXArgs, ModeOfXArgs0)
+			get_arg_insts(InstOfX1, InstConsId, Arity,
+				InstOfXArgs0),
+			get_mode_of_args(Inst, InstOfXArgs0, ModeOfXArgs0)
 		->
-			ModeOfXArgs = ModeOfXArgs0
+			ModeOfXArgs = ModeOfXArgs0,
+			InstOfXArgs = InstOfXArgs0
 		;
 			error("get_(inst/mode)_of_args failed")
 		),
@@ -559,8 +565,13 @@
 		split_complicated_subunifies(Unification1, ArgVars0,
 				Unification, ArgVars, ExtraGoals1,
 				ModeInfo3, ModeInfo4),
-		modecheck_set_var_inst(X, Inst, ModeInfo4, ModeInfo5),
-		( bind_args(Inst, ArgVars, ModeInfo5, ModeInfo6) ->
+		modecheck_set_var_inst(X, Inst, yes(InstOfY),
+			ModeInfo4, ModeInfo5),
+		UnifyArgInsts = list__map(func(I) = yes(I), InstOfXArgs),
+		(
+			bind_args(Inst, ArgVars, UnifyArgInsts,
+				ModeInfo5, ModeInfo6)
+		->
 			ModeInfo = ModeInfo6
 		;
 			error("bind_args failed")
@@ -582,8 +593,9 @@
 		ModeOfX = (InstOfX -> Inst),
 		ModeOfY = (InstOfY -> Inst),
 		Mode = ModeOfX - ModeOfY,
-		modecheck_set_var_inst(X, Inst, ModeInfo2, ModeInfo3),
-		( bind_args(Inst, ArgVars0, ModeInfo3, ModeInfo4) ->
+		modecheck_set_var_inst(X, Inst, no, ModeInfo2, ModeInfo3),
+		NoArgInsts = list__duplicate(length(ArgVars0), no),
+		( bind_args(Inst, ArgVars0, NoArgInsts, ModeInfo3, ModeInfo4) ->
 			ModeInfo = ModeInfo4
 		;
 			error("bind_args failed")
@@ -1235,41 +1247,44 @@
 
 %-----------------------------------------------------------------------------%
 
-:- pred bind_args(inst, list(prog_var), mode_info, mode_info).
-:- mode bind_args(in, in, mode_info_di, mode_info_uo) is semidet.
+:- pred bind_args(inst, list(prog_var), list(maybe(inst)),
+		mode_info, mode_info).
+:- mode bind_args(in, in, in, mode_info_di, mode_info_uo) is semidet.
 
-bind_args(not_reached, _) -->
+bind_args(not_reached, _, _) -->
 	{ instmap__init_unreachable(InstMap) },
 	mode_info_set_instmap(InstMap).
-bind_args(ground(Uniq, none), Args) -->
-	ground_args(Uniq, Args).
-bind_args(bound(_Uniq, List), Args) -->
+bind_args(ground(Uniq, none), Args, UnifyArgInsts) -->
+	ground_args(Uniq, Args, UnifyArgInsts).
+bind_args(bound(_Uniq, List), Args, UnifyArgInsts) -->
 	( { List = [] } ->
 		% the code is unreachable
 		{ instmap__init_unreachable(InstMap) },
 		mode_info_set_instmap(InstMap)
 	;
 		{ List = [functor(_, InstList)] },
-		bind_args_2(Args, InstList)
+		bind_args_2(Args, InstList, UnifyArgInsts)
 	).
-bind_args(constrained_inst_vars(_, Inst), Args) -->
-	bind_args(Inst, Args).
+bind_args(constrained_inst_vars(_, Inst), Args, UnifyArgInsts) -->
+	bind_args(Inst, Args, UnifyArgInsts).
 
-:- pred bind_args_2(list(prog_var), list(inst), mode_info, mode_info).
-:- mode bind_args_2(in, in, mode_info_di, mode_info_uo) is semidet.
+:- pred bind_args_2(list(prog_var), list(inst), list(maybe(inst)),
+		mode_info, mode_info).
+:- mode bind_args_2(in, in, in, mode_info_di, mode_info_uo) is semidet.
+
+bind_args_2([], [], []) --> [].
+bind_args_2([Arg | Args], [Inst | Insts], [UnifyArgInst | UnifyArgInsts]) -->
+	modecheck_set_var_inst(Arg, Inst, UnifyArgInst),
+	bind_args_2(Args, Insts, UnifyArgInsts).
+
+:- pred ground_args(uniqueness, list(prog_var), list(maybe(inst)),
+		mode_info, mode_info).
+:- mode ground_args(in, in, in, mode_info_di, mode_info_uo) is semidet.
 
-bind_args_2([], []) --> [].
-bind_args_2([Arg | Args], [Inst | Insts]) -->
-	modecheck_set_var_inst(Arg, Inst),
-	bind_args_2(Args, Insts).
-
-:- pred ground_args(uniqueness, list(prog_var), mode_info, mode_info).
-:- mode ground_args(in, in, mode_info_di, mode_info_uo) is det.
-
-ground_args(_Uniq, []) --> [].
-ground_args(Uniq, [Arg | Args]) -->
-	modecheck_set_var_inst(Arg, ground(Uniq, none)),
-	ground_args(Uniq, Args).
+ground_args(_Uniq, [], []) --> [].
+ground_args(Uniq, [Arg | Args], [UnifyArgInst | UnifyArgInsts]) -->
+	modecheck_set_var_inst(Arg, ground(Uniq, none), UnifyArgInst),
+	ground_args(Uniq, Args, UnifyArgInsts).
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/modes.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modes.m,v
retrieving revision 1.268
diff -u -r1.268 modes.m
--- compiler/modes.m	26 May 2003 09:00:02 -0000	1.268
+++ compiler/modes.m	28 May 2003 01:04:17 -0000
@@ -138,7 +138,7 @@
 :- import_module parse_tree__inst.
 :- import_module parse_tree__prog_data.
 
-:- import_module bool, list, io.
+:- import_module bool, list, io, std_util.
 
 	% modecheck(HLDS0, HLDS, UnsafeToContinue):
 	% Perform mode inference and checking for a whole module.
@@ -234,8 +234,20 @@
 :- mode modecheck_var_has_inst_list(in, in, in, in, out, mode_info_di, mode_info_uo)
 	is det.
 
-:- pred modecheck_set_var_inst(prog_var, inst, mode_info, mode_info).
-:- mode modecheck_set_var_inst(in, in, mode_info_di, mode_info_uo) is det.
+	% modecheck_set_var_inst(Var, Inst, MaybeUInst, ModeInfo0, ModeInfo).
+	% 	Assign the given Inst to the given Var, after checking that
+	% 	it is okay to do so.  If the inst to be assigned is the
+	% 	result of an abstract unification then the MaybeUInst
+	% 	argument should be the initial inst of the _other_ side of
+	% 	the unification.  This allows more precise (i.e. less
+	% 	conservative) checking in the case that Inst contains `any'
+	% 	components and Var is locked (i.e. is a nonlocal variable in
+	% 	a negated context).  Where the inst is not the result of an
+	% 	abstract unification then MaybeUInst should be `no'.
+
+:- pred modecheck_set_var_inst(prog_var, inst, maybe(inst),
+			mode_info, mode_info).
+:- mode modecheck_set_var_inst(in, in, in, mode_info_di, mode_info_uo) is det.
 
 :- pred modecheck_set_var_inst_list(list(prog_var), list(inst), list(inst),
 		int, list(prog_var), extra_goals, mode_info, mode_info).
@@ -1721,7 +1733,7 @@
 		% record the fact that Var was bound to ConsId in the instmap
 	{ list__duplicate(AdjustedArity, free, ArgInsts) },
 	modecheck_set_var_inst(Var,
-		bound(unique, [functor(ConsId, ArgInsts)])).
+		bound(unique, [functor(ConsId, ArgInsts)]), no).
 
 %-----------------------------------------------------------------------------%
 
@@ -1945,11 +1957,12 @@
 		instmap__lookup_var(InstMap0, Var0, VarInst0),
 		handle_implied_mode(Var0, VarInst0, InitialInst,
 		 	Var, ExtraGoals0, ExtraGoals, ModeInfo0, ModeInfo1),
-		modecheck_set_var_inst(Var0, FinalInst, ModeInfo1, ModeInfo2),
+		modecheck_set_var_inst(Var0, FinalInst, no,
+			ModeInfo1, ModeInfo2),
 		( Var = Var0 ->
 			ModeInfo = ModeInfo2
 		;
-			modecheck_set_var_inst(Var, FinalInst,
+			modecheck_set_var_inst(Var, FinalInst, no,
 				ModeInfo2, ModeInfo)
 		)
 	;
@@ -1959,11 +1972,11 @@
 	).
 
 	% Note that there are two versions of modecheck_set_var_inst,
-	% one with arity 7 and one with arity 4.
+	% one with arity 7 and one with arity 5.
 	% The former is used for predicate calls, where we may need
 	% to introduce unifications to handle calls to implied modes.
 
-modecheck_set_var_inst(Var0, FinalInst, ModeInfo00, ModeInfo) :-
+modecheck_set_var_inst(Var0, FinalInst, MaybeUInst, ModeInfo00, ModeInfo) :-
 	mode_info_get_instmap(ModeInfo0, InstMap0),
 	mode_info_get_parallel_vars(PVars0, ModeInfo00, ModeInfo0),
 	( instmap__is_reachable(InstMap0) ->
@@ -1982,6 +1995,8 @@
 			error("modecheck_set_var_inst: unify_inst failed")
 		),
 		mode_info_set_module_info(ModeInfo0, ModuleInfo, ModeInfo1),
+		mode_info_get_var_types(ModeInfo1, VarTypes),
+		map__lookup(VarTypes, Var0, Type),
 		(
 			% if the top-level inst of the variable is not_reached,
 			% then the instmap as a whole must be unreachable
@@ -1993,8 +2008,6 @@
 			% If we haven't added any information and
 			% we haven't bound any part of the var, then
 			% the only thing we can have done is lose uniqueness.
-			mode_info_get_var_types(ModeInfo1, VarTypes),
-			map__lookup(VarTypes, Var0, Type),
 			inst_matches_initial(Inst0, Inst, Type, ModuleInfo)
 		->
 			instmap__set(InstMap0, Var0, Inst, InstMap),
@@ -2004,8 +2017,6 @@
 			% lost some uniqueness, or bound part of the var.
 			% The call to inst_matches_binding will succeed
 			% only if we haven't bound any part of the var.
-			mode_info_get_var_types(ModeInfo1, VarTypes),
-			map__lookup(VarTypes, Var0, Type),
 			inst_matches_binding(Inst, Inst0, Type, ModuleInfo)
 		->
 			% We've just added some information
@@ -2018,8 +2029,24 @@
 				ModeInfo2, ModeInfo3)
 		;
 			% We've bound part of the var.  If the var was locked,
-			% then we need to report an error.
-			mode_info_var_is_locked(ModeInfo1, Var0, Reason0)
+			% then we need to report an error...
+			mode_info_var_is_locked(ModeInfo1, Var0, Reason0),
+			\+ (
+				% ...unless the goal is a unification and the
+				% var was unified with something less
+				% instantiated than itself.
+				% This allows for the case of `any = free', for
+				% example. The call to
+				% inst_matches_binding, above will fail for the
+				% var with mode `any >> any' however, it should
+				% be allowed because it has only been unified
+				% with a free variable.
+				MaybeUInst = yes(UInst),
+				inst_is_at_least_as_instantiated(Inst, UInst,
+					Type, ModuleInfo),
+				\+ inst_is_at_least_as_instantiated(UInst, Inst,
+					Type, ModuleInfo)
+			)
 		->
 			set__singleton_set(WaitingVars, Var0),
 			mode_info_error(WaitingVars,
Index: tests/hard_coded/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/hard_coded/Mmakefile,v
retrieving revision 1.197
diff -u -r1.197 Mmakefile
--- tests/hard_coded/Mmakefile	7 May 2003 06:42:43 -0000	1.197
+++ tests/hard_coded/Mmakefile	28 May 2003 01:04:17 -0000
@@ -7,6 +7,7 @@
 ORDINARY_PROGS=	\
 	address_of_builtins \
 	agg \
+	any_free_unify \
 	bidirectional \
 	brace \
 	builtin_inst_rename \
Index: tests/hard_coded/any_free_unify.exp
===================================================================
RCS file: tests/hard_coded/any_free_unify.exp
diff -N tests/hard_coded/any_free_unify.exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/any_free_unify.exp	28 May 2003 01:04:17 -0000
@@ -0,0 +1 @@
+yes
Index: tests/hard_coded/any_free_unify.m
===================================================================
RCS file: tests/hard_coded/any_free_unify.m
diff -N tests/hard_coded/any_free_unify.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/any_free_unify.m	28 May 2003 01:04:17 -0000
@@ -0,0 +1,33 @@
+:- module any_free_unify.
+
+:- interface.
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+
+:- implementation.
+
+:- import_module std_util, list, bool.
+
+main -->
+	{ test_any_free_unify([], Result1) },
+	io__print(Result1), io__nl.
+
+:- pred test_any_free_unify(list(int), bool).
+:- mode test_any_free_unify(in(list_skel(any)), out) is det.
+
+% In the unification in the condition of the if-then-else, the variable
+% List has an inst which includes `any' components.  Normally, we can't
+% check whether `any' has become further instantiated over a goal so we
+% do not allow it in a negated context.  However, in this case, the
+% `any' component is unified with `free' so we know that it cannot have
+% become further instantiated.  Therefore we should allow the
+% unification in the condition.
+
+test_any_free_unify(List, Result) :-
+	( List = [_ | _] ->
+		Result = no
+	;
+		Result = yes
+	).
-- 
David Overton                  Uni of Melbourne     +61 3 8344 1354
dmo at cs.mu.oz.au                Monash Uni (Clayton) +61 3 9905 5779
http://www.cs.mu.oz.au/~dmo    Mobile Phone         +61 4 0337 4393
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------