GADT Type Checking GHC 6.10 versus older GHC

[Jason Dagit]

On Fri, Nov 21, 2008 at 8:57 AM, Simon Peyton-Jones
<simonpj at microsoft.com>wrote:

> You need a type signature for the case expression.  As Daniel says, this is
> worth a read
>
> http://haskell.org/haskellwiki/Upgrading_packages%23Changes_to_GADT_matching#Changes_to_GADT_matching


Thanks Simon.  I had read that several times in the past and I've pointed it
out to others.  It's still relevant but, my question was about whether or
not examples like the one posted are really in error or if GHC is just being
overly strict now.

In my case, we had rigid type signatures all over the place.  The wiki
document says that the type must be rigid at the point of the match.  I
guess that's what we were violating.  If the code I posted isn't supposed to
type check then I would like to report, as user feedback, that GADTs have
become unwieldy.

I couldn't figure out how to fix that code by just adding a type signature.
 The only way I could manage to fix it was to remove the case-expressions
and replace them with local functions and give the type signature of those
functions.  From a practical point of view, it seems that GADTs cannot be
used with case-expressions.  So that means that I am now unable to use
pattern matches on GADTs with case, let, and where.

I urge you to consider designing a modified or new syntactic form for
working with GADT pattern matches.  The quasi-dependent typing that GADTs
give developers is very powerful and it would seem that GHC Haskell with
GADTs is as close to dependent typing that developers writing "real-world"
software can get.  I know of no other production ready compilers that
provide dependent or close to dependent typing.  Dependent typing seems to
be a growing area of interest.  For these reasons I think it's important for
GHC to focus on making them pleasanter to work with again; even if it means
adding to the language again.

I also feel that the type errors given when working with existential types,
especially GADTs with existentials, are confusing.  I think mostly because
the types of the sub-expressions in the program are not visible to the user.
 More introspection into the inferred types would help users.  I have some
ideas on how to improve this, what the output should look like and I would
like to implement it too, but I haven't had a chance to start a prototype
yet.

Thank you for your time!
Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20081121/57eedcce/attachment-0001.htm