First beware that functor application is still a function application, which may construct large records. For instance, in
the functor application is allocating a record with more than 40 fields in order to construct a small set.
My personal point of view is that instantiating (large) functors should be seen as building libraries. And while it is fine to have some duplication of libraries, commonly used libraries should be explicitly shared. In particular, with
module PolytopeQ = Polytope.Make(Number.Q)(VectorQ)(VectorSetQ)
I expect that the PolytopeQ should use the common instance of ℚ-vectors rather than defining its own. Similarly, if there are multiple users of sets of vectors (which seems to be a subtle notion if one expects to have robust sets beyond fixed-point numbers or ℚ).
Some of the rules for aliasing functor applications and arguments are expected to be relaxed in some future versions of the language (5.6? 5.7? maybe even later?), but I would expect that sharing common instance of functor applications to be still more readable.