for review: bugfix for exist_q_vars bound to head tvars

[David Glen JEFFERY]

Hi,

This one's for you, Fergus.

Test case to follow.

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

Estimated hours taken: 2

compiler/typecheck.m:
	Don't get rid of an existentially quantified tvar if it is bound to
	a type variable from the head of the predicate. If you do, you find
	that, eg. :- some [T1] pred p(T1, T2) gets squashed into
	:- some [T2] pred p(T2, T2) if T1 is internally bound to T2.

Index: typecheck.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/typecheck.m,v
retrieving revision 1.247
diff -u -t -r1.247 typecheck.m
--- typecheck.m	1998/09/22 16:14:14	1.247
+++ typecheck.m	1998/09/24 05:05:49
@@ -393,9 +393,10 @@
                 typecheck_check_for_ambiguity(whole_pred, HeadVars,
                                 TypeCheckInfo3, TypeCheckInfo4),
                 typecheck_info_get_final_info(TypeCheckInfo4, ExistQVars0,
-                                TypeVarSet, HeadTypeParams2, InferredVarTypes0,
-                                InferredTypeConstraints0, ConstraintProofs,
-                                TVarRenaming, ExistTypeRenaming),
+                                TypeVarSet, HeadTypeParams1, HeadTypeParams2, 
+                                InferredVarTypes0, InferredTypeConstraints0,
+                                ConstraintProofs, TVarRenaming,
+                                ExistTypeRenaming),
                 map__optimize(InferredVarTypes0, InferredVarTypes),
                 ClausesInfo = clauses_info(VarSet, ExplicitVarTypes,
                                 InferredVarTypes, HeadVars, Clauses),
@@ -2827,15 +2828,16 @@
 %       in OldExistQVars.
 
 :- pred typecheck_info_get_final_info(typecheck_info, existq_tvars,
-                tvarset, existq_tvars, map(var, type),
+                tvarset, list(tvar), existq_tvars, map(var, type),
                 class_constraints, map(class_constraint, constraint_proof),
                 map(tvar, tvar), map(tvar, tvar)).
-:- mode typecheck_info_get_final_info(in, in, out, out, out, out, out, out, out)
-                is det.
+:- mode typecheck_info_get_final_info(in, in, out, in, 
+                out, out, out, out, out, out) is det.
 
 typecheck_info_get_final_info(TypeCheckInfo, OldExistQVars, NewTypeVarSet,
-                NewHeadTypeParams, NewVarTypes, NewTypeConstraints,
-                NewConstraintProofs, TSubst, ExistTypeRenaming) :-
+                OldHeadTypeParams, NewHeadTypeParams, NewVarTypes,
+                NewTypeConstraints, NewConstraintProofs, TSubst,
+                ExistTypeRenaming) :-
         typecheck_info_get_type_assign_set(TypeCheckInfo, TypeAssignSet),
         ( TypeAssignSet = [TypeAssign | _] ->
                 type_assign_get_head_type_params(TypeAssign, HeadTypeParams),
@@ -2851,11 +2853,11 @@
                 expand_types(Vars, TypeBindings, VarTypes0, VarTypes),
 
                 %
-                % figure out how we should renaming the existential types
+                % figure out how we should rename the existential types
                 % in the type declaration (if any)
                 %
-                get_existq_tvar_renaming(OldExistQVars, TypeBindings,
-                        ExistTypeRenaming),
+                get_existq_tvar_renaming(OldExistQVars, OldHeadTypeParams,
+                        TypeBindings, ExistTypeRenaming),
 
                 %
                 % We used to just use the OldTypeVarSet that we got
@@ -2917,17 +2919,20 @@
 % We rename any existentially quantified type variables which
 % get mapped to other type variables.
 %
-:- pred get_existq_tvar_renaming(existq_tvars, tsubst, map(tvar, tvar)).
-:- mode get_existq_tvar_renaming(in, in, out) is det.
+:- pred get_existq_tvar_renaming(existq_tvars, list(tvar), tsubst, 
+        map(tvar, tvar)).
+:- mode get_existq_tvar_renaming(in, in, in, out) is det.
 
-get_existq_tvar_renaming(ExistQVars, TypeBindings, ExistTypeRenaming) :-
+get_existq_tvar_renaming(ExistQVars, OldHeadTypeParams, TypeBindings,
+                ExistTypeRenaming) :-
         MaybeAddToMap = lambda([TVar::in, Renaming0::in, Renaming::out] is det,
                 (
                         term__apply_rec_substitution(term__variable(TVar),
                                 TypeBindings, Result),
                         (
                                 Result = term__variable(NewTVar),
-                                NewTVar \= TVar
+                                NewTVar \= TVar,
+                                \+ list__member(NewTVar, OldHeadTypeParams)
                         ->
                                 map__det_insert(Renaming0, TVar, NewTVar,
                                         Renaming)

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


dgj
-- 
David Jeffery (dgj at cs.mu.oz.au) |  Marge: Did you just call everyone "chicken"?
PhD 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.