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 0340381799 for ; Mon, 29 Jul 2013 10:52:29 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of arnaud.spiwack@gmail.com) identity=pra; client-ip=74.125.82.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="arnaud.spiwack@gmail.com"; x-sender="arnaud.spiwack@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of arnaud.spiwack@gmail.com designates 74.125.82.177 as permitted sender) identity=mailfrom; client-ip=74.125.82.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="arnaud.spiwack@gmail.com"; x-sender="arnaud.spiwack@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-we0-f177.google.com) identity=helo; client-ip=74.125.82.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="arnaud.spiwack@gmail.com"; x-sender="postmaster@mail-we0-f177.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AmUCAPQs9lFKfVKxk2dsb2JhbABbDoN9gxC7UwgWDgEBAQEHCwsJFAQkgiQBAQQBIx0BEiYBAwwBBQUEAQY3AgIiEgEFARwGiBEDCQaaRowAg1CELicNiFgBBQySXYEiA5dfj2cWKYFdgh9AOg X-IPAS-Result: AmUCAPQs9lFKfVKxk2dsb2JhbABbDoN9gxC7UwgWDgEBAQEHCwsJFAQkgiQBAQQBIx0BEiYBAwwBBQUEAQY3AgIiEgEFARwGiBEDCQaaRowAg1CELicNiFgBBQySXYEiA5dfj2cWKYFdgh9AOg X-IronPort-AV: E=Sophos;i="4.89,768,1367964000"; d="scan'208";a="22626930" Received: from mail-we0-f177.google.com ([74.125.82.177]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 29 Jul 2013 10:52:29 +0200 Received: by mail-we0-f177.google.com with SMTP id m46so3571168wev.8 for ; Mon, 29 Jul 2013 01:52:29 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; bh=9e/aV+7zfhQrRmorsNJBQpcCJdo9qnBenPSX5KWu1Nc=; b=Y096D9efoFVCKMkJunfVbjaz/ZzP9/Bpsk+mlCmK/R+5u2ye8V0lf0lUlY//tHT3DR x+NHDIZ7EVtRrsEt+H8wa4AwldPLh2F7Z+1/RL70OTXn/8TpuB4z3Y40tX6/iU34GBEw dhAVpfLDbWZcqV+VM+luYy+Uto909E8G0r6ICNsn71nnBIhKKL/HEmLxuXelGLoixKLR 2R4q08SFZzFgtXTH2Ymvz5TaoIFx8D32BZRlvI1Bo11789q0FCLUoolX3mLvBBW95jlE x0zx5wtTpmBXT8oBszzAzSUYtkORJKnQzOcTRVoZAPTkYNKOEgG+pfjUptHCumbrZc/6 mt8g== X-Received: by 10.180.74.134 with SMTP id t6mr4448998wiv.56.1375087949090; Mon, 29 Jul 2013 01:52:29 -0700 (PDT) MIME-Version: 1.0 Sender: arnaud.spiwack@gmail.com Received: by 10.217.137.134 with HTTP; Mon, 29 Jul 2013 01:51:49 -0700 (PDT) In-Reply-To: <059C2901-8AFE-4E28-B1D2-BC1D660CCA3A@math.nagoya-u.ac.jp> References: <059C2901-8AFE-4E28-B1D2-BC1D660CCA3A@math.nagoya-u.ac.jp> From: Arnaud Spiwack Date: Mon, 29 Jul 2013 10:51:49 +0200 X-Google-Sender-Auth: 9IXtMkPkICo5LJL5khZvRyqLJUU Message-ID: To: Jacques Garrigue Cc: Philippe Veber , caml users Content-Type: multipart/alternative; boundary=f46d043c820cbd961904e2a29c9e Subject: Re: [Caml-list] Narrowing a signature with a constrained type --f46d043c820cbd961904e2a29c9e Content-Type: text/plain; charset=UTF-8 > > 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 > an unconstrained one? > Actually, I don't know. > The unconstrained type does not enforce the invariants of the constrained > one, > but they will be checked as soon as you try to unify the two. > So it may be possible to lift this restriction. > It sounds pretty unlikely. If I have a functor taking a T in argument and I pass it a T with constraints, it's likely to be inconsistent. May I wonder, though, about the reason why T with blah should be a subtype of T? I must confess I fail to see the point. Arnaud --f46d043c820cbd961904e2a29c9e Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

=

Well, to ensure the coherence of the with constraints, we requi= re 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
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.
=C2=A0=
It sounds pretty unlikely. If I have a functor taking a T in= argument and I pass it a T with constraints, it's likely to be inconsi= stent.

May I wonder, though, about the reason why T with blah shoul= d be a subtype of T? I must confess I fail to see the point.


Arnaud
--f46d043c820cbd961904e2a29c9e--