equations' :: (MonadError String m) => Env -> Expr -> Type -> [Symb] -> m [(Type,Type)]
equations' (Env env) (Var s) t bad = do
                                let res = lookup s env
                                case res of {(Just r) -> return $ [(t, r)] ;
                                              Nothing -> throwError $ "There is no variable " ++ (show s) ++ " in the enviroment."}


equations' e@(Env env) expr@(m :@ n) t bad = do
                                 e1 <- (equations' e m (TVar alpha :-> t) (alpha : bad ++ allVars expr ++ freeTVarsEnv e))
                                 e2 <- (equations' e n (TVar alpha) (alpha : bad ++ allVars expr ++ freeTVarsEnv e))
                                 return $ e1 ++ e2
                                 where alpha = getNext' (bad ++ allVars expr ++ freeTVarsEnv e)
                                       --beta = getNext' expr (alpha : bad)

equations' e@(Env env) expr@(Lam x mm) t bad = do
                e1 <- (equations' (Env $ (x, TVar alpha) : env) mm (TVar beta) (alpha : beta : bad ++ allVars expr ++ freeTVarsEnv e))
                return $ (TVar alpha :-> TVar beta, t) : e1
                     where alpha  = getNext' (bad ++ allVars expr ++ freeTVarsEnv e)
                           beta   = getNext' (alpha : bad ++ allVars expr ++ freeTVarsEnv e)



allVars :: Expr -> [Symb]
allVars (Var v) = [v]
allVars (e1 :@ e2) = (allVars e1) ++ (allVars e2)
allVars (Lam s e) = s : (allVars e)

principlePair :: (MonadError String m) =>  Expr -> m (Env,Type)
principlePair expr = do
                     let env = [(a, TVar (a ++ "name")) | a <- freeVars expr]
                     let bad = [a ++ "name" | a <- freeVars expr]
                     eqs <- equations' (Env env) expr (TVar "answertype") bad
                     res <- unif2 eqs (SubsTy [])
                     return $ (appSubsEnv res (Env env), appSubsTy res (TVar "answertype"))

unif2 :: (MonadError String m) =>  [(Type,Type)] -> SubsTy -> m SubsTy
unif2 ((a, b):xs) s = do
       g <- unify (appSubsTy s a) (appSubsTy s b)
       unif2 xs (composeSubsTy g s)
unif2 [] s = return s

l = 5 `replicateM` "abcdefghijklmnopqrstuvwxyz012346789"
getNext' bad = head (l \\  bad)