Agda2 における関数定義と変数束縛

本日Ktさんに聞いてわかったことを、備忘のためにメモ。Agda 2 でデータ型からデータ型　への関数を定義するとき、変数の束縛に関して、思いもよらないことがおこる（昨日はバグはこのせい）。
Aのデータ型は

A : Nat -> A
g : (n : Nat) -> ...

の形をしており、Bも同様の形をしているとする。また関数 g は g :(n : Nat) -> X -> A n の形の関数で、データ型 A n のコンストラクターの一つとする。このとき、 g zero p : A zero （ただし p : X）が成立する。
さて、以下の関数 f を定義するとき、問題が起こる。

f : A zero -> B zero
f g .zero p = q

これは、一行目でデーター型を引数として取りデータ型を返す関数 f を定義し、なおかつそれにコンストラクター g を適用している場合に起こる問題で、zeroのところに .をつける（被束縛であることを明示する）ことをしない限り、エラーが出る。つまり、g の引数は、すでに上の行で束縛されているので、二行目では .zero と被束縛であることを明示しないといけない。
Agda 2 ではパターンマッチを採用したため、こういう点で変数の束縛に関するルールが非常に厳しくなっているようだ。