> > For the record, your simplification based on identity of signature
> > identifiers
> > is probably ok in practice, but it does
> > rule out some examples that involve package types with free type
> > variables. 
> 
> Right. Would it break something to allow named module type with
> explicit arguments:
> 
> module type 'a ARRAY = sig
>    type array
>    val init: 'a -> array
>    val sub: array -> int -> 'a
>    val update : array -> int -> 'a -> array
> end
> 
> ?
> 
> Then the unification between < (a1,...,ap) S > and < (b1,...,bq) T >
> is solved by equating S = T (syntactically), p=q  and unifying
> a1=b1,...,ap=bp.


I think this would be fine, but you then also have to deal with the
meaning
of these parameterised signatures in other contexts, eg:

functor F(X: ('a -> int) S )= <modexp>;

and so on. Is this declaration illegal or should the functor F be
implicitly polymorphic in 'a?
This is not impossible to deal with, just needs some more work. I
suppose you could only allow
signature applications in core type expressions of the form < sigexp >,
but that seems a little hacky.

-c




> 
> -- 
>   Alain Frisch
> 
>