[m-rev.] for review: allow arbitrary types in class constraints

[David Jeffery]

> Hi,
>
> This change would probably be best reviewed by Fergus or DJ, but since
> I'm not sure whether either of them is able to do it at the moment, if
> anyone else wants to that would be great.

Hi David,

Just some brief comments for now. The good news is that I'll be in Melbourne
from next Monday (the 15th) for about 2 weeks, so you can hassle me
about it then. ;-)

> Estimated hours taken: 25
> Branches: main
>
>
> Allow constraints on pred/func, instance and typeclass declarations to
> constraint arbitrary types rather than just type variables.  The only
> restriction is that each constraint must contain at least one type
> variable and that all type variables in the constraint must also occur
> somewhere else in the declaration.
>
> compiler/prog_io_typeclass.m:
> When parsing class constraints (on pred/func, instance and
> typeclass declarations) remove the restriction that the
> arguments must all be variables.  Instead, ensure that at least
> one argument contains at least one variable.
>
> compiler/hlds_data.m:
> compiler/hlds_out.m:
> compiler/make_hlds.m:
> Allow superclass constraints to have arguments of arbitrary type
> (rather than just variables) in the superclass table.

OK, problem here.

Without some kind of restriction on the constraints on instance
and typeclass declarations, type checking cannot be gauranteed
to terminate. (Well, at least not the way that we implement it at
the moment... you can always gaurantee termination by limiting the
number of iterations that the type checker does, in much the same
way that we manage to gaurantee termination when inferring types
in the presence of polymorphic recursion. But we don't.).

For example, applying the instance declaration:

:- instance c(f(T)) <= c(f(f(T))).

is almost certainly going to give you troubles when trying to satisfy
a 'f(...)' constraint on a pred call.

...and similarly for typeclass declarations. e.g. given the following
declaration:

:- typeclass c(T) <= c(f(T)) where [...].

then checking the correctness of an instance declaration for 'c' is
going to result in an infinite loop. e.g. for 'c(int)' to be a valid
instance, the typeclass declaration makes us check that
c(f(int)) is valid, and in turn that c(f(f(int))) is valid, ad infinitum.

But there shouldn't be any problems with allowing 'arbitrary'
constraints on predicate types.

I'm going to have to leave it there... I'll discuss it with you in
person next week.


dgj
---
David Jeffery (dgj at missioncriticalit.com)
Software Engineer,
Mission Critical


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