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?

I haven't tried it, but if we define a notation like this: Notation ":fun var => body" := (fun n var => body) (at level <some-level>)., then Definition id {A : nat -> Type} : [ A :-> A ] := :fun a => a. should work. Not sure if this is what you are looking for. — Anton Trunov
But sometimes I don't want to bind anything. E.g. I'd like Definition app (f : [A :-> B]) (a : [A]) : [B]) := f a. to work out of the box. — gallais

Jason Gross Jason Gross · Accepted Answer · 2017-11-19T07:54:50

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.

Implicit arguments in a computed type in Coq

1 Answers