The Hindley-Milner's algorithm of unification of two types. If they could be unified, of course.

HindleyMilner.hs

module HindleyMilner where
import Control.Applicative ((<|>))
import Control.Monad (guard)
import Data.Maybe (fromJust)

type Symb = String

infixr 3 :->

data Type
  = TVar Symb
  | Type :-> Type
  deriving (Eq, Show)
  
subst :: [(Type,Type)] -> Type -> Maybe Type
subst lst t =
  case t of
    (t1 :-> t2) -> (:->) <$> (subst lst t1) <*> (subst lst t2)
    _           -> lookup t lst <|> Just t

freeVars :: Type -> [Symb]
freeVars (TVar x) = [x]
freeVars (t1 :-> t2) = freeVars t1 ++ freeVars t2

unify :: Type -> Type -> Maybe [(Type, Type)]
unify  va@(TVar _) vb@(TVar _) =
  if va == vb
  then Just [] 
  else Just [(va, vb)]
unify va@(TVar a) t
  | a `elem` freeVars t = Nothing
  | otherwise = Just [(va,t)]
unify t@(_ :-> _) va@(TVar _) = unify va t
unify (s1 :-> s2) (t1 :-> t2) = do
  uni2 <- unify s2 t2
  s1' <- subst uni2 s1
  t1' <- subst uni2 t1
  uniNew <- unify s1' t1'
  return $ uni2 ++ uniNew

-- Tests
{-
seqSubst lst e = foldl (\e s -> fromJust $ subst [s] e) e lst
test a b = unify a b >>= \lst -> return $ seqSubst lst a == seqSubst lst b
test (TVar "a" :-> TVar "b" :-> TVar "c") (TVar "d" :-> TVar "d")
test (TVar "b" :-> TVar "b") (((TVar "g" :-> TVar "d") :-> TVar "e") :-> TVar "a" :-> TVar "d")
test (TVar "a" :-> TVar "b" :-> TVar "a") (TVar "g" :-> TVar "d")
-}

To beautify types and write them like in usual Haskell, the next mess of code is produced. To work it requires

cabal install regex-applicative megaparsec 

Place this file in the same directory as HindleyMilner.hs, run ghci there and load the code

>:l TypeParser.hs

then copy and paste the strings with test commands from the end of file. Now you can test various simple types for possible unification. Look at the resulting type and the required substitutions for the originals to mutate into it. The order of substitutions from left to right.

TypeParser.hs

module TypeParser where

import Control.Monad (void, guard)
import Data.Void
import Data.Maybe
import Text.Megaparsec
import Text.Megaparsec.Expr
import Text.Megaparsec.Char 
import qualified Text.Megaparsec.Char.Lexer as L
import qualified Control.Monad.State as S
import qualified Text.Regex.Applicative as RE
import HindleyMilner

type Parser = Parsec Void String

symbol :: String -> Parser String
symbol = L.symbol space

lexeme :: Parser a -> Parser a
lexeme = L.lexeme space

expr = makeExprParser term table <?> "expression"

term = parens expr <|> lexeme var <?> "term"

parens = between (symbol "(") (symbol ")")

var :: Parser Type
var = do
  name <- (:) <$> letterChar <*> many alphaNumChar
  return $ TVar name

table = [ [ binary  "->"  (:->) ] ]

binary  name f = InfixL  (f <$ symbol name)


seqSubst lst e = foldl (\e s -> fromJust $ subst [s] e) e lst

re1 = RE.string " " *> RE.string ")"
re2 = RE.string "(" <* RE.string " " 

prettyShow :: Type -> String
prettyShow = RE.replace re2 . RE.replace re1 . unwords 
             . map (filter (flip notElem ":\""))
             . filter (/="TVar") . S.evalState prs . show

testS aS bS = do
  a <- runParser expr "" aS
  b <- runParser expr "" bS
--  maybe (Left Nothing) Right $ do
  return $ do
    lst <- unify a b 
    let aNew = seqSubst lst a
    guard $ aNew == seqSubst lst b
    return $ prettyShow aNew
--    return aNew
    

unifyS aS bS = do
  a <- runParser expr "" aS
  b <- runParser expr "" bS
  return $ map (\(a,b) -> (prettyShow a, prettyShow b)) <$> unify a b 
--  return $ unify a b 

lexing :: S.State String String
lexing = S.state (head . lex)

prs = do 
  l <- lexing
  if l == ""
  then return []
  else do 
    ls <- prs
    return (l:ls)


test a b = do
  print $ testS a b
  print $ unifyS a b 

{- Tests
test "b -> a -> b "      "(g -> g) -> d"
test "a -> ( b -> c )"   "d -> d"
test "b -> b"              "((g -> d) -> e) -> (a -> d)"
test "a -> b -> a"       "g -> d"
-}