Implicit parameter in singleton class

user_16695384 0
Viewed 75

When I create a typeclass with a single method in the usual syntax, I can give it implicit parameters:

Class Foo1 := { foo1 {n} : Int n }.

But when I use the singleton syntax, I can't give it the implicit parameter

Fail Class Foo2 := foo2 {n} : Int n.

Error: Syntax error: '.' expected after [gallina] (in [vernac_aux]).

I can't even use Arguments to make that parameter implicit:

Class Foo3 := foo3 n : Int n.
Fail Arguments foo3 {n}.

The command has indeed failed with message: Flag "rename" expected to rename Foo3 into n.

Is there a reason for it to work this way?

coq
1 Answers

On your 2nd attempt

Your second try could work by moving the n on the other side of the colon:

Class Foo2 := foo2 : forall {n}, Int n.

On your 3rd attempt

The error message tells you to use the rename flag. This is because foo3 in fact takes Foo3 (the typeclass instance it projects from) as a first (implicit) argument, before the integer. This first argument happens to already have a name (Foo3), as you can see by running About foo3.

About foo3.
(*
foo3 : Foo3 -> forall n : nat, Int n

Arguments foo3 {Foo3} _%nat_scope
*)

Hence Coq believes you want to rename that argument to n. If that was really what you wanted, you could do it using the rename flag as suggested:

Arguments foo3 {n} : rename.

After which About foo3. will yield:

foo3 : Foo3 -> forall n0 : nat, Int n0

Arguments foo3 {n} n%nat_scope
  (where some original arguments have been renamed)

But what you actually want is to affect the second argument by making it implicit. In the process, you don’t want to give it a new name (no need, it is already named n), and you don’t want to alter the first argument (i.e. you keep it implicit and avoid renaming it). Hence, what you should do is:

Arguments foo3 {_ _}.

Yielding

Arguments foo3 {Foo3} {n}%nat_scope
user_12759750
Related