GADT Type Checking GHC 6.10 versus older GHC

[Simon Peyton-Jones]

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 grant that it's less convenient than one would like.  The difficulty is that GADTs get you into territory where it's easy to write programs that  have multiple *incomparable* types.   That is, there is no "best" type (unlike Hindley-Milner).  So we pretty much have to ask the programmer to express the type.

Once we are in that territory, we need to give simple rules that say when a type signature is needed.   I know that I have not yet found a way to express these rules -- perhaps GHC's users can help.  My initial shot is http://haskell.org/haskellwiki/Upgrading_packages%23Changes_to_GADT_matching#Changes_to_GADT_matching



I couldn't figure out how to fix that code by just adding a type signature.

Did you try giving a type signature to the (entire) case expression, as I suggested?  That should do it.

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.

If I knew how to do that, I'd love to.  Here's one idea you might not like: restrict GADT matching to function definitions only (not case expressions), and require a type signature for such pattern matches.  That wouldn't require adding new stuff.  But GHC's current story is a bit more flexible.

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.

I agree they are confusing.  I always encourage people to suggest alternative wording for an error message that would make it less confusing (leaving aside how feasible or otherwise it'd be to generate such wording). So next time you are confused but figure it out, do suggest an alternative.

Thanks for helping.  You can't develop a good user interface without articulate and reflective users.  Thanks.

Simon

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20081124/0c6f9d83/attachment-0001.htm