ocaml/typing/ctype.ml

(***********************************************************************)
(*                                                                     *)
(*                           Objective Caml                            *)
(*                                                                     *)
(* Xavier Leroy and Jerome Vouillon, projet Cristal, INRIA Rocquencourt*)
(*                                                                     *)
(*  Copyright 1996 Institut National de Recherche en Informatique et   *)
(*  Automatique.  Distributed only by permission.                      *)
(*                                                                     *)
(***********************************************************************)

(* $Id$ *)

(* Operations on core types *)

open Misc
open Asttypes
open Types

(******* Notes

   - As much sharing as possible should be kept : it makes types
     smaller and better abbreviated.
     When necessary, some sharing can be lost. Types will still be
     printed correctly (XXX a faire...), and types defined for a class
     do not depend on sharing thanks to constrained abbreviations (XXX
     a faire...). (Of course, typing will still be correct.)
   - All nodes of a type must have a level : that way, one know
     whether a node must be duplicated or not when instantiating a
     type.
   - Levels of a type must be decreasing.
   - The level of a type constructor must be superior to the binding
     time of its path.

*)

(****** A faire

   - Revoir affichage des types.
   - Abreviations avec contraintes.
   - Types recursifs sans limitation.
   - #-type implementes comme de vraies abreviations.
   - Deplacer Ctype.repr dans Types ?

*)

(**** Errors ****)

exception Unify of (type_expr * type_expr) list

exception Subtype of
        (type_expr * type_expr) list * (type_expr * type_expr) list

exception Cannot_expand

(**** Type level management ****)

let generic_level = (-1)
let current_level = ref 0
let global_level = ref 1

let init_def level = current_level := level
let begin_def () = incr current_level
let end_def () = decr current_level

let reset_global_level () =
  global_level := !current_level + 1

(**** Some type creators ****)

let newgenty desc      = { desc = desc; level = generic_level }
let newgenvar ()     = newgenty Tvar

let newty desc         = { desc = desc; level = !current_level }
let newvar ()          = { desc = Tvar; level = !current_level }
let newobj fields      = newty (Tobject (fields, ref None))

let new_global_ty desc = { desc = desc; level = !global_level }
let new_global_var ()  = new_global_ty Tvar

let none = newty (Ttuple [])                (* Clearly ill-formed type *)

(**** Representative of a type ****)

let rec repr =
  function
    {desc = Tlink t'} as t ->
      let r = repr t' in
      if r != t' then t.desc <- Tlink r;
      r
  | t -> t


                  (**********************************************)
                  (*  Miscellaneous operations on object types  *)
                  (**********************************************)


(**** Object field manipulation. ****)

let flatten_fields ty =
  let rec flatten l ty =
    let ty = repr ty in
    match ty.desc with
      Tfield(s, ty1, ty2) ->
        flatten ((s, ty1)::l) ty2
    | Tvar | Tnil ->
        (l, ty)
    | _ ->
      fatal_error "Ctype.flatten_fields"
  in
    let (l, r) = flatten [] ty in
      (List.rev l, r)

let build_fields =
  List.fold_right
    (fun (s, ty1) ty2 ->
       {desc = Tfield(s, ty1, ty2);
        level = ty2.level})

let associate_fields fields1 fields2 =
  let rec associate p s s' =
    function
      (l, []) ->
        (List.rev p, (List.rev s) @ l, List.rev s')
    | ([], l') ->
        (List.rev p, List.rev s, (List.rev s') @ l')
    | ((n, t)::r, (n', t')::r') when n = n' ->
        associate ((t, t')::p) s s' (r, r')
    | ((n, t)::r, ((n', t')::_ as l')) when n < n' ->
        associate p ((n, t)::s) s' (r, l')
    | (((n, t)::r as l), (n', t')::r') (* when n > n' *) ->
        associate p s ((n', t')::s') (l, r')
  in let sort = Sort.list (fun (n, _) (n', _) -> n < n') in
  associate [] [] [] (sort fields1, sort fields2)

(**** Check whether an object is open ****)

(* XXX Faudra penser a eventuellement expanser l'abreviation *)
let rec opened_object ty =
  match (repr ty).desc with
    Tobject (t, _)  -> opened_object t
  | Tfield(_, _, t) -> opened_object t
  | Tvar            -> true
  | _               -> false

(**** Close an object ****)

let close_object ty =
  let rec close ty =
    let ty = repr ty in
    match ty.desc with
      Tvar              -> ty.desc <- Tlink {desc = Tnil; level = ty.level}
    | Tfield(_, _, ty') -> close ty'
    | Tnil              -> ()
    | _                 -> fatal_error "Ctype.close_object (1)"
  in
  match (repr ty).desc with
    Tobject (ty, _)   -> close ty
  | Tconstr (_, _, _) -> ()             (* Already closed *)
  | _                 -> fatal_error "Ctype.close_object (2)"


(**** Object name manipulation ****)
(* XXX Bientot obsolete *)

let rec row_variable ty =
  let ty = repr ty in
  match ty.desc with
    Tfield (_, _, ty) -> row_variable ty
  | Tvar              -> ty
  | Tnil              -> raise Not_found
  | _                 -> fatal_error "Ctype.row_variable"

let set_object_name ty params id =
  match (repr ty).desc with
    Tobject (fi, nm) ->
      begin try
        nm := Some (Path.Pident id, (row_variable fi)::params)
      with Not_found ->
        ()
      end
  | Tconstr (_, _, _) ->
      ()
  | _ ->
      fatal_error "Ctype.set_object_name"

let remove_object_name ty =
  match (repr ty).desc with
    Tobject (_, nm)   -> nm := None
  | Tconstr (_, _, _) -> ()
  | _                 -> fatal_error "Ctype.remove_object_name"


                         (*****************************)
                         (*  Type level manipulation  *)
                         (*****************************)

(* XXX Keep only [generalize_keep_expans] ? *)
let rec generalize ty =
  let ty = repr ty in
  if ty.level > !current_level then begin
    ty.level <- generic_level;
    begin match ty.desc with
      Tconstr (_, _, abbrev) ->
        (* The expansions are not correct anymore (wrong level.) *)
        abbrev := Mnil
    | _ -> ()
    end;
    iter_type_expr generalize ty
  end

(* Generalize and keep abbreviations *)
let rec generalize_keep_expans ty =
  let ty = repr ty in
  if ty.level > !current_level then begin
    ty.level <- generic_level;
    begin match ty.desc with
      Tconstr (_, _, abbrev) ->
        generalize_expans !abbrev
    | _ -> ()
    end;
    iter_type_expr generalize_keep_expans ty
  end

and generalize_expans =
  function
    Mnil              ->  ()
  | Mcons(_, ty, rem) ->  generalize_keep_expans ty; generalize_expans rem
  | Mlink rem         ->  generalize_expans !rem

let rec ungeneralize ty =
  let ty = repr ty in
  if ty.level = generic_level then begin
    ty.level <- !current_level;
    begin match ty.desc with
      Tconstr (_, _, abbrev) ->
        ungeneralize_expans !abbrev
    | _ -> ()
    end;
    iter_type_expr ungeneralize ty
  end

and ungeneralize_expans =
  function
    Mnil              ->  ()
  | Mcons(_, ty, rem) ->  ungeneralize ty; ungeneralize_expans rem
  | Mlink rem         ->  ungeneralize_expans !rem

let expand_abbrev' = (* Forward declaration *)
  ref (fun env path args abbrev level -> raise Cannot_expand)

(* Lower the levels of a type. *)
(* Assume [level] is not [generic_level]. *)
let rec update_level env level ty =
  let ty = repr ty in
  if ty.level > level then begin
    ty.level <- level;
    begin match ty.desc with
      Tconstr(p, tl, abbrev)  when level < Path.binding_time p ->
        (* Try first to replace an abbreviation by its expansion. *)
        begin try
          let ty' = !expand_abbrev' env p tl abbrev ty.level in
          ty.desc <- Tlink ty'
          (* [expand_abbrev] already checks the level, so no need to
             recurse further. *)
        with Cannot_expand ->
          raise (Unify [])
        end
    | _ ->
        iter_type_expr (update_level env level) ty
    end;
  end

let make_nongen ty = update_level Env.empty !current_level ty
(* 
   Function [update_level] will never try to expand an abbreviation in
   this case ([current_level] is higher than the binding time of any
   type constructor path). So, it can be called with the empty
   environnement.
*)


                              (*******************)
                              (*  Instantiation  *)
                              (*******************)


(*
   Generic nodes are duplicated, while non-generic nodes are left
   as-is. The instance cannot be generic.
   During instantiation, the description of a generic node is first
   replaced by a link to a stub ([Tlink (newvar ())]). Once the copy
   is made, it replaces the stub.
   After instantiation, the description of generic node, which was
   stored in [saved_desc], must be put back, using [cleanup_types].
   [bind_param t t'] can be used to replace a node [t] by a node [t'].
*)

let saved_desc = ref []
  (* Saved association of generic node with their description. *)
let abbreviations = ref (ref Mnil)
  (* Abbreviation memorized. *)

let rec copy =
  function  (* [repr] cannot be used here. *)
    {desc = Tlink ty'} ->
      copy ty'
  | ty when ty.level <> generic_level ->
      ty
  | ty ->
      let desc = ty.desc in
      saved_desc := (ty, desc)::!saved_desc;
      let t = newvar () in              (* Stub *)
      ty.desc <- Tlink t;
      t.desc <-
        begin match desc with
          Tvar ->
            Tvar
        | Tarrow (t1, t2) ->
            Tarrow (copy t1, copy t2)
        | Ttuple tl ->
            Ttuple (List.map copy tl)
        | Tconstr (p, tl, _) ->
            (*
               One must allocate a new reference, so that abbrevia-
               tions belonging to different branches of a type are
               independent.
               Moreover, a reference containing a [Mcons] must be
               shared, so that the memorized expansion of an abbrevia-
               tion can be released by changing the content of just
               one reference.
            *)
            Tconstr (p, List.map copy tl,
                     ref (match ! !abbreviations with
                            Mcons _ -> Mlink !abbreviations
                          | abbrev  -> abbrev))
        | Tobject (t1, {contents = name}) ->
            let name' =
              match name with
                None ->
                  None
              | Some (p, tl) ->
                  Some (p, List.map copy tl)
            in
            Tobject (copy t1, ref name')
        | Tfield (label, t1, t2) ->
            Tfield (label, copy t1, copy t2)
        | Tnil ->
            Tnil
        | Tlink t ->
            Tlink (copy t)
        end;
      t

let bind_param ty ty' =
  saved_desc := (ty, ty.desc)::!saved_desc;
  ty.desc <- Tlink ty'

let cleanup_types () =
  List.iter (fun (ty, desc) -> ty.desc <- desc) !saved_desc;
  saved_desc := []

(**** Variants of instantiations ****)

let instance sch =
  let ty = copy sch in
  cleanup_types ();
  ty

let instance_constructor cstr =
  let ty_res = copy cstr.cstr_res in
  let ty_args = List.map copy cstr.cstr_args in
  cleanup_types ();
  (ty_args, ty_res)

let instance_label lbl =
  let ty_res = copy lbl.lbl_res in
  let ty_arg = copy lbl.lbl_arg in
  cleanup_types ();
  (ty_arg, ty_res)

let instance_parameterized_type sch_args sch =
  let ty_args = List.map copy sch_args in
  let ty = copy sch in
  cleanup_types ();
  (ty_args, ty)

let instance_parameterized_type_2 sch_args sch_lst sch =
  let ty_args = List.map copy sch_args in
  let ty_lst = List.map copy sch_lst in
  let ty = copy sch in
  cleanup_types ();
  (ty_args, ty_lst, ty)

let instance_class cl =
  let params = List.map copy cl.cty_params in
  let args = List.map copy cl.cty_args in
  let vars =
    Vars.fold
      (fun lab (mut, ty) ->
         Vars.add lab (mut, copy ty))
      cl.cty_vars
      Vars.empty in
  let self = copy cl.cty_self in
  cleanup_types ();
  (params, args, vars, self)

(**** Instantiation with parameter substitution ****)

let rec subst level abbrev params args body =
  if level <> generic_level then begin
    let old_level = !current_level in
    current_level := level;
    List.iter2 bind_param params args;
    abbreviations := abbrev;
    let ty = copy body in
    abbreviations := ref Mnil;
    cleanup_types ();
    current_level := old_level;
    ty
  end else begin
    (* One cannot expand directly to a generic type. *)
    let vars = List.map (fun _ -> newvar ()) args in
    begin_def ();
    let ty = subst !current_level abbrev params vars body in
    end_def ();
    generalize_keep_expans ty;
    List.iter2 (fun v a -> v.desc <- Tlink a) vars args;
    ty
  end

(* Only the shape of the type matters, not whether is is generic or
   not. [generic_level] might be slighty slower, but it ensures
   invariants on types (decreasing levels.) *)
let substitute params args body =
  subst generic_level (ref Mnil) params args body


                              (****************************)
                              (*  Abbreviation expansion  *)
                              (****************************)


(* Search whether the expansion has been memorized. *)
let rec find_expans p1 =
  function
    Mnil ->
      None
  | Mcons (p2, ty, _) when Path.same p1 p2 ->
      Some ty
  | Mcons (_, _, rem) ->
      find_expans p1 rem
  | Mlink {contents = rem} ->
      find_expans p1 rem

let previous_env = ref Env.empty

(* Expand an abbreviation. The expansion is memorized. *)
let expand_abbrev env path args abbrev level =
  (* If the environnement has changed, memorized expansions might not
     be correct anymore, and so we flush the cache (this is safe but
     quite pessimistic.) *)
  if env != !previous_env then begin
    cleanup_abbrev ();
    previous_env := env
  end;
  match find_expans path !abbrev with
    Some ty ->
      if level <> generic_level then
        update_level env level ty;
      ty
  | None ->
      let decl =
        try Env.find_type path env with Not_found -> raise Cannot_expand in
      match decl.type_manifest with
        Some body ->
          let v = newvar () in          (* Stub *)
          memorize_abbrev abbrev path v;
          let ty = subst level abbrev decl.type_params args body in
          v.desc <- Tlink ty;
          ty
      | _ ->
          raise Cannot_expand

let _ = expand_abbrev' := expand_abbrev

(* Recursively expand the root of a type. *)
let rec expand_root env ty =
  let ty = repr ty in
  match ty.desc with
    Tconstr(p, tl, abbrev) ->
      begin try
        expand_root env (expand_abbrev env p tl abbrev ty.level)
      with Cannot_expand ->
        ty
      end
  | _ ->
      ty

(* Recursively expand the root of a type.
   Also expand #-types. *)
(* XXX This is a hack ! *)
let rec full_expand env ty =
  let ty = repr (expand_root env ty) in
  match ty.desc with
    Tobject (fi, {contents = Some (_, v::_)}) when (repr v).desc = Tvar ->
      { desc = Tobject (fi, ref None); level = ty.level }
  | _ ->
      ty

(* Check whether the abbreviation expands to a well-defined type.
   During the typing of a class, abbreviations for correspondings
   types expand to non-generic types. *)
let generic_abbrev env path =
  try
    let decl = Env.find_type path env in
    match decl.type_manifest with
      Some body -> body.level = generic_level
    | None      -> false
  with
    Not_found ->
      false


                              (*****************)
                              (*  Unification  *)
                              (*****************)



(**** Occur check ****)

(* XXX A supprimer *)
let occur env ty0 ty =
  let visited = ref ([] : type_expr list) in
  let rec occur_rec ty =
    let ty = repr ty in
    if ty == ty0 then raise (Unify []);
    match ty.desc with
      Tvar ->
        ()
    | Tarrow(t1, t2) ->
        occur_rec t1; occur_rec t2
    | Ttuple tl ->
        List.iter occur_rec tl
    | Tconstr(p, [], abbrev) ->
        ()
    | Tconstr(p, tl, abbrev) ->
        if not (List.memq ty !visited) then begin
          visited := ty :: !visited;
          try List.iter occur_rec tl with Unify _ ->
          try
            let ty' = expand_abbrev env p tl abbrev ty.level in
            occur_rec ty'
          with Cannot_expand -> ()
        end
    | Tobject (_, _) | Tfield (_, _, _) | Tnil ->
        ()
    | Tlink _ ->
        fatal_error "Ctype.occur"
  in
    occur_rec ty

(**** Transform error trace ****)
(* XXX Move it to some other place ? *)

let expand_trace env trace =
  List.fold_right
    (fun (t1, t2) rem ->
       (repr t1, full_expand env t1)::(repr t2, full_expand env t2)::rem)
    trace []

let rec filter_trace =
  function
    (t1, t1')::(t2, t2')::rem ->
      let rem' = filter_trace rem in
      if (t1 == t1') & (t2 == t2') then
        rem'
      else
        (t1, t1')::(t2, t2')::rem
  | _ ->
      []

(**** Unification ****)

let rec unify_rec env a1 a2 t1 t2 =     (* Variables and abbreviations *)
  if t1 == t2 then () else
  let t1 = repr t1 in
  let t2 = repr t2 in
  if t1 == t2 then () else
  try
    match (t1.desc, t2.desc) with
      (Tvar, _) ->
         update_level env t1.level t2;
         begin match a2 with
           None    ->
             occur env t1 t2; t1.desc <- Tlink t2
         | Some l2 ->
             occur env t1 l2; t1.desc <- Tlink l2
         end
    | (_, Tvar) ->
         update_level env t2.level t1;
         begin match a1 with
           None    ->
             occur env t2 t1; t2.desc <- Tlink t1
         | Some l1 ->
             occur env t2 l1; t2.desc <- Tlink l1
         end
    | (Tconstr (p1, tl1, abbrev1), Tconstr (p2, tl2, abbrev2))
            when Path.same p1 p2 ->
        begin
          try
            unify_core env a1 a2 t1 t2
          with Unify lst ->
          try
            let t3 = expand_abbrev env p1 tl1 abbrev1 t1.level in
            update_level env t2.level t1;
            unify_rec env (Some t1) a2 t3 t2
          with Cannot_expand ->
          try
            let t3 = expand_abbrev env p2 tl2 abbrev2 t2.level in
            update_level env t1.level t2;
            unify_rec env a1 (Some t2) t1 t3
          with Cannot_expand ->
            raise (Unify lst)
        end
    | (Tconstr (p1, tl1, abbrev1), Tconstr (p2, tl2, abbrev2)) ->
        begin
          try
            let t3 = expand_abbrev env p1 tl1 abbrev1 t1.level in
            update_level env t2.level t1;
            unify_rec env (Some t1) a2 t3 t2
          with Cannot_expand ->
          try
            let t3 = expand_abbrev env p2 tl2 abbrev2 t2.level in
            update_level env t1.level t2;
            unify_rec env a1 (Some t2) t1 t3
          with Cannot_expand ->
            raise (Unify [])
        end
    | (Tconstr (p1, tl1, abbrev1), _) ->
        begin try
          let t3 = expand_abbrev env p1 tl1 abbrev1 t1.level in
          update_level env t2.level t1;
          unify_rec env (Some t1) a2 t3 t2
        with Cannot_expand ->
          unify_core env a1 a2 t1 t2
        end
    | (_, Tconstr (p2, tl2, abbrev2)) ->
        begin try
          let t3 = expand_abbrev env p2 tl2 abbrev2 t2.level in
          update_level env t1.level t2;
          unify_rec env a1 (Some t2) t1 t3
        with Cannot_expand ->
          unify_core env a1 a2 t1 t2
        end
    | (_, _) ->
        unify_core env a1 a2 t1 t2
  with
    Unify [] ->
      raise (Unify [(t1, t2)])
  | Unify (_::l) ->
      raise (Unify ((t1, t2)::l))

and unify_core env a1 a2 t1 t2 =        (* Other cases *)
  let d1 = t1.desc and d2 = t2.desc in
  begin match (a1, a2) with
    (None,    Some l2) ->
      update_level env t1.level t2; t1.desc <- Tlink l2
  | (Some l1, None) ->
      update_level env t2.level t1; t2.desc <- Tlink l1
  | (_, _) ->
      update_level env t1.level t2; occur env t1 t2; t1.desc <- Tlink t2
  end;
  try
    match (d1, d2) with
      (Tarrow (t1, u1), Tarrow (t2, u2)) ->
        unify_rec env None None t1 t2; unify_rec env None None u1 u2
    | (Ttuple tl1, Ttuple tl2) ->
        unify_list env tl1 tl2
    | (Tconstr (p1, [], _), Tconstr (p2, [], _)) (*when Path.same p1 p2*) ->
        ()
    | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _)) (*when Path.same p1 p2*) ->
        unify_list env tl1 tl2
    | (Tobject (fi1, nm1), Tobject (fi2, nm2)) ->
        unify_fields env fi1 fi2;
        begin match !nm2 with
          Some (_, va::_) when (repr va).desc = Tvar -> ()
        | _                                          -> nm2 := !nm1
        end
    | (Tfield _, Tfield _) ->
        unify_fields env t1 t2
    | (Tnil, Tnil) ->
        ()
    | (_, _) ->
        raise (Unify [])
  with
    Unify l ->
      t1.desc <- d1;
      t2.desc <- d2;
      raise (Unify ((t1, t2)::l))
  | exn ->
      t1.desc <- d1;
      t2.desc <- d2;
      raise exn

and unify_list env tl1 tl2 =
  if List.length tl1 <> List.length tl2 then
    raise (Unify []);
  List.iter2 (unify_rec env None None) tl1 tl2

and unify_fields env ty1 ty2 =          (* Optimization *)
  let (fields1, rest1) = flatten_fields ty1
  and (fields2, rest2) = flatten_fields ty2 in
  let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
  let va = newvar () in
    begin match rest1.desc with
      Tvar ->
        unify_rec env None None rest1 (build_fields miss2 va)
    | Tnil ->
        if miss2 <> [] then raise (Unify []);
        va.desc <- Tlink {desc = Tnil; level = va.level}
    | _ ->
        fatal_error "Ctype.unify_fields (1)"
    end;
    begin match rest2.desc with
      Tvar ->
        unify_rec env None None (build_fields miss1 va) rest2
    | Tnil ->
        if miss1 <> [] then raise (Unify []);
        va.desc <- Tlink {desc = Tnil; level = va.level}
    | _ ->
        fatal_error "Ctype.unify_fields (2)"
    end;
    List.iter (fun (t1, t2) -> unify_rec env None None t1 t2) pairs

let unify env ty1 ty2 =
  try
    unify_rec env None None ty1 ty2
  with Unify trace ->
    let trace = expand_trace env trace in
    match trace with
      t1::t2::rem ->
        raise (Unify (t1::t2::filter_trace rem))
    | _ ->
        fatal_error "Ctype.unify"

(**** Special cases of unification ****)

(* Unify [t] and ['a -> 'b]. Return ['a] and ['b]. *)
let rec filter_arrow env t =
  let t = repr t in
  match t.desc with
    Tvar ->
      let t1 = newvar () and t2 = newvar () in
      let t' = newty (Tarrow (t1, t2)) in
      update_level env t.level t';
      t.desc <- Tlink t';
      (t1, t2)
  | Tarrow(t1, t2) ->
      (t1, t2)
  | Tconstr(p, tl, abbrev) ->
      begin try
        filter_arrow env (expand_abbrev env p tl abbrev t.level)
      with Cannot_expand ->
        raise (Unify [])
      end
  | _ ->
      raise (Unify [])

(* Used by [filter_method]. *)
let rec filter_method_field env name ty =
  let ty = repr ty in
  match ty.desc with
    Tvar ->
      let ty1 = newvar () and ty2 = newvar () in
      let ty' = newty (Tfield (name, ty1, ty2)) in
      update_level env ty.level ty';
      ty.desc <- Tlink ty';
      ty1
  | Tfield(n, ty1, ty2) ->
      if n = name then
        ty1
      else
        filter_method_field env name ty2
  | _ ->
      raise (Unify [])

(* Unify [ty] and [< name : 'a; .. >]. Return ['a]. *)
let rec filter_method env name ty =
  let ty = repr ty in
  match ty.desc with
    Tvar ->
      let ty1 = newvar () in
      let ty' = newobj ty1 in
      update_level env ty.level ty';
      ty.desc <- Tlink ty';
      filter_method_field env name ty1
  | Tobject(f, _) ->
      filter_method_field env name f
  | Tconstr(p, tl, abbrev) ->
      begin try
        filter_method env name (expand_abbrev env p tl abbrev ty.level)
      with Cannot_expand ->
        raise (Unify [])
      end
  | _ ->
      raise (Unify [])


                        (***********************************)
                        (*  Matching between type schemes  *)
                        (***********************************)

(* XXX A voir... *)


(* XXX This is not really an occur check !!! *)
let moregen_occur env ty0 ty =
  let visited = ref [] in
  let rec occur_rec ty =
    let ty = repr ty in
    if not (List.memq ty !visited) then begin
      visited := ty::!visited;
      begin match ty.desc with
        Tvar when ty.level = generic_level & ty0.level < !current_level ->
          (* ty0 has level = !current_level iff it is generic
             in the original type scheme. In this case, it can be freely
             instantiated. Otherwise, ty0 is not generic
             and cannot be instantiated by a type that contains
             generic variables. *)
          raise (Unify [])
      | Tconstr(p, tl, abbrev) ->
          (* XXX Pourquoi expanser ? *)
          begin try
            List.iter occur_rec tl
          with Unify lst ->
            let ty' =
              try expand_abbrev env p tl abbrev ty.level
              with Cannot_expand -> raise (Unify lst) in
            occur_rec ty'
          end
      | _ ->
          iter_type_expr occur_rec ty
      end
    end
  in
    occur_rec ty

let rec moregen env t1 t2 =
  if t1 == t2 then () else
  let t1 = repr t1 in
  let t2 = repr t2 in
  if t1 == t2 then () else
  let d1 = t1.desc in
  try
    begin match (t1.desc, t2.desc) with
      (Tvar, _) ->
        if t1.level = generic_level then raise (Unify []);
        moregen_occur env t1 t2;
        t1.desc <- Tlink t2
    | (Tarrow(t1, u1), Tarrow(t2, u2)) ->
        moregen env t1 t2; moregen env u1 u2
    | (Ttuple tl1, Ttuple tl2) ->
        moregen_list env tl1 tl2
    | (Tconstr(p1, tl1, abbrev1), Tconstr(p2, tl2, abbrev2)) ->
        if Path.same p1 p2 then begin
          try
            t1.desc <- Tlink t2;
            moregen_list env tl1 tl2;
            t1.desc <- d1
          with Unify lst ->
          t1.desc <- d1;
          try
            moregen env (expand_abbrev env p1 tl1 abbrev1 t1.level) t2
          with Cannot_expand ->
          try
            moregen env t1 (expand_abbrev env p2 tl2 abbrev2 t2.level)
          with Cannot_expand ->
            raise (Unify lst)
        end else begin
          try
            moregen env (expand_abbrev env p1 tl1 abbrev1 t1.level) t2
          with Cannot_expand ->
          try
            moregen env t1 (expand_abbrev env p2 tl2 abbrev2 t2.level)
          with Cannot_expand ->
            raise (Unify [])
        end
    | (Tobject(f1, _), Tobject(f2, _)) ->
        t1.desc <- Tlink t2;
        moregen_fields env f1 f2
    | (Tconstr(p1, tl1, abbrev1), _) ->
        begin try
          moregen env (expand_abbrev env p1 tl1 abbrev1 t1.level) t2
        with Cannot_expand ->
          raise (Unify [])
        end
    | (_, Tconstr(p2, tl2, abbrev2)) ->
        begin try
          moregen env t1 (expand_abbrev env p2 tl2 abbrev2 t2.level)
        with Cannot_expand ->
          raise (Unify [])
        end
    | (_, _) ->
        raise (Unify [])
    end
  with exn ->
    t1.desc <- d1;
    raise exn

and moregen_list env tl1 tl2 =
  if List.length tl1 <> List.length tl2 then
    raise (Unify []);
  List.iter2 (moregen env) tl1 tl2

and moregen_fields env ty1 ty2 =
  let (fields1, rest1) = flatten_fields ty1
  and (fields2, rest2) = flatten_fields ty2 in
  let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
  if miss1 <> [] then raise (Unify []);
  begin match rest1.desc with
    Tvar ->
      if rest1.level = generic_level then raise (Unify []);
      let fi = build_fields miss2 rest2 in
      moregen_occur env rest1 fi
  | Tnil ->
      if miss2 <> [] then raise (Unify []);
      if rest2.desc <> Tnil then raise (Unify [])
  | _ ->
      fatal_error "moregen_fields"
  end;
  List.iter (fun (t1, t2) -> moregen env t1 t2) pairs

let moregeneral env sch1 sch2 =
  begin_def();
  try
    moregen env (instance sch1) sch2;
    end_def();
    true
  with Unify _ ->
    end_def();
    false


                 (*********************************************)
                 (*  Equivalence between parameterized types  *)
                 (*********************************************)


(* XXX A voir... *)

let equal env params1 ty1 params2 ty2 =
  let subst = ref (List.combine params1 params2) in
  let type_pairs = ref [] in
  let rec eqtype t1 t2 =
    let t1 = repr t1 in
    let t2 = repr t2 in
    match (t1.desc, t2.desc) with
      (Tvar, Tvar) ->
        begin try
          List.assq t1 !subst == t2
        with Not_found ->
          subst := (t1, t2) :: !subst;
          true
        end
    | (Tarrow(t1, u1), Tarrow(t2, u2)) ->
        eqtype t1 t2 & eqtype u1 u2
    | (Ttuple tl1, Ttuple tl2) ->
        eqtype_list tl1 tl2
    | (Tconstr(p1, tl1, abbrev1), Tconstr(p2, tl2, abbrev2)) ->
        List.exists (function (t1', t2') -> t1 == t1' & t2 == t2') !type_pairs
        or begin
          type_pairs := (t1, t2) :: !type_pairs;
          if Path.same p1 p2 then
            eqtype_list tl1 tl2
          else begin
            try
              eqtype (expand_abbrev env p1 tl1 abbrev1 t1.level) t2
            with Cannot_expand ->
            try
              eqtype t1 (expand_abbrev env p2 tl2 abbrev2 t2.level)
            with Cannot_expand ->
              false
          end
        end
    | (Tobject (f1, _), Tobject (f2, _)) ->
        List.exists (function (t1', t2') -> t1 == t1' & t2 == t2') !type_pairs
        or begin
          type_pairs := (t1, t2) :: !type_pairs;
          eqtype_fields f1 f2
        end
    | (Tconstr(p1, tl1, abbrev1), _) ->
        begin try
          eqtype (expand_abbrev env p1 tl1 abbrev1 t1.level) t2
        with Cannot_expand ->
          false
        end
    | (_, Tconstr(p2, tl2, abbrev2)) ->
        begin try
          eqtype t1 (expand_abbrev env p2 tl2 abbrev2 t2.level)
        with Cannot_expand ->
          false
        end
    | (Tfield _, Tfield _) ->
        eqtype_fields t1 t2
    | (Tnil, Tnil) ->
        true
    | (_, _) ->
        false
  and eqtype_list tl1 tl2 =
    match (tl1, tl2) with
      ([], []) -> true
    | (t1::r1, t2::r2) -> eqtype t1 t2 & eqtype_list r1 r2
    | (_, _) -> false
  and eqtype_fields ty1 ty2 =           (* Optimization *)
    let (fields1, rest1) = flatten_fields ty1
    and (fields2, rest2) = flatten_fields ty2 in
    List.length fields1 = List.length fields2
      &
    eqtype rest1 rest2
      &
    List.for_all
      (function (label, t) ->
         List.exists
           (function (label', t') -> (label = label') & (eqtype t t'))
           fields2)
      fields1
  in
    eqtype ty1 ty2


                              (***************)
                              (*  Subtyping  *)
                              (***************)


(**** Build a subtype of a given type. ****)

let subtypes = ref []

(* XXX Types r<>cursifs ? *)
let rec build_subtype env t =
  let t = repr t in
  match t.desc with
    Tlink t' ->                         (* Redundant ! *)
      build_subtype env t'
  | Tvar ->
      (t, false)
  | Tarrow(t1, t2) ->
      let (t1', c1) = (t1, false) in
      let (t2', c2) = build_subtype env t2 in
      if c1 or c2 then (new_global_ty (Tarrow(t1', t2')), true)
      else (t, false)
  | Ttuple tlist ->
      let (tlist', clist) =
        List.split (List.map (build_subtype env) tlist)
      in
      if List.exists (function c -> c) clist then
        (new_global_ty (Ttuple tlist'), true)
      else (t, false)
  | Tconstr(p, tl, abbrev) when generic_abbrev env p ->
      let t' = expand_abbrev env p tl abbrev t.level in
      let (t'', c) = build_subtype env t' in
      if c then (t'', true)
      else (t, false)
  | Tconstr(p, tl, abbrev) ->
      (t, false)
  | Tobject (t1, _) when opened_object t1 ->
      (t, false)
  | Tobject (t1, _) ->
      (begin try
         List.assq t !subtypes
       with Not_found ->
         let t' = new_global_var () in
         subtypes := (t, t')::!subtypes;
         let (t1', _) = build_subtype env t1 in
         t'.desc <- Tobject (t1', ref None);
         t'
       end,
       true)
  | Tfield(s, t1, t2) ->
      let (t1', _) = build_subtype env t1 in
      let (t2', _) = build_subtype env t2 in
      (new_global_ty (Tfield(s, t1', t2')), true)
  | Tnil ->
      let v = new_global_var () in
      (v, true)

let enlarge_type env ty =
  subtypes := [];
  let (ty', _) = build_subtype env ty in
  subtypes := [];
  ty'

(**** Check whether a type is a subtype of another type. ****)

(*
    During the traversal, a trace of visited types is maintained. It
    is printed in case of error.
    Constraints (pairs of types that must be equals) are accumulated
    rather than being enforced straight. Indeed, the result would
    otherwise depend on the order in which these constraints are
    enforced.
    A function enforcing these constraints is returned. That way, type
    variables can be bound to their actual values before this function
    is called (see Typecore).
    Only well-defined abbreviations are expanded (hence the tests
    [generic_abbrev ...]).
*)

let subtypes = ref [];;

let subtype_error env trace =
  raise (Subtype (expand_trace env (List.rev trace), []))

let rec subtype_rec env trace t1 t2 =
  let t1 = repr t1 in
  let t2 = repr t2 in
  if t1 == t2 then [] else
  if List.exists (fun (t1', t2') -> t1 == t1' & t2 == t2') !subtypes then
    []
  else begin
    subtypes := (t1, t2) :: !subtypes;
    match (t1.desc, t2.desc) with
      (Tvar, _) | (_, Tvar) ->
        [(trace, t1, t2)]
    | (Tarrow(t1, u1), Tarrow(t2, u2)) ->
        (subtype_rec env ((t2, t1)::trace) t2 t1) @
        (subtype_rec env ((u1, u2)::trace) u1 u2)
    | (Ttuple tl1, Ttuple tl2) ->
        subtype_list env trace tl1 tl2
    | (Tconstr(p1, tl1, abbrev1), Tconstr _) when generic_abbrev env p1 ->
        subtype_rec env trace (expand_abbrev env p1 tl1 abbrev1 t1.level) t2
    | (Tconstr _, Tconstr(p2, tl2, abbrev2)) when generic_abbrev env p2 ->
        subtype_rec env trace t1 (expand_abbrev env p2 tl2 abbrev2 t2.level)
    | (Tconstr _, Tconstr _) ->
        [(trace, t1, t2)]
    | (Tconstr(p1, tl1, abbrev1), _) when generic_abbrev env p1 ->
        subtype_rec env trace (expand_abbrev env p1 tl1 abbrev1 t1.level) t2
    | (_, Tconstr (p2, tl2, abbrev2)) when generic_abbrev env p2 ->
        subtype_rec env trace t1 (expand_abbrev env p2 tl2 abbrev2 t2.level)
    | (Tobject (f1, _), Tobject (f2, _))
              when opened_object f1 & opened_object f2 ->
        (* Same row variable implies same object. *)
        [(trace, t1, t2)]
    | (Tobject (f1, _), Tobject (f2, _)) ->
        subtype_fields env trace f1 f2
    | (_, _) ->
        subtype_error env trace
  end

and subtype_list env trace tl1 tl2 =
  if List.length tl1 <> List.length tl2 then
    subtype_error env trace;
  List.fold_left2
    (fun cstrs t1 t2 -> cstrs @ (subtype_rec env ((t1, t2)::trace) t1 t2))
    [] tl1 tl2

and subtype_fields env trace ty1 ty2 =
  let (fields1, rest1) = flatten_fields ty1 in
  let (fields2, rest2) = flatten_fields ty2 in
  let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
  begin match rest1.desc with
    Tvar   -> [(trace, rest1, build_fields miss2 (newvar ()))]
  | Tnil   -> if miss2 = [] then [] else subtype_error env trace
  | _      -> fatal_error "Ctype.subtype_fields (1)"
  end
    @
  begin match rest2.desc with
    Tvar   -> [(trace, build_fields miss1 (rest1), rest2)]
  | Tnil   -> []
  | _      -> fatal_error "Ctype.subtype_fields (2)"
  end
    @
  (List.fold_left
     (fun cstrs (t1, t2) -> cstrs @ (subtype_rec env ((t1, t2)::trace) t1 t2))
     [] pairs)

let subtype env ty1 ty2 =
  subtypes := [];
  (* Build constraint set. *)
  let cstrs = subtype_rec env [(ty1, ty2)] ty1 ty2 in
  (* Enforce constraints. *)
  function () ->
    List.iter
      (function (trace0, t1, t2) ->
         try unify env t1 t2 with Unify trace ->
           raise (Subtype (expand_trace env (List.rev trace0),
                           List.tl (List.tl trace))))
      cstrs;
    subtypes := []


                              (*************************)
                              (*  Remove dependencies  *)
                              (*************************)


let inst_subst = ref ([] : (type_expr * type_expr) list)

(* XXX A voir... *)
(* XXX Petit probleme... (deroulement) *)
(*     module F(X : sig type t end) = struct type t = X.t end;;       *)
(*     module M = F(struct type t = <x : t> end);;                    *)
(*  -> module M : sig type t = < x : < x : 'a > as 'a > end  *)
let rec nondep_type_rec env id ty =
  let ty = repr ty in
  if ty.desc = Tvar then ty else
  try newgenty (Tlink (List.assq ty !inst_subst)) with Not_found ->
            (* Tlink important permet de ne pas modifier la variable *)
    let ty' = newgenvar () in
    inst_subst := (ty, ty') :: !inst_subst;
    ty'.desc <-
      begin match ty.desc with
        Tvar ->
          Tvar
      | Tarrow(t1, t2) ->
          Tarrow(nondep_type_rec env id t1, nondep_type_rec env id t2)
      | Ttuple tl ->
          Ttuple(List.map (nondep_type_rec env id) tl)
      | Tconstr(p, tl, abbrev) ->
          if Path.isfree id p then
            begin try
              (nondep_type_rec env id
                 (expand_abbrev env p tl abbrev ty.level)).desc
            with Cannot_expand ->
              raise Not_found
            end
          else
            Tconstr(p, List.map (nondep_type_rec env id) tl, ref Mnil)
      | Tobject (t1, name) ->
          Tobject (nondep_type_rec env id t1,
                 ref (match !name with
                        None -> None
                      | Some (p, tl) ->
                          if Path.isfree id p then None
                          else Some (p, List.map (nondep_type_rec env id) tl)))
       | Tfield(label, t1, t2) ->
           Tfield(label, nondep_type_rec env id t1, nondep_type_rec env id t2)
       | Tnil ->
           Tnil
       | Tlink _ ->
           fatal_error "Ctype.nondep_type"
       end;
     ty'

let nondep_type env id ty =
  inst_subst := [];
  let ty' = nondep_type_rec env id ty in
  inst_subst := [];
  ty'

let nondep_class_type env id decl =
  inst_subst := [];
  let decl =
    { cty_params = List.map (nondep_type_rec env id) decl.cty_params;
      cty_args = List.map (nondep_type_rec env id) decl.cty_args;
      cty_vars =
        Vars.fold (fun l (m, t) -> Vars.add l (m, nondep_type_rec env id t))
          decl.cty_vars Vars.empty;
      cty_self = nondep_type_rec env id decl.cty_self;
      cty_concr = decl.cty_concr;
      cty_new =
        begin match decl.cty_new with
          None    -> None
        | Some ty -> Some (nondep_type_rec env id ty)
        end }
  in
  inst_subst := [];
  decl


                              (******************)
                              (*  Type pruning  *)
                              (******************)


(* XXX Rendu obsolete par abbreviations avec contraintes ? *)

let inst_subst = ref ([] : (type_expr * type_expr) list)

let rec prune_rec top cstr ty =
  let ty = repr ty in
  try List.assq ty (if top then [] else cstr) with Not_found ->
  match ty.desc with
    Tvar ->
      if ty.level = generic_level then
        begin try
          List.assq ty !inst_subst
        with Not_found ->
          let ty' = newvar() in
          inst_subst := (ty, ty') :: !inst_subst;
          ty'
        end
      else
        ty
  | Tarrow(t1, t2) ->
      newty (Tarrow(prune_rec false cstr t1, prune_rec false cstr t2))
  | Ttuple tl ->
      newty (Ttuple(List.map (prune_rec false cstr) tl))
  | Tconstr(p, tl, _) ->
      begin try
        List.assq ty !inst_subst
      with Not_found ->
        let ty' = newvar() in
        inst_subst := (ty, ty') :: !inst_subst;
        let ty'' = 
          newty (Tconstr(p, List.map (prune_rec false cstr) tl, ref Mnil))
        in
          ty'.desc <- Tlink ty'';
          ty''
      end
  | Tobject (t1, name) ->
      begin try
        List.assq ty !inst_subst
      with Not_found ->
        let ty' = newvar() in
        inst_subst := (ty, ty') :: !inst_subst;
        let ty'' = newty
          (Tobject (prune_rec false cstr t1,
                    ref (match !name with
                           None -> None
                         | Some (p, tl) ->
                             Some (p, List.map (prune_rec false cstr) tl))))
        in
          ty'.desc <- Tlink ty'';
          ty''
      end
  | Tfield(label, t1, t2) ->
      newty (Tfield(label, prune_rec false cstr t1, prune_rec false cstr t2))
  | Tnil ->
      newty Tnil
  | Tlink _             ->
      fatal_error "Ctype.prune_rec"

let prune_cstr cstr (old_cstr, new_cstr) ((ty, v) as c) =
  let c' =
    try (v, List.assq ty old_cstr) with Not_found ->
    match ty.desc with
      Tvar ->
        (v, v)
    | _ ->
        (v, prune_rec true cstr ty)
  in
    (c :: old_cstr, c' :: new_cstr)

let prune ty leaves =
  inst_subst := [];
  let cstr = List.map (fun leaf -> (repr leaf, newvar ())) leaves in
  let new_ty = prune_rec true cstr ty in
  inst_subst := [];
  (new_ty, List.map (fun (ty, v) -> (v, ty)) cstr)

let prune_class_type cl =
  inst_subst := [];
  let cstr = List.map (fun leaf -> (repr leaf, newvar ())) cl.cty_params in
  let args = List.map (prune_rec false cstr) cl.cty_args in
  let vars =
    Vars.fold
      (fun lab (mut, ty) -> Vars.add lab (mut, prune_rec false cstr ty))
      cl.cty_vars Vars.empty in
  let self = prune_rec true cstr cl.cty_self in
  let (_, cstr) = List.fold_left (prune_cstr cstr) ([], []) cstr in
  inst_subst := [];
  (List.rev cstr, args, vars, self)


                              (******************************)
                              (*  Abbreviation correctness  *)
                              (******************************)


exception Nonlinear_abbrev
exception Recursive_abbrev

let rec non_recursive_abbrev env path constrs ty =
  let ty = repr ty in
  match ty.desc with
    Tarrow (ty1, ty2) ->
      non_recursive_abbrev env path constrs ty1;
      non_recursive_abbrev env path constrs ty2
  | Ttuple tl ->
      List.iter (non_recursive_abbrev env path constrs) tl
  | Tconstr(p, args, abbrev) ->
      if Path.same path p then
        raise Recursive_abbrev
      else begin
        begin try
          let ty' = expand_abbrev env p args abbrev ty.level in
          if List.memq ty' constrs then () else
            non_recursive_abbrev env path (ty'::constrs) ty'
        with Cannot_expand ->
          ()
        end
      end
  | _ (* Tvar | Tobject (_, _) | Tfield (_, _, _) | Tnil *) ->
      ()

let rec path_assoc x =
  function
    [] -> raise Not_found
  | (a,b)::l -> if Path.same a x then b else path_assoc x l

let visited_abbrevs = ref []

let visited_abbrev p args =
  try
    let slot = path_assoc p !visited_abbrevs in
    if
      List.exists
        (function args' ->
           List.for_all2 (fun ty ty' -> repr ty == ty') args args')
        !slot
    then
      true
    else begin
      slot := (List.map repr args)::!slot;
      false
    end
  with Not_found ->
    visited_abbrevs := (p, ref [args])::!visited_abbrevs;
    false

let rec linear_abbrev env path params visited ty =
  let ty = repr ty in
  match ty.desc with
    Tarrow (ty1, ty2) ->
      linear_abbrev env path params visited ty1;
      linear_abbrev env path params visited ty2
  | Ttuple tl ->
      List.iter (linear_abbrev env path params visited) tl
  | Tconstr(p, args, abbrev) ->
      if Path.same p path then begin
        if
          List.exists (fun (ty1, ty2) -> repr ty1 != repr ty2)
            (List.combine params args)
        then
          raise Nonlinear_abbrev
      end else begin
        try
          let ty' = expand_abbrev env p args abbrev ty.level in
          if not (visited_abbrev p args) then
            linear_abbrev env path params visited ty'
        with Cannot_expand ->
        if not (List.memq ty visited) then begin
          List.iter
            (linear_abbrev env path params (ty::visited))
            args
        end
      end
  | Tobject (ty', _) ->
      if not (List.memq ty visited) then
        linear_abbrev env path params (ty::visited) ty'
  | Tfield(_, ty1, ty2) ->
      linear_abbrev env path params visited ty1;
      linear_abbrev env path params visited ty2
  | _ (* Tvar | Tnil *) ->
      ()

let correct_abbrev env ident params ty =
  let path = Path.Pident ident in
  non_recursive_abbrev env path [] ty;
  if params <> [] then begin
    visited_abbrevs := [];
    linear_abbrev env path params [] ty;
    visited_abbrevs := []
  end


                              (*******************)
                              (*  Miscellaneous  *)
                              (*******************)


let unroll_abbrev id tl ty =
  let ty = repr ty in
  match ty.desc with
    Tvar ->
      (* XXX Maybe abbreviations should not expand to a type variable ? *)
      ty
  | _ ->
      let ty' = {desc = ty.desc; level = ty.level} in
      ty.desc <- Tlink {desc = Tconstr (Path.Pident id, tl, ref Mnil);
                        level = ty.level};
      ty'

type closed_schema_result = Var of type_expr | Row_var of type_expr
exception Failed of closed_schema_result

let visited = ref []

let rec closed_schema_rec ty =
  let ty = repr ty in
  if not (List.memq ty !visited) then begin
    visited := ty::!visited;
    match ty.desc with
      Tvar when ty.level != generic_level -> raise (Failed (Var ty))
    | Tobject(f, {contents = Some (_, p)}) ->
        begin try closed_schema_rec f with
          Failed (Row_var v) -> raise (Failed (Var v))
        | Failed (Var v) -> raise (Failed (Row_var v))
        end;
        List.iter closed_schema_rec p
    | Tobject(f, _) ->
        begin try closed_schema_rec f with
          Failed (Row_var v) -> raise (Failed (Var v))
        | Failed (Var v) -> raise (Failed (Row_var v))
        end
    | Tfield(_, t1, t2) ->
        begin try
          closed_schema_rec t1
        with
          Failed (Row_var v) -> raise (Failed (Var v))
        | Failed (Var v) -> raise (Failed (Row_var v))
        end;
        closed_schema_rec t2
    | _ ->
        iter_type_expr closed_schema_rec ty
  end

let closed_schema ty =
  visited := [];
  try
    closed_schema_rec ty;
    visited := [];
    true
  with Failed _ ->
    visited := [];
    false

let closed_schema_verbose ty =
  visited := [];
  try
    closed_schema_rec ty;
    visited := [];
    None
  with Failed status ->
    visited := [];
    Some status

let is_generic ty =
  let ty = repr ty in
  match ty.desc with
    Tvar -> ty.level = generic_level
  | _ -> fatal_error "Ctype.is_generic"

let rec arity ty =
  match (repr ty).desc with
    Tarrow(t1, t2) -> 1 + arity t2
  | _ -> 0