The Coq mailing list

[Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>]

This is a simplified example that is only meant to demonstrate what I'd 
like to achieve.

Module Type Variables.
  Variable V : Set.
End Variables.

An interpretation associates a natural number to every variable.

Module Type Interpretation.
  Declare Module Vars : Variables.
  Variable interp : Vars.V -> nat.
End Interpretation.

The extension of an interpretation allows also to interprete sums and 
products:

Module Interpretation_ext (I:Interpretation).
  Inductive X : Set :=
  | Plus : I.Vars.V -> I.Vars.V -> X
  | Times : I.Vars.V -> I.Vars.V -> X.

  Definition interp_ext (x : X) :=
  match x with
  | Plus v w => I.interp v + I.interp w
  | Times v w => I.interp v * I.interp w
  end.
End Interpretation_ext.

Now, I'd like to compare two different interpretations that have the 
same set of variables.

Module Interp_compat (V:Variables) (I1 I2 : Interpretation  with Module 
Vars := V).
  Module I1_ext := Interpretation_ext(I1).
  Module I2_ext := Interpretation_ext(I2).

  Definition same := forall x, I1_ext.interp_ext x = I2_ext.interp_ext 
x.

The last definition gets rejected:
  Error: In environment
  x : I1_ext.X
  The term "x" has type "I1_ext.X" while it is expected to have type 
"I2_ext.X"

The type X in Interpretation_ext is the same for I1_ext and I2_ext

I also tried to specify this as a constraint when defining I1 and I2 :

Module Type IntExt.
  Variable X : Set.
  Variable interp_ext : X -> nat.
End IntExt.

Module Interp_compat (V:Variables) (I1 I2 : Interpretation  with Module 
Vars := V).
  Module I1_ext : IntExt := Interpretation_ext(I1).
  Module I2_ext : IntExt with Definition X := I1_ext.X := 
Interpretation_ext(I2).

But I get the error :
  "User error: Signature components for label X do not match"

Is there a way to do this ? Of course I1.V.Vars and I2.V.Vars are the 
same, but can this be extended to the results of functor applications ?

thank you