Lambda the Ultimate

I am pleased to announce that LaTiKi is now available as a public beta.

LaTiKi accepts LaTeX syntax as input rather than the wiki syntax that is
standard across many wiki implementations. This Wiki enables LaTeX users to
collaborate on papers, edit, and track each paper. It is entirely based upon
the open-source and widely used platform MediaWiki. I am looking for
interested users to contribute, try out how well the system works and how
useful the system really is. I also hope that any major underlying bugs are
identified.

I have prepared a sandbox wiki with some of Philip Wadler's papers on the
site to demonstrate how the system works. Note that to be able to edit
papers on the sandbox you MUST sign up to the site and confirm your email
address. This is available at http://www.stuartbeard.com/wiki
Feedback is greatly appreciated.

If any readers are interested in this project and would like to do a similar
thing with their own papers then a tarball is available
at http://www.stuartbeard.com/project or http://www.mediafire.com/file/lymzlwz3m0m/latexwiki-1.0.1b.tar

I came across this paper proposing that Let Should Not Be Generalized (TLDI 2010, Vytiniotis, Peyton Jones, and Schrijvers).

While generalisation for local let bindings is straightforward in Hindley-Milner, we show that it becomes much more complicated in more sophisticated type systems. The extensions we have in mind include functional dependencies, GADTs, units of measure, and type functions. The only technically straightforward way to combine these developments with let-generalisation has unpalatable practical consequences, that appear to be unavoidable.

I'm actually fairly convinced by this. Among other things, it provides a fairly clear path to eliminating the monomorphism restriction:

Our [] proposal completely subsumes the [Haskell monomorphism restriction] for local let bindings, so the MR would then only apply to top-level bindings. In that case the arguments for its abolition, or for generating a warning rather than rejecting the program, would become very strong. A nasty wart would thereby be removed from the face of Haskell.

Are they right? Are they wrong? Has anyone laid out the case for the defense?