From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 3347BBC57 for ; Tue, 21 Sep 2010 15:35:27 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AoUEAKhRmEyNTDBjgWdsb2JhbACUNI10FQEBFiIiwnKFQQSKOIsR X-IronPort-AV: E=Sophos;i="4.56,399,1280700000"; d="scan'208";a="60450126" Received: from os.inf.tu-dresden.de ([141.76.48.99]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 21 Sep 2010 15:35:26 +0200 Received: from [2002:8d4c:3001:48:222:68ff:fe19:71d] (helo=blau.inf.tu-dresden.de) by os.inf.tu-dresden.de with esmtpsa (TLSv1:AES256-SHA:256) (Exim 4.72) id 1Oy30H-0005mq-U0; Tue, 21 Sep 2010 15:35:26 +0200 Received: from tews by blau.inf.tu-dresden.de with local (Exim 4.72) (envelope-from ) id 1Oy30G-0001i6-KR; Tue, 21 Sep 2010 15:35:24 +0200 From: Hendrik Tews MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <19608.46236.174842.349640@blau.inf.tu-dresden.de> Date: Tue, 21 Sep 2010 15:35:24 +0200 To: garrigue@math.nagoya-u.ac.jp Cc: caml-list@inria.fr Subject: Re: [Caml-list] difference of [< `A of & int] and [< `A of int] ? In-Reply-To: References: <19608.41484.202892.641777@blau.inf.tu-dresden.de> X-Mailer: VM 8.1.0 under 23.2.1 (i486-pc-linux-gnu) X-Spam: no; 0.00; hendrik:01 tews:01 tews:01 conjunctive:01 typexpr:01 typexpr:01 conjunctive:01 checker:01 unify:01 compiler:01 hendrik:01 tu-dresden:01 caml-list:01 caml-list:01 constructor:01 Thanks for this quick and enlightening answer! Jacques Garrigue writes: Date: Tue, 21 Sep 2010 21:41:01 +0900 Subject: Re: [Caml-list] difference of [< `A of & int] and [< `A of int] ? > [< `A of & int] This is an (impossible) conjunctive type. Basically it says that `A is both a constant constructor (taking no argument), and a constructor taking an argument of type int. Actually, this type expression is not covered by the grammar in the reference manual. The rule tag-spec-full ::= `tag-name [ of typexpr ] { & typexpr } does not produce it, because typexpr cannot produce the empty string. I believe a sentence about this special case in the manual would be helpful. > File "test/x.ml", line 1, characters 0-1: > Error: The implementation test/x.ml > does not match the interface (inferred signature): > Type declarations do not match: > type 'a t = 'a constraint 'a = [< `A of & int ] > is not included in > type 'a t = 'a constraint 'a = [< `A of & int ] Err, it is actually a feature, but I agree this is not very intuitive. When checking types against an interface, such conjunctive types are not allowed. So the type checker attemps to unify all possibilities, but since no argument is not unifiable with anything else, it fails. Unfortunately, the error message is not very explicit about the cause. However, the following impossible type type 'a t = [< `A of int & string] as 'a is accepted by the compiler. Is there a reason for treating these two impossible types differently? Bye, Hendrik