@@ -0,0 +1,490 @@
1+-----------------------------------------------------------------------------
2+--
3+-- Module : PureScript.TypeChecker.Types
4+-- Copyright : (c) Phil Freeman 2013
5+-- License : MIT
6+--
7+-- Maintainer : Phil Freeman <paf31@cantab.net>
8+-- Stability : experimental
9+-- Portability :
10+--
11+-- |
12+--
13+-----------------------------------------------------------------------------
14+
15+module PureScript.TypeChecker.Types (
16+ TypeConstraint(..),
17+ TypeSolution(..),
18+ typeOf
19+) where
20+
21+import Data.List
22+import Data.Function
23+import Data.Data (Data(..))
24+import Data.Generics (everywhere, everywhereM, everything, mkT, mkM, mkQ, extM, extQ)
25+
26+import PureScript.Values
27+import PureScript.Types
28+import PureScript.Kinds
29+import PureScript.Names
30+import PureScript.TypeChecker.Monad
31+import PureScript.TypeChecker.Kinds
32+import PureScript.TypeChecker.Synonyms
33+
34+import Control.Monad.State
35+import Control.Monad.Error
36+
37+import Control.Applicative
38+import Control.Arrow (Kleisli(..), (***), (&&&))
39+import qualified Control.Category as C
40+
41+import qualified Data.Map as M
42+
43+data TypeConstraint
44+ = TypeConstraint Int Type
45+ | RowConstraint Int Row deriving Show
46+
47+newtype TypeSolution = TypeSolution { runTypeSolution :: (Int -> Type, Int -> Row) }
48+
49+emptyTypeSolution :: TypeSolution
50+emptyTypeSolution = TypeSolution (TUnknown, RUnknown)
51+
52+typeOf :: Ident -> Value -> Check PolyType
53+typeOf name val = do
54+ me <- fresh
55+ (cs, n) <- typeConstraints (M.singleton name me) val
56+ solution <- solveTypeConstraints ((TypeConstraint me (TUnknown n)) : cs) emptyTypeSolution
57+ return $ varIfUnknown $ fst (runTypeSolution solution) n
58+
59+varIfUnknown :: Type -> PolyType
60+varIfUnknown ty =
61+ let
62+ (ty', m) = flip runState M.empty $ everywhereM (flip extM g $ mkM f) ty
63+ -- TODO : check no nested unknowns
64+ in
65+ PolyType (sort $ nub $ M.elems m) ty'
66+ where
67+ f :: Type -> State (M.Map Int String) Type
68+ f (TUnknown n) = do
69+ m <- get
70+ case M.lookup n m of
71+ Nothing -> do
72+ let name = "t" ++ show (M.size m)
73+ put $ M.insert n name m
74+ return $ TypeVar name
75+ Just name -> return $ TypeVar name
76+ f t = return t
77+ g :: Row -> State (M.Map Int String) Row
78+ g (RUnknown n) = do
79+ m <- get
80+ case M.lookup n m of
81+ Nothing -> do
82+ let name = "r" ++ show (M.size m)
83+ put $ M.insert n name m
84+ return $ RowVar name
85+ Just name -> return $ RowVar name
86+ g r = return r
87+
88+replaceVarsWithUnknowns :: [String] -> Type -> Check Type
89+replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)
90+ where
91+ f :: Type -> StateT (M.Map String Int) Check Type
92+ f (TypeVar var) | var `elem` idents = do
93+ m <- get
94+ n <- lift fresh
95+ case M.lookup var m of
96+ Nothing -> do
97+ put (M.insert var n m)
98+ return $ TUnknown n
99+ Just u -> return $ TUnknown u
100+ f t = return t
101+ g :: Row -> StateT (M.Map String Int) Check Row
102+ g (RowVar var) | var `elem` idents = do
103+ m <- get
104+ n <- lift fresh
105+ case M.lookup var m of
106+ Nothing -> do
107+ put (M.insert var n m)
108+ return $ RUnknown n
109+ Just u -> return $ RUnknown u
110+ g r = return r
111+
112+replaceType :: (Data d) => Int -> Type -> d -> d
113+replaceType n t = everywhere (mkT go)
114+ where
115+ go (TUnknown m) | m == n = t
116+ go t = t
117+
118+replaceRow :: (Data d) => Int -> Row -> d -> d
119+replaceRow n r = everywhere (mkT go)
120+ where
121+ go (RUnknown m) | m == n = r
122+ go r = r
123+
124+typeOccursCheck :: Int -> Type -> Check ()
125+typeOccursCheck u (TUnknown _) = return ()
126+typeOccursCheck u t = when (occursCheck u t) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ show t
127+
128+rowOccursCheck :: Int -> Row -> Check ()
129+rowOccursCheck u (RUnknown _) = return ()
130+rowOccursCheck u r = when (occursCheck u r) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ show r
131+
132+occursCheck :: (Data d) => Int -> d -> Bool
133+occursCheck u = everything (||) $ flip extQ g $ mkQ False f
134+ where
135+ f (TUnknown u') | u' == u = True
136+ f _ = False
137+ g (RUnknown u') | u' == u = True
138+ g _ = False
139+
140+typeConstraints :: M.Map Ident Int -> Value -> Check ([TypeConstraint], Int)
141+typeConstraints _ (NumericLiteral _) = do
142+ me <- fresh
143+ return ([TypeConstraint me Number], me)
144+typeConstraints _ (StringLiteral _) = do
145+ me <- fresh
146+ return ([TypeConstraint me String], me)
147+typeConstraints _ (BooleanLiteral _) = do
148+ me <- fresh
149+ return ([TypeConstraint me Boolean], me)
150+typeConstraints m (ArrayLiteral vals) = do
151+ all <- mapM (typeConstraints m) vals
152+ let (cs, ns) = (concat . map fst &&& map snd) all
153+ me <- fresh
154+ return (cs ++ map (TypeConstraint me . Array . TUnknown) ns, me)
155+typeConstraints m (Unary op val) = do
156+ (cs, n1) <- typeConstraints m val
157+ me <- fresh
158+ return (cs ++ unaryOperatorConstraints op n1 me, me)
159+typeConstraints m (Binary op left right) = do
160+ (cs1, n1) <- typeConstraints m left
161+ (cs2, n2) <- typeConstraints m right
162+ me <- fresh
163+ return (cs1 ++ cs2 ++ binaryOperatorConstraints op n1 n2 me, me)
164+typeConstraints m (ObjectLiteral ps) = do
165+ all <- mapM (typeConstraints m . snd) ps
166+ let (cs, ns) = (concat . map fst &&& map snd) all
167+ me <- fresh
168+ let tys = zipWith (\(name, _) u -> (name, TUnknown u)) ps ns
169+ return ((TypeConstraint me (Object (typesToRow tys))) : cs, me)
170+ where
171+ typesToRow [] = REmpty
172+ typesToRow ((name, ty):tys) = RCons name ty (typesToRow tys)
173+typeConstraints m (Indexer index val) = do
174+ (cs1, n1) <- typeConstraints m index
175+ (cs2, n2) <- typeConstraints m val
176+ me <- fresh
177+ return ((TypeConstraint n1 Number) : (TypeConstraint n2 (Array (TUnknown me))) : cs1 ++ cs2, me)
178+typeConstraints m (Accessor prop val) = do
179+ (cs, n1) <- typeConstraints m val
180+ me <- fresh
181+ rest <- fresh
182+ return ((TypeConstraint n1 (Object (RCons prop (TUnknown me) (RUnknown rest)))) : cs, me)
183+typeConstraints m (Abs args ret) = do
184+ ns <- replicateM (length args) fresh
185+ let m' = m `M.union` M.fromList (zipWith (,) args ns)
186+ (cs, n') <- typeConstraints m' ret
187+ me <- fresh
188+ return ((TypeConstraint me (Function (map TUnknown ns) (TUnknown n'))) : cs, me)
189+typeConstraints m (App f xs) = do
190+ (cs1, n1) <- typeConstraints m f
191+ all <- mapM (typeConstraints m) xs
192+ let (cs2, ns) = (concat . map fst &&& map snd) all
193+ me <- fresh
194+ return ((TypeConstraint n1 (Function (map TUnknown ns) (TUnknown me))) : cs1 ++ cs2, me)
195+typeConstraints m (Var var) =
196+ case M.lookup var m of
197+ Nothing -> do
198+ env <- getEnv
199+ case M.lookup var (names env) of
200+ Nothing -> throwError $ show var ++ " is undefined"
201+ Just (PolyType idents ty, _) -> do
202+ me <- fresh
203+ replaced <- replaceVarsWithUnknowns idents ty
204+ return ([TypeConstraint me replaced], me)
205+ Just u -> do
206+ me <- fresh
207+ return ([TypeConstraint u (TUnknown me)], me)
208+typeConstraints m (Block ss) = do
209+ ret <- fresh
210+ (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m M.empty ret ss
211+ guardWith "Block is missing a return statement" allCodePathsReturn
212+ return (cs, ret)
213+typeConstraints m (Constructor c) = do
214+ env <- getEnv
215+ case M.lookup c (dataConstructors env) of
216+ Nothing -> throwError $ "Constructor " ++ c ++ " is undefined"
217+ Just (PolyType idents ty) -> do
218+ me <- fresh
219+ replaced <- replaceVarsWithUnknowns idents ty
220+ return ([TypeConstraint me replaced], me)
221+typeConstraints m (Case val binders) = do
222+ (cs1, n1) <- typeConstraints m val
223+ ret <- fresh
224+ cs2 <- typeConstraintsForBinders m n1 ret binders
225+ return (cs1 ++ cs2, ret)
226+typeConstraints m (TypedValue val poly@(PolyType idents ty)) = do
227+ kind <- kindOf poly
228+ guardWith ("Expected type of kind *, was " ++ show kind) $ kind == Star
229+ desugared <- replaceAllTypeSynonyms ty
230+ (cs, n1) <- typeConstraints m val
231+ return (TypeConstraint n1 desugared : cs, n1)
232+
233+replaceAllTypeSynonyms :: Type -> Check Type
234+replaceAllTypeSynonyms ty = do
235+ env <- getEnv
236+ go (M.toList $ typeSynonyms env) ty
237+ where
238+ go [] ty = return ty
239+ go ((name, (args, repl)):rest) ty = do
240+ ty' <- either throwError return (substituteTypeSynonym name args repl ty)
241+ go rest ty'
242+
243+unaryOperatorConstraints :: UnaryOperator -> Int -> Int -> [TypeConstraint]
244+unaryOperatorConstraints Negate val result = [TypeConstraint val Number, TypeConstraint result Number]
245+unaryOperatorConstraints Not val result = [TypeConstraint val Boolean, TypeConstraint result Boolean]
246+unaryOperatorConstraints BitwiseNot val result = [TypeConstraint val Number, TypeConstraint result Number]
247+
248+binaryOperatorConstraints :: BinaryOperator -> Int -> Int -> Int -> [TypeConstraint]
249+binaryOperatorConstraints Add = symBinOpConstraints Number
250+binaryOperatorConstraints Subtract = symBinOpConstraints Number
251+binaryOperatorConstraints Multiply = symBinOpConstraints Number
252+binaryOperatorConstraints Divide = symBinOpConstraints Number
253+binaryOperatorConstraints Modulus = symBinOpConstraints Number
254+binaryOperatorConstraints LessThan = asymBinOpConstraints Number Boolean
255+binaryOperatorConstraints LessThanOrEqualTo = asymBinOpConstraints Number Boolean
256+binaryOperatorConstraints GreaterThan = asymBinOpConstraints Number Boolean
257+binaryOperatorConstraints GreaterThanOrEqualTo = asymBinOpConstraints Number Boolean
258+binaryOperatorConstraints BitwiseAnd = symBinOpConstraints Number
259+binaryOperatorConstraints BitwiseOr = symBinOpConstraints Number
260+binaryOperatorConstraints BitwiseXor = symBinOpConstraints Number
261+binaryOperatorConstraints ShiftLeft = symBinOpConstraints Number
262+binaryOperatorConstraints ShiftRight = symBinOpConstraints Number
263+binaryOperatorConstraints ZeroFillShiftRight = symBinOpConstraints Number
264+binaryOperatorConstraints EqualTo = equalityBinOpConstraints
265+binaryOperatorConstraints NotEqualTo = equalityBinOpConstraints
266+binaryOperatorConstraints And = symBinOpConstraints Boolean
267+binaryOperatorConstraints Or = symBinOpConstraints Boolean
268+binaryOperatorConstraints Concat = symBinOpConstraints String
269+
270+equalityBinOpConstraints :: Int -> Int -> Int -> [TypeConstraint]
271+equalityBinOpConstraints left right result = [TypeConstraint left (TUnknown right), TypeConstraint result Boolean]
272+
273+symBinOpConstraints :: Type -> Int -> Int -> Int -> [TypeConstraint]
274+symBinOpConstraints ty left right result = asymBinOpConstraints ty ty left right result
275+
276+asymBinOpConstraints :: Type -> Type -> Int -> Int -> Int -> [TypeConstraint]
277+asymBinOpConstraints ty res left right result = [TypeConstraint left ty, TypeConstraint right ty, TypeConstraint result res]
278+
279+typeConstraintsForBinder :: Int -> Binder -> Check ([TypeConstraint], M.Map Ident Int)
280+typeConstraintsForBinder val (StringBinder _) = constantBinder val String
281+typeConstraintsForBinder val (NumberBinder _) = constantBinder val Number
282+typeConstraintsForBinder val (BooleanBinder _) = constantBinder val Boolean
283+typeConstraintsForBinder val (VarBinder name) = do
284+ me <- fresh
285+ return ([TypeConstraint me (TUnknown val)], M.singleton name me)
286+typeConstraintsForBinder val (NullaryBinder ctor) = do
287+ env <- getEnv
288+ case M.lookup ctor (dataConstructors env) of
289+ Just (PolyType args ret) -> do
290+ ret' <- replaceVarsWithUnknowns args ret
291+ return ([TypeConstraint val ret'], M.empty)
292+ _ -> throwError $ "Constructor " ++ ctor ++ " is not defined"
293+typeConstraintsForBinder val (UnaryBinder ctor binder) = do
294+ env <- getEnv
295+ case M.lookup ctor (dataConstructors env) of
296+ Just (PolyType idents f@(Function [_] _)) -> do
297+ obj <- fresh
298+ (Function [ty] ret) <- replaceVarsWithUnknowns idents f
299+ (cs, m1) <- typeConstraintsForBinder obj binder
300+ return ((TypeConstraint val ret) : (TypeConstraint obj ty) : cs, m1)
301+ Just _ -> throwError $ ctor ++ " is not a unary constructor"
302+ _ -> throwError $ "Constructor " ++ ctor ++ " is not defined"
303+typeConstraintsForBinder val (ObjectBinder props) = do
304+ row <- fresh
305+ rest <- fresh
306+ (cs, m1) <- typeConstraintsForProperties row (RUnknown rest) props
307+ return ((TypeConstraint val (Object (RUnknown row))) : cs, m1)
308+ where
309+ typeConstraintsForProperties :: Int -> Row -> [(String, Binder)] -> Check ([TypeConstraint], M.Map Ident Int)
310+ typeConstraintsForProperties nrow row [] = return ([RowConstraint nrow row], M.empty)
311+ typeConstraintsForProperties nrow row ((name, binder):binders) = do
312+ propTy <- fresh
313+ (cs1, m1) <- typeConstraintsForBinder propTy binder
314+ (cs2, m2) <- typeConstraintsForProperties nrow (RCons name (TUnknown propTy) row) binders
315+ return (cs1 ++ cs2, M.union m1 m2)
316+typeConstraintsForBinder val (ArrayBinder binders rest) = do
317+ el <- fresh
318+ all <- mapM (typeConstraintsForBinder el) binders
319+ let (cs1, m1) = (concat . map fst &&& M.unions . map snd) all
320+ let arrayConstraint = TypeConstraint val (Array (TUnknown el))
321+ case rest of
322+ Nothing -> return (arrayConstraint : cs1, m1)
323+ Just binder -> do
324+ (cs2, m2) <- typeConstraintsForBinder val binder
325+ return (arrayConstraint : cs1 ++ cs2, M.union m1 m2)
326+
327+constantBinder :: Int -> Type -> Check ([TypeConstraint], M.Map Ident Int)
328+constantBinder val ty = return ([TypeConstraint val ty], M.empty)
329+
330+typeConstraintsForBinders :: M.Map Ident Int -> Int -> Int -> [(Binder, Value)] -> Check [TypeConstraint]
331+typeConstraintsForBinders _ _ _ [] = return []
332+typeConstraintsForBinders m nval ret ((binder, val):bs) = do
333+ (cs1, m1) <- typeConstraintsForBinder nval binder
334+ (cs2, n2) <- typeConstraints (M.union m m1) val
335+ cs3 <- typeConstraintsForBinders m nval ret bs
336+ return ((TypeConstraint n2 (TUnknown ret)) : cs1 ++ cs2 ++ cs3)
337+
338+typeConstraintsForStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> Statement -> Check ([TypeConstraint], Bool, M.Map Ident Int)
339+typeConstraintsForStatement m mass ret (VariableIntroduction name val) = do
340+ case M.lookup name (m `M.union` mass) of
341+ Nothing -> do
342+ (cs1, n1) <- typeConstraints m val
343+ return $ (cs1, False, M.insert name n1 mass)
344+ Just ty -> throwError $ "Variable with name " ++ show name ++ " already exists."
345+typeConstraintsForStatement m mass ret (Assignment tgt val) = do
346+ (cs1, n1) <- typeConstraints m val
347+ cs2 <- typeConstraintsForAssignmentTarget m mass n1 tgt
348+ return (cs1 ++ cs2, False, mass)
349+typeConstraintsForStatement m mass ret (While val inner) = do
350+ (cs1, n1) <- typeConstraints m val
351+ (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret inner
352+ return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2, allCodePathsReturn, mass)
353+typeConstraintsForStatement m mass ret (IfThenElse val thens Nothing) = do
354+ (cs1, n1) <- typeConstraints m val
355+ (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret thens
356+ return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2, allCodePathsReturn, mass)
357+typeConstraintsForStatement m mass ret (IfThenElse val thens (Just elses)) = do
358+ (cs1, n1) <- typeConstraints m val
359+ (cs2, allCodePathsReturn1, _) <- typeConstraintsForBlock m mass ret thens
360+ (cs3, allCodePathsReturn2, _) <- typeConstraintsForBlock m mass ret elses
361+ return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2 ++ cs3, allCodePathsReturn1 && allCodePathsReturn2, mass)
362+typeConstraintsForStatement m mass ret (For (init, cond, cont) inner) = do
363+ (cs1, b1, mass1) <- typeConstraintsForStatement m mass ret init
364+ guardWith "Cannot return from inside for" $ not b1
365+ (cs2, n1) <- typeConstraints (m `M.union` mass1) cond
366+ (cs3, b2, mass2) <- typeConstraintsForStatement (m `M.union` mass1) mass1 ret cont
367+ guardWith "Cannot return from inside for" $ not b2
368+ (cs4, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass2) mass2 ret inner
369+ return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2 ++ cs3 ++ cs4, allCodePathsReturn, mass)
370+typeConstraintsForStatement m mass ret (Return val) = do
371+ (cs1, n1) <- typeConstraints (m `M.union` mass) val
372+ return ((TypeConstraint n1 (TUnknown ret)) : cs1, True, mass)
373+
374+typeConstraintsForAssignmentTarget :: M.Map Ident Int -> M.Map Ident Int -> Int -> AssignmentTarget -> Check [TypeConstraint]
375+typeConstraintsForAssignmentTarget m mass nval (AssignVariable var) =
376+ case M.lookup var mass of
377+ Nothing -> throwError $ "No local variable with name " ++ show var
378+ Just ty -> do
379+ return [TypeConstraint nval (TUnknown ty)]
380+typeConstraintsForAssignmentTarget m mass nval (AssignArrayIndex index tgt) = do
381+ arr <- fresh
382+ (cs1, n1) <- typeConstraints (m `M.union` mass) index
383+ cs2 <- typeConstraintsForAssignmentTarget m mass arr tgt
384+ return $ (TypeConstraint arr (Array (TUnknown nval))) : (TypeConstraint n1 Number) : cs1 ++ cs2
385+typeConstraintsForAssignmentTarget m mass nval (AssignObjectProperty prop tgt) = do
386+ obj <- fresh
387+ row <- fresh
388+ cs <- typeConstraintsForAssignmentTarget m mass obj tgt
389+ return $ (TypeConstraint obj (Object (RCons prop (TUnknown nval) $ RUnknown row))) : cs
390+
391+typeConstraintsForBlock :: M.Map Ident Int -> M.Map Ident Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, M.Map Ident Int)
392+typeConstraintsForBlock _ mass _ [] = return ([], False, mass)
393+typeConstraintsForBlock m mass ret (s:ss) = do
394+ (cs1, b1, mass1) <- typeConstraintsForStatement (m `M.union` mass) mass ret s
395+ case (b1, ss) of
396+ (True, []) -> return (cs1, True, mass1)
397+ (True, _) -> throwError "Unreachable code"
398+ (False, ss) -> do
399+ (cs2, b2, mass2) <- typeConstraintsForBlock m mass1 ret ss
400+ return (cs1 ++ cs2, b2, mass2)
401+
402+solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
403+solveTypeConstraints [] s = return s
404+solveTypeConstraints all@(TypeConstraint n t:cs) s = do
405+ typeOccursCheck n t
406+ let s' = let (f, g) = runTypeSolution s
407+ in TypeSolution (replaceType n t . f, replaceType n t . g)
408+ cs' <- fmap concat $ mapM (substituteTypeInConstraint n t) cs
409+ solveTypeConstraints cs' s'
410+solveTypeConstraints (RowConstraint n r:cs) s = do
411+ rowOccursCheck n r
412+ let s' = let (f, g) = runTypeSolution s
413+ in TypeSolution $ (replaceRow n r . f, replaceRow n r . g)
414+ cs' <- fmap concat $ mapM (substituteRowInConstraint n r) cs
415+ solveTypeConstraints cs' s'
416+
417+substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
418+substituteTypeInConstraint n s (TypeConstraint m t)
419+ | n == m = unifyTypes s t
420+ | otherwise = return [TypeConstraint m (replaceType n s t)]
421+substituteTypeInConstraint n s (RowConstraint m r)
422+ = return [RowConstraint m (replaceType n s r)]
423+
424+substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
425+substituteRowInConstraint n r (TypeConstraint m t)
426+ = return [TypeConstraint m (replaceRow n r t)]
427+substituteRowInConstraint n r (RowConstraint m r1)
428+ | m == n = unifyRows r r1
429+ | otherwise = return [RowConstraint m (replaceRow n r r1)]
430+
431+unifyTypes :: Type -> Type -> Check [TypeConstraint]
432+unifyTypes (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
433+unifyTypes (TUnknown u) t = do
434+ typeOccursCheck u t
435+ return [TypeConstraint u t]
436+unifyTypes t (TUnknown u) = do
437+ typeOccursCheck u t
438+ return [TypeConstraint u t]
439+unifyTypes Number Number = return []
440+unifyTypes String String = return []
441+unifyTypes Boolean Boolean = return []
442+unifyTypes (Array s) (Array t) = unifyTypes s t
443+unifyTypes (Object row1) (Object row2) = unifyRows row1 row2
444+unifyTypes (Function args1 ret1) (Function args2 ret2) = do
445+ guardWith "Function applied to incorrect number of args" $ length args1 == length args2
446+ cs1 <- fmap concat $ zipWithM unifyTypes args1 args2
447+ cs2 <- unifyTypes ret1 ret2
448+ return $ cs1 ++ cs2
449+unifyTypes (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
450+unifyTypes (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = return []
451+unifyTypes (TypeVar v1) (TypeVar v2) = return []
452+unifyTypes (TypeApp t1 t2) (TypeApp t3 t4) = do
453+ cs1 <- unifyTypes t1 t3
454+ cs2 <- unifyTypes t2 t4
455+ return $ cs1 ++ cs2
456+unifyTypes t1 t2 = throwError $ "Cannot unify " ++ show t1 ++ " with " ++ show t2 ++ "."
457+
458+unifyRows :: Row -> Row -> Check [TypeConstraint]
459+unifyRows r1 r2 =
460+ let
461+ (s1, r1') = toList r1
462+ (s2, r2') = toList r2
463+ int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
464+ sd1 = [ (name, t1) | (name, t1) <- s1, not (elem name (map fst s2)) ]
465+ sd2 = [ (name, t2) | (name, t2) <- s2, not (elem name (map fst s1)) ]
466+ in rethrow (\e -> "Cannot unify " ++ show r1 ++ " with " ++ show r2 ++ ": " ++ e) $ do
467+ cs1 <- fmap concat $ mapM (uncurry unifyTypes) int
468+ cs2 <- unifyRows' sd1 r1' sd2 r2'
469+ return $ cs1 ++ cs2
470+ where
471+ unifyRows' :: [(String, Type)] -> Row -> [(String, Type)] -> Row -> Check [TypeConstraint]
472+ unifyRows' [] (RUnknown u) sd r = do
473+ rowOccursCheck u r
474+ return [RowConstraint u (fromList (sd, r))]
475+ unifyRows' sd r [] (RUnknown u) = do
476+ rowOccursCheck u r
477+ return [RowConstraint u (fromList (sd, r))]
478+ unifyRows' ((name, ty):row) r others (RUnknown u) = do
479+ u' <- fresh
480+ cs <- unifyRows' row r others (RUnknown u')
481+ return [ RowConstraint u (RCons name ty (RUnknown u')) ]
482+ unifyRows' [] REmpty [] REmpty = return []
483+ unifyRows' sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ show (fromList (sd1, r1)) ++ " with " ++ show (fromList (sd2, r2)) ++ "."
484+ toList :: Row -> ([(String, Type)], Row)
485+ toList (RCons name ty row) = let (tys, rest) = toList row
486+ in ((name, ty):tys, rest)
487+ toList r = ([], r)
488+ fromList :: ([(String, Type)], Row) -> Row
489+ fromList ([], r) = r
490+ fromList ((name, t):ts, r) = RCons name t (fromList (ts, r))