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

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Reply via email to