I found a really minor bug in the "new" function in StackSet.hs. I've attached a patch to fix it. More interesting, however, is how I found this. I've been transcribing XMonad's StackSets to the functional language/proof assistant Coq. I've set up a darcs repository with my work so far: darcs get www.cs.nott.ac.uk/~wss/repos/StackSet At the moment I have a fairly complete implementation of StackSets in Coq. I have to admit that I did cut a few corners here and there, but there's nothing that can't be fixed with a bit more work. From this Coq file, you can (in principle) extract Haskell code that is pretty close to the current StackSet.hs. I should emphasize that I haven't proven much about StackSets just yet. This only shows that the definitions in StackSet.hs can be made total (i.e. non-crashing and terminating) in a richer type theory. It should be fun to prove some QuickCheck properties in Coq – which is what I'd like to do next. Wouter