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 D23697EC41
	for <caml-list@sympa.inria.fr>; Fri, 19 Oct 2012 16:05:55 +0200 (CEST)
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.134;
  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.134;
  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.134;
  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: AlQBAAtdgVBQDPKGk2dsb2JhbABFwQUBAQEBCQkLCRQDJIJOCwEFQD0WGAMCAQIBWAgBAYgEmz6hV48kgyMDlW+FZI1F
X-IronPort-AV: E=Sophos;i="4.80,612,1344204000"; 
   d="scan'208";a="159662467"
Received: from smtp12.smtpout.orange.fr (HELO smtp.smtpout.orange.fr) ([80.12.242.134])
  by mail4-smtp-sop.national.inria.fr with ESMTP; 19 Oct 2012 16:05:55 +0200
Received: from [192.168.1.14] ([2.11.235.219])
	by mwinf5d35 with ME
	id D25u1k00S4khYo20325uVP; Fri, 19 Oct 2012 16:05:55 +0200
Message-ID: <50815E40.5080601@furic.org>
Date: Fri, 19 Oct 2012 16:05:52 +0200
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
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 8bit
Subject: [Caml-list] Clarification needed: use of "as" in patterns (with
 GADTs)

  Hello,

  Would someone be kind enough to explain me what's going on with the 
following code:

type empty
and nonempty
type ('a, _) my_list =
   | Nil: ('a, empty) my_list
   | Cons: 'a * ('a, 'b) my_list -> ('a, nonempty) my_list

(* Works fine *)
let rec max = function
   | Cons (x, Nil) -> x
   | Cons (x, Cons (x', xs)) when x <= x' -> max (Cons (x', xs))
   | Cons (x, Cons (_, xs)) -> max (Cons (x, xs))

(* Fails *)
let rec max = function
   | Cons (x, Nil) -> x
   | Cons (x, (Cons (x', _) as xs)) when x <= x' -> max xs
   | Cons (x, Cons (_, xs)) -> max (Cons (x, xs));;

Characters 97-99:
   | Cons (x, (Cons (x', _) as xs)) when x <= 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

  I remember having seen similar issues in the past, involving "as" and 
polymorphic variants (but I can't find it in the archives). Is it the 
same issue? 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)?

  Cheers,

  Sébastien.