Hi, {- ICFP referees look away now -} Dons asked me to check some of the StackSet code for potential pattern match errors, and indeed, there are some. I used Catch (http://www-users.cs.york.ac.uk/~ndm/catch/) to do all the testing. The first thing I had to do was apply a 2 line patch to get that module building with Yhc/nhc, to do with defaulting. Next I ran the program and found: 1) view related: * view calls error, this clearly makes it possible to crash. * raiseFocus calls view 2) head related: * promote calls head, in a potentially unsafe manner 3) tail related: * swap calls tail, again potentially unsafe. This one is easy to fix, simply use drop 1. This also means that promote could crash due to swap. 4) fromJust related: index calls fromJust, which means that it may crash. This means that all functions calling index are potentially unsafe, including: delete, insert, promote, push, shift, view, raiseFocus I took a look at delete, and it looks like the safety depends on the stacks and the cache all agreeing - plus possibly some other invariants. You could probably rewrite some of this code to be more rebust, and gain a proof of safety. 5) everything else: Everything else is safe, apart from (potentially) the Ord instances passed around - I abstracted them away for the testing of Data.Map. Realistically, I think you are fine on this point. This means you have a proof of pattern match safety for: screen, peekStack, empty, peek, member, rotate, workspace, visibleWorkspaces No changes were required for testing (other than the 2 line one for Yhc) - the test sits in a separate module and is very simple: main = screen ||| peekStack ||| index ||| empty ||| peek ||| push ||| delete ||| member ||| raiseFocus ||| rotate ||| promote ||| shift ||| view ||| workspace ||| insert ||| visibleWorkspaces ||| swap I hope some of that is useful to you. The testing is 100% automatic and pretty easy to run, once you have Yhc and Catch installed and configured. You have two choices related to pattern match failure: 1) Ignore it, guard against with QuickCheck 2) Prove it, using Catch You also have three options regarding Catch use: 1) Integrate the 2 line change, add the Catch module testing framework in so anyone with Catch installed can replicate these tests - and check you don't get worse. 2) Have a catch branch, which has the library driver and the patch. This would be a really small branch :-) 3) Don't do anything, I can continue to check things occasionally. I'm on #haskell as ndm, so let me know if you want any help running any of this. Thanks Neil