From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id oBQ5udgc017269 for ; Sun, 26 Dec 2010 06:56:39 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhwCAPtnFk3RVdK2mGdsb2JhbACZL4p6CBUBAQEBAQgJDAcRJKUYjA+DUokFAQEDBYVFBIRjhiGEBoU7 X-IronPort-AV: E=Sophos;i="4.60,230,1291590000"; d="scan'208";a="71382916" Received: from mail-iy0-f182.google.com ([209.85.210.182]) by mail3-smtp-sop.national.inria.fr with ESMTP; 26 Dec 2010 06:56:33 +0100 Received: by iyb26 with SMTP id 26so7350415iyb.27 for ; Sat, 25 Dec 2010 21:56:33 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:sender:subject:mime-version :content-type:from:in-reply-to:date:cc:content-transfer-encoding :message-id:references:to:x-mailer; bh=b9AHG7YqE/ppb0E5XuX/m/pHbQXDAm6JOKel+cy2SxE=; b=j5GjOm+tjIKs3Msm0iatXfNsIeKPUdyxpE3Ht6D8gwOyD0bucyEBdLJaVLR0xjq8nn QhYr443ODP+f+X6aSmsSnLxyGbdkUE8MTVLKAn2jKcW3gzhOwRn+Ya6mRshFj2pfRJFb wJaBMc2cnmzAgPVK2gu74LKG9TnZJXuEUAoUc= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to:x-mailer; b=qUXzK0eYXzbbbomB7KswwS/2t+bwnWsDwzvyLMiPf3Dwbq+8AlljLWzbBPJkC+dHiQ riP1tKzDHmklyI1j4h76kutAXRlHNqm4yHsCEnPuFQcVETu5Mf9PpWotfvooS4e/rWMA ejLER7op96VWfSSlq49ccOaMJihwKnUj1LkN8= Received: by 10.231.206.80 with SMTP id ft16mr11031283ibb.110.1293342993179; Sat, 25 Dec 2010 21:56:33 -0800 (PST) Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mx.google.com with ESMTPS id d21sm9630243ibg.9.2010.12.25.21.56.31 (version=TLSv1/SSLv3 cipher=RC4-MD5); Sat, 25 Dec 2010 21:56:32 -0800 (PST) Sender: Jacques Garrigue Mime-Version: 1.0 (Apple Message framework v1082) Content-Type: text/plain; charset=us-ascii From: Jacques Garrigue In-Reply-To: Date: Sun, 26 Dec 2010 14:56:28 +0900 Cc: OCaml List Content-Transfer-Encoding: 7bit Message-Id: <1988FE07-0BE7-41C7-911A-FBC8DC9530EE@math.nagoya-u.ac.jp> References: To: Markus Mottl X-Mailer: Apple Mail (2.1082) Subject: Re: [Caml-list] Manifest types in module type inclusions On 2010/12/26, at 14:19, Markus Mottl wrote: > please consider the following code: > > ------------------- > module M = struct type t = A | B end > > module X : sig > (* type t = M.t = A | B *) > include module type of M > (* include module type of M with type t = M.t = A | B *) > end = struct include M end > > let () = assert (M.A = X.A) > ------------------- > > This will fail, because M.A is not of the same type as X.A. But I > would really like to make the types equivalent. > > Using the first commented out line instead of the module type > inclusion will succeed, but then I would not be able to automatically > include any functions potentially contained in module M. The last > commented out line won't work, because one cannot establish a type > equivalence via a manifest type definition after "with type". Even > if, I don't think one could override anything else but an abstract > type that way, and we are including a sum type here already. > > Does anybody have any suggestions for a workaround? I suspect this > may be a missing feature. Unfortunately there is no easy workaround using 3.12.0. Intuitively at least the 3rd line should work, but a bug prevents this. In 3.12.1, you should be able to write either the 3rd, or the simpler following version: include module type of M with type t = M.t This should solve your problem. Side note: the choice to make "include M" define "type t = A | B" rather than "type t = M.t = A | B" was done to allow more implementations (any module defining the same operations as M is allowed, rather than modules sharing the same representation for types.) But it resulted in not allowing the code you write here, which was not intentional. Jacques Garrigue