Hindley-Milner with top-level existentials April 24, 2016
Content advisory: This is a half-baked research post.
Abstract. Top-level unpacking of existentials are easy to integrate into Hindley-Milner type inference. Haskell should support them. It’s possible this idea can work for internal bindings of existentials as well (ala F-ing modules) but I have not worked out how to do it.
Update. And UHC did it first!
Update 2. And rank-2 type inference is decidable (and rank-1 existentials are an even weaker system), although the algorithm for rank-2 inference requires semiunification.