Does Coq's Module and Functor type-check incrementally?

Question

I am trying to search the following questions online but I failed:

1. When applying a functor (parametrized module), will the contents inside the functor be re-type-checked?

2. Will Coq's command Include trigger 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.

---

Not-so-related-but-helpful question:

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.

Answer 1

The whole goal of the module system is to provide, as the name implies, modularity. In particular, the typing rules guarantee that if M : S and F(X : S) : T are respectively a module and a functor, then F(M) : T{X:=M}. Just as function application, this does not need additional re-type-checking, except for 1. the subtyping check when applying a module whose interface does not match exactly, and 2. keeping the graph of global universes consistent.

Subtyping is essentialy checking for the conversion of the type of the definitions with the ones of the signature. Since we keep those types we do not have to recompute them. Conversion being fairly arbitrary in CIC, you can still cook up degenerate examples that will explode, e.g. with a very expensive call on one side and its reduced form on the other.

Universe checking is a consequence of the subtyping check, because new constraints between floating universes can appear when trying to convert two types, e.g. think of Type@{u} ≡ Type@{v}, which needs to add u ≡ v. This additional cost is much tamer because it's polynomial in the number of constraints, and usually this number is rather small.

About Include, this doesn't check anything but it still needs to substitute the names of the module being included by the ones of the current module. As such, this is ideally O(n).

I found it a bit hard to understand the source code structure of Module/Module Type implementation

Unfortunately you are not the only one. I would not make a very exaggerated claim if I said that nobody understands the module system of Coq in full.