[m-rev.] for review: use typeclass constraints to help resolve overloading

[David Jeffery]

Hi Pete,

Thanks for this one. I've pointed out a few problems and how you might fix
them further down in the code.


dgj

----- Original Message -----
From: "Peter Ross" <petdr at cs.mu.OZ.AU>
To: "Mercury Reviews" <mercury-reviews at cs.mu.OZ.AU>
Sent: Wednesday, January 16, 2002 5:15 AM
Subject: [m-rev.] for review: use typeclass constraints to help resolve
overloading


> ===================================================================
>
>
> Estimated hours taken: 3
> Branches: main
>
> compiler/typecheck.m:
>     When resolving predicate overloading to a typeclass method use the
>     instance declarations to help resolve the overloading.
>
> tests/hard_coded/typeclasses/Mmakefile:
> tests/hard_coded/typeclasses/overload.exp:
> tests/hard_coded/typeclasses/overload.m:
>     A test case.

The log message could really be improved... I had to look at the code and
test case quite carefully to work out what problem you were trying to fix.

The log message is also slightly inaccurate: this is not actually about
resolving
overloading for typeclass methods... it is about resolving overloading for
any
predicate. If you replace the method call in your test case with a call to
an
overloaded, class contrained function you get exactly the same behaviour.

e.g.
...
main --> io__write(f(5)), io__nl.

:- typeclass c1(T) where [].
:- instance c1(int).
:- func f(T) = int <= c1(T).
f(_) = 1.
:- import_module overload__sub.
:- module sub.
:- interface.
:- typeclass c2(T) where [].
:- instance c2(string).
:- func f(T) = int <= c2(T).
:- implementation.
f(_) = 9876.
:- end_module sub.

> Index: compiler/typecheck.m
> ===================================================================
> RCS file: /home/staff/zs/imp/mercury/compiler/typecheck.m,v
> retrieving revision 1.308
> diff -u -r1.308 typecheck.m
> --- compiler/typecheck.m 25 Sep 2001 09:36:55 -0000 1.308
> +++ compiler/typecheck.m 16 Jan 2002 04:11:17 -0000
> @@ -1587,7 +1587,11 @@
>   PredArgTypes0),
>
>   arg_type_list_subsumes(TVarSet, ArgTypes,
> - PredTVarSet, PredExistQVars0, PredArgTypes0)
> + PredTVarSet, PredExistQVars0, PredArgTypes0),
> +
> + % We also need to check the universal typeclass constraints.
> + check_univ_constraints(ModuleInfo, PredInfo,
> + ArgTypes, PredArgTypes0)
>   ->
>   %
>   % we've found a matching predicate
> @@ -1610,6 +1614,69 @@
>   typecheck__find_matching_pred_id(PredIds, ModuleInfo,
>   TVarSet, ArgTypes, ThePredId, PredName)
>   ).
> +
> + % check_univ_constraints(MI, PI, ArgTypes, PredArgTypes)
> + %
> + % For each universally constrained type variable in
> + % PredArgTypes, check that the corresponding type in ArgTypes
> + % has an instance declaration.  The predicate succeeds if this
> + % test succeeds for each constrained type variable.

This seems rather odd... surely you should iterate over the constraints
rather than the type variables. Also, I'm not sure what "check that
the corresponding type in ArgTypes has an instance declaration"
could mean. An instance for which type class?

Anyhow, all the code from here downwards seems to reproduce the logic
done by 'context reduction' in typecheck.m. I haven't gone over the
code closely because I think that rather than reproducing that logic
(and it's quite hard to get right), you should call the context reduction
code directly.

Basically, you should use typecheck__reduce_context_by_rule_application
and check that the set of reduced set of constraints that is returned is
empty.

This will allow you to use all the machinery of context reduction rather
than just checking that there is an instance for each constraint.
(Constraints can also be satisfied by constraints in the calling predicate
or by using a superclass constraint... and that process can be recursive.
You really don't want to reproduce that logic).

I think you should either add a call to
typecheck__reduce_context_by_rule_application straight after
the call to arg_type_list_subsumes, or an even better idea might be to
change the interface to arg_type_list_subsumes and make it check
constraints using typecheck__reduce_context_by_rule_application
instead. (The only other place that seems to use arg_type_list_subsumes
is also doing overloading resolution, and there is a comment there to
the effect that it is ignoring constraints for now).

> + % eg If we call predicate p with type signature p(int) and p is a
> + % member of the typeclass tc(T) with the type signature p(T).
> + % Then check whether or not there is an instance tc(int).
> + %
> +:- pred check_univ_constraints(module_info::in, pred_info::in,
> + list(type)::in, list(type)::in) is semidet.
> +
> +check_univ_constraints(_ModuleInfo, _PredInfo, [], []).
> +check_univ_constraints(ModuleInfo, PredInfo,
> + [ArgType | ArgTypes], [PredArg | PredArgs]) :-
> + obeys_universal_constraints(ModuleInfo, PredInfo, ArgType, PredArg),
> + check_univ_constraints(ModuleInfo, PredInfo,
> + ArgTypes, PredArgs).
> +
> +:- pred obeys_universal_constraints(module_info::in, pred_info::in,
> + (type)::in, (type)::in) is semidet.
> +
> +obeys_universal_constraints(ModuleInfo, PredInfo, ArgType, PredArgType)
:-
> + ( PredArgType = term__variable(_TVar) ->
> + pred_info_get_class_context(PredInfo, ClassConstraints),
> + ClassConstraints = constraints(Univs, _Exist),
> +
> + % Get the Univ constraints which mention TVar
> + list__filter_map((pred(C::in, {N, C}::out) is semidet :-
> + C = constraint(_CName, CTypes),
> + list__nth_member_search(CTypes, PredArgType, N)
> + ), Univs, TVarUnivs),
> +
> + % Ensure that there exists at least one instance
> + % declaration with ArgType for each typeclass
> + % constraint.
> + list__filter(instance_decl_exists(ModuleInfo, ArgType),
> + TVarUnivs, _Compatible, Incompatible),
> + Incompatible = []
> + ;
> + true
> + ).
> +
> +:- pred instance_decl_exists(module_info::in, (type)::in,
> + {int, class_constraint}::in) is semidet.
> +
> +instance_decl_exists(ModuleInfo, ArgType, {N, constraint(Name, Types)})
:-
> + module_info_instances(ModuleInfo, Instances),
> + map__lookup(Instances, class_id(Name, list__length(Types)),
> + InstanceDefns),
> + list__filter((pred(InstanceDefn::in) is semidet :-
> + InstanceDefn = hlds_instance_defn(_, _, _, _,
> + InstanceTypes, _, _, _, _),
> + list__index1_det(InstanceTypes, N, InstanceType),
> + type_list_subsumes([ArgType], [InstanceType], _)
> + ), InstanceDefns, Compatible, _Incompatible),
> +
> + % There must be at least one instance declaration which
> + % metions the ArgType.
> + Compatible = [_ | _].
>
>
%---------------------------------------------------------------------------
--%
>
> Index: tests/hard_coded/typeclasses/Mmakefile
> ===================================================================
> RCS file: /home/staff/zs/imp/tests/hard_coded/typeclasses/Mmakefile,v
> retrieving revision 1.44
> diff -u -r1.44 Mmakefile
> --- tests/hard_coded/typeclasses/Mmakefile 12 Feb 2001 05:14:57 -0000 1.44
> +++ tests/hard_coded/typeclasses/Mmakefile 16 Jan 2002 04:08:57 -0000
> @@ -41,6 +41,7 @@
>   multi_parameter_bug \
>   nondet_class_method \
>   operator_classname \
> + overload \
>   record_syntax \
>   reordered_existential_constraint \
>   superclass_bug \
> Index: tests/hard_coded/typeclasses/overload.exp
> ===================================================================
> RCS file: tests/hard_coded/typeclasses/overload.exp
> diff -N tests/hard_coded/typeclasses/overload.exp
> --- /dev/null 1 Jan 1970 00:00:00 -0000
> +++ tests/hard_coded/typeclasses/overload.exp 16 Jan 2002 04:08:32 -0000
> @@ -0,0 +1 @@
> +5

Maybe this test case should use the version I put above (underneath the
log message). I'm not sure which is more appropriate. (Maybe put both).

> Index: tests/hard_coded/typeclasses/overload.m
> ===================================================================
> RCS file: tests/hard_coded/typeclasses/overload.m
> diff -N tests/hard_coded/typeclasses/overload.m
> --- /dev/null 1 Jan 1970 00:00:00 -0000
> +++ tests/hard_coded/typeclasses/overload.m 16 Jan 2002 04:09:51 -0000
> @@ -0,0 +1,35 @@
> +% Check that we can resolve unambigiously which call to f/1 we mean, by
> +% checking the typeclass constraints on f.
> +:- module overload.
> +:- interface.
> +:- import_module io.
> +
> +:- pred main(io__state::di, io__state::uo) is det.
> +
> +:- implementation.
> +
> +:- typeclass tc(T) where
> +[
> + func f(T) = int
> +].
> +:- instance tc(int) where
> +[
> + f(X) = X
> +].
> +
> +:- import_module overload__sub.
> +:- module sub.
> +:- interface.
> +:- typeclass tc2(T) where
> +[
> + func f(T) = int
> +].
> +:- instance tc2(string) where
> +[
> + f(_) = 123456789
> +].
> +:- end_module sub.
> +
> +main -->
> + io__write_int(f(5)),
> + io__nl.
>

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