double-vision-problem.ml

signature S_A =
  sig
    type u (* 外部から与えられる *)
    type t
    val f : t -> u * t
  end

signature S_B =
  sig
    type t (* 外部から与えられる *)
    type u
    val g : t -> u * t
  end

signature S =
  rec (X) sig
    module A : (S_A with type u = X.B.u)
    module B : (S_B with type t = X.A.t)
  end

module AB =
  rec (X : S) struct
    module A :> (S_A with type u = X.B.u) =
      struct
        type u = X.B.u

        type t = int

        val f (x : t) : u * t =
          let (y, z) = X.B.g (x + 3) in
          (y, z + 5)
            (* 型環境は rec (X : S) に基づいて X.B.g : X.A.t -> X.B.u * X.A.t であることは保持しているが，
               X.A.t が最終的に int と等しくなるという情報はもっていないため，
               X.B.g (x + 3) を検査する時点で型エラーになってしまう．
               これがdouble vision problem． *)
      end

    module B :> (S_B with type t = X.A.t) =
      struct
        type t = X.A.t

        type u = bool

        val g (x : t) : u * t =
          ...
      end
  end