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 EB10A7F02D for ; Wed, 8 Oct 2014 05:29:55 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AuwAANKuNFSFBoIFl2dsb2JhbABfg2FYgwTIJIdVAoEgAREBAQEBAQgWB0CEBAEBBCMEGQMBNQEBDgsYAgIYDgICVwaIUKwUeIUIAok/hkEBEAEGgSyOZTMHgnc2gR6LX4pahw6Zel2CSgEBAQ X-IPAS-Result: AuwAANKuNFSFBoIFl2dsb2JhbABfg2FYgwTIJIdVAoEgAREBAQEBAQgWB0CEBAEBBCMEGQMBNQEBDgsYAgIYDgICVwaIUKwUeIUIAok/hkEBEAEGgSyOZTMHgnc2gR6LX4pahw6Zel2CSgEBAQ X-IronPort-AV: E=Sophos;i="5.04,674,1406584800"; d="scan'208";a="99918037" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 08 Oct 2014 05:29:53 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 8BF4F63C2; Wed, 8 Oct 2014 12:29:50 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 56BA12564; Wed, 8 Oct 2014 12:29:50 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= content-type:mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=oAH9IGfWEH29ReDqtEwLjQrOlxg=; b=dUN9/ac208JNze5Stto95PsjvG// FNoQS71iYA0B/dDIP3LWdxQ9b0FVkkefWZTpLhqVZvYnenLyBgFCeuBhXxqILTVw 19+7rem6I4S4M/5Lp0RMum0DO18HmHuzG5Yj3pOuUhxooQgDT+IJKB51pcmKEbNY bokQ7o7O8Hn9k70= DomainKey-Signature: a=rsa-sha1; h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=dh6prWI0+mhcb1nCIzYh/a/j20E17vFQS9sIPegCgEznrkiFklvd+jzQnAfKViIB8QBjOYFnVJ+oTcBAEoddkNOGhkAGSpNEAOWD2wk+jERr0vqvazsaSpDaa28cdBBfV7KC8SFJy39XVuaEEgKQwnm3sQhJKuHl7J0rrzBI7Ic=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id EBDAB24CC; Wed, 8 Oct 2014 12:29:49 +0900 (JST) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 7.3 \(1878.6\)) From: Jacques Garrigue In-Reply-To: Date: Wed, 8 Oct 2014 12:29:47 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: <43F352EF-1F58-4CE3-8EA5-91D61EBBA751@math.nagoya-u.ac.jp> References: To: =?utf-8?Q?Milan_Stanojevi=C4=87?= X-Mailer: Apple Mail (2.1878.6) Subject: Re: [Caml-list] constructor disambiguation for gadts On 2014/10/08 01:14, Milan Stanojevi=C4=87 wrote: >=20 > I was wondering what are technical difficulties that prevent > constructor disambiguation for GADTs? >=20 > I got an interesting error today, where it is clear that compiler > knows the type but because it is GADT it is still asking me to qualify > the constructor. >=20 > Here is the simple example. > module A : sig > type _ t =3D > | I : int t > | S : string t > end =3D struct > type _ t =3D > | I : int t > | S : string t > end >=20 > let add : type a . a A.t -> a -> a -> a =3D > fun w a1 a2 -> > match w with > | I -> a1 + a2 > | S -> String.concat "" [a1; a2] > ;; >=20 > I get File "foo.ml", line 14, characters 6-7: > Error: The GADT constructor I of type A.t must be qualified in this patte= rn. >=20 > I'm not sure what extra information I'm giving to the type checker by > qualifying the constructor. Typing of GADT patterns follows a slightly different path, which makes harder to insert constructor disambiguation. To be more precise, the type-checker first looks at the patterns, and tries to guess whether there are some GADT constructors inside it. If some constructors are ambiguous, it may guess wrongly that there are none, and take the non-GADT path, to find later that it should have taken the GADT path. Jacques Garrigue=