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 640997FD90 for ; Tue, 27 Dec 2016 21:05:03 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=antronbachin@gmail.com; spf=Pass smtp.mailfrom=antronbachin@gmail.com; spf=None smtp.helo=postmaster@mail-it0-f66.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of antronbachin@gmail.com) identity=pra; client-ip=209.85.214.66; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="antronbachin@gmail.com"; x-sender="antronbachin@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of antronbachin@gmail.com designates 209.85.214.66 as permitted sender) identity=mailfrom; client-ip=209.85.214.66; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="antronbachin@gmail.com"; x-sender="antronbachin@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-it0-f66.google.com) identity=helo; client-ip=209.85.214.66; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="antronbachin@gmail.com"; x-sender="postmaster@mail-it0-f66.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AU+ELKhcnT03E/eETUrqEzrgBlGMj4u6mDksu8pMi?= =?us-ascii?q?zoh2WeGdxc66YB7h7PlgxGXEQZ/co6odzbGH7+a4ASdZuM7J8ChbNscTB1ld0Y?= =?us-ascii?q?RetjdjKfDGIHWzFOTtYS0+EZYKf35e1Fb/D3JoHt3jbUbZuHy44G1aMBz+MQ1o?= =?us-ascii?q?Ora9QdaK3Izkn9y1rtfYagBMwT68eq9aLROsrAyXuNNenJBvML17gk/Cq35MPu?= =?us-ascii?q?BX3n9AJFSJnh+66N3mr7B59CEFkvQ98MgIe6zxf6U+BehRCig8NGY/7cbrtB/r?= =?us-ascii?q?Qg6G539aWWITxEkbSzPZ5Q33C8+i+hDxsfBwjXGX?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CTAQDQyGJYWELWVdFdHgYMGQYMgmclA?= =?us-ascii?q?QEBAQEfHgFAgQyDb6kgiiGEGSqHTUIRAQEBAQEBAQEBAQEFARcWBx0ygjMYgks?= =?us-ascii?q?TBgEbDwMMAxIQXhEBBQEIGi6IOQEDGAENnDiDPz+NbRgFARyDCwWDVAoZJw1Ug?= =?us-ascii?q?mUBAQEBBgEBAQEBARoCBgkBCIg4CIluC1qCMAWIbYcVinuGVIprgkaBB4ZJhkC?= =?us-ascii?q?OG4JdMoEUNYEpUQ4BA4FEggGCKFOIVwEBAQ?= X-IPAS-Result: =?us-ascii?q?A0CTAQDQyGJYWELWVdFdHgYMGQYMgmclAQEBAQEfHgFAgQy?= =?us-ascii?q?Db6kgiiGEGSqHTUIRAQEBAQEBAQEBAQEFARcWBx0ygjMYgksTBgEbDwMMAxIQX?= =?us-ascii?q?hEBBQEIGi6IOQEDGAENnDiDPz+NbRgFARyDCwWDVAoZJw1UgmUBAQEBBgEBAQE?= =?us-ascii?q?BARoCBgkBCIg4CIluC1qCMAWIbYcVinuGVIprgkaBB4ZJhkCOG4JdMoEUNYEpU?= =?us-ascii?q?Q4BA4FEggGCKFOIVwEBAQ?= X-IronPort-AV: E=Sophos;i="5.33,418,1477954800"; d="scan'208";a="251943041" Received: from mail-it0-f66.google.com ([209.85.214.66]) by mail2-smtp-roc.national.inria.fr with ESMTP; 27 Dec 2016 21:05:02 +0100 Received: by mail-it0-f66.google.com with SMTP id 75so34366086ite.1 for ; Tue, 27 Dec 2016 12:05:02 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:content-transfer-encoding:mime-version:subject:message-id:date :to; bh=iKpjuRBVjVxg+qcNmfzx4OedFNtxzWxRJ1948k/PJkg=; b=BirgRT/8yjiQ4wur75DBKp9SYyih3qUDaDbDBcLFpkBXv7MFmJ6IO5gbRNMKGpfKU/ ElXVi3nVZGze/ofDOorVVNYOHw5bM0z4ZRUKZfc6yPUXDwonANxtQmAXuU9cQs2I2tEh XVCBQMgpIDdHu3zkdU3M1ncaN+vF3X+K1u9wXeGhjBOp6dP8+6JPGX2HbW9jmYNu8SfW 1ZlFkKPTM4YNVq3wNXwlXt6ap2yzZYm+ZPP17wrDonqD/30Gx6PCCZMChDriljstk4tg VSe7Nm+4dPthaUCMX/lb/ZA3b85/xpm33S+rk/o21jNKBK3lFeAOdvw5SG7siurONr1a 801Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:content-transfer-encoding:mime-version :subject:message-id:date:to; bh=iKpjuRBVjVxg+qcNmfzx4OedFNtxzWxRJ1948k/PJkg=; b=OTf7uPNXDXjRp8/uI/IL7qvNXYXMEyxddTo3sEQTbRvqMc/LYaGKFBGlqdu0v4D0eh DSWfLbv3SIMJ+SGSHXwZ69OVKKd9ggf6e253vtT7yaBO18FufLksiBwA83xMXdSHFWPz Ypd8husImw8MkrRUDrS/T4TKbY4puWQk/7D9yJFFPTMoqPpi3q985IHFaz27/Bq+nkLF LWu55l8brtE/t/vViLCJB6i1roaowWGXsP+E6R/8Ca24uvHdC5thGRi19p7k/pG7Ywnw 4fk+ZfJNfMI5nJ1/jl9g5WR3pHSp2FGjH82YZIYXpp8/byI89Y9zkvXRgVtzASsM4qvU X4NA== X-Gm-Message-State: AIkVDXIJIEWreT1jMaBbu2h+y3CDet3SIU8NWKpgXF0quHxZIBgPt57LlAVe2d0TCpNerQ== X-Received: by 10.36.83.3 with SMTP id n3mr27505084itb.95.1482869101500; Tue, 27 Dec 2016 12:05:01 -0800 (PST) Received: from ?IPv6:2601:240:c600:8bd0:6c04:ef8c:c796:78ac? ([2601:240:c600:8bd0:6c04:ef8c:c796:78ac]) by smtp.gmail.com with ESMTPSA id f75sm14947304ita.13.2016.12.27.12.05.00 for (version=TLS1 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Tue, 27 Dec 2016 12:05:00 -0800 (PST) From: Anton Bachin Content-Type: text/plain; charset=us-ascii X-Mao-Original-Outgoing-Id: 504561899.874571-0d2b88eeab33bdcce3877a4e4b499bd0 Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2070.6\)) Message-Id: Date: Tue, 27 Dec 2016 14:04:59 -0600 To: "caml-list@inria.fr users" X-Mailer: Apple Mail (2.2070.6) Subject: [Caml-list] GADT+polymorphic variants quirk Hello, Consider this code for simulating an ad-hoc polymorphic addition function: type whole = [ `Integer ] type general = [ whole | `Float ] type _ num = | I : int -> [> whole ] num | F : float -> general num module M : sig val add : ([< general ] as 'a) num -> 'a num -> 'a num val to_int : whole num -> int val to_float : general num -> float end = struct let add : type a. a num -> a num -> a num = fun a b -> match a, b with | I n, I m -> I (n + m) | F n, I m -> F (n +. float_of_int m) | F n, F m -> F (n +. m) | _ -> (* ----NOTE---- *) match b, a with | F m, I n -> F (float_of_int n +. m) | _ -> assert false let to_int : whole num -> int = fun (I n) -> n let to_float = function | I n -> float_of_int n | F n -> n end let () = M.add (I 1) (I 2) |> M.to_int |> Printf.printf "%i\n"; M.add (I 1) (F 2.) |> M.to_float |> Printf.printf "%f\n" Instead of the nested match expression (marked with (* NOTE *)), I would have expected to just write | I n, F m -> ... However, if I actually do that, the result is an error on the expression in the case: Error: This expression has type general num but an expression was expected of type a num Type general = [ `Float | `Integer ] is not compatible with type a = [> `Integer ] The second variant type does not allow tag(s) `Float While the reversed case type-checks successfully. I can imagine why this would be so, but I want to ask the experts on the mailing list. Is this a known quirk of the typechecker? A bug? Is there some alternative syntax I am missing that would allow the I n pattern to be written first? Note that there is a way to rewrite the nested match cases to avoid _ and maintain the exhaustiveness check. I wrote them out as above for clarity. The actual solution I have settled on for now is: let add : type a. a num -> a num -> a num = fun a b -> match a, b with | I n, I m -> I (n + m) | F n, I m -> F (n +. float_of_int m) | _, F m -> match a with | I n -> F (float_of_int n +. m) | F n -> F (n +. m) Best, Anton P.S. If interested, the code was for this Stack Overflow question: http://stackoverflow.com/questions/41214000 answer: http://stackoverflow.com/a/41334879/2482998