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

[oleg@okmij.org]

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