The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

> I have a question about Coq 8.2 (beta), specifically about sort  
> polymorphism and the module system.  I'm going to use the FSets  
> library as an example.
> 
> <<
> Require Import FSets.
> 
> Module NatSet := FSetWeakList.Make Nat_as_DT.
> 
> Print NatSet.elt.  (* NatSet.elt = nat : Type *)
>  >>
> 
> My question: Given the definition of NatSet.elt, I would expect that  
> it could be given type Set.  After all, nat has type Set.  However,  
> "Check (NatSet.elt : Set)" fails.  Why is this the case?  Judging from  
> the description of sort polymorphism in the reference manual, perhaps  
> I'm expecting more than is actually the case?

This is not specifically related to sort-polymorphism of inductive
types but to the way functors work. 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,

Hugo