-----------------------------------------------------------------------------
--
-- Module      :  PureScript.TypeChecker.Types
-- Copyright   :  (c) Phil Freeman 2013
-- License     :  MIT
--
-- Maintainer  :  Phil Freeman <paf31@cantab.net>
-- Stability   :  experimental
-- Portability :
--
-- |
--
-----------------------------------------------------------------------------

module PureScript.TypeChecker.Types (
    TypeConstraint(..),
    TypeSolution(..),
    typeOf
) where

import Data.List
import Data.Function

import PureScript.Values
import PureScript.Types
import PureScript.TypeChecker.Monad

import Control.Monad.State
import Control.Monad.Error

import Control.Applicative
import Control.Arrow (Kleisli(..), (***), (&&&))
import qualified Control.Category as C

import qualified Data.Map as M

data TypeConstraint
  = TypeConstraint Int Type
  | RowConstraint Int Row deriving Show

newtype TypeSolution = TypeSolution { runTypeSolution :: (Int -> Type, Int -> Row) }

emptyTypeSolution :: TypeSolution
emptyTypeSolution = TypeSolution (TUnknown, RUnknown)

typeOf :: String -> Value -> Check Type
typeOf name val = do
  me <- fresh
  (cs, n) <- typeConstraints (M.singleton name me) val
  solution <- solveTypeConstraints ((TypeConstraint me (TUnknown n)) : cs) emptyTypeSolution
  return $ varIfUnknown $ fst (runTypeSolution solution) n

varIfUnknown :: Type -> Type
varIfUnknown = flip evalState M.empty . varIfUnknown'
  where
  varIfUnknown' :: Type -> State (M.Map Int String) Type
  varIfUnknown' (TUnknown n) = do
    m <- get
    case M.lookup n m of
      Nothing -> do
        let name = "t" ++ show (M.size m)
        put $ M.insert n name m
        return $ TypeVar name
      Just name -> return $ TypeVar name
  varIfUnknown' (Array t) = Array <$> varIfUnknown' t
  varIfUnknown' (Object row) = Object <$> varIfUnknown'' row
  varIfUnknown' (Function args ret) = Function <$> mapM varIfUnknown' args <*> varIfUnknown' ret
  varIfUnknown' (TypeApp t1 t2) = TypeApp <$> varIfUnknown' t1 <*> varIfUnknown' t2
  varIfUnknown' t = return t
  varIfUnknown'' :: Row -> State (M.Map Int String) Row
  varIfUnknown'' (RUnknown n) = do
    m <- get
    case M.lookup n m of
      Nothing -> do
        let name = "r" ++ show (M.size m)
        put $ M.insert n name m
        return $ RowVar name
      Just name -> return $ RowVar name
  varIfUnknown'' (RCons name ty row) = RCons name ty <$> varIfUnknown'' row
  varIfUnknown'' r = return r

replaceVarsWithUnknowns :: Type -> Check Type
replaceVarsWithUnknowns = flip evalStateT M.empty . replaceVarsWithUnknowns'
  where
  replaceVarsWithUnknowns' :: Type -> StateT (M.Map String Int) Check Type
  replaceVarsWithUnknowns' (Array t) = Array <$> replaceVarsWithUnknowns' t
  replaceVarsWithUnknowns' (Object row) = Object <$> replaceVarsWithUnknowns'' row
  replaceVarsWithUnknowns' (Function args ret) = Function <$> mapM replaceVarsWithUnknowns' args <*> replaceVarsWithUnknowns' ret
  replaceVarsWithUnknowns' (TypeApp t1 t2) = TypeApp <$> replaceVarsWithUnknowns' t1 <*> replaceVarsWithUnknowns' t2
  replaceVarsWithUnknowns' (TypeVar var) = do
    m <- get
    n <- lift fresh
    case M.lookup var m of
      Nothing -> do
        put (M.insert var n m)
        return $ TUnknown n
      Just u -> return $ TUnknown u
  replaceVarsWithUnknowns' t = return t
  replaceVarsWithUnknowns'' :: Row -> StateT (M.Map String Int) Check Row
  replaceVarsWithUnknowns'' (RowVar var) = do
    m <- get
    n <- lift fresh
    case M.lookup var m of
      Nothing -> do
        put (M.insert var n m)
        return $ RUnknown n
      Just u -> return $ RUnknown u
  replaceVarsWithUnknowns'' (RCons name ty row) = RCons name <$> replaceVarsWithUnknowns' ty <*> replaceVarsWithUnknowns'' row
  replaceVarsWithUnknowns'' r = return r

typeConstraints :: M.Map String Int -> Value -> Check ([TypeConstraint], Int)
typeConstraints _ (NumericLiteral _) = do
  me <- fresh
  return ([TypeConstraint me Number], me)
typeConstraints _ (StringLiteral _) = do
  me <- fresh
  return ([TypeConstraint me String], me)
typeConstraints _ (BooleanLiteral _) = do
  me <- fresh
  return ([TypeConstraint me Boolean], me)
typeConstraints m (ArrayLiteral vals) = do
  all <- mapM (typeConstraints m) vals
  let (cs, ns) = (concat . map fst &&& map snd) all
  me <- fresh
  return (cs ++ map (TypeConstraint me . Array . TUnknown) ns, me)
typeConstraints m (Unary op val) = do
  (cs, n1) <- typeConstraints m val
  me <- fresh
  return (cs ++ unaryOperatorConstraints op n1 me, me)
typeConstraints m (Binary op left right) = do
  (cs1, n1) <- typeConstraints m left
  (cs2, n2) <- typeConstraints m right
  me <- fresh
  return (cs1 ++ cs2 ++ binaryOperatorConstraints op n1 n2 me, me)
typeConstraints m (ObjectLiteral ps) = do
  all <- mapM (typeConstraints m . snd) ps
  let (cs, ns) = (concat . map fst &&& map snd) all
  me <- fresh
  let tys = zipWith (\(name, _) u -> (name, TUnknown u)) ps ns
  return ((TypeConstraint me (Object (typesToRow tys))) : cs, me)
  where
    typesToRow [] = REmpty
    typesToRow ((name, ty):tys) = RCons name ty (typesToRow tys)
typeConstraints m (Indexer index val) = do
  (cs1, n1) <- typeConstraints m index
  (cs2, n2) <- typeConstraints m val
  me <- fresh
  return ((TypeConstraint n1 Number) : (TypeConstraint n2 (Array (TUnknown me))) : cs1 ++ cs2, me)
typeConstraints m (Accessor prop val) = do
  (cs, n1) <- typeConstraints m val
  me <- fresh
  rest <- fresh
  return ((TypeConstraint n1 (Object (RCons prop (TUnknown me) (RUnknown rest)))) : cs, me)
typeConstraints m (Abs args ret) = do
  ns <- replicateM (length args) fresh
  let m' = m `M.union` M.fromList (zipWith (,) args ns)
  (cs, n') <- typeConstraints m' ret
  me <- fresh
  return ((TypeConstraint me (Function (map TUnknown ns) (TUnknown n'))) : cs, me)
typeConstraints m (App f xs) = do
  (cs1, n1) <- typeConstraints m f
  all <- mapM (typeConstraints m) xs
  let (cs2, ns) = (concat . map fst &&& map snd) all
  me <- fresh
  return ((TypeConstraint n1 (Function (map TUnknown ns) (TUnknown me))) : cs1 ++ cs2, me)
typeConstraints m (Var var) =
  case M.lookup var m of
    Nothing -> do
      env <- getEnv
      case M.lookup var (names env) of
        Nothing -> throwError $ var ++ " is undefined"
        Just ty -> do
          me <- fresh
          replaced <- replaceVarsWithUnknowns ty
          return ([TypeConstraint me replaced], me)
    Just u -> do
      me <- fresh
      return ([TypeConstraint u (TUnknown me)], me)
typeConstraints m (Block ss) = do
  ret <- fresh
  (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m M.empty ret ss
  guardWith "Block is missing a return statement" allCodePathsReturn
  return (cs, ret)
typeConstraints m (Constructor c) = do
  env <- getEnv
  case M.lookup c (names env) of
    Nothing -> throwError $ c ++ " is undefined"
    Just ty -> do
      me <- fresh
      replaced <- replaceVarsWithUnknowns ty
      return ([TypeConstraint me replaced], me)
typeConstraints m (Case val binders) = do
  (cs1, n1) <- typeConstraints m val
  ret <- fresh
  cs2 <- typeConstraintsForBinders m n1 ret binders
  return (cs1 ++ cs2, ret)
typeConstraints m (TypedValue val ty) = do
  (cs, n1) <- typeConstraints m val
  return ([TypeConstraint n1 ty], n1)
  -- TODO: Kind-check the type

unaryOperatorConstraints :: UnaryOperator -> Int -> Int -> [TypeConstraint]
unaryOperatorConstraints Negate val result = [TypeConstraint val Number, TypeConstraint result Number]
unaryOperatorConstraints Not val result = [TypeConstraint val Boolean, TypeConstraint result Boolean]
unaryOperatorConstraints BitwiseNot val result = [TypeConstraint val Number, TypeConstraint result Number]

binaryOperatorConstraints :: BinaryOperator -> Int -> Int -> Int -> [TypeConstraint]
binaryOperatorConstraints Add = symBinOpConstraints Number
binaryOperatorConstraints Subtract = symBinOpConstraints Number
binaryOperatorConstraints Multiply = symBinOpConstraints Number
binaryOperatorConstraints Divide = symBinOpConstraints Number
binaryOperatorConstraints Modulus = symBinOpConstraints Number
binaryOperatorConstraints LessThan = asymBinOpConstraints Number Boolean
binaryOperatorConstraints LessThanOrEqualTo = asymBinOpConstraints Number Boolean
binaryOperatorConstraints GreaterThan = asymBinOpConstraints Number Boolean
binaryOperatorConstraints GreaterThanOrEqualTo = asymBinOpConstraints Number Boolean
binaryOperatorConstraints BitwiseAnd = symBinOpConstraints Number
binaryOperatorConstraints BitwiseOr = symBinOpConstraints Number
binaryOperatorConstraints BitwiseXor = symBinOpConstraints Number
binaryOperatorConstraints ShiftLeft = symBinOpConstraints Number
binaryOperatorConstraints ShiftRight = symBinOpConstraints Number
binaryOperatorConstraints ZeroFillShiftRight = symBinOpConstraints Number
binaryOperatorConstraints EqualTo = equalityBinOpConstraints
binaryOperatorConstraints NotEqualTo = equalityBinOpConstraints
binaryOperatorConstraints And = symBinOpConstraints Boolean
binaryOperatorConstraints Or = symBinOpConstraints Boolean
binaryOperatorConstraints Concat = symBinOpConstraints String

equalityBinOpConstraints :: Int -> Int -> Int -> [TypeConstraint]
equalityBinOpConstraints left right result = [TypeConstraint left (TUnknown right), TypeConstraint result Boolean]

symBinOpConstraints :: Type -> Int -> Int -> Int -> [TypeConstraint]
symBinOpConstraints ty left right result = asymBinOpConstraints ty ty left right result

asymBinOpConstraints :: Type -> Type -> Int -> Int -> Int -> [TypeConstraint]
asymBinOpConstraints ty res left right result = [TypeConstraint left ty, TypeConstraint right ty, TypeConstraint result res]

typeConstraintsForBinder :: Int -> Binder -> Check ([TypeConstraint], M.Map String Int)
typeConstraintsForBinder val (StringBinder _) = constantBinder val String
typeConstraintsForBinder val (NumberBinder _) = constantBinder val Number
typeConstraintsForBinder val (BooleanBinder _) = constantBinder val Boolean
typeConstraintsForBinder val (VarBinder name) = do
  me <- fresh
  return ([TypeConstraint me (TUnknown val)], M.singleton name me)
typeConstraintsForBinder val (NullaryBinder ctor) = do
  env <- getEnv
  case M.lookup ctor (names env) of
    Just ret -> do
      ret' <- replaceVarsWithUnknowns ret
      return ([TypeConstraint val ret'], M.empty)
    _ -> throwError $ "Constructor " ++ ctor ++ " is not defined"
typeConstraintsForBinder val (UnaryBinder ctor binder) = do
  env <- getEnv
  case M.lookup ctor (names env) of
    Just f@(Function [ty] ret) -> do
      obj <- fresh
      Function [ty'] ret' <- replaceVarsWithUnknowns f
      (cs, m1) <- typeConstraintsForBinder obj binder
      return ((TypeConstraint val ret') : (TypeConstraint obj ty') : cs, m1)
    Just _ -> throwError $ ctor ++ " is not a unary constructor"
    _ -> throwError $ "Constructor " ++ ctor ++ " is not defined"
typeConstraintsForBinder val (ObjectBinder props) = do
  row <- fresh
  rest <- fresh
  (cs, m1) <- typeConstraintsForProperties row (RUnknown rest) props
  return ((TypeConstraint val (Object (RUnknown row))) : cs, m1)
  where
  typeConstraintsForProperties :: Int -> Row -> [(String, Binder)] -> Check ([TypeConstraint], M.Map String Int)
  typeConstraintsForProperties nrow row [] = return ([RowConstraint nrow row], M.empty)
  typeConstraintsForProperties nrow row ((name, binder):binders) = do
    propTy <- fresh
    (cs1, m1) <- typeConstraintsForBinder propTy binder
    (cs2, m2) <- typeConstraintsForProperties nrow (RCons name (TUnknown propTy) row) binders
    return (cs1 ++ cs2, M.union m1 m2)
typeConstraintsForBinder val (ArrayBinder binders rest) = do
  el <- fresh
  all <- mapM (typeConstraintsForBinder el) binders
  let (cs1, m1) = (concat . map fst &&& M.unions . map snd) all
  let arrayConstraint = TypeConstraint val (Array (TUnknown el))
  case rest of
    Nothing -> return (arrayConstraint : cs1, m1)
    Just binder -> do
      (cs2, m2) <- typeConstraintsForBinder val binder
      return (arrayConstraint : cs1 ++ cs2, M.union m1 m2)

constantBinder :: Int -> Type -> Check ([TypeConstraint], M.Map String Int)
constantBinder val ty = return ([TypeConstraint val ty], M.empty)

typeConstraintsForBinders :: M.Map String Int -> Int -> Int -> [(Binder, Value)] -> Check [TypeConstraint]
typeConstraintsForBinders _ _ _ [] = return []
typeConstraintsForBinders m nval ret ((binder, val):bs) = do
  (cs1, m1) <- typeConstraintsForBinder nval binder
  (cs2, n2) <- typeConstraints (M.union m m1) val
  cs3 <- typeConstraintsForBinders m nval ret bs
  return ((TypeConstraint n2 (TUnknown ret)) : cs1 ++ cs2 ++ cs3)

typeConstraintsForStatement :: M.Map String Int -> M.Map String Int -> Int -> Statement -> Check ([TypeConstraint], Bool, M.Map String Int)
typeConstraintsForStatement m mass ret (VariableIntroduction name val) = do
  case M.lookup name (m `M.union` mass) of
    Nothing -> do
      (cs1, n1) <- typeConstraints m val
      return $ (cs1, False, M.insert name n1 mass)
    Just ty -> throwError $ "Variable with name " ++ name ++ " already exists."
typeConstraintsForStatement m mass ret (Assignment tgt val) = do
  (cs1, n1) <- typeConstraints m val
  cs2 <- typeConstraintsForAssignmentTarget m mass n1 tgt
  return (cs1 ++ cs2, False, mass)
typeConstraintsForStatement m mass ret (While val inner) = do
  (cs1, n1) <- typeConstraints m val
  (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret inner
  return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2, allCodePathsReturn, mass)
typeConstraintsForStatement m mass ret (IfThenElse val thens Nothing) = do
  (cs1, n1) <- typeConstraints m val
  (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret thens
  return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2, allCodePathsReturn, mass)
typeConstraintsForStatement m mass ret (IfThenElse val thens (Just elses)) = do
  (cs1, n1) <- typeConstraints m val
  (cs2, allCodePathsReturn1, _) <- typeConstraintsForBlock m mass ret thens
  (cs3, allCodePathsReturn2, _) <- typeConstraintsForBlock m mass ret elses
  return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2 ++ cs3, allCodePathsReturn1 && allCodePathsReturn2, mass)
typeConstraintsForStatement m mass ret (For (init, cond, cont) inner) = do
  (cs1, b1, mass1) <- typeConstraintsForStatement m mass ret init
  guardWith "Cannot return from inside for" $ not b1
  (cs2, n1) <- typeConstraints (m `M.union` mass1) cond
  (cs3, b2, mass2) <- typeConstraintsForStatement (m `M.union` mass1) mass1 ret cont
  guardWith "Cannot return from inside for" $ not b2
  (cs4, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass2) mass2 ret inner
  return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2 ++ cs3 ++ cs4, allCodePathsReturn, mass)
typeConstraintsForStatement m mass ret (Return val) = do
  (cs1, n1) <- typeConstraints (m `M.union` mass) val
  return ((TypeConstraint n1 (TUnknown ret)) : cs1, True, mass)

typeConstraintsForAssignmentTarget :: M.Map String Int -> M.Map String Int -> Int -> AssignmentTarget -> Check [TypeConstraint]
typeConstraintsForAssignmentTarget m mass nval (AssignVariable var) =
  case M.lookup var mass of
    Nothing -> throwError $ "No local variable with name " ++ var
    Just ty -> do
     return [TypeConstraint nval (TUnknown ty)]
typeConstraintsForAssignmentTarget m mass nval (AssignArrayIndex index tgt) = do
  arr <- fresh
  (cs1, n1) <- typeConstraints (m `M.union` mass) index
  cs2 <- typeConstraintsForAssignmentTarget m mass arr tgt
  return $ (TypeConstraint arr (Array (TUnknown nval))) : (TypeConstraint n1 Number) : cs1 ++ cs2
typeConstraintsForAssignmentTarget m mass nval (AssignObjectProperty prop tgt) =  do
  obj <- fresh
  row <- fresh
  cs <- typeConstraintsForAssignmentTarget m mass obj tgt
  return $ (TypeConstraint obj (Object (RCons prop (TUnknown nval) $ RUnknown row))) : cs

typeConstraintsForBlock :: M.Map String Int -> M.Map String Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, M.Map String Int)
typeConstraintsForBlock _ mass _ [] = return ([], False, mass)
typeConstraintsForBlock m mass ret (s:ss) = do
  (cs1, b1, mass1) <- typeConstraintsForStatement (m `M.union` mass) mass ret s
  case (b1, ss) of
    (True, []) -> return (cs1, True, mass1)
    (True, _) -> throwError "Unreachable code"
    (False, ss) -> do
      (cs2, b2, mass2) <- typeConstraintsForBlock m mass1 ret ss
      return (cs1 ++ cs2, b2, mass2)

solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
solveTypeConstraints [] s = return s
solveTypeConstraints all@(TypeConstraint n t:cs) s = do
  guardWith "Occurs check failed" $ not $ typeOccursCheck False n t
  let s' = let (f, g) = runTypeSolution s
           in TypeSolution (replaceTypeInType n t . f, replaceTypeInRow n t . g)
  cs' <- fmap concat $ mapM (substituteTypeInConstraint n t) cs
  solveTypeConstraints cs' s'
solveTypeConstraints (RowConstraint n r:cs) s = do
  guardWith "Occurs check failed" $ not $ rowOccursCheck False n r
  let s' = let (f, g) = runTypeSolution s
           in TypeSolution $ (replaceRowInType n r . f, replaceRowInRow n r . g)
  cs' <- fmap concat $ mapM (substituteRowInConstraint n r) cs
  solveTypeConstraints cs' s'

substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
substituteTypeInConstraint n s (TypeConstraint m t)
  | n == m = unifyTypes s t
  | otherwise = return [TypeConstraint m (replaceTypeInType n s t)]
substituteTypeInConstraint n s (RowConstraint m r)
  = return [RowConstraint m (replaceTypeInRow n s r)]

substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
substituteRowInConstraint n r (TypeConstraint m t)
  = return [TypeConstraint m (replaceRowInType n r t)]
substituteRowInConstraint n r (RowConstraint m r1)
  | m == n = unifyRows r r1
  | otherwise = return [RowConstraint m (replaceRowInRow n r r1)]

replaceTypeInType :: Int -> Type -> Type -> Type
replaceTypeInType n t (TUnknown m) | m == n = t
replaceTypeInType n t (Array t1) = Array $ replaceTypeInType n t t1
replaceTypeInType n t (Object row) = Object $ replaceTypeInRow n t row
replaceTypeInType n t (Function args ret) = Function (map (replaceTypeInType n t) args) (replaceTypeInType n t ret)
replaceTypeInType n t (TypeApp t1 t2) = TypeApp (replaceTypeInType n t t1) (replaceTypeInType n t t2)
replaceTypeInType _ _ other = other

replaceTypeInRow :: Int -> Type -> Row -> Row
replaceTypeInRow n t (RCons name ty row) = RCons name (replaceTypeInType n t ty) (replaceTypeInRow n t row)
replaceTypeInRow n t other = other

replaceRowInType :: Int -> Row -> Type -> Type
replaceRowInType n r (Array t1) = Array $ replaceRowInType n r t1
replaceRowInType n r (Object row) = Object $ replaceRowInRow n r row
replaceRowInType n r (Function args ret) = Function (map (replaceRowInType n r) args) (replaceRowInType n r ret)
replaceRowInType n r (TypeApp t1 t2) = TypeApp (replaceRowInType n r t1) (replaceRowInType n r t2)
replaceRowInType _ _ other = other

replaceRowInRow :: Int -> Row -> Row -> Row
replaceRowInRow n r (RUnknown m) | m == n = r
replaceRowInRow n r (RCons name ty row) = RCons name (replaceRowInType n r ty) (replaceRowInRow n r row)
replaceRowInRow _ _ other = other

unifyTypes :: Type -> Type -> Check [TypeConstraint]
unifyTypes (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
unifyTypes (TUnknown u) t = do
  guardWith "Occurs check failed" $ not $ typeOccursCheck False u t
  return [TypeConstraint u t]
unifyTypes t (TUnknown u) = do
  guardWith "Occurs check failed" $ not $ typeOccursCheck False u t
  return [TypeConstraint u t]
unifyTypes Number Number = return []
unifyTypes String String = return []
unifyTypes Boolean Boolean = return []
unifyTypes (Array s) (Array t) = unifyTypes s t
unifyTypes (Object row1) (Object row2) = unifyRows row1 row2
unifyTypes (Function args1 ret1) (Function args2 ret2) = do
  guardWith "Function applied to incorrect number of args" $ length args1 == length args2
  cs1 <- fmap concat $ zipWithM unifyTypes args1 args2
  cs2 <- unifyTypes ret1 ret2
  return $ cs1 ++ cs2
unifyTypes (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
unifyTypes (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = return []
unifyTypes (TypeVar v1) (TypeVar v2) = return []
unifyTypes (TypeApp t1 t2) (TypeApp t3 t4) = do
  cs1 <- unifyTypes t1 t3
  cs2 <- unifyTypes t2 t4
  return $ cs1 ++ cs2
unifyTypes t1 t2 = throwError $ "Cannot unify " ++ show t1 ++ " with " ++ show t2 ++ "."

unifyRows :: Row -> Row -> Check [TypeConstraint]
unifyRows r1 r2 =
  let
    (s1, r1') = toList r1
    (s2, r2') = toList r2
    int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
    sd1 = [ (name, t1) | (name, t1) <- s1, not (elem name (map fst s2)) ]
    sd2 = [ (name, t2) | (name, t2) <- s2, not (elem name (map fst s1)) ]
  in rethrow (const $ "Cannot unify " ++ show r1 ++ " with " ++ show r2) $ do
    cs1 <- fmap concat $ mapM (uncurry unifyTypes) int
    cs2 <- unifyRows' sd1 r1' sd2 r2'
    return $ cs1 ++ cs2
  where
  unifyRows' :: [(String, Type)] -> Row -> [(String, Type)] -> Row -> Check [TypeConstraint]
  unifyRows' [] (RUnknown u) sd r = do
    guardWith "Occurs check failed" $ not $ rowOccursCheck False u r
    return [RowConstraint u (fromList (sd, r))]
  unifyRows' ((name, ty):row) r others (RUnknown u) = do
    u' <- fresh
    cs <- unifyRows' row r others (RUnknown u')
    return [ RowConstraint u (RCons name ty (RUnknown u')) ]
  unifyRows' [] REmpty [] REmpty = return []
  unifyRows' sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ show (fromList (sd1, r1)) ++ " with " ++ show (fromList (sd2, r2)) ++ "."
  toList :: Row -> ([(String, Type)], Row)
  toList (RCons name ty row) = let (tys, rest) = toList row
                               in ((name, ty):tys, rest)
  toList r = ([], r)
  fromList :: ([(String, Type)], Row) -> Row
  fromList ([], r) = r
  fromList ((name, t):ts, r) = RCons name t (fromList (ts, r))

typeOccursCheck :: Bool -> Int -> Type -> Bool
typeOccursCheck b u (TUnknown u') | u == u' = b
typeOccursCheck _ u (Array t) = typeOccursCheck True u t
typeOccursCheck _ u (Object row) = rowOccursCheck True u row
typeOccursCheck _ u (Function args ret) = any (typeOccursCheck True u) args || typeOccursCheck True u ret
typeOccursCheck _ u (TypeApp s t) = typeOccursCheck True u s || typeOccursCheck True u t
typeOccursCheck _ _ _ = False

rowOccursCheck :: Bool -> Int -> Row -> Bool
rowOccursCheck b u (RUnknown u') | u == u' = b
rowOccursCheck _ u (RCons name ty row) = typeOccursCheck True u ty || rowOccursCheck True u row
rowOccursCheck _ _ _ = False