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 567E57ED1D for ; Tue, 13 Oct 2015 11:45:29 +0200 (CEST) IronPort-PHdr: 9a23:YRobUhfsVwSzaC+dD9zwHPa8lGMj4u6mDksu8pMizoh2WeGdxc69Yx7h7PlgxGXEQZ/co6odzbGG7+awBCdYu96oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDuvc2OKF0SzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IeezAcq85Vb1VCig9eyBwvZWz9EqLcQzazHYaGkAXlh5XBA/JpEXwW5b1tjT9seZV2iCcMNbqV705RXKp6KI9GzHyjyJSFTMj/WTGwv15iKZcuFr1thV7x4nMSI6QPft6OKjaeIVJFiJ6Qs9NWnkZUcuHZIwVAr9EZL4Aog== 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-lb0-f169.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.217.169; 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.217.169 as permitted sender) identity=mailfrom; client-ip=209.85.217.169; 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-lb0-f169.google.com) identity=helo; client-ip=209.85.217.169; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="postmaster@mail-lb0-f169.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CaAQDs0RxWm6nZVdFdg3puBrF9jXQjgnCCCn8CgTcHPBABAQEBAQEBARABAQEBAQYLCwkhLoIfggcBAQECAQESEQQZARsdAQMBCwYFCwMKAgImAgIiAREBBQEcBhMJGYd2AQMKCA2fDIExPjGLSYFsgnmJBgoZJw1WhEMBAQEBBgEBAQEBFwEFDoEUilGFDQeCaYFFBY0OiQiNGpo8EiOBFziCLyMdgT89MwGGcAEBAQ X-IPAS-Result: A0CaAQDs0RxWm6nZVdFdg3puBrF9jXQjgnCCCn8CgTcHPBABAQEBAQEBARABAQEBAQYLCwkhLoIfggcBAQECAQESEQQZARsdAQMBCwYFCwMKAgImAgIiAREBBQEcBhMJGYd2AQMKCA2fDIExPjGLSYFsgnmJBgoZJw1WhEMBAQEBBgEBAQEBFwEFDoEUilGFDQeCaYFFBY0OiQiNGpo8EiOBFziCLyMdgT89MwGGcAEBAQ X-IronPort-AV: E=Sophos;i="5.17,677,1437429600"; d="scan'208";a="182517081" Received: from mail-lb0-f169.google.com ([209.85.217.169]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 13 Oct 2015 11:45:28 +0200 Received: by lbcao8 with SMTP id ao8so13097629lbc.3 for ; Tue, 13 Oct 2015 02:45:28 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=jxHnrHZOr56VBf4Ag0eyxv5WeMqYyqb9KbNBS4ObXjk=; b=ATFT97dEECVT9kOg9wco5wYPNmDHqNYDqUlfxsPB7dGBV3OlGPzSmIHNSxnMB61AEX lxYMOLLt4+j9LUwIA1mtWgCLqQDnhKFvFewGjSx6Mjc4h3D0p4kIqfDoYF9ECa+OfBoZ k4n5H+nMPQ30fxvK3/bYevhra7kAb70AsKryHAJ7RM+O0xlQPVNR02hWE3OWAOjEPL8O jM7wQMmq7BTG40h6Qs44eaSRkk9HKkiphtnWYvcursLl/1i7DG67DQzGMVgYCdzsJt5m z+WFxtuJAive9FohMgC8leH5NjvIhZmZDFiOjjiEd77bAqPpRpJmS+9UtFICAkBwyGhH JB2w== MIME-Version: 1.0 X-Received: by 10.112.134.197 with SMTP id pm5mr14648432lbb.3.1444729527949; Tue, 13 Oct 2015 02:45:27 -0700 (PDT) Received: by 10.25.24.90 with HTTP; Tue, 13 Oct 2015 02:45:27 -0700 (PDT) In-Reply-To: References: Date: Tue, 13 Oct 2015 10:45:27 +0100 Message-ID: From: Jeremy Yallop To: Ben Millwood Cc: Philippe Veber , Abdallah Saffidine , caml users Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] How to use GADTs across modules in OCaml without raising warnings? On 13 October 2015 at 07:15, Ben Millwood wrote: > I'll advance on others' advice by pointing out that if you say: > > type never = private [`never] > > then you neither "use up" a constructor name nor is it possible to write an > expression with type never. A nit: there are lots of *expressions* of type 'never', such as '(assert false: never)'. However, there are no (closed) *values* of type 'never'. > Unfortunately, the compiler still doesn't realise that, so it > doesn't help you for pattern-matching. The gadt-warnings branch, which is described here: GADTs and exhaustiveness: looking for the impossible Jacques Garrigue's and Jacques Le Normand ACM SIGPLAN Workshop on ML, September 2015 http://www.mlworkshop.org/gadts-and-exhaustiveness-looking-for-the-impossible.pdf includes better supports for "empty" types. For example, here's a definition of an empty type 'wrong': type 'a is_true = T: [`True] is_true type wrong = [`False] is_true and here's a function definition which omits a case that you can deduce is unmatchable when you know that 'wrong' is empty: let f : wrong option -> unit = fun None -> () The current OCaml compiler (4.02.3) issues a warning for 'f': Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: Some _ In contrast, the compiler in the gadt-warnings branch compiles 'f' without complaint (and generates more efficient code, since there's no need to inspect the argument). Jeremy.