l4/pkg/ocaml/ocaml/contrib/typing/ctype.ml

   1 (***********************************************************************)
   2 (*                                                                     *)
   3 (*                           Objective Caml                            *)
   4 (*                                                                     *)
   5 (* Xavier Leroy and Jerome Vouillon, projet Cristal, INRIA Rocquencourt*)
   6 (*                                                                     *)
   7 (*  Copyright 1996 Institut National de Recherche en Informatique et   *)
   8 (*  en Automatique.  All rights reserved.  This file is distributed    *)
   9 (*  under the terms of the Q Public License version 1.0.               *)
  10 (*                                                                     *)
  11 (***********************************************************************)
  12
  13 (* $Id: ctype.ml 9453 2009-12-07 13:04:54Z garrigue $ *)
  14
  15 (* Operations on core types *)
  16
  17 open Misc
  18 open Asttypes
  19 open Types
  20 open Btype
  21
  22 (*
  23    Type manipulation after type inference
  24    ======================================
  25    If one wants to manipulate a type after type inference (for
  26    instance, during code generation or in the debugger), one must
  27    first make sure that the type levels are correct, using the
  28    function [correct_levels]. Then, this type can be correctely
  29    manipulated by [apply], [expand_head] and [moregeneral].
  30 *)
  31
  32 (*
  33    General notes
  34    =============
  35    - As much sharing as possible should be kept : it makes types
  36      smaller and better abbreviated.
  37      When necessary, some sharing can be lost. Types will still be
  38      printed correctly (+++ TO DO...), and abbreviations defined by a
  39      class do not depend on sharing thanks to constrained
  40      abbreviations. (Of course, even if some sharing is lost, typing
  41      will still be correct.)
  42    - All nodes of a type have a level : that way, one know whether a
  43      node need to be duplicated or not when instantiating a type.
  44    - Levels of a type are decreasing (generic level being considered
  45      as greatest).
  46    - The level of a type constructor is superior to the binding
  47      time of its path.
  48    - Recursive types without limitation should be handled (even if
  49      there is still an occur check). This avoid treating specially the
  50      case for objects, for instance. Furthermore, the occur check
  51      policy can then be easily changed.
  52 *)
  53
  54 (*
  55    A faire
  56    =======
  57    - Revoir affichage des types.
  58    - Etendre la portee d'un alias [... as 'a] a tout le type englobant.
  59    - #-type implementes comme de vraies abreviations.
  60    - Niveaux plus fins pour les identificateurs :
  61        Champ [global] renomme en [level];
  62        Niveau -1 : global
  63                0 : module toplevel
  64                1 : module contenu dans module toplevel
  65               ...
  66      En fait, incrementer le niveau a chaque fois que l'on rentre dans
  67      un module.
  68
  69        3   4 6
  70         \ / /
  71        1 2 5
  72         \|/
  73          0
  74
  75      [Subst] doit ecreter les niveaux (pour qu'un variable non
  76      generalisable dans un module de niveau 2 ne se retrouve pas
  77      generalisable lorsque l'on l'utilise au niveau 0).
  78
  79    - Traitement de la trace de l'unification separe de la fonction
  80      [unify].
  81 *)
  82
  83 (**** Errors ****)
  84
  85 exception Unify of (type_expr * type_expr) list
  86
  87 exception Tags of label * label
  88
  89 exception Subtype of
  90         (type_expr * type_expr) list * (type_expr * type_expr) list
  91
  92 exception Cannot_expand
  93
  94 exception Cannot_apply
  95
  96 exception Recursive_abbrev
  97
  98 (**** Type level management ****)
  99
 100 let current_level = ref 0
 101 let nongen_level = ref 0
 102 let global_level = ref 1
 103 let saved_level = ref []
 104
 105 let init_def level = current_level := level; nongen_level := level
 106 let begin_def () =
 107   saved_level := (!current_level, !nongen_level) :: !saved_level;
 108   incr current_level; nongen_level := !current_level
 109 let begin_class_def () =
 110   saved_level := (!current_level, !nongen_level) :: !saved_level;
 111   incr current_level
 112 let raise_nongen_level () =
 113   saved_level := (!current_level, !nongen_level) :: !saved_level;
 114   nongen_level := !current_level
 115 let end_def () =
 116   let (cl, nl) = List.hd !saved_level in
 117   saved_level := List.tl !saved_level;
 118   current_level := cl; nongen_level := nl
 119
 120 let reset_global_level () =
 121   global_level := !current_level + 1
 122 let increase_global_level () =
 123   let gl = !global_level in
 124   global_level := !current_level;
 125   gl
 126 let restore_global_level gl =
 127   global_level := gl
 128
 129 (* Abbreviations without parameters *)
 130 (* Shall reset after generalizing *)
 131 let simple_abbrevs = ref Mnil
 132 let proper_abbrevs path tl abbrev =
 133   if !Clflags.principal || tl <> [] then abbrev else
 134   let name = match path with Path.Pident id -> Ident.name id
 135                            | Path.Pdot(_, s,_) -> s
 136                            | Path.Papply _ -> assert false in
 137   if name.[0] <> '#' then simple_abbrevs else abbrev
 138
 139 (**** Some type creators ****)
 140
 141 (* Re-export generic type creators *)
 142
 143 let newty2             = Btype.newty2
 144 let newty desc         = newty2 !current_level desc
 145 let new_global_ty desc = newty2 !global_level desc
 146
 147 let newvar ()          = newty2 !current_level Tvar
 148 let newvar2 level      = newty2 level Tvar
 149 let new_global_var ()  = newty2 !global_level Tvar
 150
 151 let newobj fields      = newty (Tobject (fields, ref None))
 152
 153 let newconstr path tyl = newty (Tconstr (path, tyl, ref Mnil))
 154
 155 let none = newty (Ttuple [])                (* Clearly ill-formed type *)
 156
 157 (**** Representative of a type ****)
 158
 159 (* Re-export repr *)
 160 let repr = repr
 161
 162 (**** Type maps ****)
 163
 164 module TypePairs =
 165   Hashtbl.Make (struct
 166     type t = type_expr * type_expr
 167     let equal (t1, t1') (t2, t2') = (t1 == t2) && (t1' == t2')
 168     let hash (t, t') = t.id + 93 * t'.id
 169  end)
 170
 171                   (**********************************************)
 172                   (*  Miscellaneous operations on object types  *)
 173                   (**********************************************)
 174
 175
 176 (**** Object field manipulation. ****)
 177
 178 let dummy_method = "*dummy method*"
 179
 180 let object_fields ty =
 181   match (repr ty).desc with
 182     Tobject (fields, _) -> fields
 183   | _                   -> assert false
 184
 185 let flatten_fields ty =
 186   let rec flatten l ty =
 187     let ty = repr ty in
 188     match ty.desc with
 189       Tfield(s, k, ty1, ty2) ->
 190         flatten ((s, k, ty1)::l) ty2
 191     | _ ->
 192         (l, ty)
 193   in
 194     let (l, r) = flatten [] ty in
 195     (Sort.list (fun (n, _, _) (n', _, _) -> n < n') l, r)
 196
 197 let build_fields level =
 198   List.fold_right
 199     (fun (s, k, ty1) ty2 -> newty2 level (Tfield(s, k, ty1, ty2)))
 200
 201 let associate_fields fields1 fields2 =
 202   let rec associate p s s' =
 203     function
 204       (l, []) ->
 205         (List.rev p, (List.rev s) @ l, List.rev s')
 206     | ([], l') ->
 207         (List.rev p, List.rev s, (List.rev s') @ l')
 208     | ((n, k, t)::r, (n', k', t')::r') when n = n' ->
 209         associate ((n, k, t, k', t')::p) s s' (r, r')
 210     | ((n, k, t)::r, ((n', k', t')::_ as l')) when n < n' ->
 211         associate p ((n, k, t)::s) s' (r, l')
 212     | (((n, k, t)::r as l), (n', k', t')::r') (* when n > n' *) ->
 213         associate p s ((n', k', t')::s') (l, r')
 214   in
 215   associate [] [] [] (fields1, fields2)
 216
 217 (**** Check whether an object is open ****)
 218
 219 (* +++ Il faudra penser a eventuellement expanser l'abreviation *)
 220 let rec object_row ty =
 221   let ty = repr ty in
 222   match ty.desc with
 223     Tobject (t, _)     -> object_row t
 224   | Tfield(_, _, _, t) -> object_row t
 225   | _ -> ty
 226
 227 let opened_object ty =
 228   match (object_row ty).desc with
 229   | Tvar               -> true
 230   | Tunivar            -> true
 231   | Tconstr _          -> true
 232   | _                  -> false
 233
 234 (**** Close an object ****)
 235
 236 let close_object ty =
 237   let rec close ty =
 238     let ty = repr ty in
 239     match ty.desc with
 240       Tvar ->
 241         link_type ty (newty2 ty.level Tnil)
 242     | Tfield(_, _, _, ty') -> close ty'
 243     | _                    -> assert false
 244   in
 245   match (repr ty).desc with
 246     Tobject (ty, _)   -> close ty
 247   | _                 -> assert false
 248
 249 (**** Row variable of an object type ****)
 250
 251 let row_variable ty =
 252   let rec find ty =
 253     let ty = repr ty in
 254     match ty.desc with
 255       Tfield (_, _, _, ty) -> find ty
 256     | Tvar                 -> ty
 257     | _                    -> assert false
 258   in
 259   match (repr ty).desc with
 260     Tobject (fi, _) -> find fi
 261   | _               -> assert false
 262
 263 (**** Object name manipulation ****)
 264 (* +++ Bientot obsolete *)
 265
 266 let set_object_name id rv params ty =
 267   match (repr ty).desc with
 268     Tobject (fi, nm) ->
 269       set_name nm (Some (Path.Pident id, rv::params))
 270   | _ ->
 271       assert false
 272
 273 let remove_object_name ty =
 274   match (repr ty).desc with
 275     Tobject (_, nm)   -> set_name nm None
 276   | Tconstr (_, _, _) -> ()
 277   | _                 -> fatal_error "Ctype.remove_object_name"
 278
 279 (**** Hiding of private methods ****)
 280
 281 let hide_private_methods ty =
 282   match (repr ty).desc with
 283     Tobject (fi, nm) ->
 284       nm := None;
 285       let (fl, _) = flatten_fields fi in
 286       List.iter
 287         (function (_, k, _) ->
 288           match field_kind_repr k with
 289             Fvar r -> set_kind r Fabsent
 290           | _      -> ())
 291         fl
 292   | _ ->
 293       assert false
 294
 295
 296                               (*******************************)
 297                               (*  Operations on class types  *)
 298                               (*******************************)
 299
 300
 301 let rec signature_of_class_type =
 302   function
 303     Tcty_constr (_, _, cty) -> signature_of_class_type cty
 304   | Tcty_signature sign     -> sign
 305   | Tcty_fun (_, ty, cty)   -> signature_of_class_type cty
 306
 307 let self_type cty =
 308   repr (signature_of_class_type cty).cty_self
 309
 310 let rec class_type_arity =
 311   function
 312     Tcty_constr (_, _, cty) ->  class_type_arity cty
 313   | Tcty_signature _        ->  0
 314   | Tcty_fun (_, _, cty)    ->  1 + class_type_arity cty
 315
 316
 317                   (*******************************************)
 318                   (*  Miscellaneous operations on row types  *)
 319                   (*******************************************)
 320
 321 let sort_row_fields = Sort.list (fun (p,_) (q,_) -> p < q)
 322
 323 let rec merge_rf r1 r2 pairs fi1 fi2 =
 324   match fi1, fi2 with
 325     (l1,f1 as p1)::fi1', (l2,f2 as p2)::fi2' ->
 326       if l1 = l2 then merge_rf r1 r2 ((l1,f1,f2)::pairs) fi1' fi2' else
 327       if l1 < l2 then merge_rf (p1::r1) r2 pairs fi1' fi2 else
 328       merge_rf r1 (p2::r2) pairs fi1 fi2'
 329   | [], _ -> (List.rev r1, List.rev_append r2 fi2, pairs)
 330   | _, [] -> (List.rev_append r1 fi1, List.rev r2, pairs)
 331
 332 let merge_row_fields fi1 fi2 =
 333   match fi1, fi2 with
 334     [], _ | _, [] -> (fi1, fi2, [])
 335   | [p1], _ when not (List.mem_assoc (fst p1) fi2) -> (fi1, fi2, [])
 336   | _, [p2] when not (List.mem_assoc (fst p2) fi1) -> (fi1, fi2, [])
 337   | _ -> merge_rf [] [] [] (sort_row_fields fi1) (sort_row_fields fi2)
 338
 339 let rec filter_row_fields erase = function
 340     [] -> []
 341   | (l,f as p)::fi ->
 342       let fi = filter_row_fields erase fi in
 343       match row_field_repr f with
 344         Rabsent -> fi
 345       | Reither(_,_,false,e) when erase -> set_row_field e Rabsent; fi
 346       | _ -> p :: fi
 347
 348                     (**************************************)
 349                     (*  Check genericity of type schemes  *)
 350                     (**************************************)
 351
 352
 353 exception Non_closed
 354
 355 let rec closed_schema_rec ty =
 356   let ty = repr ty in
 357   if ty.level >= lowest_level then begin
 358     let level = ty.level in
 359     ty.level <- pivot_level - level;
 360     match ty.desc with
 361       Tvar when level <> generic_level ->
 362         raise Non_closed
 363     | Tfield(_, kind, t1, t2) ->
 364         if field_kind_repr kind = Fpresent then
 365           closed_schema_rec t1;
 366         closed_schema_rec t2
 367     | Tvariant row ->
 368         let row = row_repr row in
 369         iter_row closed_schema_rec row;
 370         if not (static_row row) then closed_schema_rec row.row_more
 371     | _ ->
 372         iter_type_expr closed_schema_rec ty
 373   end
 374
 375 (* Return whether all variables of type [ty] are generic. *)
 376 let closed_schema ty =
 377   try
 378     closed_schema_rec ty;
 379     unmark_type ty;
 380     true
 381   with Non_closed ->
 382     unmark_type ty;
 383     false
 384
 385 exception Non_closed of type_expr * bool
 386
 387 let free_variables = ref []
 388 let really_closed = ref None
 389
 390 let rec free_vars_rec real ty =
 391   let ty = repr ty in
 392   if ty.level >= lowest_level then begin
 393     ty.level <- pivot_level - ty.level;
 394     begin match ty.desc, !really_closed with
 395       Tvar, _ ->
 396         free_variables := (ty, real) :: !free_variables
 397     | Tconstr (path, tl, _), Some env ->
 398         begin try
 399           let (_, body) = Env.find_type_expansion path env in
 400           if (repr body).level <> generic_level then
 401             free_variables := (ty, real) :: !free_variables
 402         with Not_found -> ()
 403         end;
 404         List.iter (free_vars_rec true) tl
 405 (* Do not count "virtual" free variables
 406     | Tobject(ty, {contents = Some (_, p)}) ->
 407         free_vars_rec false ty; List.iter (free_vars_rec true) p
 408 *)
 409     | Tobject (ty, _), _ ->
 410         free_vars_rec false ty
 411     | Tfield (_, _, ty1, ty2), _ ->
 412         free_vars_rec true ty1; free_vars_rec false ty2
 413     | Tvariant row, _ ->
 414         let row = row_repr row in
 415         iter_row (free_vars_rec true) row;
 416         if not (static_row row) then free_vars_rec false row.row_more
 417     | _    ->
 418         iter_type_expr (free_vars_rec true) ty
 419     end;
 420   end
 421
 422 let free_vars ?env ty =
 423   free_variables := [];
 424   really_closed := env;
 425   free_vars_rec true ty;
 426   let res = !free_variables in
 427   free_variables := [];
 428   really_closed := None;
 429   res
 430
 431 let free_variables ?env ty =
 432   let tl = List.map fst (free_vars ?env ty) in
 433   unmark_type ty;
 434   tl
 435
 436 let rec closed_type ty =
 437   match free_vars ty with
 438       []           -> ()
 439   | (v, real) :: _ -> raise (Non_closed (v, real))
 440
 441 let closed_parameterized_type params ty =
 442   List.iter mark_type params;
 443   let ok =
 444     try closed_type ty; true with Non_closed _ -> false in
 445   List.iter unmark_type params;
 446   unmark_type ty;
 447   ok
 448
 449 let closed_type_decl decl =
 450   try
 451     List.iter mark_type decl.type_params;
 452     begin match decl.type_kind with
 453       Type_abstract ->
 454         ()
 455     | Type_variant v ->
 456         List.iter (fun (_, tyl) -> List.iter closed_type tyl) v
 457     | Type_record(r, rep) ->
 458         List.iter (fun (_, _, ty) -> closed_type ty) r
 459     end;
 460     begin match decl.type_manifest with
 461       None    -> ()
 462     | Some ty -> closed_type ty
 463     end;
 464     unmark_type_decl decl;
 465     None
 466   with Non_closed (ty, _) ->
 467     unmark_type_decl decl;
 468     Some ty
 469
 470 type closed_class_failure =
 471     CC_Method of type_expr * bool * string * type_expr
 472   | CC_Value of type_expr * bool * string * type_expr
 473
 474 exception Failure of closed_class_failure
 475
 476 let closed_class params sign =
 477   let ty = object_fields (repr sign.cty_self) in
 478   let (fields, rest) = flatten_fields ty in
 479   List.iter mark_type params;
 480   mark_type rest;
 481   List.iter
 482     (fun (lab, _, ty) -> if lab = dummy_method then mark_type ty)
 483     fields;
 484   try
 485     mark_type_node (repr sign.cty_self);
 486     List.iter
 487       (fun (lab, kind, ty) ->
 488         if field_kind_repr kind = Fpresent then
 489         try closed_type ty with Non_closed (ty0, real) ->
 490           raise (Failure (CC_Method (ty0, real, lab, ty))))
 491       fields;
 492     mark_type_params (repr sign.cty_self);
 493     List.iter unmark_type params;
 494     unmark_class_signature sign;
 495     None
 496   with Failure reason ->
 497     mark_type_params (repr sign.cty_self);
 498     List.iter unmark_type params;
 499     unmark_class_signature sign;
 500     Some reason
 501
 502
 503                             (**********************)
 504                             (*  Type duplication  *)
 505                             (**********************)
 506
 507
 508 (* Duplicate a type, preserving only type variables *)
 509 let duplicate_type ty =
 510   Subst.type_expr Subst.identity ty
 511
 512 (* Same, for class types *)
 513 let duplicate_class_type ty =
 514   Subst.class_type Subst.identity ty
 515
 516
 517                          (*****************************)
 518                          (*  Type level manipulation  *)
 519                          (*****************************)
 520
 521 (*
 522    It would be a bit more efficient to remove abbreviation expansions
 523    rather than generalizing them: these expansions will usually not be
 524    used anymore. However, this is not possible in the general case, as
 525    [expand_abbrev] (via [subst]) requires these expansions to be
 526    preserved. Does it worth duplicating this code ?
 527 *)
 528 let rec iter_generalize tyl ty =
 529   let ty = repr ty in
 530   if (ty.level > !current_level) && (ty.level <> generic_level) then begin
 531     set_level ty generic_level;
 532     begin match ty.desc with
 533       Tconstr (_, _, abbrev) ->
 534         iter_abbrev (iter_generalize tyl) !abbrev
 535     | _ -> ()
 536     end;
 537     iter_type_expr (iter_generalize tyl) ty
 538   end else
 539     tyl := ty :: !tyl
 540
 541 let iter_generalize tyl ty =
 542   simple_abbrevs := Mnil;
 543   iter_generalize tyl ty
 544
 545 let generalize ty =
 546   iter_generalize (ref []) ty
 547
 548 (* Efficient repeated generalisation of the same type *)
 549 let iterative_generalization min_level tyl =
 550   let tyl' = ref [] in
 551   List.iter (iter_generalize tyl') tyl;
 552   List.fold_right (fun ty l -> if ty.level <= min_level then l else ty::l)
 553     !tyl' []
 554
 555 (* Generalize the structure and lower the variables *)
 556
 557 let rec generalize_structure var_level ty =
 558   let ty = repr ty in
 559   if ty.level <> generic_level then begin
 560     if ty.desc = Tvar && ty.level > var_level then
 561       set_level ty var_level
 562     else if ty.level > !current_level then begin
 563       set_level ty generic_level;
 564       begin match ty.desc with
 565         Tconstr (_, _, abbrev) -> abbrev := Mnil
 566       | _ -> ()
 567       end;
 568       iter_type_expr (generalize_structure var_level) ty
 569     end
 570   end
 571
 572 let generalize_structure var_level ty =
 573   simple_abbrevs := Mnil;
 574   generalize_structure var_level ty
 575
 576 (* let generalize_expansive ty = generalize_structure !nongen_level ty *)
 577 let generalize_global ty = generalize_structure !global_level ty
 578 let generalize_structure ty = generalize_structure !current_level ty
 579
 580 (* Generalize the spine of a function, if the level >= !current_level *)
 581
 582 let rec generalize_spine ty =
 583   let ty = repr ty in
 584   if ty.level < !current_level || ty.level = generic_level then () else
 585   match ty.desc with
 586     Tarrow (_, _, ty', _) | Tpoly (ty', _) ->
 587       set_level ty generic_level;
 588       generalize_spine ty'
 589   | _ -> ()
 590
 591 let forward_try_expand_once = (* Forward declaration *)
 592   ref (fun env ty -> raise Cannot_expand)
 593
 594 (*
 595    Lower the levels of a type (assume [level] is not
 596    [generic_level]).
 597 *)
 598 (*
 599     The level of a type constructor must be greater than its binding
 600     time. That way, a type constructor cannot escape the scope of its
 601     definition, as would be the case in
 602       let x = ref []
 603       module M = struct type t let _ = (x : t list ref) end
 604     (without this constraint, the type system would actually be unsound.)
 605 *)
 606 let rec update_level env level ty =
 607   let ty = repr ty in
 608   if ty.level > level then begin
 609     begin match ty.desc with
 610       Tconstr(p, tl, abbrev)  when level < Path.binding_time p ->
 611         (* Try first to replace an abbreviation by its expansion. *)
 612         begin try
 613           link_type ty (!forward_try_expand_once env ty);
 614           update_level env level ty
 615         with Cannot_expand ->
 616           (* +++ Levels should be restored... *)
 617           raise (Unify [(ty, newvar2 level)])
 618         end
 619     | Tobject(_, ({contents=Some(p, tl)} as nm))
 620       when level < Path.binding_time p ->
 621         set_name nm None;
 622         update_level env level ty
 623     | Tvariant row ->
 624         let row = row_repr row in
 625         begin match row.row_name with
 626         | Some (p, tl) when level < Path.binding_time p ->
 627             log_type ty;
 628             ty.desc <- Tvariant {row with row_name = None}
 629         | _ -> ()
 630         end;
 631         set_level ty level;
 632         iter_type_expr (update_level env level) ty
 633     | Tfield(lab, _, _, _) when lab = dummy_method ->
 634         raise (Unify [(ty, newvar2 level)])
 635     | _ ->
 636         set_level ty level;
 637         (* XXX what about abbreviations in Tconstr ? *)
 638         iter_type_expr (update_level env level) ty
 639     end
 640   end
 641
 642 (* Generalize and lower levels of contravariant branches simultaneously *)
 643
 644 let rec generalize_expansive env var_level ty =
 645   let ty = repr ty in
 646   if ty.level <> generic_level then begin
 647     if ty.level > var_level then begin
 648       set_level ty generic_level;
 649       match ty.desc with
 650         Tconstr (path, tyl, abbrev) ->
 651           let variance =
 652             try (Env.find_type path env).type_variance
 653             with Not_found -> List.map (fun _ -> (true,true,true)) tyl in
 654           abbrev := Mnil;
 655           List.iter2
 656             (fun (co,cn,ct) t ->
 657               if ct then update_level env var_level t
 658               else generalize_expansive env var_level t)
 659             variance tyl
 660       | Tarrow (_, t1, t2, _) ->
 661           update_level env var_level t1;
 662           generalize_expansive env var_level t2
 663       | _ ->
 664           iter_type_expr (generalize_expansive env var_level) ty
 665     end
 666   end
 667
 668 let generalize_expansive env ty =
 669   simple_abbrevs := Mnil;
 670   try
 671     generalize_expansive env !nongen_level ty
 672   with Unify [_, ty'] ->
 673     raise (Unify [ty, ty'])
 674
 675 (* Correct the levels of type [ty]. *)
 676 let correct_levels ty =
 677   duplicate_type ty
 678
 679 (* Only generalize the type ty0 in ty *)
 680 let limited_generalize ty0 ty =
 681   let ty0 = repr ty0 in
 682
 683   let graph = Hashtbl.create 17 in
 684   let idx = ref lowest_level in
 685   let roots = ref [] in
 686
 687   let rec inverse pty ty =
 688     let ty = repr ty in
 689     if (ty.level > !current_level) || (ty.level = generic_level) then begin
 690       decr idx;
 691       Hashtbl.add graph !idx (ty, ref pty);
 692       if (ty.level = generic_level) || (ty == ty0) then
 693         roots := ty :: !roots;
 694       set_level ty !idx;
 695       iter_type_expr (inverse [ty]) ty
 696     end else if ty.level < lowest_level then begin
 697       let (_, parents) = Hashtbl.find graph ty.level in
 698       parents := pty @ !parents
 699     end
 700
 701   and generalize_parents ty =
 702     let idx = ty.level in
 703     if idx <> generic_level then begin
 704       set_level ty generic_level;
 705       List.iter generalize_parents !(snd (Hashtbl.find graph idx));
 706       (* Special case for rows: must generalize the row variable *)
 707       match ty.desc with
 708         Tvariant row ->
 709           let more = row_more row in
 710           let lv = more.level in
 711           if (lv < lowest_level || lv > !current_level)
 712           && lv <> generic_level then set_level more generic_level
 713       | _ -> ()
 714     end
 715   in
 716
 717   inverse [] ty;
 718   if ty0.level < lowest_level then
 719     iter_type_expr (inverse []) ty0;
 720   List.iter generalize_parents !roots;
 721   Hashtbl.iter
 722     (fun _ (ty, _) ->
 723        if ty.level <> generic_level then set_level ty !current_level)
 724     graph
 725
 726
 727                               (*******************)
 728                               (*  Instantiation  *)
 729                               (*******************)
 730
 731
 732 let rec find_repr p1 =
 733   function
 734     Mnil ->
 735       None
 736   | Mcons (Public, p2, ty, _, _) when Path.same p1 p2 ->
 737       Some ty
 738   | Mcons (_, _, _, _, rem) ->
 739       find_repr p1 rem
 740   | Mlink {contents = rem} ->
 741       find_repr p1 rem
 742
 743 (*
 744    Generic nodes are duplicated, while non-generic nodes are left
 745    as-is.
 746    During instantiation, the description of a generic node is first
 747    replaced by a link to a stub ([Tsubst (newvar ())]). Once the
 748    copy is made, it replaces the stub.
 749    After instantiation, the description of generic node, which was
 750    stored by [save_desc], must be put back, using [cleanup_types].
 751 *)
 752
 753 let abbreviations = ref (ref Mnil)
 754   (* Abbreviation memorized. *)
 755
 756 let rec copy ty =
 757   let ty = repr ty in
 758   match ty.desc with
 759     Tsubst ty -> ty
 760   | _ ->
 761     if ty.level <> generic_level then ty else
 762     let desc = ty.desc in
 763     save_desc ty desc;
 764     let t = newvar() in          (* Stub *)
 765     ty.desc <- Tsubst t;
 766     t.desc <-
 767       begin match desc with
 768       | Tconstr (p, tl, _) ->
 769           let abbrevs = proper_abbrevs p tl !abbreviations in
 770           begin match find_repr p !abbrevs with
 771             Some ty when repr ty != t -> (* XXX Commentaire... *)
 772               Tlink ty
 773           | _ ->
 774           (*
 775              One must allocate a new reference, so that abbrevia-
 776              tions belonging to different branches of a type are
 777              independent.
 778              Moreover, a reference containing a [Mcons] must be
 779              shared, so that the memorized expansion of an abbrevi-
 780              ation can be released by changing the content of just
 781              one reference.
 782           *)
 783               Tconstr (p, List.map copy tl,
 784                        ref (match !(!abbreviations) with
 785                               Mcons _ -> Mlink !abbreviations
 786                             | abbrev  -> abbrev))
 787           end
 788       | Tvariant row0 ->
 789           let row = row_repr row0 in
 790           let more = repr row.row_more in
 791           (* We must substitute in a subtle way *)
 792           (* Tsubst takes a tuple containing the row var and the variant *)
 793           begin match more.desc with
 794             Tsubst {desc = Ttuple [_;ty2]} ->
 795               (* This variant type has been already copied *)
 796               ty.desc <- Tsubst ty2; (* avoid Tlink in the new type *)
 797               Tlink ty2
 798           | _ ->
 799               (* If the row variable is not generic, we must keep it *)
 800               let keep = more.level <> generic_level in
 801               let more' =
 802                 match more.desc with
 803                   Tsubst ty -> ty
 804                 | Tconstr _ ->
 805                     if keep then save_desc more more.desc;
 806                     copy more
 807                 | Tvar | Tunivar ->
 808                     save_desc more more.desc;
 809                     if keep then more else newty more.desc
 810                 |  _ -> assert false
 811               in
 812               (* Register new type first for recursion *)
 813               more.desc <- Tsubst(newgenty(Ttuple[more';t]));
 814               (* Return a new copy *)
 815               Tvariant (copy_row copy true row keep more')
 816           end
 817       | Tfield (p, k, ty1, ty2) ->
 818           begin match field_kind_repr k with
 819             Fabsent  -> Tlink (copy ty2)
 820           | Fpresent -> copy_type_desc copy desc
 821           | Fvar r ->
 822               dup_kind r;
 823               copy_type_desc copy desc
 824           end
 825       | _ -> copy_type_desc copy desc
 826       end;
 827     t
 828
 829 (**** Variants of instantiations ****)
 830
 831 let instance sch =
 832   let ty = copy sch in
 833   cleanup_types ();
 834   ty
 835
 836 let instance_list schl =
 837   let tyl = List.map copy schl in
 838   cleanup_types ();
 839   tyl
 840
 841 let instance_constructor cstr =
 842   let ty_res = copy cstr.cstr_res in
 843   let ty_args = List.map copy cstr.cstr_args in
 844   cleanup_types ();
 845   (ty_args, ty_res)
 846
 847 let instance_parameterized_type sch_args sch =
 848   let ty_args = List.map copy sch_args in
 849   let ty = copy sch in
 850   cleanup_types ();
 851   (ty_args, ty)
 852
 853 let instance_parameterized_type_2 sch_args sch_lst sch =
 854   let ty_args = List.map copy sch_args in
 855   let ty_lst = List.map copy sch_lst in
 856   let ty = copy sch in
 857   cleanup_types ();
 858   (ty_args, ty_lst, ty)
 859
 860 let instance_class params cty =
 861   let rec copy_class_type =
 862     function
 863       Tcty_constr (path, tyl, cty) ->
 864         Tcty_constr (path, List.map copy tyl, copy_class_type cty)
 865     | Tcty_signature sign ->
 866         Tcty_signature
 867           {cty_self = copy sign.cty_self;
 868            cty_vars =
 869              Vars.map (function (m, v, ty) -> (m, v, copy ty)) sign.cty_vars;
 870            cty_concr = sign.cty_concr;
 871            cty_inher =
 872              List.map (fun (p,tl) -> (p, List.map copy tl)) sign.cty_inher}
 873     | Tcty_fun (l, ty, cty) ->
 874         Tcty_fun (l, copy ty, copy_class_type cty)
 875   in
 876   let params' = List.map copy params in
 877   let cty' = copy_class_type cty in
 878   cleanup_types ();
 879   (params', cty')
 880
 881 (**** Instanciation for types with free universal variables ****)
 882
 883 module TypeHash = Hashtbl.Make(TypeOps)
 884 module TypeSet = Set.Make(TypeOps)
 885
 886 type inv_type_expr =
 887     { inv_type : type_expr;
 888       mutable inv_parents : inv_type_expr list }
 889
 890 let rec inv_type hash pty ty =
 891   let ty = repr ty in
 892   try
 893     let inv = TypeHash.find hash ty in
 894     inv.inv_parents <- pty @ inv.inv_parents
 895   with Not_found ->
 896     let inv = { inv_type = ty; inv_parents = pty } in
 897     TypeHash.add hash ty inv;
 898     iter_type_expr (inv_type hash [inv]) ty
 899
 900 let compute_univars ty =
 901   let inverted = TypeHash.create 17 in
 902   inv_type inverted [] ty;
 903   let node_univars = TypeHash.create 17 in
 904   let rec add_univar univ inv =
 905     match inv.inv_type.desc with
 906       Tpoly (ty, tl) when List.memq univ (List.map repr tl) -> ()
 907     | _ ->
 908         try
 909           let univs = TypeHash.find node_univars inv.inv_type in
 910           if not (TypeSet.mem univ !univs) then begin
 911             univs := TypeSet.add univ !univs;
 912             List.iter (add_univar univ) inv.inv_parents
 913           end
 914         with Not_found ->
 915           TypeHash.add node_univars inv.inv_type (ref(TypeSet.singleton univ));
 916           List.iter (add_univar univ) inv.inv_parents
 917   in
 918   TypeHash.iter (fun ty inv -> if ty.desc = Tunivar then add_univar ty inv)
 919     inverted;
 920   fun ty ->
 921     try !(TypeHash.find node_univars ty) with Not_found -> TypeSet.empty
 922
 923 let rec diff_list l1 l2 =
 924   if l1 == l2 then [] else
 925   match l1 with [] -> invalid_arg "Ctype.diff_list"
 926   | a :: l1 -> a :: diff_list l1 l2
 927
 928 let conflicts free bound =
 929   let bound = List.map repr bound in
 930   TypeSet.exists (fun t -> List.memq (repr t) bound) free
 931
 932 let delayed_copy = ref []
 933     (* copying to do later *)
 934
 935 (* Copy without sharing until there are no free univars left *)
 936 (* all free univars must be included in [visited]            *)
 937 let rec copy_sep fixed free bound visited ty =
 938   let ty = repr ty in
 939   let univars = free ty in
 940   if TypeSet.is_empty univars then
 941     if ty.level <> generic_level then ty else
 942     let t = newvar () in
 943     delayed_copy :=
 944       lazy (t.desc <- Tlink (copy ty))
 945       :: !delayed_copy;
 946     t
 947   else try
 948     let t, bound_t = List.assq ty visited in
 949     let dl = if ty.desc = Tunivar then [] else diff_list bound bound_t in
 950     if dl <> [] && conflicts univars dl then raise Not_found;
 951     t
 952   with Not_found -> begin
 953     let t = newvar() in          (* Stub *)
 954     let visited =
 955       match ty.desc with
 956         Tarrow _ | Ttuple _ | Tvariant _ | Tconstr _ | Tobject _ ->
 957           (ty,(t,bound)) :: visited
 958       | _ -> visited in
 959     let copy_rec = copy_sep fixed free bound visited in
 960     t.desc <-
 961       begin match ty.desc with
 962       | Tvariant row0 ->
 963           let row = row_repr row0 in
 964           let more = repr row.row_more in
 965           (* We shall really check the level on the row variable *)
 966           let keep = more.desc = Tvar && more.level <> generic_level in
 967           let more' = copy_rec more in
 968           let fixed' = fixed && (repr more').desc = Tvar in
 969           let row = copy_row copy_rec fixed' row keep more' in
 970           Tvariant row
 971       | Tpoly (t1, tl) ->
 972           let tl = List.map repr tl in
 973           let tl' = List.map (fun t -> newty Tunivar) tl in
 974           let bound = tl @ bound in
 975           let visited =
 976             List.map2 (fun ty t -> ty,(t,bound)) tl tl' @ visited in
 977           Tpoly (copy_sep fixed free bound visited t1, tl')
 978       | _ -> copy_type_desc copy_rec ty.desc
 979       end;
 980     t
 981   end
 982
 983 let instance_poly fixed univars sch =
 984   let vars = List.map (fun _ -> newvar ()) univars in
 985   let pairs = List.map2 (fun u v -> repr u, (v, [])) univars vars in
 986   delayed_copy := [];
 987   let ty = copy_sep fixed (compute_univars sch) [] pairs sch in
 988   List.iter Lazy.force !delayed_copy;
 989   delayed_copy := [];
 990   cleanup_types ();
 991   vars, ty
 992
 993 let instance_label fixed lbl =
 994   let ty_res = copy lbl.lbl_res in
 995   let vars, ty_arg =
 996     match repr lbl.lbl_arg with
 997       {desc = Tpoly (ty, tl)} ->
 998         instance_poly fixed tl ty
 999     | ty ->
1000         [], copy lbl.lbl_arg
1001   in
1002   cleanup_types ();
1003   (vars, ty_arg, ty_res)
1004
1005 (**** Instantiation with parameter substitution ****)
1006
1007 let unify' = (* Forward declaration *)
1008   ref (fun env ty1 ty2 -> raise (Unify []))
1009
1010 let rec subst env level priv abbrev ty params args body =
1011   if List.length params <> List.length args then raise (Unify []);
1012   let old_level = !current_level in
1013   current_level := level;
1014   try
1015     let body0 = newvar () in          (* Stub *)
1016     begin match ty with
1017       None      -> ()
1018     | Some ({desc = Tconstr (path, tl, _)} as ty) ->
1019         let abbrev = proper_abbrevs path tl abbrev in
1020         memorize_abbrev abbrev priv path ty body0
1021     | _ ->
1022         assert false
1023     end;
1024     abbreviations := abbrev;
1025     let (params', body') = instance_parameterized_type params body in
1026     abbreviations := ref Mnil;
1027     !unify' env body0 body';
1028     List.iter2 (!unify' env) params' args;
1029     current_level := old_level;
1030     body'
1031   with Unify _ as exn ->
1032     current_level := old_level;
1033     raise exn
1034
1035 (*
1036    Only the shape of the type matters, not whether is is generic or
1037    not. [generic_level] might be somewhat slower, but it ensures
1038    invariants on types are enforced (decreasing levels.), and we don't
1039    care about efficiency here.
1040 *)
1041 let apply env params body args =
1042   try
1043     subst env generic_level Public (ref Mnil) None params args body
1044   with
1045     Unify _ -> raise Cannot_apply
1046
1047
1048                               (****************************)
1049                               (*  Abbreviation expansion  *)
1050                               (****************************)
1051
1052 (*
1053    If the environnement has changed, memorized expansions might not
1054    be correct anymore, and so we flush the cache. This is safe but
1055    quite pessimistic: it would be enough to flush the cache when a
1056    type or module definition is overriden in the environnement.
1057 *)
1058 let previous_env = ref Env.empty
1059 let string_of_kind = function Public -> "public" | Private -> "private"
1060 let check_abbrev_env env =
1061   if env != !previous_env then begin
1062     (* prerr_endline "cleanup expansion cache"; *)
1063     cleanup_abbrev ();
1064     previous_env := env
1065   end
1066
1067 (* Expand an abbreviation. The expansion is memorized. *)
1068 (*
1069    Assume the level is greater than the path binding time of the
1070    expanded abbreviation.
1071 *)
1072 (*
1073    An abbreviation expansion will fail in either of these cases:
1074    1. The type constructor does not correspond to a manifest type.
1075    2. The type constructor is defined in an external file, and this
1076       file is not in the path (missing -I options).
1077    3. The type constructor is not in the "local" environment. This can
1078       happens when a non-generic type variable has been instantiated
1079       afterwards to the not yet defined type constructor. (Actually,
1080       this cannot happen at the moment due to the strong constraints
1081       between type levels and constructor binding time.)
1082    4. The expansion requires the expansion of another abbreviation,
1083       and this other expansion fails.
1084 *)
1085 let expand_abbrev_gen kind find_type_expansion env ty =
1086   check_abbrev_env env;
1087   match ty with
1088     {desc = Tconstr (path, args, abbrev); level = level} ->
1089       let lookup_abbrev = proper_abbrevs path args abbrev in
1090       begin match find_expans kind path !lookup_abbrev with
1091         Some ty ->
1092           (* prerr_endline
1093             ("found a "^string_of_kind kind^" expansion for "^Path.name path);*)
1094           if level <> generic_level then
1095             begin try
1096               update_level env level ty
1097             with Unify _ ->
1098               (* XXX This should not happen.
1099                  However, levels are not correctly restored after a
1100                  typing error *)
1101               ()
1102             end;
1103           ty
1104       | None ->
1105           let (params, body) =
1106             try find_type_expansion path env with Not_found ->
1107               raise Cannot_expand
1108           in
1109           (* prerr_endline
1110             ("add a "^string_of_kind kind^" expansion for "^Path.name path);*)
1111           let ty' = subst env level kind abbrev (Some ty) params args body in
1112           (* Hack to name the variant type *)
1113           begin match repr ty' with
1114             {desc=Tvariant row} as ty when static_row row ->
1115               ty.desc <- Tvariant { row with row_name = Some (path, args) }
1116           | _ -> ()
1117           end;
1118           ty'
1119       end
1120   | _ ->
1121       assert false
1122
1123 let expand_abbrev = expand_abbrev_gen Public Env.find_type_expansion
1124
1125 let safe_abbrev env ty =
1126   let snap = Btype.snapshot () in
1127   try ignore (expand_abbrev env ty); true
1128   with Cannot_expand | Unify _ ->
1129     Btype.backtrack snap;
1130     false
1131
1132 let try_expand_once env ty =
1133   let ty = repr ty in
1134   match ty.desc with
1135     Tconstr _ -> repr (expand_abbrev env ty)
1136   | _ -> raise Cannot_expand
1137
1138 let _ = forward_try_expand_once := try_expand_once
1139
1140 (* Fully expand the head of a type.
1141    Raise Cannot_expand if the type cannot be expanded.
1142    May raise Unify, if a recursion was hidden in the type. *)
1143 let rec try_expand_head env ty =
1144   let ty' = try_expand_once env ty in
1145   begin try
1146     try_expand_head env ty'
1147   with Cannot_expand ->
1148     ty'
1149   end
1150
1151 (* Expand once the head of a type *)
1152 let expand_head_once env ty =
1153   try expand_abbrev env (repr ty) with Cannot_expand -> assert false
1154
1155 (* Fully expand the head of a type. *)
1156 let expand_head_unif env ty =
1157   try try_expand_head env ty with Cannot_expand -> repr ty
1158
1159 let expand_head env ty =
1160   let snap = Btype.snapshot () in
1161   try try_expand_head env ty
1162   with Cannot_expand | Unify _ -> (* expand_head shall never fail *)
1163     Btype.backtrack snap;
1164     repr ty
1165
1166 (* Implementing function [expand_head_opt], the compiler's own version of
1167    [expand_head] used for type-based optimisations.
1168    [expand_head_opt] uses [Env.find_type_expansion_opt] to access the
1169    manifest type information of private abstract data types which is
1170    normally hidden to the type-checker out of the implementation module of
1171    the private abbreviation. *)
1172
1173 let expand_abbrev_opt = expand_abbrev_gen Private Env.find_type_expansion_opt
1174
1175 let try_expand_once_opt env ty =
1176   let ty = repr ty in
1177   match ty.desc with
1178     Tconstr _ -> repr (expand_abbrev_opt env ty)
1179   | _ -> raise Cannot_expand
1180
1181 let rec try_expand_head_opt env ty =
1182   let ty' = try_expand_once_opt env ty in
1183   begin try
1184     try_expand_head_opt env ty'
1185   with Cannot_expand ->
1186     ty'
1187   end
1188
1189 let expand_head_opt env ty =
1190   let snap = Btype.snapshot () in
1191   try try_expand_head_opt env ty
1192   with Cannot_expand | Unify _ -> (* expand_head shall never fail *)
1193     Btype.backtrack snap;
1194     repr ty
1195
1196 (* Make sure that the type parameters of the type constructor [ty]
1197    respect the type constraints *)
1198 let enforce_constraints env ty =
1199   match ty with
1200     {desc = Tconstr (path, args, abbrev); level = level} ->
1201       let decl = Env.find_type path env in
1202       ignore
1203         (subst env level Public (ref Mnil) None decl.type_params args
1204            (newvar2 level))
1205   | _ ->
1206       assert false
1207
1208 (* Recursively expand the head of a type.
1209    Also expand #-types. *)
1210 let rec full_expand env ty =
1211   let ty = repr (expand_head env ty) in
1212   match ty.desc with
1213     Tobject (fi, {contents = Some (_, v::_)}) when (repr v).desc = Tvar ->
1214       newty2 ty.level (Tobject (fi, ref None))
1215   | _ ->
1216       ty
1217
1218 (*
1219    Check whether the abbreviation expands to a well-defined type.
1220    During the typing of a class, abbreviations for correspondings
1221    types expand to non-generic types.
1222 *)
1223 let generic_abbrev env path =
1224   try
1225     let (_, body) = Env.find_type_expansion path env in
1226     (repr body).level = generic_level
1227   with
1228     Not_found ->
1229       false
1230
1231
1232                               (*****************)
1233                               (*  Occur check  *)
1234                               (*****************)
1235
1236
1237 exception Occur
1238
1239 (* The marks are already used by [expand_abbrev]... *)
1240 let visited = ref []
1241
1242 let rec non_recursive_abbrev env ty0 ty =
1243   let ty = repr ty in
1244   if ty == repr ty0 then raise Recursive_abbrev;
1245   if not (List.memq ty !visited) then begin
1246     visited := ty :: !visited;
1247     match ty.desc with
1248       Tconstr(p, args, abbrev) ->
1249         begin try
1250           non_recursive_abbrev env ty0 (try_expand_once env ty)
1251         with Cannot_expand ->
1252           if !Clflags.recursive_types then () else
1253           iter_type_expr (non_recursive_abbrev env ty0) ty
1254         end
1255     | Tobject _ | Tvariant _ ->
1256         ()
1257     | _ ->
1258         if !Clflags.recursive_types then () else
1259         iter_type_expr (non_recursive_abbrev env ty0) ty
1260   end
1261
1262 let correct_abbrev env path params ty =
1263   check_abbrev_env env;
1264   let ty0 = newgenvar () in
1265   visited := [];
1266   let abbrev = Mcons (Public, path, ty0, ty0, Mnil) in
1267   simple_abbrevs := abbrev;
1268   try
1269     non_recursive_abbrev env ty0
1270       (subst env generic_level Public (ref abbrev) None [] [] ty);
1271     simple_abbrevs := Mnil;
1272     visited := []
1273   with exn ->
1274     simple_abbrevs := Mnil;
1275     visited := [];
1276     raise exn
1277
1278 let rec occur_rec env visited ty0 ty =
1279   if ty == ty0  then raise Occur;
1280   match ty.desc with
1281     Tconstr(p, tl, abbrev) ->
1282       begin try
1283         if List.memq ty visited || !Clflags.recursive_types then raise Occur;
1284         iter_type_expr (occur_rec env (ty::visited) ty0) ty
1285       with Occur -> try
1286         let ty' = try_expand_head env ty in
1287         (* Maybe we could simply make a recursive call here,
1288            but it seems it could make the occur check loop
1289            (see change in rev. 1.58) *)
1290         if ty' == ty0 || List.memq ty' visited then raise Occur;
1291         match ty'.desc with
1292           Tobject _ | Tvariant _ -> ()
1293         | _ ->
1294             if not !Clflags.recursive_types then
1295               iter_type_expr (occur_rec env (ty'::visited) ty0) ty'
1296       with Cannot_expand ->
1297         if not !Clflags.recursive_types then raise Occur
1298       end
1299   | Tobject _ | Tvariant _ ->
1300       ()
1301   | _ ->
1302       if not !Clflags.recursive_types then
1303         iter_type_expr (occur_rec env visited ty0) ty
1304
1305 let type_changed = ref false (* trace possible changes to the studied type *)
1306
1307 let merge r b = if b then r := true
1308
1309 let occur env ty0 ty =
1310   let old = !type_changed in
1311   try
1312     while type_changed := false; occur_rec env [] ty0 ty; !type_changed
1313     do () (* prerr_endline "changed" *) done;
1314     merge type_changed old
1315   with exn ->
1316     merge type_changed old;
1317     raise (match exn with Occur -> Unify [] | _ -> exn)
1318
1319
1320                    (*****************************)
1321                    (*  Polymorphic Unification  *)
1322                    (*****************************)
1323
1324 (* Since we cannot duplicate universal variables, unification must
1325    be done at meta-level, using bindings in univar_pairs *)
1326 let rec unify_univar t1 t2 = function
1327     (cl1, cl2) :: rem ->
1328       let find_univ t cl =
1329         try
1330           let (_, r) = List.find (fun (t',_) -> t == repr t') cl in
1331           Some r
1332         with Not_found -> None
1333       in
1334       begin match find_univ t1 cl1, find_univ t2 cl2 with
1335         Some {contents=Some t'2}, Some _ when t2 == repr t'2 ->
1336           ()
1337       | Some({contents=None} as r1), Some({contents=None} as r2) ->
1338           set_univar r1 t2; set_univar r2 t1
1339       | None, None ->
1340           unify_univar t1 t2 rem
1341       | _ ->
1342           raise (Unify [])
1343       end
1344   | [] -> raise (Unify [])
1345
1346 module TypeMap = Map.Make (TypeOps)
1347
1348 (* Test the occurence of free univars in a type *)
1349 (* that's way too expansive. Must do some kind of cacheing *)
1350 let occur_univar env ty =
1351   let visited = ref TypeMap.empty in
1352   let rec occur_rec bound ty =
1353     let ty = repr ty in
1354     if ty.level >= lowest_level &&
1355       if TypeSet.is_empty bound then
1356         (ty.level <- pivot_level - ty.level; true)
1357       else try
1358         let bound' = TypeMap.find ty !visited in
1359         if TypeSet.exists (fun x -> not (TypeSet.mem x bound)) bound' then
1360           (visited := TypeMap.add ty (TypeSet.inter bound bound') !visited;
1361            true)
1362         else false
1363       with Not_found ->
1364         visited := TypeMap.add ty bound !visited;
1365         true
1366     then
1367       match ty.desc with
1368         Tunivar ->
1369           if not (TypeSet.mem ty bound) then raise (Unify [ty, newgenvar()])
1370       | Tpoly (ty, tyl) ->
1371           let bound = List.fold_right TypeSet.add (List.map repr tyl) bound in
1372           occur_rec bound  ty
1373       | Tconstr (_, [], _) -> ()
1374       | Tconstr (p, tl, _) ->
1375           begin try
1376             let td = Env.find_type p env in
1377             List.iter2
1378               (fun t (pos,neg,_) -> if pos || neg then occur_rec bound t)
1379               tl td.type_variance
1380           with Not_found ->
1381             List.iter (occur_rec bound) tl
1382           end
1383       | _ -> iter_type_expr (occur_rec bound) ty
1384   in
1385   try
1386     occur_rec TypeSet.empty ty; unmark_type ty
1387   with exn ->
1388     unmark_type ty; raise exn
1389
1390 (* Grouping univars by families according to their binders *)
1391 let add_univars =
1392   List.fold_left (fun s (t,_) -> TypeSet.add (repr t) s)
1393
1394 let get_univar_family univar_pairs univars =
1395   if univars = [] then TypeSet.empty else
1396   let rec insert s = function
1397       cl1, (_::_ as cl2) ->
1398         if List.exists (fun (t1,_) -> TypeSet.mem (repr t1) s) cl1 then
1399           add_univars s cl2
1400         else s
1401     | _ -> s
1402   in
1403   let s = List.fold_right TypeSet.add univars TypeSet.empty in
1404   List.fold_left insert s univar_pairs
1405
1406 (* Whether a family of univars escapes from a type *)
1407 let univars_escape env univar_pairs vl ty =
1408   let family = get_univar_family univar_pairs vl in
1409   let visited = ref TypeSet.empty in
1410   let rec occur t =
1411     let t = repr t in
1412     if TypeSet.mem t !visited then () else begin
1413       visited := TypeSet.add t !visited;
1414       match t.desc with
1415         Tpoly (t, tl) ->
1416           if List.exists (fun t -> TypeSet.mem (repr t) family) tl then ()
1417           else occur t
1418       | Tunivar ->
1419           if TypeSet.mem t family then raise Occur
1420       | Tconstr (_, [], _) -> ()
1421       | Tconstr (p, tl, _) ->
1422           begin try
1423             let td = Env.find_type p env in
1424             List.iter2 (fun t (pos,neg,_) -> if pos || neg then occur t)
1425               tl td.type_variance
1426           with Not_found ->
1427             List.iter occur tl
1428           end
1429       | _ ->
1430           iter_type_expr occur t
1431     end
1432   in
1433   try occur ty; false with Occur -> true
1434
1435 (* Wrapper checking that no variable escapes and updating univar_pairs *)
1436 let enter_poly env univar_pairs t1 tl1 t2 tl2 f =
1437   let old_univars = !univar_pairs in
1438   let known_univars =
1439     List.fold_left (fun s (cl,_) -> add_univars s cl)
1440       TypeSet.empty old_univars
1441   in
1442   let tl1 = List.map repr tl1 and tl2 = List.map repr tl2 in
1443   if List.exists (fun t -> TypeSet.mem t known_univars) tl1 &&
1444     univars_escape env old_univars tl1 (newty(Tpoly(t2,tl2)))
1445   || List.exists (fun t -> TypeSet.mem t known_univars) tl2 &&
1446     univars_escape env old_univars tl2 (newty(Tpoly(t1,tl1)))
1447   then raise (Unify []);
1448   let cl1 = List.map (fun t -> t, ref None) tl1
1449   and cl2 = List.map (fun t -> t, ref None) tl2 in
1450   univar_pairs := (cl1,cl2) :: (cl2,cl1) :: old_univars;
1451   try let res = f t1 t2 in univar_pairs := old_univars; res
1452   with exn -> univar_pairs := old_univars; raise exn
1453
1454 let univar_pairs = ref []
1455
1456
1457                               (*****************)
1458                               (*  Unification  *)
1459                               (*****************)
1460
1461
1462
1463 let rec has_cached_expansion p abbrev =
1464   match abbrev with
1465     Mnil                   -> false
1466   | Mcons(_, p', _, _, rem)   -> Path.same p p' || has_cached_expansion p rem
1467   | Mlink rem              -> has_cached_expansion p !rem
1468
1469 (**** Transform error trace ****)
1470 (* +++ Move it to some other place ? *)
1471
1472 let expand_trace env trace =
1473   List.fold_right
1474     (fun (t1, t2) rem ->
1475        (repr t1, full_expand env t1)::(repr t2, full_expand env t2)::rem)
1476     trace []
1477
1478 (* build a dummy variant type *)
1479 let mkvariant fields closed =
1480   newgenty
1481     (Tvariant
1482        {row_fields = fields; row_closed = closed; row_more = newvar();
1483         row_bound = (); row_fixed = false; row_name = None })
1484
1485 (* force unification in Reither when one side has as non-conjunctive type *)
1486 let rigid_variants = ref false
1487
1488 (**** Unification ****)
1489
1490 (* Return whether [t0] occurs in [ty]. Objects are also traversed. *)
1491 let deep_occur t0 ty =
1492   let rec occur_rec ty =
1493     let ty = repr ty in
1494     if ty.level >= lowest_level then begin
1495       if ty == t0 then raise Occur;
1496       ty.level <- pivot_level - ty.level;
1497       iter_type_expr occur_rec ty
1498     end
1499   in
1500   try
1501     occur_rec ty; unmark_type ty; false
1502   with Occur ->
1503     unmark_type ty; true
1504
1505 (*
1506    1. When unifying two non-abbreviated types, one type is made a link
1507       to the other. When unifying an abbreviated type with a
1508       non-abbreviated type, the non-abbreviated type is made a link to
1509       the other one. When unifying to abbreviated types, these two
1510       types are kept distincts, but they are made to (temporally)
1511       expand to the same type.
1512    2. Abbreviations with at least one parameter are systematically
1513       expanded. The overhead does not seem to high, and that way
1514       abbreviations where some parameters does not appear in the
1515       expansion, such as ['a t = int], are correctly handled. In
1516       particular, for this example, unifying ['a t] with ['b t] keeps
1517       ['a] and ['b] distincts. (Is it really important ?)
1518    3. Unifying an abbreviation ['a t = 'a] with ['a] should not yield
1519       ['a t as 'a]. Indeed, the type variable would otherwise be lost.
1520       This problem occurs for abbreviations expanding to a type
1521       variable, but also to many other constrained abbreviations (for
1522       instance, [(< x : 'a > -> unit) t = <x : 'a>]). The solution is
1523       that, if an abbreviation is unified with some subpart of its
1524       parameters, then the parameter actually does not get
1525       abbreviated.  It would be possible to check whether some
1526       information is indeed lost, but it probably does not worth it.
1527 *)
1528 let rec unify env t1 t2 =
1529   (* First step: special cases (optimizations) *)
1530   if t1 == t2 then () else
1531   let t1 = repr t1 in
1532   let t2 = repr t2 in
1533   if t1 == t2 then () else
1534
1535   try
1536     type_changed := true;
1537     match (t1.desc, t2.desc) with
1538       (Tvar, Tconstr _) when deep_occur t1 t2 ->
1539         unify2 env t1 t2
1540     | (Tconstr _, Tvar) when deep_occur t2 t1 ->
1541         unify2 env t1 t2
1542     | (Tvar, _) ->
1543         occur env t1 t2; occur_univar env t2;
1544         update_level env t1.level t2;
1545         link_type t1 t2
1546     | (_, Tvar) ->
1547         occur env t2 t1; occur_univar env t1;
1548         update_level env t2.level t1;
1549         link_type t2 t1
1550     | (Tunivar, Tunivar) ->
1551         unify_univar t1 t2 !univar_pairs;
1552         update_level env t1.level t2;
1553         link_type t1 t2
1554     | (Tconstr (p1, [], a1), Tconstr (p2, [], a2))
1555           when Path.same p1 p2
1556             (* This optimization assumes that t1 does not expand to t2
1557                (and conversely), so we fall back to the general case
1558                when any of the types has a cached expansion. *)
1559             && not (has_cached_expansion p1 !a1
1560                  || has_cached_expansion p2 !a2) ->
1561         update_level env t1.level t2;
1562         link_type t1 t2
1563     | _ ->
1564         unify2 env t1 t2
1565   with Unify trace ->
1566     raise (Unify ((t1, t2)::trace))
1567
1568 and unify2 env t1 t2 =
1569   (* Second step: expansion of abbreviations *)
1570   let rec expand_both t1'' t2'' =
1571     let t1' = expand_head_unif env t1 in
1572     let t2' = expand_head_unif env t2 in
1573     (* Expansion may have changed the representative of the types... *)
1574     if t1' == t1'' && t2' == t2'' then (t1',t2') else
1575     expand_both t1' t2'
1576   in
1577   let t1', t2' = expand_both t1 t2 in
1578   if t1' == t2' then () else
1579
1580   let t1 = repr t1 and t2 = repr t2 in
1581   if (t1 == t1') || (t2 != t2') then
1582     unify3 env t1 t1' t2 t2'
1583   else
1584     try unify3 env t2 t2' t1 t1' with Unify trace ->
1585       raise (Unify (List.map (fun (x, y) -> (y, x)) trace))
1586
1587 and unify3 env t1 t1' t2 t2' =
1588   (* Third step: truly unification *)
1589   (* Assumes either [t1 == t1'] or [t2 != t2'] *)
1590   let d1 = t1'.desc and d2 = t2'.desc in
1591
1592   let create_recursion = (t2 != t2') && (deep_occur t1' t2) in
1593   occur env t1' t2;
1594   update_level env t1'.level t2;
1595   link_type t1' t2;
1596
1597   try
1598     begin match (d1, d2) with
1599       (Tvar, _) ->
1600         occur_univar env t2
1601     | (_, Tvar) ->
1602         let td1 = newgenty d1 in
1603         occur env t2' td1;
1604         occur_univar env td1;
1605         if t1 == t1' then begin
1606           (* The variable must be instantiated... *)
1607           let ty = newty2 t1'.level d1 in
1608           update_level env t2'.level ty;
1609           link_type t2' ty
1610         end else begin
1611           log_type t1';
1612           t1'.desc <- d1;
1613           update_level env t2'.level t1;
1614           link_type t2' t1
1615         end
1616     | (Tarrow (l1, t1, u1, c1), Tarrow (l2, t2, u2, c2)) when l1 = l2
1617       || !Clflags.classic && not (is_optional l1 || is_optional l2) ->
1618         unify env t1 t2; unify env u1 u2;
1619         begin match commu_repr c1, commu_repr c2 with
1620           Clink r, c2 -> set_commu r c2
1621         | c1, Clink r -> set_commu r c1
1622         | _ -> ()
1623         end
1624     | (Ttuple tl1, Ttuple tl2) ->
1625         unify_list env tl1 tl2
1626     | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) when Path.same p1 p2 ->
1627         unify_list env tl1 tl2
1628     | (Tobject (fi1, nm1), Tobject (fi2, _)) ->
1629         unify_fields env fi1 fi2;
1630         (* Type [t2'] may have been instantiated by [unify_fields] *)
1631         (* XXX One should do some kind of unification... *)
1632         begin match (repr t2').desc with
1633           Tobject (_, {contents = Some (_, va::_)})
1634           when let va = repr va in List.mem va.desc [Tvar; Tunivar; Tnil] ->
1635             ()
1636         | Tobject (_, nm2) ->
1637             set_name nm2 !nm1
1638         | _ ->
1639             ()
1640         end
1641     | (Tvariant row1, Tvariant row2) ->
1642         unify_row env row1 row2
1643     | (Tfield _, Tfield _) ->           (* Actually unused *)
1644         unify_fields env t1' t2'
1645     | (Tfield(f,kind,_,rem), Tnil) | (Tnil, Tfield(f,kind,_,rem)) ->
1646         begin match field_kind_repr kind with
1647           Fvar r when f <> dummy_method -> set_kind r Fabsent
1648         | _      -> raise (Unify [])
1649         end
1650     | (Tnil, Tnil) ->
1651         ()
1652     | (Tpoly (t1, []), Tpoly (t2, [])) ->
1653         unify env t1 t2
1654     | (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
1655         enter_poly env univar_pairs t1 tl1 t2 tl2 (unify env)
1656     | (_, _) ->
1657         raise (Unify [])
1658     end;
1659
1660 (* XXX Commentaires + changer "create_recursion" *)
1661     if create_recursion then begin
1662       match t2.desc with
1663         Tconstr (p, tl, abbrev) ->
1664           forget_abbrev abbrev p;
1665           let t2'' = expand_head_unif env t2 in
1666           if not (closed_parameterized_type tl t2'') then
1667             link_type (repr t2) (repr t2')
1668       | _ ->
1669           () (* t2 has already been expanded by update_level *)
1670     end
1671
1672 (*
1673     (*
1674        Can only be done afterwards, once the row variable has
1675        (possibly) been instantiated.
1676     *)
1677     if t1 != t1' (* && t2 != t2' *) then begin
1678       match (t1.desc, t2.desc) with
1679         (Tconstr (p, ty::_, _), _)
1680             when ((repr ty).desc <> Tvar)
1681               && weak_abbrev p
1682               && not (deep_occur t1 t2) ->
1683           update_level env t1.level t2;
1684           link_type t1 t2
1685       | (_, Tconstr (p, ty::_, _))
1686             when ((repr ty).desc <> Tvar)
1687               && weak_abbrev p
1688               && not (deep_occur t2 t1) ->
1689           update_level env t2.level t1;
1690           link_type t2 t1;
1691           link_type t1' t2'
1692       | _ ->
1693           ()
1694     end
1695 *)
1696   with Unify trace ->
1697     t1'.desc <- d1;
1698     raise (Unify trace)
1699
1700 and unify_list env tl1 tl2 =
1701   if List.length tl1 <> List.length tl2 then
1702     raise (Unify []);
1703   List.iter2 (unify env) tl1 tl2
1704
1705 and unify_fields env ty1 ty2 =          (* Optimization *)
1706   let (fields1, rest1) = flatten_fields ty1
1707   and (fields2, rest2) = flatten_fields ty2 in
1708   let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
1709   let l1 = (repr ty1).level and l2 = (repr ty2).level in
1710   let va =
1711     if miss1 = [] then rest2
1712     else if miss2 = [] then rest1
1713     else newty2 (min l1 l2) Tvar
1714   in
1715   let d1 = rest1.desc and d2 = rest2.desc in
1716   try
1717     unify env (build_fields l1 miss1 va) rest2;
1718     unify env rest1 (build_fields l2 miss2 va);
1719     List.iter
1720       (fun (n, k1, t1, k2, t2) ->
1721         unify_kind k1 k2;
1722         try unify env t1 t2 with Unify trace ->
1723           raise (Unify ((newty (Tfield(n, k1, t1, va)),
1724                          newty (Tfield(n, k2, t2, va)))::trace)))
1725       pairs
1726   with exn ->
1727     log_type rest1; rest1.desc <- d1;
1728     log_type rest2; rest2.desc <- d2;
1729     raise exn
1730
1731 and unify_kind k1 k2 =
1732   let k1 = field_kind_repr k1 in
1733   let k2 = field_kind_repr k2 in
1734   if k1 == k2 then () else
1735   match k1, k2 with
1736     (Fvar r, (Fvar _ | Fpresent)) -> set_kind r k2
1737   | (Fpresent, Fvar r)            -> set_kind r k1
1738   | (Fpresent, Fpresent)          -> ()
1739   | _                             -> assert false
1740
1741 and unify_pairs env tpl =
1742   List.iter (fun (t1, t2) -> unify env t1 t2) tpl
1743
1744 and unify_row env row1 row2 =
1745   let row1 = row_repr row1 and row2 = row_repr row2 in
1746   let rm1 = row_more row1 and rm2 = row_more row2 in
1747   if rm1 == rm2 then () else
1748   let r1, r2, pairs = merge_row_fields row1.row_fields row2.row_fields in
1749   if r1 <> [] && r2 <> [] then begin
1750     let ht = Hashtbl.create (List.length r1) in
1751     List.iter (fun (l,_) -> Hashtbl.add ht (hash_variant l) l) r1;
1752     List.iter
1753       (fun (l,_) ->
1754         try raise (Tags(l, Hashtbl.find ht (hash_variant l)))
1755         with Not_found -> ())
1756       r2
1757   end;
1758   let more =
1759     if row1.row_fixed then rm1 else
1760     if row2.row_fixed then rm2 else
1761     newgenvar ()
1762   in update_level env (min rm1.level rm2.level) more;
1763   let fixed = row1.row_fixed || row2.row_fixed
1764   and closed = row1.row_closed || row2.row_closed in
1765   let keep switch =
1766     List.for_all
1767       (fun (_,f1,f2) ->
1768         let f1, f2 = switch f1 f2 in
1769         row_field_repr f1 = Rabsent || row_field_repr f2 <> Rabsent)
1770       pairs
1771   in
1772   let empty fields =
1773     List.for_all (fun (_,f) -> row_field_repr f = Rabsent) fields in
1774   (* Check whether we are going to build an empty type *)
1775   if closed && (empty r1 || row2.row_closed) && (empty r2 || row1.row_closed)
1776   && List.for_all
1777       (fun (_,f1,f2) ->
1778         row_field_repr f1 = Rabsent || row_field_repr f2 = Rabsent)
1779       pairs
1780   then raise (Unify [mkvariant [] true, mkvariant [] true]);
1781   let name =
1782     if row1.row_name <> None && (row1.row_closed || empty r2) &&
1783       (not row2.row_closed || keep (fun f1 f2 -> f1, f2) && empty r1)
1784     then row1.row_name
1785     else if row2.row_name <> None && (row2.row_closed || empty r1) &&
1786       (not row1.row_closed || keep (fun f1 f2 -> f2, f1) && empty r2)
1787     then row2.row_name
1788     else None
1789   in
1790   let row0 = {row_fields = []; row_more = more; row_bound = ();
1791               row_closed = closed; row_fixed = fixed; row_name = name} in
1792   let set_more row rest =
1793     let rest =
1794       if closed then
1795         filter_row_fields row.row_closed rest
1796       else rest in
1797     if rest <> [] && (row.row_closed || row.row_fixed)
1798     || closed && row.row_fixed && not row.row_closed then begin
1799       let t1 = mkvariant [] true and t2 = mkvariant rest false in
1800       raise (Unify [if row == row1 then (t1,t2) else (t2,t1)])
1801     end;
1802     let rm = row_more row in
1803     if row.row_fixed then
1804       if row0.row_more == rm then () else
1805       if rm.desc = Tvar then link_type rm row0.row_more else
1806       unify env rm row0.row_more
1807     else
1808       let ty = newty2 generic_level (Tvariant {row0 with row_fields = rest}) in
1809       update_level env rm.level ty;
1810       link_type rm ty
1811   in
1812   let md1 = rm1.desc and md2 = rm2.desc in
1813   begin try
1814     set_more row2 r1;
1815     set_more row1 r2;
1816     List.iter
1817       (fun (l,f1,f2) ->
1818         try unify_row_field env row1.row_fixed row2.row_fixed l f1 f2
1819         with Unify trace ->
1820           raise (Unify ((mkvariant [l,f1] true,
1821                          mkvariant [l,f2] true) :: trace)))
1822       pairs;
1823   with exn ->
1824     log_type rm1; rm1.desc <- md1; log_type rm2; rm2.desc <- md2; raise exn
1825   end
1826
1827 and unify_row_field env fixed1 fixed2 l f1 f2 =
1828   let f1 = row_field_repr f1 and f2 = row_field_repr f2 in
1829   if f1 == f2 then () else
1830   match f1, f2 with
1831     Rpresent(Some t1), Rpresent(Some t2) -> unify env t1 t2
1832   | Rpresent None, Rpresent None -> ()
1833   | Reither(c1, tl1, m1, e1), Reither(c2, tl2, m2, e2) ->
1834       if e1 == e2 then () else
1835       let redo =
1836         (m1 || m2 ||
1837          !rigid_variants && (List.length tl1 = 1 || List.length tl2 = 1)) &&
1838         begin match tl1 @ tl2 with [] -> false
1839         | t1 :: tl ->
1840             if c1 || c2 then raise (Unify []);
1841             List.iter (unify env t1) tl;
1842             !e1 <> None || !e2 <> None
1843         end in
1844       if redo then unify_row_field env fixed1 fixed2 l f1 f2 else
1845       let tl1 = List.map repr tl1 and tl2 = List.map repr tl2 in
1846       let rec remq tl = function [] -> []
1847         | ty :: tl' ->
1848             if List.memq ty tl then remq tl tl' else ty :: remq tl tl'
1849       in
1850       let tl2' = remq tl2 tl1 and tl1' = remq tl1 tl2 in
1851       let e = ref None in
1852       let f1' = Reither(c1 || c2, tl1', m1 || m2, e)
1853       and f2' = Reither(c1 || c2, tl2', m1 || m2, e) in
1854       set_row_field e1 f1'; set_row_field e2 f2';
1855   | Reither(_, _, false, e1), Rabsent -> set_row_field e1 f2
1856   | Rabsent, Reither(_, _, false, e2) -> set_row_field e2 f1
1857   | Rabsent, Rabsent -> ()
1858   | Reither(false, tl, _, e1), Rpresent(Some t2) when not fixed1 ->
1859       set_row_field e1 f2;
1860       (try List.iter (fun t1 -> unify env t1 t2) tl
1861       with exn -> e1 := None; raise exn)
1862   | Rpresent(Some t1), Reither(false, tl, _, e2) when not fixed2 ->
1863       set_row_field e2 f1;
1864       (try List.iter (unify env t1) tl
1865       with exn -> e2 := None; raise exn)
1866   | Reither(true, [], _, e1), Rpresent None when not fixed1 ->
1867       set_row_field e1 f2
1868   | Rpresent None, Reither(true, [], _, e2) when not fixed2 ->
1869       set_row_field e2 f1
1870   | _ -> raise (Unify [])
1871
1872
1873 let unify env ty1 ty2 =
1874   try
1875     unify env ty1 ty2
1876   with Unify trace ->
1877     raise (Unify (expand_trace env trace))
1878
1879 let unify_var env t1 t2 =
1880   let t1 = repr t1 and t2 = repr t2 in
1881   if t1 == t2 then () else
1882   match t1.desc with
1883     Tvar ->
1884       begin try
1885         occur env t1 t2;
1886         update_level env t1.level t2;
1887         link_type t1 t2
1888       with Unify trace ->
1889         raise (Unify (expand_trace env ((t1,t2)::trace)))
1890       end
1891   | _ ->
1892       unify env t1 t2
1893
1894 let _ = unify' := unify_var
1895
1896 let unify_pairs env ty1 ty2 pairs =
1897   univar_pairs := pairs;
1898   unify env ty1 ty2
1899
1900 let unify env ty1 ty2 =
1901   univar_pairs := [];
1902   unify env ty1 ty2
1903
1904
1905 (**** Special cases of unification ****)
1906
1907 (*
1908    Unify [t] and [l:'a -> 'b]. Return ['a] and ['b].
1909    In label mode, label mismatch is accepted when
1910    (1) the requested label is ""
1911    (2) the original label is not optional
1912 *)
1913 let rec filter_arrow env t l =
1914   let t = expand_head_unif env t in
1915   match t.desc with
1916     Tvar ->
1917       let t1 = newvar () and t2 = newvar () in
1918       let t' = newty (Tarrow (l, t1, t2, Cok)) in
1919       update_level env t.level t';
1920       link_type t t';
1921       (t1, t2)
1922   | Tarrow(l', t1, t2, _)
1923     when l = l' || !Clflags.classic && l = "" && not (is_optional l') ->
1924       (t1, t2)
1925   | _ ->
1926       raise (Unify [])
1927
1928 (* Used by [filter_method]. *)
1929 let rec filter_method_field env name priv ty =
1930   let ty = repr ty in
1931   match ty.desc with
1932     Tvar ->
1933       let level = ty.level in
1934       let ty1 = newvar2 level and ty2 = newvar2 level in
1935       let ty' = newty2 level (Tfield (name,
1936                                       begin match priv with
1937                                         Private -> Fvar (ref None)
1938                                       | Public  -> Fpresent
1939                                       end,
1940                                       ty1, ty2))
1941       in
1942       link_type ty ty';
1943       ty1
1944   | Tfield(n, kind, ty1, ty2) ->
1945       let kind = field_kind_repr kind in
1946       if (n = name) && (kind <> Fabsent) then begin
1947         if priv = Public then
1948           unify_kind kind Fpresent;
1949         ty1
1950       end else
1951         filter_method_field env name priv ty2
1952   | _ ->
1953       raise (Unify [])
1954
1955 (* Unify [ty] and [< name : 'a; .. >]. Return ['a]. *)
1956 let rec filter_method env name priv ty =
1957   let ty = expand_head_unif env ty in
1958   match ty.desc with
1959     Tvar ->
1960       let ty1 = newvar () in
1961       let ty' = newobj ty1 in
1962       update_level env ty.level ty';
1963       link_type ty ty';
1964       filter_method_field env name priv ty1
1965   | Tobject(f, _) ->
1966       filter_method_field env name priv f
1967   | _ ->
1968       raise (Unify [])
1969
1970 let check_filter_method env name priv ty =
1971   ignore(filter_method env name priv ty)
1972
1973 let filter_self_method env lab priv meths ty =
1974   let ty' = filter_method env lab priv ty in
1975   try
1976     Meths.find lab !meths
1977   with Not_found ->
1978     let pair = (Ident.create lab, ty') in
1979     meths := Meths.add lab pair !meths;
1980     pair
1981
1982
1983                         (***********************************)
1984                         (*  Matching between type schemes  *)
1985                         (***********************************)
1986
1987 (*
1988    Update the level of [ty]. First check that the levels of generic
1989    variables from the subject are not lowered.
1990 *)
1991 let moregen_occur env level ty =
1992   let rec occur ty =
1993     let ty = repr ty in
1994     if ty.level > level then begin
1995       if ty.desc = Tvar && ty.level >= generic_level - 1 then raise Occur;
1996       ty.level <- pivot_level - ty.level;
1997       match ty.desc with
1998         Tvariant row when static_row row ->
1999           iter_row occur row
2000       | _ ->
2001           iter_type_expr occur ty
2002     end
2003   in
2004   begin try
2005     occur ty; unmark_type ty
2006   with Occur ->
2007     unmark_type ty; raise (Unify [])
2008   end;
2009   (* also check for free univars *)
2010   occur_univar env ty;
2011   update_level env level ty
2012
2013 let may_instantiate inst_nongen t1 =
2014   if inst_nongen then t1.level <> generic_level - 1
2015                  else t1.level =  generic_level
2016
2017 let rec moregen inst_nongen type_pairs env t1 t2 =
2018   if t1 == t2 then () else
2019   let t1 = repr t1 in
2020   let t2 = repr t2 in
2021   if t1 == t2 then () else
2022
2023   try
2024     match (t1.desc, t2.desc) with
2025       (Tunivar, Tunivar) ->
2026         unify_univar t1 t2 !univar_pairs
2027     | (Tvar, _) when may_instantiate inst_nongen t1 ->
2028         moregen_occur env t1.level t2;
2029         occur env t1 t2;
2030         link_type t1 t2
2031     | (Tconstr (p1, [], _), Tconstr (p2, [], _)) when Path.same p1 p2 ->
2032         ()
2033     | _ ->
2034         let t1' = expand_head_unif env t1 in
2035         let t2' = expand_head_unif env t2 in
2036         (* Expansion may have changed the representative of the types... *)
2037         let t1' = repr t1' and t2' = repr t2' in
2038         if t1' == t2' then () else
2039         begin try
2040           TypePairs.find type_pairs (t1', t2')
2041         with Not_found ->
2042           TypePairs.add type_pairs (t1', t2') ();
2043           match (t1'.desc, t2'.desc) with
2044             (Tvar, _) when may_instantiate inst_nongen t1' ->
2045               moregen_occur env t1'.level t2;
2046               link_type t1' t2
2047           | (Tarrow (l1, t1, u1, _), Tarrow (l2, t2, u2, _)) when l1 = l2
2048             || !Clflags.classic && not (is_optional l1 || is_optional l2) ->
2049               moregen inst_nongen type_pairs env t1 t2;
2050               moregen inst_nongen type_pairs env u1 u2
2051           | (Ttuple tl1, Ttuple tl2) ->
2052               moregen_list inst_nongen type_pairs env tl1 tl2
2053           | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _))
2054                 when Path.same p1 p2 ->
2055               moregen_list inst_nongen type_pairs env tl1 tl2
2056           | (Tvariant row1, Tvariant row2) ->
2057               moregen_row inst_nongen type_pairs env row1 row2
2058           | (Tobject (fi1, nm1), Tobject (fi2, nm2)) ->
2059               moregen_fields inst_nongen type_pairs env fi1 fi2
2060           | (Tfield _, Tfield _) ->           (* Actually unused *)
2061               moregen_fields inst_nongen type_pairs env t1' t2'
2062           | (Tnil, Tnil) ->
2063               ()
2064           | (Tpoly (t1, []), Tpoly (t2, [])) ->
2065               moregen inst_nongen type_pairs env t1 t2
2066           | (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
2067               enter_poly env univar_pairs t1 tl1 t2 tl2
2068                 (moregen inst_nongen type_pairs env)
2069           | (_, _) ->
2070               raise (Unify [])
2071         end
2072   with Unify trace ->
2073     raise (Unify ((t1, t2)::trace))
2074
2075 and moregen_list inst_nongen type_pairs env tl1 tl2 =
2076   if List.length tl1 <> List.length tl2 then
2077     raise (Unify []);
2078   List.iter2 (moregen inst_nongen type_pairs env) tl1 tl2
2079
2080 and moregen_fields inst_nongen type_pairs env ty1 ty2 =
2081   let (fields1, rest1) = flatten_fields ty1
2082   and (fields2, rest2) = flatten_fields ty2 in
2083   let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
2084   if miss1 <> [] then raise (Unify []);
2085   moregen inst_nongen type_pairs env rest1
2086     (build_fields (repr ty2).level miss2 rest2);
2087   List.iter
2088     (fun (n, k1, t1, k2, t2) ->
2089        moregen_kind k1 k2;
2090        try moregen inst_nongen type_pairs env t1 t2 with Unify trace ->
2091          raise (Unify ((newty (Tfield(n, k1, t1, rest2)),
2092                         newty (Tfield(n, k2, t2, rest2)))::trace)))
2093     pairs
2094
2095 and moregen_kind k1 k2 =
2096   let k1 = field_kind_repr k1 in
2097   let k2 = field_kind_repr k2 in
2098   if k1 == k2 then () else
2099   match k1, k2 with
2100     (Fvar r, (Fvar _ | Fpresent))  -> set_kind r k2
2101   | (Fpresent, Fpresent)           -> ()
2102   | _                              -> raise (Unify [])
2103
2104 and moregen_row inst_nongen type_pairs env row1 row2 =
2105   let row1 = row_repr row1 and row2 = row_repr row2 in
2106   let rm1 = repr row1.row_more and rm2 = repr row2.row_more in
2107   if rm1 == rm2 then () else
2108   let may_inst = rm1.desc = Tvar && may_instantiate inst_nongen rm1 in
2109   let r1, r2, pairs = merge_row_fields row1.row_fields row2.row_fields in
2110   let r1, r2 =
2111     if row2.row_closed then
2112       filter_row_fields may_inst r1, filter_row_fields false r2
2113     else r1, r2
2114   in
2115   if r1 <> [] || row1.row_closed && (not row2.row_closed || r2 <> [])
2116   then raise (Unify []);
2117   begin match rm1.desc, rm2.desc with
2118     Tunivar, Tunivar ->
2119       unify_univar rm1 rm2 !univar_pairs
2120   | Tunivar, _ | _, Tunivar ->
2121       raise (Unify [])
2122   | _ when static_row row1 -> ()
2123   | _ when may_inst ->
2124       if not (static_row row2) then moregen_occur env rm1.level rm2;
2125       let ext =
2126         if r2 = [] then rm2 else
2127         let row_ext = {row2 with row_fields = r2} in
2128         iter_row (moregen_occur env rm1.level) row_ext;
2129         newty2 rm1.level (Tvariant row_ext)
2130       in
2131       link_type rm1 ext
2132   | Tconstr _, Tconstr _ ->
2133       moregen inst_nongen type_pairs env rm1 rm2
2134   | _ -> raise (Unify [])
2135   end;
2136   List.iter
2137     (fun (l,f1,f2) ->
2138       let f1 = row_field_repr f1 and f2 = row_field_repr f2 in
2139       if f1 == f2 then () else
2140       match f1, f2 with
2141         Rpresent(Some t1), Rpresent(Some t2) ->
2142           moregen inst_nongen type_pairs env t1 t2
2143       | Rpresent None, Rpresent None -> ()
2144       | Reither(false, tl1, _, e1), Rpresent(Some t2) when may_inst ->
2145           set_row_field e1 f2;
2146           List.iter (fun t1 -> moregen inst_nongen type_pairs env t1 t2) tl1
2147       | Reither(c1, tl1, _, e1), Reither(c2, tl2, m2, e2) ->
2148           if e1 != e2 then begin
2149             if c1 && not c2 then raise(Unify []);
2150             set_row_field e1 (Reither (c2, [], m2, e2));
2151             if List.length tl1 = List.length tl2 then
2152               List.iter2 (moregen inst_nongen type_pairs env) tl1 tl2
2153             else match tl2 with
2154               t2 :: _ ->
2155                 List.iter (fun t1 -> moregen inst_nongen type_pairs env t1 t2)
2156                   tl1
2157             | [] ->
2158                 if tl1 <> [] then raise (Unify [])
2159           end
2160       | Reither(true, [], _, e1), Rpresent None when may_inst ->
2161           set_row_field e1 f2
2162       | Reither(_, _, _, e1), Rabsent when may_inst ->
2163           set_row_field e1 f2
2164       | Rabsent, Rabsent -> ()
2165       | _ -> raise (Unify []))
2166     pairs
2167
2168 (* Must empty univar_pairs first *)
2169 let moregen inst_nongen type_pairs env patt subj =
2170   univar_pairs := [];
2171   moregen inst_nongen type_pairs env patt subj
2172
2173 (*
2174    Non-generic variable can be instanciated only if [inst_nongen] is
2175    true. So, [inst_nongen] should be set to false if the subject might
2176    contain non-generic variables (and we do not want them to be
2177    instanciated).
2178    Usually, the subject is given by the user, and the pattern
2179    is unimportant.  So, no need to propagate abbreviations.
2180 *)
2181 let moregeneral env inst_nongen pat_sch subj_sch =
2182   let old_level = !current_level in
2183   current_level := generic_level - 1;
2184   (*
2185      Generic variables are first duplicated with [instance].  So,
2186      their levels are lowered to [generic_level - 1].  The subject is
2187      then copied with [duplicate_type].  That way, its levels won't be
2188      changed.
2189   *)
2190   let subj = duplicate_type (instance subj_sch) in
2191   current_level := generic_level;
2192   (* Duplicate generic variables *)
2193   let patt = instance pat_sch in
2194   let res =
2195     try moregen inst_nongen (TypePairs.create 13) env patt subj; true with
2196       Unify _ -> false
2197   in
2198   current_level := old_level;
2199   res
2200
2201
2202 (* Alternative approach: "rigidify" a type scheme,
2203    and check validity after unification *)
2204 (* Simpler, no? *)
2205
2206 let rec rigidify_rec vars ty =
2207   let ty = repr ty in
2208   if ty.level >= lowest_level then begin
2209     ty.level <- pivot_level - ty.level;
2210     match ty.desc with
2211     | Tvar ->
2212         if not (List.memq ty !vars) then vars := ty :: !vars
2213     | Tvariant row ->
2214         let row = row_repr row in
2215         let more = repr row.row_more in
2216         if more.desc = Tvar && not row.row_fixed then begin
2217           let more' = newty2 more.level Tvar in
2218           let row' = {row with row_fixed=true; row_fields=[]; row_more=more'}
2219           in link_type more (newty2 ty.level (Tvariant row'))
2220         end;
2221         iter_row (rigidify_rec vars) row;
2222         (* only consider the row variable if the variant is not static *)
2223         if not (static_row row) then rigidify_rec vars (row_more row)
2224     | _ ->
2225         iter_type_expr (rigidify_rec vars) ty
2226   end
2227
2228 let rigidify ty =
2229   let vars = ref [] in
2230   rigidify_rec vars ty;
2231   unmark_type ty;
2232   !vars
2233
2234 let all_distinct_vars env vars =
2235   let tyl = ref [] in
2236   List.for_all
2237     (fun ty ->
2238       let ty = expand_head env ty in
2239       if List.memq ty !tyl then false else
2240       (tyl := ty :: !tyl; ty.desc = Tvar))
2241     vars
2242
2243 let matches env ty ty' =
2244   let snap = snapshot () in
2245   let vars = rigidify ty in
2246   cleanup_abbrev ();
2247   let ok =
2248     try unify env ty ty'; all_distinct_vars env vars
2249     with Unify _ -> false
2250   in
2251   backtrack snap;
2252   ok
2253
2254
2255                  (*********************************************)
2256                  (*  Equivalence between parameterized types  *)
2257                  (*********************************************)
2258
2259 let expand_head_rigid env ty =
2260   let old = !rigid_variants in
2261   rigid_variants := true;
2262   let ty' = expand_head_unif env ty in
2263   rigid_variants := old; ty'
2264
2265 let normalize_subst subst =
2266   if List.exists
2267       (function {desc=Tlink _}, _ | _, {desc=Tlink _} -> true | _ -> false)
2268       !subst
2269   then subst := List.map (fun (t1,t2) -> repr t1, repr t2) !subst
2270
2271 let rec eqtype rename type_pairs subst env t1 t2 =
2272   if t1 == t2 then () else
2273   let t1 = repr t1 in
2274   let t2 = repr t2 in
2275   if t1 == t2 then () else
2276
2277   try
2278     match (t1.desc, t2.desc) with
2279       (Tvar, Tvar) when rename ->
2280         begin try
2281           normalize_subst subst;
2282           if List.assq t1 !subst != t2 then raise (Unify [])
2283         with Not_found ->
2284           subst := (t1, t2) :: !subst
2285         end
2286     | (Tconstr (p1, [], _), Tconstr (p2, [], _)) when Path.same p1 p2 ->
2287         ()
2288     | _ ->
2289         let t1' = expand_head_rigid env t1 in
2290         let t2' = expand_head_rigid env t2 in
2291         (* Expansion may have changed the representative of the types... *)
2292         let t1' = repr t1' and t2' = repr t2' in
2293         if t1' == t2' then () else
2294         begin try
2295           TypePairs.find type_pairs (t1', t2')
2296         with Not_found ->
2297           TypePairs.add type_pairs (t1', t2') ();
2298           match (t1'.desc, t2'.desc) with
2299             (Tvar, Tvar) when rename ->
2300               begin try
2301                 normalize_subst subst;
2302                 if List.assq t1' !subst != t2' then raise (Unify [])
2303               with Not_found ->
2304                 subst := (t1', t2') :: !subst
2305               end
2306           | (Tarrow (l1, t1, u1, _), Tarrow (l2, t2, u2, _)) when l1 = l2
2307             || !Clflags.classic && not (is_optional l1 || is_optional l2) ->
2308               eqtype rename type_pairs subst env t1 t2;
2309               eqtype rename type_pairs subst env u1 u2;
2310           | (Ttuple tl1, Ttuple tl2) ->
2311               eqtype_list rename type_pairs subst env tl1 tl2
2312           | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _))
2313                 when Path.same p1 p2 ->
2314               eqtype_list rename type_pairs subst env tl1 tl2
2315           | (Tvariant row1, Tvariant row2) ->
2316               eqtype_row rename type_pairs subst env row1 row2
2317           | (Tobject (fi1, nm1), Tobject (fi2, nm2)) ->
2318               eqtype_fields rename type_pairs subst env fi1 fi2
2319           | (Tfield _, Tfield _) ->       (* Actually unused *)
2320               eqtype_fields rename type_pairs subst env t1' t2'
2321           | (Tnil, Tnil) ->
2322               ()
2323           | (Tpoly (t1, []), Tpoly (t2, [])) ->
2324               eqtype rename type_pairs subst env t1 t2
2325           | (Tpoly (t1, tl1), Tpoly (t2, tl2)) ->
2326               enter_poly env univar_pairs t1 tl1 t2 tl2
2327                 (eqtype rename type_pairs subst env)
2328           | (Tunivar, Tunivar) ->
2329               unify_univar t1' t2' !univar_pairs
2330           | (_, _) ->
2331               raise (Unify [])
2332         end
2333   with Unify trace ->
2334     raise (Unify ((t1, t2)::trace))
2335
2336 and eqtype_list rename type_pairs subst env tl1 tl2 =
2337   if List.length tl1 <> List.length tl2 then
2338     raise (Unify []);
2339   List.iter2 (eqtype rename type_pairs subst env) tl1 tl2
2340
2341 and eqtype_fields rename type_pairs subst env ty1 ty2 =
2342   let (fields2, rest2) = flatten_fields ty2 in
2343   (* Try expansion, needed when called from Includecore.type_manifest *)
2344   match expand_head_rigid env rest2 with
2345     {desc=Tobject(ty2,_)} -> eqtype_fields rename type_pairs subst env ty1 ty2
2346   | _ ->
2347   let (fields1, rest1) = flatten_fields ty1 in
2348   let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
2349   eqtype rename type_pairs subst env rest1 rest2;
2350   if (miss1 <> []) || (miss2 <> []) then raise (Unify []);
2351   List.iter
2352     (function (n, k1, t1, k2, t2) ->
2353        eqtype_kind k1 k2;
2354        try eqtype rename type_pairs subst env t1 t2 with Unify trace ->
2355          raise (Unify ((newty (Tfield(n, k1, t1, rest2)),
2356                         newty (Tfield(n, k2, t2, rest2)))::trace)))
2357     pairs
2358
2359 and eqtype_kind k1 k2 =
2360   let k1 = field_kind_repr k1 in
2361   let k2 = field_kind_repr k2 in
2362   match k1, k2 with
2363     (Fvar _, Fvar _)
2364   | (Fpresent, Fpresent) -> ()
2365   | _                    -> raise (Unify [])
2366
2367 and eqtype_row rename type_pairs subst env row1 row2 =
2368   (* Try expansion, needed when called from Includecore.type_manifest *)
2369   match expand_head_rigid env (row_more row2) with
2370     {desc=Tvariant row2} -> eqtype_row rename type_pairs subst env row1 row2
2371   | _ ->
2372   let row1 = row_repr row1 and row2 = row_repr row2 in
2373   let r1, r2, pairs = merge_row_fields row1.row_fields row2.row_fields in
2374   if row1.row_closed <> row2.row_closed
2375   || not row1.row_closed && (r1 <> [] || r2 <> [])
2376   || filter_row_fields false (r1 @ r2) <> []
2377   then raise (Unify []);
2378   if not (static_row row1) then
2379     eqtype rename type_pairs subst env row1.row_more row2.row_more;
2380   List.iter
2381     (fun (_,f1,f2) ->
2382       match row_field_repr f1, row_field_repr f2 with
2383         Rpresent(Some t1), Rpresent(Some t2) ->
2384           eqtype rename type_pairs subst env t1 t2
2385       | Reither(true, [], _, _), Reither(true, [], _, _) ->
2386           ()
2387       | Reither(false, t1::tl1, _, _), Reither(false, t2::tl2, _, _) ->
2388           eqtype rename type_pairs subst env t1 t2;
2389           if List.length tl1 = List.length tl2 then
2390             (* if same length allow different types (meaning?) *)
2391             List.iter2 (eqtype rename type_pairs subst env) tl1 tl2
2392           else begin
2393             (* otherwise everything must be equal *)
2394             List.iter (eqtype rename type_pairs subst env t1) tl2;
2395             List.iter (fun t1 -> eqtype rename type_pairs subst env t1 t2) tl1
2396           end
2397       | Rpresent None, Rpresent None -> ()
2398       | Rabsent, Rabsent -> ()
2399       | _ -> raise (Unify []))
2400     pairs
2401
2402 (* Two modes: with or without renaming of variables *)
2403 let equal env rename tyl1 tyl2 =
2404   try
2405     univar_pairs := [];
2406     eqtype_list rename (TypePairs.create 11) (ref []) env tyl1 tyl2; true
2407   with
2408     Unify _ -> false
2409
2410 (* Must empty univar_pairs first *)
2411 let eqtype rename type_pairs subst env t1 t2 =
2412   univar_pairs := [];
2413   eqtype rename type_pairs subst env t1 t2
2414
2415
2416                           (*************************)
2417                           (*  Class type matching  *)
2418                           (*************************)
2419
2420
2421 type class_match_failure =
2422     CM_Virtual_class
2423   | CM_Parameter_arity_mismatch of int * int
2424   | CM_Type_parameter_mismatch of (type_expr * type_expr) list
2425   | CM_Class_type_mismatch of class_type * class_type
2426   | CM_Parameter_mismatch of (type_expr * type_expr) list
2427   | CM_Val_type_mismatch of string * (type_expr * type_expr) list
2428   | CM_Meth_type_mismatch of string * (type_expr * type_expr) list
2429   | CM_Non_mutable_value of string
2430   | CM_Non_concrete_value of string
2431   | CM_Missing_value of string
2432   | CM_Missing_method of string
2433   | CM_Hide_public of string
2434   | CM_Hide_virtual of string * string
2435   | CM_Public_method of string
2436   | CM_Private_method of string
2437   | CM_Virtual_method of string
2438
2439 exception Failure of class_match_failure list
2440
2441 let rec moregen_clty trace type_pairs env cty1 cty2 =
2442   try
2443     match cty1, cty2 with
2444       Tcty_constr (_, _, cty1), _ ->
2445         moregen_clty true type_pairs env cty1 cty2
2446     | _, Tcty_constr (_, _, cty2) ->
2447         moregen_clty true type_pairs env cty1 cty2
2448     | Tcty_fun (l1, ty1, cty1'), Tcty_fun (l2, ty2, cty2') when l1 = l2 ->
2449         begin try moregen true type_pairs env ty1 ty2 with Unify trace ->
2450           raise (Failure [CM_Parameter_mismatch (expand_trace env trace)])
2451         end;
2452         moregen_clty false type_pairs env cty1' cty2'
2453     | Tcty_signature sign1, Tcty_signature sign2 ->
2454         let ty1 = object_fields (repr sign1.cty_self) in
2455         let ty2 = object_fields (repr sign2.cty_self) in
2456         let (fields1, rest1) = flatten_fields ty1
2457         and (fields2, rest2) = flatten_fields ty2 in
2458         let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
2459         List.iter
2460           (fun (lab, k1, t1, k2, t2) ->
2461             begin try moregen true type_pairs env t1 t2 with Unify trace ->
2462               raise (Failure [CM_Meth_type_mismatch
2463                                  (lab, expand_trace env trace)])
2464            end)
2465         pairs;
2466       Vars.iter
2467         (fun lab (mut, v, ty) ->
2468            let (mut', v', ty') = Vars.find lab sign1.cty_vars in
2469            try moregen true type_pairs env ty' ty with Unify trace ->
2470              raise (Failure [CM_Val_type_mismatch
2471                                 (lab, expand_trace env trace)]))
2472         sign2.cty_vars
2473   | _ ->
2474       raise (Failure [])
2475   with
2476     Failure error when trace ->
2477       raise (Failure (CM_Class_type_mismatch (cty1, cty2)::error))
2478
2479 let match_class_types env pat_sch subj_sch =
2480   let type_pairs = TypePairs.create 53 in
2481   let old_level = !current_level in
2482   current_level := generic_level - 1;
2483   (*
2484      Generic variables are first duplicated with [instance].  So,
2485      their levels are lowered to [generic_level - 1].  The subject is
2486      then copied with [duplicate_type].  That way, its levels won't be
2487      changed.
2488   *)
2489   let (_, subj_inst) = instance_class [] subj_sch in
2490   let subj = duplicate_class_type subj_inst in
2491   current_level := generic_level;
2492   (* Duplicate generic variables *)
2493   let (_, patt) = instance_class [] pat_sch in
2494   let res =
2495     let sign1 = signature_of_class_type patt in
2496     let sign2 = signature_of_class_type subj in
2497     let t1 = repr sign1.cty_self in
2498     let t2 = repr sign2.cty_self in
2499     TypePairs.add type_pairs (t1, t2) ();
2500     let (fields1, rest1) = flatten_fields (object_fields t1)
2501     and (fields2, rest2) = flatten_fields (object_fields t2) in
2502     let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
2503     let error =
2504       List.fold_right
2505         (fun (lab, k, _) err ->
2506            let err =
2507              let k = field_kind_repr k in
2508              begin match k with
2509                Fvar r -> set_kind r Fabsent; err
2510              | _      -> CM_Hide_public lab::err
2511              end
2512            in
2513            if Concr.mem lab sign1.cty_concr then err
2514            else CM_Hide_virtual ("method", lab) :: err)
2515         miss1 []
2516     in
2517     let missing_method = List.map (fun (m, _, _) -> m) miss2 in
2518     let error =
2519       (List.map (fun m -> CM_Missing_method m) missing_method) @ error
2520     in
2521     (* Always succeeds *)
2522     moregen true type_pairs env rest1 rest2;
2523     let error =
2524       List.fold_right
2525         (fun (lab, k1, t1, k2, t2) err ->
2526            try moregen_kind k1 k2; err with
2527              Unify _ -> CM_Public_method lab::err)
2528         pairs error
2529     in
2530     let error =
2531       Vars.fold
2532         (fun lab (mut, vr, ty) err ->
2533           try
2534             let (mut', vr', ty') = Vars.find lab sign1.cty_vars in
2535             if mut = Mutable && mut' <> Mutable then
2536               CM_Non_mutable_value lab::err
2537             else if vr = Concrete && vr' <> Concrete then
2538               CM_Non_concrete_value lab::err
2539             else
2540               err
2541           with Not_found ->
2542             CM_Missing_value lab::err)
2543         sign2.cty_vars error
2544     in
2545     let error =
2546       Vars.fold
2547         (fun lab (_,vr,_) err ->
2548           if vr = Virtual && not (Vars.mem lab sign2.cty_vars) then
2549             CM_Hide_virtual ("instance variable", lab) :: err
2550           else err)
2551         sign1.cty_vars error
2552     in
2553     let error =
2554       List.fold_right
2555         (fun e l ->
2556            if List.mem e missing_method then l else CM_Virtual_method e::l)
2557         (Concr.elements (Concr.diff sign2.cty_concr sign1.cty_concr))
2558         error
2559     in
2560     match error with
2561       [] ->
2562         begin try
2563           moregen_clty true type_pairs env patt subj;
2564           []
2565         with
2566           Failure r -> r
2567         end
2568     | error ->
2569         CM_Class_type_mismatch (patt, subj)::error
2570   in
2571   current_level := old_level;
2572   res
2573
2574 let rec equal_clty trace type_pairs subst env cty1 cty2 =
2575   try
2576     match cty1, cty2 with
2577       Tcty_constr (_, _, cty1), Tcty_constr (_, _, cty2) ->
2578         equal_clty true type_pairs subst env cty1 cty2
2579     | Tcty_constr (_, _, cty1), _ ->
2580         equal_clty true type_pairs subst env cty1 cty2
2581     | _, Tcty_constr (_, _, cty2) ->
2582         equal_clty true type_pairs subst env cty1 cty2
2583     | Tcty_fun (l1, ty1, cty1'), Tcty_fun (l2, ty2, cty2') when l1 = l2 ->
2584         begin try eqtype true type_pairs subst env ty1 ty2 with Unify trace ->
2585           raise (Failure [CM_Parameter_mismatch (expand_trace env trace)])
2586         end;
2587         equal_clty false type_pairs subst env cty1' cty2'
2588     | Tcty_signature sign1, Tcty_signature sign2 ->
2589         let ty1 = object_fields (repr sign1.cty_self) in
2590         let ty2 = object_fields (repr sign2.cty_self) in
2591         let (fields1, rest1) = flatten_fields ty1
2592         and (fields2, rest2) = flatten_fields ty2 in
2593         let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
2594         List.iter
2595           (fun (lab, k1, t1, k2, t2) ->
2596              begin try eqtype true type_pairs subst env t1 t2 with
2597                Unify trace ->
2598                  raise (Failure [CM_Meth_type_mismatch
2599                                     (lab, expand_trace env trace)])
2600              end)
2601           pairs;
2602         Vars.iter
2603           (fun lab (_, _, ty) ->
2604              let (_, _, ty') = Vars.find lab sign1.cty_vars in
2605              try eqtype true type_pairs subst env ty ty' with Unify trace ->
2606                raise (Failure [CM_Val_type_mismatch
2607                                   (lab, expand_trace env trace)]))
2608           sign2.cty_vars
2609     | _ ->
2610         raise
2611           (Failure (if trace then []
2612                     else [CM_Class_type_mismatch (cty1, cty2)]))
2613   with
2614     Failure error when trace ->
2615       raise (Failure (CM_Class_type_mismatch (cty1, cty2)::error))
2616
2617 (* XXX On pourrait autoriser l'instantiation du type des parametres... *)
2618 (* XXX Correct ? (variables de type dans parametres et corps de classe *)
2619 let match_class_declarations env patt_params patt_type subj_params subj_type =
2620   let type_pairs = TypePairs.create 53 in
2621   let subst = ref [] in
2622   let sign1 = signature_of_class_type patt_type in
2623   let sign2 = signature_of_class_type subj_type in
2624   let t1 = repr sign1.cty_self in
2625   let t2 = repr sign2.cty_self in
2626   TypePairs.add type_pairs (t1, t2) ();
2627   let (fields1, rest1) = flatten_fields (object_fields t1)
2628   and (fields2, rest2) = flatten_fields (object_fields t2) in
2629   let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
2630   let error =
2631     List.fold_right
2632       (fun (lab, k, _) err ->
2633         let err =
2634           let k = field_kind_repr k in
2635           begin match k with
2636             Fvar r -> err
2637           | _      -> CM_Hide_public lab::err
2638           end
2639         in
2640         if Concr.mem lab sign1.cty_concr then err
2641         else CM_Hide_virtual ("method", lab) :: err)
2642       miss1 []
2643   in
2644   let missing_method = List.map (fun (m, _, _) -> m) miss2 in
2645   let error =
2646     (List.map (fun m -> CM_Missing_method m) missing_method) @ error
2647   in
2648   (* Always succeeds *)
2649   eqtype true type_pairs subst env rest1 rest2;
2650   let error =
2651     List.fold_right
2652       (fun (lab, k1, t1, k2, t2) err ->
2653         let k1 = field_kind_repr k1 in
2654         let k2 = field_kind_repr k2 in
2655         match k1, k2 with
2656           (Fvar _, Fvar _)
2657         | (Fpresent, Fpresent) -> err
2658         | (Fvar _, Fpresent)   -> CM_Private_method lab::err
2659         | (Fpresent, Fvar _)  -> CM_Public_method lab::err
2660         | _                    -> assert false)
2661       pairs error
2662   in
2663   let error =
2664     Vars.fold
2665       (fun lab (mut, vr, ty) err ->
2666          try
2667            let (mut', vr', ty') = Vars.find lab sign1.cty_vars in
2668            if mut = Mutable && mut' <> Mutable then
2669              CM_Non_mutable_value lab::err
2670            else if vr = Concrete && vr' <> Concrete then
2671              CM_Non_concrete_value lab::err
2672            else
2673              err
2674          with Not_found ->
2675            CM_Missing_value lab::err)
2676       sign2.cty_vars error
2677   in
2678   let error =
2679     Vars.fold
2680       (fun lab (_,vr,_) err ->
2681         if vr = Virtual && not (Vars.mem lab sign2.cty_vars) then
2682           CM_Hide_virtual ("instance variable", lab) :: err
2683         else err)
2684       sign1.cty_vars error
2685   in
2686   let error =
2687     List.fold_right
2688       (fun e l ->
2689         if List.mem e missing_method then l else CM_Virtual_method e::l)
2690       (Concr.elements (Concr.diff sign2.cty_concr sign1.cty_concr))
2691       error
2692   in
2693   match error with
2694     [] ->
2695       begin try
2696         let lp = List.length patt_params in
2697         let ls = List.length subj_params in
2698         if lp  <> ls then
2699           raise (Failure [CM_Parameter_arity_mismatch (lp, ls)]);
2700         List.iter2 (fun p s ->
2701           try eqtype true type_pairs subst env p s with Unify trace ->
2702             raise (Failure [CM_Type_parameter_mismatch
2703                                (expand_trace env trace)]))
2704           patt_params subj_params;
2705         equal_clty false type_pairs subst env patt_type subj_type;
2706         []
2707       with
2708         Failure r -> r
2709       end
2710   | error ->
2711       error
2712
2713
2714                               (***************)
2715                               (*  Subtyping  *)
2716                               (***************)
2717
2718
2719 (**** Build a subtype of a given type. ****)
2720
2721 (* build_subtype:
2722    [visited] traces traversed object and variant types
2723    [loops] is a mapping from variables to variables, to reproduce
2724      positive loops in a class type
2725    [posi] true if the current variance is positive
2726    [level] number of expansions/enlargement allowed on this branch *)
2727
2728 let warn = ref false  (* whether double coercion might do better *)
2729 let pred_expand n = if n mod 2 = 0 && n > 0 then pred n else n
2730 let pred_enlarge n = if n mod 2 = 1 then pred n else n
2731
2732 type change = Unchanged | Equiv | Changed
2733 let collect l = List.fold_left (fun c1 (_, c2) -> max c1 c2) Unchanged l
2734
2735 let rec filter_visited = function
2736     [] -> []
2737   | {desc=Tobject _|Tvariant _} :: _ as l -> l
2738   | _ :: l -> filter_visited l
2739
2740 let memq_warn t visited =
2741   if List.memq t visited then (warn := true; true) else false
2742
2743 let rec lid_of_path sharp = function
2744     Path.Pident id ->
2745       Longident.Lident (sharp ^ Ident.name id)
2746   | Path.Pdot (p1, s, _) ->
2747       Longident.Ldot (lid_of_path "" p1, sharp ^ s)
2748   | Path.Papply (p1, p2) ->
2749       Longident.Lapply (lid_of_path sharp p1, lid_of_path "" p2)
2750
2751 let find_cltype_for_path env p =
2752   let path, cl_abbr = Env.lookup_type (lid_of_path "#" p) env in
2753   match cl_abbr.type_manifest with
2754     Some ty ->
2755       begin match (repr ty).desc with
2756         Tobject(_,{contents=Some(p',_)}) when Path.same p p' -> cl_abbr, ty
2757       | _ -> raise Not_found
2758       end
2759   | None -> assert false
2760
2761 let has_constr_row' env t =
2762   has_constr_row (expand_abbrev env t)
2763
2764 let rec build_subtype env visited loops posi level t =
2765   let t = repr t in
2766   match t.desc with
2767     Tvar ->
2768       if posi then
2769         try
2770           let t' = List.assq t loops in
2771           warn := true;
2772           (t', Equiv)
2773         with Not_found ->
2774           (t, Unchanged)
2775       else
2776         (t, Unchanged)
2777   | Tarrow(l, t1, t2, _) ->
2778       if memq_warn t visited then (t, Unchanged) else
2779       let visited = t :: visited in
2780       let (t1', c1) = build_subtype env visited loops (not posi) level t1 in
2781       let (t2', c2) = build_subtype env visited loops posi level t2 in
2782       let c = max c1 c2 in
2783       if c > Unchanged then (newty (Tarrow(l, t1', t2', Cok)), c)
2784       else (t, Unchanged)
2785   | Ttuple tlist ->
2786       if memq_warn t visited then (t, Unchanged) else
2787       let visited = t :: visited in
2788       let tlist' =
2789         List.map (build_subtype env visited loops posi level) tlist
2790       in
2791       let c = collect tlist' in
2792       if c > Unchanged then (newty (Ttuple (List.map fst tlist')), c)
2793       else (t, Unchanged)
2794   | Tconstr(p, tl, abbrev)
2795     when level > 0 && generic_abbrev env p && safe_abbrev env t
2796     && not (has_constr_row' env t) ->
2797       let t' = repr (expand_abbrev env t) in
2798       let level' = pred_expand level in
2799       begin try match t'.desc with
2800         Tobject _ when posi && not (opened_object t') ->
2801           let cl_abbr, body = find_cltype_for_path env p in
2802           let ty =
2803             subst env !current_level Public abbrev None
2804               cl_abbr.type_params tl body in
2805           let ty = repr ty in
2806           let ty1, tl1 =
2807             match ty.desc with
2808               Tobject(ty1,{contents=Some(p',tl1)}) when Path.same p p' ->
2809                 ty1, tl1
2810             | _ -> raise Not_found
2811           in
2812           (* Fix PR4505: do not set ty to Tvar when it appears in tl1,
2813              as this occurence might break the occur check.
2814              XXX not clear whether this correct anyway... *)
2815           if List.exists (deep_occur ty) tl1 then raise Not_found;
2816           ty.desc <- Tvar;
2817           let t'' = newvar () in
2818           let loops = (ty, t'') :: loops in
2819           (* May discard [visited] as level is going down *)
2820           let (ty1', c) =
2821             build_subtype env [t'] loops posi (pred_enlarge level') ty1 in
2822           assert (t''.desc = Tvar);
2823           let nm =
2824             if c > Equiv || deep_occur ty ty1' then None else Some(p,tl1) in
2825           t''.desc <- Tobject (ty1', ref nm);
2826           (try unify_var env ty t with Unify _ -> assert false);
2827           (t'', Changed)
2828       | _ -> raise Not_found
2829       with Not_found ->
2830         let (t'',c) = build_subtype env visited loops posi level' t' in
2831         if c > Unchanged then (t'',c)
2832         else (t, Unchanged)
2833       end
2834   | Tconstr(p, tl, abbrev) ->
2835       (* Must check recursion on constructors, since we do not always
2836          expand them *)
2837       if memq_warn t visited then (t, Unchanged) else
2838       let visited = t :: visited in
2839       begin try
2840         let decl = Env.find_type p env in
2841         if level = 0 && generic_abbrev env p && safe_abbrev env t
2842         && not (has_constr_row' env t)
2843         then warn := true;
2844         let tl' =
2845           List.map2
2846             (fun (co,cn,_) t ->
2847               if cn then
2848                 if co then (t, Unchanged)
2849                 else build_subtype env visited loops (not posi) level t
2850               else
2851                 if co then build_subtype env visited loops posi level t
2852                 else (newvar(), Changed))
2853             decl.type_variance tl
2854         in
2855         let c = collect tl' in
2856         if c > Unchanged then (newconstr p (List.map fst tl'), c)
2857         else (t, Unchanged)
2858       with Not_found ->
2859         (t, Unchanged)
2860       end
2861   | Tvariant row ->
2862       let row = row_repr row in
2863       if memq_warn t visited || not (static_row row) then (t, Unchanged) else
2864       let level' = pred_enlarge level in
2865       let visited =
2866         t :: if level' < level then [] else filter_visited visited in
2867       let fields = filter_row_fields false row.row_fields in
2868       let fields =
2869         List.map
2870           (fun (l,f as orig) -> match row_field_repr f with
2871             Rpresent None ->
2872               if posi then
2873                 (l, Reither(true, [], false, ref None)), Unchanged
2874               else
2875                 orig, Unchanged
2876           | Rpresent(Some t) ->
2877               let (t', c) = build_subtype env visited loops posi level' t in
2878               let f =
2879                 if posi && level > 0
2880                 then Reither(false, [t'], false, ref None)
2881                 else Rpresent(Some t')
2882               in (l, f), c
2883           | _ -> assert false)
2884           fields
2885       in
2886       let c = collect fields in
2887       let row =
2888         { row_fields = List.map fst fields; row_more = newvar();
2889           row_bound = (); row_closed = posi; row_fixed = false;
2890           row_name = if c > Unchanged then None else row.row_name }
2891       in
2892       (newty (Tvariant row), Changed)
2893   | Tobject (t1, _) ->
2894       if memq_warn t visited || opened_object t1 then (t, Unchanged) else
2895       let level' = pred_enlarge level in
2896       let visited =
2897         t :: if level' < level then [] else filter_visited visited in
2898       let (t1', c) = build_subtype env visited loops posi level' t1 in
2899       if c > Unchanged then (newty (Tobject (t1', ref None)), c)
2900       else (t, Unchanged)
2901   | Tfield(s, _, t1, t2) (* Always present *) ->
2902       let (t1', c1) = build_subtype env visited loops posi level t1 in
2903       let (t2', c2) = build_subtype env visited loops posi level t2 in
2904       let c = max c1 c2 in
2905       if c > Unchanged then (newty (Tfield(s, Fpresent, t1', t2')), c)
2906       else (t, Unchanged)
2907   | Tnil ->
2908       if posi then
2909         let v = newvar () in
2910         (v, Changed)
2911       else begin
2912         warn := true;
2913         (t, Unchanged)
2914       end
2915   | Tsubst _ | Tlink _ ->
2916       assert false
2917   | Tpoly(t1, tl) ->
2918       let (t1', c) = build_subtype env visited loops posi level t1 in
2919       if c > Unchanged then (newty (Tpoly(t1', tl)), c)
2920       else (t, Unchanged)
2921   | Tunivar ->
2922       (t, Unchanged)
2923
2924 let enlarge_type env ty =
2925   warn := false;
2926   (* [level = 4] allows 2 expansions involving objects/variants *)
2927   let (ty', _) = build_subtype env [] [] true 4 ty in
2928   (ty', !warn)
2929
2930 (**** Check whether a type is a subtype of another type. ****)
2931
2932 (*
2933     During the traversal, a trace of visited types is maintained. It
2934     is printed in case of error.
2935     Constraints (pairs of types that must be equals) are accumulated
2936     rather than being enforced straight. Indeed, the result would
2937     otherwise depend on the order in which these constraints are
2938     enforced.
2939     A function enforcing these constraints is returned. That way, type
2940     variables can be bound to their actual values before this function
2941     is called (see Typecore).
2942     Only well-defined abbreviations are expanded (hence the tests
2943     [generic_abbrev ...]).
2944 *)
2945
2946 let subtypes = TypePairs.create 17
2947
2948 let subtype_error env trace =
2949   raise (Subtype (expand_trace env (List.rev trace), []))
2950
2951 let private_abbrev env path =
2952   try
2953     let decl = Env.find_type path env in
2954     decl.type_private = Private && decl.type_manifest <> None
2955   with Not_found -> false
2956
2957 let rec subtype_rec env trace t1 t2 cstrs =
2958   let t1 = repr t1 in
2959   let t2 = repr t2 in
2960   if t1 == t2 then cstrs else
2961
2962   begin try
2963     TypePairs.find subtypes (t1, t2);
2964     cstrs
2965   with Not_found ->
2966     TypePairs.add subtypes (t1, t2) ();
2967     match (t1.desc, t2.desc) with
2968       (Tvar, _) | (_, Tvar) ->
2969         (trace, t1, t2, !univar_pairs)::cstrs
2970     | (Tarrow(l1, t1, u1, _), Tarrow(l2, t2, u2, _)) when l1 = l2
2971       || !Clflags.classic && not (is_optional l1 || is_optional l2) ->
2972         let cstrs = subtype_rec env ((t2, t1)::trace) t2 t1 cstrs in
2973         subtype_rec env ((u1, u2)::trace) u1 u2 cstrs
2974     | (Ttuple tl1, Ttuple tl2) ->
2975         subtype_list env trace tl1 tl2 cstrs
2976     | (Tconstr(p1, [], _), Tconstr(p2, [], _)) when Path.same p1 p2 ->
2977         cstrs
2978     | (Tconstr(p1, tl1, abbrev1), _)
2979       when generic_abbrev env p1 && safe_abbrev env t1 ->
2980         subtype_rec env trace (expand_abbrev env t1) t2 cstrs
2981     | (_, Tconstr(p2, tl2, abbrev2))
2982       when generic_abbrev env p2 && safe_abbrev env t2 ->
2983         subtype_rec env trace t1 (expand_abbrev env t2) cstrs
2984     | (Tconstr(p1, tl1, _), Tconstr(p2, tl2, _)) when Path.same p1 p2 ->
2985         begin try
2986           let decl = Env.find_type p1 env in
2987           List.fold_left2
2988             (fun cstrs (co, cn, _) (t1, t2) ->
2989               if co then
2990                 if cn then
2991                   (trace, newty2 t1.level (Ttuple[t1]),
2992                    newty2 t2.level (Ttuple[t2]), !univar_pairs) :: cstrs
2993                 else subtype_rec env ((t1, t2)::trace) t1 t2 cstrs
2994               else
2995                 if cn then subtype_rec env ((t2, t1)::trace) t2 t1 cstrs
2996                 else cstrs)
2997             cstrs decl.type_variance (List.combine tl1 tl2)
2998         with Not_found ->
2999           (trace, t1, t2, !univar_pairs)::cstrs
3000         end
3001     | (Tconstr(p1, tl1, _), _) when private_abbrev env p1 ->
3002         subtype_rec env trace (expand_abbrev_opt env t1) t2 cstrs
3003     | (Tobject (f1, _), Tobject (f2, _))
3004       when (object_row f1).desc = Tvar && (object_row f2).desc = Tvar ->
3005         (* Same row variable implies same object. *)
3006         (trace, t1, t2, !univar_pairs)::cstrs
3007     | (Tobject (f1, _), Tobject (f2, _)) ->
3008         subtype_fields env trace f1 f2 cstrs
3009     | (Tvariant row1, Tvariant row2) ->
3010         begin try
3011           subtype_row env trace row1 row2 cstrs
3012         with Exit ->
3013           (trace, t1, t2, !univar_pairs)::cstrs
3014         end
3015     | (Tpoly (u1, []), Tpoly (u2, [])) ->
3016         subtype_rec env trace u1 u2 cstrs
3017     | (Tpoly (u1, tl1), Tpoly (u2, [])) ->
3018         let _, u1' = instance_poly false tl1 u1 in
3019         subtype_rec env trace u1' u2 cstrs
3020     | (Tpoly (u1, tl1), Tpoly (u2,tl2)) ->
3021         begin try
3022           enter_poly env univar_pairs u1 tl1 u2 tl2
3023             (fun t1 t2 -> subtype_rec env trace t1 t2 cstrs)
3024         with Unify _ ->
3025           (trace, t1, t2, !univar_pairs)::cstrs
3026         end
3027     | (_, _) ->
3028         (trace, t1, t2, !univar_pairs)::cstrs
3029   end
3030
3031 and subtype_list env trace tl1 tl2 cstrs =
3032   if List.length tl1 <> List.length tl2 then
3033     subtype_error env trace;
3034   List.fold_left2
3035     (fun cstrs t1 t2 -> subtype_rec env ((t1, t2)::trace) t1 t2 cstrs)
3036     cstrs tl1 tl2
3037
3038 and subtype_fields env trace ty1 ty2 cstrs =
3039   (* Assume that either rest1 or rest2 is not Tvar *)
3040   let (fields1, rest1) = flatten_fields ty1 in
3041   let (fields2, rest2) = flatten_fields ty2 in
3042   let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
3043   let cstrs =
3044     if rest2.desc = Tnil then cstrs else
3045     if miss1 = [] then
3046       subtype_rec env ((rest1, rest2)::trace) rest1 rest2 cstrs
3047     else
3048       (trace, build_fields (repr ty1).level miss1 rest1, rest2,
3049        !univar_pairs) :: cstrs
3050   in
3051   let cstrs =
3052     if miss2 = [] then cstrs else
3053     (trace, rest1, build_fields (repr ty2).level miss2 (newvar ()),
3054      !univar_pairs) :: cstrs
3055   in
3056   List.fold_left
3057     (fun cstrs (_, k1, t1, k2, t2) ->
3058       (* Theses fields are always present *)
3059       subtype_rec env ((t1, t2)::trace) t1 t2 cstrs)
3060     cstrs pairs
3061
3062 and subtype_row env trace row1 row2 cstrs =
3063   let row1 = row_repr row1 and row2 = row_repr row2 in
3064   let r1, r2, pairs =
3065     merge_row_fields row1.row_fields row2.row_fields in
3066   let more1 = repr row1.row_more
3067   and more2 = repr row2.row_more in
3068   match more1.desc, more2.desc with
3069     Tconstr(p1,_,_), Tconstr(p2,_,_) when Path.same p1 p2 ->
3070       subtype_rec env ((more1,more2)::trace) more1 more2 cstrs
3071   | (Tvar|Tconstr _), (Tvar|Tconstr _)
3072     when row1.row_closed && r1 = [] ->
3073       List.fold_left
3074         (fun cstrs (_,f1,f2) ->
3075           match row_field_repr f1, row_field_repr f2 with
3076             (Rpresent None|Reither(true,_,_,_)), Rpresent None ->
3077               cstrs
3078           | Rpresent(Some t1), Rpresent(Some t2) ->
3079               subtype_rec env ((t1, t2)::trace) t1 t2 cstrs
3080           | Reither(false, t1::_, _, _), Rpresent(Some t2) ->
3081               subtype_rec env ((t1, t2)::trace) t1 t2 cstrs
3082           | Rabsent, _ -> cstrs
3083           | _ -> raise Exit)
3084         cstrs pairs
3085   | Tunivar, Tunivar
3086     when row1.row_closed = row2.row_closed && r1 = [] && r2 = [] ->
3087       let cstrs =
3088         subtype_rec env ((more1,more2)::trace) more1 more2 cstrs in
3089       List.fold_left
3090         (fun cstrs (_,f1,f2) ->
3091           match row_field_repr f1, row_field_repr f2 with
3092             Rpresent None, Rpresent None
3093           | Reither(true,[],_,_), Reither(true,[],_,_)
3094           | Rabsent, Rabsent ->
3095               cstrs
3096           | Rpresent(Some t1), Rpresent(Some t2)
3097           | Reither(false,[t1],_,_), Reither(false,[t2],_,_) ->
3098               subtype_rec env ((t1, t2)::trace) t1 t2 cstrs
3099           | _ -> raise Exit)
3100         cstrs pairs
3101   | _ ->
3102       raise Exit
3103
3104 let subtype env ty1 ty2 =
3105   TypePairs.clear subtypes;
3106   univar_pairs := [];
3107   (* Build constraint set. *)
3108   let cstrs = subtype_rec env [(ty1, ty2)] ty1 ty2 [] in
3109   TypePairs.clear subtypes;
3110   (* Enforce constraints. *)
3111   function () ->
3112     List.iter
3113       (function (trace0, t1, t2, pairs) ->
3114          try unify_pairs env t1 t2 pairs with Unify trace ->
3115            raise (Subtype (expand_trace env (List.rev trace0),
3116                            List.tl (List.tl trace))))
3117       (List.rev cstrs)
3118
3119                               (*******************)
3120                               (*  Miscellaneous  *)
3121                               (*******************)
3122
3123 (* Utility for printing. The resulting type is not used in computation. *)
3124 let rec unalias_object ty =
3125   let ty = repr ty in
3126   match ty.desc with
3127     Tfield (s, k, t1, t2) ->
3128       newty2 ty.level (Tfield (s, k, t1, unalias_object t2))
3129   | Tvar | Tnil ->
3130       newty2 ty.level ty.desc
3131   | Tunivar ->
3132       ty
3133   | Tconstr _ ->
3134       newty2 ty.level Tvar
3135   | _ ->
3136       assert false
3137
3138 let unalias ty =
3139   let ty = repr ty in
3140   match ty.desc with
3141     Tvar | Tunivar ->
3142       ty
3143   | Tvariant row ->
3144       let row = row_repr row in
3145       let more = row.row_more in
3146       newty2 ty.level
3147         (Tvariant {row with row_more = newty2 more.level more.desc})
3148   | Tobject (ty, nm) ->
3149       newty2 ty.level (Tobject (unalias_object ty, nm))
3150   | _ ->
3151       newty2 ty.level ty.desc
3152
3153 let unroll_abbrev id tl ty =
3154   let ty = repr ty in
3155   if (ty.desc = Tvar) || (List.exists (deep_occur ty) tl) then
3156     ty
3157   else
3158     let ty' = newty2 ty.level ty.desc in
3159     link_type ty (newty2 ty.level (Tconstr (Path.Pident id, tl, ref Mnil)));
3160     ty'
3161
3162 (* Return the arity (as for curried functions) of the given type. *)
3163 let rec arity ty =
3164   match (repr ty).desc with
3165     Tarrow(_, t1, t2, _) -> 1 + arity t2
3166   | _ -> 0
3167
3168 (* Check whether an abbreviation expands to itself. *)
3169 let cyclic_abbrev env id ty =
3170   let rec check_cycle seen ty =
3171     let ty = repr ty in
3172     match ty.desc with
3173       Tconstr (p, tl, abbrev) ->
3174         p = Path.Pident id || List.memq ty seen ||
3175         begin try
3176           check_cycle (ty :: seen) (expand_abbrev env ty)
3177         with
3178           Cannot_expand -> false
3179         | Unify _ -> true
3180         end
3181     | _ ->
3182         false
3183   in check_cycle [] ty
3184
3185 (* Normalize a type before printing, saving... *)
3186 (* Cannot use mark_type because deep_occur uses it too *)
3187 let rec normalize_type_rec env visited ty =
3188   let ty = repr ty in
3189   if not (TypeSet.mem ty !visited) then begin
3190     visited := TypeSet.add ty !visited;
3191     begin match ty.desc with
3192     | Tvariant row ->
3193       let row = row_repr row in
3194       let fields = List.map
3195           (fun (l,f0) ->
3196             let f = row_field_repr f0 in l,
3197             match f with Reither(b, ty::(_::_ as tyl), m, e) ->
3198               let tyl' =
3199                 List.fold_left
3200                   (fun tyl ty ->
3201                     if List.exists (fun ty' -> equal env false [ty] [ty']) tyl
3202                     then tyl else ty::tyl)
3203                   [ty] tyl
3204               in
3205               if f != f0 || List.length tyl' < List.length tyl then
3206                 Reither(b, List.rev tyl', m, e)
3207               else f
3208             | _ -> f)
3209           row.row_fields in
3210       let fields =
3211         List.sort (fun (p,_) (q,_) -> compare p q)
3212           (List.filter (fun (_,fi) -> fi <> Rabsent) fields) in
3213       log_type ty;
3214       ty.desc <- Tvariant {row with row_fields = fields}
3215     | Tobject (fi, nm) ->
3216         begin match !nm with
3217         | None -> ()
3218         | Some (n, v :: l) ->
3219             if deep_occur ty (newgenty (Ttuple l)) then
3220               (* The abbreviation may be hiding something, so remove it *)
3221               set_name nm None
3222             else let v' = repr v in
3223             begin match v'.desc with
3224             | Tvar|Tunivar ->
3225                 if v' != v then set_name nm (Some (n, v' :: l))
3226             | Tnil ->
3227                 log_type ty; ty.desc <- Tconstr (n, l, ref Mnil)
3228             | _ -> set_name nm None
3229             end
3230         | _ ->
3231             fatal_error "Ctype.normalize_type_rec"
3232         end;
3233         let fi = repr fi in
3234         if fi.level < lowest_level then () else
3235         let fields, row = flatten_fields fi in
3236         let fi' = build_fields fi.level fields row in
3237         log_type ty; fi.desc <- fi'.desc
3238     | _ -> ()
3239     end;
3240     iter_type_expr (normalize_type_rec env visited) ty
3241   end
3242
3243 let normalize_type env ty =
3244   normalize_type_rec env (ref TypeSet.empty) ty
3245
3246
3247                               (*************************)
3248                               (*  Remove dependencies  *)
3249                               (*************************)
3250
3251
3252 (*
3253    Variables are left unchanged. Other type nodes are duplicated, with
3254    levels set to generic level.
3255    During copying, the description of a (non-variable) node is first
3256    replaced by a link to a stub ([Tsubst (newgenvar ())]).
3257    Once the copy is made, it replaces the stub.
3258    After copying, the description of node, which was stored by
3259    [save_desc], must be put back, using [cleanup_types].
3260 *)
3261
3262 let rec nondep_type_rec env id ty =
3263   let ty = repr ty in
3264   match ty.desc with
3265     Tvar | Tunivar -> ty
3266   | Tsubst ty -> ty
3267   | _ ->
3268     let desc = ty.desc in
3269     save_desc ty desc;
3270     let ty' = newgenvar () in        (* Stub *)
3271     ty.desc <- Tsubst ty';
3272     ty'.desc <-
3273       begin match desc with
3274       | Tconstr(p, tl, abbrev) ->
3275           if Path.isfree id p then
3276             begin try
3277               Tlink (nondep_type_rec env id
3278                        (expand_abbrev env (newty2 ty.level desc)))
3279               (*
3280                  The [Tlink] is important. The expanded type may be a
3281                  variable, or may not be completely copied yet
3282                  (recursive type), so one cannot just take its
3283                  description.
3284                *)
3285             with Cannot_expand | Unify _ -> (* expand_abbrev failed *)
3286               raise Not_found               (* cf. PR4775 for Unify *)
3287             end
3288           else
3289             Tconstr(p, List.map (nondep_type_rec env id) tl, ref Mnil)
3290       | Tobject (t1, name) ->
3291           Tobject (nondep_type_rec env id t1,
3292                  ref (match !name with
3293                         None -> None
3294                       | Some (p, tl) ->
3295                           if Path.isfree id p then None
3296                           else Some (p, List.map (nondep_type_rec env id) tl)))
3297       | Tvariant row ->
3298           let row = row_repr row in
3299           let more = repr row.row_more in
3300           (* We must substitute in a subtle way *)
3301           (* Tsubst denotes the variant itself, as the row var is unchanged *)
3302           begin match more.desc with
3303             Tsubst ty2 ->
3304               (* This variant type has been already copied *)
3305               ty.desc <- Tsubst ty2; (* avoid Tlink in the new type *)
3306               Tlink ty2
3307           | _ ->
3308               let static = static_row row in
3309               (* Register new type first for recursion *)
3310               save_desc more more.desc;
3311               more.desc <- ty.desc;
3312               let more' = if static then newgenvar () else more in
3313               (* Return a new copy *)
3314               let row =
3315                 copy_row (nondep_type_rec env id) true row true more' in
3316               match row.row_name with
3317                 Some (p, tl) when Path.isfree id p ->
3318                   Tvariant {row with row_name = None}
3319               | _ -> Tvariant row
3320           end
3321       | _ -> copy_type_desc (nondep_type_rec env id) desc
3322       end;
3323     ty'
3324
3325 let nondep_type env id ty =
3326   try
3327     let ty' = nondep_type_rec env id ty in
3328     cleanup_types ();
3329     unmark_type ty';
3330     ty'
3331   with Not_found ->
3332     cleanup_types ();
3333     raise Not_found
3334
3335 (* Preserve sharing inside type declarations. *)
3336 let nondep_type_decl env mid id is_covariant decl =
3337   try
3338     let params = List.map (nondep_type_rec env mid) decl.type_params in
3339     let tk =
3340       try match decl.type_kind with
3341         Type_abstract ->
3342           Type_abstract
3343       | Type_variant cstrs ->
3344           Type_variant
3345             (List.map
3346                (fun (c, tl) -> (c, List.map (nondep_type_rec env mid) tl))
3347                cstrs)
3348       | Type_record(lbls, rep) ->
3349           Type_record
3350             (List.map
3351                (fun (c, mut, t) -> (c, mut, nondep_type_rec env mid t))
3352                lbls,
3353              rep)
3354       with Not_found when is_covariant -> Type_abstract
3355     and tm =
3356       try match decl.type_manifest with
3357         None -> None
3358       | Some ty ->
3359           Some (unroll_abbrev id params (nondep_type_rec env mid ty))
3360       with Not_found when is_covariant ->
3361         None
3362     in
3363     cleanup_types ();
3364     List.iter unmark_type decl.type_params;
3365     begin match decl.type_kind with
3366       Type_abstract -> ()
3367     | Type_variant cstrs ->
3368         List.iter (fun (c, tl) -> List.iter unmark_type tl) cstrs
3369     | Type_record(lbls, rep) ->
3370         List.iter (fun (c, mut, t) -> unmark_type t) lbls
3371     end;
3372     begin match decl.type_manifest with
3373       None    -> ()
3374     | Some ty -> unmark_type ty
3375     end;
3376     let priv =
3377       match tm with
3378       | Some ty when Btype.has_constr_row ty -> Private
3379       | _ -> decl.type_private
3380     in
3381     { type_params = params;
3382       type_arity = decl.type_arity;
3383       type_kind = tk;
3384       type_manifest = tm;
3385       type_private = priv;
3386       type_variance = decl.type_variance;
3387     }
3388   with Not_found ->
3389     cleanup_types ();
3390     raise Not_found
3391
3392 (* Preserve sharing inside class types. *)
3393 let nondep_class_signature env id sign =
3394   { cty_self = nondep_type_rec env id sign.cty_self;
3395     cty_vars =
3396       Vars.map (function (m, v, t) -> (m, v, nondep_type_rec env id t))
3397         sign.cty_vars;
3398     cty_concr = sign.cty_concr;
3399     cty_inher =
3400       List.map (fun (p,tl) -> (p, List.map (nondep_type_rec env id) tl))
3401         sign.cty_inher }
3402
3403 let rec nondep_class_type env id =
3404   function
3405     Tcty_constr (p, _, cty) when Path.isfree id p ->
3406       nondep_class_type env id cty
3407   | Tcty_constr (p, tyl, cty) ->
3408       Tcty_constr (p, List.map (nondep_type_rec env id) tyl,
3409                    nondep_class_type env id cty)
3410   | Tcty_signature sign ->
3411       Tcty_signature (nondep_class_signature env id sign)
3412   | Tcty_fun (l, ty, cty) ->
3413       Tcty_fun (l, nondep_type_rec env id ty, nondep_class_type env id cty)
3414
3415 let nondep_class_declaration env id decl =
3416   assert (not (Path.isfree id decl.cty_path));
3417   let decl =
3418     { cty_params = List.map (nondep_type_rec env id) decl.cty_params;
3419       cty_variance = decl.cty_variance;
3420       cty_type = nondep_class_type env id decl.cty_type;
3421       cty_path = decl.cty_path;
3422       cty_new =
3423         begin match decl.cty_new with
3424           None    -> None
3425         | Some ty -> Some (nondep_type_rec env id ty)
3426         end }
3427   in
3428   cleanup_types ();
3429   List.iter unmark_type decl.cty_params;
3430   unmark_class_type decl.cty_type;
3431   begin match decl.cty_new with
3432     None    -> ()
3433   | Some ty -> unmark_type ty
3434   end;
3435   decl
3436
3437 let nondep_cltype_declaration env id decl =
3438   assert (not (Path.isfree id decl.clty_path));
3439   let decl =
3440     { clty_params = List.map (nondep_type_rec env id) decl.clty_params;
3441       clty_variance = decl.clty_variance;
3442       clty_type = nondep_class_type env id decl.clty_type;
3443       clty_path = decl.clty_path }
3444   in
3445   cleanup_types ();
3446   List.iter unmark_type decl.clty_params;
3447   unmark_class_type decl.clty_type;
3448   decl
3449
3450 (* collapse conjonctive types in class parameters *)
3451 let rec collapse_conj env visited ty =
3452   let ty = repr ty in
3453   if List.memq ty visited then () else
3454   let visited = ty :: visited in
3455   match ty.desc with
3456     Tvariant row ->
3457       let row = row_repr row in
3458       List.iter
3459         (fun (l,fi) ->
3460           match row_field_repr fi with
3461             Reither (c, t1::(_::_ as tl), m, e) ->
3462               List.iter (unify env t1) tl;
3463               set_row_field e (Reither (c, [t1], m, ref None))
3464           | _ ->
3465               ())
3466         row.row_fields;
3467       iter_row (collapse_conj env visited) row
3468   | _ ->
3469       iter_type_expr (collapse_conj env visited) ty
3470
3471 let collapse_conj_params env params =
3472   List.iter (collapse_conj env []) params