The Coq mailing list

[Brian Aydemir <baydemir AT cis.upenn.edu>]

On Sep 10, 2008, at 06:31, Hugo Herbelin wrote:

> The result of a functor
> application is obtained by simple substitution of the fields and the
> types of the fields in the applied functor are the ones computed for
> the body of the non applied functor (independently of whether the
> functor body has an explicit type constraint or not). For instance, we
> have
>
> Module Type S. Parameter t:Type. End S.
> Module F (X:S). Definition t := X.t. End F.
> Parameter nat' : Set.
> Module N. Definition t := nat'. End N.
> Module P := F N.
> Check P.t.  (* P.t : Type *)
>
> where the information that P.t can be typed of type Set has been lost.
>
> Being able to infer P.t : Set would require in the general case to
> recompute all types, as substitution of field parameters by actual
> arguments may occur arbitrarily deep in expressions and accordingly
> refine non trivially the inferred type of exported fields. Is this
> cost worth?
>
> Hoping to have clarified the point,

Thank you.  That explanation is indeed helpful.

--Brian