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

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.

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.

• Perhaps this could be tagged module?
– Couchy
Mar 29 at 19:57

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).