[m-dev.] for review: bugfix for exist_q_vars bound to head tvars

[David Glen JEFFERY]

On 24-Sep-1998, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> On 24-Sep-1998, David Glen JEFFERY <dgj at cs.mu.OZ.AU> wrote:
> >  typecheck_info_get_final_info(TypeCheckInfo, OldExistQVars, NewTypeVarSet,
> > +                OldHeadTypeParams, NewHeadTypeParams, NewVarTypes,
> > +                NewTypeConstraints, NewConstraintProofs, TSubst,
> > +                ExistTypeRenaming) :-
> 
> How about putting all the Old* parameters before all of the New* ones?
> 
> Also, if you're changing the parameter order, then I would put
> the OldHeadTypeParams (which are basically just the universally typed
> vars) before OldExistQVars (the existentially typed vars).  That's just
> for consistency with elsewhere, e.g. the order of arguments for the
> constraints/2 functor -- I've tended to put universal constraints and
> quantifiers before existential constraints and quantifiers.
> 
> >  % We rename any existentially quantified type variables which
> >  % get mapped to other type variables.
> >  %
> 
> That comment should be updated.
> 
> Could you post another diff please?

Here 'tis. The log message stays the same as before.

cvs diff: [19:45:31] obtained lock in /home/staff/zs/imp/mercury/compiler
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 09:39:34
@@ -392,10 +392,11 @@
                                 TypeCheckInfo3),
                 typecheck_check_for_ambiguity(whole_pred, HeadVars,
                                 TypeCheckInfo3, TypeCheckInfo4),
-                typecheck_info_get_final_info(TypeCheckInfo4, ExistQVars0,
-                                TypeVarSet, HeadTypeParams2, InferredVarTypes0,
-                                InferredTypeConstraints0, ConstraintProofs,
-                                TVarRenaming, ExistTypeRenaming),
+                typecheck_info_get_final_info(TypeCheckInfo4, HeadTypeParams1, 
+                                ExistQVars0, TypeVarSet, HeadTypeParams2,
+                                InferredVarTypes0, InferredTypeConstraints0,
+                                ConstraintProofs, TVarRenaming,
+                                ExistTypeRenaming),
                 map__optimize(InferredVarTypes0, InferredVarTypes),
                 ClausesInfo = clauses_info(VarSet, ExplicitVarTypes,
                                 InferredVarTypes, HeadVars, Clauses),
@@ -2813,10 +2814,13 @@
 
 %-----------------------------------------------------------------------------%
 
-% typecheck_info_get_final_info(TypeCheckInfo, OldExistQVars,
+% typecheck_info_get_final_info(TypeCheckInfo, 
+%               OldHeadTypeParams, OldExistQVars,
 %               NewTypeVarSet, New* ..., TypeRenaming, ExistTypeRenaming):
 %       extracts the final inferred types from TypeCheckInfo.
 %
+%       OldHeadTypeParams should be the type variables from the head of the
+%       predicate.
 %       OldExistQVars should be the declared existentially quantified
 %       type variables (if any).
 %       New* is the newly inferred types, in NewTypeVarSet.
@@ -2826,16 +2830,17 @@
 %       applying TypeRenaming) to rename existential type variables
 %       in OldExistQVars.
 
-:- pred typecheck_info_get_final_info(typecheck_info, existq_tvars,
+:- pred typecheck_info_get_final_info(typecheck_info, list(tvar), existq_tvars,
                 tvarset, 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, in, 
+                out, out, out, out, out, out, out) is det.
 
-typecheck_info_get_final_info(TypeCheckInfo, OldExistQVars, NewTypeVarSet,
-                NewHeadTypeParams, NewVarTypes, NewTypeConstraints,
-                NewConstraintProofs, TSubst, ExistTypeRenaming) :-
+typecheck_info_get_final_info(TypeCheckInfo, OldHeadTypeParams, OldExistQVars, 
+                NewTypeVarSet, 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 +2856,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(OldHeadTypeParams, OldExistQVars,
+                        TypeBindings, ExistTypeRenaming),
 
                 %
                 % We used to just use the OldTypeVarSet that we got
@@ -2915,19 +2920,23 @@
 
 %
 % We rename any existentially quantified type variables which
-% get mapped to other type variables.
+% get mapped to other type variables, unless they are mapped to type
+% variables from the head of the predicate.
 %
-:- 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(list(tvar), existq_tvars, 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(OldHeadTypeParams, ExistQVars, 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)


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