Why Coq's `Include` is designed to instantiate functor with current interactive defining module?

Question

It is surprising for me to see that Coq can Include a functor and will instantiate it with the current interactive module.

Coq Ref Manual:

Command Include module_type_inl <+ module_expr_inl*

Includes the content of module(s) in the current interactive module. Here module_type_inl can be a module expression or a module type expression. If it is a high-order module or module type expression then the system tries to instantiate module_type_inl with the current interactive module.

A working example:

Module Type B.
Parameter b : Set.
End B.
Module A (ctx : B).
Definition a : ctx.b -> ctx.b := fun x => x.
End A.

Module SeeHere.
Definition b := nat.
Include A.
End SeeHere.

Print SeeHere.
(* Module SeeHere := Struct Definition b : Set.
 Definition a : b -> b.
 End *)

My question is, this behaviour seems a bit random to me -- at least I don't find similar behaviour in OCaml's include -- what is the intention/main usage for this feature?

Answer 1

I am not sure what the developers intended, but this feature is used in Coq's standard library to create bundled module types. (See, e.g., this blog post, this issue, this paper, or even the section on packed vs unpacked records on pages 54--55 of my thesis for some discussion of the bundled and unbundled styles of records, which are sort-of like lightweight modules.)

For example, we have in Coq.Structures.Equalities:

Module Type Typ.
  Parameter Inline(10) t : Type.
End Typ.

Module Type HasEq (Import T:Typ).
  Parameter Inline(30) eq : t -> t -> Prop.
End HasEq.

Module Type Eq := Typ <+ HasEq.

(Note that Module Type A := B. is the same as Module Type A. Include B. End A.)

Here we want to have both module types that are parameterized over their type (HasEq) and ones that have the type as a field (Eq). Giving Include this behavior allows us to avoid duplicating definitions in the bundled and unbundled versions.