以下のようなデータ型宣言があったとする。
data T {a : A} (b : B) : X -> Set where
C1 : {c1 : C1} (d1 : D1) : T b x1
C2 : {c2 : C2} (d2 : D2) : T b x2
x1（またはx2）はaやbやc1やd1（c2やd2）からXの項が作られているものとする。
このとき、生成される要素は以下の3つである。
T : {a : A} -> (b : B) -> X -> Set
C1 : {a : A} -> {b : B} -> {c1 : C1} -> (d1 : D1) -> T {a} b x1
C1 : {a : A} -> {b : B} -> {c2 : C2} -> (d2 : D2) -> T {a} b x2
簡単に説明。
- Tは比較的そのまま。あえて言えばコロンが矢印になっているくらい。
- C1とC2は引数に「Tのパラメータだったもの」が先頭の暗黙的パラメータとしてくっついている。ただしコロンより後ろに書かれていたXはない。
つまるところ、影響があるのはTの宣言でコロンの前に書かれたaやbである。
- Tにとっては、コロンの前後にかかわらず「この型が取るパラメータ」であるため、基本的に宣言そのままの引数になる。
- Tのコロンの前にあるパラメータaとbはこの型宣言全体で可視なパラメータである。各コンストラクタはaやbを使える。一方残りの型Xのパラメータについては（今回は無名であるのもあるがそうでなくても）型宣言全体では見えず、あくまでSetまで書かれた範囲でしか見えない。
このようにaやbは可視範囲が広いので、コンストラクタが独立して存在するにあたり相当する値をどこかから拝借しなければならない。結果としてaやbは暗黙的パラメータとして追加される。
もちろんよほどのことがない限りこのパラメータを明示的に渡すことはない（必要とされる型から自動で推論される）が、c1やc2を渡そうとする際に若干ややこしいことになるので注意。（{c1 = ...}のような書き方をすると問題を回避しやすい）
なお、このパラメータは便利なのだが、コンストラクタ記述時に制約がつく。
定義時、全てのコンストラクタの型はTに（aや）bを適用した型で終わることが要求される。今回の例で言えば、必ず結果が T {a} b ... の形の型でなければならない。一方、型Xのパラメータについてはそのような制限はなく、コンストラクタ毎に異なってよい（x1とx2は異なってよい）。
あと、この制約は「結果の部分」にのみかかり、コンストラクタのパラメータにTが出現しても（aや）bを使う必要性は無い。
_≡_ の定義が複雑な考えと思うかもしれないが落ち着いて読めば読める。
xが型パラメータにあるのはコンストラクタで第一引数が固定されても特に影響ないため。
第二引数が第一引数と同じという制約はあくまでコンストラクタで行う。
