let instance pool v =

  (* [get], [set], and [setp] implement a constant-time mapping from
     descriptors of rank [none] to variables. [mapped] allows determining
     whether a given descriptor belongs to the domain of the
     mapping. [associate] and [retrieve] respectively allow extending and
     looking up the mapping.

     In order to implement a constant-time mapping without wasting extra
     space, we re-use the descriptor's [rank] field, which is redundant at
     this point, since its value must be [none], and store a pointer in
     it. The field is to be viewed as containing a pointer if and only if
     the descriptor is marked with [m]. *)

  let m =
    Mark.fresh() in

  let setp desc =
    Mark.same desc.mark m

  and set desc v =
    desc.mark <- m;
    desc.var <- Some v

  and get desc =
    unSome desc.var
  in

  (* If [v] has rank [none], then [copy v] returns a copy of the variable
     [v], and copies its descendants recursively. The copy is registered in
     the current pool and given the current rank. If [v] has nonnegative
     rank, then [copy v] returns [v]. Only one copy per variable is created,
     even if a variable is found twice during the traversal. *)

  let rec copy v =

    let desc = UnionFind.find v in

    (* If a copy has been created already for this variable, return it. We
       must check this condition first, since we must not read [desc.rank]
       unless we know that the variable hasn't been copied yet. *)

    if setp desc then 
      get desc

    (* Otherwise, check the variable's rank. If it is other than [none],
       then the variable must not be copied. *)

    else if (IntRank.compare desc.rank IntRank.none <> 0 || desc.kind = Constant)
    then 
      v

    (* Otherwise, the variable must be copied. We create a new variable,
       update the mapping, then update the new variable's descriptor. Note
       that the mapping must be updated before making a recursive call to
       [copy], so as to guarantee termination in the presence of cyclic
       terms. *)

    else 
      let desc' = 
          {
            structure = None;
            rank = pool.number;
            mark = Mark.none; 
            kind = Flexible;
            name = (match desc.kind with Rigid -> None | _ -> desc.name);
            pos = None;
            var = None
          } 
      in
      let v' = UnionFind.fresh desc' in
        register pool v';
        set desc v';
        let v' = 
          match desc.structure with
            | None ->
                v'
            | Some term ->
                desc'.structure <- Some (map copy term);
                v'
        in
          v'

  (* If [v] was effectively copied by [copy], then [restore v] returns
     [v] to its original state (that is, restores its rank to [none])
     and restores its descendants recursively. If [v] was not copied,
     [restore v] has no effect. *)

  and restore v =
    let desc = UnionFind.find v in
    if setp desc then begin
      desc.mark <- Mark.none;
      desc.rank <- IntRank.none;
      match desc.structure with
        | None ->
            ()
        | Some term ->
            iter restore term
    end

  in

  (* We are now ready to take an instance of the type scheme whose
     entry point is [v]. It is simply a matter of copying [v] and
     its descendants, stopping at non-universally-quantified nodes.
     The copy process affects the type scheme, which must be restored
     afterwards. The whole process is linear in the size of the type
     scheme, that is, in the number of universally quantified nodes. *)
  let v' = copy v in
  restore v;
  v'