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 1A16F81799 for ; Fri, 26 Jul 2013 15:32:39 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of philippe.veber@gmail.com) identity=pra; client-ip=209.85.212.169; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="philippe.veber@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of philippe.veber@gmail.com designates 209.85.212.169 as permitted sender) identity=mailfrom; client-ip=209.85.212.169; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="philippe.veber@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-wi0-f169.google.com) identity=helo; client-ip=209.85.212.169; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="postmaster@mail-wi0-f169.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgACAJ958lHRVdSpk2dsb2JhbABahAu+UwgWDgEBAQEHCwsJFAQkgmsBGx4DEgkBBl0BEQEFASKIEAEDD5hNgn6MT4J/hFoKGScNZId0AQUMk30Dl1+PZxYphDw6 X-IPAS-Result: AgACAJ958lHRVdSpk2dsb2JhbABahAu+UwgWDgEBAQEHCwsJFAQkgmsBGx4DEgkBBl0BEQEFASKIEAEDD5hNgn6MT4J/hFoKGScNZId0AQUMk30Dl1+PZxYphDw6 X-IronPort-AV: E=Sophos;i="4.89,751,1367964000"; d="scan'208";a="27429539" Received: from mail-wi0-f169.google.com ([209.85.212.169]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 26 Jul 2013 15:32:38 +0200 Received: by mail-wi0-f169.google.com with SMTP id c10so894491wiw.2 for ; Fri, 26 Jul 2013 06:32:38 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:from:date:message-id:subject:to:content-type; bh=qnOiYXTHF15+LtGFUNkslREFv3OTZw2pc7tkVv+hBC0=; b=JhXB+wCPnYpYFUdV4V6WQ4Gh4fvDU64hNFLxJANnpZBBxrHADC0bciuliz8XLuYBYK honLuwiwVTXC1VyU0t35QDwX/V9Cg4uTPB4UWH7Np6Q5wNL/jNXiLOKPj6Jpm27LRbUy bvw7LJqt9czO40w0F4SQfNqbUVT8yz9XGAPOnwezsq9q6Im+ZkZcB8I9h0S3PepXNSdO Ymrqz7jhOT0XNNLYQe58gB2Ukxi6j8dBXNGIxT+JSjyMaDCVn9g1Nnfh8uD+ajmvX11z Ynnc0OHgLCy9QW5nbtm2hkT6PEBa/2waMqnBq0a9aezc1tlds/CR/3u0JOqpnC8mGLhA EenQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=20120113; h=mime-version:from:date:message-id:subject:to:content-type; bh=qnOiYXTHF15+LtGFUNkslREFv3OTZw2pc7tkVv+hBC0=; b=RiTxqlLZrHKQ+FNajSvE9poL1ZOMil74mrTB7hI6Uu5lZdNDEjY09ekwwDHtg0Jzz6 5VEtz7C0iwREF8RC2/VyfbLzomNOwtStEJ3NZmaqZkTx+jY83JEom7HCnprg8eBVdtVp nv7y4IQ3YXAArxybOFcFh8N6CYPfW5B6vfbmMEY0HcGG3IhwyKtmGq3WMaghxHG+Dvnl qbsfNj4rxf28Zg8fMwTEfSrLjl1HyVsuYVrXsIJEy4wpkxPAFpEEOELrF4R2/9RpRLY8 SLGZgE2y0zOEsWawBmgeXPmkWI5/f4sqcuys8AgplMaGPQ/JN3RQFx3XkwdShRrhKlYO INqA== X-Received: by 10.180.21.229 with SMTP id y5mr5766286wie.17.1374845558224; Fri, 26 Jul 2013 06:32:38 -0700 (PDT) MIME-Version: 1.0 Received: by 10.194.41.138 with HTTP; Fri, 26 Jul 2013 06:32:18 -0700 (PDT) From: Philippe Veber Date: Fri, 26 Jul 2013 15:32:18 +0200 Message-ID: To: caml users Content-Type: multipart/alternative; boundary=047d7bb709981e897d04e26a2dec X-Validation-by: philippe.veber@gmail.com Subject: [Caml-list] Narrowing a signature with a constrained type --047d7bb709981e897d04e26a2dec Content-Type: text/plain; charset=ISO-8859-1 Dear camlers, Out of curiosity, I'd be happy to understand why the following definition is rejected: # module type T = sig type 'a format end;; module type T = sig type 'a format end # module F(X : T with type 'a format = 'a list constraint 'a = < .. >) = struct end;; File "", line 1, characters 13-67: Error: In this `with' constraint, the new definition of format does not match its original definition in the constrained signature: Type declarations do not match: type 'a format = 'a0 list is not included in type 'a format Their constraints differ. Would it be unsound to allow it? Cheers, ph. --047d7bb709981e897d04e26a2dec Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
Dear camlers,

Out of curiosity, I'd be happy to= understand why the following definition is rejected:

# module type T =3D sig type 'a for= mat end;;
module type T =3D sig typ= e 'a format end
<= span style=3D"font-family:courier new,monospace"># module F(X : T with type= 'a format =3D 'a list constraint 'a =3D < .. >) =3D stru= ct end;;
File "", line 1= , characters 13-67:=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 Error: I= n this `with' constraint, the new definition of format does not match i= ts original definition in the constrained signature:=A0=A0=A0=A0=A0=A0=A0= =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0
Type declarations do not match: type 'a format =3D 'a0 list is not = included in type 'a format=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0
=A0=A0=A0=A0=A0=A0 Their = constraints differ.
<= br>Would it be unsound to allow it?

Cheers,

ph.
--047d7bb709981e897d04e26a2dec--