Implicit Arguments in Computed Type in Coq

Question

I have a library for writing indexed types without an explicit index stream. This leads to cleaner top-level types by hiding unnecessary plumbing. This happens something like this:

Section Indexed. Local Open Scope type. Context {I : Type} (T : Type) (AB : 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 AB) (at level 20, right associativity). Notation "[ A ]" := (IForall A) (at level 70). 

However, Coq ignores my request to make the universal quantifier entered by IForall implicit, as shown in the figure:

 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 to get Coq to really make this argument implicit?

Answer 1

Not.

Cf Error # 3357

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

 Notation IArrow AB := (fun i => A i -> B i) Notation IForall A := (forall {i}, A i). Notation "A :-> B" := (IArrow AB) (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.