Re: [Caml-list] Request for feedback: A problem with injectivity

[oleg@okmij.org]

> 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?