(**************************************************************************)
(*                                                                        *)
(*                                 OCaml                                  *)
(*                                                                        *)
(*             Xavier Leroy, projet Cristal, INRIA Rocquencourt           *)
(*                                                                        *)
(*   Copyright 1996 Institut National de Recherche en Informatique et     *)
(*     en Automatique.                                                    *)
(*                                                                        *)
(*   All rights reserved.  This file is distributed under the terms of    *)
(*   the GNU Lesser General Public License version 2.1, with the          *)
(*   special exception on linking described in the file LICENSE.          *)
(*                                                                        *)
(**************************************************************************)

open Misc
open Longident
open Path
open Asttypes
open Parsetree
open Types
open Format_doc

module Style = Misc.Style

let () = Includemod_errorprinter.register ()

module Sig_component_kind = Shape.Sig_component_kind
module String = Misc.Stdlib.String

type hiding_error =
  | Illegal_shadowing of {
      shadowed_item_id: Ident.t;
      shadowed_item_kind: Sig_component_kind.t;
      shadowed_item_loc: Location.t;
      shadower_id: Ident.t;
      user_id: Ident.t;
      user_kind: Sig_component_kind.t;
      user_loc: Location.t;
    }
  | Appears_in_signature of {
      opened_item_id: Ident.t;
      opened_item_kind: Sig_component_kind.t;
      user_id: Ident.t;
      user_kind: Sig_component_kind.t;
      user_loc: Location.t;
    }

type error =
    Cannot_apply of module_type
  | Not_included of Includemod.explanation
  | Cannot_eliminate_dependency of module_type
  | Signature_expected
  | Structure_expected of module_type
  | With_no_component of Longident.t
  | With_mismatch of Longident.t * Includemod.explanation
  | With_makes_applicative_functor_ill_typed of
      Longident.t * Path.t * Includemod.explanation
  | With_changes_module_alias of Longident.t * Ident.t * Path.t
  | With_creates_invalid_aliases of Ident.t * Path.t * Path.t
  | With_cannot_remove_constrained_type
  | With_package_manifest of Longident.t * type_expr
  | Repeated_name of Sig_component_kind.t * string
  | Non_generalizable of { vars : type_expr list; expression : type_expr }
  | Non_generalizable_module of
      { vars : type_expr list; item : value_description; mty : module_type }
  | Implementation_is_required of string
  | Interface_not_compiled of string
  | Not_allowed_in_functor_body
  | Not_a_packed_module of type_expr
  | Incomplete_packed_module of type_expr
  | Scoping_pack of Longident.t * type_expr
  | Recursive_module_require_explicit_type
  | Apply_generative
  | Cannot_scrape_alias of Path.t
  | Cannot_scrape_package_type of Path.t
  | Badly_formed_signature of string * Typedecl.error
  | Cannot_hide_id of hiding_error
  | Invalid_type_subst_rhs
  | Non_packable_local_modtype_subst of Path.t
  | With_cannot_remove_packed_modtype of Path.t * module_type
  | Cannot_alias of Path.t

exception Error of Location.t * Env.t * error
exception Error_forward of Location.error

open Typedtree

let rec path_concat head p =
  match p with
    Pident tail -> Pdot (Pident head, Ident.name tail)
  | Pdot (pre, s) -> Pdot (path_concat head pre, s)
  | Papply _ -> assert false
  | Pextra_ty (p, extra) -> Pextra_ty (path_concat head p, extra)

(* Extract a signature from a module type *)

let extract_sig env loc mty =
  match Env.scrape_alias env mty with
    Mty_signature sg -> sg
  | Mty_alias path ->
      raise(Error(loc, env, Cannot_scrape_alias path))
  | _ -> raise(Error(loc, env, Signature_expected))

let extract_sig_open env loc mty =
  match Env.scrape_alias env mty with
    Mty_signature sg -> sg
  | Mty_alias path ->
      raise(Error(loc, env, Cannot_scrape_alias path))
  | mty -> raise(Error(loc, env, Structure_expected mty))

(* Compute the environment after opening a module *)

let type_open_ ?used_slot ?toplevel ovf env loc lid =
  let path = Env.lookup_module_path ~load:true ~loc:lid.loc lid.txt env in
  match Env.open_signature ~loc ?used_slot ?toplevel ovf path env with
  | Ok env -> path, env
  | Error _ ->
      let md = Env.find_module path env in
      ignore (extract_sig_open env lid.loc md.md_type);
      assert false

let initial_env ~loc ~initially_opened_module
    ~open_implicit_modules =
  let env = Env.initial in
  let open_module env m =
    let open Asttypes in
    let lexbuf = Lexing.from_string m in
    let txt =
      Location.init lexbuf (Printf.sprintf "command line argument: -open %S" m);
      Parse.simple_module_path lexbuf in
        snd (type_open_ Override env loc {txt;loc})
  in
  let add_units env units =
    String.Set.fold
      (fun name env ->
         Env.add_persistent_structure (Ident.create_persistent name) env)
      units
      env
  in
  let units =
    List.map Env.persistent_structures_of_dir (Load_path.get_visible ())
  in
  let env, units =
    match initially_opened_module with
    | None -> (env, units)
    | Some m ->
        (* Locate the directory that contains [m], adds the units it
           contains to the environment and open [m] in the resulting
           environment. *)
        let rec loop before after =
          match after with
          | [] -> None
          | units :: after ->
              if String.Set.mem m units then
                Some (units, List.rev_append before after)
              else
                loop (units :: before) after
        in
        let env, units =
          match loop [] units with
          | None ->
              (env, units)
          | Some (units_containing_m, other_units) ->
              (add_units env units_containing_m, other_units)
        in
        (open_module env m, units)
  in
  let env = List.fold_left add_units env units in
  List.fold_left open_module env open_implicit_modules

let type_open_descr ?used_slot ?toplevel env sod =
  let (path, newenv) =
    Builtin_attributes.warning_scope sod.popen_attributes
      (fun () ->
         type_open_ ?used_slot ?toplevel sod.popen_override env sod.popen_loc
           sod.popen_expr
      )
  in
  let od =
    {
      open_expr = (path, sod.popen_expr);
      open_bound_items = [];
      open_override = sod.popen_override;
      open_env = newenv;
      open_attributes = sod.popen_attributes;
      open_loc = sod.popen_loc;
    }
  in
  (od, newenv)

(* Forward declaration, to be filled in by type_module_type_of *)
let type_module_type_of_fwd :
    (Env.t -> Parsetree.module_expr ->
      Typedtree.module_expr * Types.module_type) ref
  = ref (fun _env _m -> assert false)

(* Additional validity checks on type definitions arising from
   recursive modules *)

let check_recmod_typedecls env decls =
  let recmod_ids = List.map fst decls in
  List.iter
    (fun (id, md) ->
      List.iter
        (fun path ->
          Typedecl.check_recmod_typedecl env md.Types.md_loc recmod_ids
                                         path (Env.find_type path env))
        (Mtype.type_paths env (Pident id) md.Types.md_type))
    decls

(* Merge one "with" constraint in a signature *)

let check_type_decl env sg loc id row_id newdecl decl =
  let fresh_id = Ident.rename id in
  let path = Pident fresh_id in
  let sub = Subst.add_type id path Subst.identity in
  let fresh_row_id, sub =
    match row_id with
    | None -> None, sub
    | Some id ->
      let fresh_row_id = Some (Ident.rename id) in
      let sub = Subst.add_type id (Pident fresh_id) sub in
      fresh_row_id, sub
  in
  let newdecl = Subst.type_declaration sub newdecl in
  let decl = Subst.type_declaration sub decl in
  let sg = List.map (Subst.signature_item Keep sub) sg in
  let env = Env.add_type ~check:false fresh_id newdecl env in
  let env =
    match fresh_row_id with
    | None -> env
    | Some fresh_row_id -> Env.add_type ~check:false fresh_row_id newdecl env
  in
  let env = Env.add_signature sg env in
  Includemod.type_declarations ~mark:true ~loc env fresh_id newdecl decl;
  Typedecl.check_coherence env loc path newdecl

let make_variance p n i =
  let open Variance in
  set_if p May_pos (set_if n May_neg (set_if i Inj null))

let rec iter_path_apply p ~f =
  match p with
  | Pident _ -> ()
  | Pdot (p, _) -> iter_path_apply p ~f
  | Papply (p1, p2) ->
     iter_path_apply p1 ~f;
     iter_path_apply p2 ~f;
     f p1 p2 (* after recursing, so we know both paths are well typed *)
  | Pextra_ty _ -> assert false

(** Checks if a flat (without functor applications) path [path] admits [~prefix]
    as a prefix, i.e. if [path = ~prefix::suffix]. The [~strict] flag indicates
    if equal paths should be rejected *)
let path_is_prefix ~strict =
  let rec list_is_prefix l ~prefix =
    match l, prefix with
    | [], [] -> (not strict)
    | _ :: _, [] -> true
    | [], _ :: _ -> false
    | s1 :: t1, s2 :: t2 ->
       String.equal s1 s2 && list_is_prefix t1 ~prefix:t2
  in
  fun path ~prefix ->
    match Path.flatten path, Path.flatten prefix with
    | `Contains_apply, _ | _, `Contains_apply -> false
    | `Ok (ident1, l1), `Ok (ident2, l2) ->
       Ident.same ident1 ident2
       && list_is_prefix l1 ~prefix:l2

let iterator_with_env super env =
  let env = ref (lazy env) in
  env, { super with
    Btype.it_signature = (fun self sg ->
      (* add all items to the env before recursing down, to handle recursive
         definitions *)
      let env_before = !env in
      env := lazy (Env.add_signature sg (Lazy.force env_before));
      super.Btype.it_signature self sg;
      env := env_before
    );
    Btype.it_module_type = (fun self -> function
    | Mty_functor (param, mty_body) ->
      let env_before = !env in
      begin match param with
      | Unit -> ()
      | Named (param, mty_arg) ->
        self.Btype.it_module_type self mty_arg;
        match param with
        | None -> ()
        | Some id ->
          env := lazy (Env.add_module ~noalias:true id Mp_present
                       mty_arg (Lazy.force env_before))
      end;
      self.Btype.it_module_type self mty_body;
      env := env_before;
    | mty ->
      super.Btype.it_module_type self mty
    )
  }

let retype_applicative_functor_type ~loc env funct arg =
  let mty_functor = (Env.find_module funct env).md_type in
  let mty_arg = (Env.find_module arg env).md_type in
  let mty_param =
    match Env.scrape_alias env mty_functor with
    | Mty_functor (Named (_, mty_param), _) -> mty_param
    | _ -> assert false (* could trigger due to MPR#7611 *)
  in
  Includemod.check_modtype_inclusion ~loc env mty_arg arg mty_param

(* When doing a deep destructive substitution with type M.N.t := .., we change M
   and M.N and so we have to check that uses of the modules other than just
   extracting components from them still make sense. There are only two such
   kinds of uses:
   - applicative functor types: F(M).t might not be well typed anymore
   - aliases: module A = M still makes sense but it doesn't mean the same thing
     anymore, so it's forbidden until it's clear what we should do with it.
   This function would be called with M.N.t and N.t to check for these uses.

   The first argument [paths] must be non-empty.
*)
let check_usage_of_path_of_substituted_item paths ~loc ~lid env super =
  match paths with
  | []  -> assert false (* affected paths must be a non-empty list *)
  | [_] -> super (* Shallow substitution, nothing to check *)
  | _   ->
      let last, rest = match List.rev paths with
        | [] -> assert false
        | last :: rest -> last, rest
      in
      (* The last item is the one that's removed. We don't need to check how
            it's used since it's replaced by a more specific type/module. *)
      assert (match last with Pident _ -> true | _ -> false);
    { super with
      Btype.it_signature_item = (fun self -> function
      | Sig_module (id, _, { md_type = Mty_alias aliased_path; _ }, _, _)
        when List.exists
            (fun p -> path_is_prefix p ~prefix:aliased_path ~strict:true) rest
        ->
         let e = With_changes_module_alias (lid.txt, id, aliased_path) in
         raise(Error(loc, Lazy.force !env, e))
      | sig_item ->
         super.Btype.it_signature_item self sig_item
      );
      Btype.it_path = (fun referenced_path ->
        iter_path_apply referenced_path ~f:(fun funct arg ->
          if List.exists
               (fun path -> path_is_prefix path ~prefix:arg ~strict:true) rest
          then
            let env = Lazy.force !env in
            match retype_applicative_functor_type ~loc env funct arg with
            | None -> ()
            | Some explanation ->
                raise(Error(loc, env,
                            With_makes_applicative_functor_ill_typed
                            (lid.txt, referenced_path, explanation)))
        )
      );
    }

(** When doing destructive module substitutions [with module X = P], the path
    [P] can be non-aliasable (by containing a functor parameter, functor
    application or recursive module). If it is the case, module aliases to [X]
    or any suffix [X.X'] would become invalid. This function checks that there
    are no module aliases to suffixes of the list of affected paths [paths]. The
    [invalid_alias] argument indicates if the test should be added to the
    iterator. Its payload [invalid_alias_path] is just used for the error
    message *)
let check_invalid_aliases paths ~loc env invalid_alias super =
  match invalid_alias with
  | None -> super (* No possible introduction of invalid alias, so no extension
                     of the iterator*)
  | Some invalid_alias_path ->
      let would_become_invalid_path aliased_path =
        List.exists
          (fun p -> path_is_prefix aliased_path ~prefix:p ~strict:false) paths
      in
      { super with
        Btype.it_signature_item = (fun self -> function
            | Sig_module (id, _, {md_type = Mty_alias aliased_path}, _, _)
              when would_become_invalid_path aliased_path ->
                raise(Error(loc, Lazy.force !env,
                            With_creates_invalid_aliases
                              (id, aliased_path, invalid_alias_path)))
            | sig_item ->
                super.Btype.it_signature_item self sig_item
          );
      }

(** This function checks the effect of destructive substitutions and the
    introduction of invalid aliases *)
let check_usage_after_substitution env ~loc ~lid paths ?(invalid_alias=None) sg=
  match paths, invalid_alias with
  (* Shallow substitution without introduction of an invalid alias : nothing to
     check (so no traversal of the signature) *)
  | [_], None -> ()
  (* Deep substitution, or possible introduction of invalid alias *)
  | _, _ ->
      with_type_mark begin fun mark ->
        let env, base_iterator =
          iterator_with_env (Btype.type_iterators mark) env in
        let iterator =
          base_iterator
          |> check_usage_of_path_of_substituted_item paths ~loc ~lid env
          |> check_invalid_aliases paths ~loc env invalid_alias
        in
        iterator.Btype.it_signature iterator sg
      end

(* After substitution one also needs to re-check the well-foundedness
   of type declarations in recursive modules *)
let rec extract_next_modules = function
  | Sig_module (id, _, mty, Trec_next, _) :: rem ->
      let (id_mty_l, rem) = extract_next_modules rem in
      ((id, mty) :: id_mty_l, rem)
  | sg -> ([], sg)

let check_well_formed_module env loc context mty =
  (* Format.eprintf "@[check_well_formed_module@ %a@]@."
     Printtyp.modtype mty; *)
  let open Btype in
  let iterator =
    let rec check_signature env = function
      | [] -> ()
      | Sig_module (id, _, mty, Trec_first, _) :: rem ->
          let (id_mty_l, rem) = extract_next_modules rem in
          begin try
            check_recmod_typedecls (Lazy.force env) ((id, mty) :: id_mty_l)
          with Typedecl.Error (_, err) ->
            raise (Error (loc, Lazy.force env,
                          Badly_formed_signature(context, err)))
          end;
          check_signature env rem
      | _ :: rem ->
          check_signature env rem
    in
    let env, super =
      iterator_with_env Btype.type_iterators_without_type_expr env in
    { super with
      it_signature = (fun self sg ->
        let env_before = !env in
        let env = lazy (Env.add_signature sg (Lazy.force env_before)) in
        check_signature env sg;
        super.it_signature self sg);
    }
  in
  iterator.it_module_type iterator mty

let () = Env.check_well_formed_module := check_well_formed_module

let type_decl_is_alias sdecl = (* assuming no explicit constraint *)
  match sdecl.ptype_manifest with
  | Some {ptyp_desc = Ptyp_constr (lid, stl)}
       when List.length stl = List.length sdecl.ptype_params ->
     begin
       match
         List.iter2 (fun x (y, _) ->
             match x, y with
               {ptyp_desc=Ptyp_var sx}, {ptyp_desc=Ptyp_var sy}
                  when sx = sy -> ()
             | _, _ -> raise Exit)
           stl sdecl.ptype_params;
       with
       | exception Exit -> None
       | () -> Some lid
     end
  | _ -> None

let params_are_constrained =
  let rec loop = function
    | [] -> false
    | hd :: tl ->
       match get_desc hd with
       | Tvar _ -> List.memq hd tl || loop tl
       | _ -> true
  in
  loop

module Merge = struct
  (** This module hosts the functions dealing with signature constraints. There
     are of three forms :
     - type constraint [... with type t = ... ], handled by [merge_type]
     - module constraint [... with module X = ... ], handled by [merge_module]
     - module type constraints [... with module type T = ...] handled by
       [merge_modtype]

     Each constraint can be *destructive*, (with the syntax [:=]) meaning that
     the substituted identifier is removed from the signature. This imposes
     additional checks to ensure wellformedness, handled by the [post_process]
     function.

     Each constraint can be *deep*, meaning that the substituted identifier
     might be inside a submodule. This is handled by the [patch_deep_item]
     function. Deep destructive substitutions inside submodules with an alias
     signature are disallowed.

     Each constraint can be *instantiating*, if the substitution replaces an
     "abstract" field (for module constraints, "abstract" means "not already an
     alias"). If the constraint is not instantiating, equivalence checks with
     the old definition are performed.

     Finally, merging is both used in (1) "normal" mode, to build a typed tree,
     in (2) "approx" mode, during the signature approximation phase of
     typechecking recursive modules, and in (3) "package" mode, for checking
     signatures of first-class modules.

     The overall structure is similar for each form:

     1. A [patch] function is defined to identify the item to substitute, do the
     equivalence checks if needed, and optionally build the new replacement item
     (if the substitution is non-destructive)

     2. The patch is applied to the module type by using the general
     [merge_signature] function. It returns the path of the affected item (along
     with the list of all suffixes, if the substitution was deep).

     3. Some post processing is applied (actual replacement for destructive
     substitutions, wellformedness checks)

  *)

  (** For the merging of type fields [S with type P.t = tdecl], the typedtree
      for the right-hand side type declaration [tdecl] is built at the point of
      the (possibly deep) constrained item [P.t] inside [S]. It is returned as
      an extra payload by merge. Other cases (module, module types) don't use
      the payload mechanism (the payload is then [()]). *)

  let return_payload ~ghosts ~replace_by ~late_typedtree ?(paths=[]) path =
    Some ((path, path::paths, late_typedtree),
          {Signature_group.ghosts; replace_by})

  let return = return_payload ~late_typedtree:()

  let split_row_id s ghosts =
    let srow = s ^ "#row" in
    let rec split before = function
      | Sig_type(id,_,_,_) :: rest when Ident.name id = srow ->
          before, Some id, rest
      | a :: rest -> split (a::before) rest
      | [] -> before, None, []
    in
    split [] ghosts

  let unsafe_signature_subst initial_env loc sg sub =
    (* This signature will not be used directly, it will always be freshened
       by the caller. So what we do with the scope doesn't really matter. But
       making it local makes it unlikely that we will ever use the result of
       this function unfreshened without issue. *)
    match Subst.Unsafe.signature Make_local sub sg with
    | Ok x -> x
    | Error (Fcm_type_substituted_away (p,mty)) ->
        let error = With_cannot_remove_packed_modtype(p,mty) in
        raise (Error(loc,initial_env,error))

  (* After the item has been patched, post processing does the actual
     destructive substitution and checks wellformedness of the resulting
     signature *)
  let post_process ~destructive loc lid env paths sg
      ?(invalid_alias=None) replace =
    let sg =
      if destructive then
        (* Check that the substitution will not make the signature ill-formed *)
        let () = check_usage_after_substitution ~loc ~lid env paths
        ~invalid_alias sg in
        (* Actually remove the identifiers *)
        let sub = Subst.change_locs Subst.identity loc in
        let sub = List.fold_left replace sub paths in
        unsafe_signature_subst env loc sg sub
      else sg
    in
    (* check that the resulting signature is still wellformed *)
    let () = check_well_formed_module env loc "this instantiated signature"
        (Mty_signature sg) in
    sg

  (* Main recursive knot to handle deep merges *)
  let rec merge_signature initial_env env sg namelist loc lid
      ~patch ~destructive =
    match
      Signature_group.replace_in_place
        (patch_deep_item ~patch ~destructive
           namelist initial_env env sg loc lid) sg
    with
    | Some ((p, paths, late_typedtree), sg) -> p, paths, late_typedtree, sg
    | None -> raise(Error(loc, initial_env, With_no_component lid.txt))
    | exception Includemod.Error explanation ->
      raise(Error(loc, initial_env, With_mismatch(lid.txt, explanation)))

  and patch_deep_item ~ghosts ~patch ~destructive
      namelist initial_env (env: Env.t) outer_sg loc lid item =
    match item, namelist with
    (* Shallow constraints : call the patch function *)
    | item, [s] -> patch item s env outer_sg ~ghosts

    (* Deep constraints *)
    | Sig_module(id, _, md, rs, priv) as current_item, s :: namelist
      when Ident.name id = s ->
        let sig_env = Env.add_signature outer_sg env in
        let sg = extract_sig sig_env loc md.md_type in
        let subpath, paths, late_typedtree, newsg =
          merge_signature ~patch initial_env sig_env sg
            namelist loc lid ~destructive in
        let path = path_concat id subpath in
        begin
          match md.md_type, destructive with
          | Mty_alias _, false ->
              (* Deep non-destructive substitutions inside aliases are checked,
                 but do not change the resulting signature *)
              return_payload ~ghosts
                ~replace_by:(Some current_item) path ~late_typedtree
          | _, _ ->
              let new_md = {md with md_type = Mty_signature newsg} in
              let new_item = Sig_module(id, Mp_present, new_md, rs, priv) in
              return_payload ~ghosts ~replace_by:(Some new_item)
                path ~paths ~late_typedtree
        end
    | _ -> None

  (* Entry point for merging *)
  let merge ~patch ~destructive env sg loc lid =
    let initial_env = env in
    let names = Longident.flatten lid.txt in
    merge_signature ~patch ~destructive initial_env env sg names loc lid

  (* merge functions *)

  (** Type constraint [sg with type lid = sdecl]

      - [sdecl] is a parse tree, it will be translated into a typed tree [tdecl]
      at the point of the constrained item (at [lid]), and returned via the
      [late_typedtree] mechanism. It is then returned along the merged
      signature *)
  let merge_type ~destructive env loc sg lid sdecl =
    let patch item s sig_env sg_for_env ~ghosts =
      match item, sdecl.ptype_kind with
      | Sig_type(id, decl, rs, priv), Ptype_abstract
        when Ident.name id = s && Typedecl.is_fixed_type sdecl ->
          let decl_row =
            let arity = List.length sdecl.ptype_params in
            {
              type_params =
                List.map (fun _ -> Btype.newgenvar()) sdecl.ptype_params;
              type_arity = arity;
              type_kind = Type_abstract Definition;
              type_private = Private;
              type_manifest = None;
              type_variance =
                List.map
                  (fun (_, (v, i)) ->
                     let (c, n) =
                       match v with
                       | Covariant -> true, false
                       | Contravariant -> false, true
                       | NoVariance -> false, false
                       | Bivariant -> true, true
                     in
                     make_variance (not n) (not c) (i = Injective)
                  )
                  sdecl.ptype_params;
              type_separability =
                Types.Separability.default_signature ~arity;
              type_loc = sdecl.ptype_loc;
              type_is_newtype = false;
              type_expansion_scope = Btype.lowest_level;
              type_attributes = [];
              type_immediate = Unknown;
              type_unboxed_default = false;
              type_uid = Uid.mk ~current_unit:(Env.get_current_unit ());
            }
          and id_row = Ident.create_local (s^"#row") in
          let initial_env =
            Env.add_type ~check:false id_row decl_row env
          in
          let sig_env = Env.add_signature sg_for_env sig_env in
          let tdecl =
            Typedecl.transl_with_constraint id ~fixed_row_path:(Pident id_row)
              ~sig_env ~sig_decl:decl ~outer_env:initial_env sdecl in
          let newdecl = tdecl.typ_type in
          let before_ghosts, row_id, after_ghosts = split_row_id s ghosts in
          check_type_decl sig_env sg_for_env sdecl.ptype_loc
            id row_id newdecl decl;
          let decl_row = {decl_row with type_params = newdecl.type_params} in
          let rs' = if rs = Trec_first then Trec_not else rs in
          let ghosts =
            List.rev_append before_ghosts
              (Sig_type(id_row, decl_row, rs', priv)::after_ghosts)
          in
          let path = Pident id in
          return_payload ~ghosts ~late_typedtree:tdecl
            ~replace_by:(Some (Sig_type(id, newdecl, rs, priv))) path

      | Sig_type(id, sig_decl, rs, priv), _
        when Ident.name id = s ->
          let sig_env = Env.add_signature sg_for_env sig_env in
          let tdecl =
            Typedecl.transl_with_constraint id
              ~sig_env ~sig_decl ~outer_env:env sdecl in
          let newdecl = tdecl.typ_type in
          let newloc = sdecl.ptype_loc in
          let before_ghosts, row_id, after_ghosts = split_row_id s ghosts in
          let ghosts = List.rev_append before_ghosts after_ghosts in
          check_type_decl sig_env sg_for_env newloc
            id row_id newdecl sig_decl;
          let path = Pident id in
          let item_opt =
            if not destructive then (Some(Sig_type(id, newdecl, rs, priv)))
            else None
          in
          return_payload ~ghosts ~late_typedtree:tdecl ~replace_by:item_opt path

      | _ -> None
    in
    (* Merging *)
    let path, paths, tdecl, sg = merge ~patch ~destructive env sg loc lid in
    (* Post processing *)
    let replace =
      match type_decl_is_alias sdecl with
      | Some lid ->
          (* if the type is an alias of [lid], replace by the definition *)
          let replacement, _ =
            try Env.find_type_by_name lid.txt env
            with Not_found -> assert false
          in
          fun s path -> Subst.Unsafe.add_type_path path replacement s
      | None ->
          (* if the type is not an alias, try to inline it *)
          let body = Option.get tdecl.typ_type.type_manifest in
          let params = tdecl.typ_type.type_params in
          if params_are_constrained params then
            raise(Error(loc, env, With_cannot_remove_constrained_type));
          fun s path ->
            Subst.Unsafe.add_type_function path ~params ~body s
    in
    let sg = post_process ~destructive loc lid env paths sg replace in
    (tdecl, (path, lid, sg))

  (** Module constraint [sg with module lid = path]

      - [md'] is the module type of the module at [path], used for equivalence
      checks
  *)
  let merge_module ~destructive env loc sg lid
      (md': Types.module_declaration) path remove_aliases =
    let aliasable = Env.is_aliasable path env in
    let patch item s sig_env sg_for_env ~ghosts =
      match item with
      | Sig_module(id, pres, md, rs, priv) when Ident.name id = s ->
          let sig_env = Env.add_signature sg_for_env sig_env in
          let real_path = Pident id in
          if destructive then
            (* Inclusion check with the strengthened definition *)
            let _ =
              Includemod.strengthened_module_decl ~loc ~mark:true
                ~aliasable sig_env md' path md in
            return ~ghosts ~replace_by:None real_path
          else
            let mty = md'.md_type in
            let mty = Mtype.scrape_for_type_of ~remove_aliases sig_env mty in
            let md'' = { md' with md_type = mty } in
            let newmd =
              Mtype.strengthen_decl ~aliasable:false sig_env md'' path in
            (* Inclusion check with the original signature *)
            let _ = Includemod.modtypes ~mark:true ~loc sig_env
                newmd.md_type md.md_type in
            return ~ghosts
              ~replace_by:(Some(Sig_module(id, pres, newmd, rs, priv)))
              real_path
      | _ -> None
    in
    let real_path,paths,_,sg = merge ~patch ~destructive env sg loc lid in
    let replace s p = Subst.Unsafe.add_module_path p path s in
    let invalid_alias = if (not aliasable) then (Some path) else None in
    let sg =
      post_process ~destructive loc lid env paths sg replace ~invalid_alias in
    real_path, lid, sg

  (** Module type constraint [sg with module type lid = mty]

      - [~approx] is used to disable equivalence checking when merging module
      types inside recursive module definitions
  *)
  let merge_modtype ?(approx=false) ~destructive env loc sg lid mty =
    let patch item s sig_env sg_for_env ~ghosts = match item with
      | Sig_modtype(id, mtd, priv)
        when Ident.name id = s ->
          (* Check for equivalence if the previous module type was not
             abstract. In approximation mode, the check is ignored *)
          let () = match mtd.mtd_type, approx with
            | Some previous_mty, false ->
                let sig_env = Env.add_signature sg_for_env sig_env in
                Includemod.check_modtype_equiv ~loc sig_env id previous_mty mty
            | _, _ -> ()
          in
          (* Create replacement item *)
          let new_item =
            if destructive then None
            else
              let mtd': modtype_declaration = {
                mtd_uid = Uid.mk ~current_unit:(Env.get_current_unit ());
                mtd_type = Some mty;
                mtd_attributes = [];
                mtd_loc = loc; }
              in Some(Sig_modtype(id, mtd', priv))
          in
          let path = Pident id in
          return ~ghosts ~replace_by:new_item path
      | _ -> None
    in
    let path,paths,_,sg = merge ~patch ~destructive env sg loc lid in
    let replace s p = Subst.Unsafe.add_modtype_path p mty s in
    let sg = post_process ~destructive loc lid env paths sg replace in
    path, lid, sg

  (** Type constraints inside a first class module type [(module sg with type
      lid = cty)] *)
  let merge_package env loc sg lid cty =
    let patch item s sig_env sg_for_env ~ghosts = match item with
      | Sig_type(id, sig_decl, rs, priv)
        when Ident.name id = s ->
          begin match sig_decl.type_manifest with
          | None -> ()
          | Some ty ->
              raise (Error(loc, sig_env, With_package_manifest (lid.txt, ty)))
          end;
          let tdecl =
            Typedecl.transl_package_constraint ~loc sig_env cty.ctyp_type
          in
          check_type_decl sig_env sg_for_env loc id None tdecl sig_decl;
          let tdecl = { tdecl with type_manifest = None } in
          let path = Pident id in
          return ~ghosts ~replace_by:(Some(Sig_type(id, tdecl, rs, priv))) path
      | _ -> None
    in
    let _, _, _, sg = merge ~patch ~destructive:false env sg loc lid in
    sg

  let check_package_with_type_constraints loc env mty constraints =
    let sg = extract_sig env loc mty in
    let sg =
      List.fold_left
        (fun sg (lid, cty) ->
           merge_package env loc sg lid cty)
        sg constraints
    in
    let scope = Ctype.create_scope () in
    Mtype.freshen ~scope (Mty_signature sg)

  let () =
    Typetexp.check_package_with_type_constraints :=
      check_package_with_type_constraints
end

(* Add recursion flags on declarations arising from a mutually recursive
   block. *)

let map_rec fn decls rem =
  match decls with
  | [] -> rem
  | d1 :: dl -> fn Trec_first d1 :: map_end (fn Trec_next) dl rem

let map_rec_type ~rec_flag fn decls rem =
  match decls with
  | [] -> rem
  | d1 :: dl ->
      let first =
        match rec_flag with
        | Recursive -> Trec_first
        | Nonrecursive -> Trec_not
      in
      fn first d1 :: map_end (fn Trec_next) dl rem

let rec map_rec_type_with_row_types ~rec_flag fn decls rem =
  match decls with
  | [] -> rem
  | d1 :: dl ->
      if Btype.is_row_name (Ident.name d1.typ_id) then
        fn Trec_not d1 :: map_rec_type_with_row_types ~rec_flag fn dl rem
      else
        map_rec_type ~rec_flag fn decls rem

(* Add type extension flags to extension constructors *)
let map_ext fn exts rem =
  match exts with
  | [] -> rem
  | d1 :: dl -> fn Text_first d1 :: map_end (fn Text_next) dl rem

(* Auxiliary for translating recursively-defined module types.
   Return a module type that approximates the shape of the given module
   type AST.  Retain only module, type, and module type
   components of signatures.  For types, retain only their arity,
   making them abstract otherwise. *)

let rec approx_modtype env smty =
  match smty.pmty_desc with
    Pmty_ident lid ->
      let path =
        Env.lookup_modtype_path ~use:false ~loc:smty.pmty_loc lid.txt env
      in
      Mty_ident path
  | Pmty_alias lid ->
      let path =
        Env.lookup_module_path ~use:false ~load:false
          ~loc:smty.pmty_loc lid.txt env
      in
      Mty_alias(path)
  | Pmty_signature ssg ->
      Mty_signature(approx_sig env ssg)
  | Pmty_functor(param, sres) ->
      let (param, newenv) =
        match param with
        | Unit -> Types.Unit, env
        | Named (param, sarg) ->
          let arg = approx_modtype env sarg in
          match param.txt with
          | None -> Types.Named (None, arg), env
          | Some name ->
            let rarg = Mtype.scrape_for_functor_arg env arg in
            let scope = Ctype.create_scope () in
            let (id, newenv) =
              Env.enter_module ~scope ~noalias:true name Mp_present rarg env
            in
            Types.Named (Some id, arg), newenv
      in
      let res = approx_modtype newenv sres in
      Mty_functor(param, res)
  | Pmty_with(sbody, constraints) ->
      (* the module type body is approximated and resolved to a signature.*)
      let approx_body = approx_modtype env sbody in
      let initial_sig = extract_sig env sbody.pmty_loc approx_body in
      (* then, the constraints are approximated and merged, instead of merged
         and approximated. For (1) type constraints, (2) module constraints and
         (3) module type constraints replacing an abstract module type, it
         should be equivalent.

         However, for module type constraints replacing a concrete module type,
         approximating the constraint and the body before merging can interact
         with the equivalence check that is done between the constraint and the
         original definition. As approximation only tries to build a skeleton of
         non-recursive module types that can be used as an under-approximation
         of the name-spaces for the typechecking phase, the equivalence check is
         disabled, allowing for ill-formed constraints to be merged. It is
         should be harmless, because the ill-formedness is caught when
         re-typechecking the module types (with the approximation in the
         environment).  *)
      Mty_signature (List.fold_left
                       (approx_constraint env) initial_sig constraints)
  | Pmty_typeof smod ->
      let (_, mty) = !type_module_type_of_fwd env smod in
      mty
  | Pmty_extension ext ->
      raise (Error_forward (Builtin_attributes.error_of_extension ext))

and approx_module_declaration env pmd =
  {
    Types.md_type = approx_modtype env pmd.pmd_type;
    md_attributes = pmd.pmd_attributes;
    md_loc = pmd.pmd_loc;
    md_uid = Uid.internal_not_actually_unique;
  }

and approx_sig env ssg =
  match ssg with
    [] -> []
  | item :: srem ->
      match item.psig_desc with
      | Psig_type (rec_flag, sdecls) ->
          let decls = Typedecl.approx_type_decl sdecls in
          let rem = approx_sig env srem in
          map_rec_type ~rec_flag
            (fun rs (id, info) -> Sig_type(id, info, rs, Exported)) decls rem
      | Psig_typesubst _ -> approx_sig env srem
      | Psig_module { pmd_name = { txt = None; _ }; _ } ->
          approx_sig env srem
      | Psig_module pmd ->
          let scope = Ctype.create_scope () in
          let md = approx_module_declaration env pmd in
          let pres =
            match md.Types.md_type with
            | Mty_alias _ -> Mp_absent
            | _ -> Mp_present
          in
          let id, newenv =
            Env.enter_module_declaration ~scope (Option.get pmd.pmd_name.txt)
              pres md env
          in
          Sig_module(id, pres, md, Trec_not, Exported) :: approx_sig newenv srem
      | Psig_modsubst pms ->
          let scope = Ctype.create_scope () in
          let _, md =
            Env.lookup_module ~use:false ~loc:pms.pms_manifest.loc
               pms.pms_manifest.txt env
          in
          let pres =
            match md.Types.md_type with
            | Mty_alias _ -> Mp_absent
            | _ -> Mp_present
          in
          let _, newenv =
            Env.enter_module_declaration ~scope pms.pms_name.txt pres md env
          in
          approx_sig newenv srem
      | Psig_recmodule sdecls ->
          let scope = Ctype.create_scope () in
          let decls =
            List.filter_map
              (fun pmd ->
                 Option.map (fun name ->
                   Ident.create_scoped ~scope name,
                   approx_module_declaration env pmd
                 ) pmd.pmd_name.txt
              )
              sdecls
          in
          let newenv =
            List.fold_left
              (fun env (id, md) -> Env.add_module_declaration ~check:false
                  id Mp_present md env)
              env decls
          in
          map_rec
            (fun rs (id, md) -> Sig_module(id, Mp_present, md, rs, Exported))
            decls
            (approx_sig newenv srem)
      | Psig_modtype d ->
          let info = approx_modtype_info env d in
          let scope = Ctype.create_scope () in
          let (id, newenv) =
            Env.enter_modtype ~scope d.pmtd_name.txt info env
          in
          Sig_modtype(id, info, Exported) :: approx_sig newenv srem
      | Psig_modtypesubst d ->
          let info = approx_modtype_info env d in
          let scope = Ctype.create_scope () in
          let (_id, newenv) =
            Env.enter_modtype ~scope d.pmtd_name.txt info env
          in
          approx_sig newenv srem
      | Psig_open sod ->
          let _, env = type_open_descr env sod in
          approx_sig env srem
      | Psig_include sincl ->
          let smty = sincl.pincl_mod in
          let mty = approx_modtype env smty in
          let scope = Ctype.create_scope () in
          let sg, newenv = Env.enter_signature ~scope
              (extract_sig env smty.pmty_loc mty) env in
          sg @ approx_sig newenv srem
      | Psig_class sdecls | Psig_class_type sdecls ->
          let decls, env = Typeclass.approx_class_declarations env sdecls in
          let rem = approx_sig env srem in
          map_rec (fun rs decl ->
            let open Typeclass in [
              Sig_class_type(decl.clsty_ty_id, decl.clsty_ty_decl, rs,
                             Exported);
              Sig_type(decl.clsty_obj_id, decl.clsty_obj_abbr, rs, Exported);
            ]
          ) decls [rem]
          |> List.flatten
      | _ ->
          approx_sig env srem

and approx_modtype_info env sinfo =
  {
   mtd_type = Option.map (approx_modtype env) sinfo.pmtd_type;
   mtd_attributes = sinfo.pmtd_attributes;
   mtd_loc = sinfo.pmtd_loc;
   mtd_uid = Uid.internal_not_actually_unique;
 }

and approx_constraint env body constr =
  match constr with
  (* type substitutions are ignored *)
  | Pwith_type _
  | Pwith_typesubst _ -> body
  (* module type substitutions are approximated then merged *)
  | Pwith_modtype (id, smty)
  | Pwith_modtypesubst (id, smty) ->
      let destructive =
        (match constr with | Pwith_modtypesubst _ -> true | _ -> false) in
      let approx_smty = approx_modtype env smty in
      let _,_,sg = Merge.merge_modtype ~approx:true ~destructive
          env smty.pmty_loc body id approx_smty in
      sg
  (* module substitutions are ignored, but checked for cyclicity *)
  | Pwith_module (_, lid') ->
      (* Lookup the module to make sure that it is not recursive.
         (GPR#1626) *)
      ignore (Env.lookup_module_path ~use:false ~load:false
                ~loc:lid'.loc lid'.txt env) ; body
  | Pwith_modsubst (_, lid') ->
      ignore (Env.lookup_module_path ~use:false ~load:false
                ~loc:lid'.loc lid'.txt env) ; body

let approx_modtype env smty =
  Warnings.without_warnings
    (fun () -> approx_modtype env smty)

(* Auxiliaries for checking the validity of name shadowing in signatures and
   structures.
   If a shadowing is valid, we also record some information (its ident,
   location where it first appears, etc) about the item that gets shadowed. *)
module Signature_names : sig
  type t

 type shadowable =
    {
      self: Ident.t;
      group: Ident.t list;
      (** group includes the element itself and all elements
                that should be removed at the same time
      *)
      loc:Location.t;
    }

  type info = [
    | `Exported
    | `From_open
    | `Shadowable of shadowable
    | `Substituted_away of Subst.Unsafe.t
  ]

  val create : unit -> t

  val check_value     : ?info:info -> t -> Location.t -> Ident.t -> unit
  val check_type      : ?info:info -> t -> Location.t -> Ident.t -> unit
  val check_typext    : ?info:info -> t -> Location.t -> Ident.t -> unit
  val check_module    : ?info:info -> t -> Location.t -> Ident.t -> unit
  val check_modtype   : ?info:info -> t -> Location.t -> Ident.t -> unit
  val check_class     : ?info:info -> t -> Location.t -> Ident.t -> unit
  val check_class_type: ?info:info -> t -> Location.t -> Ident.t -> unit

  val check_sig_item:
    ?info:info -> t -> Location.t -> Signature_group.rec_group -> unit

  val simplify: Env.t -> t -> Types.signature -> Types.signature
end = struct

  type shadowable =
    {
      self: Ident.t;
      group: Ident.t list;
      (** group includes the element itself and all elements
                that should be removed at the same time
      *)
      loc:Location.t;
    }

  type bound_info = [
    | `Exported
    | `Shadowable of shadowable
  ]

  type info = [
    | `From_open
    | `Substituted_away of Subst.Unsafe.t
    | bound_info
  ]

  type hide_reason =
    | From_open
    | Shadowed_by of Ident.t * Location.t

  type to_be_removed = {
    mutable subst: Subst.Unsafe.t;
    mutable hide: (Sig_component_kind.t * Location.t * hide_reason) Ident.Map.t;
  }

  type names_infos = (string, bound_info) Hashtbl.t

  type names = {
    values: names_infos;
    types: names_infos;
    modules: names_infos;
    modtypes: names_infos;
    typexts: names_infos;
    classes: names_infos;
    class_types: names_infos;
  }

  let new_names () = {
    values = Hashtbl.create 16;
    types = Hashtbl.create 16;
    modules = Hashtbl.create 16;
    modtypes = Hashtbl.create 16;
    typexts = Hashtbl.create 16;
    classes = Hashtbl.create 16;
    class_types = Hashtbl.create 16;
  }

  type t = {
    bound: names;
    to_be_removed: to_be_removed;
  }

  let create () = {
    bound = new_names ();
    to_be_removed = {
      subst = Subst.identity;
      hide = Ident.Map.empty;
    };
  }

  let table_for component names =
    let open Sig_component_kind in
    match component with
    | Value -> names.values
    | Type | Label | Constructor -> names.types
    | Module -> names.modules
    | Module_type -> names.modtypes
    | Extension_constructor -> names.typexts
    | Class -> names.classes
    | Class_type -> names.class_types

  let check_unsafe_subst loc env: _ result -> _ = function
    | Ok x -> x
    | Error (Subst.Unsafe.Fcm_type_substituted_away (p,_)) ->
        raise (Error (loc, env, Non_packable_local_modtype_subst p))

  let check cl t loc id (info : info) =
    let to_be_removed = t.to_be_removed in
    match info with
    | `Substituted_away s ->
        let subst =
          check_unsafe_subst loc Env.empty @@
          Subst.Unsafe.compose s to_be_removed.subst
        in
        to_be_removed.subst <- subst;
    | `From_open ->
        to_be_removed.hide <-
          Ident.Map.add id (cl, loc, From_open) to_be_removed.hide
    | #bound_info as bound_info ->
        let tbl = table_for cl t.bound in
        let name = Ident.name id in
        match Hashtbl.find_opt tbl name with
        | None -> Hashtbl.add tbl name bound_info
        | Some (`Shadowable s) ->
            Hashtbl.replace tbl name bound_info;
            let reason = Shadowed_by (id, loc) in
            List.iter (fun shadowed_id ->
            to_be_removed.hide <-
              Ident.Map.add shadowed_id (cl, s.loc, reason)
                to_be_removed.hide
              ) s.group
        | Some `Exported ->
            raise(Error(loc, Env.empty, Repeated_name(cl, name)))

  let check_value ?info t loc id =
    let info =
      match info with
      | Some i -> i
      | None -> `Shadowable {self=id; group=[id]; loc}
    in
    check Sig_component_kind.Value t loc id info
  let check_type ?(info=`Exported) t loc id =
    check Sig_component_kind.Type t loc id info
  let check_module ?(info=`Exported) t loc id =
    check Sig_component_kind.Module t loc id info
  let check_modtype ?(info=`Exported) t loc id =
    check Sig_component_kind.Module_type t loc id info
  let check_typext ?(info=`Exported) t loc id =
    check Sig_component_kind.Extension_constructor t loc id info
  let check_class ?(info=`Exported) t loc id =
    check Sig_component_kind.Class t loc id info
  let check_class_type ?(info=`Exported) t loc id =
    check Sig_component_kind.Class_type t loc id info

  let classify =
    let open Sig_component_kind in
    function
    | Sig_type(id, _, _, _) -> Type, id
    | Sig_module(id, _, _, _, _) -> Module, id
    | Sig_modtype(id, _, _) -> Module_type, id
    | Sig_typext(id, _, _, _) -> Extension_constructor, id
    | Sig_value (id, _, _) -> Value, id
    | Sig_class (id, _, _, _) -> Class, id
    | Sig_class_type (id, _, _, _) -> Class_type, id

  let check_item ?info names loc kind id ids =
    let info =
      match info with
      | None -> `Shadowable {self=id; group=ids; loc}
      | Some i -> i
    in
    check kind names loc id info

  let check_sig_item ?info names loc (item:Signature_group.rec_group) =
    let check ?info names loc item =
      let all = List.map classify (Signature_group.flatten item) in
      let group = List.map snd all in
      List.iter (fun (kind,id) -> check_item ?info names loc kind id group)
        all
    in
    (* we can ignore x.pre_ghosts: they are eliminated by strengthening, and
       thus never appear in includes *)
     List.iter (check ?info names loc) (Signature_group.rec_items item.group)

  (* We usually require name uniqueness of signature components (e.g. types,
     modules, etc), however in some situation reusing the name is allowed: if
     the component is a value or an extension, or if the name is introduced by
     an include.
     When there are multiple specifications of a component with the same name,
     we try to keep only the last (rightmost) one, removing all references to
     the previous ones from the signature.
     If some reference cannot be removed, then we error out with
     [Cannot_hide_id].
  *)
  let simplify env t sg =
    let to_remove = t.to_be_removed in
    let ids_to_remove =
      Ident.Map.fold (fun id (kind,  _, _) lst ->
        if Sig_component_kind.can_appear_in_types kind then
          id :: lst
        else
          lst
      ) to_remove.hide []
    in
    let simplify_item (component: Types.signature_item) =
      let user_kind, user_id, user_loc =
        let open Sig_component_kind in
        match component with
        | Sig_value(id, v, _) -> Value, id, v.val_loc
        | Sig_type (id, td, _, _) -> Type, id, td.type_loc
        | Sig_typext (id, te, _, _) -> Extension_constructor, id, te.ext_loc
        | Sig_module (id, _, md, _, _) -> Module, id, md.md_loc
        | Sig_modtype (id, mtd, _) -> Module_type, id, mtd.mtd_loc
        | Sig_class (id, c, _, _) -> Class, id, c.cty_loc
        | Sig_class_type (id, ct, _, _) -> Class_type, id, ct.clty_loc
      in
      if Ident.Map.mem user_id to_remove.hide then
        None
      else begin
        let component =
          if to_remove.subst == Subst.identity then
            component
          else
            check_unsafe_subst user_loc env @@
            Subst.Unsafe.signature_item Keep to_remove.subst component
        in
        let component =
          match ids_to_remove with
          | [] -> component
          | ids ->
            try Mtype.nondep_sig_item env ids component with
            | Ctype.Nondep_cannot_erase removed_item_id ->
              let (removed_item_kind, removed_item_loc, reason) =
                Ident.Map.find removed_item_id to_remove.hide
              in
              let err_loc, hiding_error =
                match reason with
                | From_open ->
                  removed_item_loc,
                  Appears_in_signature {
                    opened_item_kind = removed_item_kind;
                    opened_item_id = removed_item_id;
                    user_id;
                    user_kind;
                    user_loc;
                  }
                | Shadowed_by (shadower_id, shadower_loc) ->
                  shadower_loc,
                  Illegal_shadowing {
                    shadowed_item_kind = removed_item_kind;
                    shadowed_item_id = removed_item_id;
                    shadowed_item_loc = removed_item_loc;
                    shadower_id;
                    user_id;
                    user_kind;
                    user_loc;
                  }
              in
              raise (Error(err_loc, env, Cannot_hide_id hiding_error))
        in
        Some component
      end
    in
    List.filter_map simplify_item sg
end

(* Check and translate a module type expression *)

let transl_modtype_longident loc env lid =
  Env.lookup_modtype_path ~loc lid env

let transl_module_alias loc env lid =
  Env.lookup_module_path ~load:false ~loc lid env

let mkmty desc typ env loc attrs =
  let mty = {
    mty_desc = desc;
    mty_type = typ;
    mty_loc = loc;
    mty_env = env;
    mty_attributes = attrs;
    } in
  Cmt_format.add_saved_type (Cmt_format.Partial_module_type mty);
  mty

let mksig desc env loc =
  let sg = { sig_desc = desc; sig_loc = loc; sig_env = env } in
  Cmt_format.add_saved_type (Cmt_format.Partial_signature_item sg);
  sg

(* let signature sg = List.map (fun item -> item.sig_type) sg *)

let rec transl_modtype env smty =
  Builtin_attributes.warning_scope smty.pmty_attributes
    (fun () -> transl_modtype_aux env smty)

and transl_modtype_functor_arg env sarg =
  let mty = transl_modtype env sarg in
  {mty with mty_type = Mtype.scrape_for_functor_arg env mty.mty_type}

and transl_modtype_aux env smty =
  let loc = smty.pmty_loc in
  match smty.pmty_desc with
    Pmty_ident lid ->
      let path = transl_modtype_longident loc env lid.txt in
      mkmty (Tmty_ident (path, lid)) (Mty_ident path) env loc
        smty.pmty_attributes
  | Pmty_alias lid ->
      let path = transl_module_alias loc env lid.txt in
      mkmty (Tmty_alias (path, lid)) (Mty_alias path) env loc
        smty.pmty_attributes
  | Pmty_signature ssg ->
      let sg = transl_signature env ssg in
      mkmty (Tmty_signature sg) (Mty_signature sg.sig_type) env loc
        smty.pmty_attributes
  | Pmty_functor(sarg_opt, sres) ->
      let t_arg, ty_arg, newenv =
        match sarg_opt with
        | Unit -> Unit, Types.Unit, env
        | Named (param, sarg) ->
          let arg = transl_modtype_functor_arg env sarg in
          let (id, newenv) =
            match param.txt with
            | None -> None, env
            | Some name ->
              let scope = Ctype.create_scope () in
              let id, newenv =
                let arg_md =
                  { md_type = arg.mty_type;
                    md_attributes = [];
                    md_loc = param.loc;
                    md_uid = Uid.mk ~current_unit:(Env.get_current_unit ());
                  }
                in
                Env.enter_module_declaration ~scope ~noalias:true
                  name Mp_present arg_md env
              in
              Some id, newenv
          in
          Named (id, param, arg), Types.Named (id, arg.mty_type), newenv
      in
      let res = transl_modtype newenv sres in
      mkmty (Tmty_functor (t_arg, res))
        (Mty_functor(ty_arg, res.mty_type)) env loc
        smty.pmty_attributes
  | Pmty_with(sbody, constraints) ->
      let body = transl_modtype env sbody in
      let init_sg = extract_sig env sbody.pmty_loc body.mty_type in
      let remove_aliases =
        Builtin_attributes.has_remove_aliases smty.pmty_attributes
      in
      let (rev_tcstrs, final_sg) =
        List.fold_left (transl_with ~loc:smty.pmty_loc env remove_aliases)
        ([],init_sg) constraints in
      let scope = Ctype.create_scope () in
      mkmty (Tmty_with ( body, List.rev rev_tcstrs))
        (Mtype.freshen ~scope (Mty_signature final_sg)) env loc
        smty.pmty_attributes
  | Pmty_typeof smod ->
      let env = Env.in_signature false env in
      let tmty, mty = !type_module_type_of_fwd env smod in
      mkmty (Tmty_typeof tmty) mty env loc smty.pmty_attributes
  | Pmty_extension ext ->
      raise (Error_forward (Builtin_attributes.error_of_extension ext))

and transl_with ~loc env remove_aliases (rev_tcstrs, sg) constr =
  let destructive = match constr with
    | Pwith_typesubst _ | Pwith_modsubst _ | Pwith_modtypesubst _ -> true
    | _ -> false
  in
  let constr, (path, lid, sg) = match constr with
    | Pwith_type (l, decl)
    | Pwith_typesubst (l, decl) ->
        let tdecl, merge_res =
          Merge.merge_type ~destructive env loc sg l decl
        in
        let constr = if destructive then
            (Twith_typesubst tdecl)
          else
            (Twith_type tdecl)
        in
        (constr, merge_res)

    | Pwith_module (l, l')
    | Pwith_modsubst (l,l') ->
        let path, md = Env.lookup_module ~loc l'.txt env in
        let constr = if destructive then
            (Twith_modsubst (path, l'))
          else
            (Twith_module (path, l'))
        in
        (constr,
         Merge.merge_module ~destructive env loc sg l md path remove_aliases)

    | Pwith_modtype (l,smty)
    | Pwith_modtypesubst (l,smty) ->
        let tmty = transl_modtype env smty in
        let constr = if destructive then
            (Twith_modtypesubst tmty)
          else
            (Twith_modtype tmty)
        in
        (constr, Merge.merge_modtype ~destructive env loc sg l tmty.mty_type)

  in
  ((path, lid, constr) :: rev_tcstrs, sg)


and transl_signature env sg =
  let names = Signature_names.create () in
  let rec transl_sig env sg =
    match sg with
      [] -> [], [], env
    | item :: srem ->
        let loc = item.psig_loc in
        match item.psig_desc with
        | Psig_value sdesc ->
            let (tdesc, newenv) =
              Typedecl.transl_value_decl env item.psig_loc sdesc
            in
            Signature_names.check_value names tdesc.val_loc tdesc.val_id;
            let (trem,rem, final_env) = transl_sig newenv srem in
            mksig (Tsig_value tdesc) env loc :: trem,
            Sig_value(tdesc.val_id, tdesc.val_val, Exported) :: rem,
              final_env
        | Psig_type (rec_flag, sdecls) ->
            let (decls, newenv, _) =
              Typedecl.transl_type_decl env rec_flag sdecls
            in
            List.iter (fun td ->
              Signature_names.check_type names td.typ_loc td.typ_id;
            ) decls;
            let (trem, rem, final_env) = transl_sig newenv srem in
            let sg =
              map_rec_type_with_row_types ~rec_flag
                (fun rs td -> Sig_type(td.typ_id, td.typ_type, rs, Exported))
                decls rem
            in
            mksig (Tsig_type (rec_flag, decls)) env loc :: trem,
            sg,
            final_env
        | Psig_typesubst sdecls ->
            let (decls, newenv, _) =
              Typedecl.transl_type_decl env Nonrecursive sdecls
            in
            List.iter (fun td ->
              if td.typ_kind <> Ttype_abstract || td.typ_manifest = None ||
                 td.typ_private = Private
              then
                raise (Error (td.typ_loc, env, Invalid_type_subst_rhs));
              let params = td.typ_type.type_params in
              if params_are_constrained params
              then raise(Error(loc, env, With_cannot_remove_constrained_type));
              let info =
                  let subst =
                    Subst.Unsafe.add_type_function (Pident td.typ_id)
                      ~params
                      ~body:(Option.get td.typ_type.type_manifest)
                      Subst.identity
                  in
                  Some (`Substituted_away subst)
              in
              Signature_names.check_type ?info names td.typ_loc td.typ_id
            ) decls;
            let (trem, rem, final_env) = transl_sig newenv srem in
            let sg = rem
            in
            mksig (Tsig_typesubst decls) env loc :: trem,
            sg,
            final_env
        | Psig_typext styext ->
            let (tyext, newenv, _shapes) =
              Typedecl.transl_type_extension false env item.psig_loc styext
            in
            let constructors = tyext.tyext_constructors in
            List.iter (fun ext ->
              Signature_names.check_typext names ext.ext_loc ext.ext_id
            ) constructors;
            let (trem, rem, final_env) = transl_sig newenv srem in
              mksig (Tsig_typext tyext) env loc :: trem,
              map_ext (fun es ext ->
                Sig_typext(ext.ext_id, ext.ext_type, es, Exported)
              ) constructors rem,
              final_env
        | Psig_exception sext ->
            let (ext, newenv, _s) = Typedecl.transl_type_exception env sext in
            let constructor = ext.tyexn_constructor in
            Signature_names.check_typext names constructor.ext_loc
              constructor.ext_id;
            let (trem, rem, final_env) = transl_sig newenv srem in
            mksig (Tsig_exception ext) env loc :: trem,
            Sig_typext(constructor.ext_id,
                       constructor.ext_type,
                       Text_exception,
                       Exported) :: rem,
            final_env
        | Psig_module pmd ->
            let scope = Ctype.create_scope () in
            let tmty =
              Builtin_attributes.warning_scope pmd.pmd_attributes
                (fun () -> transl_modtype env pmd.pmd_type)
            in
            let pres =
              match tmty.mty_type with
              | Mty_alias p ->
                  if not (Env.is_aliasable p env) then
                    raise (Error (pmd.pmd_loc, env, Cannot_alias p));
                  Mp_absent
              | _ -> Mp_present
            in
            let md = {
              md_type=tmty.mty_type;
              md_attributes=pmd.pmd_attributes;
              md_loc=pmd.pmd_loc;
              md_uid = Uid.mk ~current_unit:(Env.get_current_unit ());
            }
            in
            let id, newenv =
              match pmd.pmd_name.txt with
              | None -> None, env
              | Some name ->
                let id, newenv =
                  Env.enter_module_declaration ~scope name pres md env
                in
                Signature_names.check_module names pmd.pmd_name.loc id;
                Some id, newenv
            in
            let (trem, rem, final_env) = transl_sig newenv srem in
            mksig (Tsig_module {md_id=id; md_name=pmd.pmd_name;
                                md_uid=md.md_uid; md_presence=pres;
                                md_type=tmty; md_loc=pmd.pmd_loc;
                                md_attributes=pmd.pmd_attributes})
              env loc :: trem,
            (match id with
             | None -> rem
             | Some id -> Sig_module(id, pres, md, Trec_not, Exported) :: rem),
            final_env
        | Psig_modsubst pms ->
            let scope = Ctype.create_scope () in
            let path, md =
              Env.lookup_module ~loc:pms.pms_manifest.loc
                pms.pms_manifest.txt env
            in
            let aliasable = Env.is_aliasable path env in
            let md =
              if not aliasable then
                md
              else
                { md_type = Mty_alias path;
                  md_attributes = pms.pms_attributes;
                  md_loc = pms.pms_loc;
                  md_uid = Uid.mk ~current_unit:(Env.get_current_unit ());
                }
            in
            let pres =
              match md.md_type with
              | Mty_alias _ -> Mp_absent
              | _ -> Mp_present
            in
            let id, newenv =
              Env.enter_module_declaration ~scope pms.pms_name.txt pres md env
            in
            let info =
              `Substituted_away (Subst.add_module id path Subst.identity)
            in
            Signature_names.check_module ~info names pms.pms_name.loc id;
            let (trem, rem, final_env) = transl_sig newenv srem in
            mksig (Tsig_modsubst {ms_id=id; ms_name=pms.pms_name;
                                  ms_uid=md.md_uid; ms_manifest=path;
                                  ms_txt=pms.pms_manifest; ms_loc=pms.pms_loc;
                                  ms_attributes=pms.pms_attributes})
              env loc :: trem,
            rem,
            final_env
        | Psig_recmodule sdecls ->
            let (tdecls, newenv) =
              transl_recmodule_modtypes env sdecls in
            let decls =
              List.filter_map (fun (md, uid, _) ->
                match md.md_id with
                | None -> None
                | Some id -> Some (id, md, uid)
              ) tdecls
            in
            List.iter (fun (id, md, _uid) ->
              Signature_names.check_module names md.md_loc id;
            ) decls;
            let (trem, rem, final_env) = transl_sig newenv srem in
            mksig (Tsig_recmodule (List.map (fun (md, _, _) -> md) tdecls))
              env loc :: trem,
            map_rec (fun rs (id, md, uid) ->
                let d = {Types.md_type = md.md_type.mty_type;
                         md_attributes = md.md_attributes;
                         md_loc = md.md_loc;
                         md_uid = uid;
                        } in
                Sig_module(id, Mp_present, d, rs, Exported))
              decls rem,
            final_env
        | Psig_modtype pmtd ->
            let newenv, mtd, decl = transl_modtype_decl env pmtd in
            Signature_names.check_modtype names pmtd.pmtd_loc mtd.mtd_id;
            let (trem, rem, final_env) = transl_sig newenv srem in
            mksig (Tsig_modtype mtd) env loc :: trem,
            Sig_modtype (mtd.mtd_id, decl, Exported) :: rem,
            final_env
        | Psig_modtypesubst pmtd ->
            let newenv, mtd, _decl = transl_modtype_decl env pmtd in
            let info =
              let mty = match mtd.mtd_type with
                | Some tmty -> tmty.mty_type
                | None ->
                    (* parsetree invariant, see Ast_invariants *)
                    assert false
              in
              let subst =
                Subst.Unsafe.add_modtype mtd.mtd_id mty Subst.identity in
              `Substituted_away subst
            in
            Signature_names.check_modtype ~info names pmtd.pmtd_loc mtd.mtd_id;
            let (trem, rem, final_env) = transl_sig newenv srem in
            mksig (Tsig_modtypesubst mtd) env loc :: trem,
            rem,
            final_env
        | Psig_open sod ->
            let (od, newenv) = type_open_descr env sod in
            let (trem, rem, final_env) = transl_sig newenv srem in
            mksig (Tsig_open od) env loc :: trem,
            rem, final_env
        | Psig_include sincl ->
            let smty = sincl.pincl_mod in
            let tmty =
              Builtin_attributes.warning_scope sincl.pincl_attributes
                (fun () -> transl_modtype env smty)
            in
            let mty = tmty.mty_type in
            let scope = Ctype.create_scope () in
            let sg, newenv = Env.enter_signature ~scope
                       (extract_sig env smty.pmty_loc mty) env in
            Signature_group.iter
              (Signature_names.check_sig_item names item.psig_loc)
              sg;
            let incl =
              { incl_mod = tmty;
                incl_type = sg;
                incl_attributes = sincl.pincl_attributes;
                incl_loc = sincl.pincl_loc;
              }
            in
            let (trem, rem, final_env) = transl_sig newenv srem  in
            mksig (Tsig_include incl) env loc :: trem,
            sg @ rem,
            final_env
        | Psig_class cl ->
            let (classes, newenv) = Typeclass.class_descriptions env cl in
            List.iter (fun cls ->
              let open Typeclass in
              let loc = cls.cls_id_loc.Location.loc in
              Signature_names.check_type names loc cls.cls_obj_id;
              Signature_names.check_class names loc cls.cls_id;
              Signature_names.check_class_type names loc cls.cls_ty_id;
            ) classes;
            let (trem, rem, final_env) = transl_sig newenv srem in
            let sg =
              map_rec (fun rs cls ->
                let open Typeclass in
                [Sig_class(cls.cls_id, cls.cls_decl, rs, Exported);
                 Sig_class_type(cls.cls_ty_id, cls.cls_ty_decl, rs, Exported);
                 Sig_type(cls.cls_obj_id, cls.cls_obj_abbr, rs, Exported)
                ]
              ) classes [rem]
              |> List.flatten
            in
            let typedtree =
              mksig (Tsig_class
                       (List.map (fun decr ->
                          decr.Typeclass.cls_info) classes)) env loc
              :: trem
            in
            typedtree, sg, final_env
        | Psig_class_type cl ->
            let (classes, newenv) = Typeclass.class_type_declarations env cl in
            List.iter (fun decl ->
              let open Typeclass in
              let loc = decl.clsty_id_loc.Location.loc in
              Signature_names.check_class_type names loc decl.clsty_ty_id;
              Signature_names.check_type names loc decl.clsty_obj_id;
            ) classes;
            let (trem,rem, final_env) = transl_sig newenv srem in
            let sg =
              map_rec (fun rs decl ->
                let open Typeclass in
                [Sig_class_type(decl.clsty_ty_id, decl.clsty_ty_decl, rs,
                                Exported);
                 Sig_type(decl.clsty_obj_id, decl.clsty_obj_abbr, rs, Exported);
                ]
              ) classes [rem]
              |> List.flatten
            in
            let typedtree =
              mksig
                (Tsig_class_type
                   (List.map (fun decl -> decl.Typeclass.clsty_info) classes))
                env loc
              :: trem
            in
            typedtree, sg, final_env
        | Psig_attribute x ->
            Builtin_attributes.warning_attribute x;
            let (trem,rem, final_env) = transl_sig env srem in
            mksig (Tsig_attribute x) env loc :: trem, rem, final_env
        | Psig_extension (ext, _attrs) ->
            raise (Error_forward (Builtin_attributes.error_of_extension ext))
  in
  let previous_saved_types = Cmt_format.get_saved_types () in
  Builtin_attributes.warning_scope []
    (fun () ->
       let (trem, rem, final_env) = transl_sig (Env.in_signature true env) sg in
       let rem = Signature_names.simplify final_env names rem in
       let sg =
         { sig_items = trem; sig_type = rem; sig_final_env = final_env }
       in
       Cmt_format.set_saved_types
         ((Cmt_format.Partial_signature sg) :: previous_saved_types);
       sg
    )

and transl_modtype_decl env pmtd =
  Builtin_attributes.warning_scope pmtd.pmtd_attributes
    (fun () -> transl_modtype_decl_aux env pmtd)

and transl_modtype_decl_aux env
    {pmtd_name; pmtd_type; pmtd_attributes; pmtd_loc} =
  let tmty =
    Option.map (transl_modtype (Env.in_signature true env)) pmtd_type
  in
  let decl =
    {
     Types.mtd_type=Option.map (fun t -> t.mty_type) tmty;
     mtd_attributes=pmtd_attributes;
     mtd_loc=pmtd_loc;
     mtd_uid = Uid.mk ~current_unit:(Env.get_current_unit ());
    }
  in
  let scope = Ctype.create_scope () in
  let (id, newenv) = Env.enter_modtype ~scope pmtd_name.txt decl env in
  let mtd =
    {
     mtd_id=id;
     mtd_name=pmtd_name;
     mtd_uid=decl.mtd_uid;
     mtd_type=tmty;
     mtd_attributes=pmtd_attributes;
     mtd_loc=pmtd_loc;
    }
  in
  newenv, mtd, decl

and transl_recmodule_modtypes env sdecls =
  let make_env curr =
    List.fold_left (fun env (id_shape, _, md, _) ->
      Option.fold ~none:env ~some:(fun (id, shape) ->
        Env.add_module_declaration ~check:true ~shape ~noalias:true
          id Mp_present md env
      ) id_shape
    ) env curr
  in
  let transition env_c curr =
    List.map2
      (fun pmd (id_shape, id_loc, md, _) ->
        let tmty =
          Builtin_attributes.warning_scope pmd.pmd_attributes
            (fun () -> transl_modtype env_c pmd.pmd_type)
        in
        let md = { md with Types.md_type = tmty.mty_type } in
        (id_shape, id_loc, md, tmty))
      sdecls curr in
  let map_mtys curr =
    List.filter_map
      (fun (id_shape, _, md, _) ->
         Option.map (fun (id, _) -> (id, md)) id_shape)
      curr
  in
  let scope = Ctype.create_scope () in
  let ids =
    List.map (fun x -> Option.map (Ident.create_scoped ~scope) x.pmd_name.txt)
      sdecls
  in
  let approx_env container =
    List.fold_left
      (fun env ->
         Option.fold ~none:env ~some:(fun id -> (* cf #5965 *)
           Env.enter_unbound_module (Ident.name id)
             (Mod_unbound_illegal_recursion
                { container; unbound = Ident.name id })
             env
         ))
      env ids
  in
  let init =
    List.map2
      (fun id pmd ->
         let md_uid = Uid.mk ~current_unit:(Env.get_current_unit ()) in
         let md =
           { md_type =
               approx_modtype (approx_env pmd.pmd_name.txt) pmd.pmd_type;
             md_loc = pmd.pmd_loc;
             md_attributes = pmd.pmd_attributes;
             md_uid }
         in
         let id_shape =
           Option.map (fun id -> id, Shape.var md_uid id) id
         in
         (id_shape, pmd.pmd_name, md, ()))
      ids sdecls
  in
  let env0 = make_env init in
  let dcl1 =
    Warnings.without_warnings
      (fun () -> transition env0 init)
  in
  let env1 = make_env dcl1 in
  check_recmod_typedecls env1 (map_mtys dcl1);
  let dcl2 = transition env1 dcl1 in
(*
  List.iter
    (fun (id, mty) ->
      Format.printf "%a: %a@." Printtyp.ident id Printtyp.modtype mty)
    dcl2;
*)
  let env2 = make_env dcl2 in
  check_recmod_typedecls env2 (map_mtys dcl2);
  let dcl2 =
    List.map2 (fun pmd (id_shape, id_loc, md, mty) ->
      let tmd =
        {md_id=Option.map fst id_shape; md_name=id_loc; md_type=mty;
         md_uid=md.Types.md_uid; md_presence=Mp_present;
         md_loc=pmd.pmd_loc;
         md_attributes=pmd.pmd_attributes}
      in
      tmd, md.Types.md_uid, Option.map snd id_shape
    ) sdecls dcl2
  in
  (dcl2, env2)

(* Try to convert a module expression to a module path. *)

exception Not_a_path

let rec path_of_module mexp =
  match mexp.mod_desc with
  | Tmod_ident (p,_) -> p
  | Tmod_apply(funct, arg, _coercion) when !Clflags.applicative_functors ->
      Papply(path_of_module funct, path_of_module arg)
  | Tmod_constraint (mexp, _, _, _) ->
      path_of_module mexp
  | (Tmod_structure _ | Tmod_functor _ | Tmod_apply_unit _ | Tmod_unpack _ |
    Tmod_apply _) ->
    raise Not_a_path

let path_of_module mexp =
 try Some (path_of_module mexp) with Not_a_path -> None

(* Check that all core type schemes in a structure
   do not contain non-generalized type variable *)

let rec nongen_modtype env = function
    Mty_ident _ -> None
  | Mty_alias _ -> None
  | Mty_signature sg ->
      let env = Env.add_signature sg env in
      List.find_map (nongen_signature_item env) sg
  | Mty_functor(arg_opt, body) ->
      let env =
        match arg_opt with
        | Unit
        | Named (None, _) -> env
        | Named (Some id, param) ->
            Env.add_module ~noalias:true id Mp_present param env
      in
      nongen_modtype env body

and nongen_signature_item env = function
  | Sig_value(_id, desc, _) ->
      Ctype.nongen_vars_in_schema env desc.val_type
      |> Option.map (fun vars -> (vars, desc))
  | Sig_module(_id, _, md, _, _) -> nongen_modtype env md.md_type
  | _ -> None

let check_nongen_modtype env loc mty =
  nongen_modtype env mty
  |> Option.iter (fun (vars, item) ->
      let vars = Btype.TypeSet.elements vars in
      let error =
        Non_generalizable_module { vars; item; mty }
      in
      raise(Error(loc, env, error))
    )

let check_nongen_signature_item env sig_item =
  match sig_item with
    Sig_value(_id, vd, _) ->
      Ctype.nongen_vars_in_schema env vd.val_type
      |> Option.iter (fun vars ->
          let vars = Btype.TypeSet.elements vars in
          let error =
            Non_generalizable { vars; expression = vd.val_type }
          in
          raise (Error (vd.val_loc, env, error))
        )
  | Sig_module (_id, _, md, _, _) ->
      check_nongen_modtype env md.md_loc md.md_type
  | _ -> ()

let check_nongen_signature env sg =
  List.iter (check_nongen_signature_item env) sg

(* Helpers for typing recursive modules *)

let anchor_submodule name anchor =
  match anchor, name with
  | None, _
  | _, None ->
      None
  | Some p, Some name ->
      Some(Pdot(p, name))

let anchor_recmodule = Option.map (fun id -> Pident id)

let enrich_type_decls anchor decls oldenv newenv =
  match anchor with
    None -> newenv
  | Some p ->
      List.fold_left
        (fun e info ->
          let id = info.typ_id in
          let info' =
            Mtype.enrich_typedecl oldenv (Pdot(p, Ident.name id))
              id info.typ_type
          in
            Env.add_type ~check:true id info' e)
        oldenv decls

let enrich_module_type anchor name mty env =
  match anchor, name with
  | None, _
  | _, None ->
      mty
  | Some p, Some name ->
      Mtype.enrich_modtype env (Pdot(p, name)) mty

let check_recmodule_inclusion env bindings =
  (* PR#4450, PR#4470: consider
        module rec X : DECL = MOD  where MOD has inferred type ACTUAL
     The "natural" typing condition
        E, X: ACTUAL |- ACTUAL <: DECL
     leads to circularities through manifest types.
     Instead, we "unroll away" the potential circularities a finite number
     of times.  The (weaker) condition we implement is:
        E, X: DECL,
           X1: ACTUAL,
           X2: ACTUAL{X <- X1}/X1
           ...
           Xn: ACTUAL{X <- X(n-1)}/X(n-1)
        |- ACTUAL{X <- Xn}/Xn <: DECL{X <- Xn}
     so that manifest types rooted at X(n+1) are expanded in terms of X(n),
     avoiding circularities.  The strengthenings ensure that
     Xn.t = X(n-1).t = ... = X2.t = X1.t.
     N can be chosen arbitrarily; larger values of N result in more
     recursive definitions being accepted.  A good choice appears to be
     the number of mutually recursive declarations. *)

  let subst_and_strengthen env scope s id mty =
    let mty = Subst.modtype (Rescope scope) s mty in
    match id with
    | None -> mty
    | Some id ->
        Mtype.strengthen ~aliasable:false env mty
          (Subst.module_path s (Pident id))
  in

  let rec check_incl first_time n env s =
    let scope = Ctype.create_scope () in
    if n > 0 then begin
      (* Generate fresh names Y_i for the rec. bound module idents X_i *)
      let bindings1 =
        List.map
          (fun (id, _name, _mty_decl, _modl,
                mty_actual, _attrs, _loc, shape, _uid) ->
             let ids =
               Option.map
                 (fun id -> (id, Ident.create_scoped ~scope (Ident.name id))) id
             in
             (ids, mty_actual, shape))
          bindings in
      (* Enter the Y_i in the environment with their actual types substituted
         by the input substitution s *)
      let env' =
        List.fold_left
          (fun env (ids, mty_actual, shape) ->
             match ids with
             | None -> env
             | Some (id, id') ->
               let mty_actual' =
                 if first_time
                 then mty_actual
                 else subst_and_strengthen env scope s (Some id) mty_actual
               in
               Env.add_module ~noalias:false ~shape id'
                 Mp_present mty_actual' env)
          env bindings1 in
      (* Build the output substitution Y_i <- X_i *)
      let s' =
        List.fold_left
          (fun s (ids, _mty_actual, _shape) ->
             match ids with
             | None -> s
             | Some (id, id') -> Subst.add_module id (Pident id') s)
          Subst.identity bindings1 in
      (* Recurse with env' and s' *)
      check_incl false (n-1) env' s'
    end else begin
      (* Base case: check inclusion of s(mty_actual) in s(mty_decl)
         and insert coercion if needed *)
      let check_inclusion
            (id, name, mty_decl, modl, mty_actual, attrs, loc, shape, uid) =
        let mty_decl' = Subst.modtype (Rescope scope) s mty_decl.mty_type
        and mty_actual' = subst_and_strengthen env scope s id mty_actual in
        let coercion, shape =
          try
            Includemod.modtypes_constraint ~shape
              ~loc:modl.mod_loc ~mark:true
              env mty_actual' mty_decl'
          with Includemod.Error msg ->
            raise(Error(modl.mod_loc, env, Not_included msg)) in
        let modl' =
            { mod_desc = Tmod_constraint(modl, mty_decl.mty_type,
                Tmodtype_explicit mty_decl, coercion);
              mod_type = mty_decl.mty_type;
              mod_env = env;
              mod_loc = modl.mod_loc;
              mod_attributes = [];
             } in
        let mb =
          {
            mb_id = id;
            mb_name = name;
            mb_uid = uid;
            mb_presence = Mp_present;
            mb_expr = modl';
            mb_attributes = attrs;
            mb_loc = loc;
          }
        in
        mb, shape, uid
      in
      List.map check_inclusion bindings
    end
  in check_incl true (List.length bindings) env Subst.identity

(* Helper for unpack *)

let rec package_constraints_sig env loc sg constrs =
  List.map
    (function
      | Sig_type (id, ({type_params=[]} as td), rs, priv)
        when List.mem_assoc [Ident.name id] constrs ->
          let ty = List.assoc [Ident.name id] constrs in
          let td = {td with type_manifest = Some ty} in
          let type_immediate = Typedecl_immediacy.compute_decl env td in
          Sig_type (id, {td with type_immediate}, rs, priv)
      | Sig_module (id, pres, md, rs, priv) ->
          let rec aux = function
            | (m :: ((_ :: _) as l), t) :: rest when m = Ident.name id ->
                (l, t) :: aux rest
            | _ :: rest -> aux rest
            | [] -> []
          in
          let md =
            {md with
             md_type = package_constraints env loc md.md_type (aux constrs)
            }
          in
          Sig_module (id, pres, md, rs, priv)
      | item -> item
    )
    sg

and package_constraints env loc mty constrs =
  if constrs = [] then mty
  else begin
    match Mtype.scrape env mty with
    | Mty_signature sg ->
        Mty_signature (package_constraints_sig env loc sg constrs)
    | Mty_functor _ | Mty_alias _ -> assert false
    | Mty_ident p -> raise(Error(loc, env, Cannot_scrape_package_type p))
  end

let modtype_of_package env loc pack =
  (* We call Ctype.duplicate_type to ensure that the types being added to the
     module type are at generic_level. *)
  let mty =
    package_constraints env loc (Mty_ident pack.pack_path)
      (List.map (fun (n, t) -> n, Ctype.duplicate_type t) pack.pack_cstrs)
  in
  Subst.modtype Keep Subst.identity mty

let package_subtype env pack1 pack2 =
  let mkmty pack =
    let fl =
      List.filter (fun (_n,t) -> Ctype.closed_type_expr t) pack.pack_cstrs in
    modtype_of_package env Location.none {pack with pack_cstrs = fl}
  in
  match mkmty pack1, mkmty pack2 with
  | exception Error(_, _, Cannot_scrape_package_type r) ->
      Result.Error (Errortrace.Package_cannot_scrape r)
  | mty1, mty2 ->
    let loc = Location.none in
    match Includemod.modtypes ~loc ~mark:true env mty1 mty2 with
    | Tcoerce_none -> Ok ()
    | c ->
        let msg =
          Includemod_errorprinter.coercion_in_package_subtype env mty1 c
        in
        Result.Error (Errortrace.Package_coercion msg)
    | exception Includemod.Error e ->
        let msg = doc_printf "%a" Includemod_errorprinter.err_msgs e in
        Result.Error (Errortrace.Package_inclusion msg)

let () = Ctype.package_subtype := package_subtype

let wrap_constraint_package env mark arg mty explicit =
  let mty1 = Subst.modtype Keep Subst.identity arg.mod_type in
  let mty2 = Subst.modtype Keep Subst.identity mty in
  let coercion =
    try
      Includemod.modtypes ~loc:arg.mod_loc env ~mark mty1 mty2
    with Includemod.Error msg ->
      raise(Error(arg.mod_loc, env, Not_included msg)) in
  { mod_desc = Tmod_constraint(arg, mty, explicit, coercion);
    mod_type = mty;
    mod_env = env;
    mod_attributes = [];
    mod_loc = arg.mod_loc }

let wrap_constraint_with_shape env mark arg mty
  shape explicit =
  let coercion, shape =
    try
      Includemod.modtypes_constraint ~shape ~loc:arg.mod_loc env ~mark
        arg.mod_type mty
    with Includemod.Error msg ->
      raise(Error(arg.mod_loc, env, Not_included msg)) in
  { mod_desc = Tmod_constraint(arg, mty, explicit, coercion);
    mod_type = mty;
    mod_env = env;
    mod_attributes = [];
    mod_loc = arg.mod_loc }, shape

(* Type a module value expression *)


(* These describe the X in [F(X)] (which might be missing, for [F ()]) *)
type argument_summary = {
  is_syntactic_unit: bool;
  arg: Typedtree.module_expr;
  path: Path.t option;
  shape: Shape.t
}

type application_summary = {
  loc: Location.t;
  attributes: attributes;
  f_loc: Location.t; (* loc for F *)
  arg: argument_summary option (* None for () *)
}

let simplify_app_summary app_view = match app_view.arg with
  | None ->
    Includemod.Error.Unit, Mty_signature []
  | Some arg ->
    let mty = arg.arg.mod_type in
    match arg.is_syntactic_unit , arg.path with
    | true , _      -> Includemod.Error.Empty_struct, mty
    | false, Some p -> Includemod.Error.Named p, mty
    | false, None   -> Includemod.Error.Anonymous, mty

let check_package_closed ~loc ~env ~typ fl =
  if List.exists (fun (_n, t) -> not (Ctype.closed_type_expr t)) fl
  then
    raise (Error (loc, env, Incomplete_packed_module typ))

let not_principal msg = Warnings.Not_principal (Format_doc.Doc.msg msg)

let rec type_module ?(alias=false) ~strengthen ~funct_body anchor env smod =
  Builtin_attributes.warning_scope smod.pmod_attributes
    (fun () -> type_module_aux ~alias ~strengthen ~funct_body anchor env smod)

and type_module_aux ~alias ~strengthen ~funct_body anchor env smod =
  match smod.pmod_desc with
    Pmod_ident lid ->
      let path =
        Env.lookup_module_path ~load:(not alias) ~loc:smod.pmod_loc lid.txt env
      in
      let md = { mod_desc = Tmod_ident (path, lid);
                 mod_type = Mty_alias path;
                 mod_env = env;
                 mod_attributes = smod.pmod_attributes;
                 mod_loc = smod.pmod_loc } in
      let aliasable = Env.is_aliasable path env in
      let shape =
        Env.shape_of_path ~namespace:Shape.Sig_component_kind.Module env path
      in
      let shape = if alias && aliasable then Shape.alias shape else shape in
      let md =
        if alias && aliasable then
          (Env.add_required_global (Path.head path); md)
        else begin
          let mty =
            if strengthen then
              Env.find_strengthened_module ~aliasable path env
            else
              (Env.find_module path env).md_type
          in
          match mty with
          | Mty_alias p1 when not alias ->
              let p1 = Env.normalize_module_path (Some smod.pmod_loc) env p1 in
              let mty = Includemod.expand_module_alias
                  ~strengthen env p1 in
              { md with
                mod_desc =
                  Tmod_constraint (md, mty, Tmodtype_implicit,
                                   Tcoerce_alias (env, path, Tcoerce_none));
                mod_type = mty }
          | mty ->
              { md with mod_type = mty }
        end
      in
      md, shape
  | Pmod_structure sstr ->
      let (str, sg, names, shape, _finalenv) =
        type_structure ~funct_body anchor env sstr in
      let md =
        { mod_desc = Tmod_structure str;
          mod_type = Mty_signature sg;
          mod_env = env;
          mod_attributes = smod.pmod_attributes;
          mod_loc = smod.pmod_loc }
      in
      let sg' = Signature_names.simplify _finalenv names sg in
      if List.length sg' = List.length sg then md, shape else
      wrap_constraint_with_shape env false md
        (Mty_signature sg') shape Tmodtype_implicit
  | Pmod_functor(arg_opt, sbody) ->
      let t_arg, ty_arg, newenv, funct_shape_param, funct_body =
        match arg_opt with
        | Unit ->
          Unit, Types.Unit, env, Shape.for_unnamed_functor_param, false
        | Named (param, smty) ->
          let mty = transl_modtype_functor_arg env smty in
          let scope = Ctype.create_scope () in
          let (id, newenv, var) =
            match param.txt with
            | None -> None, env, Shape.for_unnamed_functor_param
            | Some name ->
              let md_uid =  Uid.mk ~current_unit:(Env.get_current_unit ()) in
              let arg_md =
                { md_type = mty.mty_type;
                  md_attributes = [];
                  md_loc = param.loc;
                  md_uid;
                }
              in
              let id = Ident.create_scoped ~scope name in
              let shape = Shape.var md_uid id in
              let newenv = Env.add_module_declaration
                ~shape ~noalias:true ~check:true id Mp_present arg_md env
              in
              Some id, newenv, id
          in
          Named (id, param, mty), Types.Named (id, mty.mty_type), newenv,
          var, true
      in
      let body, body_shape =
        type_module ~strengthen:true ~funct_body None newenv sbody
      in
      { mod_desc = Tmod_functor(t_arg, body);
        mod_type = Mty_functor(ty_arg, body.mod_type);
        mod_env = env;
        mod_attributes = smod.pmod_attributes;
        mod_loc = smod.pmod_loc },
      Shape.abs funct_shape_param body_shape
  | Pmod_apply _ | Pmod_apply_unit _ ->
      type_application smod.pmod_loc ~strengthen ~funct_body env smod
  | Pmod_constraint(sarg, smty) ->
      let arg, arg_shape =
        type_module ~alias ~strengthen:true ~funct_body anchor env sarg
      in
      let mty = transl_modtype env smty in
      let md, final_shape =
        wrap_constraint_with_shape env true arg mty.mty_type arg_shape
          (Tmodtype_explicit mty)
      in
      { md with
        mod_loc = smod.pmod_loc;
        mod_attributes = smod.pmod_attributes;
      },
      final_shape
  | Pmod_unpack sexp ->
      let exp =
        Ctype.with_local_level_generalize_structure_if_principal
          (fun () -> Typecore.type_exp env sexp)
      in
      let mty =
        match get_desc (Ctype.expand_head env exp.exp_type) with
          Tpackage pack ->
            check_package_closed ~loc:smod.pmod_loc ~env ~typ:exp.exp_type
              pack.pack_cstrs;
            if !Clflags.principal &&
              not (Typecore.generalizable (Btype.generic_level-1) exp.exp_type)
            then
              Location.prerr_warning smod.pmod_loc
                (not_principal "this module unpacking");
            modtype_of_package env smod.pmod_loc pack
        | Tvar _ ->
            raise (Typecore.Error
                     (smod.pmod_loc, env, Typecore.Cannot_infer_signature))
        | _ ->
            raise (Error(smod.pmod_loc, env, Not_a_packed_module exp.exp_type))
      in
      if funct_body && Mtype.contains_type env mty then
        raise (Error (smod.pmod_loc, env, Not_allowed_in_functor_body));
      { mod_desc = Tmod_unpack(exp, mty);
        mod_type = mty;
        mod_env = env;
        mod_attributes = smod.pmod_attributes;
        mod_loc = smod.pmod_loc },
      Shape.leaf_for_unpack
  | Pmod_extension ext ->
      raise (Error_forward (Builtin_attributes.error_of_extension ext))

and type_application loc ~strengthen ~funct_body env smod =
  let rec extract_application ~funct_body env sargs smod =
    match smod.pmod_desc with
    | Pmod_apply (f, sarg) ->
        let arg, shape =
          type_module ~strengthen:true ~funct_body None env sarg
        in
        let summary = {
          loc = smod.pmod_loc;
          attributes = smod.pmod_attributes;
          f_loc = f.pmod_loc;
          arg = Some {
            is_syntactic_unit = sarg.pmod_desc = Pmod_structure [];
            arg;
            path = path_of_module arg;
            shape;
          }
        } in
        extract_application ~funct_body env (summary::sargs) f
    | Pmod_apply_unit f ->
        let summary = {
          loc = smod.pmod_loc;
          attributes = smod.pmod_attributes;
          f_loc = f.pmod_loc;
          arg = None
        } in
        extract_application ~funct_body env (summary::sargs) f
    | _ -> smod, sargs
  in
  let sfunct, args = extract_application ~funct_body env [] smod in
  let funct, funct_shape =
    let has_path { arg } = match arg with
      | None | Some { path = None } -> false
      | Some { path = Some _ } -> true
    in
    let strengthen = strengthen && List.for_all has_path args in
    type_module ~strengthen ~funct_body None env sfunct
  in
  List.fold_left
    (type_one_application ~ctx:(loc, sfunct, funct, args) funct_body env)
    (funct, funct_shape) args

and type_one_application ~ctx:(apply_loc,sfunct,md_f,args)
    funct_body env (funct, funct_shape) app_view =
  match Env.scrape_alias env funct.mod_type with
  | Mty_functor (Unit, mty_res) ->
      begin match app_view.arg with
        | None -> ()
        | Some arg ->
          if arg.is_syntactic_unit then
            (* this call to warning_scope allows e.g.
               [ F (struct end [@warning "-73"]) ]
               not to warn; useful when generating code that must
               work over multiple versions of OCaml *)
            Builtin_attributes.warning_scope arg.arg.mod_attributes @@ fun () ->
            Location.prerr_warning arg.arg.mod_loc
              Warnings.Generative_application_expects_unit
          else
            raise (Error (app_view.f_loc, env, Apply_generative));
      end;
      if funct_body && Mtype.contains_type env funct.mod_type then
        raise (Error (apply_loc, env, Not_allowed_in_functor_body));
      { mod_desc = Tmod_apply_unit funct;
        mod_type = mty_res;
        mod_env = env;
        mod_attributes = app_view.attributes;
        mod_loc = funct.mod_loc },
      Shape.app funct_shape ~arg:Shape.dummy_mod
  | Mty_functor (Named (param, mty_param), mty_res) as mty_functor ->
      let apply_error () =
        let args = List.map simplify_app_summary args in
        let mty_f = md_f.mod_type in
        let app_name = match sfunct.pmod_desc with
          | Pmod_ident l -> Includemod.Named_leftmost_functor l.txt
          | _ -> Includemod.Anonymous_functor
        in
        raise(Includemod.Apply_error {loc=apply_loc;env;app_name;mty_f;args})
      in
      begin match app_view with
      | { arg = None; _ } -> apply_error ()
      | { loc = app_loc; attributes = app_attributes;
          arg = Some { shape = arg_shape; path = arg_path; arg } } ->
      let coercion =
        try Includemod.modtypes ~loc:arg.mod_loc ~mark:true env
              arg.mod_type mty_param
        with Includemod.Error _ -> apply_error ()
      in
      let mty_appl =
        match arg_path with
        | Some path ->
            let scope = Ctype.create_scope () in
            let subst =
              match param with
              | None -> Subst.identity
              | Some p -> Subst.add_module p path Subst.identity
            in
            Subst.modtype (Rescope scope) subst mty_res
        | None ->
            let env, nondep_mty =
              match param with
              | None -> env, mty_res
              | Some param ->
                  let env =
                    Env.add_module ~noalias:true param
                      Mp_present arg.mod_type env
                  in
                  check_well_formed_module env app_loc
                    "the signature of this functor application" mty_res;
                  try env, Mtype.nondep_supertype env [param] mty_res
                  with Ctype.Nondep_cannot_erase _ ->
                    let error = Cannot_eliminate_dependency mty_functor in
                    raise (Error(app_loc, env, error))
            in
            begin match
              Includemod.modtypes ~loc:app_loc ~mark:false env
                mty_res nondep_mty
            with
            | Tcoerce_none -> ()
            | _ ->
                fatal_error
                  "unexpected coercion from original module type to \
                   nondep_supertype one"
            | exception Includemod.Error _ ->
                fatal_error
                  "nondep_supertype not included in original module type"
            end;
            nondep_mty
      in
      check_well_formed_module env apply_loc
        "the signature of this functor application" mty_appl;
      { mod_desc = Tmod_apply(funct, arg, coercion);
        mod_type = mty_appl;
        mod_env = env;
        mod_attributes = app_attributes;
        mod_loc = app_loc },
      Shape.app ~arg:arg_shape funct_shape
    end
  | Mty_alias path ->
      raise(Error(app_view.f_loc, env, Cannot_scrape_alias path))
  | Mty_ident _ | Mty_signature _  ->
      let args = List.map simplify_app_summary args in
      let mty_f = md_f.mod_type in
      let app_name = match sfunct.pmod_desc with
        | Pmod_ident l -> Includemod.Named_leftmost_functor l.txt
        | _ -> Includemod.Anonymous_functor
      in
      raise(Includemod.Apply_error {loc=apply_loc;env;app_name;mty_f;args})

and type_open_decl ?used_slot ?toplevel ~funct_body names env sod =
  Builtin_attributes.warning_scope sod.popen_attributes
    (fun () ->
       type_open_decl_aux ?used_slot ?toplevel ~funct_body names env sod
    )

and type_open_decl_aux ?used_slot ?toplevel ~funct_body names env od =
  let loc = od.popen_loc in
  match od.popen_expr.pmod_desc with
  | Pmod_ident lid ->
    let path, newenv =
      type_open_ ?used_slot ?toplevel od.popen_override env loc lid
    in
    let md = { mod_desc = Tmod_ident (path, lid);
               mod_type = Mty_alias path;
               mod_env = env;
               mod_attributes = od.popen_expr.pmod_attributes;
               mod_loc = od.popen_expr.pmod_loc }
    in
    let open_descr = {
      open_expr = md;
      open_bound_items = [];
      open_override = od.popen_override;
      open_env = newenv;
      open_loc = loc;
      open_attributes = od.popen_attributes
    } in
    open_descr, [], newenv
  | _ ->
    let md, mod_shape =
      type_module ~strengthen:true ~funct_body None env od.popen_expr
    in
    let scope = Ctype.create_scope () in
    let sg, newenv =
      Env.enter_signature ~scope ~mod_shape
        (extract_sig_open env md.mod_loc md.mod_type) env
    in
    let info, visibility =
      match toplevel with
      | Some false | None -> Some `From_open, Hidden
      | Some true -> None, Exported
    in
    Signature_group.iter (Signature_names.check_sig_item ?info names loc) sg;
    let sg =
      List.map (function
        | Sig_value(id, vd, _) -> Sig_value(id, vd, visibility)
        | Sig_type(id, td, rs, _) -> Sig_type(id, td, rs, visibility)
        | Sig_typext(id, ec, et, _) -> Sig_typext(id, ec, et, visibility)
        | Sig_module(id, mp, md, rs, _) ->
            Sig_module(id, mp, md, rs, visibility)
        | Sig_modtype(id, mtd, _) -> Sig_modtype(id, mtd, visibility)
        | Sig_class(id, cd, rs, _) -> Sig_class(id, cd, rs, visibility)
        | Sig_class_type(id, ctd, rs, _) ->
            Sig_class_type(id, ctd, rs, visibility)
      ) sg
    in
    let open_descr = {
      open_expr = md;
      open_bound_items = sg;
      open_override = od.popen_override;
      open_env = newenv;
      open_loc = loc;
      open_attributes = od.popen_attributes
    } in
    open_descr, sg, newenv

and type_structure ?(toplevel = false) ~funct_body anchor env sstr =
  let names = Signature_names.create () in
  let rec type_struct env shape_map sstr =
    match sstr with
    | [] -> ([], [], shape_map, env)
    | pstr :: srem ->
        let previous_saved_types = Cmt_format.get_saved_types () in
        let str, sg, shape_map, new_env =
          type_str_item ~names ~toplevel ~funct_body anchor env shape_map pstr
        in
        Cmt_format.set_saved_types (Cmt_format.Partial_structure_item str
                                    :: previous_saved_types);
        let (str_rem, sig_rem, shape_map, final_env) =
          type_struct new_env shape_map srem
        in
        (str :: str_rem, sg @ sig_rem, shape_map, final_env)
  in
  let previous_saved_types = Cmt_format.get_saved_types () in
  let run () =
    let (items, sg, shape_map, final_env) =
      type_struct env Shape.Map.empty sstr
    in
    let str = { str_items = items; str_type = sg; str_final_env = final_env } in
    Cmt_format.set_saved_types
      (Cmt_format.Partial_structure str :: previous_saved_types);
    str, sg, names, Shape.str shape_map, final_env
  in
  if toplevel then run ()
  else Builtin_attributes.warning_scope [] run

and type_str_item ~names ~toplevel ~funct_body anchor env shape_map
    {pstr_loc = loc; pstr_desc = desc} =
  let desc, sg, shape_map, new_env =
    match desc with
    | Pstr_eval (sexpr, attrs) ->
        let expr =
          Builtin_attributes.warning_scope attrs
            (fun () -> Typecore.type_expression env sexpr)
        in
        Tstr_eval (expr, attrs), [], shape_map, env
    | Pstr_value(rec_flag, sdefs) ->
        let (defs, newenv) =
          Typecore.type_binding env rec_flag sdefs in
        let defs = match rec_flag with
          | Recursive -> Typecore.annotate_recursive_bindings env defs
          | Nonrecursive -> defs
        in
        (* Note: Env.find_value does not trigger the value_used event. Values
           will be marked as being used during the signature inclusion test. *)
        let items, shape_map =
          List.fold_left
            (fun (acc, shape_map) (id, { Asttypes.loc; _ }, _typ, _uid)->
              Signature_names.check_value names loc id;
              let vd =  Env.find_value (Pident id) newenv in
              Sig_value(id, vd, Exported) :: acc,
              Shape.Map.add_value shape_map id vd.val_uid
            )
            ([], shape_map)
            (let_bound_idents_full defs)
        in
        Tstr_value(rec_flag, defs),
        List.rev items,
        shape_map,
        newenv
    | Pstr_primitive sdesc ->
        let (desc, newenv) = Typedecl.transl_value_decl env loc sdesc in
        Signature_names.check_value names desc.val_loc desc.val_id;
        Tstr_primitive desc,
        [Sig_value(desc.val_id, desc.val_val, Exported)],
        Shape.Map.add_value shape_map desc.val_id desc.val_val.val_uid,
        newenv
    | Pstr_type (rec_flag, sdecls) ->
        let (decls, newenv, shapes) =
          Typedecl.transl_type_decl env rec_flag sdecls
        in
        List.iter
          Signature_names.(fun td -> check_type names td.typ_loc td.typ_id)
          decls;
        let items = map_rec_type_with_row_types ~rec_flag
          (fun rs info -> Sig_type(info.typ_id, info.typ_type, rs, Exported))
          decls []
        in
        let shape_map = List.fold_left2
          (fun map { typ_id; _} shape ->
            Shape.Map.add_type map typ_id shape)
          shape_map
          decls
          shapes
        in
        Tstr_type (rec_flag, decls),
        items,
        shape_map,
        enrich_type_decls anchor decls env newenv
    | Pstr_typext styext ->
        let (tyext, newenv, shapes) =
          Typedecl.transl_type_extension true env loc styext
        in
        let constructors = tyext.tyext_constructors in
        let shape_map = List.fold_left2 (fun shape_map ext shape ->
            Signature_names.check_typext names ext.ext_loc ext.ext_id;
            Shape.Map.add_extcons shape_map ext.ext_id shape
          ) shape_map constructors shapes
        in
        (Tstr_typext tyext,
         map_ext
           (fun es ext -> Sig_typext(ext.ext_id, ext.ext_type, es, Exported))
           constructors [],
        shape_map,
         newenv)
    | Pstr_exception sext ->
        let (ext, newenv, shape) = Typedecl.transl_type_exception env sext in
        let constructor = ext.tyexn_constructor in
        Signature_names.check_typext names constructor.ext_loc
          constructor.ext_id;
        Tstr_exception ext,
        [Sig_typext(constructor.ext_id,
                    constructor.ext_type,
                    Text_exception,
                    Exported)],
        Shape.Map.add_extcons shape_map
          constructor.ext_id
          shape,
        newenv
    | Pstr_module {pmb_name = name; pmb_expr = smodl; pmb_attributes = attrs;
                   pmb_loc;
                  } ->
        let outer_scope = Ctype.get_current_level () in
        let scope = Ctype.create_scope () in
        let modl, md_shape =
          Builtin_attributes.warning_scope attrs
            (fun () ->
               type_module ~alias:true ~strengthen:true ~funct_body
                 (anchor_submodule name.txt anchor) env smodl
            )
        in
        let pres =
          match modl.mod_type with
          | Mty_alias _ -> Mp_absent
          | _ -> Mp_present
        in
        let md_uid = Uid.mk ~current_unit:(Env.get_current_unit ()) in
        let md =
          { md_type = enrich_module_type anchor name.txt modl.mod_type env;
            md_attributes = attrs;
            md_loc = pmb_loc;
            md_uid;
          }
        in
        let md_shape = Shape.set_uid_if_none md_shape md_uid in
        (*prerr_endline (Ident.unique_toplevel_name id);*)
        Mtype.lower_nongen outer_scope md.md_type;
        let id, newenv, sg =
          match name.txt with
          | None -> None, env, []
          | Some name ->
            let id, e = Env.enter_module_declaration
              ~scope ~shape:md_shape name pres md env
            in
            Signature_names.check_module names pmb_loc id;
            Some id, e,
            [Sig_module(id, pres,
                        {md_type = modl.mod_type;
                         md_attributes = attrs;
                         md_loc = pmb_loc;
                         md_uid;
                        }, Trec_not, Exported)]
        in
        let shape_map = match id with
          | Some id -> Shape.Map.add_module shape_map id md_shape
          | None -> shape_map
        in
        Tstr_module {mb_id=id; mb_name=name; mb_uid = md.md_uid;
                     mb_expr=modl; mb_presence=pres; mb_attributes=attrs;
                     mb_loc=pmb_loc; },
        sg,
        shape_map,
        newenv
    | Pstr_recmodule sbind ->
        let sbind =
          List.map
            (function
              | {pmb_name = name;
                 pmb_expr = {pmod_desc=Pmod_constraint(expr, typ)};
                 pmb_attributes = attrs;
                 pmb_loc = loc;
                } ->
                  name, typ, expr, attrs, loc
              | mb ->
                  raise (Error (mb.pmb_expr.pmod_loc, env,
                                Recursive_module_require_explicit_type))
            )
            sbind
        in
        let (decls, newenv) =
          transl_recmodule_modtypes env
            (List.map (fun (name, smty, _smodl, attrs, loc) ->
                 {pmd_name=name; pmd_type=smty;
                  pmd_attributes=attrs; pmd_loc=loc}) sbind
            ) in
        List.iter
          (fun (md, _, _) ->
             Option.iter Signature_names.(check_module names md.md_loc) md.md_id
          ) decls;
        let bindings1 =
          List.map2
            (fun ({md_id=id; md_type=mty}, uid, _prev_shape)
                 (name, _, smodl, attrs, loc) ->
               let modl, shape =
                 Builtin_attributes.warning_scope attrs
                   (fun () ->
                      type_module ~strengthen:true ~funct_body
                        (anchor_recmodule id) newenv smodl
                   )
               in
               let mty' =
                 enrich_module_type anchor name.txt modl.mod_type newenv
               in
               Includemod.modtypes_consistency ~loc:modl.mod_loc newenv
                mty' mty.mty_type;
               (id, name, mty, modl, mty', attrs, loc, shape, uid))
            decls sbind in
        let newenv = (* allow aliasing recursive modules from outside *)
          List.fold_left
            (fun env (id_opt, _, mty, _, _, attrs, loc, shape, uid) ->
               match id_opt with
               | None -> env
               | Some id ->
                   let mdecl =
                     {
                       md_type = mty.mty_type;
                       md_attributes = attrs;
                       md_loc = loc;
                       md_uid = uid;
                     }
                   in
                   Env.add_module_declaration ~check:true ~shape
                     id Mp_present mdecl env
            )
            env bindings1
        in
        let bindings2 =
          check_recmodule_inclusion newenv bindings1 in
        let mbs =
          List.filter_map (fun (mb, shape, uid) ->
            Option.map (fun id -> id, mb, uid, shape)  mb.mb_id
          ) bindings2
        in
        let shape_map =
          List.fold_left (fun map (id, _mb, _uid, shape) ->
            Shape.Map.add_module map id shape
          ) shape_map mbs
        in
        Tstr_recmodule (List.map (fun (mb, _, _) -> mb) bindings2),
        map_rec (fun rs (id, mb, uid, _shape) ->
            Sig_module(id, Mp_present, {
                md_type=mb.mb_expr.mod_type;
                md_attributes=mb.mb_attributes;
                md_loc=mb.mb_loc;
                md_uid = uid;
              }, rs, Exported))
           mbs [],
        shape_map,
        newenv
    | Pstr_modtype pmtd ->
        (* check that it is non-abstract *)
        let newenv, mtd, decl = transl_modtype_decl env pmtd in
        Signature_names.check_modtype names pmtd.pmtd_loc mtd.mtd_id;
        let id = mtd.mtd_id in
        let map = Shape.Map.add_module_type shape_map id decl.mtd_uid in
        Tstr_modtype mtd, [Sig_modtype (id, decl, Exported)], map, newenv
    | Pstr_open sod ->
        let (od, sg, newenv) =
          type_open_decl ~toplevel ~funct_body names env sod
        in
        Tstr_open od, sg, shape_map, newenv
    | Pstr_class cl ->
        let (classes, new_env) = Typeclass.class_declarations env cl in
        let shape_map = List.fold_left (fun acc cls ->
            let open Typeclass in
            let loc = cls.cls_id_loc.Location.loc in
            Signature_names.check_class names loc cls.cls_id;
            Signature_names.check_class_type names loc cls.cls_ty_id;
            Signature_names.check_type names loc cls.cls_obj_id;
            let uid = cls.cls_decl.cty_uid in
            let map f id v acc = f acc id v in
            map Shape.Map.add_class cls.cls_id uid acc
            |> map Shape.Map.add_class_type cls.cls_ty_id uid
            |> map Shape.Map.add_type cls.cls_obj_id (Shape.leaf uid)
          ) shape_map classes
        in
        Tstr_class
          (List.map (fun cls ->
               (cls.Typeclass.cls_info,
                cls.Typeclass.cls_pub_methods)) classes),
        List.flatten
          (map_rec
            (fun rs cls ->
              let open Typeclass in
              [Sig_class(cls.cls_id, cls.cls_decl, rs, Exported);
               Sig_class_type(cls.cls_ty_id, cls.cls_ty_decl, rs, Exported);
               Sig_type(cls.cls_obj_id, cls.cls_obj_abbr, rs, Exported)
              ])
             classes []),
        shape_map,
        new_env
    | Pstr_class_type cl ->
        let (classes, new_env) = Typeclass.class_type_declarations env cl in
        let shape_map = List.fold_left (fun acc decl ->
            let open Typeclass in
            let loc = decl.clsty_id_loc.Location.loc in
            Signature_names.check_class_type names loc decl.clsty_ty_id;
            Signature_names.check_type names loc decl.clsty_obj_id;
            let uid = decl.clsty_ty_decl.clty_uid in
            let map f id v acc = f acc id v in
            map Shape.Map.add_class_type decl.clsty_ty_id uid acc
            |> map Shape.Map.add_type decl.clsty_obj_id (Shape.leaf uid)
          ) shape_map classes
        in
        Tstr_class_type
          (List.map (fun cl ->
               (cl.Typeclass.clsty_ty_id,
                cl.Typeclass.clsty_id_loc,
                cl.Typeclass.clsty_info)) classes),
        List.flatten
          (map_rec
             (fun rs decl ->
                let open Typeclass in
                [Sig_class_type(decl.clsty_ty_id, decl.clsty_ty_decl, rs,
                                Exported);
                 Sig_type(decl.clsty_obj_id, decl.clsty_obj_abbr, rs, Exported);
                ])
             classes []),
        shape_map,
        new_env
    | Pstr_include sincl ->
        let smodl = sincl.pincl_mod in
        let modl, modl_shape =
          Builtin_attributes.warning_scope sincl.pincl_attributes
            (fun () -> type_module ~strengthen:true ~funct_body None env smodl)
        in
        let scope = Ctype.create_scope () in
        (* Rename all identifiers bound by this signature to avoid clashes *)
        let sg, shape, new_env =
          Env.enter_signature_and_shape ~scope ~parent_shape:shape_map
            modl_shape (extract_sig_open env smodl.pmod_loc modl.mod_type) env
        in
        Signature_group.iter (Signature_names.check_sig_item names loc) sg;
        let incl =
          { incl_mod = modl;
            incl_type = sg;
            incl_attributes = sincl.pincl_attributes;
            incl_loc = sincl.pincl_loc;
          }
        in
        Tstr_include incl, sg, shape, new_env
    | Pstr_extension (ext, _attrs) ->
        raise (Error_forward (Builtin_attributes.error_of_extension ext))
    | Pstr_attribute x ->
        Builtin_attributes.warning_attribute x;
        Tstr_attribute x, [], shape_map, env
  in
  { str_desc = desc; str_loc = loc; str_env = env }, sg, shape_map, new_env

let type_toplevel_phrase env s =
  Env.reset_required_globals ();
  type_structure ~toplevel:true ~funct_body:false None env s

let type_module_alias =
  type_module ~alias:true ~strengthen:true ~funct_body:false None
let type_module =
  type_module ~strengthen:true ~funct_body:false None
let type_structure =
  type_structure ~funct_body:false None

(* Normalize types in a signature *)

let rec normalize_modtype = function
    Mty_ident _
  | Mty_alias _ -> ()
  | Mty_signature sg -> normalize_signature sg
  | Mty_functor(_param, body) -> normalize_modtype body

and normalize_signature sg = List.iter normalize_signature_item sg

and normalize_signature_item = function
    Sig_value(_id, desc, _) -> Ctype.normalize_type desc.val_type
  | Sig_module(_id, _, md, _, _) -> normalize_modtype md.md_type
  | _ -> ()

(* Extract the module type of a module expression *)

let type_module_type_of env smod =
  let remove_aliases =
    Builtin_attributes.has_remove_aliases smod.pmod_attributes in
  let tmty =
    match smod.pmod_desc with
    | Pmod_ident lid -> (* turn off strengthening in this case *)
        let path, md = Env.lookup_module ~loc:smod.pmod_loc lid.txt env in
          { mod_desc = Tmod_ident (path, lid);
            mod_type = md.md_type;
            mod_env = env;
            mod_attributes = smod.pmod_attributes;
            mod_loc = smod.pmod_loc }
    | _ ->
        let me, _shape = type_module env smod in
        me
  in
  let mty = Mtype.scrape_for_type_of ~remove_aliases env tmty.mod_type in
  (* PR#5036: must not contain non-generalized type variables *)
  check_nongen_modtype env smod.pmod_loc mty;
  tmty, mty

(* For Typecore *)

(* Graft a longident onto a path *)
let rec extend_path path =
  fun lid ->
    match lid with
    | Lident name -> Pdot(path, name)
    | Ldot({ txt = m; _ }, { txt = name; _ }) -> Pdot(extend_path path m, name)
    | Lapply _ -> assert false

(* Lookup a type's longident within a signature *)
let lookup_type_in_sig sg =
  let types, modules =
    List.fold_left
      (fun acc item ->
         match item with
         | Sig_type(id, _, _, _) ->
             let types, modules = acc in
             let types = String.Map.add (Ident.name id) id types in
             types, modules
         | Sig_module(id, _, _, _, _) ->
             let types, modules = acc in
             let modules = String.Map.add (Ident.name id) id modules in
             types, modules
         | _ -> acc)
      (String.Map.empty, String.Map.empty) sg
  in
  let rec module_path = function
    | Lident name -> Pident (String.Map.find name modules)
    | Ldot({ txt = m; _ }, { txt = name; _ }) -> Pdot(module_path m, name)
    | Lapply _ -> assert false
  in
  fun lid ->
    match lid with
    | Lident name -> Pident (String.Map.find name types)
    | Ldot({ txt = m; _ }, { txt = name; _ }) -> Pdot(module_path m, name)
    | Lapply _ -> assert false

let type_package env m pack =
  let modl, scope =
    Typetexp.TyVarEnv.with_local_scope begin fun () ->
      (* type the module and create a scope in a raised level *)
      Ctype.with_local_level begin fun () ->
        let modl, _mod_shape = type_module env m in
        let scope = Ctype.create_scope () in
        modl, scope
      end
    end
  in
  let fl', env =
    match pack.pack_cstrs with
    | [] -> [], env
    | fl ->
      let type_path, env =
        match modl.mod_desc with
        | Tmod_ident (mp,_)
        | Tmod_constraint
            ({mod_desc=Tmod_ident (mp,_)}, _, Tmodtype_implicit, _) ->
          (* We special case these because interactions between
             strengthening of module types and packages can cause
             spurious escape errors. See examples from PR#6982 in the
             testsuite. This can be removed when such issues are
             fixed. *)
          extend_path mp, env
        | _ ->
          let sg = extract_sig_open env modl.mod_loc modl.mod_type in
          let sg, env = Env.enter_signature ~scope sg env in
          lookup_type_in_sig sg, env
      in
      let fl' =
        List.fold_right
          (fun (lid, _t) fl ->
             match type_path (Longident.unflatten lid |> Option.get) with
             | exception Not_found -> fl
             | path -> begin
                 match Env.find_type path env with
                 | exception Not_found -> fl
                 | decl ->
                     if decl.type_arity > 0 then begin
                       fl
                     end else begin
                       let t = Btype.newgenty (Tconstr (path,[],ref Mnil)) in
                       (lid, t) :: fl
                     end
               end)
          fl []
      in
      fl', env
  in
  let mty =
    if pack.pack_cstrs = [] then (Mty_ident pack.pack_path)
    else modtype_of_package env modl.mod_loc {pack with pack_cstrs = fl'}
  in
  List.iter
    (fun (n, ty) ->
      try Ctype.unify env ty (Ctype.newvar ())
      with Ctype.Unify _ ->
        let lid = Longident.unflatten n |> Option.get in
        raise (Error(modl.mod_loc, env, Scoping_pack (lid,ty))))
    fl';
  let modl = wrap_constraint_package env true modl mty Tmodtype_implicit in
  modl, {pack with pack_cstrs = fl'}

(* Fill in the forward declarations *)

let type_open_decl ?used_slot env od =
  type_open_decl ?used_slot ?toplevel:None ~funct_body:false
    (Signature_names.create ()) env od

let type_open_descr ?used_slot env od =
  type_open_descr ?used_slot ?toplevel:None env od

let type_str_item env pstri =
  let si, _, _, new_env =
    type_str_item
      ~toplevel:false ~funct_body:false ~names:(Signature_names.create ())
      None env Shape.Map.empty pstri
  in
  si, new_env

let () =
  Typecore.type_module := type_module_alias;
  Typecore.type_str_item := type_str_item;
  Typetexp.transl_modtype_longident := transl_modtype_longident;
  Typetexp.transl_modtype := transl_modtype;
  Typecore.type_open := type_open_ ?toplevel:None;
  Typetexp.type_open := type_open_ ?toplevel:None;
  Typecore.type_open_decl := type_open_decl;
  Typecore.type_package := type_package;
  Typeclass.type_open_descr := type_open_descr;
  type_module_type_of_fwd := type_module_type_of


(* Typecheck an implementation file *)

let gen_annot target annots =
  let annot = Unit_info.annot target in
  Cmt2annot.gen_annot (Some (Unit_info.Artifact.filename annot))
    ~sourcefile:(Unit_info.Artifact.source_file annot)
    ~use_summaries:false
    annots

let type_implementation target initial_env ast =
  let sourcefile = Unit_info.source_file target in
  let save_cmt target annots initial_env cmi shape =
    Cmt_format.save_cmt (Unit_info.cmt target)
      annots initial_env cmi shape;
    gen_annot target annots;
  in
  Cmt_format.clear ();
  Misc.try_finally (fun () ->
      Typecore.reset_delayed_checks ();
      Env.reset_required_globals ();
      if !Clflags.print_types then (* #7656 *)
        ignore @@ Warnings.parse_options false "-32-34-37-38-60";
      let (str, sg, names, shape, finalenv) =
        type_structure initial_env ast in
      let shape =
        let id = Ident.create_persistent @@ Unit_info.modname target in
        Shape.set_uid_if_none shape (Uid.of_compilation_unit_id id)
      in
      let simple_sg = Signature_names.simplify finalenv names sg in
      if !Clflags.print_types then begin
        Typecore.force_delayed_checks ();
        let shape = Shape_reduce.local_reduce Env.empty shape in
        Printtyp.wrap_printing_env ~error:false initial_env
          Format.(fun () -> fprintf std_formatter "%a@."
              (Printtyp.printed_signature @@ Unit_info.source_file target)
              simple_sg
          );
        gen_annot target (Cmt_format.Implementation str);
        { structure = str;
          coercion = Tcoerce_none;
          shape;
          signature = simple_sg
        } (* result is ignored by Compile.implementation *)
      end else begin
        let source_intf = Unit_info.mli_from_source target in
        if !Clflags.cmi_file <> None
        || Sys.file_exists source_intf then begin
          let compiled_intf_file =
            match !Clflags.cmi_file with
            | Some cmi_file -> Unit_info.Artifact.from_filename cmi_file
            | None ->
                try Unit_info.find_normalized_cmi target with Not_found ->
                  raise(Error(Location.in_file sourcefile, Env.empty,
                              Interface_not_compiled source_intf))
          in
          let dclsig = Env.read_signature compiled_intf_file in
          let coercion, shape =
            Includemod.compunit initial_env ~mark:true
              sourcefile sg source_intf
              dclsig shape
          in
          Typecore.force_delayed_checks ();
          (* It is important to run these checks after the inclusion test above,
             so that value declarations which are not used internally but
             exported are not reported as being unused. *)
          let shape = Shape_reduce.local_reduce Env.empty shape in
          let annots = Cmt_format.Implementation str in
          save_cmt target annots initial_env None (Some shape);
          { structure = str;
            coercion;
            shape;
            signature = dclsig
          }
        end else begin
          Location.prerr_warning
            (Location.in_file (Unit_info.source_file target))
            Warnings.Missing_mli;
          let coercion, shape =
            Includemod.compunit initial_env ~mark:true
              sourcefile sg "(inferred signature)" simple_sg shape
          in
          check_nongen_signature finalenv simple_sg;
          normalize_signature simple_sg;
          Typecore.force_delayed_checks ();
          (* See comment above. Here the target signature contains all
             the values being exported. We can still capture unused
             declarations like "let x = true;; let x = 1;;", because in this
             case, the inferred signature contains only the last declaration. *)
          let shape = Shape_reduce.local_reduce Env.empty shape in
          let alerts = Builtin_attributes.alerts_of_str ~mark:true ast in
          if not !Clflags.dont_write_files then begin
            let cmi =
              Env.save_signature ~alerts simple_sg (Unit_info.cmi target)
            in
            let annots = Cmt_format.Implementation str in
            save_cmt target annots initial_env (Some cmi) (Some shape)
          end;
          { structure = str;
            coercion;
            shape;
            signature = simple_sg
          }
        end
      end
    )
    ~exceptionally:(fun () ->
        let annots =
          Cmt_format.Partial_implementation
            (Array.of_list (Cmt_format.get_saved_types ()))
        in
        save_cmt target annots initial_env None None
      )

let save_signature target tsg initial_env cmi =
  Cmt_format.save_cmt (Unit_info.cmti target)
    (Cmt_format.Interface tsg) initial_env (Some cmi) None

let type_interface env ast =
  transl_signature env ast

(* "Packaging" of several compilation units into one unit
   having them as sub-modules.  *)

let package_signatures units =
  let units_with_ids =
    List.map
      (fun (name, sg) ->
        let oldid = Ident.create_persistent name in
        let newid = Ident.create_local name in
        (oldid, newid, sg))
      units
  in
  let subst =
    List.fold_left
      (fun acc (oldid, newid, _) ->
        Subst.add_module oldid (Pident newid) acc)
      Subst.identity units_with_ids
  in
  List.map
    (fun (_, newid, sg) ->
      (* This signature won't be used for anything, it'll just be saved in a cmi
         and cmt. *)
      let sg = Subst.signature Make_local subst sg in
      let md =
        { md_type=Mty_signature sg;
          md_attributes=[];
          md_loc=Location.none;
          md_uid = Uid.mk ~current_unit:(Env.get_current_unit ());
        }
      in
      Sig_module(newid, Mp_present, md, Trec_not, Exported))
    units_with_ids

let package_units initial_env objfiles target_cmi =
  (* Read the signatures of the units *)
  let units =
    List.map
      (fun f ->
         let artifact = Unit_info.Artifact.from_filename f in
         let sg = Env.read_signature (Unit_info.companion_cmi artifact) in
         if Unit_info.is_cmi artifact &&
            not(Mtype.no_code_needed_sig Env.initial sg)
         then raise(Error(Location.none, Env.empty,
                          Implementation_is_required f));
         Unit_info.Artifact.modname artifact, sg)
      objfiles in
  (* Compute signature of packaged unit *)
  Ident.reinit();
  let sg = package_signatures units in
  (* Compute the shape of the package *)
  let prefix = Unit_info.Artifact.prefix target_cmi in
  let pack_uid = Uid.of_compilation_unit_id (Ident.create_persistent prefix) in
  let shape =
    List.fold_left (fun map (name, _sg) ->
      let id = Ident.create_persistent name in
      Shape.Map.add_module map id (Shape.for_persistent_unit name)
    ) Shape.Map.empty units
    |> Shape.str ~uid:pack_uid
  in
  (* See if explicit interface is provided *)
  let mli = Unit_info.mli_from_artifact target_cmi in
  if Sys.file_exists mli then begin
    if not (Sys.file_exists @@ Unit_info.Artifact.filename target_cmi) then
    begin
      raise(Error(Location.in_file mli, Env.empty,
                  Interface_not_compiled mli))
    end;
    let dclsig = Env.read_signature target_cmi in
    let cc, _shape =
      Includemod.compunit initial_env ~mark:true
        "(obtained by packing)" sg mli dclsig shape
    in
    Cmt_format.save_cmt (Unit_info.companion_cmt target_cmi)
      (Cmt_format.Packed (sg, objfiles)) initial_env  None (Some shape);
    cc
  end else begin
    (* Determine imports *)
    let unit_names = List.map fst units in
    let imports =
      List.filter
        (fun (name, _crc) -> not (List.mem name unit_names))
        (Env.imports()) in
    (* Write packaged signature *)
    if not !Clflags.dont_write_files then begin
      let cmi =
        Env.save_signature_with_imports ~alerts:Misc.Stdlib.String.Map.empty
          sg target_cmi imports
      in
      Cmt_format.save_cmt (Unit_info.companion_cmt target_cmi)
        (Cmt_format.Packed (cmi.Cmi_format.cmi_sign, objfiles)) initial_env
        (Some cmi) (Some shape);
    end;
    Tcoerce_none
  end


(* Error report *)
open Printtyp.Doc

let report_error ~loc _env = function
    Cannot_apply mty ->
      Location.errorf ~loc
        "@[This module is not a functor; it has type@ %a@]"
        (Style.as_inline_code modtype) mty
  | Not_included errs ->
      Location.errorf ~loc ~footnote:Out_type.Ident_conflicts.err_msg
        "@[<v>Signature mismatch:@ %a@]"
        Includemod_errorprinter.err_msgs errs
  | Cannot_eliminate_dependency mty ->
      Location.errorf ~loc
        "@[This functor has type@ %a@ \
           The parameter cannot be eliminated in the result type.@ \
         Please bind the argument to a module identifier.@]"
        (Style.as_inline_code modtype) mty
  | Signature_expected ->
      Location.errorf ~loc "This module type is not a signature"
  | Structure_expected mty ->
      Location.errorf ~loc
        "@[This module is not a structure; it has type@ %a"
        (Style.as_inline_code modtype) mty
  | With_no_component lid ->
      Location.errorf ~loc
        "@[The signature constrained by %a has no component named %a@]"
        Style.inline_code "with"
        (Style.as_inline_code longident) lid
  | With_mismatch(lid, explanation) ->
      Location.errorf ~loc ~footnote:Out_type.Ident_conflicts.err_msg
        "@[<v>\
           @[In this %a constraint, the new definition of %a@ \
             does not match its original definition@ \
             in the constrained signature:@]@ \
         %a@]"
        Style.inline_code "with"
        (Style.as_inline_code longident) lid
        Includemod_errorprinter.err_msgs explanation
  | With_makes_applicative_functor_ill_typed(lid, path, explanation) ->
      Location.errorf ~loc ~footnote:Out_type.Ident_conflicts.err_msg
        "@[<v>\
           @[This %a constraint on %a makes the applicative functor @ \
             type %a ill-typed in the constrained signature:@]@ \
         %a@]"
        Style.inline_code "with"
        (Style.as_inline_code longident) lid
        Style.inline_code (Path.name path)
        Includemod_errorprinter.err_msgs explanation
  | With_changes_module_alias(lid, id, path) ->
      Location.errorf ~loc
        "@[<v>\
           @[This %a constraint on %a changes %a, which is aliased @ \
             in the constrained signature (as %a)@].@]"
        Style.inline_code "with"
        (Style.as_inline_code longident) lid
        Style.inline_code (Path.name path)
        Style.inline_code (Ident.name id)
  | With_creates_invalid_aliases(id, path, invalid_path) ->
      Location.errorf ~loc
        "In this %a constraint,@ replacing %a@ by %a@ would @ \
         introduce an invalid alias@ at %a"
        Style.inline_code "with"
        Style.inline_code (Path.name path)
        Style.inline_code (Path.name invalid_path)
        Style.inline_code (Ident.name id)
  | With_cannot_remove_constrained_type ->
      Location.errorf ~loc
        "@[<v>Destructive substitutions are not supported for constrained @ \
              types (other than when replacing a type constructor with @ \
              a type constructor with the same arguments).@]"
  | With_cannot_remove_packed_modtype (p,mty) ->
      let[@manual.ref "ss:module-type-substitution"] manual_ref =
        [ 12; 7; 3 ]
      in
      let pp_constraint ppf (p,mty) =
        fprintf ppf "%s := %a" (Path.name p) modtype mty
      in
      Location.errorf ~loc
        "This %a constraint@ %a@ makes a packed module ill-formed.@ %a"
        Style.inline_code "with"
        (Style.as_inline_code pp_constraint) (p,mty)
        Misc.print_see_manual manual_ref
  | With_package_manifest (lid, ty) ->
      Location.errorf ~loc
        "In the constrained signature, type %a is defined to be %a.@ \
         Package %a constraints may only be used on abstract types."
        (Style.as_inline_code longident) lid
        (Style.as_inline_code type_expr) ty
        Style.inline_code "with"
  | Repeated_name(kind, name) ->
      Location.errorf ~loc
        "@[Multiple definition of the %s name %a.@ \
         Names must be unique in a given structure or signature.@]"
        (Sig_component_kind.to_string kind) Style.inline_code name
  | Non_generalizable { vars; expression } ->
      let[@manual.ref "ss:valuerestriction"] manual_ref = [ 6; 1; 2 ] in
      Out_type.prepare_for_printing vars;
      Out_type.add_type_to_preparation expression;
      Location.errorf ~loc
        "@[The type of this expression,@ %a,@ \
         contains the non-generalizable type variable(s): %a.@ %a@]"
        (Style.as_inline_code Out_type.prepared_type_scheme) expression
        (pp_print_list ~pp_sep:(fun f () -> fprintf f ",@ ")
           (Style.as_inline_code Out_type.prepared_type_scheme)) vars
        Misc.print_see_manual manual_ref
  | Non_generalizable_module { vars; mty; item } ->
      let[@manual.ref "ss:valuerestriction"] manual_ref = [ 6; 1; 2 ] in
      Out_type.prepare_for_printing vars;
      Out_type.add_type_to_preparation item.val_type;
      Location.errorf ~loc
        "@[The type of this module,@ %a,@ \
         contains non-generalizable type variable(s).@ %a@]"
        modtype mty
        Misc.print_see_manual manual_ref
        ~sub:[ Location.msg ~loc:item.val_loc
                 "The type of this value,@ %a,@ \
                  contains the non-generalizable type variable(s) %a."
                 (Style.as_inline_code Out_type.prepared_type_scheme)
                 item.val_type
                 (pp_print_list ~pp_sep:(fun f () -> fprintf f ",@ ")
                  @@ Style.as_inline_code Out_type.prepared_type_scheme) vars
             ]
  | Implementation_is_required intf_name ->
      Location.errorf ~loc
        "@[The interface %a@ declares values, not just types.@ \
           An implementation must be provided.@]"
        Location.Doc.quoted_filename intf_name
  | Interface_not_compiled intf_name ->
      Location.errorf ~loc
        "@[Could not find the .cmi file for interface@ %a.@]"
        Location.Doc.quoted_filename intf_name
  | Not_allowed_in_functor_body ->
      Location.errorf ~loc
        "@[This expression creates fresh types.@ %s@]"
        "It is not allowed inside applicative functors."
  | Not_a_packed_module ty ->
      Location.errorf ~loc
        "This expression is not a packed module. It has type@ %a"
        (Style.as_inline_code type_expr) ty
  | Incomplete_packed_module ty ->
      Location.errorf ~loc
        "The type of this packed module contains variables:@ %a"
        (Style.as_inline_code type_expr) ty
  | Scoping_pack (lid, ty) ->
      Location.errorf ~loc
        "The type %a in this module cannot be exported.@ \
         Its type contains local dependencies:@ %a"
        (Style.as_inline_code longident) lid
        (Style.as_inline_code type_expr) ty
  | Recursive_module_require_explicit_type ->
      Location.errorf ~loc "Recursive modules require an explicit module type."
  | Apply_generative ->
      Location.errorf ~loc
        "This is a generative functor. It can only be applied to %a"
        Style.inline_code "()"
  | Cannot_scrape_alias p ->
      Location.errorf ~loc
        "This is an alias for module %a, which is missing"
        (Style.as_inline_code path) p
  | Cannot_alias p ->
      Location.errorf ~loc
        "Functor arguments and@ recursive modules@ (within the@ recursive \
         definition),@ such as %a,@ cannot be aliased"
        (Style.as_inline_code path) p
  | Cannot_scrape_package_type p ->
      Location.errorf ~loc
        "The type of this packed module refers to %a, which is missing"
        (Style.as_inline_code path) p
  | Badly_formed_signature (context, err) ->
     let report = Typedecl.report_error ~loc err in
     let txt =
       Format_doc.doc_printf "In %s:@ %a"
         context
         Format_doc.pp_doc report.main.txt
     in
     { report with main = { report.main with txt} }
  | Cannot_hide_id Illegal_shadowing
      { shadowed_item_kind; shadowed_item_id; shadowed_item_loc;
        shadower_id; user_id; user_kind; user_loc } ->
      let shadowed =
        Printtyp.namespaced_ident shadowed_item_kind shadowed_item_id
      in
      let shadower =
        Printtyp.namespaced_ident shadowed_item_kind shadower_id
      in
      let shadowed_item_kind= Sig_component_kind.to_string shadowed_item_kind in
      let shadowed_msg =
        Location.msg ~loc:shadowed_item_loc
          "@[%s %a came from this include.@]"
          (String.capitalize_ascii shadowed_item_kind)
          Style.inline_code shadowed
      in
      let user_msg =
        Location.msg ~loc:user_loc
        "@[The %s %a has no valid type@ if %a is shadowed.@]"
        (Sig_component_kind.to_string user_kind)
         Style.inline_code (Ident.name user_id)
         Style.inline_code shadowed
      in
      Location.errorf ~loc ~sub:[shadowed_msg; user_msg]
        "Illegal shadowing of included %s %a@ by %a."
        shadowed_item_kind
        Style.inline_code shadowed
        Style.inline_code shadower
  | Cannot_hide_id Appears_in_signature
      { opened_item_kind; opened_item_id; user_id; user_kind; user_loc } ->
      let opened_item_kind= Sig_component_kind.to_string opened_item_kind in
      let opened_id = Ident.name opened_item_id in
      let user_msg =
        Location.msg ~loc:user_loc
          "@[The %s %a has no valid type@ if %a is hidden.@]"
          (Sig_component_kind.to_string user_kind)
          Style.inline_code (Ident.name user_id)
          Style.inline_code opened_id
      in
      Location.errorf ~loc ~sub:[user_msg]
        "The %s %a introduced by this open appears in the signature."
        opened_item_kind
        Style.inline_code opened_id
  | Invalid_type_subst_rhs ->
      Location.errorf ~loc "Only type synonyms are allowed on the right of %a"
        Style.inline_code  ":="
  | Non_packable_local_modtype_subst p ->
      let[@manual.ref "ss:module-type-substitution"] manual_ref =
        [ 12; 7; 3 ]
      in
      Location.errorf ~loc
        "The module type@ %a@ is not a valid type for a packed module:@ \
         it is defined as a local substitution (temporary name)@ \
         for an anonymous module type.@ %a"
        Style.inline_code (Path.name p)
        Misc.print_see_manual manual_ref

let report_error env ~loc err =
  Printtyp.wrap_printing_env ~error:true env
    (fun () -> report_error env ~loc err)

let () =
  Location.register_error_of_exn
    (function
      | Error (loc, env, err) ->
        Some (report_error ~loc env err)
      | Error_forward err ->
        Some err
      | _ ->
        None
    )