module Unification (
  UP,
  unify
  ) where
import CoreFP

type UP = [(Type, Type)]

tsubUP :: TSub -> UP -> UP
tsubUP s = map (\(l, r) -> (tsub s l, tsub s r))

unify :: UP -> TSub
unify eqs = go [] eqs
  where
    go s []       = s
    go s (eq:eqs) =
      go (s `tcomp` s') (eqs' ++ tsubUP s' eqs)
      where
        (eqs', s') = step eq
    step :: (Type, Type) -> (UP, TSub)
    step (t, u) | t == u      = ([], [])
    step (TVar x, t)          = singletonSub x t
    step (t, TVar x)          = singletonSub x t
    step (TCon f ts, TCon g us) |
      f == g && length ts == length us = (zip ts us, [])
    step _                    = notUnif
    notUnif = error "not unifiable"
    singletonSub x t =
      if x `elem` tvars t then notUnif else ([], [(x, t)])