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 A9524801DD for ; Wed, 30 Aug 2017 10:29:16 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=garrigue@math.nagoya-u.ac.jp; spf=None smtp.mailfrom=garrigue@math.nagoya-u.ac.jp; spf=None smtp.helo=postmaster@ms.math.nagoya-u.ac.jp Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.11; receiver=mail3-smtp-sop.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 (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.11; receiver=mail3-smtp-sop.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 (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@ms.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.11; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@ms.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AlIC74hVvduSN0bEit+NMCX4KzS/V8LGtZVwlr6E/?= =?us-ascii?q?grcLSJyIuqrYZhSEt8tkgFKBZ4jH8fUM07OQ6P+wHzFYqb+681k8M7V0Hycfjs?= =?us-ascii?q?sXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aMlzFOAF0?= =?us-ascii?q?PuX4HJLJx4Tyjrjqus6bXwIdpSS0Z/tdKwmxsw7Rt9UNyd9jNKkZyxbErz1PYe?= =?us-ascii?q?sAlk1yIlfGvR/3/9q959ZM+j5Kuv08+oYUXqzgZaU3ULFwCT06MyYz7cLspBCG?= =?us-ascii?q?UE2G7T0eSjNFwVJzHwHZ4USiDd/KuSzgu784gXHCMA=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DMAAC7dqZZlwuCBoVeGQEBAQEBAQEBA?= =?us-ascii?q?QEBBwEBAQEBFAEBAQEBAQEBAQEBBwEBAQEBhBaBEoN3ixKRF5YnghIBhUYChFk?= =?us-ascii?q?XAQEBAQEBAQEBAQESAQEBAQEIFgZXgjMFAR4BBYI7AQEBAQIBIwQZAQE3AQQLC?= =?us-ascii?q?w4KAgImAgJXBoo8B6xUa4FtOoMIAQEFhF0ag0ABAQEBAQEBAwEBAQEBAQEBAQE?= =?us-ascii?q?WCIENgh2FMyuCfYR1gxMwgjGHbAeCJogdWY1elEyLUocZkWyEViEDgUBTOUkSA?= =?us-ascii?q?YJyggQfggIxNokagVMBAQE?= X-IPAS-Result: =?us-ascii?q?A0DMAAC7dqZZlwuCBoVeGQEBAQEBAQEBAQEBBwEBAQEBFAE?= =?us-ascii?q?BAQEBAQEBAQEBBwEBAQEBhBaBEoN3ixKRF5YnghIBhUYChFkXAQEBAQEBAQEBA?= =?us-ascii?q?QESAQEBAQEIFgZXgjMFAR4BBYI7AQEBAQIBIwQZAQE3AQQLCw4KAgImAgJXBoo?= =?us-ascii?q?8B6xUa4FtOoMIAQEFhF0ag0ABAQEBAQEBAwEBAQEBAQEBAQEWCIENgh2FMyuCf?= =?us-ascii?q?YR1gxMwgjGHbAeCJogdWY1elEyLUocZkWyEViEDgUBTOUkSAYJyggQfggIxNok?= =?us-ascii?q?agVMBAQE?= X-IronPort-AV: E=Sophos;i="5.41,448,1498514400"; d="scan'208";a="235699856" Received: from bsd20.math.nagoya-u.ac.jp (HELO ms.math.nagoya-u.ac.jp) ([133.6.130.11]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 30 Aug 2017 10:29:14 +0200 Received: from [192.168.1.156] (bsdserver10-alias1.math.nagoya-u.ac.jp [172.16.62.1]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ms.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id C5A4F5160A8; Wed, 30 Aug 2017 17:22:18 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=math.nagoya-u.ac.jp; s=20160220; t=1504081338; bh=WvQa3MqWfsyMz+cBD5DHhJ4YD188r/YlW2fNnF9m1z0=; h=Subject:From:In-Reply-To:Date:Cc:References:To; b=NF6wEvPtYv8ox47+LB6XUlwxvxrtsfxQUtw7NwwfI0tqwshSggKm1IJmGY+nBqB6J nexprXzU9HltQcGRPQmD8i6kmyFerZvLp/pcH7Krs7nslgFHDOJb2DVclYk70dT3WO Qc35w7pqgXHH2SHorZUD4xGrZSG5sdBiL2bcsnfQ= Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 10.3 \(3273\)) From: Jacques Garrigue In-Reply-To: Date: Wed, 30 Aug 2017 17:29:05 +0900 Cc: Mailing List OCaml Content-Transfer-Encoding: quoted-printable Message-Id: References: To: Ivan Gotovchits X-Mailer: Apple Mail (2.3273) X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.6.2 (ms.math.nagoya-u.ac.jp [0.0.0.0]); Wed, 30 Aug 2017 17:22:18 +0900 (JST) X-Virus-Scanned: clamav-milter 0.99.2 at bsdserver20 X-Virus-Status: Clean X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on bsdserver20.math.nagoya-u.ac.jp Subject: Re: [Caml-list] An inconsistency (possibly) in typing constraints with GADT Sorry for the slow answer, On 2017/07/14 10:00, Ivan Gotovchits wrote: >=20 > Hi Everyone,=20 >=20 > I'm wondering, is the following type definition rejected because there is= some fundamental reason, that I'm missing, or this is just a missed case i= n the type checker? >=20 > type ('a,'b) domain =3D Domain > type 'd exp =3D Ret : 'a -> 'd exp constraint 'd =3D ('a,'b) domain >=20 > Fails with: >=20 > Error: Constraints are not satisfied in this type. > Type 'd exp should be an instance of ('a, 'b) domain exp The problem is the scope of =E2=80=98d in the definition of exp above. It is actually equivalent to type =E2=80=98d exp =3D Ret : =E2=80=98a -> =E2=80=98e exp constraint = =E2=80=98d =3D (=E2=80=98a,=E2=80=99 b) domain I.e. type variables in GADT clauses use a completely different scope, which= ignores constraint clauses. This makes combining GADTs and constraint very awkward. On the other hand, a different semantics would be cumbersome too. Jacques Garrigue > If we will express the same without GADT, it will be accepted, e.g., >=20 > type 'd exp =3D Ret of 'a constraint 'd =3D ('a,'b) domain >=20 >=20 > And, of course, we can make typechecker happy with >=20 > type 'd exp =3D Ret : 'a -> ('a,'b) domain exp constraint 'd =3D ('a,'= b) domain >=20 > However, it will, somewhat, defeat the whole purpose of introducing the c= onstraint, as I'm using constraints as a sort of type abstraction to bind t= ype variables, and to my understanding the [constraint 'x =3D ] makes any occurrence of `'x` to be equivalent to the in its scope.=20 >=20 > Thanks, > Ivan >=20 > P.S. Of course, the provided example is a simplification of a real code, = where the constraint is really needed.=20