The Coq mailing list

["Kyle Stemen" <ncyms8r3x2 AT snkmail.com>]

I'm not sure what the proper fix is, but the problem is that the coercion isn't getting used, because ModTypeImpl.S is only equal to nat after unfolding.

On Fri, Jul 14, 2023 at 11:09 PM Chris Dams chris.dams.nl-at-gmail.com |coq-club/Example Allow| <k3xf67o2kbvxpwt AT sneakemail.com> wrote:

Dear All,

I am trying to define a Coercion inside a Module. When trying to use
this Coercion outside the Module, it seems to be running into trouble.
See example below. Is it possible to define a Coercion inside a module
that accepts something from the Module Type and use it outside the
Module?

Kind Regards,
Chris


Module Type ModType.
   Axiom S: Set.
   Axiom T: Set.
End ModType.

Module Mod (M: ModType).
   Export M.
   Axiom f: S -> T.
   Coercion f: S >-> T.
End Mod.

Module ModTypeImpl <: ModType.
   Definition S: Set := nat.
   Definition T: Set := bool.
End ModTypeImpl.

Module ModImpl := Mod ModTypeImpl.
Import ModImpl.

(* Error: The term "1" has type "nat" while it is expected to have
type "bool". *)
(* Check negb 1. *)

(* Error: The term "1" has type "nat" while it is expected to have
type "bool". *)
Fail Check negb 1.

(* Casting works *)
Check (negb: ModTypeImpl.T -> bool) (1 : ModTypeImpl.S).

(* Declaring more coercions fixes it. *)
Definition unfold_S (n: nat) : ModTypeImpl.S := n.
Coercion unfold_S: nat >-> ModTypeImpl.S.
Definition fold_T (b : ModTypeImpl.T) : bool := b.
Coercion fold_T: ModTypeImpl.T >-> bool.

Check negb 1.

 

Definition ff: nat -> bool := f.
Coercion ff: nat >-> bool.

(* No error: apparently it was made to work with the coercion ff,
which is defined
   to be f. But f was also made a coercion above in Mod. *)
Check negb 1.