From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 D08757ED11 for ; Sat, 17 Sep 2016 19:39:00 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=markus.mottl@gmail.com; spf=Pass smtp.mailfrom=markus.mottl@gmail.com; spf=None smtp.helo=postmaster@mail-io0-f170.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of markus.mottl@gmail.com) identity=pra; client-ip=209.85.223.170; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of markus.mottl@gmail.com designates 209.85.223.170 as permitted sender) identity=mailfrom; client-ip=209.85.223.170; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@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-io0-f170.google.com) identity=helo; client-ip=209.85.223.170; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="postmaster@mail-io0-f170.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AqLP4gRXKaoI2p75xd7HQlI1iu1zV8LGtZVwlr6E/?= =?us-ascii?q?grcLSJyIuqrYZhWHt8tkgFKBZ4jH8fUM07OQ6PG5HzxYqs/Z6DhCKMUKDEBVz5?= =?us-ascii?q?1O3kQJO42sNw7SFLbSdSs0HcBPBhdO3kqQFgxrIvv4fEDYuXao7DQfSV3VPAtx?= =?us-ascii?q?IfnpSMaJ15zkn8j7wZDYYh1JiTyhevsyaUzu9USC/vUR1KxJI6M1gj/IuWcAL+?= =?us-ascii?q?9fwGctIVOIgz794N2x9dht6XIDlegm8ptlWL/5Yr9waLtEEDBuZ2U8/s72rl/G?= =?us-ascii?q?SheT4lMTV2wXllxDBA2Tv0KyZYv4riav7rk14yKdJ8CjCOlsATk=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BuAACYft1Xh6rfVdFeHQYMGAEXAQYBg?= =?us-ascii?q?wMBAQEBATw5fAeNLJdwBJNJggMchz4HOBQBAQEBAQEBAQEBARIBAQEIDQkJGS+?= =?us-ascii?q?CMgQBFQEEgikRBBkBFAceAxIQDwImAiMBAREBBQEiEyKIDQEDF6YTggeBMj4yi?= =?us-ascii?q?z2Ba4JfBYNbChknDVSCfAIGEHaFMYcbhH+CWgWZOjWBZYsHgnCPaohVhkgTHoE?= =?us-ascii?q?RHkuCJ1SBdiI0hhaBQAEBAQ?= X-IPAS-Result: =?us-ascii?q?A0BuAACYft1Xh6rfVdFeHQYMGAEXAQYBgwMBAQEBATw5fAe?= =?us-ascii?q?NLJdwBJNJggMchz4HOBQBAQEBAQEBAQEBARIBAQEIDQkJGS+CMgQBFQEEgikRB?= =?us-ascii?q?BkBFAceAxIQDwImAiMBAREBBQEiEyKIDQEDF6YTggeBMj4yiz2Ba4JfBYNbChk?= =?us-ascii?q?nDVSCfAIGEHaFMYcbhH+CWgWZOjWBZYsHgnCPaohVhkgTHoERHkuCJ1SBdiI0h?= =?us-ascii?q?haBQAEBAQ?= X-IronPort-AV: E=Sophos;i="5.30,352,1470693600"; d="scan'208";a="237219159" Received: from mail-io0-f170.google.com ([209.85.223.170]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 17 Sep 2016 19:39:00 +0200 Received: by mail-io0-f170.google.com with SMTP id m186so56328027ioa.2 for ; Sat, 17 Sep 2016 10:39:00 -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; bh=wjRIkzWZipjDdcUME/yhd+Rk0WI3/ggdZlLtsbAGEAY=; b=y/qVipqDB/tHZSgHivDdaLxfTPbUf2aRDW7kweJP6ZgS2pcFG6QzdzY1NMClWcZqxe 3M+lHy3r7I02OPzForPnWjSZfyFTheKnIJlunlXpYRiZipJiU5NmQHaSKEJDbgSq2sgh F7b8vp2e4VavTLgnfuzVVIy7mTav8iMdx7cQ9NvJBo6xvwCr2/OuHOD6HUdoiJuF4gMB DGVihc6tf8Tz5dL0VBMX5zlhbSRdxmEQsCA79OSqsg2las5iZcz4krBchjkBJdk+WNSP WipmqYPCzcosjVMOlhobaFVvVIMFu3fCM0oDZB56NaB14DZsz+Qxl3A/H8hmn5vjucTU 4WWA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:from:date:message-id:subject:to; bh=wjRIkzWZipjDdcUME/yhd+Rk0WI3/ggdZlLtsbAGEAY=; b=j7CpY/UmIGlQ4ZWoc0Xu8aIpBTV5DkYl+BgbSbGG5BkPQ5ufpryZYYBFHQbrKtylk4 FWsmLgPwInHYLOiZVeFsSmOp7jUg3/2w5nhBg0aKPRCsev8gDLHF5w8B9gXoCC04f+sw LBnpNUao/aUycMbbuinp36FS7ygoAf+3aWmOVzrRkFNe1nmojjgSgAj6xyIbCybp3gG8 /IpEAlX0sOyxt8+flta1E7gfbukcULv4ySzGmMMcr/9Y7OHbcfm+RUApzSPUKt2x59Nq bO1G5PdHsmKYFl2sWEp2weNBYlw5K/kVu6977zp76wdhEOAIFykhkQRd2d4atJo4rx46 bxEQ== X-Gm-Message-State: AE9vXwOIO8Gv4XFnzqCgldexaqM+KUEqn6JHPgXGO50M14rry0/Lp+1LCQHK87lQneuzYhrDaB/D+KzpaAMGsQ== X-Received: by 10.107.185.3 with SMTP id j3mr29497524iof.3.1474133938653; Sat, 17 Sep 2016 10:38:58 -0700 (PDT) MIME-Version: 1.0 Received: by 10.107.131.219 with HTTP; Sat, 17 Sep 2016 10:38:58 -0700 (PDT) From: Markus Mottl Date: Sat, 17 Sep 2016 13:38:58 -0400 Message-ID: To: OCaml List Content-Type: text/plain; charset=UTF-8 Subject: [Caml-list] Covariant GADTs Hi, GADTs currently do not allow for variance annotations so I wondered whether there are any workarounds for what I want: ----- type +_ t = | Z : [ `z ] t | S : [ `z | `s ] t -> [ `s ] t let get_next (s : [ `s ] t) = match s with | S next -> next ----- The above compiles without the variance annotation, but then you cannot express "S Z", because there is no way to coerce Z to be of type [`z | `s] t. Another approach I tried is the following: ----- type _ t = | Z : [ `z ] t | S : [< `z | `s ] t -> [ `s ] t let get_next (s : [ `s ] t) : [< `z | `s ] t = match s with | S next -> next ----- The above gives the confusing error: ----- Error: This expression has type [< `s | `z ] t but an expression was expected of type [< `s | `z ] t The type constructor $S would escape its scope ----- There are apparently two type variables associated with [< `s | `z ] t: the locally existential one introduced by matching the GADT, and the one in the type restriction of the function, but the compiler cannot figure out that these can be safely unified. There is currently no way of specifying locally abstract types that have type constraints, which could possibly also help here. Are there workarounds to achieve the above? Are there any plans to add variance annotations for GADTs? Regards, Markus -- Markus Mottl http://www.ocaml.info markus.mottl@gmail.com