From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <programming.languages@furic.org>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105])
	by sympa.inria.fr (Postfix) with ESMTPS id E3C927F249
	for <caml-list@sympa.inria.fr>; Mon, 29 Oct 2012 12:23:55 +0100 (CET)
Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  programming.languages@furic.org) identity=pra;
  client-ip=80.12.242.127;
  receiver=mail4-smtp-sop.national.inria.fr;
  envelope-from="programming.languages@furic.org";
  x-sender="programming.languages@furic.org";
  x-conformance=sidf_compatible
Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  programming.languages@furic.org) identity=mailfrom;
  client-ip=80.12.242.127;
  receiver=mail4-smtp-sop.national.inria.fr;
  envelope-from="programming.languages@furic.org";
  x-sender="programming.languages@furic.org";
  x-conformance=sidf_compatible
Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@smtp.smtpout.orange.fr) identity=helo;
  client-ip=80.12.242.127;
  receiver=mail4-smtp-sop.national.inria.fr;
  envelope-from="programming.languages@furic.org";
  x-sender="postmaster@smtp.smtpout.orange.fr";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: Aj8BAFxmjlBQDPJ/jWdsb2JhbABEvyKDYwEBAQEJCQsJEgUkgh4BAQUyAQVAEQsYCRYPCQMCAQIBRRMIAQEXh2+7b4t1gzmDJAOVdIVpjUk
X-IronPort-AV: E=Sophos;i="4.80,671,1344204000"; 
   d="scan'208";a="160750100"
Received: from smtp05.smtpout.orange.fr (HELO smtp.smtpout.orange.fr) ([80.12.242.127])
  by mail4-smtp-sop.national.inria.fr with ESMTP; 29 Oct 2012 12:23:55 +0100
Received: from [192.168.1.14] ([2.11.96.246])
	by mwinf5d10 with ME
	id GzJs1k00w5JwXWA03zJtmP; Mon, 29 Oct 2012 12:18:54 +0100
Message-ID: <508E6635.1060205@furic.org>
Date: Mon, 29 Oct 2012 12:19:17 +0100
From: Sebastien Furic <programming.languages@furic.org>
User-Agent: Mozilla/5.0 (X11; Linux i686; rv:16.0) Gecko/20121011 Thunderbird/16.0.1
MIME-Version: 1.0
To: caml-list@inria.fr
References: <50815E40.5080601@furic.org> <565CA144-D2B0-45D5-8C2C-845610AE860A@math.nagoya-u.ac.jp>
In-Reply-To: <565CA144-D2B0-45D5-8C2C-845610AE860A@math.nagoya-u.ac.jp>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 8bit
Subject: Re: [Caml-list] Clarification needed: use of "as" in patterns (with
 GADTs)



On 10/20/2012 09:27 AM, Jacques Garrigue wrote:
> Actually, this is not the same issue: the problem here is related to ambiguity inference, which in the case of OCaml is required for soundness in presence of GADTs.
> What happens here is that you Cons constructor introduces an existential variable, which is immediately forced to nonempty by matching against the nested 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 annotation 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 existential 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.

  Thank you Jacques, for the explanation and for the hint.

  Cheers,

  Sébastien.