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?
Coq 8.16.0
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.
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
Maybe a section should be used with the parameter S
as a section variable? (haven't tried)
Putting (S:Type) in a section works.
Last updated: Mar 29 2024 at 00:41 UTC