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

[David Glen JEFFERY]

On 08-Apr-1998, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> Hi,
> 
> DJ, can you please review this one?

Certainly... and I'll start off with a big thank you. I was just about to
check out a new version of the compiler to work on this one, and mail appears
telling me that it's already done. If only all bug-fixes worked like this! :-)

> 
> --------------------------------------------------
> 
> Estimated hours taken: 10
> 
> Fix some bugs in the handling of "non-simple" type class constraints
> (ones for which the types being constrained are not just type variables).
> 
> compiler/prog_io_typeclass.m:
> 	Ensure that constraints on type class declarations must be "simple".
> 	This is needed the ensure termination of type checking.
> 	(We already did this for instance declarations, but not for
> 	superclass constraints on type class declarations.)
> 
> 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.

> compiler/type_util.m:
> compiler/equiv_type.m:
> compiler/polymorphism.m:
> compiler/prog_io_typeclass.m:
> 	Enforce the above-mentioned invariant.
> 	
> compiler/typecheck.m:
> 	Allow the declared constraints to be a superset of the
> 	inferred constraints.
> 	When performing context reduction, eliminate declared
> 	constraints at each step rather than only at the end.
> 	Remove declared constraints and apply superclass rules
> 	before applying instance rules.
> 	When applying instance rules, make sure that it is a type
> 	error if there is no matching instance rule for a ground
> 	constraint.
> 	If context reduction results in an error, restore the
> 	original type assign set, to avoid repeating the same
> 	error message at every subsequent call to perform_context_reduction.
> 
> 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).

> cvs diff: Diffing .
> Index: check_typeclass.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/check_typeclass.m,v
> retrieving revision 1.4
> diff -u -u -r1.4 check_typeclass.m
> --- check_typeclass.m	1998/03/03 17:33:38	1.4
> +++ check_typeclass.m	1998/04/08 02:10:51
> @@ -448,13 +448,15 @@
>  	(
>  			% 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).

This can be a separate change, though.

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

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

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

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

BTW, we still don't do the "search" for super classes do we? I'll put that on
my TODO list. (Which probably means you can finish that one before I start it
too  ;-) ).

Once you have addressed the points above, please commit it.

Thanks again.


love and cuddles,
dgj
-- 
David Jeffery (dgj at cs.mu.oz.au) |  Marge: Did you just call everyone "chicken"?
MEngSc student,                 |  Homer: Noooo.  I swear on this Bible!
Department of Computer Science  |  Marge: That's not a Bible; that's a book of
University of Melbourne         |         carpet samples!
Australia                       |  Homer: Ooooh... Fuzzy.