for review: preliminary support for existential types

Fergus Henderson fjh at cs.mu.OZ.AU
Fri Jun 5 04:27:30 AEST 1998


Hi,

DJ, can you please review this?

--------------------

Estimated hours taken: 20

Add support for existentially-typed functions and predicates.

There's three main limitations:

1.  XXX It doesn't do any mode checking or mode reordering.
If you write code that uses existentially typed procedures in the
wrong order, then you'll get an internal error in polymorphism.m
or in the code generator.  (Cases where a type_info has no
producer at all are caught by the check for unbound type
variables in post_typecheck.m.)

2.  Mixing existential typing and type classes won't work yet.
If you try to put a type class constraint on an existentially
quantified type variable, you will get a compile error.
(Extending it to support this would be pretty straight-forward.)

3.  Using `in' modes on arguments of existential type won't work.
If you try, you will get a compile error.
(Extending it to support this would be somewhat tricky.)

Nevertheless, it is still quite useful as is.
I think it is worthwhile committing it now, and then fixing item 1
and extending it to support items 2 and maybe 3 at some later time.

The test case for this stuff will be `std_util.m' and `term.m'
in the standard library.  But for bootstrapping reasons,
I'm not committing that now.

compiler/prog_data.m:
	Add a new field to the parse tree representation of pred and
	func declarations to hold a list of the existentially quantified
	type variables.

compiler/hlds_pred.m:
	Add two new fields to the pred_info:
	a list of the existentially quantified type variables
	and a list of the "HeadTypeParams": type variables which
	cannot be bound by this predicate (i.e. those whose type_infos
	come from this pred's caller or are returned from
	other preds called by this one).

compiler/prog_io.m:
	Add code to parse existential quantifiers on pred and func
	declarations.

compiler/mercury_to_mercury.m:
	Add code to pretty-print existential quantifiers on pred and func
	declarations.

compiler/make_hlds.m:
	Take the set of existentially quantified type variables from
	the parse tree and use that to initialize the new field in
	the pred_info.

compiler/typecheck.m:
	Move the `HeadTypeParams' (the set of type variables which the
	predicate is not allowed to bind) from the typecheck_info into the
	type_assign structure, since with existential types, this set
	varies dynamically during the process of type checking/inference
	and can be different for different overloadings.

	When type checking predicates with existential types,
	don't include the existentially typed variables in that set.

	When type checking calls to predicates with existential
	types, or unifications with functions that have
	existential types, add the existentially typed variables
	from the callee's type to that the HeadTypeParams set.

	Save the final HeadTypeParams in the pred_info.

compiler/post_typecheck.m:
	When checking for unbound type variables,
	use the value of HeadTypeParams from the pred_info.

compiler/polymorphism.m:
	Give type_infos for existentially quantified type variables
	mode "out" rather than mode "in".
	At calls, don't try to produce a value for such variables
	(the callee will do that) and update the instmap delta to
	record that they are now ground.

compiler/*.m:
	Minor changes to reflect the above-mentioned data structure
	changes in prog_data.m and hlds_pred.m.

Index: compiler/arg_info.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/arg_info.m,v
retrieving revision 1.28
diff -u -r1.28 arg_info.m
--- arg_info.m	1998/04/08 11:31:07	1.28
+++ arg_info.m	1998/06/03 13:02:12
@@ -89,7 +89,7 @@
 	module_info_preds(ModuleInfo0, PredTable0),
 	map__lookup(PredTable0, PredId, PredInfo0),
 	pred_info_procedures(PredInfo0, ProcTable0),
-	pred_info_arg_types(PredInfo0, _TVarSet, ArgTypes),
+	pred_info_arg_types(PredInfo0, ArgTypes),
 	map__lookup(ProcTable0, ProcId, ProcInfo0),
 
 	generate_proc_arg_info(ProcInfo0, ArgTypes, ModuleInfo0,
Index: compiler/check_typeclass.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/check_typeclass.m,v
retrieving revision 1.9
diff -u -r1.9 check_typeclass.m
--- check_typeclass.m	1998/05/27 14:36:40	1.9
+++ check_typeclass.m	1998/06/03 15:19:54
@@ -197,7 +197,7 @@
 			)),
 		ProcIds),
 	module_info_pred_info(ModuleInfo0, PredId, PredInfo),
-	pred_info_arg_types(PredInfo, ArgTypeVars, ArgTypes),
+	pred_info_arg_types(PredInfo, ArgTypeVars, _ExistQVars, ArgTypes),
 	pred_info_get_class_context(PredInfo, ClassContext0),
 		% The first constraint in the class context of a class method
 		% is always the constraint for the class of which it is
@@ -495,7 +495,7 @@
 	Info0 = instance_method_info(ModuleInfo0, PredName, PredArity, ArgTypes,
 		ClassContext, ArgModes, Errors, ArgTypeVars, Status,
 		PredOrFunc, Context),
-	pred_info_arg_types(InstancePredInfo, _, InstanceArgTypes),
+	pred_info_arg_types(InstancePredInfo, _, ExistQVars, InstanceArgTypes),
 	pred_info_get_class_context(InstancePredInfo, InstanceClassContext),
 	(
 			% As an optimisation, if the types and constraints
@@ -538,9 +538,9 @@
 
 
 		pred_info_init(ModuleName, PredName, PredArity, ArgTypeVars, 
-			ArgTypes, Cond, Context, DummyClausesInfo, Status,
-			Markers, none, PredOrFunc, ClassContext, Proofs,
-			PredInfo0),
+			ExistQVars, ArgTypes, Cond, Context, DummyClausesInfo,
+			Status, Markers, none, PredOrFunc, ClassContext,
+			Proofs, PredInfo0),
 
 		module_info_globals(ModuleInfo0, Globals),
 		globals__get_args_method(Globals, ArgsMethod),
Index: compiler/code_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/code_util.m,v
retrieving revision 1.97
diff -u -r1.97 code_util.m
--- code_util.m	1998/05/25 21:48:46	1.97
+++ code_util.m	1998/06/03 13:06:57
@@ -259,7 +259,7 @@
 	(
 		code_util__compiler_generated(PredInfo)
 	->
-		pred_info_arg_types(PredInfo, _TypeVarSet, ArgTypes),
+		pred_info_arg_types(PredInfo, ArgTypes),
 		(
 			special_pred_get_type(PredName, ArgTypes, Type),
 			type_to_type_id(Type, TypeId, _),
Index: compiler/deforest.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/deforest.m,v
retrieving revision 1.2
diff -u -r1.2 deforest.m
--- deforest.m	1998/05/15 07:07:01	1.2
+++ deforest.m	1998/06/03 14:53:52
@@ -933,7 +933,8 @@
 	pd_info_get_module_info(ModuleInfo),
 	{ module_info_pred_proc_info(ModuleInfo, PredId, ProcId,
 		CalledPredInfo, CalledProcInfo) },
-	{ pred_info_arg_types(CalledPredInfo, CalledTVarSet, ArgTypes0) },
+	{ pred_info_arg_types(CalledPredInfo, CalledTVarSet, _CalledExistQVars,
+		ArgTypes0) },
 
 		% Rename the arguments in the version.
 	pd_info_get_proc_info(ProcInfo0),
@@ -1207,7 +1208,7 @@
 
 	module_info_pred_info(ModuleInfo, NonGeneralisedPredId, 
 		NonGeneralisedPredInfo),
-	pred_info_arg_types(NonGeneralisedPredInfo, _, NonGeneralisedArgTypes),
+	pred_info_arg_types(NonGeneralisedPredInfo, NonGeneralisedArgTypes),
 	deforest__create_deforest_call_args(NonGeneralisedArgs, 
 		NonGeneralisedArgTypes, GeneralRenaming, TypeRenaming,
 		NewArgs, VarSet, _, VarTypes, _),
Index: compiler/equiv_type.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/equiv_type.m,v
retrieving revision 1.15
diff -u -r1.15 equiv_type.m
--- equiv_type.m	1998/04/08 15:23:23	1.15
+++ equiv_type.m	1998/06/03 11:28:46
@@ -113,10 +113,10 @@
 				TypeDefn, VarSet, ContainsCirc).
 
 equiv_type__replace_in_item(
-		pred(VarSet0, PredName, TypesAndModes0, 
+		pred(VarSet0, ExistQVars, PredName, TypesAndModes0, 
 			Det, Cond, Purity, ClassContext0),
 		EqvMap,
-		pred(VarSet, PredName, TypesAndModes, 
+		pred(VarSet, ExistQVars, PredName, TypesAndModes, 
 			Det, Cond, Purity, ClassContext),
 		no) :-
 	equiv_type__replace_in_class_constraints(ClassContext0, VarSet0, 
@@ -125,11 +125,11 @@
 					TypesAndModes, VarSet).
 
 equiv_type__replace_in_item(
-			func(VarSet0, PredName, TypesAndModes0, 
+			func(VarSet0, ExistQVars, PredName, TypesAndModes0, 
 				RetTypeAndMode0, Det, Cond, Purity,
 				ClassContext0),
 			EqvMap,
-			func(VarSet, PredName, TypesAndModes, 
+			func(VarSet, ExistQVars, PredName, TypesAndModes, 
 				RetTypeAndMode, Det, Cond, Purity,
 				ClassContext),
 			no) :-
@@ -225,9 +225,9 @@
 :- mode equiv_type__replace_in_class_method(in, in, out) is det.
 
 equiv_type__replace_in_class_method(EqvMap,
-			pred(VarSet0, PredName, TypesAndModes0, 
+			pred(VarSet0, ExistQVars, PredName, TypesAndModes0, 
 				Det, Cond, ClassContext0, Context),
-			pred(VarSet, PredName, TypesAndModes, 
+			pred(VarSet, ExistQVars, PredName, TypesAndModes, 
 				Det, Cond, ClassContext, Context)
 			) :-
 	equiv_type__replace_in_class_constraints(ClassContext0, VarSet0, 
@@ -236,10 +236,10 @@
 					TypesAndModes, VarSet).
 
 equiv_type__replace_in_class_method(EqvMap,
-			func(VarSet0, PredName, TypesAndModes0, 
+			func(VarSet0, ExistQVars, PredName, TypesAndModes0, 
 				RetTypeAndMode0, Det, Cond,
 				ClassContext0, Context),
-			func(VarSet, PredName, TypesAndModes, 
+			func(VarSet, ExistQVars, PredName, TypesAndModes, 
 				RetTypeAndMode, Det, Cond,
 				ClassContext, Context)
 			) :-
Index: compiler/export.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/export.m,v
retrieving revision 1.23
diff -u -r1.23 export.m
--- export.m	1998/05/27 02:20:11	1.23
+++ export.m	1998/06/03 13:09:54
@@ -231,7 +231,7 @@
 	pred_info_procedures(PredInfo, ProcTable),
 	map__lookup(ProcTable, ProcId, ProcInfo),
 	proc_info_arg_info(ProcInfo, ArgInfos),
-	pred_info_arg_types(PredInfo, _TVarSet, ArgTypes),
+	pred_info_arg_types(PredInfo, ArgTypes),
 	proc_info_interface_code_model(ProcInfo, CodeModel),
 	assoc_list__from_corresponding_lists(ArgInfos, ArgTypes,
 		ArgInfoTypes0),
Index: compiler/fact_table.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/fact_table.m,v
retrieving revision 1.19
diff -u -r1.19 fact_table.m
--- fact_table.m	1998/05/21 16:51:42	1.19
+++ fact_table.m	1998/06/03 13:11:22
@@ -182,7 +182,7 @@
 	io__open_output(OutputFileName, Result1),
 	(
 	    { Result1 = ok(OutputStream) },
-	    { pred_info_arg_types(PredInfo0, _, Types) },
+	    { pred_info_arg_types(PredInfo0, Types) },
 	    { init_fact_arg_infos(Types, FactArgInfos0) },
 	    infer_determinism_pass_1(PredInfo0, PredInfo1, Context, ModuleInfo,
 	    	CheckProcs, ExistsAllInMode, WriteHashTables, WriteDataTable,
@@ -377,7 +377,7 @@
 		(
 		    { Len = Arity }
 		->
-		    { pred_info_arg_types(PredInfo, _, Types) },
+		    { pred_info_arg_types(PredInfo, Types) },
 		    check_fact_type_and_mode(Types, Terms, 0, PredOrFunc, 
 			Context, Result),
 		    { pred_info_procedures(PredInfo, ProcTable) },
Index: compiler/higher_order.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/higher_order.m,v
retrieving revision 1.43
diff -u -r1.43 higher_order.m
--- higher_order.m	1998/06/03 00:43:08	1.43
+++ higher_order.m	1998/06/04 17:27:23
@@ -583,7 +583,7 @@
 		Changed = unchanged,
 		Goal = Goal0
 	;	
-		pred_info_arg_types(PredInfo, _, ArgTypes),
+		pred_info_arg_types(PredInfo, ArgTypes),
 		find_higher_order_args(Module, Args0, ArgTypes, PredVars, 1,
 				[], HigherOrderArgs0, Args0, Args1),
 		list__reverse(HigherOrderArgs0, HigherOrderArgs),
@@ -661,7 +661,7 @@
 		% Find any known higher-order arguments
 		% in the list of curried arguments.
 		module_info_pred_info(ModuleInfo, PredId, PredInfo),
-		pred_info_arg_types(PredInfo, _, CurriedArgTypes),
+		pred_info_arg_types(PredInfo, CurriedArgTypes),
 		find_higher_order_args(ModuleInfo, CurriedArgs,
 			CurriedArgTypes, PredVars, 1, [], HOCurriedArgs0,
 			CurriedArgs, NewExtraArgs0),
@@ -804,7 +804,7 @@
 	pred_info_module(PredInfo0, PredModule),
 	globals__io_lookup_bool_option(very_verbose, VeryVerbose,
 							IOState0, IOState1),
-        pred_info_arg_types(PredInfo0, Tvars, Types0),
+        pred_info_arg_types(PredInfo0, Tvars, ExistQVars, Types0),
 	string__int_to_string(Arity, ArStr),
 	(
  		VeryVerbose = yes
@@ -842,7 +842,7 @@
 	% hlds dumps if it's filled in.
 	ClausesInfo = clauses_info(EmptyVarSet, EmptyVarTypes,
 		EmptyVarTypes, [], []),
-	pred_info_init(PredModule, Name, Arity, Tvars,
+	pred_info_init(PredModule, Name, Arity, Tvars, ExistQVars,
 		Types, true, Context, ClausesInfo, local, MarkerList, GoalType,
 		PredOrFunc, ClassContext, EmptyProofs, PredInfo1),
 	pred_info_set_typevarset(PredInfo1, TypeVars, PredInfo2),
@@ -964,6 +964,7 @@
 	predicate_table_get_preds(PredTable0, Preds0),
 	map__lookup(Preds0, NewPredId, NewPredInfo0),
 	pred_info_procedures(NewPredInfo0, NewProcs0),
+	pred_info_get_exist_quant_tvars(NewPredInfo0, ExistQVars0),
 	map__init(Substitution0),
 	proc_info_headvars(NewProcInfo0, HeadVars0),
 	proc_info_argmodes(NewProcInfo0, ArgModes0),
@@ -997,7 +998,10 @@
 	goal_util__create_variables(TypeVars, VarSet0, DummyVarTypes,
 		Renaming0, DummyVarTypes, VarSet0, ArgTVarset, _, Renaming),
 	term__apply_variable_renaming_to_list(ArgTypes0, Renaming, ArgTypes),
-	pred_info_set_arg_types(NewPredInfo1, ArgTVarset, ArgTypes,
+	% the real set of existentially quantified variables may be
+	% smaller, but this is OK
+	apply_partial_map_to_list(ExistQVars0, Renaming, ExistQVars),
+	pred_info_set_arg_types(NewPredInfo1, ArgTVarset, ExistQVars, ArgTypes,
 							 NewPredInfo2),
 	map__init(PredVars0),
         traverse_goal(Goal1, Goal2, proc(NewPredId, NewProcId), _, GoalSize,
@@ -1057,7 +1061,8 @@
 	list__index1_det(HeadVars0, Index, LVar),
 	module_info_pred_proc_info(ModuleInfo, PredId, ProcId,
 					CalledPredInfo, CalledProcInfo),
-	pred_info_arg_types(CalledPredInfo, CalledTVarset, CalledArgTypes0),
+	pred_info_arg_types(CalledPredInfo, CalledTVarset, _CalledExistQVars,
+		CalledArgTypes0),
 					
 	% Add the curried arguments to the procedure's argument list.
 	proc_info_argmodes(CalledProcInfo, CalledArgModes),
Index: compiler/hlds_out.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_out.m,v
retrieving revision 1.193
diff -u -r1.193 hlds_out.m
--- hlds_out.m	1998/05/15 07:07:09	1.193
+++ hlds_out.m	1998/06/04 16:15:54
@@ -255,7 +255,8 @@
 		{ special_pred_description(Kind, Descr) },
 		io__write_string(Descr),
 		io__write_string(" for type "),
-		{ pred_info_arg_types(PredInfo, TVarSet, ArgTypes) },
+		{ pred_info_arg_types(PredInfo, TVarSet, _ExistQVars,
+			ArgTypes) },
 		( { special_pred_get_type(Name, ArgTypes, Type) } ->
 			mercury_output_term(Type, TVarSet, no)
 		;
@@ -475,7 +476,8 @@
 
 hlds_out__write_pred(Indent, ModuleInfo, PredId, PredInfo) -->
 	{ pred_info_module(PredInfo, Module) },
-	{ pred_info_arg_types(PredInfo, _, ArgTypes) },
+	{ pred_info_arg_types(PredInfo, ArgTypes) },
+	{ pred_info_get_exist_quant_tvars(PredInfo, ExistQVars) },
 	{ pred_info_typevarset(PredInfo, TVarSet) },
 	{ pred_info_clauses_info(PredInfo, ClausesInfo) },
 	{ pred_info_procedures(PredInfo, ProcTable) },
@@ -486,11 +488,13 @@
 	{ pred_info_get_is_pred_or_func(PredInfo, PredOrFunc) },
 	{ pred_info_get_class_context(PredInfo, ClassContext) },
 	{ pred_info_get_purity(PredInfo, Purity) },
+	{ pred_info_get_head_type_params(PredInfo, HeadTypeParams) },
 	globals__io_lookup_string_option(verbose_dump_hlds, Verbose),
 	( { string__contains_char(Verbose, 'C') } ->
 		% Information about predicates is dumped if 'C' 
 		% suboption is on.
-		mercury_output_pred_type(TVarSet, qualified(Module, PredName), 
+		mercury_output_pred_type(TVarSet, ExistQVars,
+				qualified(Module, PredName), 
 				ArgTypes, no, Purity, ClassContext, Context)
 	;
 		[]
@@ -524,6 +528,16 @@
 		{ AppendVarnums = no }
 	),
 	( { string__contains_char(Verbose, 'C') } ->
+		( { HeadTypeParams \= [] } ->
+			io__write_string(
+				"% head_type_params:\n"),
+			io__write_string("% "),
+			mercury_output_vars(HeadTypeParams, TVarSet,
+					AppendVarnums),
+			io__write_string("\n")
+		;
+			[]
+		),
 		hlds_out__write_var_types(Indent, VarSet, AppendVarnums,
 			VarTypes, TVarSet),
 
@@ -1400,7 +1414,7 @@
 	),
 	( { MaybeType = yes(Type), TypeQual = yes(TVarSet, _) } ->
 		io__write_string(" TYPE_QUAL_OP "),
-		mercury_output_term(Type, TVarSet, no)
+		mercury_output_term(Type, TVarSet, AppendVarnums)
 	;
 		[]
 	),
@@ -1691,7 +1705,7 @@
 	io__write_int(VarNum),
 	io__write_string(")"),
 	io__write_string(" :: "),
-	mercury_output_term(Type, TypeVarSet, no),
+	mercury_output_term(Type, TypeVarSet, AppendVarnums),
 	io__write_string("\n"),
 	hlds_out__write_var_types_2(Vars, Indent, VarSet, AppendVarnums,
 		VarTypes, TypeVarSet).
Index: compiler/hlds_pred.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_pred.m,v
retrieving revision 1.48
diff -u -r1.48 hlds_pred.m
--- hlds_pred.m	1998/05/15 07:07:10	1.48
+++ hlds_pred.m	1998/06/03 19:52:52
@@ -275,26 +275,18 @@
 	% Various predicates for accessing the information stored in the
 	% pred_id and pred_info data structures.
 
-:- pred pred_info_init(module_name, sym_name, arity, tvarset, list(type),
-	condition, term__context, clauses_info, import_status,
+:- pred pred_info_init(module_name, sym_name, arity, tvarset, existq_tvars,
+	list(type), condition, term__context, clauses_info, import_status,
 	pred_markers, goal_type, pred_or_func, list(class_constraint), 
 	map(class_constraint, constraint_proof), pred_info).
-:- mode pred_info_init(in, in, in, in, in, in, in, in, in, in, in, in, in, in,
-	out) is det.
+:- mode pred_info_init(in, in, in, in, in, in, in, in, in, in, in, in, in,
+	in, in, out) is det.
 
-:- pred pred_info_create(module_name, sym_name, tvarset, list(type),
-	condition, term__context, import_status, pred_markers,
+:- pred pred_info_create(module_name, sym_name, tvarset, existq_tvars,
+	list(type), condition, term__context, import_status, pred_markers,
 	pred_or_func, list(class_constraint), proc_info, proc_id, pred_info).
-:- mode pred_info_create(in, in, in, in, in, in, in, in, in, in, in, out, out)
-	is det.
-
-:- pred pred_info_set(tvarset, list(type), condition, clauses_info, proc_table,
-	term__context, module_name, string, arity, import_status,
-	tvarset, goal_type, pred_markers, pred_or_func, 
-	list(class_constraint), map(class_constraint, constraint_proof),
-	pred_info).
-:- mode pred_info_set(in, in, in, in, in, in, in, in, in, in, in, in, in, in, 
-	in, in, out) is det.
+:- mode pred_info_create(in, in, in, in, in, in, in, in, in, in, in, in,
+	out, out) is det.
 
 :- pred pred_info_module(pred_info, module_name).
 :- mode pred_info_module(in, out) is det.
@@ -322,11 +314,26 @@
 :- pred pred_info_exported_procids(pred_info, list(proc_id)).
 :- mode pred_info_exported_procids(in, out) is det.
 
-:- pred pred_info_arg_types(pred_info, tvarset, list(type)).
-:- mode pred_info_arg_types(in, out, out) is det.
+:- pred pred_info_arg_types(pred_info, list(type)).
+:- mode pred_info_arg_types(in, out) is det.
+
+:- pred pred_info_arg_types(pred_info, tvarset, existq_tvars, list(type)).
+:- mode pred_info_arg_types(in, out, out, out) is det.
+
+:- pred pred_info_set_arg_types(pred_info, tvarset, existq_tvars, list(type),
+			pred_info).
+:- mode pred_info_set_arg_types(in, in, in, in, out) is det.
+
+:- pred pred_info_get_exist_quant_tvars(pred_info, existq_tvars).
+:- mode pred_info_get_exist_quant_tvars(in, out) is det.
+
+:- type head_type_params == list(tvar).
+
+:- pred pred_info_get_head_type_params(pred_info, head_type_params).
+:- mode pred_info_get_head_type_params(in, out) is det.
 
-:- pred pred_info_set_arg_types(pred_info, tvarset, list(type), pred_info).
-:- mode pred_info_set_arg_types(in, in, in, out) is det.
+:- pred pred_info_set_head_type_params(pred_info, head_type_params, pred_info).
+:- mode pred_info_set_head_type_params(in, in, out) is det.
 
 :- pred pred_info_clauses_info(pred_info, clauses_info).
 :- mode pred_info_clauses_info(in, out) is det.
@@ -466,11 +473,7 @@
 invalid_proc_id(-1).
 
 	% The information specific to a predicate, as opposed to a procedure.
-	%
-	% Any changes in this type definition will almost certainly require
-	% corresponding changes in define.m.
-	% XXX: This comment is either ancient, or prophesy. It seems
-	% define.m doesn't exist yet.
+	% (Functions count as predicates.)
 
 :- type pred_info
 	--->	predicate(
@@ -505,27 +508,46 @@
 			list(class_constraint),
 					% the class constraints on the 
 					% predicate
-			map(class_constraint, constraint_proof)
+			map(class_constraint, constraint_proof),
 					% explanations of how redundant
 					% constraints were eliminated. These
 					% are needed by polymorphism.m to
 					% work out where to get the
 					% typeclass_infos from.
+					% Computed during type checking.
+			existq_tvars,	% the set of existentially quantified
+					% type variables in the predicate's
+					% type decl
+			head_type_params
+					% The set of type variables which the
+					% body of the predicate can't bind,
+					% and whose type_infos are produced
+					% elsewhere.  This includes
+					% universally quantified head types
+					% (the type_infos are passed in)
+					% plus existentially quantified types
+					% in preds called from the body
+					% (the type_infos are returned from
+					% the called preds).
+					% Computed during type checking.
 		).
 
-pred_info_init(ModuleName, SymName, Arity, TypeVarSet, Types, Cond, Context,
-		ClausesInfo, Status, Markers, GoalType, PredOrFunc, 
-		ClassContext, ClassProofs, PredInfo) :-
+pred_info_init(ModuleName, SymName, Arity, TypeVarSet, ExistQVars, Types,
+		Cond, Context, ClausesInfo, Status, Markers, GoalType,
+		PredOrFunc, ClassContext, ClassProofs, PredInfo) :-
 	map__init(Procs),
 	unqualify_name(SymName, PredName),
 	sym_name_get_module_name(SymName, ModuleName, PredModuleName),
+	term__vars_list(Types, TVars),
+	list__delete_elems(TVars, ExistQVars, HeadTypeParams),
 	PredInfo = predicate(TypeVarSet, Types, Cond, ClausesInfo, Procs,
 		Context, PredModuleName, PredName, Arity, Status, TypeVarSet, 
-		GoalType, Markers, PredOrFunc, ClassContext, ClassProofs).
+		GoalType, Markers, PredOrFunc, ClassContext, ClassProofs,
+		ExistQVars, HeadTypeParams).
 
-pred_info_create(ModuleName, SymName, TypeVarSet, Types, Cond, Context,
-		Status, Markers, PredOrFunc, ClassContext, ProcInfo, ProcId,
-		PredInfo) :-
+pred_info_create(ModuleName, SymName, TypeVarSet, ExistQVars, Types, Cond,
+		Context, Status, Markers, PredOrFunc, ClassContext,
+		ProcInfo, ProcId, PredInfo) :-
 	map__init(Procs0),
 	proc_info_declared_determinism(ProcInfo, MaybeDetism),
 	next_mode_id(Procs0, MaybeDetism, ProcId),
@@ -538,21 +560,16 @@
 	% The empty list of clauses is a little white lie.
 	ClausesInfo = clauses_info(VarSet, VarTypes, VarTypes, HeadVars, []),
 	map__init(ClassProofs),
+	term__vars_list(Types, TVars),
+	list__delete_elems(TVars, ExistQVars, HeadTypeParams),
 	PredInfo = predicate(TypeVarSet, Types, Cond, ClausesInfo, Procs,
 		Context, ModuleName, PredName, Arity, Status, TypeVarSet, 
-		clauses, Markers, PredOrFunc, ClassContext, ClassProofs).
-
-pred_info_set(HeadTVarSet, Types, Cond, ClausesInfo, Procs, Context,
-		PredModuleName, PredName, Arity, Status, AllTVarSet,
-		GoalType, Markers, PredOrFunc, ClassContext, ClassProofs,
-		PredInfo) :-
-	PredInfo = predicate(HeadTVarSet, Types, Cond, ClausesInfo, Procs,
-		Context, PredModuleName, PredName, Arity, Status, AllTVarSet, 
-		GoalType, Markers, PredOrFunc, ClassContext, ClassProofs).
+		clauses, Markers, PredOrFunc, ClassContext, ClassProofs,
+		ExistQVars, HeadTypeParams).
 
 pred_info_procids(PredInfo, ProcIds) :-
 	PredInfo = predicate(_, _, _, _, Procs, _, _, _, _, _, _, _, 
-		_, _, _, _),
+		_, _, _, _, _, _),
 	map__keys(Procs, ProcIds).
 
 pred_info_non_imported_procids(PredInfo, ProcIds) :-
@@ -578,51 +595,58 @@
 	).
 
 pred_info_clauses_info(PredInfo, Clauses) :-
-	PredInfo = predicate(_, _, _, Clauses, _, _, _, _, _, _, _, _,
-		_, _, _, _).
+	PredInfo = predicate(_, _, _, Clauses, _, _, _, _, _, _, _, _, _,
+		_, _, _, _, _).
 
 pred_info_set_clauses_info(PredInfo0, Clauses, PredInfo) :-
-	PredInfo0 = predicate(A, B, C, _, E, F, G, H, I, J, K, L, M, N, O, P),
+	PredInfo0 = predicate(A, B, C, _, E, F, G, H, I, J, K, L, M, N, O, P,
+		Q, R),
 	PredInfo = predicate(A, B, C, Clauses, E, F, G, H, I, J, K, 
-		L, M, N, O, P).
+		L, M, N, O, P, Q, R).
+
+pred_info_arg_types(PredInfo, ArgTypes) :-
+	pred_info_arg_types(PredInfo, _TypeVars, _ExistQVars, ArgTypes).
 
-pred_info_arg_types(PredInfo, TypeVars, ArgTypes) :-
+pred_info_arg_types(PredInfo, TypeVars, ExistQVars, ArgTypes) :-
 	PredInfo = predicate(TypeVars, ArgTypes, 
-		_, _, _, _, _, _, _, _, _, _, _, _, _, _).
+		_, _, _, _, _, _, _, _, _, _, _, _, _, _, ExistQVars, _).
 
-pred_info_set_arg_types(PredInfo0, TypeVarSet, ArgTypes, PredInfo) :-
-	PredInfo0 = predicate(_, _, C, D, E, F, G, H, I, J, K, L, M, N, O, P),
+pred_info_set_arg_types(PredInfo0, TypeVarSet, ExistQVars, ArgTypes,
+		PredInfo) :-
+	PredInfo0 = predicate(_, _, C, D, E, F, G, H, I, J, K, L, M, N, O, P,
+		_, R),
 	PredInfo = predicate(TypeVarSet, ArgTypes, 
-			C, D, E, F, G, H, I, J, K, L, M, N, O, P).
+		C, D, E, F, G, H, I, J, K, L, M, N, O, P, ExistQVars, R).
 
 pred_info_procedures(PredInfo, Procs) :-
 	PredInfo = predicate(_, _, _, _, Procs, _, _, _, _, _, _, 
-		_, _, _, _, _).
+		_, _, _, _, _, _, _).
 
 pred_info_set_procedures(PredInfo0, Procedures, PredInfo) :-
-	PredInfo0 = predicate(A, B, C, D, _, F, G, H, I, J, K, L, M, N, O, P),
+	PredInfo0 = predicate(A, B, C, D, _, F, G, H, I, J, K, L, M, N, O, P,
+		Q, R),
 	PredInfo = predicate(A, B, C, D, Procedures, F, G, H, I, J, K, L, M, 
-		N, O, P).
+		N, O, P, Q, R).
 
 pred_info_context(PredInfo, Context) :-
 	PredInfo = predicate(_, _, _, _, _, Context, _, _, _, 
-		_, _, _, _, _, _, _).
+		_, _, _, _, _, _, _, _, _).
 
 pred_info_module(PredInfo, Module) :-
 	PredInfo = predicate(_, _, _, _, _, _, Module, _, _, _, _, 
-		_, _, _, _, _).
+		_, _, _, _, _, _, _).
 
 pred_info_name(PredInfo, PredName) :-
 	PredInfo = predicate(_, _, _, _, _, _, _, PredName, _, _, _, 
-		_, _, _, _, _).
+		_, _, _, _, _, _, _).
 
 pred_info_arity(PredInfo, Arity) :-
 	PredInfo = predicate(_, _, _, _, _, _, _, _, Arity, _, _, 
-		_, _, _, _, _).
+		_, _, _, _, _, _, _).
 
 pred_info_import_status(PredInfo, ImportStatus) :-
 	PredInfo = predicate(_, _, _, _, _, _, _, _, _, ImportStatus, _, _, _,
-				_, _, _).
+				_, _, _, _, _).
 
 pred_info_is_imported(PredInfo) :-
 	pred_info_import_status(PredInfo, imported).
@@ -640,32 +664,36 @@
 	ImportStatus = pseudo_exported.
 
 pred_info_mark_as_external(PredInfo0, PredInfo) :-
-	PredInfo0 = predicate(A, B, C, D, E, F, G, H, I, _, K, L, M, N, O, P),
+	PredInfo0 = predicate(A, B, C, D, E, F, G, H, I, _, K, L, M, N, O, P,
+		Q, R),
 	PredInfo  = predicate(A, B, C, D, E, F, G, H, I, imported, K, L, M, 
-		N, O, P).
+		N, O, P, Q, R).
 
 pred_info_set_import_status(PredInfo0, Status, PredInfo) :-
-	PredInfo0 = predicate(A, B, C, D, E, F, G, H, I, _, K, L, M, N, O, P),
+	PredInfo0 = predicate(A, B, C, D, E, F, G, H, I, _, K, L, M, N, O, P,
+		Q, R),
 	PredInfo  = predicate(A, B, C, D, E, F, G, H, I, Status, K, 
-		L, M, N, O, P).
+		L, M, N, O, P, Q, R).
 
 pred_info_typevarset(PredInfo, TypeVarSet) :-
 	PredInfo = predicate(_, _, _, _, _, _, _, _, _, _, TypeVarSet, _, _, 
-		_, _, _).
+		_, _, _, _, _).
 
 pred_info_set_typevarset(PredInfo0, TypeVarSet, PredInfo) :-
-	PredInfo0 = predicate(A, B, C, D, E, F, G, H, I, J, _, L, M, N, O, P),
+	PredInfo0 = predicate(A, B, C, D, E, F, G, H, I, J, _, L, M, N, O, P,
+		Q, R),
 	PredInfo  = predicate(A, B, C, D, E, F, G, H, I, J, TypeVarSet, L, M,
-				N, O, P).
+				N, O, P, Q, R).
 
 pred_info_get_goal_type(PredInfo, GoalType) :-
 	PredInfo = predicate(_, _, _, _, _, _, _, _, _, _, _, GoalType, _, 
-		_, _, _).
+		_, _, _, _, _).
 
 pred_info_set_goal_type(PredInfo0, GoalType, PredInfo) :-
-	PredInfo0 = predicate(A, B, C, D, E, F, G, H, I, J, K, _, M, N, O, P),
+	PredInfo0 = predicate(A, B, C, D, E, F, G, H, I, J, K, _, M, N, O, P,
+		Q, R),
 	PredInfo  = predicate(A, B, C, D, E, F, G, H, I, J, K, GoalType, M, 
-		N, O, P).
+		N, O, P, Q, R).
 
 pred_info_requested_inlining(PredInfo0) :-
 	pred_info_get_markers(PredInfo0, Markers),
@@ -699,34 +727,51 @@
 
 pred_info_get_markers(PredInfo, Markers) :-
 	PredInfo = predicate(_, _, _, _, _, _, _, _, _, _, _, _, Markers, 
-		_, _, _).
+		_, _, _, _, _).
 
 pred_info_set_markers(PredInfo0, Markers, PredInfo) :-
-	PredInfo0 = predicate(A, B, C, D, E, F, G, H, I, J, K, L, _, N, O, P),
+	PredInfo0 = predicate(A, B, C, D, E, F, G, H, I, J, K, L, _, N, O, P,
+		Q, R),
 	PredInfo  = predicate(A, B, C, D, E, F, G, H, I, J, K, L, Markers, 
-		N, O, P).
+		N, O, P, Q, R).
 
 pred_info_get_is_pred_or_func(PredInfo, IsPredOrFunc) :-
 	PredInfo = predicate(_, _, _, _, _, _, _, _, _, _, _, _, _,
-			IsPredOrFunc, _, _).
+			IsPredOrFunc, _, _, _, _).
 
 pred_info_set_class_context(PredInfo0, ClassContext, PredInfo) :-
-	PredInfo0 = predicate(A, B, C, D, E, F, G, H, I, J, K, L, M, N, _, P),
+	PredInfo0 = predicate(A, B, C, D, E, F, G, H, I, J, K, L, M, N, _, P,
+		Q, R),
 	PredInfo  = predicate(A, B, C, D, E, F, G, H, I, J, K, L, M, N, 
-		ClassContext, P).
+		ClassContext, P, Q, R).
 
 pred_info_get_class_context(PredInfo, ClassContext) :-
 	PredInfo = predicate(_, _, _, _, _, _, _, _, _, _, _, _, _, _, 
-		ClassContext, _).
+		ClassContext, _, _, _).
 
 pred_info_set_constraint_proofs(PredInfo0, Proofs, PredInfo) :-
-	PredInfo0 = predicate(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, _),
+	PredInfo0 = predicate(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, _,
+		Q, R),
 	PredInfo  = predicate(A, B, C, D, E, F, G, H, I, J, K, L, M, N, 
-		O, Proofs).
+		O, Proofs, Q, R).
 
 pred_info_get_constraint_proofs(PredInfo, ConstraintProofs) :-
 	PredInfo = predicate(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _,
-		ConstraintProofs).
+		ConstraintProofs, _, _).
+
+pred_info_get_exist_quant_tvars(PredInfo, ExistQVars) :-
+	PredInfo = predicate(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _,
+		_, ExistQVars, _).
+
+pred_info_get_head_type_params(PredInfo, HeadTypeParams) :-
+	PredInfo = predicate(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _,
+		_, _, HeadTypeParams).
+
+pred_info_set_head_type_params(PredInfo0, HeadTypeParams, PredInfo) :-
+	PredInfo0 = predicate(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P,
+		Q, _),
+	PredInfo  = predicate(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P,
+		Q, HeadTypeParams).
 
 %-----------------------------------------------------------------------------%
 
@@ -796,12 +841,17 @@
 
 	globals__get_args_method(Globals, ArgsMethod),
 
-	proc_info_create(VarSet, VarTypes, ArgVars, ArgModes, Detism,
-		Goal0, Context, TVarMap, TCVarMap, ArgsMethod, ProcInfo0),
+	proc_info_create(VarSet, VarTypes, ArgVars, ArgModes,
+		Detism, Goal0, Context, TVarMap, TCVarMap, ArgsMethod,
+		ProcInfo0),
 	proc_info_set_maybe_termination_info(ProcInfo0, TermInfo, ProcInfo),
 
-	pred_info_create(ModuleName, SymName, TVarSet, ArgTypes, true,
-		Context, local, Markers, predicate, ClassContext, 
+	% XXX The set of existentially quantified type variables
+	% here might not be correct.
+	ExistQVars = [],
+
+	pred_info_create(ModuleName, SymName, TVarSet, ExistQVars, ArgTypes,
+		true, Context, local, Markers, predicate, ClassContext, 
 		ProcInfo, ProcId, PredInfo),
 
 	module_info_get_predicate_table(ModuleInfo0, PredTable0),
Index: compiler/intermod.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/intermod.m,v
retrieving revision 1.54
diff -u -r1.54 intermod.m
--- intermod.m	1998/06/03 00:43:12	1.54
+++ intermod.m	1998/06/04 17:27:26
@@ -904,20 +904,20 @@
 	{ module_info_pred_info(ModuleInfo, PredId, PredInfo) },
 	{ pred_info_module(PredInfo, Module) },
 	{ pred_info_name(PredInfo, Name) },
-	{ pred_info_arg_types(PredInfo, TVarSet, ArgTypes) },
+	{ pred_info_arg_types(PredInfo, TVarSet, ExistQVars, ArgTypes) },
 	{ pred_info_context(PredInfo, Context) },
 	{ pred_info_get_purity(PredInfo, Purity) },
 	{ pred_info_get_is_pred_or_func(PredInfo, PredOrFunc) },
 	{ pred_info_get_class_context(PredInfo, ClassContext) },
 	(
 		{ PredOrFunc = predicate },
-		mercury_output_pred_type(TVarSet, qualified(Module, Name),
-					ArgTypes, no, Purity, ClassContext,
-					Context)
+		mercury_output_pred_type(TVarSet, ExistQVars,
+			qualified(Module, Name), ArgTypes, no, Purity,
+			ClassContext, Context)
 	;
 		{ PredOrFunc = function },
 		{ pred_args_to_func_args(ArgTypes, FuncArgTypes, FuncRetType) },
-		mercury_output_func_type(TVarSet,
+		mercury_output_func_type(TVarSet, ExistQVars,
 			qualified(Module, Name), FuncArgTypes,
 			FuncRetType, no, Purity, ClassContext, Context)
 	),
@@ -973,7 +973,7 @@
 intermod__write_preds(_, []) --> [].
 intermod__write_preds(ModuleInfo, [PredId | PredIds]) -->
 	{ module_info_pred_info(ModuleInfo, PredId, PredInfo) },
-	{ pred_info_arg_types(PredInfo, _, ArgTypes) },
+	{ pred_info_arg_types(PredInfo, ArgTypes) },
 	{ list__length(ArgTypes, Arity) },
 	{ pred_info_module(PredInfo, Module) },
 	{ pred_info_name(PredInfo, Name) },
Index: compiler/lambda.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/lambda.m,v
retrieving revision 1.42
diff -u -r1.42 lambda.m
--- lambda.m	1998/04/27 04:01:30	1.42
+++ lambda.m	1998/06/03 15:13:37
@@ -353,8 +353,12 @@
 			PredOrFunc, OrigPredName, OrigLine,
 			LambdaCount, PredName),
 		goal_info_get_context(LambdaGoalInfo, LambdaContext),
-		% the TVarSet is a superset of what it really ought be,
-		% but that shouldn't matter
+		% The TVarSet is a superset of what it really ought be,
+		% but that shouldn't matter.
+		% Currently lambda expressions are always monomorphic
+		% in Mercury, so there are no existentially quantified
+		% type variables (no universally quantified tvars either).
+		ExistQVars = [],
 		lambda__uni_modes_to_modes(UniModes1, OrigArgModes),
 
 		% We have to jump through hoops to work out the mode
@@ -402,9 +406,9 @@
 			TVarMap, TCVarMap, ArgsMethod, ProcInfo),
 
 		init_markers(Markers),
-		pred_info_create(ModuleName, PredName, TVarSet, ArgTypes,
-			true, LambdaContext, local, Markers, PredOrFunc,
-			Constraints, ProcInfo, ProcId, PredInfo),
+		pred_info_create(ModuleName, PredName, TVarSet, ExistQVars,
+			ArgTypes, true, LambdaContext, local, Markers,
+			PredOrFunc, Constraints, ProcInfo, ProcId, PredInfo),
 
 		% save the new predicate in the predicate table
 
Index: compiler/make_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.265
diff -u -r1.265 make_hlds.m
--- make_hlds.m	1998/05/15 07:07:16	1.265
+++ make_hlds.m	1998/06/03 14:57:59
@@ -188,19 +188,19 @@
 	module_add_mode_defn(Module0, VarSet, ModeDefn, Cond, Context,
 			Status, Module).
 
-add_item_decl_pass_1(pred(VarSet, PredName, TypesAndModes, 
+add_item_decl_pass_1(pred(VarSet, ExistQVars, PredName, TypesAndModes, 
 		MaybeDet, Cond, Purity, ClassContext),
 		Context, Status, Module0, Status, Module) -->
 	{ init_markers(Markers) },
-	module_add_pred(Module0, VarSet, PredName, TypesAndModes, MaybeDet,
-		Cond, Purity, ClassContext, Markers, Context, Status, _,
-		Module).
+	module_add_pred(Module0, VarSet, ExistQVars, PredName, TypesAndModes,
+		MaybeDet, Cond, Purity, ClassContext, Markers, Context,
+		Status, _, Module).
 
-add_item_decl_pass_1(func(VarSet, FuncName, TypesAndModes, RetTypeAndMode,
-		MaybeDet, Cond, Purity, ClassContext), 
+add_item_decl_pass_1(func(VarSet, ExistQVars, FuncName, TypesAndModes,
+		RetTypeAndMode, MaybeDet, Cond, Purity, ClassContext), 
 		Context, Status, Module0, Status, Module) -->
 	{ init_markers(Markers) },
-	module_add_func(Module0, VarSet, FuncName, TypesAndModes,
+	module_add_func(Module0, VarSet, ExistQVars, FuncName, TypesAndModes,
 		RetTypeAndMode, MaybeDet, Cond, Purity, ClassContext, Markers,
 		Context, Status, _, Module).
 
@@ -397,8 +397,8 @@
 			Module)
 	).
 
-add_item_decl_pass_2(func(_VarSet, FuncName, TypesAndModes, _RetTypeAndMode,
-		_MaybeDet, _Cond, _Purity, _ClassContext), 
+add_item_decl_pass_2(func(_VarSet, _ExistQVars, FuncName, TypesAndModes,
+		_RetTypeAndMode, _MaybeDet, _Cond, _Purity, _ClassContext), 
 		_Context, Status, Module0, Status, Module) -->
 	%
 	% add default modes for function declarations, if necessary
@@ -425,7 +425,7 @@
 		--> [].
 add_item_decl_pass_2(mode_defn(_, _, _), _, Status, Module, Status, Module)
 		--> [].
-add_item_decl_pass_2(pred(_, _, _, _, _, _, _), _, Status, Module, Status,
+add_item_decl_pass_2(pred(_, _, _, _, _, _, _, _), _, Status, Module, Status,
 		Module) --> [].
 add_item_decl_pass_2(pred_mode(_, _, _, _, _), _, Status, Module, Status,
 		Module) --> [].
@@ -483,9 +483,9 @@
 				Module, Module, Info, Info) --> [].
 add_item_clause(mode_defn(_, _, _), Status, Status, _,
 				Module, Module, Info, Info) --> [].
-add_item_clause(pred(_, _, _, _, _, _, _), Status, Status, _,
+add_item_clause(pred(_, _, _, _, _, _, _, _), Status, Status, _,
 				Module, Module, Info, Info) --> [].
-add_item_clause(func(_, _, _, _, _, _, _, _), Status, Status, _,
+add_item_clause(func(_, _, _, _, _, _, _, _, _), Status, Status, _,
 				Module, Module, Info, Info) --> [].
 add_item_clause(pred_mode(_, _, _, _, _), Status, Status, _,
 				Module, Module, Info, Info) --> [].
@@ -1205,16 +1205,17 @@
 
 %-----------------------------------------------------------------------------%
 
-:- pred module_add_pred(module_info, varset, sym_name, list(type_and_mode),
-		maybe(determinism), condition, purity, list(class_constraint), 
+:- pred module_add_pred(module_info, varset, existq_tvars, sym_name,
+		list(type_and_mode), maybe(determinism), condition, purity,
+		list(class_constraint), 
 		pred_markers, term__context, item_status, 
 		maybe(pair(pred_id, proc_id)), module_info, 
 		io__state, io__state).
-:- mode module_add_pred(in, in, in, in, in, in, in, in, in, in, in, out, out,
-		di, uo) is det.
+:- mode module_add_pred(in, in, in, in, in, in, in, in, in, in, in, in,
+		out, out, di, uo) is det.
 
-module_add_pred(Module0, VarSet, PredName, TypesAndModes, MaybeDet, Cond,
-		Purity, ClassContext, Markers, Context, 
+module_add_pred(Module0, VarSet, ExistQVars, PredName, TypesAndModes, MaybeDet,
+		Cond, Purity, ClassContext, Markers, Context, 
 		item_status(Status, NeedQual), MaybePredProcId, Module) -->
 	% Only preds with opt_imported clauses are tagged as opt_imported, so
 	% that the compiler doesn't look for clauses for other preds read in
@@ -1225,8 +1226,8 @@
 		DeclStatus = Status
 	},
 	{ split_types_and_modes(TypesAndModes, Types, MaybeModes) },
-	add_new_pred(Module0, VarSet, PredName, Types, Cond, Purity, 
-		ClassContext, Markers, Context, DeclStatus, NeedQual, 
+	add_new_pred(Module0, VarSet, ExistQVars, PredName, Types, Cond,
+		Purity, ClassContext, Markers, Context, DeclStatus, NeedQual, 
 		predicate, Module1),
 	(
 		{ MaybeModes = yes(Modes) }
@@ -1239,15 +1240,17 @@
 		{ MaybePredProcId = no }
 	).
 
-:- pred module_add_func(module_info, varset, sym_name, list(type_and_mode),
+:- pred module_add_func(module_info, varset, existq_tvars, sym_name,
+		list(type_and_mode),
 		type_and_mode, maybe(determinism), condition, purity,
 		list(class_constraint), pred_markers, term__context,
 		item_status, maybe(pair(pred_id, proc_id)),
 		module_info, io__state, io__state).
-:- mode module_add_func(in, in, in, in, in, in, in, in, in, in, in, in, 			out, out, di, uo) is det.
+:- mode module_add_func(in, in, in, in, in, in, in, in, in, in, in, in, in, 			out, out, di, uo) is det.
 
-module_add_func(Module0, VarSet, FuncName, TypesAndModes, RetTypeAndMode,
-		MaybeDet, Cond, Purity, ClassContext, Markers, Context,
+module_add_func(Module0, VarSet, ExistQVars, FuncName, TypesAndModes,
+		RetTypeAndMode, MaybeDet, Cond, Purity, ClassContext,
+		Markers, Context,
 		item_status(Status, NeedQual), MaybePredProcId, Module) -->
 	% Only funcs with opt_imported clauses are tagged as opt_imported, so
 	% that the compiler doesn't look for clauses for other preds.
@@ -1259,9 +1262,9 @@
 	{ split_types_and_modes(TypesAndModes, Types, MaybeModes) },
 	{ split_type_and_mode(RetTypeAndMode, RetType, MaybeRetMode) },
 	{ list__append(Types, [RetType], Types1) },
-	add_new_pred(Module0, VarSet, FuncName, Types1, Cond, Purity,
-		ClassContext, Markers, Context, DeclStatus, NeedQual, function,
-		Module1),
+	add_new_pred(Module0, VarSet, ExistQVars, FuncName, Types1, Cond,
+		Purity, ClassContext, Markers, Context, DeclStatus, NeedQual,
+		function, Module1),
 	(
 		{ MaybeModes = yes(Modes) },
 		{ MaybeRetMode = yes(RetMode) }
@@ -1370,25 +1373,27 @@
 module_add_class_method(Method, Name, Vars, Status, MaybePredIdProcId, 
 		Module0, Module) -->
 	(
-		{ Method = pred(VarSet, PredName, TypesAndModes, 
+		{ Method = pred(VarSet, ExistQVars, PredName, TypesAndModes, 
 			MaybeDet, Cond, ClassContext, Context) },
 		{ term__var_list_to_term_list(Vars, VarTerms) },
 		{ NewClassContext = [constraint(Name, VarTerms)|ClassContext] },
 		{ init_markers(Markers0) },
 		{ add_marker(Markers0, class_method, Markers) },
-		module_add_pred(Module0, VarSet, PredName, TypesAndModes,
-			MaybeDet, Cond, pure, NewClassContext, Markers,
-			Context, Status, MaybePredIdProcId, Module)
+		module_add_pred(Module0, VarSet, ExistQVars, PredName,
+			TypesAndModes, MaybeDet, Cond, pure, NewClassContext,
+			Markers, Context, Status, MaybePredIdProcId, Module)
 	;
-		{ Method = func(VarSet, FuncName, TypesAndModes, RetTypeAndMode,
-			MaybeDet, Cond, ClassContext, Context) },
+		{ Method = func(VarSet, ExistQVars, FuncName, TypesAndModes,
+			RetTypeAndMode, MaybeDet, Cond, ClassContext,
+			Context) },
 		{ term__var_list_to_term_list(Vars, VarTerms) },
 		{ NewClassContext = [constraint(Name, VarTerms)|ClassContext] },
 		{ init_markers(Markers0) },
 		{ add_marker(Markers0, class_method, Markers) },
-		module_add_func(Module0, VarSet, FuncName, TypesAndModes,
-			RetTypeAndMode, MaybeDet, Cond, pure, NewClassContext,
-			Markers, Context, Status, MaybePredIdProcId, Module)
+		module_add_func(Module0, VarSet, ExistQVars, FuncName,
+			TypesAndModes, RetTypeAndMode, MaybeDet, Cond, pure,
+			NewClassContext, Markers, Context, Status,
+			MaybePredIdProcId, Module)
 	;
 		{ Method = pred_mode(VarSet, PredName, Modes, MaybeDet, 
 			Cond, Context) },
@@ -1417,7 +1422,7 @@
 add_default_class_method_func_modes([M|Ms], PredProcIds0, PredProcIds,
 		Module0, Module) :-
 	(
-		M = func(_, FuncName, TypesAndModes, _, _, _, _, _)
+		M = func(_, _, FuncName, TypesAndModes, _, _, _, _, _)
 	->
 		( FuncName = qualified(ModuleName0, Func0) ->
 			ModuleName = ModuleName0,
@@ -1497,19 +1502,20 @@
 
 %-----------------------------------------------------------------------------%
 
-:- pred add_new_pred(module_info, tvarset, sym_name, list(type), condition, 
-		purity, list(class_constraint), pred_markers, term__context,
-		import_status, need_qualifier, pred_or_func,
+:- pred add_new_pred(module_info, tvarset, existq_tvars, sym_name, list(type),
+		condition, purity, list(class_constraint), pred_markers,
+		term__context, import_status, need_qualifier, pred_or_func,
 		module_info, io__state, io__state).
-:- mode add_new_pred(in, in, in, in, in, in, in, in, in, in, in, in, out, 
+:- mode add_new_pred(in, in, in, in, in, in, in, in, in, in, in, in, in, out, 
 		di, uo) is det.
 
 % NB.  Predicates are also added in lambda.m, which converts
 % lambda expressions into separate predicates, so any changes may need
 % to be reflected there too.
 
-add_new_pred(Module0, TVarSet, PredName, Types, Cond, Purity, ClassContext,
-		Markers0, Context, Status, NeedQual, PredOrFunc, Module) -->
+add_new_pred(Module0, TVarSet, ExistQVars, PredName, Types, Cond, Purity,
+		ClassContext, Markers0, Context, Status, NeedQual, PredOrFunc,
+		Module) -->
 	{ module_info_name(Module0, ModuleName) },
 	{ list__length(Types, Arity) },
 	(
@@ -1532,7 +1538,8 @@
 				add_marker(TheMarkers0, M, TheMarkers)
 			)) },
 		{ list__foldl(AddMarker, MarkersList, Markers0, Markers) },
-		{ pred_info_init(ModuleName, PredName, Arity, TVarSet, Types,
+		{ pred_info_init(ModuleName, PredName, Arity, TVarSet,
+				ExistQVars, Types,
 				Cond, Context, ClausesInfo, Status, Markers,
 				none, PredOrFunc, ClassContext, Proofs,
 				PredInfo0) },
@@ -1718,9 +1725,10 @@
 		% XXX If/when we have "comparable" or "unifiable" typeclasses, 
 		% XXX this context might not be empty
 	ClassContext = [],
-	pred_info_init(ModuleName, PredName, Arity, TVarSet, ArgTypes, Cond,
-		Context, ClausesInfo0, Status, Markers, none, predicate, 
-		ClassContext, Proofs, PredInfo0),
+	ExistQVars = [],
+	pred_info_init(ModuleName, PredName, Arity, TVarSet, ExistQVars,
+		ArgTypes, Cond, Context, ClausesInfo0, Status, Markers,
+		none, predicate, ClassContext, Proofs, PredInfo0),
 	ArgLives = no,
 	module_info_globals(Module0, Globals),
 	globals__get_args_method(Globals, ArgsMethod),
@@ -1876,10 +1884,13 @@
 		% The class context is empty since this is an implicit
 		% definition. Inference will fill it in.
 	ClassContext = [],
+		% We assume none of the arguments are existentially typed.
+		% Existential types must be declared, they won't be inferred.
+	ExistQVars = [],
 	init_markers(Markers0),
-	pred_info_init(ModuleName, PredName, Arity, TVarSet, Types, Cond,
-		Context, ClausesInfo, local, Markers0, none, PredOrFunc, 
-		ClassContext, Proofs, PredInfo0),
+	pred_info_init(ModuleName, PredName, Arity, TVarSet, ExistQVars,
+		Types, Cond, Context, ClausesInfo, local, Markers0, none,
+		PredOrFunc, ClassContext, Proofs, PredInfo0),
 	add_marker(Markers0, infer_type, Markers),
 	pred_info_set_markers(PredInfo0, Markers, PredInfo),
 	(
@@ -2015,9 +2026,10 @@
 		pred_info_set_clauses_info(PredInfo2, Clauses, PredInfo3),
 		pred_info_set_goal_type(PredInfo3, clauses, PredInfo4),
 		pred_info_set_typevarset(PredInfo4, TVarSet, PredInfo5),
-		pred_info_arg_types(PredInfo5, _ArgTVarSet, ArgTypes),
+		pred_info_arg_types(PredInfo5, _ArgTVarSet,
+				ExistQVars, ArgTypes),
 		pred_info_set_arg_types(PredInfo5, TVarSet,
-					ArgTypes, PredInfo6),
+				ExistQVars, ArgTypes, PredInfo6),
 
 		%
 		% check if there are still no modes for the predicate,
@@ -2217,7 +2229,7 @@
 	%
 	{ pred_info_get_is_pred_or_func(PredInfo0, PredOrFunc) },
 	{ pred_info_clauses_info(PredInfo0, Clauses0) },
-	{ pred_info_arg_types(PredInfo0, _TVarSet, ArgTypes) },
+	{ pred_info_arg_types(PredInfo0, ArgTypes) },
 	{ pred_info_get_purity(PredInfo0, Purity) },
 	{ pred_info_procedures(PredInfo0, Procs) },
 	{ map__lookup(Procs, ProcId, ProcInfo) },
@@ -2480,7 +2492,7 @@
 						ModuleInfo0, ProcId) }
 		->
 			{ pred_info_clauses_info(PredInfo1, Clauses0) },
-			{ pred_info_arg_types(PredInfo1, _TVarSet, ArgTypes) },
+			{ pred_info_arg_types(PredInfo1, ArgTypes) },
 			{ pred_info_get_purity(PredInfo1, Purity) },
 			clauses_info_add_pragma_c_code(Clauses0, Purity,
 				MayCallMercury, PredId, ProcId, VarSet,
@@ -4555,7 +4567,7 @@
 		{module_info_set_pred_info(Module0, PredID, PredInfo, Module1)},
 		{ pred_info_procedures(PredInfo, ProcTable) },
 		{ pred_info_procids(PredInfo, ProcIDs) },
-		{ pred_info_arg_types(PredInfo, _, ArgTypes) },
+		{ pred_info_arg_types(PredInfo, ArgTypes) },
 		{ pred_info_get_is_pred_or_func(PredInfo, PredOrFunc) },
 		{
 		    PredOrFunc = predicate,
Index: compiler/mercury_compile.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_compile.m,v
retrieving revision 1.95
diff -u -r1.95 mercury_compile.m
--- mercury_compile.m	1998/06/04 17:25:57	1.95
+++ mercury_compile.m	1998/06/04 17:38:18
@@ -634,9 +634,6 @@
 		    % only write out the `.opt' file if there are no type errors
 		    % or undefined modes
 		    ( { FoundTypeError = no, FoundUndefModeError = no } ->
-			mercury_compile__maybe_write_optfile(MakeOptInt,
-		    		HLDS3, HLDS4), !
-		    ;
 			    mercury_compile__maybe_write_optfile(MakeOptInt,
 		    		    HLDS4, HLDS5), !
 		    ;
Index: compiler/mercury_to_c.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_to_c.m,v
retrieving revision 1.34
diff -u -r1.34 mercury_to_c.m
--- mercury_to_c.m	1998/03/03 17:35:05	1.34
+++ mercury_to_c.m	1998/06/03 13:47:36
@@ -161,7 +161,7 @@
 :- mode c_gen_pred(in, in, in, in, di, uo) is det.
 
 c_gen_pred(Indent, ModuleInfo, PredId, PredInfo) -->
-	{ pred_info_arg_types(PredInfo, TVarSet, ArgTypes) },
+	{ pred_info_arg_types(PredInfo, TVarSet, ExistQVars, ArgTypes) },
 	{ pred_info_context(PredInfo, Context) },
 	{ pred_info_name(PredInfo, PredName) },
 	{ pred_info_non_imported_procids(PredInfo, ProcIds) },
@@ -172,8 +172,9 @@
 		c_gen_indent(Indent),
 		io__write_string("/****\n"),
 		{ pred_info_get_purity(PredInfo, Purity) },
-		mercury_output_pred_type(TVarSet, unqualified(PredName),
-			ArgTypes, no, Purity, ClassContext, Context),
+		mercury_output_pred_type(TVarSet, ExistQVars,
+			unqualified(PredName), ArgTypes, no, Purity,
+			ClassContext, Context),
 
 		{ pred_info_clauses_info(PredInfo, ClausesInfo) },
 		{ ClausesInfo = clauses_info(VarSet, _VarTypes, _, HeadVars,
@@ -352,7 +353,7 @@
 	{ proc_info_interface_code_model(ProcInfo, CodeModel) },
 	{ proc_info_varset(ProcInfo, VarSet) },
 	{ proc_info_headvars(ProcInfo, HeadVars) },
-	{ pred_info_arg_types(PredInfo, _HeadTypeVarSet, HeadTypes) },
+	{ pred_info_arg_types(PredInfo, HeadTypes) },
 	{ proc_info_argmodes(ProcInfo, HeadModes) },
 
 	( { CodeModel = model_semi } ->
Index: compiler/mercury_to_goedel.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_to_goedel.m,v
retrieving revision 1.63
diff -u -r1.63 mercury_to_goedel.m
--- mercury_to_goedel.m	1998/03/03 17:35:06	1.63
+++ mercury_to_goedel.m	1998/06/03 20:55:34
@@ -143,9 +143,10 @@
 goedel_output_item(mode_defn(VarSet, ModeDefn, _Cond), Context) -->
 	goedel_output_mode_defn(VarSet, ModeDefn, Context).
 
-	% XXX Should we ignore ClassContext, or give an error?
-goedel_output_item(pred(VarSet, PredName, TypesAndModes, _Det, _Cond,
-		Purity, _ClassContext), Context) -->
+	% XXX Should we ignore ClassContext and ExistQVars,
+	% or give an error if they're non-empty?
+goedel_output_item(pred(VarSet, _ExistQVars, PredName, TypesAndModes,
+		_Det, _Cond, Purity, _ClassContext), Context) -->
 	io__write_string("\n"),
 	maybe_write_line_number(Context),
 	(   { Purity = pure } ->
@@ -157,8 +158,10 @@
 	),
 	goedel_output_pred(VarSet, PredName, TypesAndModes, Context).
 
-	% XXX Should we ignore ClassContext, or give an error?
-goedel_output_item(func(VarSet, PredName, TypesAndModes, RetTypeAndMode, _Det,
+	% XXX Should we ignore ClassContext and ExistQVars,
+	% or give an error if they're non-empty?
+goedel_output_item(func(VarSet, _ExistQVars, PredName,
+		TypesAndModes, RetTypeAndMode, _Det,
 		_Cond, Purity, _ClassContext), Context) -->
 	io__write_string("\n"),
 	maybe_write_line_number(Context),
Index: compiler/mercury_to_mercury.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_to_mercury.m,v
retrieving revision 1.136
diff -u -r1.136 mercury_to_mercury.m
--- mercury_to_mercury.m	1998/05/26 19:19:16	1.136
+++ mercury_to_mercury.m	1998/06/03 15:14:09
@@ -31,15 +31,16 @@
 				io__state, io__state).
 :- mode convert_to_mercury(in, in, in, di, uo) is det.
 
-:- pred mercury_output_pred_type(varset, sym_name, list(type),
+:- pred mercury_output_pred_type(tvarset, existq_tvars, sym_name, list(type),
 		maybe(determinism), purity, list(class_constraint),
 		term__context, io__state, io__state).
-:- mode mercury_output_pred_type(in, in, in, in, in, in, in, di, uo) is det.
+:- mode mercury_output_pred_type(in, in, in, in, in, in, in, in, di, uo) is det.
 
-:- pred mercury_output_func_type(varset, sym_name, list(type), type,
+:- pred mercury_output_func_type(tvarset, existq_tvars, sym_name,
+		list(type), type,
 		maybe(determinism), purity, list(class_constraint),
 		term__context, io__state, io__state).
-:- mode mercury_output_func_type(in, in, in, in, in, in, in, in, 
+:- mode mercury_output_func_type(in, in, in, in, in, in, in, in, in, 
 		di, uo) is det.
 
 :- pred mercury_output_pred_mode_decl(varset, sym_name, list(mode),
@@ -241,16 +242,16 @@
 	maybe_output_line_number(Context),
 	mercury_output_mode_defn(VarSet, ModeDefn, Context).
 
-mercury_output_item(pred(VarSet, PredName, TypesAndModes, Det, _Cond,
-		Purity, ClassContext), Context) -->
+mercury_output_item(pred(VarSet, ExistQVars, PredName, TypesAndModes, Det,
+		_Cond, Purity, ClassContext), Context) -->
 	maybe_output_line_number(Context),
-	mercury_output_pred_decl(VarSet, PredName, TypesAndModes, Det,
-		Purity, ClassContext, Context, ":- ", ".\n", ".\n").
+	mercury_output_pred_decl(VarSet, ExistQVars, PredName, TypesAndModes,
+		Det, Purity, ClassContext, Context, ":- ", ".\n", ".\n").
 
-mercury_output_item(func(VarSet, PredName, TypesAndModes, RetTypeAndMode, Det,
-		_Cond, Purity, ClassContext), Context) -->
+mercury_output_item(func(VarSet, ExistQVars, PredName, TypesAndModes,
+		RetTypeAndMode, Det, _Cond, Purity, ClassContext), Context) -->
 	maybe_output_line_number(Context),
-	mercury_output_func_decl(VarSet, PredName, TypesAndModes,
+	mercury_output_func_decl(VarSet, ExistQVars, PredName, TypesAndModes,
 			RetTypeAndMode, Det, Purity, ClassContext, Context, 
 			":- ", ".\n", ".\n").
 
@@ -439,17 +440,19 @@
 output_class_method(Method) -->
 	io__write_string("\t"),
 	(
-		{ Method = pred(VarSet, Name, TypesAndModes, Detism, 
-			_Condition, ClassContext, Context) },
-		mercury_output_pred_decl(VarSet, Name, TypesAndModes, Detism,
-			pure, ClassContext, Context, "", ",\n\t", "")
-	;
-		{ Method = func(VarSet, Name, TypesAndModes, TypeAndMode, 
+		{ Method = pred(VarSet, ExistQVars, Name, TypesAndModes,
 			Detism, _Condition, ClassContext, Context) },
-		mercury_output_func_decl(VarSet, Name, TypesAndModes,
-			TypeAndMode, Detism, pure, ClassContext, Context, 
+		mercury_output_pred_decl(VarSet, ExistQVars, Name,
+			TypesAndModes, Detism, pure, ClassContext, Context,
 			"", ",\n\t", "")
 	;
+		{ Method = func(VarSet, ExistQVars, Name, TypesAndModes,
+			TypeAndMode, Detism, _Condition, ClassContext,
+			Context) },
+		mercury_output_func_decl(VarSet, ExistQVars, Name,
+			TypesAndModes, TypeAndMode, Detism, pure,
+			ClassContext, Context, "", ",\n\t", "")
+	;
 		{ Method = pred_mode(VarSet, Name, Modes, Detism, 
 			_Condition, Context) },
 		mercury_output_pred_mode_decl_2(VarSet, Name, Modes, Detism,
@@ -1236,13 +1239,14 @@
 
 %-----------------------------------------------------------------------------%
 
-:- pred mercury_output_pred_decl(varset, sym_name, list(type_and_mode),
+:- pred mercury_output_pred_decl(tvarset, existq_tvars,
+		sym_name, list(type_and_mode),
 		maybe(determinism), purity, list(class_constraint),
 		term__context, string, string, string, io__state, io__state).
-:- mode mercury_output_pred_decl(in, in, in, in, in, in, in, in, in, in,
+:- mode mercury_output_pred_decl(in, in, in, in, in, in, in, in, in, in, in,
 		di, uo) is det.
 
-mercury_output_pred_decl(VarSet, PredName, TypesAndModes, MaybeDet, 
+mercury_output_pred_decl(VarSet, ExistQVars, PredName, TypesAndModes, MaybeDet, 
 		Purity, ClassContext, Context, StartString, Separator,
 		Terminator) -->
 	{ split_types_and_modes(TypesAndModes, Types, MaybeModes) },
@@ -1250,30 +1254,33 @@
 		{ MaybeModes = yes(Modes) },
 		{ Modes \= [] }
 	->
-		mercury_output_pred_type_2(VarSet, PredName, Types, MaybeDet, 
-			Purity, ClassContext, Context, StartString, Separator),
+		mercury_output_pred_type_2(VarSet, ExistQVars, PredName,
+			Types, MaybeDet, Purity, ClassContext, Context,
+			StartString, Separator),
 		mercury_output_pred_mode_decl_2(VarSet, PredName, Modes,
 				MaybeDet, Context, StartString, Terminator)
 	;
-		mercury_output_pred_type_2(VarSet, PredName, Types, MaybeDet, 
-			Purity, ClassContext, Context, StartString, Terminator)
+		mercury_output_pred_type_2(VarSet, ExistQVars, PredName,
+			Types, MaybeDet, Purity, ClassContext, Context,
+			StartString, Terminator)
 	).
 
-mercury_output_pred_type(VarSet, PredName, Types, MaybeDet, Purity,
+mercury_output_pred_type(VarSet, ExistQVars, PredName, Types, MaybeDet, Purity,
 		ClassContext, Context) -->
-	mercury_output_pred_type_2(VarSet, PredName, Types, MaybeDet,
-		Purity, ClassContext, Context, ":- ", ".\n").
+	mercury_output_pred_type_2(VarSet, ExistQVars, PredName, Types,
+		MaybeDet, Purity, ClassContext, Context, ":- ", ".\n").
 
 
-:- pred mercury_output_pred_type_2(varset, sym_name, list(type),
+:- pred mercury_output_pred_type_2(tvarset, existq_tvars, sym_name, list(type),
 		maybe(determinism), purity, list(class_constraint),
 		term__context, string, string, io__state, io__state).
-:- mode mercury_output_pred_type_2(in, in, in, in, in, in, in, in, in,
+:- mode mercury_output_pred_type_2(in, in, in, in, in, in, in, in, in, in,
 		di, uo) is det.
 
-mercury_output_pred_type_2(VarSet, PredName, Types, MaybeDet, Purity,
-		ClassContext, _Context, StartString, Separator) -->
+mercury_output_pred_type_2(VarSet, ExistQVars, PredName, Types, MaybeDet,
+		Purity, ClassContext, _Context, StartString, Separator) -->
 	io__write_string(StartString),
+	mercury_output_quantifier(VarSet, ExistQVars),
 	write_purity_prefix(Purity),
 	io__write_string("pred "),
 	(
@@ -1317,48 +1324,51 @@
 
 %-----------------------------------------------------------------------------%
 
-:- pred mercury_output_func_decl(varset, sym_name, list(type_and_mode),
-		type_and_mode, maybe(determinism), 
+:- pred mercury_output_func_decl(tvarset, existq_tvars, sym_name,
+		list(type_and_mode), type_and_mode, maybe(determinism), 
 		purity, list(class_constraint), term__context, string, string,
 		string, io__state, io__state).
 :- mode mercury_output_func_decl(in, in, in, in, in, in, in, in, in, in, in,
-		di, uo) is det.
+		in, di, uo) is det.
 
-mercury_output_func_decl(VarSet, FuncName, TypesAndModes, RetTypeAndMode,
-		MaybeDet, Purity, ClassContext, Context, 
-		StartString, Separator, Terminator) -->
+mercury_output_func_decl(VarSet, ExistQVars, FuncName,
+		TypesAndModes, RetTypeAndMode, MaybeDet, Purity, ClassContext,
+		Context, StartString, Separator, Terminator) -->
 	{ split_types_and_modes(TypesAndModes, Types, MaybeModes) },
 	{ split_type_and_mode(RetTypeAndMode, RetType, MaybeRetMode) },
 	(
 		{ MaybeModes = yes(Modes) },
 		{ MaybeRetMode = yes(RetMode) }
 	->
-		mercury_output_func_type_2(VarSet, FuncName, Types, RetType,
-				no, Purity, ClassContext, Context, 
-				StartString, Separator),
+		mercury_output_func_type_2(VarSet, ExistQVars, FuncName,
+				Types, RetType, no, Purity, ClassContext,
+				Context, StartString, Separator),
 		mercury_output_func_mode_decl_2(VarSet, FuncName, Modes,
 				RetMode, MaybeDet, Context, 
 				StartString, Terminator)
 	;
-		mercury_output_func_type_2(VarSet, FuncName, Types, RetType,
-				MaybeDet, Purity, ClassContext, Context, 
-				StartString, Terminator)
+		mercury_output_func_type_2(VarSet, ExistQVars, FuncName,
+				Types, RetType, MaybeDet, Purity, ClassContext,
+				Context, StartString, Terminator)
 	).
 
-mercury_output_func_type(VarSet, FuncName, Types, RetType, MaybeDet, 
-		Purity, ClassContext, Context) -->
-	mercury_output_func_type_2(VarSet, FuncName, Types, RetType, MaybeDet, 
-			Purity, ClassContext, Context, ":- ", ".\n").
+mercury_output_func_type(VarSet, ExistQVars, FuncName, Types, RetType,
+		MaybeDet, Purity, ClassContext, Context) -->
+	mercury_output_func_type_2(VarSet, ExistQVars, FuncName, Types,
+		RetType, MaybeDet, Purity, ClassContext, Context,
+		":- ", ".\n").
 
-:- pred mercury_output_func_type_2(varset, sym_name, list(type), type,
-		maybe(determinism), purity, list(class_constraint),
+:- pred mercury_output_func_type_2(varset, existq_tvars, sym_name, list(type),
+		type, maybe(determinism), purity, list(class_constraint),
 		term__context, string, string, io__state, io__state).
-:- mode mercury_output_func_type_2(in, in, in, in, in, in, in, in, in, in, 
+:- mode mercury_output_func_type_2(in, in, in, in, in, in, in, in, in, in, in, 
 		di, uo) is det.
 
-mercury_output_func_type_2(VarSet, FuncName, Types, RetType, MaybeDet, 
-		Purity, ClassContext, _Context, StartString, Separator) -->
+mercury_output_func_type_2(VarSet, ExistQVars, FuncName, Types, RetType,
+		MaybeDet, Purity, ClassContext, _Context, StartString,
+		Separator) -->
 	io__write_string(StartString),
+	mercury_output_quantifier(VarSet, ExistQVars),
 	write_purity_prefix(Purity),
 	io__write_string("func "),
 	(
@@ -1377,6 +1387,20 @@
 	mercury_output_class_context(ClassContext, VarSet),
 	mercury_output_det_annotation(MaybeDet),
 	io__write_string(Separator).
+
+%-----------------------------------------------------------------------------%
+
+:- pred mercury_output_quantifier(tvarset, list(tvar), io__state, io__state).
+:- mode mercury_output_quantifier(in, in, di, uo) is det.
+
+mercury_output_quantifier(VarSet, ExistQVars) -->
+	( { ExistQVars = [] } ->
+		[]
+	;
+		io__write_string("some ["),
+		mercury_output_vars(ExistQVars, VarSet, no),
+		io__write_string("] ")
+	).
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/module_qual.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/module_qual.m,v
retrieving revision 1.36
diff -u -r1.36 module_qual.m
--- module_qual.m	1998/05/15 07:07:25	1.36
+++ module_qual.m	1998/06/03 13:53:28
@@ -138,8 +138,8 @@
 	add_mode_defn(ModeDefn, Info0, Info).
 collect_mq_info_2(module_defn(_, ModuleDefn), Info0, Info) :-
 	process_module_defn(ModuleDefn, Info0, Info).
-collect_mq_info_2(pred(_,_,_,_,_,_,_), Info, Info).
-collect_mq_info_2(func(_,_,_,_,_,_,_,_), Info, Info).
+collect_mq_info_2(pred(_,_,_,_,_,_,_,_), Info, Info).
+collect_mq_info_2(func(_,_,_,_,_,_,_,_,_), Info, Info).
 collect_mq_info_2(pred_mode(_,_,_,_,_), Info, Info).
 collect_mq_info_2(func_mode(_,_,_,_,_,_), Info, Info).
 collect_mq_info_2(pragma(_), Info, Info).
@@ -281,8 +281,10 @@
 	{ update_import_status(ModuleDefn, Info0, Info, Continue) }.
 
 module_qualify_item(
-		pred(A, SymName, TypesAndModes0, D,E,F, Constraints0) - Context,
-		pred(A, SymName, TypesAndModes, D,E,F, Constraints) - Context,
+		pred(A, B, SymName, TypesAndModes0, C, D, E,
+			Constraints0) - Context,
+		pred(A, B, SymName, TypesAndModes,  C, D, E,
+			Constraints) - Context,
 		Info0, Info, yes) -->
 	{ list__length(TypesAndModes0, Arity) },
 	{ mq_info_set_error_context(Info0, pred(SymName - Arity) - Context,
@@ -291,9 +293,9 @@
 	qualify_class_constraints(Constraints0, Constraints, Info2, Info).
 
 module_qualify_item(
-		func(A,SymName, TypesAndModes0, TypeAndMode0, D, E, F
-			,Constraints0) - Context,
-		func(A, SymName, TypesAndModes, TypeAndMode, D, E, F,
+		func(A, B, SymName, TypesAndModes0, TypeAndMode0, F, G, H,
+			Constraints0) - Context,
+		func(A, B, SymName, TypesAndModes, TypeAndMode, F, G, H,
 			Constraints) - Context,
 		Info0, Info, yes) -->
 	{ list__length(TypesAndModes0, Arity) },
@@ -741,9 +743,9 @@
 	% There is no need to qualify the method name, since that is
 	% done when the item is parsed.
 qualify_class_method(
-		pred(Varset, Name, TypesAndModes0, MaybeDet, Cond,
+		pred(Varset, ExistQVars, Name, TypesAndModes0, MaybeDet, Cond,
 			ClassContext0, Context), 
-		pred(Varset, Name, TypesAndModes, MaybeDet, Cond, 
+		pred(Varset, ExistQVars, Name, TypesAndModes, MaybeDet, Cond, 
 			ClassContext, Context), 
 		MQInfo0, MQInfo
 		) -->
@@ -752,10 +754,10 @@
 	qualify_class_constraints(ClassContext0, ClassContext, 
 		MQInfo1, MQInfo).
 qualify_class_method(
-		func(Varset, Name, TypesAndModes0, ReturnMode0, MaybeDet, Cond,
-			ClassContext0, Context), 
-		func(Varset, Name, TypesAndModes, ReturnMode, MaybeDet, Cond,
-			ClassContext, Context), 
+		func(Varset, ExistQVars, Name, TypesAndModes0, ReturnMode0,
+			MaybeDet, Cond, ClassContext0, Context), 
+		func(Varset, ExistQVars, Name, TypesAndModes, ReturnMode,
+			MaybeDet, Cond, ClassContext, Context), 
 		MQInfo0, MQInfo
 		) -->
 	qualify_types_and_modes(TypesAndModes0, TypesAndModes, 
Index: compiler/polymorphism.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/polymorphism.m,v
retrieving revision 1.134
diff -u -r1.134 polymorphism.m
--- polymorphism.m	1998/05/25 21:48:53	1.134
+++ polymorphism.m	1998/06/04 15:59:55
@@ -418,7 +418,8 @@
 		map__lookup(ProcTable0, ProcId, ProcInfo),
 		proc_info_vartypes(ProcInfo, VarTypes),
 		proc_info_headvars(ProcInfo, HeadVars),
-		pred_info_arg_types(PredInfo0, TypeVarSet, ArgTypes0),
+		pred_info_arg_types(PredInfo0, TypeVarSet, ExistQVars,
+			ArgTypes0),
 		list__length(ArgTypes0, NumOldArgs),
 		list__length(HeadVars, NumNewArgs),
 		NumExtraArgs is NumNewArgs - NumOldArgs,
@@ -433,8 +434,8 @@
 			error("polymorphism.m: list__split_list failed")
 		),
 
-		pred_info_set_arg_types(PredInfo0, TypeVarSet, ArgTypes,
-			PredInfo),
+		pred_info_set_arg_types(PredInfo0, TypeVarSet, ExistQVars,
+			ArgTypes, PredInfo),
 		map__det_update(PredTable0, PredId, PredInfo, PredTable),
 		module_info_set_preds(ModuleInfo0, PredTable, ModuleInfo1)
 	;
@@ -485,8 +486,10 @@
 
 polymorphism__process_proc(ProcInfo0, PredInfo0, ModuleInfo0,
 				ProcInfo, PredInfo, ModuleInfo) :-
+	%
 	% grab the appropriate fields from the pred_info and proc_info
-	pred_info_arg_types(PredInfo0, ArgTypeVarSet, ArgTypes),
+	%
+	pred_info_arg_types(PredInfo0, ArgTypeVarSet, ExistQVars, ArgTypes),
 	pred_info_typevarset(PredInfo0, TypeVarSet0),
 	pred_info_get_class_context(PredInfo0, ClassContext),
 	pred_info_get_constraint_proofs(PredInfo0, Proofs),
@@ -497,12 +500,13 @@
 	proc_info_goal(ProcInfo0, Goal0),
 	proc_info_argmodes(ProcInfo0, ArgModes0),
 
-
-		% Insert extra head variables to hold the address of the
-		% type_infos and typeclass_infos.
-		% We insert one variable for each unconstrained type variable
-		% (for the type_info) and one variable for each constraint (for
-		% the typeclass_info).
+	%
+	% Insert extra head variables to hold the address of the
+	% type_infos and typeclass_infos.
+	% We insert one variable for each unconstrained type variable
+	% (for the type_info) and one variable for each constraint (for
+	% the typeclass_info).
+	%
 	term__vars_list(ArgTypes, HeadTypeVars0),
 		% Make a fresh variable for each class constraint, returning
 		% a list of variables that appear in the constraints, along
@@ -524,26 +528,34 @@
 	list__append(ExtraHeadTypeclassInfoVars, HeadVars0, HeadVars1),
 	list__append(ExtraHeadTypeInfoVars, HeadVars1, HeadVars),
 
-		% Work out the total number of new vars
-	list__length(ExtraHeadTypeInfoVars, NumExtraVars0),
-	list__length(ExtraHeadTypeclassInfoVars, NumExtraVars1),
-	NumExtraVars is NumExtraVars1 + NumExtraVars0,
-
+	%
+	% Figure out the modes of the introduced type_info and
+	% typeclass_info arguments
+	%
+		
+	list__map(polymorphism__typeinfo_mode(ExistQVars),
+		UnconstrainedTVars, TypeInfoModes),
 	in_mode(In),
-	list__duplicate(NumExtraVars, In, ExtraModes),
-	list__append(ExtraModes, ArgModes0, ArgModes),
+	list__length(ExtraHeadTypeclassInfoVars, NumExtraClassInfoVars),
+	list__duplicate(NumExtraClassInfoVars, In, TypeClassInfoModes),
+	list__append(TypeClassInfoModes, ArgModes0, ArgModes1),
+	list__append(TypeInfoModes, ArgModes1, ArgModes),
 
-		% Make a map of the locations of the unconstrained typeinfos
+	%
+	% Build up the initial tvar->type_info_var mapping
+	%
+		% Make a map of the locations of the typeinfos
+		% for unconstrained, universally quantified type variables.
 	AddLocn = lambda([TVarAndVar::in, TIM0::in, TIM::out] is det,
 		(
 			TVarAndVar = TVar - TheVar,
-			map__det_insert(TIM0, TVar, type_info(TheVar), TIM)
+			map__det_insert(TIM0, TVar, type_info(TheVar),
+				TIM)
 		)),
 	assoc_list__from_corresponding_lists(UnconstrainedTVars,
 		ExtraHeadTypeInfoVars, TVarsAndVars),
 	list__foldl(AddLocn, TVarsAndVars, TypeClassInfoMap, TypeInfoMap1),
 
-
 		% Make a map of the locations of the typeclass_infos
 	map__from_corresponding_lists(ClassContext, ExtraHeadTypeclassInfoVars,
 				TypeclassInfoLocations0),
@@ -552,14 +564,18 @@
 				TypeInfoMap1, TypeclassInfoLocations0,
 				Proofs, PredName, ModuleInfo0),
 
+	%
 	% process any polymorphic calls inside the goal
+	%
 	polymorphism__process_goal(Goal0, Goal1, Info0, Info1),
 	polymorphism__fixup_quantification(Goal1, Goal, _, Info1, Info),
 	Info = poly_info(VarSet, VarTypes, TypeVarSet,
 				TypeInfoMap, TypeclassInfoLocations,
 				_Proofs, _PredName, ModuleInfo),
 
+	%
 	% set the new values of the fields in proc_info and pred_info
+	%
 	proc_info_set_headvars(ProcInfo0, HeadVars, ProcInfo1),
 	proc_info_set_goal(ProcInfo1, Goal, ProcInfo2),
 	proc_info_set_varset(ProcInfo2, VarSet, ProcInfo3),
@@ -595,7 +611,7 @@
 		--> [].
 
 polymorphism__process_goal_expr(call(PredId0, ProcId0, ArgVars0,
-		Builtin, Context, Name0), GoalInfo, Goal) -->
+		Builtin, UnifyContext, Name0), GoalInfo, Goal) -->
 	% Check for a call to a special predicate like compare/3
 	% for which the type is known at compile-time.
 	% Replace such calls with calls to the particular version
@@ -625,12 +641,10 @@
 		{ Name = Name0 }
 	),
 
-	polymorphism__process_call(PredId1, ProcId1, ArgVars0,
-		PredId, ProcId, ArgVars, ExtraVars, ExtraGoals),
-	{ goal_info_get_nonlocals(GoalInfo, NonLocals0) },
-	{ set__insert_list(NonLocals0, ExtraVars, NonLocals) },
-	{ goal_info_set_nonlocals(GoalInfo, NonLocals, CallGoalInfo) },
-	{ Call = call(PredId, ProcId, ArgVars, Builtin, Context, Name)
+	polymorphism__process_call(PredId1, ProcId1, ArgVars0, GoalInfo,
+		PredId, ProcId, ArgVars, _ExtraVars, CallGoalInfo, ExtraGoals),
+
+	{ Call = call(PredId, ProcId, ArgVars, Builtin, UnifyContext, Name)
 		- CallGoalInfo },
 	{ list__append(ExtraGoals, [Call], GoalList) },
 	{ conj_list_to_goal(GoalList, GoalInfo, Goal) }.
@@ -789,14 +803,8 @@
 polymorphism__process_goal_expr(pragma_c_code(IsRecursive, PredId0, ProcId0,
 		ArgVars0, ArgInfo0, OrigArgTypes0, PragmaCode),
 		GoalInfo, Goal) -->
-	polymorphism__process_call(PredId0, ProcId0, ArgVars0,
-		PredId, ProcId, ArgVars, ExtraVars, ExtraGoals),
-	%
-	% update the non-locals
-	%
-	{ goal_info_get_nonlocals(GoalInfo, NonLocals0) },
-	{ set__insert_list(NonLocals0, ExtraVars, NonLocals) },
-	{ goal_info_set_nonlocals(GoalInfo, NonLocals, CallGoalInfo) },
+	polymorphism__process_call(PredId0, ProcId0, ArgVars0, GoalInfo,
+		PredId, ProcId, ArgVars, ExtraVars, CallGoalInfo, ExtraGoals),
 
 	%
 	% insert the type_info vars into the arg-name map,
@@ -805,11 +813,12 @@
 	%
 	=(poly_info(_, _, _, _, _, _, _, ModuleInfo)),
 	{ module_info_pred_info(ModuleInfo, PredId, PredInfo) },
-	{ pred_info_arg_types(PredInfo, PredTypeVarSet, PredArgTypes) },
+	{ pred_info_arg_types(PredInfo, PredTypeVarSet, ExistQVars,
+			PredArgTypes) },
 	{ term__vars_list(PredArgTypes, PredTypeVars0) },
 	{ list__remove_dups(PredTypeVars0, PredTypeVars) },
 	{ polymorphism__c_code_add_typeinfos(ExtraVars, PredTypeVars,
-			PredTypeVarSet, ArgInfo0, ArgInfo) },
+			PredTypeVarSet, ExistQVars, ArgInfo0, ArgInfo) },
 
 	%
 	% insert type_info types for all the inserted type_info vars
@@ -830,27 +839,48 @@
 	{ list__append(ExtraGoals, [Call], GoalList) },
 	{ conj_list_to_goal(GoalList, GoalInfo, Goal) }.
 
-:- pred polymorphism__c_code_add_typeinfos(list(var), list(tvar), tvarset,
-	list(maybe(pair(string, mode))), list(maybe(pair(string, mode)))).
-:- mode polymorphism__c_code_add_typeinfos(in, in, in, in, out) is det.
+:- pred polymorphism__c_code_add_typeinfos(list(var), list(tvar),
+		tvarset, existq_tvars, list(maybe(pair(string, mode))),
+		list(maybe(pair(string, mode)))). 
+:- mode polymorphism__c_code_add_typeinfos(in, in, in, in, in, out) is det.
 
-polymorphism__c_code_add_typeinfos([], [], _, ArgNames, ArgNames).
+polymorphism__c_code_add_typeinfos([], [], _, _, ArgNames, ArgNames).
 polymorphism__c_code_add_typeinfos([_Var|Vars], [TVar|TVars], TypeVarSet,
-		ArgNames0, ArgNames) :-
+		ExistQVars, ArgNames0, ArgNames) :-
 	polymorphism__c_code_add_typeinfos(Vars, TVars, TypeVarSet,
-		ArgNames0, ArgNames1),
+		ExistQVars, ArgNames0, ArgNames1),
 	( varset__search_name(TypeVarSet, TVar, TypeVarName) ->
 		string__append("TypeInfo_for_", TypeVarName, C_VarName),
-		in_mode(Input),
-		ArgNames = [yes(C_VarName - Input) | ArgNames1]
+		polymorphism__typeinfo_mode(ExistQVars, TVar, Mode),
+		ArgNames = [yes(C_VarName - Mode) | ArgNames1]
 	;
 		ArgNames = [no | ArgNames1]
 	).
-polymorphism__c_code_add_typeinfos([], [_|_], _, _, _) :-
+polymorphism__c_code_add_typeinfos([], [_|_], _, _, _, _) :-
 	error("polymorphism__c_code_add_typeinfos: length mismatch").
-polymorphism__c_code_add_typeinfos([_|_], [], _, _, _) :-
+polymorphism__c_code_add_typeinfos([_|_], [], _, _, _, _) :-
 	error("polymorphism__c_code_add_typeinfos: length mismatch").
 
+:- pred polymorphism__typeinfo_mode(existq_tvars, tvar, mode).
+:- mode polymorphism__typeinfo_mode(in, in, out) is det.
+
+polymorphism__typeinfo_mode(ExistQVars, TVar, Mode) :-
+	%
+	% type_infos have mode `in', unless the type
+	% variable is existentially quantified, in which
+	% case the mode is `out'.
+	%
+	% [XXX this would need to change if we allow
+	% `in' modes for arguments with existential types,
+	% because in that case the mode for the type_info
+	% must also be `in']
+	%
+	( list__member(TVar, ExistQVars) ->
+		out_mode(Mode)
+	;
+		in_mode(Mode)
+	).
+
 :- pred polymorphism__process_goal_list(list(hlds_goal), list(hlds_goal),
 					poly_info, poly_info).
 :- mode polymorphism__process_goal_list(in, out, in, out) is det.
@@ -873,27 +903,42 @@
 
 %-----------------------------------------------------------------------------%
 
-:- pred polymorphism__process_call(pred_id, proc_id, list(var),
-					pred_id, proc_id, list(var),
-					list(var), list(hlds_goal),
-					poly_info, poly_info).
-:- mode polymorphism__process_call(in, in, in, out, out, out, out, out,
-					in, out) is det.
+:- pred polymorphism__process_call(pred_id, proc_id, list(var), hlds_goal_info,
+		pred_id, proc_id, list(var), list(var), hlds_goal_info,
+		list(hlds_goal), poly_info, poly_info).
+:- mode polymorphism__process_call(in, in, in, in,
+		out, out, out, out, out, out, in, out) is det.
 
-polymorphism__process_call(PredId0, ProcId0, ArgVars0, PredId, ProcId, ArgVars,
-				ExtraVars, ExtraGoals, Info0, Info) :-
+polymorphism__process_call(PredId0, ProcId0, ArgVars0, GoalInfo0,
+		PredId, ProcId, ArgVars, ExtraVars, GoalInfo, ExtraGoals,
+		Info0, Info) :-
 
 	Info0 = poly_info(A, VarTypes, TypeVarSet0, D, E, F, G, ModuleInfo),
 
 	module_info_pred_info(ModuleInfo, PredId0, PredInfo),
-	pred_info_arg_types(PredInfo, PredTypeVarSet, PredArgTypes0),
+	pred_info_arg_types(PredInfo, PredTypeVarSet, PredExistQVars0,
+		PredArgTypes0),
 	pred_info_get_class_context(PredInfo, PredClassContext0),
 		% rename apart
 		% (this merge might be a performance bottleneck?)
-	varset__merge_subst(TypeVarSet0, PredTypeVarSet, TypeVarSet, Subst),
-	term__apply_substitution_to_list(PredArgTypes0, Subst,
-		PredArgTypes),
-	term__vars_list(PredArgTypes, PredTypeVars0),
+	( varset__is_empty(PredTypeVarSet) ->
+		% optimize common case
+		PredArgTypes = PredArgTypes0,
+		PredExistQVarTerms1 = [],
+		PredTypeVars0 = [],
+		TypeVarSet = TypeVarSet0,
+		map__init(Subst)
+	;
+		varset__merge_subst(TypeVarSet0, PredTypeVarSet, TypeVarSet,
+			Subst),
+		term__apply_substitution_to_list(PredArgTypes0, Subst,
+			PredArgTypes),
+		term__var_list_to_term_list(PredExistQVars0,
+			PredExistQVarTerms0),
+		term__apply_substitution_to_list(PredExistQVarTerms0, Subst,
+			PredExistQVarTerms1),
+		term__vars_list(PredArgTypes, PredTypeVars0)
+	),
 
 	pred_info_module(PredInfo, PredModule),
 	pred_info_name(PredInfo, PredName),
@@ -911,6 +956,7 @@
 		PredId = PredId0,
 		ProcId = ProcId0,
 		ArgVars = ArgVars0,
+		GoalInfo = GoalInfo0,
 		ExtraGoals = [],
 		ExtraVars = [],
 		Info = Info0
@@ -924,7 +970,6 @@
 		error("polymorphism__process_goal_expr: type unification failed")
 		),
 
-
 		apply_subst_to_constraints(Subst, PredClassContext0,
 			PredClassContext),
 
@@ -934,8 +979,10 @@
 			% Make the typeclass_infos for the call, and return
 			% a list of which variables were constrained by the
 			% context
+		goal_info_get_context(GoalInfo0, Context),
 		polymorphism__make_typeclass_info_vars(	
 			PredClassContext, Subst, TypeSubst,
+			PredExistQVars, Context,
 			hlds_class_proc(PredId0, ProcId0),
 			hlds_class_proc(PredId, ProcId),
 			ExtraTypeClassVars, ExtraTypeClassGoals,
@@ -948,17 +995,45 @@
 		term__var_list_to_term_list(PredTypeVars, PredTypes0),
 		term__apply_rec_substitution_to_list(PredTypes0, TypeSubst,
 			PredTypes),
+		term__apply_rec_substitution_to_list(PredExistQVarTerms1,
+			TypeSubst, PredExistQVarTerms),
+		term__term_list_to_var_list(PredExistQVarTerms,
+			PredExistQVars),
 
-		polymorphism__make_type_info_vars(PredTypes,
-			ExtraTypeInfoVars, ExtraTypeInfoGoals,
+		polymorphism__make_type_info_vars(PredTypes, PredExistQVars,
+			Context, ExtraTypeInfoVars, ExtraTypeInfoGoals,
 			Info2, Info),
 		list__append(ExtraTypeClassVars, ArgVars0, ArgVars1),
 		list__append(ExtraTypeInfoVars, ArgVars1, ArgVars),
 		list__append(ExtraTypeClassGoals, ExtraTypeInfoGoals,
 			ExtraGoals),
 		list__append(ExtraTypeClassVars, ExtraTypeInfoVars,
-			ExtraVars)
+			ExtraVars),
+
+		%
+		% update the non-locals
+		%
+		goal_info_get_nonlocals(GoalInfo0, NonLocals0),
+		set__insert_list(NonLocals0, ExtraVars, NonLocals),
+		goal_info_set_nonlocals(GoalInfo0, NonLocals, GoalInfo1),
 
+		%
+		% update the instmap delta for typeinfos vars for
+		% any existentially quantified type vars in the callee's
+		% type: such typeinfo variables are produced by this call
+		%
+		Info = poly_info(_, _, _, TypeVarMap, _, _, _, _),
+
+		goal_info_get_instmap_delta(GoalInfo1, InstmapDelta0),
+		AddInstDelta = lambda([TVar::in, IMD0::in, IMD::out] is det, (
+			map__lookup(TypeVarMap, TVar, TypeInfoLocn),
+			type_info_locn_var(TypeInfoLocn, TypeInfoVar),
+			instmap_delta_set(IMD0, TypeInfoVar,
+				ground(shared, no), IMD)
+			)),
+		list__foldl(AddInstDelta, PredExistQVars,
+			InstmapDelta0, InstmapDelta),
+		goal_info_set_instmap_delta(GoalInfo1, InstmapDelta, GoalInfo)
 	).
 
 :- pred polymorphism__fixup_quantification(hlds_goal, hlds_goal,
@@ -1045,14 +1120,15 @@
 % Otherwise return the original pred_proc_id unchanged.
 
 :- pred polymorphism__make_typeclass_info_vars(list(class_constraint),
-	substitution, tsubst, hlds_class_proc, hlds_class_proc,
+	substitution, tsubst, existq_tvars, term__context,
+	hlds_class_proc, hlds_class_proc,
 	list(var), list(hlds_goal), list(var),
 	poly_info, poly_info).
-:- mode polymorphism__make_typeclass_info_vars(in, in, in, in, out,
+:- mode polymorphism__make_typeclass_info_vars(in, in, in, in, in, in, out,
 	out, out, out, in, out) is det.
 
 polymorphism__make_typeclass_info_vars(PredClassContext, Subst, TypeSubst, 
-		PredProcId0, PredProcId,
+		ExistQVars, Context, PredProcId0, PredProcId,
 		ExtraVars, ExtraGoals, ConstrainedVars, Info0, Info) :-
 
 		% initialise the accumulators
@@ -1069,7 +1145,8 @@
 
 		% do the work
 	polymorphism__make_typeclass_info_vars_2(PredClassContext, 
-		Subst, TypeSubst, MaybePredProcId0, MaybePredProcId,
+		Subst, TypeSubst, ExistQVars, Context,
+		MaybePredProcId0, MaybePredProcId,
 		ExtraVars0, ExtraVars1, 
 		ExtraGoals0, ExtraGoals1,
 		ConstrainedVars0, ConstrainedVars, 
@@ -1090,52 +1167,51 @@
 % Accumulator version of the above.
 :- pred polymorphism__make_typeclass_info_vars_2(
 	list(class_constraint), substitution, tsubst,
+	existq_tvars, term__context,
 	maybe(hlds_class_proc), maybe(hlds_class_proc),
 	list(var), list(var), 
 	list(hlds_goal), list(hlds_goal), 
 	list(var), list(var),
 	poly_info, poly_info).
-:- mode polymorphism__make_typeclass_info_vars_2(in, in, in,
+:- mode polymorphism__make_typeclass_info_vars_2(in, in, in, in, in,
 	in, out, in, out, in, out, in, out, in, out) is det.
 
-polymorphism__make_typeclass_info_vars_2([], _Subst, _TypeSubst,
-		MaybePredProcId, MaybePredProcId,
+polymorphism__make_typeclass_info_vars_2([], _Subst, _TypeSubst, _ExistQVars,
+		_Context, MaybePredProcId, MaybePredProcId,
 		ExtraVars, ExtraVars, 
 		ExtraGoals, ExtraGoals, 
 		ConstrainedVars, ConstrainedVars,
 		Info, Info).
-polymorphism__make_typeclass_info_vars_2([C|Cs], Subst, TypeSubst,
-		MaybePredProcId0, MaybePredProcId,
+polymorphism__make_typeclass_info_vars_2([C|Cs], Subst, TypeSubst, ExistQVars,
+		Context, MaybePredProcId0, MaybePredProcId,
 		ExtraVars0, ExtraVars,
 		ExtraGoals0, ExtraGoals, 
 		ConstrainedVars0, ConstrainedVars,
 		Info0, Info) :-
-	polymorphism__make_typeclass_info_var(C, Subst, TypeSubst,
-			MaybePredProcId0, MaybePredProcId,
+	polymorphism__make_typeclass_info_var(C, Subst, TypeSubst, ExistQVars,
+			Context, MaybePredProcId0, MaybePredProcId,
 			ExtraGoals0, ExtraGoals1, 
 			ConstrainedVars0, ConstrainedVars1,
 			Info0, Info1, MaybeExtraVar),
 	maybe_insert_var(MaybeExtraVar, ExtraVars0, ExtraVars1),
 	polymorphism__make_typeclass_info_vars_2(Cs, Subst, TypeSubst,
-			no, _,
+			ExistQVars, Context, no, _,
 			ExtraVars1, ExtraVars,
 			ExtraGoals1, ExtraGoals, 
 			ConstrainedVars1, ConstrainedVars,
 			Info1, Info).
 
 :- pred polymorphism__make_typeclass_info_var(class_constraint,
-	substitution, tsubst, maybe(hlds_class_proc), maybe(hlds_class_proc),
-	list(hlds_goal), list(hlds_goal), 
-	list(var), list(var),
-	poly_info, poly_info,
-	maybe(var)). 
-:- mode polymorphism__make_typeclass_info_var(in, in, in, in, out,
+	substitution, tsubst, existq_tvars, term__context,
+	maybe(hlds_class_proc), maybe(hlds_class_proc),
+	list(hlds_goal), list(hlds_goal), list(var), list(var),
+	poly_info, poly_info, maybe(var)). 
+:- mode polymorphism__make_typeclass_info_var(in, in, in, in, in, in, out,
 	in, out, in, out, in, out, out) is det.
 
-polymorphism__make_typeclass_info_var(Constraint, Subst, TypeSubst,
-		MaybePredProcId0, MaybePredProcId,
-		ExtraGoals0, ExtraGoals, 
-		ConstrainedVars0, ConstrainedVars, 
+polymorphism__make_typeclass_info_var(Constraint, Subst, TypeSubst, ExistQVars,
+		Context, MaybePredProcId0, MaybePredProcId,
+		ExtraGoals0, ExtraGoals, ConstrainedVars0, ConstrainedVars, 
 		Info0, Info, MaybeVar) :-
 	Constraint = constraint(ClassName, NewConstrainedTypes),
 	list__length(NewConstrainedTypes, ClassArity),
@@ -1253,8 +1329,8 @@
 					% that are constrained by this. These
 					% are packaged in the typeclass_info
 				polymorphism__make_type_info_vars(
-					ConstrainedTypes,
-					InstanceExtraTypeInfoVars,
+					ConstrainedTypes, ExistQVars,
+					Context, InstanceExtraTypeInfoVars,
 					TypeInfoGoals,
 					Info0, Info1),
 
@@ -1263,7 +1339,7 @@
 					% instance decl.
 				polymorphism__make_typeclass_info_vars_2(
 					InstanceConstraints, Subst, TypeSubst, 
-					no, _,
+					ExistQVars, Context, no, _,
 					[], InstanceExtraTypeClassInfoVars, 
 					ExtraGoals0, ExtraGoals1, 
 					[], _,
@@ -1272,7 +1348,9 @@
 				polymorphism__construct_typeclass_info(
 					InstanceExtraTypeInfoVars, 
 					InstanceExtraTypeClassInfoVars, 
-					ClassId, InstanceNum, Var, NewGoals, 
+					ClassId, InstanceNum,
+					ExistQVars,
+					Var, NewGoals, 
 					Info2, Info),
 
 				MaybeVar = yes(Var),
@@ -1322,7 +1400,7 @@
 				% Make the typeclass_info for the subclass
 			polymorphism__make_typeclass_info_var(
 				SubClassConstraint, Subst, TypeSubst, 
-				no, _,
+				ExistQVars, Context, no, _,
 				ExtraGoals0, ExtraGoals1, 
 				[], _,
 				Info1, Info2,
@@ -1420,12 +1498,13 @@
 	).
 
 :- pred polymorphism__construct_typeclass_info(list(var), list(var), class_id, 
-	int, var, list(hlds_goal), poly_info, poly_info).
-:- mode polymorphism__construct_typeclass_info(in, in, in, in, out, out, 
+	int, existq_tvars, var, list(hlds_goal), poly_info, poly_info).
+:- mode polymorphism__construct_typeclass_info(in, in, in, in, in, out, out, 
 	in, out) is det.
 
 polymorphism__construct_typeclass_info(ArgTypeInfoVars, ArgTypeClassInfoVars,
-		ClassId, InstanceNum, NewVar, NewGoals, Info0, Info) :-
+		ClassId, InstanceNum, ExistQVars,
+		NewVar, NewGoals, Info0, Info) :-
 
 	Info0 = poly_info(_, _, _, _, _, _, _, ModuleInfo),
 
@@ -1439,8 +1518,8 @@
 	map__lookup(ClassTable, ClassId, ClassDefn),
 
 	polymorphism__get_arg_superclass_vars(ClassDefn, InstanceTypes,
-		SuperClassProofs, ArgSuperClassVars, SuperClassGoals, 
-		Info0, Info1),
+		SuperClassProofs, ExistQVars, ArgSuperClassVars,
+		SuperClassGoals, Info0, Info1),
 
 	Info1 = poly_info(VarSet0, VarTypes0, TVarSet, TVarMap, TCVarMap, 
 			Proofs, PredName, _),
@@ -1534,13 +1613,14 @@
 %---------------------------------------------------------------------------%
 
 :- pred polymorphism__get_arg_superclass_vars(hlds_class_defn, list(type),
-	map(class_constraint, constraint_proof), list(var), list(hlds_goal),
-	poly_info, poly_info).
-:- mode polymorphism__get_arg_superclass_vars(in, in, in, out, out, 
+	map(class_constraint, constraint_proof), existq_tvars,
+	list(var), list(hlds_goal), poly_info, poly_info).
+:- mode polymorphism__get_arg_superclass_vars(in, in, in, in, out, out, 
 	in, out) is det.
 
 polymorphism__get_arg_superclass_vars(ClassDefn, InstanceTypes, 
-		SuperClassProofs, NewVars, NewGoals, Info0, Info) :-
+		SuperClassProofs, ExistQVars, NewVars, NewGoals,
+		Info0, Info) :-
 
 	Info0 = poly_info(VarSet0, VarTypes0, TVarSet, TVarMap0, TCVarMap0, 
 			Proofs, PredName, ModuleInfo),
@@ -1554,7 +1634,8 @@
 			SuperClassProofs, PredName, ModuleInfo),
 
 	polymorphism__make_superclasses_from_proofs(SuperClasses, Subst,
-		TypeSubst, [], NewGoals, Info1, Info2, [], NewVars),
+		TypeSubst, ExistQVars, [], NewGoals, Info1, Info2,
+		[], NewVars),
 
 	Info2 = poly_info(VarSet, VarTypes, _, TVarMap, TCVarMap, _, _, _),
 
@@ -1563,19 +1644,21 @@
 
 
 :- pred polymorphism__make_superclasses_from_proofs(list(class_constraint), 
-	substitution, tsubst, list(hlds_goal), list(hlds_goal), 
+	substitution, tsubst, existq_tvars, list(hlds_goal), list(hlds_goal), 
 	poly_info, poly_info, list(var), list(var)).
-:- mode polymorphism__make_superclasses_from_proofs(in, in, in, in, out, 
+:- mode polymorphism__make_superclasses_from_proofs(in, in, in, in, in, out, 
 	in, out, in, out) is det.
 
-polymorphism__make_superclasses_from_proofs([], _, _, 
+polymorphism__make_superclasses_from_proofs([], _, _, _,
 		Goals, Goals, Info, Info, Vars, Vars).
-polymorphism__make_superclasses_from_proofs([C|Cs], Subst, TypeSubst, 
-		Goals0, Goals, Info0, Info, Vars0, Vars) :-
+polymorphism__make_superclasses_from_proofs([C|Cs], Subst, TypeSubst,
+		ExistQVars, Goals0, Goals, Info0, Info, Vars0, Vars) :-
 	polymorphism__make_superclasses_from_proofs(Cs, Subst, TypeSubst,
-		Goals0, Goals1, Info0, Info1, Vars0, Vars1),
+		ExistQVars, Goals0, Goals1, Info0, Info1, Vars0, Vars1),
+	term__context_init(Context),
 	polymorphism__make_typeclass_info_var(C, Subst, TypeSubst,
-		no, _, Goals1, Goals, [], _, Info1, Info, MaybeVar),
+		ExistQVars, Context, no, _, Goals1, Goals, [], _, Info1, Info,
+		MaybeVar),
 	maybe_insert_var(MaybeVar, Vars1, Vars).
 
 :- pred maybe_insert_var(maybe(var), list(var), list(var)).
@@ -1590,26 +1673,62 @@
 % variables to the appropriate type_info structures for the types.
 % Update the varset and vartypes accordingly.
 
-:- pred polymorphism__make_type_info_vars(list(type),
-	list(var), list(hlds_goal), poly_info, poly_info).
-:- mode polymorphism__make_type_info_vars(in, out, out, in, out) is det.
+:- pred polymorphism__make_type_info_vars(list(type), existq_tvars,
+	term__context, list(var), list(hlds_goal), poly_info, poly_info).
+:- mode polymorphism__make_type_info_vars(in, in, in, out, out, in, out) is det.
 
-polymorphism__make_type_info_vars([], [], [], Info, Info).
-polymorphism__make_type_info_vars([Type | Types], 
+polymorphism__make_type_info_vars([], _, _, [], [], Info, Info).
+polymorphism__make_type_info_vars([Type | Types], ExistQVars, Context,
 		ExtraVars, ExtraGoals, Info0, Info) :-
-	polymorphism__make_type_info_var(Type, 
+	polymorphism__make_type_info_var(Type, ExistQVars, Context,
 		Var, ExtraGoals1, Info0, Info1),
-	polymorphism__make_type_info_vars(Types, 
+	polymorphism__make_type_info_vars(Types, ExistQVars, Context,
 		ExtraVars2, ExtraGoals2, Info1, Info),
 	ExtraVars = [Var | ExtraVars2],
 	list__append(ExtraGoals1, ExtraGoals2, ExtraGoals).
 
-:- pred polymorphism__make_type_info_var(type, var, list(hlds_goal), 
-	poly_info, poly_info).
-:- mode polymorphism__make_type_info_var(in, out, out, in, out) is det.
+:- pred polymorphism__make_type_info_var(type, existq_tvars, term__context,
+		var, list(hlds_goal), poly_info, poly_info).
+:- mode polymorphism__make_type_info_var(in, in, in, out, out, in, out) is det.
 
-polymorphism__make_type_info_var(Type, Var, ExtraGoals, Info0, Info) :-
+polymorphism__make_type_info_var(Type, ExistQVars, Context, Var, ExtraGoals,
+		Info0, Info) :-
 	(
+		%
+		% Check for type variables which are existentially quantified
+		% in the callee's type declaration.
+		% For these type variables, we assume that the callee will
+		% return the type_info.  So all we need to do is to make
+		% a variable to hold the returned type_info, and insert
+		% that in the TypeInfoMap.
+		%
+		% [XXX This would need to change if we allow
+		% `in' modes for arguments with existential types,
+		% because in that case the mode for the type_info
+		% must also be `in', so we would need to construct it.
+		% The condition of the if-then-else below would
+		% need to be changed to fail for those cases]
+		%
+		Type = term__variable(TVar),
+		list__member(TVar, ExistQVars)
+	->
+		Info0 = poly_info(VarSet0, VarTypes0, C, TypeInfoMap0, 
+			E, F, G, H),
+		% existentially quantified tvars in the head will already
+		% have a type_info var allocated for them
+		( map__search(TypeInfoMap0, TVar, type_info(HeadVar)) ->
+			Var = HeadVar,
+			Info = Info0
+		;
+			polymorphism__new_type_info_var(Type, "type_info",
+				VarSet0, VarTypes0, Var, VarSet, VarTypes),
+			map__det_insert(TypeInfoMap0, TVar, type_info(Var),
+				TypeInfoMap),
+			Info = poly_info(VarSet, VarTypes, C, TypeInfoMap,
+				E, F, G, H)
+		),
+		ExtraGoals = []
+	;
 		type_is_higher_order(Type, PredOrFunc, TypeArgs)
 	->
 		% This occurs for code where a predicate calls a polymorphic
@@ -1625,7 +1744,8 @@
 		hlds_out__pred_or_func_to_str(PredOrFunc, PredOrFuncStr),
 		TypeId = unqualified(PredOrFuncStr) - 0,
 		polymorphism__construct_type_info(Type, TypeId, TypeArgs,
-			yes, Var, ExtraGoals, Info0, Info)
+			yes, ExistQVars, Context,
+			Var, ExtraGoals, Info0, Info)
 	;
 		type_to_type_id(Type, TypeId, TypeArgs)
 	->
@@ -1635,11 +1755,11 @@
 		% at the top of the module.
 
 		polymorphism__construct_type_info(Type, TypeId, TypeArgs,
-			no, Var, ExtraGoals, Info0, Info)
+			no, ExistQVars, Context, Var, ExtraGoals, Info0, Info)
 	;
-		Type = term__variable(TypeVar1),
+		Type = term__variable(TypeVar),
 		Info0 = poly_info(_, _, _, TypeInfoMap0, _, _, _, _),
-		map__search(TypeInfoMap0, TypeVar1, TypeInfoLocn)
+		map__search(TypeInfoMap0, TypeVar, TypeInfoLocn)
 	->
 		% This occurs for code where a predicate calls a polymorphic
 		% predicate with a bound but unknown value of the type variable.
@@ -1668,73 +1788,57 @@
 				% If the typeinfo is in a typeclass_info, first
 				% extract it, then use it
 			TypeInfoLocn = typeclass_info(TypeClassInfoVar, Index),
-			extract_type_info(Type, TypeVar1, TypeClassInfoVar,
+			extract_type_info(Type, TypeVar, TypeClassInfoVar,
 				Index, ExtraGoals, Var, Info0, Info)
 		)
 	;
-		Type = term__variable(_TypeVar1)
+		Type = term__variable(TypeVar)
 	->
-		% This occurs for code where a predicate calls a polymorphic
-		% predicate with an unbound type variable, for example
-		%
-		%	:- pred p.
-		%	:- pred q(list(T)).
-		%	p :- q([]).
-
-		% this case is now treated as an error;
-		% it should be caught by purity.m.
-		error("polymorphism__make_var: unbound type variable")
-/************
-This is what we used to do... but this didn't handle the case of type
-variables used by lambda expressions properly.
-Binding unbound type variables to `void' is now done in purity.m,
-because it is easier to do it correctly there.
-
-		% In this case T is unbound, so there cannot be any objects
-		% of type T, and so q/1 cannot possibly use the unification
-		% predicate for type T.  We pass the type-info for the
-		% type `void'/0.
-		%
-		%	:- pred p.
-		%	:- pred q(type_info(T), list(T)).
-		%	p :- q(<void/0>, []).
 		%
-		% Passing `void'/0 should ensure that we get a runtime
-		% error if the special predicates for this type are
-		% ever used (void has its special predicates set to
-		% `unused'/0).
+		% This occurs for code where a predicate calls a polymorphic
+		% predicate with an unbound type variable.
+		% Cases where there is no producer at all for the type
+		% variable should get caught by purity.m.
+		% XXX Cases where there is a producer but it occurs
+		% somewhere further on in the goal should be avoided by
+		% mode reordering, but currently mode analysis doesn't
+		% do that.
 		%
-		% XXX what about io__read_anything/3?
-		% e.g.
-		%	foo --> io__read_anything(_).
-		% ?
-
-		% introduce a new variable, and
-		% create a construction unification which initializes the
-		% variable to zero
-		TypeId = unqualified("void") - 0,
-		polymorphism__construct_type_info(Type, TypeId, [],
-			no, Var, ExtraGoals, Info0, Info1),
-		Info1 = poly_info(A, B, C, TypeInfoMap1, E, F, G, H),
-		map__det_insert(TypeInfoMap1, TypeVar1, type_info(Var),
-			TypeInfoMap),
-		Info = poly_info(A, B, C, TypeInfoMap, E, F, G, H)
-***************/
+		Info0 = poly_info(_VarSet, _VarTypes, TypeVarSet, _TypeVarMap,
+				_TypeClassVarMap, _Proofs, PredName,
+				_ModuleInfo),
+		varset__lookup_name(TypeVarSet, TypeVar, TypeVarName),
+		term__context_file(Context, FileName),
+		term__context_line(Context, LineNumber),
+		( FileName = "" ->
+			ContextMessage = ""
+		;
+			string__format("%s:%03d: ",
+				[s(FileName), i(LineNumber)], ContextMessage)
+		),
+		string__append_list([
+			"polymorphism__make_var:\n",
+			ContextMessage, "In predicate `", PredName, "':\n",
+			ContextMessage, "  unbound type variable `",
+				TypeVarName, "'."
+			], Message),
+		error(Message)
 	;
 		error("polymorphism__make_var: unknown type")
 	).
 
 :- pred polymorphism__construct_type_info(type, type_id, list(type),
-	bool, var, list(hlds_goal), poly_info, poly_info).
-:- mode polymorphism__construct_type_info(in, in, in, in, out, out, 
+	bool, existq_tvars, term__context, var, list(hlds_goal),
+	poly_info, poly_info).
+:- mode polymorphism__construct_type_info(in, in, in, in, in, in, out, out, 
 	in, out) is det.
 
 polymorphism__construct_type_info(Type, TypeId, TypeArgs, IsHigherOrder, 
-		Var, ExtraGoals, Info0, Info) :-
+		ExistQVars, Context, Var, ExtraGoals, Info0, Info) :-
 
 	% Create the typeinfo vars for the arguments
-	polymorphism__make_type_info_vars(TypeArgs, ArgTypeInfoVars, 
-		ArgTypeInfoGoals, Info0, Info1),
+	polymorphism__make_type_info_vars(TypeArgs, ExistQVars, Context,
+		ArgTypeInfoVars, ArgTypeInfoGoals, Info0, Info1),
 
 	Info1 = poly_info(VarSet1, VarTypes1, C, D, E, F, G, ModuleInfo),
 
Index: compiler/post_typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/post_typecheck.m,v
retrieving revision 1.1
diff -u -r1.1 post_typecheck.m
--- post_typecheck.m	1998/06/04 17:25:59	1.1
+++ post_typecheck.m	1998/06/04 16:17:08
@@ -89,12 +89,11 @@
 post_typecheck__check_type_bindings(PredId, PredInfo0, PredInfo, ModuleInfo,
 		NumErrors, IOState0, IOState) :-
 	pred_info_clauses_info(PredInfo0, ClausesInfo0),
+	pred_info_get_head_type_params(PredInfo0, HeadTypeParams),
 	ClausesInfo0 = clauses_info(VarSet, B, VarTypesMap0, HeadVars, E),
-	map__apply_to_list(HeadVars, VarTypesMap0, HeadVarTypes),
-	term__vars_list(HeadVarTypes, HeadVarTypeParams),
 	map__to_assoc_list(VarTypesMap0, VarTypesList),
 	set__init(Set0),
-	check_type_bindings_2(VarTypesList, HeadVarTypeParams,
+	check_type_bindings_2(VarTypesList, HeadTypeParams,
 			[], Errs, Set0, Set),
 	( Errs = [] ->
 		PredInfo = PredInfo0,
@@ -272,7 +271,7 @@
 	% 
 post_typecheck__finish_imported_pred(ModuleInfo, PredId, PredInfo0, PredInfo)
 		-->
-	{ pred_info_arg_types(PredInfo0, _, ArgTypes) },
+	{ pred_info_arg_types(PredInfo0, ArgTypes) },
 	{ pred_info_procedures(PredInfo0, Procs0) },
 	{ pred_info_procids(PredInfo0, ProcIds) },
 	propagate_types_into_proc_modes(ModuleInfo, PredId, ProcIds, ArgTypes,
Index: compiler/prog_data.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_data.m,v
retrieving revision 1.35
diff -u -r1.35 prog_data.m
--- prog_data.m	1998/05/15 07:07:31	1.35
+++ prog_data.m	1998/06/03 15:00:17
@@ -51,16 +51,20 @@
 	; 	mode_defn(varset, mode_defn, condition)
 	; 	module_defn(varset, module_defn)
 
-	; 	pred(varset, sym_name, list(type_and_mode),
+	; 	pred(tvarset, existq_tvars, sym_name, list(type_and_mode),
 			maybe(determinism), condition, purity,
 			list(class_constraint))
-		%     VarNames, PredName, ArgTypes, Deterministicness, Cond
+		%       VarNames, ExistentiallyQuantifiedTypeVars,
+		%	PredName, ArgTypes, Deterministicness, Cond,
+		%	Purity, TypeClassContext
 
-	; 	func(varset, sym_name, list(type_and_mode), type_and_mode,
-			maybe(determinism), condition, purity,
+	; 	func(tvarset, existq_tvars, sym_name, list(type_and_mode),
+			type_and_mode, maybe(determinism), condition, purity,
 			list(class_constraint))
-		%       VarNames, PredName, ArgTypes, ReturnType,
-		%       Deterministicness, Cond
+		%       VarNames, ExistentiallyQuantifiedTypeVars,
+		%       PredName, ArgTypes, ReturnType,
+		%       Deterministicness, Cond,
+		%	Purity, TypeClassContext
 
 	; 	pred_mode(varset, sym_name, list(mode), maybe(determinism),
 			condition)
@@ -243,37 +247,38 @@
 
 :- type class_interface  == list(class_method).	
 
-:- type class_method	--->	pred(varset, sym_name, list(type_and_mode),
-					maybe(determinism), condition,
-					list(class_constraint), term__context)
-				%       VarNames, PredName, ArgTypes,
-				%	Determinism, Cond
-				%	ClassContext, Context
-
-			; 	func(varset, sym_name, list(type_and_mode),
-					type_and_mode,
-					maybe(determinism), condition,
-					list(class_constraint), term__context)
-				%       VarNames, PredName, ArgTypes,
-				%	ReturnType,
-				%	Determinism, Cond
-				%	ClassContext, Context
-
-			; 	pred_mode(varset, sym_name, list(mode),
-					maybe(determinism), condition,
-					term__context)
-				%       VarNames, PredName, ArgModes,
-				%	Determinism, Cond
-				%	Context
-
-			; 	func_mode(varset, sym_name, list(mode), mode,
-					maybe(determinism), condition,
-					term__context)
-				%       VarNames, PredName, ArgModes,
-				%	ReturnValueMode,
-				%	Determinism, Cond
-				%	Context
-			.
+:- type class_method
+	--->	pred(tvarset, existq_tvars, sym_name, list(type_and_mode),
+			maybe(determinism), condition,
+			list(class_constraint), term__context)
+		%       VarNames, ExistentiallyQuantifiedTypeVars,
+		%	PredName, ArgTypes, Determinism, Cond
+		%	ClassContext, Context
+
+	; 	func(tvarset, existq_tvars, sym_name, list(type_and_mode),
+			type_and_mode,
+			maybe(determinism), condition,
+			list(class_constraint), term__context)
+		%       VarNames, ExistentiallyQuantfiedTypeVars,
+		%	PredName, ArgTypes, ReturnType,
+		%	Determinism, Cond
+		%	ClassContext, Context
+
+	; 	pred_mode(varset, sym_name, list(mode),
+			maybe(determinism), condition,
+			term__context)
+		%       VarNames, PredName, ArgModes,
+		%	Determinism, Cond
+		%	Context
+
+	; 	func_mode(varset, sym_name, list(mode), mode,
+			maybe(determinism), condition,
+			term__context)
+		%       VarNames, PredName, ArgModes,
+		%	ReturnValueMode,
+		%	Determinism, Cond
+		%	Context
+	.
 
 :- type instance_method	--->	func_instance(sym_name, sym_name, arity)
 			;	pred_instance(sym_name, sym_name, arity)
@@ -365,6 +370,10 @@
 :- type tvar		==	var.	% used for type variables
 :- type tvarset		==	varset. % used for sets of type variables
 :- type tsubst		==	map(tvar, type). % used for type substitutions
+
+	% existq_tvars is used to record the set of type variables which are
+	% existentially quantified
+:- type existq_tvars	==	list(tvar).
 
 	% Types may have arbitrary assertions associated with them
 	% (eg. you can define a type which represents sorted lists).
Index: compiler/prog_io.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io.m,v
retrieving revision 1.173
diff -u -r1.173 prog_io.m
--- prog_io.m	1998/05/30 12:25:45	1.173
+++ prog_io.m	1998/06/03 15:38:37
@@ -808,6 +808,36 @@
 		    Decl)
 	).
 
+process_decl(ModuleName, VarSet, "some", [TVars, Decl], Result) :-
+	% XXX we should check that `TVars' is of the
+	%     appropriate form (i.e. a list of variables)
+	term__vars(TVars, TVarsList),
+	parse_decl(ModuleName, VarSet, Decl, Result0),
+	(
+		Result0 = ok(pred(TVarSet, ExistQVars0, Name, ArgsAndModes,
+			Detism, Cond, Purity, ClassConstraints), _Context)
+	->
+		list__append(TVarsList, ExistQVars0, ExistQVars),
+		Result = ok(pred(TVarSet, ExistQVars, Name, ArgsAndModes,
+			Detism, Cond, Purity, ClassConstraints))
+	;
+		Result0 = ok(func(TVarSet, ExistQVars0, Name, ArgsAndModes,
+			RetArgAndMode, Detism, Cond, Purity, ClassConstraints),
+			_Context)
+	->
+		list__append(TVarsList, ExistQVars0, ExistQVars),
+		Result = ok(func(TVarSet, ExistQVars, Name, ArgsAndModes,
+			RetArgAndMode, Detism, Cond, Purity, ClassConstraints))
+	;
+		Result0 = error(Msg, Term)
+	->
+		Result = error(Msg, Term)
+	;
+		Result = error(
+	"Existential quantifiers only allowed on pred or func declarations", 
+		    Decl)
+	).
+
 process_decl(ModuleName, VarSet, "mode", [ModeDecl], Result) :-
 	parse_mode_decl(ModuleName, VarSet, ModeDecl, Result).
 
@@ -1460,8 +1490,9 @@
 		(
 			verify_type_and_mode_list(As)
 		->
-			Result = ok(pred(VarSet, F, As, MaybeDet, Cond,
-				Purity, ClassContext))
+			ExistQVars = [],
+			Result = ok(pred(VarSet, ExistQVars, F, As, MaybeDet,
+				Cond, Purity, ClassContext))
 		;
 			Result = error("some but not all arguments have modes", PredType)
 		)
@@ -1593,8 +1624,10 @@
 "function declaration specifies a determinism but does not specify the mode",
 					FuncTerm)
 			;
-				Result = ok(func(VarSet, F, As, ReturnType,
-					MaybeDet, Cond, Purity, ClassContext))
+				ExistQVars = [],
+				Result = ok(func(VarSet, ExistQVars, F, As,
+					ReturnType, MaybeDet, Cond, Purity,
+					ClassContext))
 			)
 		;
 			Result = error(
Index: compiler/prog_io_typeclass.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io_typeclass.m,v
retrieving revision 1.7
diff -u -r1.7 prog_io_typeclass.m
--- prog_io_typeclass.m	1998/04/08 15:23:30	1.7
+++ prog_io_typeclass.m	1998/06/03 14:09:08
@@ -213,14 +213,14 @@
 item_to_class_method(ok(Item, Context), Term, Result) :-
 	(
 			% XXX Purity is ignored
-		Item = pred(A, B, C, D, E, _, G)
+		Item = pred(A, B, C, D, E, F, _, H)
 	->
-		Result = ok(pred(A, B, C, D, E, G, Context))
+		Result = ok(pred(A, B, C, D, E, F, H, Context))
 	;
 			% XXX Purity is ignored
-		Item = func(A, B, C, D, E, F, _, H)
+		Item = func(A, B, C, D, E, F, G, _, I)
 	->
-		Result = ok(func(A, B, C, D, E, F, H, Context))
+		Result = ok(func(A, B, C, D, E, F, G, I, Context))
 	;
 		Item = pred_mode(A, B, C, D, E)
 	->
Index: compiler/stratify.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/stratify.m,v
retrieving revision 1.16
diff -u -r1.16 stratify.m
--- stratify.m	1998/05/15 07:07:36	1.16
+++ stratify.m	1998/06/03 14:09:50
@@ -646,7 +646,7 @@
 	module_info_pred_info(Module, PredId, PredInfo),
 	pred_info_non_imported_procids(PredInfo, Procs),
 	pred_info_procedures(PredInfo, ProcTable),
-	pred_info_arg_types(PredInfo, _TVarSet, ArgTypes),
+	pred_info_arg_types(PredInfo, ArgTypes),
 	process_procs(Procs, Module, PredId, ArgTypes, ProcTable, ProcCalls0, 
 		ProcCalls1, HOInfo0, HOInfo1, CallsHO0, CallsHO1), 
 	expand_predids(PredIds, Module, ProcCalls1, ProcCalls, HOInfo1, 
Index: compiler/switch_detection.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/switch_detection.m,v
retrieving revision 1.82
diff -u -r1.82 switch_detection.m
--- switch_detection.m	1998/05/15 07:07:38	1.82
+++ switch_detection.m	1998/06/01 14:00:37
@@ -222,7 +222,8 @@
 	(
 		instmap__lookup_var(InstMap, Var, VarInst0),
 		inst_is_bound(ModuleInfo, VarInst0),
-		partition_disj(Goals0, Var, GoalInfo, Left, CasesList)
+		partition_disj(Goals0, Var, GoalInfo, ModuleInfo,
+			Left, CasesList)
 	->
 		%
 		% A switch needs to have at least two cases.
@@ -352,25 +353,26 @@
 	% We partition the goals by abstractly interpreting the unifications
 	% at the start of each disjunction, to build up a substitution.
 
-:- pred partition_disj(list(hlds_goal), var, hlds_goal_info, list(hlds_goal),
-	sorted_case_list).
-:- mode partition_disj(in, in, in, out, out) is semidet.
+:- pred partition_disj(list(hlds_goal), var, hlds_goal_info, module_info,
+		list(hlds_goal), sorted_case_list).
+:- mode partition_disj(in, in, in, in, out, out) is semidet.
 
-partition_disj(Goals0, Var, GoalInfo, Left, CasesList) :-
+partition_disj(Goals0, Var, GoalInfo, ModuleInfo, Left, CasesList) :-
 	map__init(Cases0),
-	partition_disj_trial(Goals0, Var, [], Left, Cases0, Cases),
+	partition_disj_trial(Goals0, Var, [], ModuleInfo, Left, Cases0, Cases),
 	map__to_assoc_list(Cases, CasesAssocList),
 	CasesAssocList \= [], % there must be at least one case
 	fix_case_list(CasesAssocList, GoalInfo, CasesList).
 
 :- pred partition_disj_trial(list(hlds_goal), var,
-	list(hlds_goal), list(hlds_goal), cases, cases).
-:- mode partition_disj_trial(in, in, in, out, in, out) is det.
+	list(hlds_goal), module_info, list(hlds_goal), cases, cases).
+:- mode partition_disj_trial(in, in, in, in, out, in, out) is det.
 
-partition_disj_trial([], _Var, Left, Left, Cases, Cases).
-partition_disj_trial([Goal0 | Goals], Var, Left0, Left, Cases0, Cases) :-
+partition_disj_trial([], _Var, Left, _, Left, Cases, Cases).
+partition_disj_trial([Goal0 | Goals], Var, Left0, ModuleInfo, Left,
+		Cases0, Cases) :-
 	map__init(Substitution),
-	find_bind_var_for_switch(Goal0, Substitution, Var,
+	find_bind_var_for_switch(Goal0, Substitution, Var, ModuleInfo,
 			Goal, _NewSubstitution, MaybeFunctor),
 	(
 		MaybeFunctor = yes(Functor),
@@ -387,10 +389,11 @@
 		Left1 = [Goal0 | Left0],
 		Cases1 = Cases0
 	),
-	partition_disj_trial(Goals, Var, Left1, Left, Cases1, Cases).
+	partition_disj_trial(Goals, Var, Left1, ModuleInfo, Left,
+		Cases1, Cases).
 
-	% find_bind_var_for_switch(Goal0, Subst0, Var, Goal, Subst,
-	%		MaybeFunctor):
+	% find_bind_var_for_switch(Goal0, Subst0, Var, ModuleInfo,
+	%		Goal, Subst, MaybeFunctor):
 	% conj_find_bind_var_for_switch(Goals0, Subst0, Var, Goals, Subst,
 	%		MaybeFunctor):
 	%	Searches through Goals0 looking for a deconstruction
@@ -403,18 +406,18 @@
 	%	resulting substitution from interpreting through the goal.
 
 :- pred find_bind_var_for_switch(hlds_goal, substitution, var,
-	hlds_goal, substitution, maybe(cons_id)).
-:- mode find_bind_var_for_switch(in, in, in, out, out, out) is det.
+	module_info, hlds_goal, substitution, maybe(cons_id)).
+:- mode find_bind_var_for_switch(in, in, in, in, out, out, out) is det.
 
-find_bind_var_for_switch(Goal0 - GoalInfo, Substitution0, Var,
+find_bind_var_for_switch(Goal0 - GoalInfo, Substitution0, Var, ModuleInfo,
 		Goal - GoalInfo, Substitution, MaybeFunctor) :-
 	( Goal0 = some(Vars, SubGoal0) ->
 		find_bind_var_for_switch(SubGoal0, Substitution0, Var,
-			SubGoal, Substitution, MaybeFunctor),
+			ModuleInfo, SubGoal, Substitution, MaybeFunctor),
 		Goal = some(Vars, SubGoal)
 	; Goal0 = conj(SubGoals0) ->
 		conj_find_bind_var_for_switch(SubGoals0, Substitution0, Var,
-			SubGoals, Substitution, MaybeFunctor),
+			ModuleInfo, SubGoals, Substitution, MaybeFunctor),
 		Goal = conj(SubGoals)
 	; Goal0 = unify(A, B, C, UnifyInfo0, E) ->
 			% check whether the unification is a deconstruction
@@ -453,22 +456,32 @@
 	).
 
 :- pred conj_find_bind_var_for_switch(list(hlds_goal), substitution, var,
-	list(hlds_goal), substitution, maybe(cons_id)).
-:- mode conj_find_bind_var_for_switch(in, in, in, out, out, out) is det.
+	module_info, list(hlds_goal), substitution, maybe(cons_id)).
+:- mode conj_find_bind_var_for_switch(in, in, in, in, out, out, out) is det.
 
-conj_find_bind_var_for_switch([], Substitution, _Var, [], Substitution, no).
-conj_find_bind_var_for_switch([Goal0 | Goals0], Substitution0, Var,
+conj_find_bind_var_for_switch([], Substitution, _Var, _ModuleInfo,
+			[], Substitution, no).
+conj_find_bind_var_for_switch([Goal0 | Goals0], Substitution0, Var, ModuleInfo,
 		[Goal | Goals], Substitution, MaybeFunctor) :-
-	find_bind_var_for_switch(Goal0,
-		Substitution0, Var,
+	find_bind_var_for_switch(Goal0, Substitution0, Var, ModuleInfo,
 		Goal, Substitution1, MaybeFunctor1),
 	( MaybeFunctor1 = yes(_) ->
 		Goals = Goals0,
 		Substitution = Substitution1,
 		MaybeFunctor = MaybeFunctor1
 	;
+		% stop search at predicate calls (but not function calls)
+		Goal0 = call(PredId, _, _, _, _, _) - _,
+		module_info_pred_info(ModuleInfo, PredId, PredInfo),
+		pred_info_get_is_pred_or_func(PredInfo, IsPredOrFunc),
+		IsPredOrFunc = predicate
+	->
+		Goals = Goals0,
+		Substitution = Substitution1,
+		MaybeFunctor = no
+	;
 		conj_find_bind_var_for_switch(Goals0, Substitution1, Var,
-			Goals, Substitution, MaybeFunctor)
+			ModuleInfo, Goals, Substitution, MaybeFunctor)
 	).
 
 :- pred cases_to_switch(sorted_case_list, var, map(var, type), hlds_goal_info,
Index: compiler/termination.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/termination.m,v
retrieving revision 1.12
diff -u -r1.12 termination.m
--- termination.m	1998/05/25 21:48:56	1.12
+++ termination.m	1998/06/03 14:09:56
@@ -566,7 +566,7 @@
 :- mode all_args_input_or_zero_size(in, in, in) is semidet.
 
 all_args_input_or_zero_size(Module, PredInfo, ProcInfo) :-
-	pred_info_arg_types(PredInfo, _, TypeList),
+	pred_info_arg_types(PredInfo, TypeList),
 	proc_info_argmodes(ProcInfo, ModeList),
 	all_args_input_or_zero_size_2(TypeList, ModeList, Module). 
 
Index: compiler/type_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/type_util.m,v
retrieving revision 1.54
diff -u -r1.54 type_util.m
--- type_util.m	1998/05/25 21:48:57	1.54
+++ type_util.m	1998/06/03 15:18:11
@@ -182,6 +182,11 @@
 	class_constraint).
 :- mode apply_subst_to_constraint(in, in, out) is det.
 
+% Apply a renaming (partial map) to a list.
+% Useful for applying a variable renaming to a list of variables.
+:- pred apply_partial_map_to_list(list(T), map(T, T), list(T)).
+:- mode apply_partial_map_to_list(in, in, out) is det.
+
 % strip out the term__context fields, replacing them with empty
 % term__contexts (as obtained by term__context_init/1)
 % in a type or list of types
@@ -745,6 +750,19 @@
 	Constraint0 = constraint(ClassName, Types0),
 	term__apply_substitution_to_list(Types0, Subst, Types),
 	Constraint  = constraint(ClassName, Types).
+
+%-----------------------------------------------------------------------------%
+
+apply_partial_map_to_list([], _PartialMap, []).
+apply_partial_map_to_list([X|Xs], PartialMap, [Y|Ys]) :-
+	( map__search(PartialMap, X, Y0) ->
+		Y = Y0
+	;
+		Y = X
+	),
+	apply_partial_map_to_list(Xs, PartialMap, Ys).
+
+%-----------------------------------------------------------------------------%
 
 strip_term_contexts(Terms, StrippedTerms) :-
 	list__map(strip_term_context, Terms, StrippedTerms).
Index: compiler/typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
retrieving revision 1.240
diff -u -r1.240 typecheck.m
--- typecheck.m	1998/06/04 17:26:08	1.240
+++ typecheck.m	1998/06/04 18:07:29
@@ -317,7 +317,8 @@
 	    Changed = no,
 	    IOState = IOState0
 	;
-	    pred_info_arg_types(PredInfo0, _ArgTypeVarSet, ArgTypes0),
+	    pred_info_arg_types(PredInfo0, _ArgTypeVarSet, ExistQVars0,
+		    ArgTypes0),
 	    pred_info_typevarset(PredInfo0, TypeVarSet0),
 	    pred_info_clauses_info(PredInfo0, ClausesInfo0),
 	    pred_info_import_status(PredInfo0, Status),
@@ -334,7 +335,7 @@
 			IOState = IOState0,
 				% For the moment, we just insert the types
 				% of the head vars into the clauses_info
-			pred_info_arg_types(PredInfo0, _, ArgTypes),
+			pred_info_arg_types(PredInfo0, ArgTypes),
 			map__from_corresponding_lists(HeadVars, ArgTypes,
 				VarTypes),
 			ClausesInfo = clauses_info(VarSet, VarTypes,
@@ -358,13 +359,15 @@
 			% initial type declaration of 
 			% `pred foo(T1, T2, ..., TN)' by make_hlds.m.
 			Inferring = yes,
-			HeadTypeParams = [],
+			HeadTypeParams1 = [],
 			Constraints = [],
 			write_pred_progress_message("% Inferring type of ",
 				PredId, ModuleInfo, IOState0, IOState1)
 		;
 			Inferring = no,
-			term__vars_list(ArgTypes0, HeadTypeParams),
+			term__vars_list(ArgTypes0, HeadTypeParams0),
+			list__delete_elems(HeadTypeParams0, ExistQVars0,
+				HeadTypeParams1),
 			pred_info_get_class_context(PredInfo0, Constraints),
 			write_pred_progress_message("% Type-checking ",
 				PredId, ModuleInfo, IOState0, IOState1)
@@ -372,7 +375,7 @@
 
 		typecheck_info_init(IOState1, ModuleInfo, PredId,
 				TypeVarSet0, VarSet, ExplicitVarTypes,
-				HeadTypeParams, Constraints, Status,
+				HeadTypeParams1, Constraints, Status,
 				TypeCheckInfo1),
 		typecheck_info_get_type_assign_set(TypeCheckInfo1,
 				OrigTypeAssignSet),
@@ -387,7 +390,7 @@
 		typecheck_check_for_ambiguity(whole_pred, HeadVars,
 				TypeCheckInfo4, TypeCheckInfo5),
 		typecheck_info_get_final_info(TypeCheckInfo5, Constraints,
-				TypeVarSet, InferredVarTypes0,
+				TypeVarSet, HeadTypeParams2, InferredVarTypes0,
 				InferredTypeConstraints, RenamedOldConstraints,
 				ConstraintProofs),
 		map__optimize(InferredVarTypes0, InferredVarTypes),
@@ -398,16 +401,55 @@
 		pred_info_set_constraint_proofs(PredInfo2, ConstraintProofs,
 			PredInfo3),
 		map__apply_to_list(HeadVars, InferredVarTypes, ArgTypes),
-		pred_info_set_arg_types(PredInfo3, TypeVarSet,
-				ArgTypes, PredInfo4),
+		( Inferring = yes ->
+			%
+			% Now we need to infer which of the head variable
+			% types must be existentially quantified:
+			% anything that was inserted into the HeadTypeParams2
+			% set must have been inserted due to an existential
+			% type in something we called, and thus must be
+			% existentially quantified.
+			% (In theory, we could also infer more variables as
+			% being existentially typed, but we try to infer
+			% universally quantified types or concrete
+			% types in preference to existentially quantified
+			% types.)
+			%
+			term__vars_list(ArgTypes, ArgTypeVars),
+			set__list_to_set(ArgTypeVars, ArgTypeVarsSet),
+			set__list_to_set(HeadTypeParams2, HeadTypeParamsSet),
+			set__intersect(ArgTypeVarsSet, HeadTypeParamsSet,
+				ExistQVarsSet),
+			set__to_sorted_list(ExistQVarsSet, ExistQVars),
+			%
+			% Then we need to insert the universally
+			% quantified head variable types into the
+			% HeadTypeParams set, and delete the
+			% existentially quantified ones.
+			% This is needed so that it has the right
+			% value when post_typecheck.m uses it to
+			% check for unbound type variables.
+			%
+			list__append(ArgTypeVars, HeadTypeParams2,
+				HeadTypeParams3),
+			list__delete_elems(HeadTypeParams3, ExistQVars,
+				HeadTypeParams)
+		;
+			ExistQVars = ExistQVars0,
+			HeadTypeParams = HeadTypeParams2
+		),
+		pred_info_set_head_type_params(PredInfo3, HeadTypeParams,
+			PredInfo4),
+		pred_info_set_arg_types(PredInfo4, TypeVarSet, ExistQVars,
+				ArgTypes, PredInfo5),
 		( Inferring = no ->
-			pred_info_set_class_context(PredInfo4,
+			pred_info_set_class_context(PredInfo5,
 				RenamedOldConstraints, PredInfo),
 			Changed = no
 		;
 			pred_info_get_class_context(PredInfo0,
 				OldTypeConstraints),
-			pred_info_set_class_context(PredInfo4,
+			pred_info_set_class_context(PredInfo5,
 				InferredTypeConstraints, PredInfo),
 			(
 				% If the argument types and the type
@@ -486,7 +528,7 @@
 	% and check whether that type is a type for which there is
 	% a user-defined equality predicate.
 	%
-	pred_info_arg_types(PredInfo, _TypeVarSet, ArgTypes),
+	pred_info_arg_types(PredInfo, ArgTypes),
 	special_pred_get_type(PredName, ArgTypes, Type),
 	type_to_type_id(Type, TypeId, _TypeArgs),
 	module_info_types(ModuleInfo, TypeTable),
@@ -711,9 +753,13 @@
 	typecheck_unification(A, B0, B).
 typecheck_goal_2(switch(_, _, _, _), _) -->
 	{ error("unexpected switch") }.
-% no need to typecheck pragmas
-typecheck_goal_2(pragma_c_code(A,B,C,D,E,F,G), pragma_c_code(A,B,C,D,E,F,G))
-	--> []. 
+typecheck_goal_2(pragma_c_code(A, PredId, C, Args, E, F, G), 
+		pragma_c_code(A, PredId, C, Args, E, F, G)) -->
+	% pragma_c_codes are automatically generated, so they
+	% will always be type-correct, but we need to do
+	% the type analysis in order to correctly compute the
+	% HeadTypeParams that result from existentially typed pragma_c_codes.
+	typecheck_call_pred_id(PredId, Args).
 
 %-----------------------------------------------------------------------------%
 
@@ -747,8 +793,8 @@
 		{ varset__new_vars(TypeVarSet0, NumVars,
 			TypeVars, TypeVarSet) },
 		{ term__var_list_to_term_list(TypeVars, Types) },
-		typecheck_var_has_polymorphic_type_list(Vars,
-			TypeVarSet, Types, [])
+		typecheck_var_has_polymorphic_type_list(Vars, TypeVarSet, [],
+			Types, [])
 	).
 
 %-----------------------------------------------------------------------------%
@@ -765,10 +811,11 @@
 	{ PredCallId = unqualified("call")/Arity1 },
 	typecheck_info_set_called_predid(PredCallId),
 		% The class context is empty because higher-order predicates
-		% are always monomorphic.
+		% are always monomorphic.  Similarly for ExistQVars.
 	{ ClassContext = [] },
+	{ ExistQVars = [] },
 	typecheck_var_has_polymorphic_type_list([PredVar|Args], TypeVarSet,
-		[PredVarType|ArgTypes], ClassContext).
+		ExistQVars, [PredVarType|ArgTypes], ClassContext).
 
 :- pred higher_order_pred_type(int, tvarset, type, list(type)).
 :- mode higher_order_pred_type(in, out, out, out) is det.
@@ -832,39 +879,9 @@
 		% (so that we can optimize the case of a non-overloaded,
 		% non-polymorphic predicate)
 		( PredIdList = [PredId0] ->
-			
 			PredId = PredId0,
-			predicate_table_get_preds(PredicateTable, Preds),
-			map__lookup(Preds, PredId, PredInfo),
-			pred_info_arg_types(PredInfo, PredTypeVarSet,
-						PredArgTypes),
-			pred_info_get_class_context(PredInfo,
-						PredClassContext),
-
-				% rename apart the type variables in 
-				% called predicate's arg types and then 
-				% unify the types of the call arguments
-				% with the called predicates' arg types
-				% (optimize for the common case of
-				% a non-polymorphic predicate)
-			( varset__is_empty(PredTypeVarSet) ->
-			    typecheck_var_has_type_list(Args,
-				PredArgTypes, 0, TypeCheckInfo1,
-				TypeCheckInfo2),
-			    ( 
-					% sanity check
-			        PredClassContext \= []
-			    ->
-			        error("non-polymorphic pred has class context")
-			    ;
-			    	true
-			    )
-			;
-			    typecheck_var_has_polymorphic_type_list(
-				Args, PredTypeVarSet, PredArgTypes,
-				PredClassContext,
+			typecheck_call_pred_id(PredId, Args,
 				TypeCheckInfo1, TypeCheckInfo2)
-			)
 		;
 			typecheck_info_get_pred_import_status(TypeCheckInfo1,
 						CallingStatus),
@@ -899,6 +916,45 @@
 				PredicateTable, PredCallId, TypeCheckInfo)
 	).
 
+:- pred typecheck_call_pred_id(pred_id, list(var), 
+				typecheck_info, typecheck_info).
+:- mode typecheck_call_pred_id(in, in, typecheck_info_di, 
+				typecheck_info_uo) is det.
+
+typecheck_call_pred_id(PredId, Args, TypeCheckInfo0, TypeCheckInfo) :-
+	typecheck_info_get_module_info(TypeCheckInfo0, ModuleInfo),
+	module_info_get_predicate_table(ModuleInfo, PredicateTable),
+	predicate_table_get_preds(PredicateTable, Preds),
+	map__lookup(Preds, PredId, PredInfo),
+	pred_info_arg_types(PredInfo, PredTypeVarSet, PredExistQVars,
+			PredArgTypes),
+	pred_info_get_class_context(PredInfo, PredClassContext),
+	%
+	% rename apart the type variables in 
+	% called predicate's arg types and then 
+	% unify the types of the call arguments
+	% with the called predicates' arg types
+	% (optimize for the common case of
+	% a non-polymorphic predicate)
+	%
+	( varset__is_empty(PredTypeVarSet) ->
+		typecheck_var_has_type_list(Args,
+			PredArgTypes, 0, TypeCheckInfo0,
+			TypeCheckInfo),
+		( 
+			% sanity check
+			PredClassContext \= []
+		->
+			error("non-polymorphic pred has class context")
+		;
+			true
+		)
+	;
+		typecheck_var_has_polymorphic_type_list(Args,
+			PredTypeVarSet, PredExistQVars, PredArgTypes,
+			PredClassContext, TypeCheckInfo0, TypeCheckInfo)
+	).
+
 :- pred report_pred_call_error(typecheck_info, module_info, predicate_table, 
 			pred_call_id, typecheck_info).
 :- mode report_pred_call_error(typecheck_info_di, in, in,
@@ -975,10 +1031,12 @@
 get_overloaded_pred_arg_types([PredId | PredIds], Preds, CallingPredStatus,
 		TypeAssignSet0, ArgsTypeAssignSet0, ArgsTypeAssignSet) :-
 	map__lookup(Preds, PredId, PredInfo),
-	pred_info_arg_types(PredInfo, PredTypeVarSet, PredArgTypes),
+	pred_info_arg_types(PredInfo, PredTypeVarSet, PredExistQVars,
+		PredArgTypes),
 	pred_info_get_class_context(PredInfo, PredClassContext),
-	rename_apart(TypeAssignSet0, PredTypeVarSet, PredArgTypes,
-		PredClassContext, ArgsTypeAssignSet0, ArgsTypeAssignSet1),
+	rename_apart(TypeAssignSet0, PredTypeVarSet, PredExistQVars,
+		PredArgTypes, PredClassContext,
+		ArgsTypeAssignSet0, ArgsTypeAssignSet1),
 	get_overloaded_pred_arg_types(PredIds, Preds, CallingPredStatus,
 		TypeAssignSet0, ArgsTypeAssignSet1, ArgsTypeAssignSet).
 
@@ -1027,7 +1085,8 @@
 		% (or the argument types + return type of the candidate
 		% function)
 		%
-		pred_info_arg_types(PredInfo, PredTVarSet, PredArgTypes0),
+		pred_info_arg_types(PredInfo, PredTVarSet, _PredExistQVars0,
+			PredArgTypes0),
 
 		%
 		% rename them apart from the actual argument types
@@ -1035,10 +1094,14 @@
 		varset__merge_subst(TVarSet, PredTVarSet, _TVarSet1, Subst),
 		term__apply_substitution_to_list(PredArgTypes0, Subst,
 					PredArgTypes),
+		% apply_partial_map_to_list(_PredExistQVars0, Subst,
+		% 			_PredExistQVars),
 
 		%
 		% check that the types of the candidate predicate/function
 		% subsume the actual argument types
+		% (XXX what about existential types?  Do we need to
+		% do something with _PredExistQVars0 here?)
 		%
 		type_list_subsumes(PredArgTypes, ArgTypes, _TypeSubst)
 	->
@@ -1074,35 +1137,58 @@
 	% A set of class constraints are also passed in, which must have the
 	% types contained within renamed apart. 
 
-:- pred typecheck_var_has_polymorphic_type_list(list(var), tvarset, list(type),
-		list(class_constraint), typecheck_info, typecheck_info).
-:- mode typecheck_var_has_polymorphic_type_list(in, in, in, in,
+:- pred typecheck_var_has_polymorphic_type_list(list(var),
+		tvarset, existq_tvars, list(type), list(class_constraint),
+		typecheck_info, typecheck_info).
+:- mode typecheck_var_has_polymorphic_type_list(in, in, in, in, in,
 		typecheck_info_di, typecheck_info_uo) is det.
 
-typecheck_var_has_polymorphic_type_list(Args, PredTypeVarSet, PredArgTypes,
-		PredClassConstraints, TypeCheckInfo0, TypeCheckInfo) :-
+typecheck_var_has_polymorphic_type_list(Args, PredTypeVarSet, PredExistQVars,
+		PredArgTypes, PredClassConstraints,
+		TypeCheckInfo0, TypeCheckInfo) :-
 	typecheck_info_get_type_assign_set(TypeCheckInfo0, TypeAssignSet0),
-	rename_apart(TypeAssignSet0, PredTypeVarSet, PredArgTypes,
-				PredClassConstraints, [], ArgsTypeAssignSet),
+	rename_apart(TypeAssignSet0, PredTypeVarSet, PredExistQVars,
+				PredArgTypes, PredClassConstraints,
+				[], ArgsTypeAssignSet),
 	typecheck_var_has_arg_type_list(Args, 0, ArgsTypeAssignSet,
 				TypeCheckInfo0, TypeCheckInfo).
 
-:- pred rename_apart(type_assign_set, tvarset, list(type),
+:- pred rename_apart(type_assign_set, tvarset, existq_tvars, list(type),
 			list(class_constraint),
                         args_type_assign_set, args_type_assign_set).
-:- mode rename_apart(in, in, in, in, in, out) is det.
+:- mode rename_apart(in, in, in, in, in, in, out) is det.
 
-rename_apart([], _, _, _, ArgTypeAssigns, ArgTypeAssigns).
-rename_apart([TypeAssign0 | TypeAssigns0], PredTypeVarSet, PredArgTypes0,
-		PredClassConstraints0, ArgTypeAssigns0, ArgTypeAssigns) :-
+rename_apart([], _, _, _, _, ArgTypeAssigns, ArgTypeAssigns).
+rename_apart([TypeAssign0 | TypeAssigns0], PredTypeVarSet, PredExistQVars0,
+		PredArgTypes0, PredClassConstraints0,
+		ArgTypeAssigns0, ArgTypeAssigns) :-
+	%
+	% rename everything apart
+	%
         type_assign_rename_apart(TypeAssign0, PredTypeVarSet, PredArgTypes0,
-                        TypeAssign, PredArgTypes, Subst),
+                        TypeAssign1, PredArgTypes, Subst),
+	apply_substitution_to_var_list(PredExistQVars0, Subst, PredExistQVars),
 	apply_subst_to_constraints(Subst, PredClassConstraints0,
-		PredClassConstraints),
-	NewArgTypeAssign = args(TypeAssign, PredArgTypes, PredClassConstraints),
+			PredClassConstraints),
+
+	%
+	% insert the existentially quantified type variables for the called
+	% predicate into HeadTypeParams (which holds the set of type
+	% variables which the caller is not allowed to bind).
+	%
+	type_assign_get_head_type_params(TypeAssign1, HeadTypeParams0),
+	list__append(PredExistQVars, HeadTypeParams0, HeadTypeParams),
+	type_assign_set_head_type_params(TypeAssign1, HeadTypeParams,
+			TypeAssign),
+	%
+	% save the results and recurse
+	%
+	NewArgTypeAssign = args(TypeAssign, PredArgTypes,
+			PredClassConstraints),
         ArgTypeAssigns1 = [NewArgTypeAssign | ArgTypeAssigns0],
-        rename_apart(TypeAssigns0, PredTypeVarSet, PredArgTypes0,
-			PredClassConstraints0, ArgTypeAssigns1, ArgTypeAssigns).
+        rename_apart(TypeAssigns0, PredTypeVarSet, PredExistQVars0,
+			PredArgTypes0, PredClassConstraints0,
+			ArgTypeAssigns1, ArgTypeAssigns).
 
 :- pred type_assign_rename_apart(type_assign, tvarset, list(type),
 			type_assign, list(type), substitution).
@@ -1185,8 +1271,7 @@
 
 typecheck_var_has_arg_type(VarId, ArgTypeAssignSet0, ArgTypeAssignSet,
 				TypeCheckInfo0, TypeCheckInfo) :-
-	typecheck_info_get_head_type_params(TypeCheckInfo0, HeadTypeParams),
-	typecheck_var_has_arg_type_2(ArgTypeAssignSet0, HeadTypeParams,
+	typecheck_var_has_arg_type_2(ArgTypeAssignSet0,
 				VarId, [], ArgTypeAssignSet1),
 	(
 		ArgTypeAssignSet1 = [],
@@ -1219,24 +1304,24 @@
 	),
 	skip_arg(ArgTypeAssigns0, ArgTypeAssigns).
 
-:- pred typecheck_var_has_arg_type_2(args_type_assign_set, headtypes, var,
+:- pred typecheck_var_has_arg_type_2(args_type_assign_set, var,
 				args_type_assign_set, args_type_assign_set).
-:- mode typecheck_var_has_arg_type_2(in, in, in, in, out) is det.
+:- mode typecheck_var_has_arg_type_2(in, in, in, out) is det.
 
-typecheck_var_has_arg_type_2([], _, _) --> [].
+typecheck_var_has_arg_type_2([], _) --> [].
 typecheck_var_has_arg_type_2(
 		[args(TypeAssign0, ArgTypes0, ClassContext) | TypeAssignSet0],
-		HeadTypeParams, VarId) -->
+		VarId) -->
 	arg_type_assign_var_has_type(TypeAssign0, ArgTypes0,
-					HeadTypeParams, VarId, ClassContext),
-	typecheck_var_has_arg_type_2(TypeAssignSet0, HeadTypeParams, VarId).
+					VarId, ClassContext),
+	typecheck_var_has_arg_type_2(TypeAssignSet0, VarId).
 
-:- pred arg_type_assign_var_has_type(type_assign, list(type), headtypes, var,
+:- pred arg_type_assign_var_has_type(type_assign, list(type), var,
 				list(class_constraint),
 				args_type_assign_set, args_type_assign_set).
-:- mode arg_type_assign_var_has_type(in, in, in, in, in, in, out) is det.
+:- mode arg_type_assign_var_has_type(in, in, in, in, in, out) is det.
 
-arg_type_assign_var_has_type(TypeAssign0, ArgTypes0, HeadTypeParams, VarId,
+arg_type_assign_var_has_type(TypeAssign0, ArgTypes0, VarId,
 		ClassContext, ArgTypeAssignSet0, ArgTypeAssignSet) :-
 	type_assign_get_var_types(TypeAssign0, VarTypes0),
 	( ArgTypes0 = [Type | ArgTypes] ->
@@ -1244,7 +1329,7 @@
 		map__search(VarTypes0, VarId, VarType)
 	    ->
 		(
-		    type_assign_unify_type(TypeAssign0, HeadTypeParams,
+		    type_assign_unify_type(TypeAssign0,
 				VarType, Type, TypeAssign1)
 		->
 		    ArgTypeAssignSet = 
@@ -1290,8 +1375,7 @@
 
 typecheck_var_has_type(VarId, Type, TypeCheckInfo0, TypeCheckInfo) :-
 	typecheck_info_get_type_assign_set(TypeCheckInfo0, TypeAssignSet0),
-	typecheck_info_get_head_type_params(TypeCheckInfo0, HeadTypeParams),
-	typecheck_var_has_type_2(TypeAssignSet0, HeadTypeParams, VarId, Type,
+	typecheck_var_has_type_2(TypeAssignSet0, VarId, Type,
 			[], TypeAssignSet),
 	(
 		TypeAssignSet = [],
@@ -1382,28 +1466,28 @@
 
 :- type headtypes == list(tvar).
 
-:- pred typecheck_var_has_type_2(type_assign_set, headtypes, var, type,
+:- pred typecheck_var_has_type_2(type_assign_set, var, type,
 				type_assign_set, type_assign_set).
-:- mode typecheck_var_has_type_2(in, in, in, in, in, out) is det.
+:- mode typecheck_var_has_type_2(in, in, in, in, out) is det.
 
-typecheck_var_has_type_2([], _, _, _) --> [].
-typecheck_var_has_type_2([TypeAssign0 | TypeAssignSet0], HeadTypeParams, VarId,
+typecheck_var_has_type_2([], _, _) --> [].
+typecheck_var_has_type_2([TypeAssign0 | TypeAssignSet0], VarId,
 		Type) -->
-	type_assign_var_has_type(TypeAssign0, HeadTypeParams, VarId, Type),
-	typecheck_var_has_type_2(TypeAssignSet0, HeadTypeParams, VarId, Type).
+	type_assign_var_has_type(TypeAssign0, VarId, Type),
+	typecheck_var_has_type_2(TypeAssignSet0, VarId, Type).
 
-:- pred type_assign_var_has_type(type_assign, headtypes, var, type,
+:- pred type_assign_var_has_type(type_assign, var, type,
 				type_assign_set, type_assign_set).
-:- mode type_assign_var_has_type(in, in, in, in, in, out) is det.
+:- mode type_assign_var_has_type(in, in, in, in, out) is det.
 
-type_assign_var_has_type(TypeAssign0, HeadTypeParams, VarId, Type,
+type_assign_var_has_type(TypeAssign0, VarId, Type,
 		TypeAssignSet0, TypeAssignSet) :-
 	type_assign_get_var_types(TypeAssign0, VarTypes0),
 	( %%% if some [VarType]
 		map__search(VarTypes0, VarId, VarType)
 	->
 		( %%% if some [TypeAssign1]
-			type_assign_unify_type(TypeAssign0, HeadTypeParams,
+			type_assign_unify_type(TypeAssign0,
 				VarType, Type, TypeAssign1)
 		->
 			TypeAssignSet = [TypeAssign1 | TypeAssignSet0]
@@ -1438,9 +1522,7 @@
 		TypeAssignSet, [TypeAssign|TypeAssignSet]).
 type_assign_var_has_type_list([Arg | Args], [Type | Types], TypeAssign0,
 		TypeCheckInfo, TypeAssignSet0, TypeAssignSet) :-
-	typecheck_info_get_head_type_params(TypeCheckInfo, HeadTypeParams),
-	type_assign_var_has_type(TypeAssign0, HeadTypeParams, Arg, Type,
-		[], TypeAssignSet1),
+	type_assign_var_has_type(TypeAssign0, Arg, Type, [], TypeAssignSet1),
 	type_assign_list_var_has_type_list(TypeAssignSet1,
 		Args, Types, TypeCheckInfo, TypeAssignSet0, TypeAssignSet).
 
@@ -1579,8 +1661,7 @@
 
 typecheck_unify_var_var(X, Y, TypeCheckInfo0, TypeCheckInfo) :-
 	typecheck_info_get_type_assign_set(TypeCheckInfo0, TypeAssignSet0),
-	typecheck_unify_var_var_2(TypeAssignSet0, X, Y, TypeCheckInfo0,
-			[], TypeAssignSet),
+	typecheck_unify_var_var_2(TypeAssignSet0, X, Y, [], TypeAssignSet),
 	( TypeAssignSet = [], TypeAssignSet0 \= [] ->
 		typecheck_info_get_io_state(TypeCheckInfo0, IOState0),
 		report_error_unif_var_var(TypeCheckInfo0, X, Y, TypeAssignSet0,
@@ -1637,8 +1718,8 @@
 		% check that the type of the functor matches the type
 		% of the variable
 		%
-		typecheck_functor_type( ConsTypeAssignSet, Var,
-			TypeCheckInfo0, [], ArgsTypeAssignSet),
+		typecheck_functor_type(ConsTypeAssignSet, Var,
+			[], ArgsTypeAssignSet),
 		( ArgsTypeAssignSet = [], ConsTypeAssignSet \= [] ->
 			typecheck_info_get_io_state(TypeCheckInfo0, IOState0),
 			report_error_functor_type(TypeCheckInfo0,
@@ -1706,7 +1787,7 @@
 :- type args_type_assign 
 	--->	args(
 			type_assign, 	% Type assignment, 
-			list(type), 	% types of callee,
+			list(type), 	% types of callee args,
 			list(class_constraint) % constraints from callee
 		).
 
@@ -1741,23 +1822,21 @@
 	typecheck_unify_var_functor_get_ctors_2(ConsDefns, TypeCheckInfo,
 			TypeAssign0).
 
-	% typecheck_functor_type(ConsTypeAssignSet, Var, ...):
+	% typecheck_functor_type(ConsTypeAssignSet, Var):
 	%
 	% For each possible cons type assignment in `ConsTypeAssignSet',
 	% for each possible constructor type,
 	% check that the type of `Var' matches this type.
 
-:- pred typecheck_functor_type(cons_type_assign_set, var, typecheck_info,
+:- pred typecheck_functor_type(cons_type_assign_set, var,
 				args_type_assign_set, args_type_assign_set).
-:- mode typecheck_functor_type(in, in, typecheck_info_ui, in, out) is det.
+:- mode typecheck_functor_type(in, in, in, out) is det.
 
-typecheck_functor_type([], _, _) --> [].
-typecheck_functor_type([TypeAssign - ConsType | ConsTypeAssigns],
-			Var, TypeCheckInfo) -->
+typecheck_functor_type([], _) --> [].
+typecheck_functor_type([TypeAssign - ConsType | ConsTypeAssigns], Var) -->
 	{ ConsType = cons_type(Type, ArgTypes) },
-	type_assign_check_functor_type(Type, ArgTypes, Var,
-					TypeAssign, TypeCheckInfo),
-	typecheck_functor_type(ConsTypeAssigns, Var, TypeCheckInfo).
+	type_assign_check_functor_type(Type, ArgTypes, Var, TypeAssign),
+	typecheck_functor_type(ConsTypeAssigns, Var).
 
 	% typecheck_functor_arg_types(ConsTypeAssignSet, Var, Args, ...):
 	%
@@ -1780,15 +1859,14 @@
 
 	% iterate over all the possible type assignments.
 
-:- pred typecheck_unify_var_var_2(type_assign_set, var, var, typecheck_info, 
+:- pred typecheck_unify_var_var_2(type_assign_set, var, var,
 				type_assign_set, type_assign_set).
-:- mode typecheck_unify_var_var_2(in, in, in, typecheck_info_ui, in, out)
-				is det.
+:- mode typecheck_unify_var_var_2(in, in, in, in, out) is det.
 
-typecheck_unify_var_var_2([], _, _, _) --> [].
-typecheck_unify_var_var_2([TypeAssign0 | TypeAssigns0], X, Y, TypeCheckInfo) -->
-	type_assign_unify_var_var(X, Y, TypeAssign0, TypeCheckInfo),
-	typecheck_unify_var_var_2(TypeAssigns0, X, Y, TypeCheckInfo).
+typecheck_unify_var_var_2([], _, _) --> [].
+typecheck_unify_var_var_2([TypeAssign0 | TypeAssigns0], X, Y) -->
+	type_assign_unify_var_var(X, Y, TypeAssign0),
+	typecheck_unify_var_var_2(TypeAssigns0, X, Y).
 
 %-----------------------------------------------------------------------------%
 
@@ -1800,13 +1878,11 @@
 	% any type assignment(s) resulting from TypeAssign0 and this
 	% unification.
 
-:- pred type_assign_unify_var_var(var, var, type_assign, typecheck_info,
+:- pred type_assign_unify_var_var(var, var, type_assign, 
 				type_assign_set, type_assign_set).
-:- mode type_assign_unify_var_var(in, in, in, typecheck_info_ui, in, out)
-				is det.
+:- mode type_assign_unify_var_var(in, in, in, in, out) is det.
 
-type_assign_unify_var_var(X, Y, TypeAssign0, TypeCheckInfo, TypeAssignSet0,
-			TypeAssignSet) :-
+type_assign_unify_var_var(X, Y, TypeAssign0, TypeAssignSet0, TypeAssignSet) :-
 	type_assign_get_var_types(TypeAssign0, VarTypes0),
 	(
 		map__search(VarTypes0, X, TypeX)
@@ -1816,12 +1892,9 @@
 		->
 			% both X and Y already have types - just
 			% unify their types
-			typecheck_info_get_head_type_params(TypeCheckInfo,
-					HeadTypeParams),
 			( 
 				type_assign_unify_type(TypeAssign0,
-					HeadTypeParams, TypeX, TypeY,
-					TypeAssign3)
+					TypeX, TypeY, TypeAssign3)
 			->
 				TypeAssignSet = [TypeAssign3 | TypeAssignSet0]
 			;
@@ -1865,23 +1938,19 @@
 %-----------------------------------------------------------------------------%
 
 :- pred type_assign_check_functor_type(type, list(type), 
-		var, type_assign, typecheck_info,
-		args_type_assign_set, args_type_assign_set).
-:- mode type_assign_check_functor_type(in, in, in, in, typecheck_info_ui,
-		in, out) is det.
+		var, type_assign, args_type_assign_set, args_type_assign_set).
+:- mode type_assign_check_functor_type(in, in, in, in, in, out) is det.
 
 type_assign_check_functor_type(ConsType, ArgTypes, Y, TypeAssign1,
-		TypeCheckInfo, TypeAssignSet0, TypeAssignSet) :-
+		TypeAssignSet0, TypeAssignSet) :-
 
 		% unify the type of Var with the type of the constructor
 	type_assign_get_var_types(TypeAssign1, VarTypes0),
 	( %%% if some [TypeY]
 		map__search(VarTypes0, Y, TypeY)
 	->
-		typecheck_info_get_head_type_params(TypeCheckInfo,
-				HeadTypeParams),
 		( %%% if some [TypeAssign2]
-			type_assign_unify_type(TypeAssign1, HeadTypeParams,
+			type_assign_unify_type(TypeAssign1,
 					ConsType, TypeY, TypeAssign2)
 		->
 				% The constraints are empty here because
@@ -1916,8 +1985,8 @@
 get_cons_stuff(ConsDefn, TypeAssign0, _TypeCheckInfo, ConsType, ArgTypes,
 			TypeAssign) :-
 
-	ConsDefn = cons_type_info(ConsTypeVarSet, ConsType0, ArgTypes0,
-			ClassConstraints0),
+	ConsDefn = cons_type_info(ConsTypeVarSet, ConsExistQVars0,
+			ConsType0, ArgTypes0, ClassConstraints0),
 
 	% Rename apart the type vars in the type of the constructor
 	% and the types of its arguments.
@@ -1932,20 +2001,38 @@
 			[ConsType0 | ArgTypes0],
 			TypeAssign1, [ConsType1 | ArgTypes1], Subst)
 	->
+		apply_substitution_to_var_list(ConsExistQVars0, Subst,
+			ConsExistQVars),
 		apply_subst_to_constraints(Subst, ClassConstraints0,
 			ClassConstraints2),
 		type_assign_get_typeclass_constraints(TypeAssign1,
 			OldConstraints),
+		% XXX this is O(n*n) -- is it safe to swap the order here?
 		list__append(OldConstraints, ClassConstraints2,
 			ClassConstraints),
 		type_assign_set_typeclass_constraints(TypeAssign1,
-			ClassConstraints, TypeAssign),
+			ClassConstraints, TypeAssign2),
+		type_assign_get_head_type_params(TypeAssign2,
+			HeadTypeParams0),
+		list__append(ConsExistQVars, HeadTypeParams0,
+			HeadTypeParams),
+		type_assign_set_head_type_params(TypeAssign2,
+			HeadTypeParams, TypeAssign),
+
 		ConsType = ConsType1,
 		ArgTypes = ArgTypes1
 	;
 		error("get_cons_stuff: type_assign_rename_apart failed")
 	).
 
+:- pred apply_substitution_to_var_list(list(var), map(var, term), list(var)).
+:- mode apply_substitution_to_var_list(in, in, out) is det.
+
+apply_substitution_to_var_list(Vars0, RenameSubst, Vars) :-
+	term__var_list_to_term_list(Vars0, Terms0),
+	term__apply_substitution_to_list(Terms0, RenameSubst, Terms),
+	term__term_list_to_var_list(Terms, Vars).
+
 %-----------------------------------------------------------------------------%
 
 	% typecheck_lambda_var_has_type(Var, ArgVars, ...)
@@ -1960,8 +2047,7 @@
 typecheck_lambda_var_has_type(PredOrFunc, Var, ArgVars, TypeCheckInfo0,
 				TypeCheckInfo) :-
 	typecheck_info_get_type_assign_set(TypeCheckInfo0, TypeAssignSet0),
-	typecheck_info_get_head_type_params(TypeCheckInfo0, HeadTypeParams),
-	typecheck_lambda_var_has_type_2(TypeAssignSet0, HeadTypeParams,
+	typecheck_lambda_var_has_type_2(TypeAssignSet0,
 			PredOrFunc, Var, ArgVars, [], TypeAssignSet),
 	(
 		TypeAssignSet = [],
@@ -1979,14 +2065,14 @@
 				TypeAssignSet, TypeCheckInfo)
 	).
 
-:- pred typecheck_lambda_var_has_type_2(type_assign_set, headtypes,
+:- pred typecheck_lambda_var_has_type_2(type_assign_set, 
 				pred_or_func, var, list(var),
 				type_assign_set, type_assign_set).
-:- mode typecheck_lambda_var_has_type_2(in, in, in, in, in, in, out) is det.
+:- mode typecheck_lambda_var_has_type_2(in, in, in, in, in, out) is det.
 
-typecheck_lambda_var_has_type_2([], _, _, _, _) --> [].
+typecheck_lambda_var_has_type_2([], _, _, _) --> [].
 typecheck_lambda_var_has_type_2([TypeAssign0 | TypeAssignSet0],
-				HeadTypeParams, PredOrFunc, Var, ArgVars) -->
+				PredOrFunc, Var, ArgVars) -->
 	{ type_assign_get_types_of_vars(ArgVars, TypeAssign0, ArgVarTypes,
 					TypeAssign1) },
 	{ term__context_init(Context) },
@@ -2002,8 +2088,8 @@
 					FuncArgTypes, Context),
 				RetType], Context)
 	},
-	type_assign_var_has_type(TypeAssign1, HeadTypeParams, Var, LambdaType),
-	typecheck_lambda_var_has_type_2(TypeAssignSet0, HeadTypeParams,
+	type_assign_var_has_type(TypeAssign1, Var, LambdaType),
+	typecheck_lambda_var_has_type_2(TypeAssignSet0,
 					PredOrFunc, Var, ArgVars).
 
 :- pred type_assign_get_types_of_vars(list(var), type_assign, list(type),
@@ -2038,10 +2124,11 @@
 	% Unify (with occurs check) two types in a type assignment 
 	% and update the type bindings.
 
-:- pred type_assign_unify_type(type_assign, headtypes, type, type, type_assign).
-:- mode type_assign_unify_type(in, in, in, in, out) is semidet.
+:- pred type_assign_unify_type(type_assign, type, type, type_assign).
+:- mode type_assign_unify_type(in, in, in, out) is semidet.
 
-type_assign_unify_type(TypeAssign0, HeadTypeParams, X, Y, TypeAssign) :-
+type_assign_unify_type(TypeAssign0, X, Y, TypeAssign) :-
+	type_assign_get_head_type_params(TypeAssign0, HeadTypeParams),
 	type_assign_get_type_bindings(TypeAssign0, TypeBindings0),
 	type_unify(X, Y, HeadTypeParams, TypeBindings0, TypeBindings),
 	type_assign_set_type_bindings(TypeAssign0, TypeBindings, TypeAssign).
@@ -2106,6 +2193,8 @@
 :- type cons_type_info 
 	---> cons_type_info(
 			tvarset, 		% Type variables
+			existq_tvars,		% Existentially quantified
+						% type vars
 			type, 			% Constructor type
 			list(type), 		% Types of the arguments
 			list(class_constraint)	% Constraints introduced by 
@@ -2127,8 +2216,8 @@
 		IsPredOrFunc = predicate,
 		PredArity >= FuncArity
 	->
-		pred_info_arg_types(PredInfo, PredTypeVarSet,
-					CompleteArgTypes),
+		pred_info_arg_types(PredInfo, PredTypeVarSet, PredExistQVars,
+			CompleteArgTypes),
 		(
 			list__split_list(FuncArity, CompleteArgTypes,
 				ArgTypes, PredTypeParams)
@@ -2137,6 +2226,7 @@
 			PredType = term__functor(term__atom("pred"),
 					PredTypeParams, Context),
 			ConsInfo = cons_type_info(PredTypeVarSet,
+					PredExistQVars,
 					PredType, ArgTypes, ClassContext),
 			L = [ConsInfo | L0]
 		;
@@ -2147,7 +2237,7 @@
 		PredAsFuncArity is PredArity - 1,
 		PredAsFuncArity >= FuncArity
 	->
-		pred_info_arg_types(PredInfo, PredTypeVarSet,
+		pred_info_arg_types(PredInfo, PredTypeVarSet, PredExistQVars,
 					CompleteArgTypes),
 		(
 			list__split_list(FuncArity, CompleteArgTypes,
@@ -2170,6 +2260,7 @@
 					], Context)
 			),
 			ConsInfo = cons_type_info(PredTypeVarSet,
+					PredExistQVars,
 					FuncType, FuncArgTypes, ClassContext),
 			L = [ConsInfo | L0]
 		;
@@ -2194,7 +2285,8 @@
 	Arity >= 1,
 	Arity1 is Arity - 1,
 	higher_order_func_type(Arity1, TypeVarSet, FuncType, ArgTypes, RetType),
-	ConsTypeInfos = [cons_type_info(TypeVarSet, RetType,
+	ExistQVars = [],
+	ConsTypeInfos = [cons_type_info(TypeVarSet, ExistQVars, RetType,
 					[FuncType | ArgTypes], [])].
 
 %-----------------------------------------------------------------------------%
@@ -2232,7 +2324,7 @@
 
 			bool,		% did we find any type errors?
 
-			headtypes,	% Head type params
+			unit,		% UNUSED junk field
 
 			list(class_constraint),
 					% The declared typeclass constraints
@@ -2306,9 +2398,9 @@
 	TypeCheckInfo = typecheck_info(
 		IOState, ModuleInfo, CallPredId, 0, PredId, Context,
 		unify_context(explicit, []), VarSet, 
-		[type_assign(VarTypes, TypeVarSet, TypeBindings, 
-			Constraints, Proofs)],
-		FoundTypeError, HeadTypeParams, Constraints,
+		[type_assign(VarTypes, TypeVarSet, HeadTypeParams,
+			TypeBindings, Constraints, Proofs)],
+		FoundTypeError, unit, Constraints,
 		WarnedAboutOverloading, Status
 	).
 
@@ -2478,16 +2570,18 @@
 %-----------------------------------------------------------------------------%
 
 :- pred typecheck_info_get_final_info(typecheck_info, list(class_constraint),
-		tvarset, map(var, type),
+		tvarset, existq_tvars, map(var, type),
 		list(class_constraint), list(class_constraint),
 		map(class_constraint, constraint_proof)).
-:- mode typecheck_info_get_final_info(in, in, out, out, out, out, out) is det.
+:- mode typecheck_info_get_final_info(in, in, out, out, out, out, out, out)
+		is det.
 
 typecheck_info_get_final_info(TypeCheckInfo, OldConstraints, NewTypeVarSet,
-		NewVarTypes, NewTypeConstraints, RenamedOldConstraints,
-		NewConstraintProofs) :-
+		NewHeadTypeParams, NewVarTypes, NewTypeConstraints,
+		RenamedOldConstraints, NewConstraintProofs) :-
 	typecheck_info_get_type_assign_set(TypeCheckInfo, TypeAssignSet),
 	( TypeAssignSet = [TypeAssign | _] ->
+		type_assign_get_head_type_params(TypeAssign, HeadTypeParams),
 		type_assign_get_typevarset(TypeAssign, OldTypeVarSet),
 		type_assign_get_var_types(TypeAssign, VarTypes0),
 		type_assign_get_type_bindings(TypeAssign, TypeBindings),
@@ -2547,6 +2641,7 @@
 		%
 		term__apply_variable_renaming_to_list(Types, TSubst, NewTypes),
 		map__from_corresponding_lists(Vars, NewTypes, NewVarTypes),
+		map__apply_to_list(HeadTypeParams, TSubst, NewHeadTypeParams),
 		list__map(rename_class_constraint(TSubst), TypeConstraints,
 			NewTypeConstraints),
 		list__map(rename_class_constraint(TSubst), OldConstraints,
@@ -2650,25 +2745,23 @@
 
 %-----------------------------------------------------------------------------%
 
-:- pred typecheck_info_get_head_type_params(typecheck_info, headtypes).
-:- mode typecheck_info_get_head_type_params(typecheck_info_ui, out) is det.
+:- pred typecheck_info_get_junk(typecheck_info, unit).
+:- mode typecheck_info_get_junk(typecheck_info_ui, out) is det.
 
-typecheck_info_get_head_type_params(TypeCheckInfo, HeadTypeParams) :-
+typecheck_info_get_junk(TypeCheckInfo, Junk) :-
 	TypeCheckInfo =
-		typecheck_info(_,_,_,_,_,_,_,_,_,_,HeadTypeParams,_,_,_).
+		typecheck_info(_,_,_,_,_,_,_,_,_,_,Junk,_,_,_).
 
 %-----------------------------------------------------------------------------%
 
-:- pred typecheck_info_set_head_type_params(typecheck_info, headtypes, 
-			typecheck_info).
-:- mode typecheck_info_set_head_type_params(typecheck_info_di, in, 
-			typecheck_info_uo) is det.
+:- pred typecheck_info_set_junk(typecheck_info, unit, typecheck_info).
+:- mode typecheck_info_set_junk(typecheck_info_di, in, typecheck_info_uo)
+	is det.
 
-typecheck_info_set_head_type_params(TypeCheckInfo0, HeadTypeParams,
+typecheck_info_set_junk(TypeCheckInfo0, Junk,
 					TypeCheckInfo) :-
 	TypeCheckInfo0 = typecheck_info(A,B,C,D,E,F,G,H,I,J,_,L,M,N),
-	TypeCheckInfo =
-		typecheck_info(A,B,C,D,E,F,G,H,I,J,HeadTypeParams,L,M,N).
+	TypeCheckInfo = typecheck_info(A,B,C,D,E,F,G,H,I,J,Junk,L,M,N).
 
 %-----------------------------------------------------------------------------%
 
@@ -2776,7 +2869,7 @@
 		ConsType = term__functor(term__atom(BuiltInTypeName), [],
 				Context),
 		varset__init(ConsTypeVarSet),
-		ConsInfo = cons_type_info(ConsTypeVarSet, ConsType, [], []),
+		ConsInfo = cons_type_info(ConsTypeVarSet, [], ConsType, [], []),
 		ConsInfoList1 = [ConsInfo | ConsInfoList0]
 	;
 		ConsInfoList1 = ConsInfoList0
@@ -2831,7 +2924,7 @@
 typecheck_constraints(no, TypeCheckInfo0, TypeCheckInfo) :-
 		% reject any type assignment whose constraints have
 		% not all been eliminated by context reduction
-		% (i.e. those chich have constraints which do not match the
+		% (i.e. those which have constraints which do not match the
 		% declared constraints and which are not redundant for any
 		% other reason)
 	typecheck_info_get_type_assign_set(TypeCheckInfo0, TypeAssignSet0),
@@ -3288,7 +3381,8 @@
 	hlds_data__get_type_defn_tvarset(TypeDefn, ConsTypeVarSet),
 	hlds_data__get_type_defn_tparams(TypeDefn, ConsTypeParams),
 	construct_type(TypeId, ConsTypeParams, Context, ConsType),
-	ConsTypeInfo = cons_type_info(ConsTypeVarSet, ConsType, ArgTypes, []).
+	ConsTypeInfo = cons_type_info(ConsTypeVarSet, [],
+				ConsType, ArgTypes, []).
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
@@ -3301,6 +3395,8 @@
 	--->	type_assign(
 			map(var, type),		% var types
 			tvarset,		% type names
+			headtypes,		% universally quantified
+						% type variables
 			tsubst,			% type bindings
 			list(class_constraint),	% typeclass constraints
 			map(class_constraint,	% for each constraint
@@ -3316,21 +3412,29 @@
 :- pred type_assign_get_var_types(type_assign, map(var, type)).
 :- mode type_assign_get_var_types(in, out) is det.
 
-type_assign_get_var_types(type_assign(VarTypes, _, _, _, _), VarTypes).
+type_assign_get_var_types(type_assign(VarTypes, _, _, _, _, _), VarTypes).
 
 %-----------------------------------------------------------------------------%
 
 :- pred type_assign_get_typevarset(type_assign, tvarset).
 :- mode type_assign_get_typevarset(in, out) is det.
 
-type_assign_get_typevarset(type_assign(_, TypeVarSet, _, _, _), TypeVarSet).
+type_assign_get_typevarset(type_assign(_, TypeVarSet, _, _, _, _), TypeVarSet).
+
+%-----------------------------------------------------------------------------%
+
+:- pred type_assign_get_head_type_params(type_assign, headtypes).
+:- mode type_assign_get_head_type_params(in, out) is det.
+
+type_assign_get_head_type_params(type_assign(_, _, HeadTypeParams, _, _, _),
+			HeadTypeParams).
 
 %-----------------------------------------------------------------------------%
 
 :- pred type_assign_get_type_bindings(type_assign, tsubst).
 :- mode type_assign_get_type_bindings(in, out) is det.
 
-type_assign_get_type_bindings(type_assign(_, _, TypeBindings, _, _),
+type_assign_get_type_bindings(type_assign(_, _, _, TypeBindings, _, _),
 	TypeBindings).
 %-----------------------------------------------------------------------------%
 
@@ -3338,7 +3442,7 @@
 	list(class_constraint)).
 :- mode type_assign_get_typeclass_constraints(in, out) is det.
 
-type_assign_get_typeclass_constraints(type_assign(_, _, _, Constraints, _),
+type_assign_get_typeclass_constraints(type_assign(_, _, _, _, Constraints, _),
 	Constraints).
 
 %-----------------------------------------------------------------------------%
@@ -3347,30 +3451,38 @@
 	map(class_constraint, constraint_proof)).
 :- mode type_assign_get_constraint_proofs(in, out) is det.
 
-type_assign_get_constraint_proofs(type_assign(_, _, _, _, Proofs), Proofs).  
+type_assign_get_constraint_proofs(type_assign(_, _, _, _, _, Proofs), Proofs).  
 %-----------------------------------------------------------------------------%
 
 :- pred type_assign_set_var_types(type_assign, map(var, type), type_assign).
 :- mode type_assign_set_var_types(in, in, out) is det.
 
-type_assign_set_var_types(type_assign(_, B, C, D, E), VarTypes,
-			type_assign(VarTypes, B, C, D, E)).
+type_assign_set_var_types(type_assign(_, B, C, D, E, F), VarTypes,
+			type_assign(VarTypes, B, C, D, E, F)).
 
 %-----------------------------------------------------------------------------%
 
 :- pred type_assign_set_typevarset(type_assign, tvarset, type_assign).
 :- mode type_assign_set_typevarset(in, in, out) is det.
 
-type_assign_set_typevarset(type_assign(A, _, C, D, E), TypeVarSet,
-			type_assign(A, TypeVarSet, C, D, E)).
+type_assign_set_typevarset(type_assign(A, _, C, D, E, F), TypeVarSet,
+			type_assign(A, TypeVarSet, C, D, E, F)).
+
+%-----------------------------------------------------------------------------%
+
+:- pred type_assign_set_head_type_params(type_assign, headtypes, type_assign).
+:- mode type_assign_set_head_type_params(in, in, out) is det.
+
+type_assign_set_head_type_params(type_assign(A, B, _, D, E, F), HeadTypeParams,
+			type_assign(A, B, HeadTypeParams, D, E, F)).
 
 %-----------------------------------------------------------------------------%
 
 :- pred type_assign_set_type_bindings(type_assign, tsubst, type_assign).
 :- mode type_assign_set_type_bindings(in, in, out) is det.
 
-type_assign_set_type_bindings(type_assign(A, B, _, D, E), TypeBindings,
-			type_assign(A, B, TypeBindings, D, E)).
+type_assign_set_type_bindings(type_assign(A, B, C, _, E, F), TypeBindings,
+			type_assign(A, B, C, TypeBindings, E, F)).
 
 %-----------------------------------------------------------------------------%
 
@@ -3378,8 +3490,8 @@
 	list(class_constraint), type_assign).
 :- mode type_assign_set_typeclass_constraints(in, in, out) is det.
 
-type_assign_set_typeclass_constraints(type_assign(A, B, C, _, E), Constraints,
-			type_assign(A, B, C, Constraints, E)).
+type_assign_set_typeclass_constraints(type_assign(A, B, C, D, _, F),
+			Constraints, type_assign(A, B, C, D, Constraints, F)).
 
 %-----------------------------------------------------------------------------%
 
@@ -3387,8 +3499,8 @@
 	map(class_constraint, constraint_proof), type_assign).
 :- mode type_assign_set_constraint_proofs(in, in, out) is det.
 
-type_assign_set_constraint_proofs(type_assign(A, B, C, D, _),
-			Proofs, type_assign(A, B, C, D, Proofs)).
+type_assign_set_constraint_proofs(type_assign(A, B, C, D, E, _),
+			Proofs, type_assign(A, B, C, D, E, Proofs)).
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
@@ -3430,7 +3542,7 @@
 	{ pred_info_name(PredInfo, PredName) },
 	{ Name = unqualified(PredName) },
 	{ pred_info_context(PredInfo, Context) },
-	{ pred_info_arg_types(PredInfo, VarSet, Types0) },
+	{ pred_info_arg_types(PredInfo, VarSet, ExistQVars, Types0) },
 	{ strip_builtin_qualifiers_from_type_list(Types0, Types) },
 	{ pred_info_get_is_pred_or_func(PredInfo, PredOrFunc) },
 	{ pred_info_get_class_context(PredInfo, ClassContext) },
@@ -3439,11 +3551,11 @@
 	prog_out__write_context(Context),
 	io__write_string("Inferred "),
 	(	{ PredOrFunc = predicate },
-		mercury_output_pred_type(VarSet, Name, Types, MaybeDet,
-			Purity, ClassContext, Context)
+		mercury_output_pred_type(VarSet, ExistQVars, Name, Types,
+			MaybeDet, Purity, ClassContext, Context)
 	;	{ PredOrFunc = function },
 		{ pred_args_to_func_args(Types, ArgTypes, RetType) },
-		mercury_output_func_type(VarSet, Name, ArgTypes,
+		mercury_output_func_type(VarSet, ExistQVars, Name, ArgTypes,
 			RetType, MaybeDet, Purity, ClassContext, Context)
 	).
 
@@ -3700,7 +3812,7 @@
 		(
 			% could the type of the functor be polymorphic?
 			{ list__member(ConsDefn, ConsDefnList) },
-			{ ConsDefn = cons_type_info(_, _, ConsArgTypes, _) },
+			{ ConsDefn = cons_type_info(_, _, _, ConsArgTypes, _) },
 			{ ConsArgTypes \= [] }
 		->
 			% if so, print out the type of `Var'
@@ -3890,7 +4002,7 @@
 :- mode write_cons_type(in, in, in, di, uo) is det.
 
 	% XXX Should we mention the context here?
-write_cons_type(cons_type_info(TVarSet, ConsType0, ArgTypes0, _), 
+write_cons_type(cons_type_info(TVarSet, _ExistQVars, ConsType0, ArgTypes0, _), 
 		Functor, _) -->
 	{ strip_builtin_qualifier_from_cons_id(Functor, Functor1) },
 	{ strip_builtin_qualifiers_from_type_list(ArgTypes0, ArgTypes) },
Index: compiler/unused_args.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/unused_args.m,v
retrieving revision 1.49
diff -u -r1.49 unused_args.m
--- unused_args.m	1998/06/03 00:43:25	1.49
+++ unused_args.m	1998/06/04 17:27:41
@@ -919,7 +919,7 @@
 	pred_info_get_is_pred_or_func(PredInfo0, PredOrFunc),
 	proc_id_to_int(ProcId, ProcInt),
 	string__int_to_string(ProcInt, Id),
-	pred_info_arg_types(PredInfo0, Tvars, ArgTypes0),
+	pred_info_arg_types(PredInfo0, Tvars, ExistQVars, ArgTypes0),
 		% create a unique new pred name using the old proc_id
 	(
 		string__prefix(Name0, "__"),
@@ -962,8 +962,9 @@
 		% *** This will need to be fixed when the condition
 		%	field of the pred_info becomes used.
 	pred_info_init(PredModule, qualified(PredModule, Name), Arity, Tvars,
-		ArgTypes, true, Context, ClausesInfo, Status, Markers,
-		GoalType, PredOrFunc, ClassContext, EmptyProofs, PredInfo1),
+		ExistQVars, ArgTypes, true, Context, ClausesInfo, Status,
+		Markers, GoalType, PredOrFunc, ClassContext, EmptyProofs,
+		PredInfo1),
 	pred_info_set_typevarset(PredInfo1, TypeVars, PredInfo).
 
 

-- 
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.



More information about the developers mailing list