The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Bonjour,

  Your example of non convertibility of inductive types is due to the
"generativity" of functor application: functor application defines new
objects that are distinct of the objects defined by distinct instances
of functor application (even if the same functor is applied to the
same argument). For defined constants, the convertibility is recovered
because of the convertibility of bodies but for inductive types, the
convertibility does not hold.

  You have to move the functor application outside M1 and M2, or to
abstract over PM1 and PM2 in M1 and M2.

  Hugo

> 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?