Fix PR#5985; compute injectivity of types but no new syntax

git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@13634 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02

1 files changed, 46 insertions, 23 deletions

diff --git a/typing/ctype.ml b/typing/ctype.ml
index 3d96ef019..a31c968c3 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -753,10 +753,10 @@ let rec generalize_expansive env var_level ty =
         Tconstr (path, tyl, abbrev) ->
           let variance =
             try (Env.find_type path env).type_variance
-            with Not_found -> List.map (fun _ -> (true,true,true)) tyl in
+            with Not_found -> List.map (fun _ -> (true,true,true,false)) tyl in
           abbrev := Mnil;
           List.iter2
-            (fun (co,cn,ct) t ->
+            (fun (co,cn,ct,_) t ->
               if ct then generalize_contravariant env var_level t
               else generalize_expansive env var_level t)
             variance tyl
@@ -1508,6 +1508,15 @@ let generic_abbrev env path =
     Not_found ->
       false
 
+let generic_private_abbrev env path =
+  try
+    match Env.find_type path env with
+      {type_kind = Type_abstract;
+       type_private = Private;
+       type_manifest = Some body} ->
+         (repr body).level = generic_level
+    | _ -> false
+  with Not_found -> false
 
                               (*****************)
                               (*  Occur check  *)
@@ -1681,7 +1690,7 @@ let occur_univar env ty =
           begin try
             let td = Env.find_type p env in
             List.iter2
-              (fun t (pos,neg,_) -> if pos || neg then occur_rec bound t)
+              (fun t (pos,neg,_,_) -> if pos || neg then occur_rec bound t)
               tl td.type_variance
           with Not_found ->
             List.iter (occur_rec bound) tl
@@ -1727,7 +1736,7 @@ let univars_escape env univar_pairs vl ty =
       | Tconstr (p, tl, _) ->
           begin try
             let td = Env.find_type p env in
-            List.iter2 (fun t (pos,neg,_) -> if pos || neg then occur t)
+            List.iter2 (fun t (pos,neg,_,_) -> if pos || neg then occur t)
               tl td.type_variance
           with Not_found ->
             List.iter occur tl
@@ -2018,8 +2027,19 @@ and mcomp_type_decl type_pairs subst env p1 p2 tl1 tl2 =
   try
     let decl = Env.find_type p1 env in
     let decl' = Env.find_type p2 env in
-    if Path.same p1 p2 then
-      (if non_aliasable p1 decl then mcomp_list type_pairs subst env tl1 tl2)
+    if Path.same p1 p2 then begin
+      (* Format.eprintf "@[%a@ %a@]@."
+	!print_raw (newconstr p1 tl2) !print_raw (newconstr p2 tl2);
+      if non_aliasable p1 decl then Format.eprintf "non_aliasable@."
+      else Format.eprintf "aliasable@."; *)
+      let inj =
+        try List.map for4 (Env.find_type p1 env).type_variance
+        with Not_found -> List.map (fun _ -> false) tl1
+      in
+      List.iter2
+        (fun i (t1,t2) -> if i then mcomp type_pairs subst env t1 t2)
+        inj (List.combine tl1 tl2)
+    end
     else match decl.type_kind, decl'.type_kind with
     | Type_record (lst,r), Type_record (lst',r') when r = r' ->
         mcomp_list type_pairs subst env tl1 tl2;
@@ -2245,14 +2265,21 @@ and unify3 env t1 t1' t2 t2' =
           then
             unify_list env tl1 tl2
           else
-            set_mode Pattern ~generate:false
-              begin fun () ->
-                let snap = snapshot () in
-                try unify_list env tl1 tl2 with Unify _ ->
-                  backtrack snap;
-                  List.iter (reify env) (tl1 @ tl2)
-              end
-        (*set_mode Pattern ~generate:false (fun () -> unify_list env tl1 tl2)*)
+            let inj =
+              try List.map for4 (Env.find_type p1 !env).type_variance
+              with Not_found -> List.map (fun _ -> false) tl1
+            in
+            List.iter2
+              (fun i (t1, t2) ->
+                if i then unify env t1 t2 else
+                set_mode Pattern ~generate:false
+                  begin fun () ->
+                    let snap = snapshot () in
+                    try unify env t1 t2 with Unify _ ->
+                      backtrack snap;
+                      reify env t1; reify env t2
+                  end)
+              inj (List.combine tl1 tl2)
       | (Tconstr ((Path.Pident p) as path,[],_),
          Tconstr ((Path.Pident p') as path',[],_))
         when is_abstract_newtype !env path && is_abstract_newtype !env path'
@@ -3560,7 +3587,7 @@ let rec build_subtype env visited loops posi level t =
         then warn := true;
         let tl' =
           List.map2
-            (fun (co,cn,_) t ->
+            (fun (co,cn,_,_) t ->
               if cn then
                 if co then (t, Unchanged)
                 else build_subtype env visited loops (not posi) level t
@@ -3665,12 +3692,6 @@ let subtypes = TypePairs.create 17
 let subtype_error env trace =
   raise (Subtype (expand_trace env (List.rev trace), []))
 
-let private_abbrev env path =
-  try
-    let decl = Env.find_type path env in
-    decl.type_private = Private && decl.type_manifest <> None
-  with Not_found -> false
-
 (* check list inclusion, assuming lists are ordered *)
 let rec included nl1 nl2 =
   match nl1, nl2 with
@@ -3719,7 +3740,7 @@ let rec subtype_rec env trace t1 t2 cstrs =
         begin try
           let decl = Env.find_type p1 env in
           List.fold_left2
-            (fun cstrs (co, cn, _) (t1, t2) ->
+            (fun cstrs (co, cn, _, _) (t1, t2) ->
               if co then
                 if cn then
                   (trace, newty2 t1.level (Ttuple[t1]),
@@ -3732,8 +3753,10 @@ let rec subtype_rec env trace t1 t2 cstrs =
         with Not_found ->
           (trace, t1, t2, !univar_pairs)::cstrs
         end
-    | (Tconstr(p1, tl1, _), _) when private_abbrev env p1 ->
+    | (Tconstr(p1, _, _), _) when generic_private_abbrev env p1 ->
         subtype_rec env trace (expand_abbrev_opt env t1) t2 cstrs
+(*  | (_, Tconstr(p2, _, _)) when generic_private_abbrev false env p2 ->
+        subtype_rec env trace t1 (expand_abbrev_opt env t2) cstrs *)
     | (Tobject (f1, _), Tobject (f2, _))
       when is_Tvar (object_row f1) && is_Tvar (object_row f2) ->
         (* Same row variable implies same object. *)