The Coq mailing list

[<akhirsch AT gwmail.gwu.edu>]

Hello all,

I'm trying to set up a coercion between types in a record, as follows:

  Require Import Setoid.

  (* We have two models here, one contains a set of domain elements *)
  Record first_model : Type := {
    D : Set;
    d_Eq : relation D
  }.

  (* And the other is a Kripke-style many-worlds model, where the worlds can
be viewed as the first model. It contains principals. *)
  Record second_model : Type := {
    P : Set;
    W : Set;
    p_Eq : relation P;
    s : W -> first_model;
    coerce_p_to_d : forall (w : W), P -> D (s w)
  }.

  (* coerce_p_to_d is supposed to be an injective function that shows that p
is a subset to d, a la Cantor. *)
  Axiom coerce_p_inj : forall (M : second_model) (w : W M) (p p' : P M), d_Eq
(s M w) (coerce_p_to_d M w p) (coerce_p_to_d M w p') -> p_Eq\
 M p p'.

  (* The following gives: Error: coerce_p_to_d does not respect the uniform
inheritance condition. *)
  Coercion coerce_p_to_d : P >-> D.

However, I get the error that I commented about above. Everything I see on
coercions has the types outside of records, however, coercions are supposed to
take any class, so it seems like this should work (P is of type forall M :
second_model, Set, etc).

Is there a way to make this work?