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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by sympa.inria.fr (Postfix) with ESMTPS id 877E87EC41 for ; Sat, 20 Oct 2012 09:27:04 +0200 (CEST) Received-SPF: None (mail1-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=mail1-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 (mail1-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=mail1-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 (mail1-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=mail1-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: Ap0EAFxRglCFBoIF/2dsb2JhbABFwhWCIAEBBAEnHAE1AgMLCzQSVwYTG4djBag6hDkBhXSJAQeRaWCIW40WkDiCfg X-IronPort-AV: E=Sophos;i="4.80,619,1344204000"; d="scan'208";a="178109043" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail1-smtp-roc.national.inria.fr with ESMTP; 20 Oct 2012 09:27:02 +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 0C32A636A; Sat, 20 Oct 2012 16:26:59 +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 D25B640E1; Sat, 20 Oct 2012 16:26:58 +0900 (JST) DomainKey-Signature: h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; 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 A3E8D40C8; Sat, 20 Oct 2012 16:26:58 +0900 (JST) Content-Type: text/plain; charset=iso-8859-1 Mime-Version: 1.0 (Mac OS X Mail 6.2 \(1499\)) From: Jacques Garrigue In-Reply-To: <50815E40.5080601@furic.org> Date: Sat, 20 Oct 2012 16:27:02 +0900 Cc: caml-list@inria.fr Content-Transfer-Encoding: quoted-printable Message-Id: <565CA144-D2B0-45D5-8C2C-845610AE860A@math.nagoya-u.ac.jp> References: <50815E40.5080601@furic.org> To: Sebastien Furic X-Mailer: Apple Mail (2.1499) Subject: Re: [Caml-list] Clarification needed: use of "as" in patterns (with GADTs) On 2012/10/19, at 23:05, Sebastien Furic = wrote: > Hello, >=20 > Would someone be kind enough to explain me what's going on with the follo= wing code: >=20 > type empty > and nonempty > type ('a, _) my_list =3D > | Nil: ('a, empty) my_list > | Cons: 'a * ('a, 'b) my_list -> ('a, nonempty) my_list >=20 > (* Works fine *) > let rec max =3D function > | Cons (x, Nil) -> x > | Cons (x, Cons (x', xs)) when x <=3D x' -> max (Cons (x', xs)) > | Cons (x, Cons (_, xs)) -> max (Cons (x, xs)) >=20 > (* Fails *) > let rec max =3D function > | Cons (x, Nil) -> x > | Cons (x, (Cons (x', _) as xs)) when x <=3D x' -> max xs > | Cons (x, Cons (_, xs)) -> max (Cons (x, xs));; >=20 > Characters 97-99: > | Cons (x, (Cons (x', _) as xs)) when x <=3D x' -> max xs > ^^ > Error: This expression has type ('a, nonempty) my_list > but an expression was expected of type ('a, nonempty) my_list > This instance of nonempty is ambiguous: > it would escape the scope of its equation >=20 > I remember having seen similar issues in the past, involving "as" and pol= ymorphic variants (but I can't find it in the archives). Is it the same iss= ue? Why does Ocaml need to "break the continuity" of types in presence of "= as"? > BTW, what is the recommended way to write the code above (I want to avoid= having to reconstruct the list)? Actually, this is not the same issue: the problem here is related to ambigu= ity inference, which in the case of OCaml is required for soundness in pres= ence of GADTs. What happens here is that you Cons constructor introduces an existential va= riable, which is immediately forced to nonempty by matching against the nes= ted Cons. However is inferred as using this existential variable. When typing the recursive call the existential variable is forced to expand= to nonempty, but as a result of this expansion it is marked as ambiguous. When you get such an error message, there is an easy solution: add a type a= nnotation on the faulty expression, using exactly the printed type: max (xs : ('a, nonempty) my_list) This is enough to make this program accepted. It could be argued that in this case there is no ambiguity, since the exist= ential cannot be exported anyway. I'll look into that, but you must keep in mind that we must be very careful= , as soundness is at stake. Jacques Garrigue=