なぜなにあぐだ

data Unit : Set0 where
  unit : Unit

data Ty : Unit -> Set0 where
  ty : (u : Unit) -> Ty u

f : Ty unit -> Unit
f (ty unit) = unit

g : Ty unit -> Unit
g (ty a) = a

gがあれだよなー

a != unit of type Unit
when checking that the pattern ty a has type Ty unit

っていうのはまぁ分かっていて、

u != unit of type Unit
when checking that the pattern ty unit has type Ty unit

でもfはunitっていうデータコンストラクタじゃんうーん。なんだうーん。ちょっと紙に色々書いてみるか。

Coqだと出来るんじゃない??

Inductive Unit : Set := unit : Unit.

Inductive Ty : Unit -> Set := ty (u : Unit) : Ty u.

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

(* "_"でマッチさせたい時は Axiom nanka : Ty unit.
として、 nanka を使えば良さげかなーとは。*)

Coqで出来るからなんだ、っていうよりも、なんでAgda2で出来ないソレなのかっていうのを知りたいんだよなぁ・・・。

うーんなんでだろう・・・。

まぁ分からんのでAgdaのIRCに行ってみたけど、完全にぼっちというか発言が１つも無い様に思えるのは何でなんだろうなーみたいな感じなので、誰かが構ってくれるまで完全に待ちです。