Coqで計算された型の暗黙の引数

Question

私は、明示的にインデックスをスレッド化することなく、インデックス付きの型を書くためのライブラリを持っています。これは、無関係の配管を隠すことによって、よりクリーンなトップレベルタイプにつながります。

Fail Definition id {A : nat -> Type} : [ A :-> A ] := fun a => a. 
Definition id {A : nat -> Type} : [ A :-> A ] := fun (n : nat) a => a. 

私が取得するための方法はあります：しかしコックがによって示されるように、暗黙のIForallによって導入普遍数量詞を作るために私の要求を無視し

Section Indexed. 

Local Open Scope type. 
Context {I : Type} (T : Type) (A B : I -> Type). 

Definition IArrow : I -> Type := 
    fun i => A i -> B i. 

Definition IForall : Type := 
    forall {i}, A i. 

End Indexed. 

Notation "A :-> B" := (IArrow A B) (at level 20, right associativity). 
Notation "[ A ]" := (IForall A) (at level 70). 

：それはこのような何かを行きますCoqは実際にこの議論を暗黙的にしていますか？

Answer 1

f。 Bug #3357

ある日、私は願って、PR #668がマージされ、その後、あなたは

Notation IArrow A B := 
    (fun i => A i -> B i) 

Notation IForall A := 
    (forall {i}, A i). 

Notation "A :-> B" := (IArrow A B) (at level 20, right associativity). 
Notation "[ A ]" := (IForall A) (at level 70). 

Definition id {A : nat -> Type} : [ A :-> A ] := fun a => a. 
Definition id {A : nat -> Type} : [ A :-> A ] := fun (n : nat) a => a.