Implicit arguments in a computed type in Coq

Question

I have a library to write indexed types without having to explicitly thread the index. This leads to cleaner top-level types by hiding away the irrelevant plumbing. It goes something like this:

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).

However Coq ignores my request to make the universal quantifier introduced by IForall implicit as demonstrated by:

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

Is there a way for me to get Coq to indeed make this argument implicit?

Answer 1

No.

C.f. Bug #3357

One day, I hope, PR #668 will be merged, and then you will be able to do

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.