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 A67357EF10 for ; Wed, 25 Feb 2015 23:46:39 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of mathieu.barbin@gmail.com) identity=pra; client-ip=209.85.216.43; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="mathieu.barbin@gmail.com"; x-sender="mathieu.barbin@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of mathieu.barbin@gmail.com designates 209.85.216.43 as permitted sender) identity=mailfrom; client-ip=209.85.216.43; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="mathieu.barbin@gmail.com"; x-sender="mathieu.barbin@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-qa0-f43.google.com) identity=helo; client-ip=209.85.216.43; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="mathieu.barbin@gmail.com"; x-sender="postmaster@mail-qa0-f43.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0DfAgB2UO5UmyvYVdFbg1RaBME0gWaHFwdDAQEBAQEBEAEBAQEBBgsLCRQuhBEEExUZARseAwERCQddAREBBQFXh3gBAwkIrQyDKz4xjRmCd444ChknDVSFEgEFDpQlBYpQgx2LO4EbhWuIfYF0EiOBFYQuIDGCQwEBAQ X-IPAS-Result: A0DfAgB2UO5UmyvYVdFbg1RaBME0gWaHFwdDAQEBAQEBEAEBAQEBBgsLCRQuhBEEExUZARseAwERCQddAREBBQFXh3gBAwkIrQyDKz4xjRmCd444ChknDVSFEgEFDpQlBYpQgx2LO4EbhWuIfYF0EiOBFYQuIDGCQwEBAQ X-IronPort-AV: E=Sophos;i="5.09,648,1418079600"; d="scan'208";a="123414472" Received: from mail-qa0-f43.google.com ([209.85.216.43]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 25 Feb 2015 23:46:39 +0100 Received: by mail-qa0-f43.google.com with SMTP id bm13so5178648qab.2 for ; Wed, 25 Feb 2015 14:46:38 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:date:message-id:subject:from:to:content-type; bh=N1xF5ApjiQf1Q0zkqx8IXOBIZQpxclI0KRaSwst3O1k=; b=oSnyHKqjAAmB/msNoOFDaUPfQbkKMLX3lhNYERpCYL77casKm9PSHxoYFmoxjok3rA RvU0504kuJ3e0NlustqCpW/+BvMX6DMOWtbQdApczKIjj20vnPcp65xqmBS7/knxenom 0lLuw1aB6TsYUgAE2CHN7VsxYcTq917gSdDlQDUMRpGLHWC0DO3im2lQbw87JMEiZki/ AdWTbb5rNQjPCX5+v+qTfu1z6TIy+89VVUtVEl7MF/yCuHDGhNXXLEXHxLhO0mv9k9p7 yfxFiNrn1vHOf8a9rSQi1UViuK7wf2gXvZPTESLav7hZu12QZRQt0/8+pvU6PXILW6sn iitA== MIME-Version: 1.0 X-Received: by 10.140.93.195 with SMTP id d61mr11429104qge.48.1424904397932; Wed, 25 Feb 2015 14:46:37 -0800 (PST) Received: by 10.229.95.5 with HTTP; Wed, 25 Feb 2015 14:46:37 -0800 (PST) Date: Wed, 25 Feb 2015 17:46:37 -0500 Message-ID: From: Mathieu Barbin To: caml-list@inria.fr Content-Type: multipart/alternative; boundary=001a113b95e27a4ed0050ff1682c Subject: [Caml-list] Signature substitution deleting an exposed type alias --001a113b95e27a4ed0050ff1682c Content-Type: text/plain; charset=ISO-8859-1 Dear list, I apologize in advance as I believe this has been discussed already in some very close forms, such as in the thread "Narrowing a signature with a constrained type" or a few other threads too. The other examples I've found in the archives I thought were maybe slightly more involving (containing either some type variable, type paramters, an object type, or type variable constraints, etc.). So in the hope that what I am trying to do might be simpler, here goes: $ cat > /tmp/a.ml module type A = sig type t = int val of_int : int -> t end module type B = sig type t include A with type t := t end $ ocamlopt /tmp/a.ml File "/tmp/a.ml", line 8, characters 10-28: Error: In this `with' constraint, the new definition of t does not match its original definition in the constrained signature: Type declarations do not match: type t = t is not included in type t = int File "/tmp/a.ml", line 2, characters 7-14: Expected declaration File "/tmp/a.ml", line 8, characters 17-28: Actual declaration EXIT STATUS 2 $ ocamlopt -version 4.00.1 In a previous answer from Jacques Garrigue I read that > 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. In the example, I am not sure what exactly are the signatures involved in the comparison, since the included signature does not contain the definition of the type t ( removed by the use of := ), and without the type [t] the signature are virtually identical. I've used the following workaround [1], however I was just wondering what was the reason behind the rejection. Thanks, Mathieu. [1] module type S = sig type t val of_int : int -> t end module type A = sig type t = int include S with type t := t end module type B = sig type t include S with type t := t end --001a113b95e27a4ed0050ff1682c Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
Dear list,

I apologize in ad= vance as I believe this has been discussed already in some very close forms= , such as in the thread "Narrowing a signature with a constrained type= " or a few other threads too.=A0 The other examples I've found in = the archives I thought were maybe slightly more involving (containing eithe= r some type variable, type paramters, an object type, or type variable cons= traints, etc.).=A0 So in the hope that what I am trying to do might be simp= ler, here goes:

$ cat > /tmp/a.ml
module type A =3D sig
=A0 type t = =3D int
=A0 val of_int : int -> t
end

=
module type B =3D sig
=A0 type t
=A0 include= A with type t :=3D t
end

$ o= camlopt /tmp/a.ml
File "/tmp/a.ml", line 8, characters 10-28:
Er= ror: In this `with' constraint, the new definition of t
=A0 = =A0 =A0 =A0does not match its original definition in the constrained signat= ure:
=A0 =A0 =A0 =A0Type declarations do not match:
=A0= =A0 =A0 =A0 =A0type t =3D t
=A0 =A0 =A0 =A0is not included in
=A0 =A0 =A0 =A0 =A0type t =3D int
=A0 =A0 =A0 =A0File &qu= ot;/tmp/a.ml", line 2, characters 7-14: Ex= pected declaration
=A0 =A0 =A0 =A0File "/tmp/a.ml", line 8, characters 17-28: Actual declaration
=
EXIT STATUS 2

$ ocamlopt -version<= /div>
4.00.1

In a previous answer f= rom Jacques Garrigue I read that=A0

> 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 obje= ct).
> This is where your code gets rejected.

In the example, I am not sure what exactly are the signatures invo= lved in the comparison, since the included signature does not contain the d= efinition of the type t ( removed by the use of :=3D ), and without the typ= e [t] the signature are virtually identical.

I've used the following workaround [1], however I was just wondering w= hat was the reason behind the rejection.

Thanks,
Mathieu.

[1]
module type S= =3D sig
=A0 type t
=A0 val of_int : int -> t
<= div>end

module type A =3D sig
=A0 type t= =3D int
=A0 include S with type t :=3D t
end

module type B =3D sig
=A0 type t
=A0 in= clude S with type t :=3D t
end

--001a113b95e27a4ed0050ff1682c--