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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 6D52381799 for ; Sat, 27 Jul 2013 01:36:02 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail2-smtp-roc.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 (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail2-smtp-roc.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 (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AmEEALcG81GFBoIFdGdsb2JhbABbwWeBLw4BDBUIPIIkAQEEAUMBNQIDCws0EiE2BhOHfgMJBaZWhEgChHsNV4gAB40VgjUzB4MWb4krjE6BaYwmiEk X-IPAS-Result: AmEEALcG81GFBoIFdGdsb2JhbABbwWeBLw4BDBUIPIIkAQEEAUMBNQIDCws0EiE2BhOHfgMJBaZWhEgChHsNV4gAB40VgjUzB4MWb4krjE6BaYwmiEk X-IronPort-AV: E=Sophos;i="4.89,754,1367964000"; d="scan'208";a="27470482" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 27 Jul 2013 01:35:59 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 4799A6389; Sat, 27 Jul 2013 08:35:57 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id C0725396F; Sat, 27 Jul 2013 08:35:56 +0900 (JST) DomainKey-Signature: h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 815DF395E; Sat, 27 Jul 2013 08:35:56 +0900 (JST) Content-Type: text/plain; charset=iso-8859-1 Mime-Version: 1.0 (Mac OS X Mail 6.5 \(1508\)) From: Jacques Garrigue In-Reply-To: Date: Sat, 27 Jul 2013 08:35:59 +0900 Cc: caml users Content-Transfer-Encoding: quoted-printable Message-Id: <059C2901-8AFE-4E28-B1D2-BC1D660CCA3A@math.nagoya-u.ac.jp> References: To: Philippe Veber X-Mailer: Apple Mail (2.1508) Subject: Re: [Caml-list] Narrowing a signature with a constrained type On 2013/07/26, at 22:32, Philippe Veber wrote: > Dear camlers, >=20 > Out of curiosity, I'd be happy to understand why the following definition= is rejected: >=20 > # module type T =3D sig type 'a format end;; > module type T =3D sig type 'a format end > # module F(X : T with type 'a format =3D 'a list constraint 'a =3D < .. >= ) =3D struct end;; > File "", line 1, characters 13-67: = Error: In this `with' c= onstraint, the new definition of format does not match its original definit= ion in the constrained signature:=20=20=20=20=20=20=20=20=20=20=20=20=20=20= =20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20 > Type declarations do not match: type 'a format =3D 'a0 list is not includ= ed in type 'a format=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20= =20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20= =20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20=20 > Their constraints differ. >=20 > Would it be unsound to allow it? Well, to ensure the coherence of the with constraints, we require that the new signature be a subtype of the original one (as a module, not as an = object). This is where your code gets rejected. Now why is it deemed unsafe to allow a constrained type definition to be a = subtype of=20 an unconstrained one? Actually, I don't know. The unconstrained type does not enforce the invariants of the constrained o= ne, but they will be checked as soon as you try to unify the two. So it may be possible to lift this restriction. However, there are technical difficulties in comparing a constrained defini= tion with an unconstrained one, so this might just be the main reason. This would also have an impact on the invariants of types through abstracti= on. Jacques=