One drawback of the Hindley-Milner type system is that its typecheckers are necessarily non-compositional. The basic idea here is that this can result in "non-s

One drawback of the Hindley-Milner type system is that its typecheckers are necessarily non-compositional. The basic idea here is that this can result in "non-symmetrical" error messages[1]: given something like MkPair :: a -> b -> Pair a b not :: Bool -> Bool succ :: Int -> Int foo x = MkPair (succ x) (not x) the error message will either complain that `x` has type `Bool` but it should be `Int`, or it will complain that `x` has type `Int` but it should be `Bool` -- depending on what implementation you use! For example, in Haskell, Hugs 98 will emit the first error message, but GHC 7.10 will emit the second (see the full example in my slides[2]). And in some sense, neither is right (and certainly neither is as helpful for the programmer as it could be). So next time you're implementing vanilla HM, maybe consider a compositional type system[3] instead, which can give the following, much more informative error message: Cannot unify 'Int' with 'Bool' when unifying 'x': Cannot unify 'Int' with 'Bool' in the following context: MkPair (succ x) (not x) Bool -> Pair Int Bool Bool x :: Int Bool I have a simple implementation here[4], and am about to release a new version which works on `haskell-src-ext`'s AST to support more of Haskell 98 syntax (but still for vanilla HM only). [1] https://gergo.erdi.hu/blog/2010-10-23-the_case_for_compositional_type_checking/ https://gergo.erdi.hu/blog/2010-10-23-the_case_for_compositi... [2] https://gergo.erdi.hu/talks/2016-06-compty/CompTy.pdf https://gergo.erdi.hu/talks/2016-06-compty/CompTy.pdf [3] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.818 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.8... [4] https://github.com/gergoerdi/hm-compo/blob/master/src/Language/HM/Compositional.hs https://github.com/gergoerdi/hm-compo/blob/master/src/Langua...