[m-dev.] diff: check for unbound type vars in class constraints
Fergus Henderson
fjh at cs.mu.OZ.AU
Wed Aug 16 18:52:20 AEST 2000
Estimated hours taken: 6
Check for various cases of type variables that occur only in type class
constraints. These cases are all errors, since the type variable can
never be bound, but previously the compiler was not checking for these
errors.
compiler/prog_io.m:
Fix a bug that was due to an accidental name clash between two
different variables both named `Args' (one was the type
constructor arguments, the other was the class constraint
arguments, but both had type `term').
This bug was preventing it from reporting errors for
type variables in existentially quantified data types
which do not occur in the argument types.
Also improve one of the other error messages slightly.
compiler/prog_io_typeclass.m:
Check that type vars in superclass constraints are parameters of
the type class. This enforces the following requirement from the
"type class constraints on type classes" section of the Mercury
language reference manual:
| The variables that appear as arguments to the type classes in the
| [superclass] constraints must also be arguments to the type class
| in question.
Likewise check type variables in instance declarations, to
enforce the following requirement from the "type class constraints
on instance declarations" section of the Mercury language reference
manual:
| The variables that appear as arguments to the type classes in the
| constraints must all be type variables that appear in the types in
| the instance declarations.
compiler/make_hlds.m:
Check that type vars in constraints on pred and func declarations
(including type class methods) occur in the procedure's argument types.
This enforces the following requirement from the "type class
constraints on predicates and functions" section of the Mercury
language reference manual:
| where ... TYPEVARIABLE is a type variable that appears in the
| predicate's or function's type signature.
Note that this can't be done in prog_io.m, since for type class
methods we don't know what the type variables in the type class
are when we're parsing the type class methods. Hence I did it
in make_hlds.m instead.
tests/invalid/type_vars.m:
tests/invalid/type_vars.err_exp:
Add another test to this test case, to test the fix to prog_io.m,
and add some comments to the existing tests.
Adjust the expected output to reflect the slightly improved
error message and the new test.
tests/invalid/Mmakefile:
tests/invalid/unbound_type_vars.m:
tests/invalid/unbound_type_vars.err_exp:
A new test case containing regression tests to test the fixes
to prog_io_typeclass.m and make_hlds.m.
Workspace: /home/pgrad/fjh/ws/hg
Index: compiler/make_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.341
diff -u -d -r1.341 make_hlds.m
--- compiler/make_hlds.m 2000/09/15 23:45:40 1.341
+++ compiler/make_hlds.m 2000/08/16 08:26:55
@@ -2536,17 +2536,19 @@
add_new_pred(Module0, TVarSet, ExistQVars, PredName, Types, Cond, Purity,
ClassContext, Markers0, Context, Status, NeedQual,
PredOrFunc, Module) -->
- { module_info_name(Module0, ModuleName) },
+ check_tvars_in_constraints(ClassContext, Types, TVarSet,
+ PredOrFunc, PredName, Context, Module0, Module1),
+
+ { module_info_name(Module1, ModuleName) },
{ list__length(Types, Arity) },
(
{ PredName = unqualified(_PName) },
- { module_info_incr_errors(Module0, Module) },
+ { module_info_incr_errors(Module1, Module) },
unqualified_pred_error(PredName, Arity, Context)
% All predicate names passed into this predicate should have
% been qualified by prog_io.m, when they were first read.
;
{ PredName = qualified(MNameOfPred, PName) },
- { Module1 = Module0 },
{ module_info_get_predicate_table(Module1, PredicateTable0) },
{ clauses_info_init(Arity, ClausesInfo) },
{ map__init(Proofs) },
@@ -2609,6 +2611,101 @@
)
).
+%-----------------------------------------------------------------------------%
+
+ %
+ % check for type variables which occur in the the class constraints,
+ % but which don't occur in the predicate argument types
+ %
+:- pred check_tvars_in_constraints(class_constraints, list(type), tvarset,
+ pred_or_func, sym_name, prog_context,
+ module_info, module_info, io__state, io__state).
+:- mode check_tvars_in_constraints(in, in, in, in, in, in,
+ in, out, di, uo) is det.
+
+check_tvars_in_constraints(ClassContext, ArgTypes, TVarSet,
+ PredOrFunc, PredName, Context, Module0, Module) -->
+ { solutions(constrained_tvar_not_in_arg_types(ClassContext, ArgTypes),
+ UnboundTVars) },
+ ( { UnboundTVars = [] } ->
+ { Module = Module0 }
+ ;
+ { module_info_incr_errors(Module0, Module) },
+ report_unbound_tvars_in_class_context(UnboundTVars, ArgTypes,
+ TVarSet, PredOrFunc, PredName, Context)
+ ).
+
+:- pred constrained_tvar_not_in_arg_types(class_constraints, list(type), tvar).
+:- mode constrained_tvar_not_in_arg_types(in, in, out) is nondet.
+
+constrained_tvar_not_in_arg_types(ClassContext, ArgTypes, TVar) :-
+ ClassContext = constraints(UnivCs, ExistCs),
+ ( Constraints = UnivCs ; Constraints = ExistCs ),
+ type_util__constraint_list_get_tvars(Constraints, TVars),
+ list__member(TVar, TVars),
+ \+ term__contains_var_list(ArgTypes, TVar).
+
+:- pred report_unbound_tvars_in_class_context(list(tvar), list(type), tvarset,
+ pred_or_func, sym_name, prog_context,
+ io__state, io__state).
+:- mode report_unbound_tvars_in_class_context(in, in, in, in, in, in,
+ di, uo) is det.
+
+/*
+The error message is intended to look like this:
+
+very_long_module_name:001: In declaration for function `very_long_function/2':
+very_long_module_name:001: error in type class constraints: type variables
+very_long_module_name:001: `T1, T2, T3' occur only in the constraints,
+very_long_module_name:001: not in the function's argument or result types.
+
+very_long_module_name:002: In declaration for predicate `very_long_predicate/3':
+very_long_module_name:002: error in type class constraints: type variable
+very_long_module_name:002: `T' occurs only in the constraints,
+very_long_module_name:002: not in the predicate's argument types.
+*/
+
+report_unbound_tvars_in_class_context(UnboundTVars, ArgTypes, TVarSet,
+ PredOrFunc, PredName, Context) -->
+ io__set_exit_status(1),
+ prog_out__write_context(Context),
+ io__write_string("In declaration for "),
+ { list__length(ArgTypes, Arity) },
+ hlds_out__write_simple_call_id(PredOrFunc, PredName, Arity),
+ io__write_string(":\n"),
+ prog_out__write_context(Context),
+ io__write_string(" error in type class constraints: "),
+ (
+ { UnboundTVars = [] },
+ { error("report_unbound_tvars_in_class_context: no type vars") }
+ ;
+ { UnboundTVars = [SingleTVar] },
+ io__write_string("type variable\n"),
+ prog_out__write_context(Context),
+ io__write_string(" `"),
+ mercury_output_var(SingleTVar, TVarSet, no),
+ io__write_string("' occurs ")
+ ;
+ { UnboundTVars = [_, _ | _] },
+ io__write_string("type variables\n"),
+ prog_out__write_context(Context),
+ io__write_string(" `"),
+ mercury_output_vars(UnboundTVars, TVarSet, no),
+ io__write_string("' occur ")
+ ),
+ io__write_string("only in the constraints,\n"),
+ prog_out__write_context(Context),
+ io__write_string(" not in the "),
+ (
+ { PredOrFunc = predicate },
+ io__write_string("predicate's argument types.\n")
+ ;
+ { PredOrFunc = function },
+ io__write_string("function's argument or result types.\n")
+ ).
+
+%-----------------------------------------------------------------------------%
+
:- pred maybe_check_field_access_function(sym_name, arity, import_status,
prog_context, module_info, io__state, io__state).
:- mode maybe_check_field_access_function(in, in, in, in, in, di, uo) is det.
Index: compiler/prog_io.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io.m,v
retrieving revision 1.190
diff -u -d -r1.190 prog_io.m
--- compiler/prog_io.m 2000/09/15 11:24:56 1.190
+++ compiler/prog_io.m 2000/08/16 06:45:04
@@ -1411,7 +1411,7 @@
convert_constructors(ModuleName, Body, Constrs)
->
% check that all type variables in the body
- % are either explicitly existentally quantified
+ % are either explicitly existentially quantified
% or occur in the head.
(
list__member(Ctor, Constrs),
@@ -1451,7 +1451,7 @@
\+ term__contains_var_list(CtorArgTypes, Var)
->
Result = error(
- "type variable does not occur in arguments of constructor",
+"type variable in existential quantifier does not occur in arguments of constructor",
Body)
% check that all type variables in existential constraints
% occur in the existential quantifiers
@@ -1465,8 +1465,8 @@
Ctor = ctor(ExistQVars, Constraints, _CtorName,
_CtorArgs),
list__member(Constraint, Constraints),
- Constraint = constraint(_Name, Args),
- term__contains_var_list(Args, Var),
+ Constraint = constraint(_Name, ConstraintArgs),
+ term__contains_var_list(ConstraintArgs, Var),
\+ list__member(Var, ExistQVars)
->
Result = error("type variables in class constraints introduced with `=>' must be explicitly existentially quantified using `some'",
Index: compiler/prog_io_typeclass.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io_typeclass.m,v
retrieving revision 1.14
diff -u -d -r1.14 prog_io_typeclass.m
--- compiler/prog_io_typeclass.m 2000/07/06 06:25:14 1.14
+++ compiler/prog_io_typeclass.m 2000/08/16 08:44:07
@@ -110,8 +110,24 @@
Result0 = ok(typeclass(_, Name, Vars, Interface,
VarSet0))
->
- Result = ok(typeclass(ConstraintList, Name, Vars,
- Interface, VarSet0))
+ (
+ %
+ % check for type variables in the constraints
+ % which do not occur in the type class
+ % parameters
+ %
+ type_util__constraint_list_get_tvars(
+ ConstraintList, ConstrainedVars),
+ list__member(Var, ConstrainedVars),
+ \+ list__member(Var, Vars)
+ ->
+ Result = error(
+"type variable in superclass constraint is not a parameter of this type class",
+ Constraints)
+ ;
+ Result = ok(typeclass(ConstraintList, Name,
+ Vars, Interface, VarSet0))
+ )
;
% if the item we get back isn't a typeclass,
% something has gone wrong...
@@ -474,8 +490,10 @@
ParsedNameAndTypes = ok(instance(Constraints,
NameString, Types, _, _))
->
- Result = ok(instance(Constraints, NameString, Types,
- concrete(MethodList), TVarSet))
+ Result0 = ok(instance(Constraints, NameString, Types,
+ concrete(MethodList), TVarSet)),
+ check_tvars_in_instance_constraint(Result0, Name,
+ Result)
;
% if the item we get back isn't a typeclass,
% something has gone wrong...
@@ -484,6 +502,33 @@
;
ParsedMethods = error(String, Term),
Result = error(String, Term)
+ ).
+
+:- pred check_tvars_in_instance_constraint(maybe1(item), term, maybe1(item)).
+:- mode check_tvars_in_instance_constraint(in, in, out) is det.
+
+check_tvars_in_instance_constraint(error(M,E), _, error(M, E)).
+check_tvars_in_instance_constraint(ok(Item), InstanceTerm, Result) :-
+ ( Item = instance(Constraints, _Name, Types, _Methods, _TVarSet) ->
+ %
+ % check that all of the type variables in the constraints
+ % on the instance declaration also occur in the type class
+ % argument types in the instance declaration
+ %
+ (
+ type_util__constraint_list_get_tvars(Constraints,
+ TVars),
+ list__member(TVar, TVars),
+ \+ term__contains_var_list(Types, TVar)
+ ->
+ Result = error(
+ "unbound type variable(s) in constraints on instance declaration",
+ InstanceTerm)
+ ;
+ Result = ok(Item)
+ )
+ ;
+ error("check_tvars_in_constraint: expecting instance item")
).
:- pred parse_instance_methods(module_name, term,
Index: tests/invalid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/Mmakefile,v
retrieving revision 1.69
diff -u -d -r1.69 Mmakefile
--- tests/invalid/Mmakefile 2000/09/16 00:08:12 1.69
+++ tests/invalid/Mmakefile 2000/08/16 08:50:06
@@ -84,6 +84,7 @@
types.m \
type_spec.m \
unbound_inst_var.m \
+ unbound_type_vars.m \
undef_lambda_mode.m \
undef_mode.m \
undef_mode_and_no_clauses.m \
Index: tests/invalid/type_vars.err_exp
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/type_vars.err_exp,v
retrieving revision 1.1
diff -u -d -r1.1 type_vars.err_exp
--- tests/invalid/type_vars.err_exp 2000/09/15 11:25:01 1.1
+++ tests/invalid/type_vars.err_exp 2000/08/16 06:50:31
@@ -1,4 +1,5 @@
-type_vars.m:006: Error: type variable does not occur in arguments of constructor: some [_1, _2] foo(_1) => c(_2).
-type_vars.m:007: Error: type variable does not occur in arguments of constructor: some [_1, _2] bar(_1).
+type_vars.m:006: Error: type variable in existential quantifier does not occur in arguments of constructor: some [_1, _2] foo(_1) => c(_2).
+type_vars.m:007: Error: type variable in existential quantifier does not occur in arguments of constructor: some [_1, _2] bar(_1).
type_vars.m:008: Error: type variable has overlapping scopes (explicit type quantifier shadows argument type): some [_1] bar(_1).
+type_vars.m:009: Error: type variables in class constraints introduced with `=>' must be explicitly existentially quantified using `some': some [_1] bar(_1) => c(_2).
For more information, try recompiling with `-E'.
Index: tests/invalid/type_vars.m
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/type_vars.m,v
retrieving revision 1.1
diff -u -d -r1.1 type_vars.m
--- tests/invalid/type_vars.m 2000/09/15 11:25:01 1.1
+++ tests/invalid/type_vars.m 2000/08/16 05:54:55
@@ -3,6 +3,7 @@
:- typeclass c(T) where [].
-:- type t1 ---> some [T1, T2] foo(T1) => c(T2).
-:- type t2 ---> some [T1, T2] bar(T1).
-:- type t3(T1) ---> some [T1] bar(T1).
+:- type t1 ---> some [T1, T2] foo(T1) => c(T2). % T2 doesn't occur in ctor args
+:- type t2 ---> some [T1, T2] bar(T1). % T2 occurs only in quantifier
+:- type t3(T1) ---> some [T1] bar(T1). % T1 has overlapping scope
+:- type t4 ---> some [T1] bar(T1) => c(T2). % T2 occurs only in constraint
Index: tests/invalid/unbound_type_vars.err_exp
===================================================================
RCS file: unbound_type_vars.err_exp
diff -N unbound_type_vars.err_exp
--- /dev/null Thu Mar 30 14:06:13 2000
+++ unbound_type_vars.err_exp Wed Aug 16 18:49:56 2000
@@ -0,0 +1,23 @@
+unbound_type_vars.m:014: Error: type variable in superclass constraint is not a parameter of this type class: c1(_1, _2).
+unbound_type_vars.m:018: Error: unbound type variable(s) in constraints on instance declaration: c1(int, float) <= c3(_1).
+unbound_type_vars.m:021: In declaration for predicate `unbound_type_vars:p1/1':
+unbound_type_vars.m:021: error in type class constraints: type variable
+unbound_type_vars.m:021: `T2' occurs only in the constraints,
+unbound_type_vars.m:021: not in the predicate's argument types.
+unbound_type_vars.m:024: In declaration for predicate `unbound_type_vars:p2/2':
+unbound_type_vars.m:024: error in type class constraints: type variable
+unbound_type_vars.m:024: `T3' occurs only in the constraints,
+unbound_type_vars.m:024: not in the predicate's argument types.
+unbound_type_vars.m:028: In declaration for predicate `unbound_type_vars:p3/1':
+unbound_type_vars.m:028: error in type class constraints: type variable
+unbound_type_vars.m:028: `T2' occurs only in the constraints,
+unbound_type_vars.m:028: not in the predicate's argument types.
+unbound_type_vars.m:031: In declaration for predicate `unbound_type_vars:p4/1':
+unbound_type_vars.m:031: error in type class constraints: type variable
+unbound_type_vars.m:031: `T2' occurs only in the constraints,
+unbound_type_vars.m:031: not in the predicate's argument types.
+unbound_type_vars.m:034: In declaration for predicate `unbound_type_vars:p5/1':
+unbound_type_vars.m:034: error in type class constraints: type variable
+unbound_type_vars.m:034: `T2' occurs only in the constraints,
+unbound_type_vars.m:034: not in the predicate's argument types.
+For more information, try recompiling with `-E'.
Index: tests/invalid/unbound_type_vars.m
===================================================================
RCS file: unbound_type_vars.m
diff -N unbound_type_vars.m
--- /dev/null Thu Mar 30 14:06:13 2000
+++ unbound_type_vars.m Wed Aug 16 18:49:25 2000
@@ -0,0 +1,42 @@
+% This test case (tests/invalid/unbound_type_vars.m) tests that the
+% compiler reports errors for type variables which occur only
+% in type class constraints.
+% This test case covers the issue for typeclass declarations,
+% instance declarations, method declarations, and predicate declarations.
+% Tests of this issue for `:- type' declarations are covered in the
+% `tests/invalid/type_vars.m' test case.
+
+:- module unbound_type_vars.
+:- interface.
+
+:- typeclass c1(T1, T2) where [].
+
+:- typeclass c2(T1) <= c1(T1, T2) where []. % T2 unbound (typeclass decl)
+
+:- typeclass c3(T1) where [].
+
+:- instance c1(int, float) <= c3(T1) where []. % T1 unbound (instance decl)
+
+:- typeclass c3(T1, T2) where [
+ pred p1(T1), % T2 unbound (method decl,
+ mode p1(in) is det, % type var from typeclass decl)
+
+ pred p2(T1, T2) <= c1(T1, T3), % T3 unbound (method decl,
+ mode p2(in, in) is det % type var from method decl)
+].
+
+:- pred p3(T1) <= c1(T1, T2). % T2 unbound (pred decl)
+:- mode p3(in) is det.
+
+:- all [T1, T2] pred p4(T1) <= c1(T1, T2). % T2 still unbound (pred decl
+:- mode p4(in) is det. % with universal quantifier)
+
+:- some [T2] pred p5(T1) <= c1(T1, T2). % T2 still unbound (pred decl
+:- mode p5(in) is det. % with existential quantifier)
+
+:- implementation.
+
+p3(_).
+p4(_).
+p5(_).
+
--
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.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to: mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions: mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------
More information about the developers
mailing list