I am trying to search the following questions online but I failed:
When applying a functor (parametrized module), will the contents inside the functor be re-type-checked?
Will Coq's command
Includetrigger unnecessary type-checking of those included fields?
Neither of these checks seems necessary to me but I worry that I miss some details, and I am not really familiar with Coq's codebase and implementation details.
I found it a bit hard to understand the source code structure of Module/Module Type implementation in Coq (unlike how the coq-plugin tutorial provides a very clear introduction to understanding most type-checking mechanism and interface inside Coq).
Thus any tutorial/analysis on Coq's Module/Module Type implementation is also welcomed.