The Coq mailing list

[Assia Mahboubi <Assia.Mahboubi AT sophia.inria.fr>]

Hello,

   I have some difficulties in understanding how unification is  performed on
the following example (sorry it is a bit long):

Here is a module type for the argument of the functors to be defined.

Module Type PARAM.
  Parameter A:Se.
End PARAM.

Then the following functor:

Module M1(P:PARAM).
  Record rec(A:Set):Type := mk_rec{f:Set}.
End M1.

will be used to define two (very similar) objects in two distinct modules.

Module M2(P:PARAM).
  Import P.
  Module PM1 := M1 P.
  Import PM1.
  Definition rec2 := mk_rec A A.
End M2.

Module M3(P:PARAM).
  Import P.
  Module PM1 := M1 P.
  Import PM1.
  Definition rec3 := mk_rec A A.
End M3.

I would have said that the types of rec2 and rec3 are unifiable,
so I try this:

Module test(P:PARAM).

Module testM1 := M1 P.
Module testM2 := M2 P.
Module testM3 := M3 P.

Import P.
Import testM1.
Import testM2.
Import testM3.

Definition t(n:nat):=
  match n with
  |O => rec3
  |_ => rec2
  end.

But this raises the following error message (using either v8 or CVS):
Error: Unable to unify the types found in the branches:
For "0" : "PM1.rec A"
For "S" : testM2.PM1.rec A"

Could somebody explain to me what happens?
Thanks a lot in advance...

Cheers

assia

------------------------------------------------------
This message was sent using IMP: http://horde.org/imp/