[m-dev.] for review: handle non-simple typeclass constraints

[Fergus Henderson]

On 08-Apr-1998, David Glen JEFFERY <dgj at cs.mu.OZ.AU> wrote:
> > compiler/prog_data.m:
> > 	Document the invariant that the types in a type class constraint
> > 	must not contain any information in their term__context fields.
> 
> I'm not sure that this is strictly necessary, but now that it's implemented,
> certainly leave it there for safety's sake.

Enforcing this invariant seemed to me to be the only way of reliably
ensuring that thing would work.

When I tested this change the first time, I got a `map__lookup failed' error,
which was due to a lookup in the class constraint proof map failing.
I didn't see any way of fixing this except to ensure that class constraints
that inserted into the map or used to look up the map never had term__contexts.
And then it seemed simplest to just require that *all* class constraints
not have term__contexts.

> > compiler/check_typeclass.m:
> > 	When checking superclass conformance for instance declarations,
> > 	pass `[]' for the extra "DeclaredConstraints" argument that is
> > 	now needed by typecheck__reduce_context_by_rule_application.
> 
> I think there is a better way than this (see comment below).
...
> >  			% Reduce the superclass constraints
> >  		typecheck__reduce_context_by_rule_application(InstanceTable, 
> > -			ClassTable, TypeSubst, InstanceVarSet1, InstanceVarSet2,
> > +			ClassTable, [], TypeSubst,
> > +			InstanceVarSet1, InstanceVarSet2,
> >  			Proofs0, Proofs1, SuperClasses, 
> >  			ReducedSuperClasses0),
> >  
> >  			% Reduce the constraints from the instance declaration
> >  		typecheck__reduce_context_by_rule_application(InstanceTable, 
> > -			ClassTable, TypeSubst, InstanceVarSet2, InstanceVarSet2,
> > +			ClassTable, [], TypeSubst,
> > +			InstanceVarSet2, InstanceVarSet2,
> >  			Proofs1, Proofs2, InstanceConstraints,
> >  			ReducedInstanceConstraints0)
> 
> The whole point of doing these two steps separately is that you see if they
> reduce to the same thing. With the machinery you've just added, you should be
> able to replace the two calls above with:
>   		typecheck__reduce_context_by_rule_application(InstanceTable, 
> 			ClassTable, TypeSubst, InstanceVarSet1, InstanceVarSet2,
> 			ClassTable, InstanceConstraints, TypeSubst,
> 			InstanceVarSet1, InstanceVarSet2,
> 			Proofs0, Proofs1, SuperClasses, 
> 			[]),
> 
> (or something like that... with appropriate variable renaming, of course).

Oh, I see.  Yes, that is much nicer.

> > Index: typecheck.m
> > ===================================================================
> > RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
> > retrieving revision 1.233
> > diff -u -u -r1.233 typecheck.m
> > --- typecheck.m	1998/03/30 13:28:13	1.233
> > +++ typecheck.m	1998/04/08 03:52:01
> >  			% "Type classes: an exploration of the design
> >  			% space", S.P. Jones, M. Jones 1997.
> 
> Oops. "Peyton" is not Simon Peyton-Jones' middle name. Could you fix that in
> this change too?

Sure.

> > -% perform_context_reduction(TypeCheckInfo0, TypeCheckInfo) is true iff
> > +% perform_context_reduction(OrigTypeAssignSet, TypeCheckInfo0, TypeCheckInfo)
> > +%	is true iff either
> >  % 	TypeCheckInfo is the typecheck_info that results from performing
> > -% 	context reduction on the type_assigns in TypeCheckInfo0.
> > +% 	context reduction on the type_assigns in TypeCheckInfo0,
> > +%	or, if there is no valid context reduction, then
> > +%	TypeCheckInfo is TypeCheckInfo0 with the type assign set replaced by
> > +%	OrigTypeAssignSet.
> 
> Mention why you reset it to OrigTypeAssignSet. ie.  give the reason that you
> give in the log message.

The comment does explain that a just little (less than a screenful) later on.

> > -% 	are two ways in which a constraint may be redundant:
> > -% 		- if there is an instance declaration that may be applied, the
> > -% 		  constraint is replaced by the constraints from that instance
> > -% 		  declaration
> > +% 	are three ways in which a constraint may be redundant:
> > +%		- if a constraint occurs in the pred/func declaration for this
> > +%		  predicate or function, then it is redundant
> 
> Seeing that you explicitly talk about the three ways, you should mention
> why the constraint_proofs don't need to record the first. (ie. because
> information is trivially reconstructed by the first stages of the 
> transformation in polymorphism.m).

OK.

> > +		DeclaredConstraints, Bindings, Tvarset0, Tvarset,
> > +		Proofs0, Proofs, Constraints0, Constraints) :-
> > +	apply_rec_subst_to_constraints(Bindings, Constraints0, Constraints1),
> > +	eliminate_declared_constraints(Constraints1, DeclaredConstraints,
> > +		Constraints2, Changed1),
> > +	apply_class_rules(Constraints2, ClassTable, Tvarset0,
> > +		Proofs0, Proofs1, Constraints3, Changed2),
> > +	apply_instance_rules(Constraints3, InstanceTable, 
> > +		Tvarset0, Tvarset1, Proofs1, Proofs2, Constraints4, Changed3),
> 
> Any reason why you've put the class rules before the instance rules? If so,
> add a comment.

Yes.  I will document it.

[Another diff will follow.]

> BTW, we still don't do the "search" for super classes do we?

No.  I'm going to leave that one for you to do ;-)

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