Nested functors: Compiler can't determine type equality

Yes and no. Normally, all modules have a runtime representation, and a functor application results in a real function application at runtime. But there are two major exceptions that make functors seem almost compile-time:

  • Type (and module type) expressions do not have any runtime representation, so functor applications that occurs in a type expression do not introduce a runtime functor application. As an example, let x : F(X).t = ... doesn’t apply the functor F at runtime because its application only occurs in the type annotation for x.
  • Modules and functors are often defined at the toplevel of compilation units, and in those cases the compiler can usually compute the functor applications at compile time as an optimisation. This is highly dependent on the compiler’s optimisation flags though.