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 74A6480198 for ; Fri, 14 Jul 2017 03:01:01 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ivg@ieee.org; spf=Pass smtp.mailfrom=ivg@ieee.org; spf=None smtp.helo=postmaster@mail-yb0-f169.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of ivg@ieee.org) identity=pra; client-ip=209.85.213.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="ivg@ieee.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of ivg@ieee.org designates 209.85.213.169 as permitted sender) identity=mailfrom; client-ip=209.85.213.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="ivg@ieee.org"; 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-yb0-f169.google.com) identity=helo; client-ip=209.85.213.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="postmaster@mail-yb0-f169.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3Ah9dCERZoXPt7eHJUY1N+c7T/LSx+4OfEezUN459i?= =?us-ascii?q?sYplN5qZocu9bnLW6fgltlLVR4KTs6sC0LuJ9fi4EUU7or+5+EgYd5JNUxJXwe?= =?us-ascii?q?43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRp?= =?us-ascii?q?OOv1BpTSj8Oq3Oyu5pHfeQtFiT6/bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+?= =?us-ascii?q?RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPC?= =?us-ascii?q?TQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD?= =?us-ascii?q?0fOjA5/m/ZidF+grxHrx+6vRNz35TZbZuJOPZifK7Qe84RS2pbXsZWUixMGoCy?= =?us-ascii?q?b5UVAOoHIO1Wro79p0cJrRugGQasBOLvyiNThnTr2qA60vohEQ7d0QwhAd0Brm?= =?us-ascii?q?rboM/yNKcIXuC41a/FxijAYfNOwTrx9pTEfxQ7rfyPXb98a9TdxVQhGg/fk1md?= =?us-ascii?q?qIjoMjWI3eoXqWeb9fBvVee3hm4ntQ5xpj+vy98piobTh4IVzknI9CViz4opPN?= =?us-ascii?q?G4RlN3bN+gHZdKuCGaMIx2QswmQ252oio11roGuZujcCgLzpQo2QLfZuSZf4SU?= =?us-ascii?q?5h/vTuWcLDdiiH57Zb6yiQy+/VWhx+D4TsW01UxFritBktnCrHAN0BnT59CGSv?= =?us-ascii?q?tj8UeswjeP2B7N5e5aO0w0krDbK5E5zr4qipUTqVjDHjPxmEjukKCZbEAk+uyx?= =?us-ascii?q?5+TjY7XmvYOcOpRvigD+N6QugtawDf45MggIRWib+P6z2Kft/U3jE/12iag9m6?= =?us-ascii?q?zd9ZTbPthT8qWwBgsQ1oc49z6+CS2n2ZIWhy9UAkhCfUemkYHvc37JPPfmBve+?= =?us-ascii?q?n0/kxDZ1yNjHM7DsRJLXIS6Qw//aYb9h5hsEm0IIxtdF6scMBw=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BQBADgFmhZf6nVVdFdHAEBFgEBBQEBC?= =?us-ascii?q?gEXAQYBgjiCYweFH7ISA1yJWgdCFQEBAQEBAQEBAQEBEgEBCQsLCCYxgjMigm0?= =?us-ascii?q?EGQEBOBgNNwIkEgEFASKKNQ2RNZEbP4sfa4FsOoMFAQEFiD0IEoMWg02BYYshg?= =?us-ascii?q?mGJdIhGjHuUFJIplA0UH4EVNYEsgQIIYwaHEiQ2AYkMAQEB?= X-IPAS-Result: =?us-ascii?q?A0BQBADgFmhZf6nVVdFdHAEBFgEBBQEBCgEXAQYBgjiCYwe?= =?us-ascii?q?FH7ISA1yJWgdCFQEBAQEBAQEBAQEBEgEBCQsLCCYxgjMigm0EGQEBOBgNNwIkE?= =?us-ascii?q?gEFASKKNQ2RNZEbP4sfa4FsOoMFAQEFiD0IEoMWg02BYYshgmGJdIhGjHuUFJI?= =?us-ascii?q?plA0UH4EVNYEsgQIIYwaHEiQ2AYkMAQEB?= X-IronPort-AV: E=Sophos;i="5.40,356,1496095200"; d="scan'208,217";a="231517881" Received: from mail-yb0-f169.google.com ([209.85.213.169]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 14 Jul 2017 03:01:00 +0200 Received: by mail-yb0-f169.google.com with SMTP id f194so28414058yba.3 for ; Thu, 13 Jul 2017 18:00:59 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=ieee-org.20150623.gappssmtp.com; s=20150623; h=mime-version:from:date:message-id:subject:to; bh=LHChs5o9RXF7B9I0AoNjp/MH3BuPaavXDKyrLoxp438=; b=jhBvIFImSDZK6kmYId+zKZvXj7d4LsLHUBi5GC3VoEyVmjL7TK+dXjiLm3y/UV6sHl VWeulFNn7ykQ4PMysE5bq18DYAn3l/a2mRWxlqcnJneS6zD7FEL3yP5UlVxCU+YGORfl kZE80P/74CeROoOMNpBFyjzNWcouTvgJyNpo1oU6UBpKdKqac+Yo4TycUvIza8N3yThS yRwcV3WsqFgwtJIOGOqb0MajwEkK5PhMLemD0Qh43fbzj8yne/aaMS2xqbfaQAaWg23m 3UOsH8HsWnfa8hNORDVLuWy0cDJnrlJOOiVjz44+ftmuNsNN2BEyW+46hPPFFSjek0Df xwxw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:from:date:message-id:subject:to; bh=LHChs5o9RXF7B9I0AoNjp/MH3BuPaavXDKyrLoxp438=; b=TF4M6+4NAQo7Iy8wOxV1U1mb7hp9oUPBDQfzhlIiT/n+Lltr+swKP3UrxFvAUr8Z84 UjI9eYRDTsyXfnwfKGhEurYrFzgDaBp9YBlh0d0m+Kuhca+RHvbw/vkNPfAeiOu0dpOz q0o27wCrCBYJfAGdko/nCRqlAEWmr0SmFno+Rl6JTfowfcHcX3+GxVkhbTLSl8vZHZji Et3vS7yrHV2ZB2gDrb9ASon8jMi/YB/CBDtEHZU+tTeQ6U7i27aVzh5FWW6lx1BWXCLI uV5yYdSAPiq3n1mmgRTxcinU0XIH6UPlNHjYpm53CZzzNj8m0yDgaq0zRWdJuxHKdUOA hcTQ== X-Gm-Message-State: AIVw112lIDH6NJsPap4JhWSPU78a1OO8y7QhsKbKaEv2jek+rfGZN96f hwtZK5EGIb1IvGwieliCvk2o5fivFG+bwcY= X-Received: by 10.37.197.147 with SMTP id v141mr575435ybe.218.1499994058231; Thu, 13 Jul 2017 18:00:58 -0700 (PDT) MIME-Version: 1.0 Received: by 10.129.39.7 with HTTP; Thu, 13 Jul 2017 18:00:57 -0700 (PDT) From: Ivan Gotovchits Date: Thu, 13 Jul 2017 21:00:57 -0400 Message-ID: To: caml-list Content-Type: multipart/alternative; boundary="94eb2c1477d201bde405543c9565" Subject: [Caml-list] An inconsistency (possibly) in typing constraints with GADT --94eb2c1477d201bde405543c9565 Content-Type: text/plain; charset="UTF-8" Hi Everyone, 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 in the type checker? type ('a,'b) domain = Domain type 'd exp = Ret : 'a -> 'd exp constraint 'd = ('a,'b) domain Fails with: Error: Constraints are not satisfied in this type. Type 'd exp should be an instance of ('a, 'b) domain exp If we will express the same without GADT, it will be accepted, e.g., type 'd exp = Ret of 'a constraint 'd = ('a,'b) domain And, of course, we can make typechecker happy with type 'd exp = Ret : 'a -> ('a,'b) domain exp constraint 'd = ('a,'b) domain However, it will, somewhat, defeat the whole purpose of introducing the constraint, as I'm using constraints as a sort of type abstraction to bind type variables, and to my understanding the [constraint 'x = ] makes any occurrence of `'x` to be equivalent to the in its scope. Thanks, Ivan P.S. Of course, the provided example is a simplification of a real code, where the constraint is really needed. --94eb2c1477d201bde405543c9565 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Everyone,=C2=A0

I'm w= ondering, is the following type definition rejected because there is some f= undamental reason, that I'm missing, or this is just a missed case in t= he type checker?

=C2=A0 =C2=A0 type ('a,'b) domain =3D Domain
=
=C2=A0 =C2=A0 type 'd exp =3D Ret : '= a -> 'd exp constraint 'd =3D ('a,'b) domain

Fails with:=

=C2=A0 =C2=A0 =C2=A0Error: Constraints are not satisfied in this type= .
=C2=A0 =C2=A0 =C2=A0 =C2=A0Type 'd exp should be an instanc= e of ('a, 'b) domain exp
<= br>
If we will express the same without = GADT, it will be accepted, e.g.,

=C2=A0 =C2=A0=C2=A0type 'd exp = =3D Ret of 'a constraint 'd =3D ('a,'b) domain

And, of course, we can make typechecker happy with

=C2=A0 =C2=A0ty= pe 'd exp =3D Ret : 'a -> ('a,'b) domain exp constraint = 'd =3D ('a,'b) domain

However, it will, somewhat, defeat the wh= ole purpose of introducing the constraint, as I'm using constraints as = a sort of type abstraction to bind type variables, and to my understanding = the=C2=A0[constraint 'x =3D <type-expression>] makes any occurren= ce of `'x` to be equivalent to the <type-expression> in its scope= .=C2=A0

Thanks,
Ivan

P.S. Of course, the= provided example is a simplification of a real code, where the constraint = is really needed.=C2=A0
--94eb2c1477d201bde405543c9565--