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 1930F8015D for ; Fri, 26 May 2017 11:09:51 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=yallop@gmail.com; spf=Pass smtp.mailfrom=yallop@gmail.com; spf=None smtp.helo=postmaster@mail-qt0-f182.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of yallop@gmail.com) identity=pra; client-ip=209.85.216.182; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of yallop@gmail.com designates 209.85.216.182 as permitted sender) identity=mailfrom; client-ip=209.85.216.182; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@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-qt0-f182.google.com) identity=helo; client-ip=209.85.216.182; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="postmaster@mail-qt0-f182.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3A2TMdCBVl9gsX4ThMA0gdcJnNrXXV8LGtZVwlr6E/?= =?us-ascii?q?grcLSJyIuqrYbBWDt8tkgFKBZ4jH8fUM07OQ6PG+HzFfqdbZ6TZZIcMKD0dEwe?= =?us-ascii?q?wt3CUeQ+e9SnfHZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5y?= =?us-ascii?q?O/inUtWK15f/2O+94YDcbBtVjzShf7xyMA+2rQLMvcUKnIduMKg8xx/Ir3dSe+?= =?us-ascii?q?lbx35jKVaPkxrh/Mu98ppu/iZKt/4968JMVLjxcrglQ7BfEDkpPGc56dHxuxXE?= =?us-ascii?q?UQWB+GYXXH8MkhpPDQjF7RX6UYn0vyDnqOdz2zSUMNPvQ7wsVjus86lkSBnziC?= =?us-ascii?q?caLDE5633YitZxjK1Avh2soQF0zpPOb4GUMPp+eb7dfc8fSGFcUMtdSzBND4Wh?= =?us-ascii?q?ZIYUEeEPIfhXoJX8p1sWrBuxGw+sBP/0yjRVgnP6xLA23/g9HQ3D2gErAtAAv2?= =?us-ascii?q?nOrNjtNqgSX+C7wqfLwzvecf1ZxSzw6JTUfh07vf2AQa58fMjXxEIyFw3FlFKQ?= =?us-ascii?q?qYn9Mj2RyOsNqXaU7+9gVOmyiWEosQVxojyoxsc0l4LEgYIUxUrA9SV9x4Y1Pc?= =?us-ascii?q?a1SEF+YdG+EZtQszuWOJdxQsMnWmxlvjsxxL4euZOjYiQG1JAqywTcZvGHaYSE?= =?us-ascii?q?/A/vWeeLLTtlh39pZrSyjAuo/0e60O3zTMy03U5KriVbltnMsWgA1xnJ5ciGTv?= =?us-ascii?q?tx516h2SqT2wzK5OFIPEM5mbTBJ54uxb4wkZUTsUDdESPshEr2i6qWel0l+uiu?= =?us-ascii?q?9evnfq3rqoGAO4JwkA3zMaQjltahDeglMwUCRXWX9Oei2LH7+E32WrRKjvk4kq?= =?us-ascii?q?nDt5DaINwWp66jDA9R1oYj7A6/Aiyp0NQdh3YHLVZFdAibgIjuPlHCOOr4Auun?= =?us-ascii?q?g1SwjDdrwOjLMaH7DZXIKnjPibPhfbdm605A0wcz1tBe55dMCr4bOv7zW0nxtM?= =?us-ascii?q?bZDhAjKQC0zfznW51B0dY7UH6CAOe6N7jTshfcu71xf+LUPt4f5matIKEuv/K0?= =?us-ascii?q?0XZjlA5CdqX2g8cZQH+9F/ViZU6eZCy/rM0GFDIosxAzSf2iuVSGVTlLLyKjVq?= =?us-ascii?q?Y44SkTB4evDIOFTYeo1u/SlBynF4FbMzgVQmuHFm3lIsDdA68B?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BuAABd8CdZhrbYVdFdGwEBAQMBAQEJA?= =?us-ascii?q?QEBFgEBAQMBAQEJAQEBhQcSB4Nom3yYCIYkAoMAB0IVAQEBAQEBAQEBAQESAQE?= =?us-ascii?q?BCAsLCCgvgjMkAYJBAQIDIwQZARsdAQMMBgULDQICJgICIQEBEQEFARwGExqJd?= =?us-ascii?q?wEDFZ5nP4wHgWwYBQEcgwoFg10KGScNVoM7AQEBAQEBBAEBAQEBGwIGEnmKToJ?= =?us-ascii?q?XhSGCYAWJQBiILItkO45QhFiRd4syh1QUH4EVNYEsMCEIGxVGGYRaH4FwPzaJC?= =?us-ascii?q?QEBAQ?= X-IPAS-Result: =?us-ascii?q?A0BuAABd8CdZhrbYVdFdGwEBAQMBAQEJAQEBFgEBAQMBAQE?= =?us-ascii?q?JAQEBhQcSB4Nom3yYCIYkAoMAB0IVAQEBAQEBAQEBAQESAQEBCAsLCCgvgjMkA?= =?us-ascii?q?YJBAQIDIwQZARsdAQMMBgULDQICJgICIQEBEQEFARwGExqJdwEDFZ5nP4wHgWw?= =?us-ascii?q?YBQEcgwoFg10KGScNVoM7AQEBAQEBBAEBAQEBGwIGEnmKToJXhSGCYAWJQBiIL?= =?us-ascii?q?ItkO45QhFiRd4syh1QUH4EVNYEsMCEIGxVGGYRaH4FwPzaJCQEBAQ?= X-IronPort-AV: E=Sophos;i="5.38,396,1491256800"; d="scan'208";a="274842855" Received: from mail-qt0-f182.google.com ([209.85.216.182]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 26 May 2017 11:09:29 +0200 Received: by mail-qt0-f182.google.com with SMTP id c13so3493003qtc.1 for ; Fri, 26 May 2017 02:09:29 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=Mo7YxXLnpJo12LSbTDs2+JuKtgXB+Sy1DLYMUS9zumQ=; b=lVfi5E2z30TMxck67fhYqdMIbdyvkb8x40KwdwY60DKDvDZABOoDrQDA0UjQfzC+o6 H+/6ecc1Wwh4AZ/n/WbSjiwKDSuucPceYGrT9BDd19qRCkt0RC/X4G+loNE0kTyatE2X 7Ik3LVMeFHT7cVPSPyv5i7xO0FQZvZ4mu28ShF2ysMrlf8akZjO4q5ZyH8bsDN/24zq8 kToMwdb3YCUUY3N4uI7TOoH32te/bqCJwN/wlSiTVgGN9xCrVWmdf+++OfKz26qxYjAC KhNTTC7bKziZw1T/kz1XVula+vgcYmXhyWm/4Xi8w0mgomUsSJ0ijoaXGtfQW3s5h4kg vPDA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=Mo7YxXLnpJo12LSbTDs2+JuKtgXB+Sy1DLYMUS9zumQ=; b=eAE+dnr82kj4C5C4ByWkVLEjmsu5jbLzZozGJQ3UTdiwJFPh553wZwjhwEDp1XbsBG XCk+FdrIHuZnwnM98BjML/QnsrWVYX65XDK9FLzl5d7uXRu5kVTYgj3cokcHVOeecfoP TUfPt7k8sUtJNTJvASUfHE36TCKr8ea2vtyoidDV6EBzdtNOBlyLD0AIJjbdSUeRCnbp JEgoR2ROyM1hbh8l5UbfxE4nhRksm+fa/09agvSvRBUqOTo0UERcMuNwwfNlsS4FDrG7 SNHNga+99ddOG3DgmObbtr+QJx2uQJUD7toiinXT3yyXUiZ3YPeAt4wRcaOYHKuO3Inb vziA== X-Gm-Message-State: AODbwcD15Y/Babmb2yvCrNQBkCAQLiV2E5JzFqszDG77zDPh3R1Rgmfk PYECy0/pXUpdH+neZ0L9dRas1f1EvA== X-Received: by 10.200.56.56 with SMTP id q53mr1095773qtb.36.1495789768216; Fri, 26 May 2017 02:09:28 -0700 (PDT) MIME-Version: 1.0 Received: by 10.55.185.134 with HTTP; Fri, 26 May 2017 02:09:27 -0700 (PDT) In-Reply-To: <8de32ec3-f6ab-7c86-a270-7f7ccbe24d20@gmail.com> References: <8de32ec3-f6ab-7c86-a270-7f7ccbe24d20@gmail.com> From: Jeremy Yallop Date: Fri, 26 May 2017 10:09:27 +0100 Message-ID: To: Matej Kosik <5764c029b688c1c0d24a2e97cd764f@gmail.com> Cc: Caml List Content-Type: text/plain; charset="UTF-8" Subject: Re: [Caml-list] a question about Ocaml semantics On 26 May 2017 at 09:08, Matej Kosik <5764c029b688c1c0d24a2e97cd764f@gmail.com> wrote: > There's an Ocaml language feature I do not understand. > > E.g. in this example: > > type 'a phantom = int > type t = { enter : 'a. 'a phantom -> int } > let f g = g.enter 2 > let _ = f { enter = fun x -> 1 + x } (* ok *) > let _ = f { enter = (+) 1 } (* fails to typecheck *) > > I don't get why, if we have: > > type 'a phantom = int > > i.e. "'a phantom" is defined as an alias of "int", > how is it possible that the following types: > > { enter : 'a. 'a phantom -> int } > > is not equal to > > { enter : 'a. int -> int } > > I've tried to find a corresponding section in the Reference Manual, but I failed. > Where is this explained? I'm not sure that the interaction of features here is documented anywhere. But your expectations seem reasonable to me. The good news is that the behaviour changed in OCaml 4.04.0, and your program is now accepted. However, it's not clear (to me) that the interaction between generalization, phantom types and variance is quite optimal or consistent yet. For example, I'd expect this similar program to be accepted type 'a phantom = int let x : type a. a phantom -> int = (+) 1 but it's rejected by OCaml 4.04.1.