[m-dev.] for review: bug fix for multiparameter typeclasses
David Glen JEFFERY
dgj at students.cs.mu.oz.au
Fri Oct 13 16:49:01 AEDT 2000
Hi,
This one is for Fergus.
-----------------------------------------------------------------------------
Estimated hours taken: 8
Fix a bug recently reported by Nancy Mazur (and previously reported by
Tom Conway) which caused a type error to be reported for type correct
code involving multi parameter type classes. The type class constraint
elimination mechanism was not correctly handling the case where a multi
parameter typeclass declaration has a constraint which involved a (strict)
subset of the type variables of the class.
compiler/typecheck.m:
When searching the superclass relation, utilise the fact that any
new variables that are introduced (eg. by moving a single parameter
superclass to a multi parameter subclass) are effectively universally
quantified; they may be found to any other type (or type variable)
when checking for redundancy.
To achieve this, we pass a long a list of variables that we are
*not* allowed to bind. These are just the variables from the original
constraint. ie. all the non-introduced variables.
tests/hard_coded/typeclasses/Mmakefile:
tests/hard_coded/typeclasses/multi_parameter_bug.exp:
tests/hard_coded/typeclasses/multi_parameter_bug.m:
A test case for this.
-----------------------------------------------------------------------------
Index: compiler/typecheck.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/typecheck.m,v
retrieving revision 1.287
diff -u -t -r1.287 typecheck.m
--- compiler/typecheck.m 2000/10/10 06:22:54 1.287
+++ compiler/typecheck.m 2000/10/13 05:30:41
@@ -4108,7 +4108,10 @@
TVarSet, Proofs0, Proofs, Constraints, Changed) :-
(
Parents = [],
- eliminate_constraint_by_class_rules(C, AssumedConstraints,
+ C = constraint(_, CTypes),
+ term__vars_list(CTypes, CVars),
+ eliminate_constraint_by_class_rules(C, CVars,
+ AssumedConstraints,
SuperClassTable, TVarSet, Parents, Proofs0, Proofs1)
->
apply_class_rules(Constraints0, AssumedConstraints,
@@ -4127,15 +4130,21 @@
% is also passed in --- these are the constraints that we are
% (recursively) in the process of checking, and is used to ensure that
% we don't get into a cycle in the relation.
-:- pred eliminate_constraint_by_class_rules(class_constraint,
+ %
+ % The list(tvar) argument contains all the variables from the
+ % original constraint that we are trying to prove. (These are the
+ % type variables that must not be found as we search through the
+ % superclass relation).
+:- pred eliminate_constraint_by_class_rules(class_constraint, list(tvar),
list(class_constraint), superclass_table, tvarset,
list(class_constraint),
map(class_constraint, constraint_proof),
map(class_constraint, constraint_proof)).
-:- mode eliminate_constraint_by_class_rules(in, in, in, in, in, in, out)
+:- mode eliminate_constraint_by_class_rules(in, in, in, in, in, in, in, out)
is semidet.
-eliminate_constraint_by_class_rules(C, AssumedConstraints, SuperClassTable,
+eliminate_constraint_by_class_rules(C, ConstVars,
+ AssumedConstraints, SuperClassTable,
TVarSet, ParentConstraints, Proofs0, Proofs) :-
% Make sure we aren't in a cycle in the
@@ -4150,8 +4159,8 @@
% Convert all the subclass_details into class_constraints by
% doing the appropriate variable renaming and applying the
% type variable bindings.
- SubDetailsToConstraint = lambda([SubClassDetails::in, SubC::out]
- is semidet, (
+ SubDetailsToConstraint = (pred(SubClassDetails::in, SubC::out)
+ is det :-
SubClassDetails = subclass_details(SuperVars0, SubID,
SubVars0, SuperVarset),
@@ -4169,21 +4178,41 @@
% Work out what the (renamed) vars from the
% typeclass declaration are bound to here
map__init(Empty),
- type_unify_list(SuperVars, SuperClassTypes, [],
- Empty, Bindings),
- SubID = class_id(SubName, _SubArity),
- term__apply_substitution_to_list(SubVars, Bindings,
- SubClassTypes),
- SubC = constraint(SubName, SubClassTypes)
- )),
+ (
+ type_unify_list(SuperVars, SuperClassTypes, [],
+ Empty, Bindings)
+ ->
+ SubID = class_id(SubName, _SubArity),
+ term__apply_substitution_to_list(SubVars, Bindings,
+ SubClassTypes),
+ SubC = constraint(SubName, SubClassTypes)
+ ;
+ error("eliminate_constraint_by_class_rules: type_unify_list failed")
+ )
+ ),
list__map(SubDetailsToConstraint, SubClasses, SubClassConstraints),
(
- % Do the first level of search
- FindSub = lambda([TheConstraint::in] is semidet,(
- list__member(TheConstraint, AssumedConstraints)
- )),
- list__filter(FindSub, SubClassConstraints, [Sub|_])
+ % Do the first level of search. We search for
+ % a assumed constraint which unifies with any
+ % of the subclass constraints.
+ NotSub = (pred(TheConstraint::in) is semidet :-
+ not (some [SubConstraint] (
+ TheConstraint = constraint(TheConstraintClass,
+ TheConstraintTypes),
+ list__member(SubClassConstraint,
+ SubClassConstraints),
+ SubClassConstraint =
+ constraint(TheConstraintClass,
+ SubClassConstraintTypes),
+ map__init(EmptySub),
+ type_unify_list(SubClassConstraintTypes,
+ TheConstraintTypes,
+ ConstVars, EmptySub, _)
+ ))
+ ),
+ list__takewhile(NotSub, AssumedConstraints, _, Subs),
+ Subs = [Sub|_]
->
map__set(Proofs0, C, superclass(Sub), Proofs)
;
@@ -4191,14 +4220,14 @@
% Recursively search the rest of the superclass
% relation.
- SubClassSearch = lambda([Constraint::in, CnstrtAndProof::out]
- is semidet, (
- eliminate_constraint_by_class_rules(Constraint,
- AssumedConstraints, SuperClassTable,
+ SubClassSearch = (pred(Constraint::in, CnstrtAndProof::out)
+ is semidet :-
+ eliminate_constraint_by_class_rules(Constraint,
+ ConstVars, AssumedConstraints, SuperClassTable,
TVarSet, NewParentConstraints,
Proofs0, SubProofs),
CnstrtAndProof = Constraint - SubProofs
- )),
+ ),
% XXX this could (and should) be more efficient.
% (ie. by manually doing a "cut").
find_first(SubClassSearch, SubClassConstraints,
Index: tests/hard_coded/typeclasses/Mmakefile
===================================================================
RCS file: /home/staff/zs/imp/tests/hard_coded/typeclasses/Mmakefile,v
retrieving revision 1.38
diff -u -t -r1.38 Mmakefile
--- tests/hard_coded/typeclasses/Mmakefile 2000/10/10 23:39:34 1.38
+++ tests/hard_coded/typeclasses/Mmakefile 2000/10/13 05:38:19
@@ -37,6 +37,7 @@
multi_constraint_same_tvar \
multi_moded \
multi_parameter \
+ multi_parameter_bug \
nondet_class_method \
operator_classname \
record_syntax \
New File: tests/hard_coded/typeclasses/multi_parameter_bug.exp
===================================================================
42
New File: tests/hard_coded/typeclasses/multi_parameter_bug.m
===================================================================
:- module multi_parameter_bug.
:- interface.
:- import_module io.
:- pred main(io__state::di, io__state::uo) is det.
:- implementation.
:- import_module int, char.
main -->
p(42, 'a').
:- pred p(T1, T2, io__state, io__state) <= c2(T1, T2).
:- mode p(in, in, di, uo) is det.
p(X, _) -->
{ m1(X, Y) },
io__write_int(Y),
io__nl.
:- typeclass c1(T) where [
pred m1(T, int),
mode m1(in, out) is det
].
:- typeclass c2(T1, T2) <= c1(T1) where [
].
:- instance c1(int) where [
m1(X,X)
].
:- instance c2(int, char) where [
].
dgj
--
David Jeffery (dgj at cs.mu.oz.au) | If your thesis is utterly vacuous
PhD student, | Use first-order predicate calculus.
Dept. of Comp. Sci. & Soft. Eng.| With sufficient formality
The University of Melbourne | The sheerist banality
Australia | Will be hailed by the critics: "Miraculous!"
| -- Anon.
--------------------------------------------------------------------------
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