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 C01E081792
	for <caml-list@sympa.inria.fr>; Thu,  4 Jul 2013 08:07:50 +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: AjoCAO4P1VFCJwNzemdsb2JhbABAGoM7wQiBIQ4BAQsHDQk8giMBAQQBJ1IFFjRpFIgOBgwzuWKPawcWg1cDl0gBgSmTLTw
X-IPAS-Result: AjoCAO4P1VFCJwNzemdsb2JhbABAGoM7wQiBIQ4BAQsHDQk8giMBAQQBJ1IFFjRpFIgOBgwzuWKPawcWg1cDl0gBgSmTLTw
X-IronPort-AV: E=Sophos;i="4.87,992,1363129200"; 
   d="scan'208";a="24522621"
Received: from www1.g3.pair.com ([66.39.3.115])
  by mail2-smtp-roc.national.inria.fr with SMTP; 04 Jul 2013 08:07:49 +0200
Received: (qmail 15629 invoked by uid 9370); 4 Jul 2013 06:07:48 -0000
Date: 4 Jul 2013 06:07:48 -0000
Message-ID: <20130704060748.15628.qmail@www1.g3.pair.com>
From: oleg@okmij.org
To: gabriel.scherer@gmail.com
CC: garrigue@math.nagoya-u.ac.jp, caml-list@inria.fr
In-reply-to:
	<CAPFanBFU_M+=q4Jk5BaaAhD86KN-E3rdwO6JwdDTRGgcsU-utw@mail.gmail.com>
Subject: Re: [Caml-list] Request for feedback: A problem with injectivity


> Indeed, virtually anyone that used GADTs in OCaml encountered that
> problem and has a way to name existential type high on his/her
> wishlist. We discussed a few ideas in the following bugtracking
> dicussion:
>
>   http://caml.inria.fr/mantis/view.php?id=5780

Just in case, here is the error message produced by GHC for the
equivalent example. 

Code:

{-# LANGUAGE GADTs #-}

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 x) = (eval f) x

The error message:

/tmp/ga.hs:9:25:
    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'
    In the expression: (eval f) x
    In an equation for `eval': eval (A f x) = (eval f) x

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?