From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <oleg@okmij.org>
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 E840881792
	for <caml-list@sympa.inria.fr>; Fri,  5 Jul 2013 12:30:00 +0200 (CEST)
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  oleg@okmij.org) identity=pra; client-ip=66.39.3.115;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="oleg@okmij.org"; x-sender="oleg@okmij.org";
  x-conformance=sidf_compatible
Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of
  oleg@okmij.org designates 66.39.3.115 as permitted sender)
  identity=mailfrom; client-ip=66.39.3.115;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="oleg@okmij.org"; x-sender="oleg@okmij.org";
  x-conformance=sidf_compatible; x-record-type="v=spf1"
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@www1.g3.pair.com) identity=helo;
  client-ip=66.39.3.115;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="oleg@okmij.org";
  x-sender="postmaster@www1.g3.pair.com";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AnoEANKe1lFCJwNzemdsb2JhbABai2i4TIEVDgEBCwcNCTyCIwEBBAEnUgUWNGkUiA4GuHePawcWg1cDl0gBlFY8
X-IPAS-Result: AnoEANKe1lFCJwNzemdsb2JhbABai2i4TIEVDgEBCwcNCTyCIwEBBAEnUgUWNGkUiA4GuHePawcWg1cDl0gBlFY8
X-IronPort-AV: E=Sophos;i="4.87,1001,1363129200"; 
   d="scan'208";a="24725554"
Received: from www1.g3.pair.com ([66.39.3.115])
  by mail2-smtp-roc.national.inria.fr with SMTP; 05 Jul 2013 12:30:00 +0200
Received: (qmail 2249 invoked by uid 9370); 5 Jul 2013 10:30:00 -0000
Date: 5 Jul 2013 10:30:00 -0000
Message-ID: <20130705103000.2248.qmail@www1.g3.pair.com>
From: oleg@okmij.org
To: alain@frisch.fr
CC: garrigue@math.nagoya-u.ac.jp, caml-list@inria.fr
In-reply-to: <51D525B2.9080907@frisch.fr>
Subject: Re: [Caml-list] Request for feedback: A problem with injectivity


> 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).

That is true, but isn't this a separate problem? Do you often need to
refer to the type in a branch? On the other hand, good error messages
are needed often, or all the time. 

BTW, GHC does allow naming the type of the existential (I can't
remember the last time I used that for real though). For example,

data E a where
    B :: Bool -> E Bool
    A :: E (a -> b) -> E a -> E b

eval :: E a -> a
eval (B x)   = x
eval (A (f::E (u->v)) x) = (eval f) ((eval x)::u)

Here, I named the type of the argument, which is quantified by the
existential, as u. However, GHC does not use those types in the error
message. For example, if I make a mistake

eval :: E a -> a
eval (B x)   = x
eval (A (f::E (u->v)) x) = (eval f) (x::u)

I get the error message which talks about the type a
/tmp/ga.hs:9:38:
    Couldn't match type `a1' with `E a1'
      `a1' is a rigid type variable bound by
           a pattern with constructor
             A :: forall b a. E (a -> b) -> E a -> E b,
           in an equation for `eval'
           at /tmp/ga.hs:9:7
    In the second argument of `eval', namely `(x :: u)'
    In the expression: (eval f) (x :: u)
    In an equation for `eval':
        eval (A (f :: E (u -> v)) x) = (eval f) (x :: u)

I would argue that is reasonable: the error message quotes the
declaration of GADT; it is only logical it would use the types from
that declaration.