[m-dev.] for review: apply `void' renaming in class proofs

[David Glen JEFFERY]

Hi,

For Fergus to review.
------------------------------

Estimated hours taken: 5

When binding unbound tvars to `void', also bind them to void in the constraint
proofs. This fixes a bug where an unbound but constrained type variable caused
a map lookup failure when the constraint was looked up in later compilation
phases.

compiler/post_typecheck.m:
	Update the constraint proofs.

tests/hard_coded/typeclasses/unbound_tvar.{m,exp}:
	A test case for this change.
tests/hard_coded/typeclasses/Mmakefile:
	Turn this test case on. For now, I have disabled type specialisation as
	this case tickles another bug (that Simon is currently working on,
	I believe).

------------------------------

Index: compiler/post_typecheck.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/post_typecheck.m,v
retrieving revision 1.25
diff -u -t -r1.25 post_typecheck.m
--- compiler/post_typecheck.m	2000/07/24 11:36:06	1.25
+++ compiler/post_typecheck.m	2000/08/23 06:23:00
@@ -172,10 +172,13 @@
                 % bind all the type variables in `Set' to `void' ...
                 %
                 pred_info_context(PredInfo0, Context),
-                bind_type_vars_to_void(Set, Context, VarTypesMap0, VarTypesMap),
+                pred_info_get_constraint_proofs(PredInfo0, Proofs0),
+                bind_type_vars_to_void(Set, Context, VarTypesMap0, VarTypesMap,
+                        Proofs0, Proofs),
                 clauses_info_set_vartypes(ClausesInfo0, VarTypesMap,
                         ClausesInfo),
-                pred_info_set_clauses_info(PredInfo0, ClausesInfo, PredInfo)
+                pred_info_set_clauses_info(PredInfo0, ClausesInfo, PredInfo1),
+                pred_info_set_constraint_proofs(PredInfo1, Proofs, PredInfo)
         ),
 
         %
@@ -224,11 +227,12 @@
 % bind all the type variables in `UnboundTypeVarsSet' to the type `void' ...
 %
 :- pred bind_type_vars_to_void(set(tvar), prog_context,
-                                map(prog_var, type), map(prog_var, type)).
-:- mode bind_type_vars_to_void(in, in, in, out) is det.
+                                map(prog_var, type), map(prog_var, type),
+                                constraint_proof_map, constraint_proof_map).
+:- mode bind_type_vars_to_void(in, in, in, out, in, out) is det.
 
 bind_type_vars_to_void(UnboundTypeVarsSet, Context,
-                VarTypesMap0, VarTypesMap) :-
+                VarTypesMap0, VarTypesMap, Proofs0, Proofs) :-
         %
         % first create a pair of corresponding lists (UnboundTypeVars, Voids)
         % that map the unbound type variables to void
@@ -239,13 +243,28 @@
         list__duplicate(Length, Void, Voids),
 
         %
-        % then apply the substitution we just created to the variable types
+        % then create a *substitution* that maps the 
+        % unbound type variables to void, but throws away the term context,
+        % for use in renaming the constraint proofs (ie. so that we can use
+        % map__lookup on the proofs).
+        %
+        term__context_init(InitContext),
+        VoidNoContext = term__functor(term__atom("void"), [], InitContext),
+        list__duplicate(Length, VoidNoContext, VoidsNoContext),
+        map__from_corresponding_lists(UnboundTypeVars, VoidsNoContext, 
+                VoidSubst),
+
+        %
+        % then apply the substitutions we just created to the variable types
+        % and constraint proofs
         %
         map__keys(VarTypesMap0, Vars),
         map__values(VarTypesMap0, Types0),
         term__substitute_corresponding_list(UnboundTypeVars, Voids,
                 Types0, Types),
-        map__from_corresponding_lists(Vars, Types, VarTypesMap).
+        map__from_corresponding_lists(Vars, Types, VarTypesMap),
+
+        apply_subst_to_constraint_proofs(VoidSubst, Proofs0, Proofs).
 
 %-----------------------------------------------------------------------------%
 %

Index: tests/hard_coded/typeclasses/Mmakefile
===================================================================
RCS file: /home/staff/zs/imp/tests/hard_coded/typeclasses/Mmakefile,v
retrieving revision 1.32
diff -u -t -r1.32 Mmakefile
--- tests/hard_coded/typeclasses/Mmakefile	2000/08/24 06:08:20	1.32
+++ tests/hard_coded/typeclasses/Mmakefile	2000/08/25 06:52:06
@@ -44,6 +44,7 @@
         typeclass_test_5 \
         typeclass_test_6 \
         type_spec \
+        unbound_tvar \
         unqualified_method \
         use_abstract_instance
 
@@ -60,6 +61,7 @@
 MCFLAGS-intermod_typeclass_bug2 = --intermodule-optimization
 MCFLAGS-lambda_multi_constraint_same_tvar = --infer-all
 MCFLAGS-abstract_instance = --infer-all
+MCFLAGS-unbound_tvar = --no-user-guided-type-specialisation
 MCFLAGS-unqualified_method = --intermodule-optimization
 MCFLAGS-unqualified_method2 = --intermodule-optimization
 MCFLAGS-unqualified_method3 = --intermodule-optimization
===================================================================
New file: unbound_tvar.m:

:- module unbound_tvar.

:- interface.

:- import_module io.

:- pred main(io__state::di, io__state::uo) is det.

:- implementation.

main -->
	{ p(a(1)) }.

:- typeclass c(T) where [ 
	pred p(T), 
	mode p(in) is det 
].

:- type t(A, B) ---> a(A) ; b(B).

:- instance c(t(A,B)) where [ pred(p/1) is x ].

:- pred x(t(A, B)::in) is det.
x(_).

===================================================================
New file: unbound_tvar.exp:

===================================================================

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