for review: allow `any' insts as non-local vars in higher-order terms

[Fergus Henderson]

Comments, please?
Andrew, is this OK with you?

Estimated hours taken: 1

compiler/modecheck_unify.m:
	Change mode checking of lambda expressions so that
	it allows non-local variables to have inst `any'.
	This change undoes some of bromage's recent change
	to add proper checking for lambda expressions.
	Andrew's change as correct, but unfortunately it breaks most
	uses of the `freeze' predicate in extras/trailed_update/var.m
	(e.g. it breaks extras/trailed_update/samples/vqueens.m).
	I think that for the moment it is better to allow such code,
	even if it may potentially be unsafe, because disallowing it
	would reduce expressiveness too much.

	In the long term we ought to look at adding support for
	some kind of `any -> the_same_any' mode which is like
	`any -> any' but which does not allow the argument to be
	bound.  Or, if that turns out to be too hard, another
	alternative would be to add run-time checking, so that
	we can ensure soundness at run-time even if we can't
	ensure it at compile-time.

Index: modecheck_unify.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modecheck_unify.m,v
retrieving revision 1.30
diff -u -u -r1.30 modecheck_unify.m
--- modecheck_unify.m	1998/02/13 18:00:35	1.30
+++ modecheck_unify.m	1998/02/15 06:47:41
@@ -347,7 +347,7 @@
 	% First modecheck the lambda goal itself:
 	%
 	% initialize the initial insts of the lambda variables,
-	% check that the non-local vars are ground,
+	% check that the non-local vars are ground (XXX or any),
 	% mark the non-local vars as shared,
 	% lock the non-local vars,
 	% mark the non-clobbered lambda variables as live,
@@ -373,8 +373,11 @@
 	% 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, we get around this by sharing
-	% all non-local variables at the top of the lambda goal.
+	% to a fixpoint. 
+	%
+	% For the moment, since doing all the 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.
 	%
 
 	mode_info_get_module_info(ModeInfo0, ModuleInfo0),
@@ -404,7 +407,8 @@
  
 	% lock the non-locals
 	% (a lambda goal is not allowed to bind any of the non-local
-	% variables, since it could get called more than once)
+	% variables, since it could get called more than once, or
+	% from inside a negation)
 	Goal0 = _ - GoalInfo0,
 	goal_info_get_nonlocals(GoalInfo0, NonLocals0),
 	set__delete_list(NonLocals0, Vars, NonLocals),
@@ -428,7 +432,17 @@
 		%     (See the above comment on merging the initial and
 		%     final instmaps.)
 
-		inst_list_is_ground(NonLocalInsts, ModuleInfo2)
+		% XXX This test is also not conservative enough!
+		%
+		%     We should not allow non-local vars to have inst `any';
+		%     because that can lead to unsoundness.
+		%     However, disallowing that idiom would break
+		%     extras/trailed_update/samples/vqueens.m, and
+		%     would make freeze/3 basically useless...
+		%     so for now at least, let's not disallow it,
+		%     even though it is unsafe.
+
+		inst_list_is_ground_or_any(NonLocalInsts, ModuleInfo2)
 	->
 		make_shared_inst_list(NonLocalInsts, ModuleInfo2,
 			SharedNonLocalInsts, ModuleInfo3),

-- 
Fergus Henderson <fjh at cs.mu.oz.au>   |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>   |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3         |     -- the last words of T. S. Garp.