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 c5ff346549e7 (Postfix) with ESMTPS id DC4DC1E6 for ; Fri, 13 Nov 2020 11:19:56 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.77,475,1596492000"; d="scan'208";a="477359814" Received: from prod-listesu18.inria.fr (HELO sympa.inria.fr) ([128.93.162.160]) by mail2-relais-roc.national.inria.fr with ESMTP; 13 Nov 2020 12:19:55 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id D75B0E1F46; Fri, 13 Nov 2020 12:19:55 +0100 (CET) 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 D4F18E1F43 for ; Fri, 13 Nov 2020 12:19:53 +0100 (CET) X-IronPort-AV: E=Sophos;i="5.77,475,1596492000"; d="scan'208";a="477359794" Received: from 91-175-127-215.subs.proxad.net (HELO MacBook-Pro-5.local) ([91.175.127.215]) by mail2-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 13 Nov 2020 12:19:53 +0100 To: OCaML Mailing List From: =?UTF-8?Q?Fran=c3=a7ois_Pottier?= Message-ID: Date: Fri, 13 Nov 2020 12:19:53 +0100 User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:68.0) Gecko/20100101 Thunderbird/68.12.1 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Language: fr Content-Transfer-Encoding: 8bit Subject: [Caml-list] Lack of an empty variant type Reply-To: =?UTF-8?Q?Fran=c3=a7ois_Pottier?= X-Loop: caml-list@inria.fr X-Sequence: 18284 Errors-To: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Help: List-Subscribe: List-Unsubscribe: List-Post: List-Owner: List-Archive: Archived-At: Hello, I was surprised today to see that this code is rejected: # let f (x : [< `A]) = ();; val f : [< `A ] -> unit = # let g (x : [< `B]) = ();; val g : [< `B ] -> unit = # fun b x -> if b then f x else g x;; Error: This expression has type [< `A ] but an expression was expected of type [< `B ] These two variant types have no intersection The type-checker rejects this code, even though it is safe, and its type should be [< ] -> unit, where [< ] is the empty variant type. I imagine that the type-checker wants to be my friend and wants to prevent me from defining a useless function. However, in the real use case I have in mind, I am abusing polymorphic variants to encode sets at the type level, and the lack of an empty set is painful! Just a random remark, -- François Pottier francois.pottier@inria.fr http://cambium.inria.fr/~fpottier/