<br><br><div class="gmail_quote">On Fri, Nov 21, 2008 at 8:57 AM, Simon Peyton-Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
You need a type signature for the case expression. As Daniel says, this is worth a read<br>
<a href="http://haskell.org/haskellwiki/Upgrading_packages%23Changes_to_GADT_matching#Changes_to_GADT_matching" target="_blank">http://haskell.org/haskellwiki/Upgrading_packages%23Changes_to_GADT_matching#Changes_to_GADT_matching</a></blockquote>
<div><br></div><div>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.</div>
<div><br></div><div>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.</div>
<div><br></div><div>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.</div>
<div><br></div><div>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.</div>
<div><br></div><div>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.</div>
<div><br></div><div>Thank you for your time!</div><div>Jason</div></div>