The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Emmanuel Polonowski wrote:
> When using the module system in order to instantiate a functor, I get a 
> strange error message.
>
> [...]
>
> Module GI (a : A) := G a (FI a).
>
> Error: Application to not path.
>    

A path is a base module with a series of projections out of it.  A path 
can't contain a functor application, and the argument in a functor 
application must be a path.  So, actually quite a good error message 
once the definition is made clear!

Here's an alternate declaration which I would assume is equivalent to 
what you wanted to write:

Module GI (a : A).
  Module FI' := FI a.
  Module G' := G a FI'.
  Import G'.
End GI.