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