Weight-biased leftist heaps verified in Haskell using dependent types

I hope the title is self-explanatory. Weight biased leftist heap data structure is taken from chapter 3 of Okasaki. I originally wrote the code in Agda. After listening to your keynote lecture at ICFP I finally decided to port it to Haskell. Upstream repo is [here](https://github.com/jstolarek/dep-typed-wbl-heaps-hs). Companion blog post is [here](http://lambda.jstolarek.com/2014/10/weight-biased-leftist-heaps-verified-in-haskell-using-dependent-types/).