Coqはどうなってるんだろう

Inductive Bool : Set := true : Bool | false : Bool.

Inductive Ty {A : Set} : A -> Set := ty (a : A) : Ty a.

Definition f (arg : Ty true) :=
  match arg with
    | ty true => true
  end.

これで、fをCheckすると

f
     : Ty true -> match true with
                  | true => Bool
                  | false => ID
                  end

なんだよなぁ・・・。

IDっていうのは、id = λA.λx.x , typeof id = (A : Set) -> A -> Aみたいなそれです。polymorphicなidですね。

ただ、fに対してexplicitなtype signatureを与えると

Definition f (arg : Ty true) : Bool :=
  match arg with
    | ty true => true
  end.

Check fすると
f
     : Ty true -> Bool

と成ってくれる。
しかし、依然として

Axiom nanka : Ty true.

Definition x := Eval compute in f nanka.

Check xすると
x
     : match true with
       | true => Bool
       | false => forall A : Type, A -> A (* これがIDの型ですね。でもfalseって...? *)
       end

何にせよ、「関数fの定義には成功」している。

Agda2でコレと同様の事をやると

data Bool : Set0 where
  true : Bool
  false : Bool

data Ty {A : Set0} : A -> Set0 where
  ty : (x : A) -> Ty x

f : (Ty true) -> Bool
f x with x
... | ty true = true

昨日書いたようなそれらそれらによってダメです。

勿論、Coqでもf (ty false)のような事をすると型チェックでエラーとしてはじかれますが・・・。

Agda2のsyntaxに成ってしまいますが、個人的には

f : (Ty true) -> Bool
f (ty true) = true

として、「定義可能である」とすべきだと思うので、Coqで定義出来るっていうのはそちらの方が良いなーと思うのですけれども、この辺の違いって、何処から出て来ているんでしょうか。

追記 Coqのバージョン

Welcome to Coq 8.2 (February 2009) (* Proof General走らせるとバッファとして出現する *coq* から *)

/Users/ranha% coqtop --version
The Coq Proof Assistant, version 8.2 (February 2009)
compiled on Feb 19 2009 16:51:28 with OCaml 3.11.0

8.2ですねー。ふむふむ。

更に追記

http://coq.inria.fr/distrib/V8.2pl1/CHANGES

• More automation in the inference of the return clause of dependent pattern-matching problems.
• Experimental allowance for omission of the clauses easily detectable as impossible in pattern-matching problems.

この辺かな。Experimentalって書いてるけど・・・。

型シグネチャが書いて無い時よりも、人間が型シグネチャ書いた時っていうのは情報が多いんだから、そこも使ってくれると嬉しいかもなーとは思ったりもするんですけれども・・・。