[m-rev.] for review: type_spec and typeclass constraints

[Mark Brown]

This is for review by Simon.

Estimated hours taken: 5
Branches: main

When specializing the type of a pred/func with class constraints on it,
make sure any constraints which become ground are removed from the
specialized version.  The presence of ground constraints was causing
dictionaries to be passed around unnecessarily, and these cases were not
always caught by unused arg elimination.

This change means that the compiler will have to prove the constraints
are satisfied using instance declarations visible at the point of the
pragma type_spec, instead of requiring the caller to supply a proof.

compiler/type_util.m:
	Add a predicate that removes ground constraints from a class
	context.

compiler/make_hlds.m:
	After the substitution has been applied to the class context,
	call the new predicate.

tests/invalid/Mmakefile:
tests/invalid/constrained_type_spec.err_exp:
tests/invalid/constrained_type_spec.m:
	A test case.

Index: compiler/make_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.423
diff -u -r1.423 make_hlds.m
--- compiler/make_hlds.m	2002/08/01 00:41:35	1.423
+++ compiler/make_hlds.m	2002/08/13 20:50:47
@@ -1270,7 +1270,21 @@
 			term__apply_rec_substitution_to_list(Types0,
 				TypeSubst, Types),
 			apply_rec_subst_to_constraints(TypeSubst,
-				ClassContext0, ClassContext),
+				ClassContext0, ClassContext1),
+			%
+			% Some constraints may have become completely ground
+			% in this process, which means that the caller of this
+			% predicate need not supply a proof of class membership
+			% (that is, a dictionary) for those constraints.  If we
+			% remove the ground constraints, then we will avoid
+			% generating the extra arguments that expect those
+			% proofs.  Instead, typechecking will be required to
+			% statically proof that the constraint is satisfied,
+			% because of the call to the non-specialized version
+			% of the predicate.
+			%
+			remove_ground_univ_constraints(ClassContext1,
+				ClassContext),
 			SubstOk = yes(TypeSubst),
 			ModuleInfo = ModuleInfo0
 			}
Index: compiler/type_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/type_util.m,v
retrieving revision 1.108
diff -u -r1.108 type_util.m
--- compiler/type_util.m	2002/06/30 17:06:41	1.108
+++ compiler/type_util.m	2002/08/13 20:47:11
@@ -467,6 +467,13 @@
 :- pred get_unconstrained_tvars(list(tvar), list(class_constraint), list(tvar)).
 :- mode get_unconstrained_tvars(in, in, out) is det.
 
+	% remove_ground_univ_constraints(Constraints0, Constraints).
+	%	Remove any ground constraints from the "universally
+	%	quantified" constraints.  These can be introduced by
+	%	type specialization, for example.
+:- pred remove_ground_univ_constraints(class_constraints, class_constraints).
+:- mode remove_ground_univ_constraints(in, out) is det.
+
 %-----------------------------------------------------------------------------%
 
 	% If possible, get the argument types for the cons_id.
@@ -1695,6 +1702,25 @@
 	constraint_list_get_tvars(Constraints, ConstrainedTvars),
 	list__delete_elems(Tvars, ConstrainedTvars, Unconstrained0),
 	list__remove_dups(Unconstrained0, Unconstrained).
+
+remove_ground_univ_constraints(Cs0, Cs) :-
+	Cs0 = constraints(UniversalCs0, ExistentialCs),
+	list__filter(constraint_is_not_ground, UniversalCs0, UniversalCs),
+	Cs = constraints(UniversalCs, ExistentialCs).
+
+:- pred constraint_is_not_ground(class_constraint).
+:- mode constraint_is_not_ground(in) is semidet.
+
+constraint_is_not_ground(constraint(_Name, Args)) :-
+	\+ terms_are_all_ground(Args).
+
+:- pred terms_are_all_ground(list(term(T))).
+:- mode terms_are_all_ground(in) is semidet.
+
+terms_are_all_ground([]).
+terms_are_all_ground([Term | Terms]) :-
+	term__is_ground(Term),
+	terms_are_all_ground(Terms).
 
 %-----------------------------------------------------------------------------%
 
Index: tests/invalid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/Mmakefile,v
retrieving revision 1.120
diff -u -r1.120 Mmakefile
--- tests/invalid/Mmakefile	2002/08/17 13:52:19	1.120
+++ tests/invalid/Mmakefile	2002/08/19 11:08:14
@@ -35,6 +35,7 @@
 	builtin_proc \
 	circ_type \
 	constrained_poly_insts \
+	constrained_type_spec \
 	constructor_warning \
 	det_errors \
 	duplicate_modes \
Index: tests/invalid/constrained_type_spec.err_exp
===================================================================
RCS file: constrained_type_spec.err_exp
diff -N constrained_type_spec.err_exp
--- /dev/null	Mon Dec 17 21:20:53 2001
+++ constrained_type_spec.err_exp	Wed Aug 14 09:29:51 2002
@@ -0,0 +1,4 @@
+constrained_type_spec.m:013: In clause for function `constrained_type_spec:TypeSpecOf__pred_or_func__f__[T = float]/1':
+constrained_type_spec.m:013:   unsatisfiable typeclass constraint(s):
+constrained_type_spec.m:013:   `constrained_type_spec:foo(float)'.
+For more information, try recompiling with `-E'.
Index: tests/invalid/constrained_type_spec.m
===================================================================
RCS file: constrained_type_spec.m
diff -N constrained_type_spec.m
--- /dev/null	Mon Dec 17 21:20:53 2001
+++ constrained_type_spec.m	Wed Aug 14 06:30:59 2002
@@ -0,0 +1,14 @@
+:- module constrained_type_spec.
+:- interface.
+
+:- typeclass foo(T) where [ func s(T) = int ].
+:- instance foo(int) where [ (s(_) = 1) ].
+
+:- func f(T) = int <= foo(T).
+
+:- implementation.
+
+f(X) = s(X).
+
+:- pragma type_spec(f/1, T = float).
+
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------