The Coq mailing list

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

Hi,

> I have the following problem with applications occurring as effective
> parameters of functors:
> 
> Module Type S.
> End S.
> 
> Module F (X : S).
> End F.
> 
> Module M1.
> End M1.
> 
> Module Type MT (Y : S).
> End MT.
> 
> Module M2 (X : S) <: MT(F(X)).
>    Module M := M1(F(X)).
> End M2.
> 
> User error: Application to not path
> 
> Why cannot I directly pass an application as effective parameter of
> a functor?

Coq paths are made of iterated module field selections.  Having
expressions like F(M) in paths would require computations at path
resolution time. Coq could somehow hide a precomputation N of F(M) and
reason with N in place of F(M) but this is not done. Hence, the user
has to do the job of "precomputation" her/himself in advance.

Doing this in the body of your module M2 is easy :

  Module M2 (X : S).
     Module FX := F(X).
     Module M := M1(FX).
  End M2.

However, in the type constraints, there is no notation for that.

> Is there any workaround?

To simulate what you want to do with your MT type constraint, there is
the standard following workaround (though it is not strictly
equivalent as it requires exporting more components than you'd like):

  Module Type S.
  End S.
  
  Module F (X : S).
  End F.
  
  Module M1 (X : S).  (* assume M1 is a functor so that example makes sense *)
  End M1.
  
  Module Type MT (Y : S).
  End MT.
  
  Module Type MTF.
  Declare Module LX:S.
  Module Y:=F(LX).
  Include Type MT(Y).  (* V8.2 only; needs otherwise to copy contents of MT *)
  End MTF.
  
  Module M2 (X : S) <: MTF with Module LX:=X.
     Module LX := X.    (* now needed because MTF exports it *)
     Module Y := F(X).  (* now needed because MTF exports it *)
     Module M := M1(Y).
  End M2.

Hope it helps.

Hugo Herbelin