Instances for id

[liyishuai]

I'm trying to add Serialize and Deserialize instances for id, but they're not found. Is this a Coq issue or where did I mess up?

Instance Serialize_id {A} {Serialize_A : Serialize A} : Serialize (id A) :=
  Serialize_A.
Fail Definition id_Z_to_sexp : id Z -> sexp atom := to_sexp.

The command has indeed failed with message: Unable to satisfy the following constraints:

?Serialize : "Serialize (id Z)"

[Lysxia]

Here's a self contained example.

Class C (A : Type) : Type :=
  test : A.

(* As expected *)
Instance C_n : C nat := 0.
Definition ok : nat := test.

Instance C_id {A} {C_A : C A} : C (id A) := test (A := A).

(* Why not? *)
Fail Definition ko : id nat := test.

[Lysxia]

It looks like a Coq issue but I can't tell whether it's a bug or working as expected.

[Lysxia]

It works if you make id universe polymorphic, which you really should if you're applying it to types:

Class C (A : Type) : Type :=
  test : A.

Instance C_nat : C nat := 0.

Polymorphic Definition id {A} : A -> A := fun x => x.

Instance C_id {A : Type} (C_A : C A) : C (id A) := test (A := A).

Definition ko : id nat := test.

[liyishuai]

or ~Set Universe Polymorphism.~ Update: Don't do so! Polymorphism might break your existing code! Use Polymorphic Instance instead.