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 1302E7F0A3 for ; Sat, 5 Sep 2015 00:19:27 +0200 (CEST) IronPort-PHdr: 9a23:QD+bbBSjNt4x61VJKUKI0D2KIdpsv+yvbD5Q0YIujvd0So/mwa64bRSN2/xhgRfzUJnB7Loc0qyN4/ymATNLuczJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvip9uLPE4Q3nKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGY2zRakzTKRZATI6KCh1oZSz7ViQBTeIs14VSGYLiVJtBBTZ6FmuW57rsTbh8O96xDWeFcLzRLEwHz+l6vE4ZgXvjXIlPjUg7WzMwuN5lrharw+s70hwypTOYY6IOdJ7d7/dO9UTSm1QV4NMESVKRIGkOdhcR9EdNPpV+tGu72AFqgGzUEz1XLvi Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jacques.garrigue@gmail.com; spf=Pass smtp.mailfrom=jacques.garrigue@gmail.com; spf=None smtp.helo=postmaster@mail-pa0-f50.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of jacques.garrigue@gmail.com) identity=pra; client-ip=209.85.220.50; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jacques.garrigue@gmail.com"; x-sender="jacques.garrigue@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of jacques.garrigue@gmail.com designates 209.85.220.50 as permitted sender) identity=mailfrom; client-ip=209.85.220.50; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jacques.garrigue@gmail.com"; x-sender="jacques.garrigue@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-pa0-f50.google.com) identity=helo; client-ip=209.85.220.50; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jacques.garrigue@gmail.com"; x-sender="postmaster@mail-pa0-f50.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0A9AQAAGOpVlDLcVdFdhF6tE5BPAQmJLTgUAQEBAQEBAQEQAQEBAQcLCwkfMIIdggcBAQQSFRMGATgBAwwBBQUYLiETAQUBHAYTIod3AxIFqQeBLz4xkCWKHCcNR4Q9AQEBAQYBAQEBAQEBFQEFDoh0gmyCT4VbgRQFjWyHZYsKgW2IaQ+KPIVwNYEXYINmUYlLAQEB X-IPAS-Result: A0A9AQAAGOpVlDLcVdFdhF6tE5BPAQmJLTgUAQEBAQEBAQEQAQEBAQcLCwkfMIIdggcBAQQSFRMGATgBAwwBBQUYLiETAQUBHAYTIod3AxIFqQeBLz4xkCWKHCcNR4Q9AQEBAQYBAQEBAQEBFQEFDoh0gmyCT4VbgRQFjWyHZYsKgW2IaQ+KPIVwNYEXYINmUYlLAQEB X-IronPort-AV: E=Sophos;i="5.17,470,1437429600"; d="scan'208";a="176108253" Received: from mail-pa0-f50.google.com ([209.85.220.50]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 05 Sep 2015 00:19:26 +0200 Received: by padhy16 with SMTP id hy16so33782259pad.1 for ; Fri, 04 Sep 2015 15:19:24 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=sender:subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; bh=VKRWccNoBqfixwaTvMz5N7D5I+9wH3RV8E4OdWWmGi8=; b=RDZqf02tgkQRBmt3MYAi8bbhat2SfWHKlFxGzoUVNcJxw7mT+r4nBkIqdgdwv8izUL QurmXHuRexAYpfTVPChjRIT56MVLeBLIISz03J47gu5T9tG6wuNUUk8N1Cf2aJaCbbil LnIxU7J8N+ZlctmmfnBt0/vSmGATcPPQCwaZRhJhKY4VJMbNkRRF455AI5X+qcgdX9cO GXz3DMH+UmDoEbW2gcQYoN3OCNSIO/f0FtAeQCCkJ6pOnb70Bg7WdItORtNkT1/3vudU eoxN/ivPVQ5vc4JZcZQmG7ZkRhWFNt3HemX7G2gRN/KE0usTlfzAlrGd/QyGJrGcrZ3e PkDw== X-Received: by 10.66.190.99 with SMTP id gp3mr12830361pac.113.1441405164503; Fri, 04 Sep 2015 15:19:24 -0700 (PDT) Received: from [10.20.30.234] ([72.2.55.21]) by smtp.gmail.com with ESMTPSA id uy4sm3143697pbc.69.2015.09.04.15.19.23 (version=TLS1 cipher=ECDHE-RSA-RC4-SHA bits=128/128); Fri, 04 Sep 2015 15:19:23 -0700 (PDT) Sender: Jacques Garrigue Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) Content-Type: text/plain; charset=us-ascii From: Jacques Garrigue In-Reply-To: Date: Fri, 4 Sep 2015 15:19:20 -0700 Cc: OCaml List Content-Transfer-Encoding: 7bit Message-Id: References: To: Markus Mottl X-Mailer: Apple Mail (2.2104) Subject: Re: [Caml-list] Late adding of type variable constraints On 2015/09/04 13:28, Markus Mottl wrote: > > Hi, > > I wonder whether there is a way to add constraints to type variables > in signatures after the signature was defined. E.g.: > > --- > module type S = sig > type 'a t > type ('a, 'b) mappers > > val map : ('a, 'b) mappers -> 'a t -> 'b t > end > > module type T = sig > type 'a t constraint 'a = unit (* whatever *) > include S with type 'a t := 'a t > end > --- > > The above will fail, because 'a has additional constraints for type > "t" in signature "T". If I write instead e.g. "type 'a t = 'a list", > this will work and also constrain the signature to something narrower. > What makes constraints on polymorphic variables special here? Consider this signature: module type S = sig type 'a t type 'a u = U of 'a t constraint 'a = < m: int; .. > end Now the signature S with type 'a constraint 'a t = unit is ill-typed, but to see it you must type-check again all of its contents (not just the definition of t). This is the reason you cannot do that. Jacques Garrigue