From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <alain@frisch.fr>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104])
	by sympa.inria.fr (Postfix) with ESMTPS id 4263C81792
	for <caml-list@sympa.inria.fr>; Thu,  4 Jul 2013 09:35:17 +0200 (CEST)
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  alain@frisch.fr) identity=pra; client-ip=193.252.23.211;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="alain@frisch.fr"; x-sender="alain@frisch.fr";
  x-conformance=sidf_compatible
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  alain@frisch.fr) identity=mailfrom; client-ip=193.252.23.211;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="alain@frisch.fr"; x-sender="alain@frisch.fr";
  x-conformance=sidf_compatible
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@msa.smtpout.orange.fr) identity=helo;
  client-ip=193.252.23.211;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="alain@frisch.fr";
  x-sender="postmaster@msa.smtpout.orange.fr";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AsEAAJMk1VHB/BfTlGdsb2JhbABagzzBB4EbDgEBAQEJCwkJFAMlgiMBAQU4QAEQCxgJFg8JAwIBAgFFBwwBBQIBAYgPuVGPZgUHg20Dl0mGIY43
X-IPAS-Result: AsEAAJMk1VHB/BfTlGdsb2JhbABagzzBB4EbDgEBAQEJCwkJFAMlgiMBAQU4QAEQCxgJFg8JAwIBAgFFBwwBBQIBAYgPuVGPZgUHg20Dl0mGIY43
X-IronPort-AV: E=Sophos;i="4.87,993,1363129200"; 
   d="scan'208";a="19959497"
Received: from msa02.smtpout.orange.fr (HELO msa.smtpout.orange.fr) ([193.252.23.211])
  by mail3-smtp-sop.national.inria.fr with ESMTP; 04 Jul 2013 09:35:16 +0200
Received: from [192.168.1.111] ([92.151.124.168])
	by mwinf5d38 with ME
	id w7bE1l00B3e6krg037bErx; Thu, 04 Jul 2013 09:35:16 +0200
Message-ID: <51D525B2.9080907@frisch.fr>
Date: Thu, 04 Jul 2013 09:35:14 +0200
From: Alain Frisch <alain@frisch.fr>
User-Agent: Mozilla/5.0 (X11; Linux i686 on x86_64; rv:22.0) Gecko/20100101 Thunderbird/22.0
MIME-Version: 1.0
To: oleg@okmij.org, gabriel.scherer@gmail.com
CC: garrigue@math.nagoya-u.ac.jp, caml-list@inria.fr
References: <20130704060748.15628.qmail@www1.g3.pair.com>
In-Reply-To: <20130704060748.15628.qmail@www1.g3.pair.com>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Subject: Re: [Caml-list] Request for feedback: A problem with injectivity

On 07/04/2013 08:07 AM, oleg@okmij.org wrote:
> The gist is using the type variable name 'a' from the definition of
> GADT, and attaching the numeric suffix to disambiguate. (GHC does that all
> the time -- and I believe OCaml does something similar in many cases,
> only not for GADTs.) What helps in particular I believe is quoting the
> clause from the GADT declaration, so we can see where the name 'a'
> comes from. So, perhaps if the error message can be improved with
> giving more information about the error, the problem will be solved
> without additional syntax?

Naming types created by opening GADT existentials is useful not only for 
error messages, but also to have a way to refer to that type in the 
branch (for instance to instantiate locally a functor whose argument 
refers to that type).

-- Alain