From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id B735A801E4 for ; Thu, 31 Aug 2017 00:21:13 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=garrigue@math.nagoya-u.ac.jp; spf=None smtp.mailfrom=garrigue@math.nagoya-u.ac.jp; spf=None smtp.helo=postmaster@ms.math.nagoya-u.ac.jp Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.11; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.11; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@ms.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.11; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@ms.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3A/hjioh0NtbGyEVZysmDT+DRfVm0co7zxezQtwd8Z?= =?us-ascii?q?segVKPad9pjvdHbS+e9qxAeQG96Eu7QZ06L/iOPJZy8p2d65qncMcZhBBVcuqP?= =?us-ascii?q?49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL3WbmHC57CYTFxPjLkI1?= =?us-ascii?q?Y72tQs+Buf+qzPi/8IH/ZABBhTz1Ie8jbUb+kQKE/PEfnI8qA+B58QfEqXhMdv?= =?us-ascii?q?4cjTdzOV+YnD7n+sq7/4Vk/TgWsPUkoZ1uS6L/KoYxRqVFAS9uHGkv/szkqBSL?= =?us-ascii?q?GQSG/GEdXXgbuh9BHwiD6hj1WYb49za8v+E72jHMbp6+dqw9RTn3t/QjcxTvki?= =?us-ascii?q?pScmNg/Q=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0A+AgAbOqdZlwuCBoVEGhoBAQEBAgEBA?= =?us-ascii?q?QEIAQEBARUBAQEBAgEBAQEIAQEBAYQTA4ESjwqQeYJolXMBK4UbAoRqFAEBAQE?= =?us-ascii?q?BAQEBAQEBEgEBAQEBCBYGV4IzBQEeBoI8AwMnEwYBASwLAQ8LJSFFEgYTEgmJf?= =?us-ascii?q?gMUETKsHoJYOoMIAQEFhCkDNhqDOQEBAQEBAQEBAQEBAQEBAQEBAQEBARUIgyq?= =?us-ascii?q?FXguCcoMmgU+DQ4Ixh20HLgyKCo45h1mMcwyCYIhmhxmRbYRWNoEuUzlJEgGCc?= =?us-ascii?q?oIEDxAMgXZnAYk0gVMBAQE?= X-IPAS-Result: =?us-ascii?q?A0A+AgAbOqdZlwuCBoVEGhoBAQEBAgEBAQEIAQEBARUBAQE?= =?us-ascii?q?BAgEBAQEIAQEBAYQTA4ESjwqQeYJolXMBK4UbAoRqFAEBAQEBAQEBAQEBEgEBA?= =?us-ascii?q?QEBCBYGV4IzBQEeBoI8AwMnEwYBASwLAQ8LJSFFEgYTEgmJfgMUETKsHoJYOoM?= =?us-ascii?q?IAQEFhCkDNhqDOQEBAQEBAQEBAQEBAQEBAQEBAQEBARUIgyqFXguCcoMmgU+DQ?= =?us-ascii?q?4Ixh20HLgyKCo45h1mMcwyCYIhmhxmRbYRWNoEuUzlJEgGCcoIEDxAMgXZnAYk?= =?us-ascii?q?0gVMBAQE?= X-IronPort-AV: E=Sophos;i="5.41,450,1498514400"; d="scan'208";a="235774276" Received: from bsd20.math.nagoya-u.ac.jp (HELO ms.math.nagoya-u.ac.jp) ([133.6.130.11]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 31 Aug 2017 00:20:41 +0200 Received: from [192.168.0.13] (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ms.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 694B0516B88; Thu, 31 Aug 2017 07:13:44 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=math.nagoya-u.ac.jp; s=20160220; t=1504131224; bh=aj+E+P+mIFGBn1IJKv6AcPtjl+gj/KAxC3DKzukBi14=; h=Subject:From:In-Reply-To:Date:Cc:References:To; b=GrB6KBXqPkXNL3EFoE/Jbyr/UPi4zWNVKvDhDjKDNgGuV75UTULeSkozY7+5bVMtN RP4sk33W4lSdP8GccoIe6laDS0C4UHUIfmilk6C4VRc35z74dZ6+x5uTVfGpCjJQvk MViIpnljehsaN7PjQgrimIUHM2jZhscEBYOusAn0= Content-Type: text/plain; charset=us-ascii Mime-Version: 1.0 (Mac OS X Mail 10.3 \(3273\)) From: Jacques Garrigue In-Reply-To: Date: Thu, 31 Aug 2017 07:20:32 +0900 Cc: Mailing List OCaml Content-Transfer-Encoding: quoted-printable Message-Id: References: To: "Paul A. Steckler" X-Mailer: Apple Mail (2.3273) X-Greylist: Sender succeeded SMTP AUTH, not delayed by milter-greylist-4.6.2 (ms.math.nagoya-u.ac.jp [0.0.0.0]); Thu, 31 Aug 2017 07:13:44 +0900 (JST) X-Virus-Scanned: clamav-milter 0.99.2 at bsdserver20 X-Virus-Status: Clean X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on bsdserver20.math.nagoya-u.ac.jp Subject: Re: [Caml-list] Typing issue in explicit module This is a known issue to fixing a long standing soundness problem in ocaml = 4.04 (I believe you are wrong in saying that it did work in 4.04, it should rath= er be 4.03 or 4.02). https://caml.inria.fr/mantis/view.php?id=3D7313 Basically, non-generalizable type variables in inner modules should be inst= antiated before leaving the module, if you want to instantiate them with local types. This is needed to ensure correct scoping in complex situations. Your solution is the correct one. Jacques Garrigue 2017/08/30 4:13, Paul A. Steckler : >=20 > Here's some code that compiles successfully with 4.05.0 ocamlc. The .ml f= ile is: >=20 > .ml file: > -- > type t > let id x =3D x > let idid =3D id id > -- > .mli file: > -- > type t > val id: 'a -> 'a > val idid : t -> t > -- >=20 > If I wrap the code in an explicit module, I get a type error: >=20 > .ml file: > -- > module Foo =3D > struct > > end > -- > .mli file: > -- > module Foo : > sig > > end > -- >=20 > With this change made, ocamlc complains: >=20 > -- > Error: The implementation Foo.ml does not match the interface Foo.cmi: > In module Foo: > Modules do not match: > sig type t =3D Foo.t val id : 'a -> 'a val idid : '_a -> '_a end > is not included in > sig type t val id : 'a -> 'a val idid : t -> t end > In module Foo: > Values do not match: > val idid : '_a -> '_a > is not included in > val idid : t -> t > -- >=20 > Adding a type annotation t -> t to the definition of "idid" gets rid > of the error. >=20 > With OCaml 4.04.0, no error occurs, and the type annotation is > unnecessary. Is this change expected? >=20 > The code I've shown is a simplified version of OCaml code extracted > from a Coq script, reported as a bug in Coq: > https://coq.inria.fr/bugs/show_bug.cgi?id=3D5705. >=20 > -- Paul >=20 > --=20 > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs