From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <rixed@happyleptic.org>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by sympa.inria.fr (Postfix) with ESMTPS id 7EDB97ED26
	for <caml-list@sympa.inria.fr>; Thu, 31 May 2012 22:06:01 +0200 (CEST)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AvwEAGTOx0/V+6tl/2dsb2JhbABEtBWBB4JZgTQoiEOXbaB4jUGCNmADlRePdIJi
X-IronPort-AV: E=Sophos;i="4.75,693,1330902000"; 
   d="scan'208";a="160796671"
Received: from eneide.happyleptic.org ([213.251.171.101])
  by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/AES256-SHA; 31 May 2012 22:06:01 +0200
Received: from extranet.securactive.org ([82.234.213.170] helo=ccellier.rd.securactive.lan)
	by eneide.happyleptic.org with esmtp (Exim 4.72)
	(envelope-from <rixed@happyleptic.org>)
	id 1SaC6N-0002kX-Nc
	for caml-list@inria.fr; Thu, 31 May 2012 22:36:11 +0200
Received: from rixed by ccellier.rd.securactive.lan with local (Exim 4.77)
	(envelope-from <rixed@happyleptic.org>)
	id 1SaBd5-00083a-FA
	for caml-list@inria.fr; Thu, 31 May 2012 22:05:55 +0200
Date: Thu, 31 May 2012 22:05:55 +0200
From: rixed@happyleptic.org
To: caml-list@inria.fr
Message-ID: <20120531200555.GA30956@securactive.lan>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
User-Agent: Mutt/1.5.21 (2010-09-15)
Subject: [Caml-list] Strange behavior from type inference after functor
 application

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?