Re: [Caml-list] Strange behavior from type inference after functor application

[Andreas Rossberg <rossberg@mpi-sws.org>]

On May 31, 2012, at 23.22 h, rixed@happyleptic.org wrote:
> -[ Thu, May 31, 2012 at 10:23:13PM +0200, Gabriel Scherer ]----
>> The problem with
>>  module C = Combi (S) (TypeWithConf (struct let v = 1 end))
>> is that the resulting type has no "name": (struct let v = 1 end) can
>> not be part of a type path.
>
> So in order for the compiler to infer a type the type must have a  
> 'name'?
> That's funny because this 'name' is not used anywhere. Couldn't just
> such anonymous modules be given random names so that everything  
> works as
> long as these names are unused? I mean, in the given example no type  
> of
> this Conf module was required to infer that C.t is a product type  
> (which
> was everything needed since f was returning the first value).
>
> Or would it be just too obscure and not useful enough?

The compiler has to give a module type to the module C, and the OCaml  
type system insists that any module type it computes is expressible by  
a syntactically valid signature. So it has to find one that avoids  
mentioning S2.t. The only way to do so in a syntactically valid manner  
is to make t abstract altogether in the resulting signature.

This is known as the "avoidance problem" in literature on ML modules.  
The only solution to avoid the avoidance problem is to not insist on  
syntactic signatures during type checking, which is essentially what  
you suggest (although it's a bit more complicated in general). Other  
dialects of ML modules indeed work like that, but it would be quite a  
fundamental change to the way module type checking is done in OCaml.

/Andreas