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