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

[rixed@happyleptic.org]

Given these definitions:

-- v1 --

module type TYPE = sig type t end

module Combi (S1 : TYPE) (S2 : TYPE) :
    TYPE with type t = S1.t * S2.t =
struct
    type t = S1.t * S2.t
end

module TypeWithConf (Conf : sig val v : int end) :
	TYPE =
struct
    type t = unit
end

module S = struct type t = unit end

module C = Combi (S) (TypeWithConf (struct let v = 1 end))

let f (x : C.t) = fst x

-----

Here, the compiler fails to infer that C.t is indeed the product of two types
(as stated in the Combi signature), and complains that:

Error: This expression has type C.t but an expression was expected of type 'a * 'b
(pointing at the argument of fst)

There is two ways to satisfies it:

- either, state that the type of TypeWithConf is 'TYPE with type t = unit'
  instead of merely 'TYPE'

- or, more surprisingly, to define the Conf structure as in:

-- v2 --
(* ... *)

module Conf = struct let v = 1 end
module C = Combi (S) (TypeWithConf (Conf))

(* ... *)
-----

Can someone help me find an explanation to this behavior?