Unification

unify :: Equations -> Maybe Substitution unify eqs = unify' eqs [] unify' :: Equations -> Substitution -> Maybe Substitution unify' [] s = Just s unify' ((Var x,Var y):eqs) s | x==y = unify' eqs s unify' ((Var x,t):eqs) s | x `elem` vars t = Nothing | not (x `elem` vars t) = unify' (substEqs x t eqs) ((x,t):substS x t s) unify' ((Fun f ts,Var x):eqs) s = unify' ((Var x,Fun f ts):eqs) s unify' ((Fun f ts1,Fun g ts2):eqs) s | f/=g || length ts1/=length ts2 = Nothing | f==g && length ts1==length ts2 = unify' (zip ts1 ts2++eqs) s