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

[Alain Frisch <alain@frisch.fr>]

On 07/05/2013 12:30 PM, oleg@okmij.org wrote:
>> 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.

To be clear: the GHC way to report errors seems good to me.  But even if 
the default error message is improved, it is still helpful to be able to 
name the existential type simply to be able to write a type annotation 
mentioning that type somewhere deep in the branch (as a way to track 
down the actual error).  Typically, only a very small number of #exN 
types exist in a given scope, so the fact that the error message does 
not tell where they come from is not a blocking point in making sense of 
the error, and not being able to name the type is more problematic.

And of course, there are many other cases where it is useful to name the 
type, not only to track errors, but as ways to document the code or 
simply to be able to write it at all (especially when using local modules).

And to answer your question: yes, I've had to introduce a local 
polymorphic function (with a locally abstract type) quite often to 
work-around the lack of naming facility.

-- Alain