[m-rev.] for review: show existential quantifiers in type error messages

Fergus Henderson fjh at cs.mu.OZ.AU
Wed Feb 6 23:04:25 AEDT 2002


Estimated hours taken: 3
Branches: main

Improve the error messages for type errors involving existentially quantified
types.

compiler/typecheck.m:
	When outputting error messages, include explicit
	`some [...]' quantifiers for existentially quantified types.

tests/invalid/ext_type_bug.err_exp:
tests/invalid/type_mismatch.err_exp:
tests/invalid/types.err_exp:
tests/invalid/types.err_exp2:
	Update the expected output for these test cases
	to reflect the above change.

Workspace: /home/earth/fjh/ws-earth4/mercury
Index: compiler/typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
retrieving revision 1.308
diff -u -d -r1.308 typecheck.m
--- compiler/typecheck.m	25 Sep 2001 09:36:55 -0000	1.308
+++ compiler/typecheck.m	29 Jan 2002 07:11:42 -0000
@@ -1880,13 +1880,14 @@
 	% Given a type assignment set and a variable id,
 	% return the list of possible different types for the variable.
 
-:- type type_stuff ---> type_stuff(type, tvarset, tsubst).
+:- type type_stuff ---> type_stuff(type, tvarset, tsubst, head_type_params).
 
 :- pred get_type_stuff(type_assign_set, prog_var, list(type_stuff)).
 :- mode get_type_stuff(in, in, out) is det.
 get_type_stuff([], _VarId, []).
 get_type_stuff([TypeAssign | TypeAssigns], VarId, L) :-
 	get_type_stuff(TypeAssigns, VarId, L0),
+	type_assign_get_head_type_params(TypeAssign, HeadTypeParams),
 	type_assign_get_type_bindings(TypeAssign, TypeBindings),
 	type_assign_get_typevarset(TypeAssign, TVarSet),
 	type_assign_get_var_types(TypeAssign, VarTypes),
@@ -1901,7 +1902,7 @@
 		term__context_init(Context),
 		Type = term__functor(term__atom("<any>"), [], Context)
 	),
-	TypeStuff = type_stuff(Type, TVarSet, TypeBindings),
+	TypeStuff = type_stuff(Type, TVarSet, TypeBindings, HeadTypeParams),
 	(
 		list__member(TypeStuff, L0)
 	->
@@ -1914,7 +1915,8 @@
 	% return the list of possible different types for the argument
 	% and the variable.
 
-:- type arg_type_stuff ---> arg_type_stuff(type, type, tvarset).
+:- type arg_type_stuff --->
+	arg_type_stuff(type, type, tvarset, head_type_params).
 
 :- pred get_arg_type_stuff(args_type_assign_set, prog_var,
 		list(arg_type_stuff)).
@@ -1923,6 +1925,7 @@
 get_arg_type_stuff([args(TypeAssign, ArgTypes, _) | ArgTypeAssigns], 
 			VarId, L) :-
 	get_arg_type_stuff(ArgTypeAssigns, VarId, L0),
+	type_assign_get_head_type_params(TypeAssign, HeadTypeParams),
 	type_assign_get_type_bindings(TypeAssign, TypeBindings),
 	type_assign_get_typevarset(TypeAssign, TVarSet),
 	type_assign_get_var_types(TypeAssign, VarTypes),
@@ -1940,7 +1943,7 @@
 	list__index0_det(ArgTypes, 0, ArgType),
 	term__apply_rec_substitution(ArgType, TypeBindings, ArgType2),
 	term__apply_rec_substitution(VarType, TypeBindings, VarType2),
-	TypeStuff = arg_type_stuff(ArgType2, VarType2, TVarSet),
+	TypeStuff = arg_type_stuff(ArgType2, VarType2, TVarSet, HeadTypeParams),
 	(
 		list__member(TypeStuff, L0)
 	->
@@ -4893,8 +4896,9 @@
 			prog_var,	% variable in that position
 			type,		% actual type of that variable
 			type,		% expected type of that variable
-			tvarset		% the type vars in the expected
+			tvarset,	% the type vars in the expected
 					% and expected types
+			head_type_params % existentially quantified type vars
 		).
 
 :- pred find_mismatched_args(assoc_list(prog_var, type), type_assign_set, int,
@@ -4907,7 +4911,8 @@
 	ArgNum1 is ArgNum0 + 1,
 	find_mismatched_args(ArgExpTypes, TypeAssignSet, ArgNum1, Mismatched1),
 	get_type_stuff(TypeAssignSet, Arg, TypeStuffList),
-	TypeStuffList = [type_stuff(ArgType, TVarSet, TypeBindings)],
+	TypeStuffList = [type_stuff(ArgType, TVarSet, TypeBindings,
+		HeadTypeParams)],
 	term__apply_rec_substitution(ArgType, TypeBindings, FullArgType),
 	term__apply_rec_substitution(ExpType, TypeBindings, FullExpType),
 	(
@@ -4924,7 +4929,7 @@
 		Mismatched = Mismatched1
 	;
 		Mismatched = [mismatch(ArgNum0, Arg, FullArgType, FullExpType,
-				TVarSet) | Mismatched1]
+				TVarSet, HeadTypeParams) | Mismatched1]
 	).
 
 :- pred report_mismatched_args(list(mismatch_info), bool, prog_varset, cons_id,
@@ -4934,7 +4939,8 @@
 report_mismatched_args([], _, _, _, _) --> [].
 report_mismatched_args([Mismatch | Mismatches], First, VarSet, Functor,
 		Context) -->
-	{ Mismatch = mismatch(ArgNum, Var, ActType, ExpType, TVarSet) },
+	{ Mismatch = mismatch(ArgNum, Var, ActType, ExpType, TVarSet,
+		HeadTypeParams) },
 	prog_out__write_context(Context),
 	(
 		% Handle higher-order syntax such as ''(F, A) specially:
@@ -4969,11 +4975,11 @@
 		[]
 	),
 	io__write_string(" has type `"),
-	mercury_output_term(ActType, TVarSet, no),
+	output_type(ActType, TVarSet, HeadTypeParams),
 	io__write_string("',\n"),
 	prog_out__write_context(Context),
 	io__write_string("  expected type was `"),
-	mercury_output_term(ExpType, TVarSet, no),
+	output_type(ExpType, TVarSet, HeadTypeParams),
 	( { Mismatches = [] } ->
 		io__write_string("'.\n")
 	;
@@ -5080,13 +5086,11 @@
 :- 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, _ExistQVars, ConsType0, ArgTypes0, _), 
+write_cons_type(cons_type_info(TVarSet, ExistQVars, ConsType, ArgTypes, _), 
 		Functor, _) -->
-	{ strip_builtin_qualifier_from_cons_id(Functor, Functor1) },
-	{ strip_builtin_qualifiers_from_type_list(ArgTypes0, ArgTypes) },
 	( { ArgTypes \= [] } ->
-		( { cons_id_and_args_to_term(Functor1, ArgTypes, Term) } ->
-			mercury_output_term(Term, TVarSet, no)
+		( { cons_id_and_args_to_term(Functor, ArgTypes, Term) } ->
+			output_type(Term, TVarSet, ExistQVars)
 		;
 			{ error("typecheck:write_cons_type - invalid cons_id") }
 		),	
@@ -5094,8 +5098,7 @@
 	;
 		[]
 	),
-	{ strip_builtin_qualifiers_from_type(ConsType0, ConsType) },
-	mercury_output_term(ConsType, TVarSet, no).
+	output_type(ConsType, TVarSet, ExistQVars).
 
 :- pred write_cons_type_list(list(cons_type_info), cons_id, int, prog_context,
 				io__state, io__state).
@@ -5268,6 +5271,14 @@
 
 	% write_type_b writes out a type after applying the type bindings.
 
+:- pred write_type_b(type, tvarset, tsubst, head_type_params,
+		io__state, io__state).
+:- mode write_type_b(in, in, in, in, di, uo) is det.
+
+write_type_b(Type0, TypeVarSet, TypeBindings, HeadTypeParams) -->
+	{ Type = maybe_add_existential_quantifier(HeadTypeParams, Type0) },
+	write_type_b(Type, TypeVarSet, TypeBindings).
+
 :- pred write_type_b(type, tvarset, tsubst, io__state, io__state).
 :- mode write_type_b(in, in, in, di, uo) is det.
 
@@ -5279,11 +5290,35 @@
 :- func typestuff_to_typestr(type_stuff) = string.
 
 typestuff_to_typestr(TypeStuff) = TypeStr :-
-	TypeStuff = type_stuff(Type0, TypeVarSet, TypeBindings),
+	TypeStuff = type_stuff(Type0, TypeVarSet, TypeBindings, HeadTypeParams),
 	term__apply_rec_substitution(Type0, TypeBindings, Type1),
-	strip_builtin_qualifiers_from_type(Type1, Type),
+	strip_builtin_qualifiers_from_type(Type1, Type2),
+	Type = maybe_add_existential_quantifier(HeadTypeParams, Type2),
 	TypeStr = mercury_term_to_string(Type, TypeVarSet, no).
 
+	%
+	% Check if any of the type variables in the type are existentially
+	% quantified (occur in HeadTypeParams), and if so, add an
+	% appropriate existential quantifier at the front of the type.
+	%
+:- func maybe_add_existential_quantifier(head_type_params, (type)) = (type).
+maybe_add_existential_quantifier(HeadTypeParams, Type0) = Type :-
+	type_util__vars(Type0, TVars),
+	ExistQuantTVars = set__to_sorted_list(set__intersect(
+		set__list_to_set(HeadTypeParams), set__list_to_set(TVars))),
+	( ExistQuantTVars = [] ->
+		Type = Type0
+	;
+		Type = term__functor(term__atom("some"), [make_list_term(
+			ExistQuantTVars), Type0],
+			term__context_init)
+	).
+
+:- func make_list_term(list(tvar)) = (type).
+make_list_term([]) = term__functor(term__atom("[]"), [], term__context_init).
+make_list_term([V|Vs]) = term__functor(term__atom("[|]"),
+	[term__variable(V), make_list_term(Vs)], term__context_init).
+
 %-----------------------------------------------------------------------------%
 
 :- pred report_error_var(typecheck_info, prog_var, type, type_assign_set,
@@ -5305,13 +5340,14 @@
 	io__write_string("  type error: "),
 	( { TypeStuffList = [SingleTypeStuff] } ->
 		write_argument_name(VarSet, VarId),
-		{ SingleTypeStuff = type_stuff(VType, TVarSet, TBinding) },
+		{ SingleTypeStuff = type_stuff(VType, TVarSet, TBinding,
+			HeadTypeParams) },
 		io__write_string(" has type `"),
-		write_type_b(VType, TVarSet, TBinding),
+		write_type_b(VType, TVarSet, TBinding, HeadTypeParams),
 		io__write_string("',\n"),
 		prog_out__write_context(Context),
 		io__write_string("  expected type was `"),
-		write_type_b(Type, TVarSet, TBinding),
+		write_type_b(Type, TVarSet, TBinding, HeadTypeParams),
 		io__write_string("'.\n")
 	;
 		io__write_string("type of "),
@@ -5352,15 +5388,14 @@
 	io__write_string("  type error: "),
 	( { ArgTypeStuffList = [SingleArgTypeStuff] } ->
 		write_argument_name(VarSet, VarId),
-		{ SingleArgTypeStuff = arg_type_stuff(Type0, VType0, TVarSet) },
+		{ SingleArgTypeStuff = arg_type_stuff(Type0, VType0, TVarSet,
+			HeadTypeParams) },
 		io__write_string(" has type `"),
-		{ strip_builtin_qualifiers_from_type(VType0, VType) },
-		mercury_output_term(VType, TVarSet, no),
+		output_type(VType0, TVarSet, HeadTypeParams),
 		io__write_string("',\n"),
 		prog_out__write_context(Context),
 		io__write_string("  expected type was `"),
-		{ strip_builtin_qualifiers_from_type(Type0, Type) },
-		mercury_output_term(Type, TVarSet, no),
+		output_type(Type0, TVarSet, HeadTypeParams),
 		io__write_string("'.\n")
 	;
 		io__write_string("type of "),
@@ -5382,6 +5417,13 @@
 	),
 	write_args_type_assign_set_msg(ArgTypeAssignSet0, VarSet).
 
+:- pred output_type((type)::in, tvarset::in, head_type_params::in,
+		io__state::di, io__state::uo) is det.
+output_type(Type0, TVarSet, HeadTypeParams) -->
+	{ strip_builtin_qualifiers_from_type(Type0, Type1) },
+	{ Type = maybe_add_existential_quantifier(HeadTypeParams, Type1) },
+	mercury_output_term(Type, TVarSet, no).
+
 :- pred write_types_list(prog_context::in, list(string)::in,
 	io__state::di, io__state::uo) is det.
 
@@ -5400,8 +5442,8 @@
 :- pred write_type_stuff(type_stuff, io__state, io__state).
 :- mode write_type_stuff(in, di, uo) is det.
 
-write_type_stuff(type_stuff(T, TVarSet, TBinding)) -->
-	write_type_b(T, TVarSet, TBinding).
+write_type_stuff(type_stuff(T, TVarSet, TBinding, HeadTypeParams)) -->
+	write_type_b(T, TVarSet, TBinding, HeadTypeParams).
 
 :- pred write_var_type_stuff_list(list(type_stuff), type, io__state, io__state).
 :- mode write_var_type_stuff_list(in, in, di, uo) is det.
@@ -5412,10 +5454,10 @@
 :- pred write_var_type_stuff(type, type_stuff, io__state, io__state).
 :- mode write_var_type_stuff(in, in, di, uo) is det.
 	
-write_var_type_stuff(T, type_stuff(VT, TVarSet, TBinding)) -->
-	write_type_b(VT, TVarSet, TBinding),
+write_var_type_stuff(T, type_stuff(VT, TVarSet, TBinding, HeadTypeParams)) -->
+	write_type_b(VT, TVarSet, TBinding, HeadTypeParams),
 	io__write_string("/"),
-	write_type_b(T, TVarSet, TBinding).
+	write_type_b(T, TVarSet, TBinding, HeadTypeParams).
 
 :- pred write_arg_type_stuff_list(list(arg_type_stuff), io__state, io__state).
 :- mode write_arg_type_stuff_list(in, di, uo) is det.
@@ -5426,12 +5468,10 @@
 :- pred write_arg_type_stuff(arg_type_stuff, io__state, io__state).
 :- mode write_arg_type_stuff(in, di, uo) is det.
 
-write_arg_type_stuff(arg_type_stuff(T0, VT0, TVarSet)) -->
-	{ strip_builtin_qualifiers_from_type(VT0, VT) },
-	mercury_output_term(VT, TVarSet, no),
+write_arg_type_stuff(arg_type_stuff(T, VT, TVarSet, HeadTypeParams)) -->
+	output_type(VT, TVarSet, HeadTypeParams),
 	io__write_string("/"),
-	{ strip_builtin_qualifiers_from_type(T0, T) },
-	mercury_output_term(T, TVarSet, no).
+	output_type(T, TVarSet, HeadTypeParams).
 
 %-----------------------------------------------------------------------------%
 
@@ -5993,12 +6033,14 @@
 	{ type_assign_get_var_types(TypeAssign2, VarTypes2) },
 	{ type_assign_get_type_bindings(TypeAssign1, TypeBindings1) },
 	{ type_assign_get_type_bindings(TypeAssign2, TypeBindings2) },
+	{ type_assign_get_head_type_params(TypeAssign1, HeadTypeParams1) },
+	{ type_assign_get_head_type_params(TypeAssign2, HeadTypeParams2) },
 	( {
 		map__search(VarTypes1, V, Type1),
 		map__search(VarTypes2, V, Type2),
-		term__apply_rec_substitution(Type1, TypeBindings1, T1a),
-		term__apply_rec_substitution(Type2, TypeBindings2, T2a),
-		\+ identical_types(T1a, T2a)
+		term__apply_rec_substitution(Type1, TypeBindings1, T1),
+		term__apply_rec_substitution(Type2, TypeBindings2, T2),
+		\+ identical_types(T1, T2)
 	} ->
 		{ typecheck_info_get_context(TypeCheckInfo, Context) },
 		( { Found0 = no } ->
@@ -6013,12 +6055,10 @@
 		mercury_output_var(V, VarSet, no),
 		io__write_string(" :: "),
 		{ type_assign_get_typevarset(TypeAssign1, TVarSet1) },
-		{ strip_builtin_qualifiers_from_type(T1a, T1) },
-		mercury_output_term(T1, TVarSet1, no),
+		output_type(T1, TVarSet1, HeadTypeParams1),
 		io__write_string(" or "),
 		{ type_assign_get_typevarset(TypeAssign2, TVarSet2) },
-		{ strip_builtin_qualifiers_from_type(T2a, T2) },
-		mercury_output_term(T2, TVarSet2, no),
+		output_type(T2, TVarSet2, HeadTypeParams2),
 		io__write_string("\n")
 	;
 		{ Found1 = Found0 }
Index: tests/invalid/ext_type_bug.err_exp
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/ext_type_bug.err_exp,v
retrieving revision 1.2
diff -u -d -r1.2 ext_type_bug.err_exp
--- tests/invalid/ext_type_bug.err_exp	13 Jul 1999 08:55:09 -0000	1.2
+++ tests/invalid/ext_type_bug.err_exp	6 Feb 2002 11:58:40 -0000
@@ -1,5 +1,5 @@
 ext_type_bug.m:011: In clause for predicate `ext_type_bug:foo/1':
 ext_type_bug.m:011:   in argument 1 of call to predicate `make_bar/1':
 ext_type_bug.m:011:   type error: variable `Bar' has type `(ext_type_bug:bar(int))',
-ext_type_bug.m:011:   expected type was `(ext_type_bug:bar(T))'.
+ext_type_bug.m:011:   expected type was `(some [T] (ext_type_bug:bar(T)))'.
 For more information, try recompiling with `-E'.
Index: tests/invalid/type_mismatch.err_exp
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/type_mismatch.err_exp,v
retrieving revision 1.2
diff -u -d -r1.2 type_mismatch.err_exp
--- tests/invalid/type_mismatch.err_exp	7 Dec 1997 08:56:01 -0000	1.2
+++ tests/invalid/type_mismatch.err_exp	29 Jan 2002 08:02:04 -0000
@@ -14,20 +14,20 @@
 type_mismatch.m:025:   in unification of variable `Tuple'
 type_mismatch.m:025:   and term `f3(V_5, Field, V_6)':
 type_mismatch.m:025:   type error in argument(s) of functor `f3/3'.
-type_mismatch.m:025:   Argument 2 (Field) has type `F3c',
-type_mismatch.m:025:   expected type was `F3b'.
+type_mismatch.m:025:   Argument 2 (Field) has type `(some [F3c] F3c)',
+type_mismatch.m:025:   expected type was `(some [F3b] F3b)'.
 type_mismatch.m:032: In clause for predicate `type_mismatch:p4a/2':
 type_mismatch.m:032:   in unification of variable `Tuple'
 type_mismatch.m:032:   and term `f4(Field, V_5, V_6)':
 type_mismatch.m:032:   type error in argument(s) of functor `f4/3'.
 type_mismatch.m:032:   Argument 1 (Field) has type `float',
-type_mismatch.m:032:   expected type was `F4'.
+type_mismatch.m:032:   expected type was `(some [F4] F4)'.
 type_mismatch.m:035: In clause for predicate `type_mismatch:p4b/3':
 type_mismatch.m:035:   in unification of variable `Tuple'
 type_mismatch.m:035:   and term `f4(Field1, Field2, V_7)':
 type_mismatch.m:035:   type error in argument(s) of functor `f4/3'.
 type_mismatch.m:035:   Argument 1 (Field1) has type `float',
-type_mismatch.m:035:   expected type was `F4';
+type_mismatch.m:035:   expected type was `(some [F4] F4)';
 type_mismatch.m:035:   argument 2 (Field2) has type `float',
 type_mismatch.m:035:   expected type was `int'.
 For more information, try recompiling with `-E'.
Index: tests/invalid/types.err_exp
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/types.err_exp,v
retrieving revision 1.8
diff -u -d -r1.8 types.err_exp
--- tests/invalid/types.err_exp	9 Nov 1999 22:40:14 -0000	1.8
+++ tests/invalid/types.err_exp	6 Feb 2002 11:57:35 -0000
@@ -18,7 +18,7 @@
 types.m:039: In clause for predicate `types:bar/1':
 types.m:039:   type error in unification of variable `X'
 types.m:039:   and constant `0'.
-types.m:039:   variable `X' has type `BarTypeParam',
+types.m:039:   variable `X' has type `(some [BarTypeParam] BarTypeParam)',
 types.m:039:   constant `0' has type `int'.
 types.m:050: Error: no clauses for predicate `types:bar2/1'.
 types.m:018: In clause for predicate `types:r/0':
Index: tests/invalid/types.err_exp2
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/types.err_exp2,v
retrieving revision 1.4
diff -u -d -r1.4 types.err_exp2
--- tests/invalid/types.err_exp2	9 Nov 1999 22:40:15 -0000	1.4
+++ tests/invalid/types.err_exp2	6 Feb 2002 11:57:37 -0000
@@ -18,7 +18,7 @@
 types.m:039: In clause for predicate `types:bar/1':
 types.m:039:   type error in unification of variable `X'
 types.m:039:   and constant `0'.
-types.m:039:   variable `X' has type `BarTypeParam',
+types.m:039:   variable `X' has type `(some [BarTypeParam] BarTypeParam)',
 types.m:039:   constant `0' has type `int'.
 types.m:050: Error: no clauses for predicate `types:bar2/1'.
 types.m:018: In clause for predicate `types:r/0':

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------



More information about the reviews mailing list