Projections can be made classes but you can't define instances

[gmalecha]

Version

$ coqtop -v
The Coq Proof Assistant, version 8.8.2 (November 2018)
compiled on Nov 7 2018 21:54:20 with OCaml 4.07.0

Operating system

Ubuntu 18.04

Description of the problem

Set Primitive Projections.

Class type (t : Type) : Type :=
  { bar : t -> Prop  }.

Instance type_nat : type nat :=
{ bar := fun _ => True }.

Existing Class bar.

Global Instance foo_bar {n : nat} : bar n := I.
(* with primitive projections, this line fails with "Error: bar is not a declared type class."
 * without primitive projections it succeeds
 *)

Expected behavior: bar should be a typeclass so there shouldn't be a problem with the definition of foo_bar as an instance.
If there is a reason to forbid supporting this, then there should be an error on the call to Existing Class bar.

[ppedrot]

The problem here is that bar n in interpreted as the primitive projection n.(bar). To fix this in a future-proof way, we need to also natively handle projections in typeclasse instances. There might be a day where we don't declare the compatibility projection constants.

[gmalecha]

Are you saying that Existing Class bar is making the compatibility definition a class, but not the projection itself?

[JasonGross]

Are you saying that Existing Class bar is making the compatibility definition a class, but not the projection itself?

Yes, it is exactly this. Here is a workaround that @ppedrot will probably say I'd be terrible for relying on:

Set Primitive Projections.
Class type (t : Type) : Type :=
  { bar : t -> Prop  }.

Instance type_nat : type nat :=
  { bar := fun _ => True }.

Existing Class bar.

Global Instance foo_bar {n : nat} : match @bar with x => x _ _ n end := I.

[JasonGross]

However, note that this workaround, while it gets the statement to be accepted, probably does not solve your problem. The instance gets picked up on

Check _ : match @bar with x => x _ _ _ end.

but not on

Check _ : @bar _ _ _.

[gmalecha]

Thanks, @JasonGross . I definitely don't want to do the workaround :-). This isn't a crucial issue for me right now.

[Alizter]

@ppedrot Isn't this closed by #9711 as well?

[ppedrot]

Indeed. We should add a test before closing this issue though. Probably not, this is too similar to the other one to be worth it.