クイズ！ 存在的多相型

しばらくつまらない問題＆解答ばかりだったので、もう少し面白いやつを。存在型と再帰関数のある多相λ計算で、次の2つの値は文脈等価でしょうか？　できれば証明ないし反例も。

v1 = pack (unit, λf:unit→unit. (f (); true)) as τ
v2 = pack (bool, λf:bool→bool. (f true) ∧ ¬(f false)) as τ

where

τ = ∃α.(α→α)→bool

OCamlで書くと、

module type T = sig
  type t
  val g : (t -> t) -> bool
end

module V1 : T = struct
  type t = unit
  let g = fun f -> (f (); true)
end

module V2 : T = struct
  type t = bool
  let g = fun f -> (f true) && not (f false)
end

に対して、

module A1 = F(V1)

は無限ループして

module A2 = F(V2)

は無限ループしないようなFはあるか、という話。ただし参照とか例外とか、pureでない言語機構は使用禁止。っていうとわかっちゃうかもしれないけど。

ちなみにデレック・ドレイヤー博士(ttic.uchicago.edu/~dreyer/)やアンドリュー・ピッツ教授(www.cl.cam.ac.uk/~amp12/)は間違えました。っていうかそういうメールを送りつけてきたので突っ込みを入れて切り返した。検索されないようにカタカナ表記。

追記：polymorphic equalityも禁止。とかいうと、ますますヒントになりますが。