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 mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id C8309BC57 for ; Tue, 21 Sep 2010 14:41:07 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgkCAAFFmExKfVO2kGdsb2JhbACiHwgVAQEBAQkJDAcRAx+nDItQhlmJAwEBAwWFPASETIVsg16FJQ X-IronPort-AV: E=Sophos;i="4.56,399,1280700000"; d="scan'208";a="70028031" Received: from mail-pv0-f182.google.com ([74.125.83.182]) by mail4-smtp-sop.national.inria.fr with ESMTP; 21 Sep 2010 14:41:06 +0200 Received: by pvc21 with SMTP id 21so1829623pvc.27 for ; Tue, 21 Sep 2010 05:41:05 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:sender:subject:mime-version :content-type:from:in-reply-to:date:cc:reply-to :content-transfer-encoding:message-id:references:to:x-mailer; bh=TDR0AP7ogrGn9QFT1nDM+a4S/m7kgFAU6dPZIjtEX3E=; b=FM+qpGyk3LazMeuQCAT9W1I+5MP85zTllLbnCz3Fq3wjb86c6N0SzoOrVbToh0aE5X ZIZ53iQwUbtlwO+J02bKpEdhAt/rQEO7d+oZzfxBq+Lr85rsWMMvKmnqavqhfC+sAmTv KWIMK7JzIng+ILKxZ3oX/qfkYiD0TGh7xmwCM= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:subject:mime-version:content-type:from:in-reply-to:date:cc :reply-to:content-transfer-encoding:message-id:references:to :x-mailer; b=Zi44WCxq27KchFRwMU92FiO7KfDvjXuzzuo9tMq+l89HNy00OaxaxmSHZJDNnccJKT tOWjeYlg+120Ncn/6VQew/7B/05Whnh2ioNRO01lmWHkGogGzitgTAmtiMfMNQQqAiKe MdBVaMPOCPUg21ywSpvxqShdrww/FS5UzMSys= Received: by 10.114.78.1 with SMTP id a1mr11446360wab.216.1285072865736; Tue, 21 Sep 2010 05:41:05 -0700 (PDT) Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mx.google.com with ESMTPS id s5sm15490818wak.12.2010.09.21.05.41.03 (version=TLSv1/SSLv3 cipher=RC4-MD5); Tue, 21 Sep 2010 05:41:04 -0700 (PDT) Sender: Jacques Garrigue Subject: Re: [Caml-list] difference of [< `A of & int] and [< `A of int] ? Mime-Version: 1.0 (Apple Message framework v1081) Content-Type: text/plain; charset=us-ascii From: Jacques Garrigue In-Reply-To: <19608.41484.202892.641777@blau.inf.tu-dresden.de> Date: Tue, 21 Sep 2010 21:41:01 +0900 Cc: caml-list@inria.fr Reply-To: garrigue@math.nagoya-u.ac.jp Content-Transfer-Encoding: quoted-printable Message-Id: References: <19608.41484.202892.641777@blau.inf.tu-dresden.de> To: Hendrik Tews X-Mailer: Apple Mail (2.1081) X-Spam: no; 0.00; hendrik:01 tews:01 camlp:01 ctyp:01 ctyp:01 camlp:01 conjunctive:01 inference:01 unifying:01 bug:01 conjunctive:01 checker:01 unify:01 wrote:01 partial:01 On 2010/09/21, at 21:16, Hendrik Tews wrote: > I am trying to grasp the camlp4 constructor for types TyOfAmp, > which is declared as=20 >=20 > | TyOfAmp of loc and ctyp and ctyp (* t of & t *) >=20 > in camlp4/Camlp4/Camlp4Ast.partial.ml. It is used in the ast of=20 > ``[< `A of & int]''. >=20 > Can somebody explain the meaning of [< `A of & int]? What is the > difference between [< `A of & int] and [< `A of int] ? This is an (impossible) conjunctive type.=20 Basically it says that `A is both a constant constructor (taking no = argument), and a constructor taking an argument of type int. This artefact is needed to make type inference principal, but this type is not useful in itself. (Well, one can think of some uses, like unifying types conditionally, = but the behaviour is rather restricted.) > And why does=20 >=20 > type 'a t =3D [< `A of & int] as 'a >=20 > produce the weird error=20 >=20 > 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 =3D 'a constraint 'a =3D [< `A of & int ] > is not included in > type 'a t =3D 'a constraint 'a =3D [< `A of & int ] >=20 > ? Is this a bug or a feature? 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. Jacques Garrigue=