Implicit argument が絡んで型検査を通らない例

型検査(推論?)がうまくいってもよさそうだけどうまくいかない話です.挙動は Coq 8.5pl2 で確認しました.他のバージョンでどうかは調べていません.

Set Implicit Arguments してから,なんか依存型を定義します.

Coq < Set Implicit Arguments.

Coq < Inductive Fin : nat -> Set :=
| F0 n : Fin (S n)
| FS n : Fin n -> Fin (S n).
Coq < Coq < Fin is defined
Fin_rect is defined
Fin_ind is defined
Fin_rec is defined

Coq < Fixpoint Fin' (n : nat) : Set :=
  match n with 0 => Empty_set | S n' => sum unit (Fin' n') end.
Coq < Fin' is defined
Fin' is recursively defined (decreasing on 1st argument)

自然数で添字付けられた集合族です.返ってくる物の中身はわりと何でもよくて,それぞれ Inductive と Fixpoint で定義されているところが重要な気がします.

それで,これらを引数に取る関数を何か作ります.ここでは面倒なので変数を宣言してしまいます.戻り値は Prop にしておきましたが,別に何でもよさそうです.

Coq < Parameter P : forall n (i : Fin' n), Fin n -> Prop.
P is assumed

Coq < Print P.
*** [ P : forall n : nat, Fin' n -> Fin n -> Prop ]

Argument n is implicit
Argument scopes are [nat_scope _ _]

P の第一引数の n は implict になります.第三引数の型から推論できそうなのでまあそうでしょうという気がします.ちょっと使ってみます.

Coq < Check (P (inl tt) (F0 0)).
Toplevel input, characters 10-16:
> Check (P (inl tt) (F0 0)).
>           ^^^^^^
Error:
The term "inl tt" has type "(unit + ?B)%type"
while it is expected to have type "Fin' ?n".

うまくいかないようです.(inl tt) の型は (unit + ?B) だけど (Fin ?n) が要求されていると言われています.実際には,第三引数の型が (Fin 1) でこいつは inductive type なので第一引数が 1 であることが(たぶん)わかり,これを第二引数の型の n に代入すれば (Fin' 1) となりますが,これは (unit + unit) に簡約できます.以上のように推論すると型が合っていることがわかる気がしますが,そんなことはしてくれないようです.

明示的に型を書くか引数を与えてやるとチェックは通ります.

Coq < Check (P (inl tt : Fin' 1) (F0 0)).
P (inl tt : Fin' 1) (F0 0)
     : Prop

Coq < Check (P (n := 1) (inl tt) (F0 0)).
P (inl tt) (F0 0)
     : Prop

でもちょっと面倒だし,読みにくくなりがち.

試しに P の引数の順番を変えてみると,

Coq < Parameter P' : forall n (i : Fin n), Fin' n -> Prop.
P' is assumed

Coq < Print P'.
*** [ P' : forall n : nat, Fin n -> Fin' n -> Prop ]

Argument n is implicit
Argument scopes are [nat_scope _ _]

Coq < Check (P' (F0 0) (inl tt)).
P' (F0 0) (inl tt)
     : Prop

こっちは問題ないようです.ということは型検査アルゴリズムが項を処理する順番の問題とかだろうか.もし引数を左からチェックするのだとすると,最初の例では n がわからない状態で (inl tt) の型検査をすることになるので,型が合わないように見える.今の例だと先に (F0 0) を検査するので,n = 1 とわかり,その後 (inl tt) を見るので型が合うと判断できる.本当にそういう実装になってるかどうか知りませんが.

ついでに両方とも inductive でない方の型にしてみると,

Coq < Parameter P'' : forall n (i : Fin' n), Fin' n -> Prop.
P'' is assumed

Coq < Print P''.
*** [ P'' : forall n : nat, Fin' n -> Fin' n -> Prop ]

Argument scopes are [nat_scope _ _]

これは n が implicit でなくなります.Fin' n のような実引数が与えられると簡約されるものは,n が何だったか後からわからなくなる可能性があるから,まあそれが自然かという気がします(オプションでいろいろ制御できる).