Stream: Coq users

Topic: Coercion with implicit Type -> Type works, fails for Type


view this post on Zulip Lef Ioannidis (Feb 26 2023 at 19:38):

Trying to understand why this coercion fails.

Module Foo.

  Inductive Dummy {S: Type -> Type}: Type := DummyC: unit -> Dummy.

  Inductive Pred {T} :=
  | Base: (T -> Prop) -> Pred.

  Definition foo_of_Prop' {S}(P : Prop) : Pred := Base (fun (_: S) => P).
  Definition foo_of_Prop {S}(P : Prop) : Pred := Base (fun (_: @Dummy S) => P).
  Fail Coercion foo_of_Prop' : Sortclass >-> Pred.
  Coercion foo_of_Prop : Sortclass >-> Pred.

End Foo.

What is more surprsing, if I change the type of Dummy to Dummy{S: Type} then both coercions fail.
Only a combination of a dummy inductive and S: Type -> Type makes the coercion work, but everything else fails.
What is going on?

view this post on Zulip Lef Ioannidis (Feb 26 2023 at 19:39):

Coq 8.16.0

view this post on Zulip Paolo Giarrusso (Feb 26 2023 at 20:12):

seems Coq's taking foo_of_Prop as a coercion from S : Type to Prop -> Pred, which is a Funclass.
For foo_of_Prop', that can't happen because S : Type -> Type lives in Funclass, which cannot be a source class. (as Fail Coercion foo_of_Prop : Funclass >-> Pred. points out).

Here's a slightly expanded example

Module Foo.

  Inductive Dummy {S: Type -> Type}: Type := DummyC: unit -> Dummy.

  Inductive Pred {T} :=
  | Base: (T -> Prop) -> Pred.
  Arguments Pred : clear implicits. (* extra readability *)

  Definition foo_of_Prop' {S : Type}(P : Prop) : Pred S := Base (fun (_: S) => P).
  Definition foo_of_Prop {S : Type -> Type} (P : Prop) : Pred Dummy := Base (fun (_: @Dummy S) => P).
  Fail Coercion foo_of_Prop' : Sortclass >-> Pred.
  (*
  The command has indeed failed with message:
  Found target class Pred instead of Funclass.
  *)

  (* Coercion foo_of_Prop' : Sortclass >-> Sortclass. *)
  Coercion foo_of_Prop' : Sortclass >-> Funclass.
  (* Coercion foo_of_Prop : Sortclass >-> Funclass. *)
  Coercion foo_of_Prop : Sortclass >-> Pred.

  Inductive Dummy' {S: Type}: Type := DummyC': unit -> Dummy'.
  Definition foo_of_Prop'' {S : Type} (P : Prop) : Pred Dummy' := Base (fun (_: @Dummy' S) => P).
  Coercion foo_of_Prop'' : Sortclass >-> Funclass.
End Foo.

view this post on Zulip Paolo Giarrusso (Feb 26 2023 at 20:14):

the extra type annotations are what I needed to make some sense of what was happening.

unfortunately I'm no coercion expert — I hope somebody else can advise

view this post on Zulip Pierre Roux (Feb 26 2023 at 20:30):

Maybe a section should be used with the parameter S as a section variable? (haven't tried)

view this post on Zulip Lef Ioannidis (Feb 27 2023 at 01:47):

Putting (S:Type) in a section works.


Last updated: Mar 29 2024 at 00:41 UTC