@@ -0,0 +1,412 @@
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 :: Value -> Check Type
47+typeOf val = do
48+ (cs, n, _) <- typeConstraints 0 M.empty val
49+ solution <- solveTypeConstraints cs emptyTypeSolution
50+ return $ varIfUnknown $ fst (runTypeSolution solution) n
51+
52+varIfUnknown :: Type -> Type
53+varIfUnknown = flip evalState M.empty . varIfUnknown'
54+ where
55+ varIfUnknown' :: Type -> State (M.Map Int String) Type
56+ varIfUnknown' (TUnknown n) = do
57+ m <- get
58+ case M.lookup n m of
59+ Nothing -> do
60+ let name = "t" ++ show (M.size m)
61+ put $ M.insert n name m
62+ return $ TypeVar name
63+ Just name -> return $ TypeVar name
64+ varIfUnknown' (Array t) = Array <$> varIfUnknown' t
65+ varIfUnknown' (Object row) = Object <$> varIfUnknown'' row
66+ varIfUnknown' (Function args ret) = Function <$> mapM varIfUnknown' args <*> varIfUnknown' ret
67+ varIfUnknown' (TypeApp t1 t2) = TypeApp <$> varIfUnknown' t1 <*> varIfUnknown' t2
68+ varIfUnknown' t = return t
69+ varIfUnknown'' :: Row -> State (M.Map Int String) Row
70+ varIfUnknown'' (RUnknown n) = do
71+ m <- get
72+ case M.lookup n m of
73+ Nothing -> do
74+ let name = "r" ++ show (M.size m)
75+ put $ M.insert n name m
76+ return $ RowVar name
77+ Just name -> return $ RowVar name
78+ varIfUnknown'' (RCons name ty row) = RCons name ty <$> varIfUnknown'' row
79+ varIfUnknown'' r = return r
80+
81+replaceVarsWithUnknowns :: Int -> Type -> (Type, Int)
82+replaceVarsWithUnknowns n = (id *** fst) . flip runState (n, M.empty) . replaceVarsWithUnknowns'
83+ where
84+ replaceVarsWithUnknowns' :: Type -> State (Int, M.Map String Int) Type
85+ replaceVarsWithUnknowns' (Array t) = Array <$> replaceVarsWithUnknowns' t
86+ replaceVarsWithUnknowns' (Object row) = Object <$> replaceVarsWithUnknowns'' row
87+ replaceVarsWithUnknowns' (Function args ret) = Function <$> mapM replaceVarsWithUnknowns' args <*> replaceVarsWithUnknowns' ret
88+ replaceVarsWithUnknowns' (TypeApp t1 t2) = TypeApp <$> replaceVarsWithUnknowns' t1 <*> replaceVarsWithUnknowns' t2
89+ replaceVarsWithUnknowns' (TypeVar var) = do
90+ (n, m) <- get
91+ case M.lookup var m of
92+ Nothing -> do
93+ put (n + 1, M.insert var n m)
94+ return $ TUnknown n
95+ Just u -> return $ TUnknown u
96+ replaceVarsWithUnknowns' t = return t
97+ replaceVarsWithUnknowns'' :: Row -> State (Int, M.Map String Int) Row
98+ replaceVarsWithUnknowns'' (RowVar var) = do
99+ (n, m) <- get
100+ case M.lookup var m of
101+ Nothing -> do
102+ put (n + 1, M.insert var n m)
103+ return $ RUnknown n
104+ Just u -> return $ RUnknown u
105+ replaceVarsWithUnknowns'' (RCons name ty row) = RCons name <$> replaceVarsWithUnknowns' ty <*> replaceVarsWithUnknowns'' row
106+ replaceVarsWithUnknowns'' r = return r
107+
108+typeConstraints :: Int -> M.Map String Int -> Value -> Check ([TypeConstraint], Int, Int)
109+typeConstraints n _ (NumericLiteral _) = return ([TypeConstraint n Number], n, n)
110+typeConstraints n _ (StringLiteral _) = return ([TypeConstraint n String], n, n)
111+typeConstraints n _ (BooleanLiteral _) = return ([TypeConstraint n Boolean], n, n)
112+typeConstraints n m (ArrayLiteral vals) = do
113+ (cs, ns, max1) <- typeConstraintsAll n m vals
114+ let me = max1 + 1
115+ return (cs ++ map (TypeConstraint me . Array . TUnknown) ns, me, me)
116+typeConstraints n m (Unary op val) = do
117+ (cs, n1, max1) <- typeConstraints n m val
118+ let me = max1 + 1
119+ return (cs ++ unaryOperatorConstraints op n1 me, me, me)
120+typeConstraints n m (Binary op left right) = do
121+ (cs1, n1, max1) <- typeConstraints n m left
122+ (cs2, n2, max2) <- typeConstraints (max1 + 1) m right
123+ let me = max1 + 1
124+ return (cs1 ++ cs2 ++ binaryOperatorConstraints op n1 n2 me, me, me)
125+typeConstraints n m (ObjectLiteral ps) = do
126+ (cs, ns, max1) <- typeConstraintsAll n m (map snd ps)
127+ let me = max1 + 1
128+ let tys = zipWith (\(name, _) u -> (name, TUnknown u)) ps ns
129+ return ((TypeConstraint me (Object (typesToRow tys))) : cs, me, me)
130+ where
131+ typesToRow [] = REmpty
132+ typesToRow ((name, ty):tys) = RCons name ty (typesToRow tys)
133+typeConstraints n m (Accessor prop val) = do
134+ (cs, n1, max1) <- typeConstraints n m val
135+ let me = max1 + 1
136+ let rest = max1 + 2
137+ return ((TypeConstraint n1 (Object (RCons prop (TUnknown me) (RUnknown rest)))) : cs, me, rest)
138+typeConstraints n m (Abs args ret) = do
139+ let ns = [n..n + length args - 1]
140+ let next = n + length args
141+ let m' = m `M.union` M.fromList (zipWith (,) args ns)
142+ (cs, n', max1) <- typeConstraints next m' ret
143+ let me = max1 + 1
144+ return ((TypeConstraint me (Function (map TUnknown ns) (TUnknown n'))) : cs, me, me)
145+typeConstraints n m (App f xs) = do
146+ (cs1, n1, max1) <- typeConstraints n m f
147+ (cs2, ns, max2) <- typeConstraintsAll (max1 + 1) m xs
148+ let me = max2 + 1
149+ return ((TypeConstraint n1 (Function (map TUnknown ns) (TUnknown me))) : cs1 ++ cs2, me, me)
150+typeConstraints n m (Var var) =
151+ case M.lookup var m of
152+ Nothing -> do
153+ env <- get
154+ case M.lookup var (names env) of
155+ Nothing -> throwError $ var ++ " is undefined"
156+ Just ty -> let (replaced, max1) = replaceVarsWithUnknowns (n + 1) ty
157+ in return ([TypeConstraint n replaced], n, max1)
158+ Just u -> return ([TypeConstraint u (TUnknown n)], n, n)
159+typeConstraints n m (Block ss) = do
160+ let ret = n + 1
161+ (cs, allCodePathsReturn, max1, _) <- typeConstraintsForBlock (ret + 1) m M.empty ret ss
162+ guardWith "Block is missing a return statement" allCodePathsReturn
163+ return (cs, ret, max1)
164+typeConstraints n m (Constructor c) = do
165+ env <- get
166+ case M.lookup c (names env) of
167+ Nothing -> throwError $ c ++ " is undefined"
168+ Just ty -> let (replaced, max1) = replaceVarsWithUnknowns (n + 1) ty
169+ in return ([TypeConstraint n replaced], n, max1)
170+typeConstraints n m (Case val binders) = do
171+ (cs1, n1, max1) <- typeConstraints n m val
172+ let ret = max1 + 1
173+ (cs2, max2) <- typeConstraintsForBinders (ret + 1) m n1 ret binders
174+ return (cs1 ++ cs2, ret, max2)
175+typeConstraints n m (TypedValue val ty) = do
176+ (cs, n1, max1) <- typeConstraints n m val
177+ return ([TypeConstraint n1 ty], n1, max1)
178+ -- TODO: Kind-check the type
179+
180+unaryOperatorConstraints :: UnaryOperator -> Int -> Int -> [TypeConstraint]
181+unaryOperatorConstraints Negate val result = [TypeConstraint val Number, TypeConstraint result Number]
182+unaryOperatorConstraints Not val result = [TypeConstraint val Boolean, TypeConstraint result Boolean]
183+unaryOperatorConstraints BitwiseNot val result = [TypeConstraint val Number, TypeConstraint result Number]
184+
185+binaryOperatorConstraints :: BinaryOperator -> Int -> Int -> Int -> [TypeConstraint]
186+binaryOperatorConstraints Add = symBinOpConstraints Number
187+binaryOperatorConstraints Subtract = symBinOpConstraints Number
188+binaryOperatorConstraints Multiply = symBinOpConstraints Number
189+binaryOperatorConstraints Divide = symBinOpConstraints Number
190+binaryOperatorConstraints Modulus = symBinOpConstraints Number
191+binaryOperatorConstraints LessThan = symBinOpConstraints Number
192+binaryOperatorConstraints LessThanOrEqualTo = symBinOpConstraints Number
193+binaryOperatorConstraints GreaterThan = symBinOpConstraints Number
194+binaryOperatorConstraints GreaterThanOrEqualTo = symBinOpConstraints Number
195+binaryOperatorConstraints BitwiseAnd = symBinOpConstraints Number
196+binaryOperatorConstraints BitwiseOr = symBinOpConstraints Number
197+binaryOperatorConstraints BitwiseXor = symBinOpConstraints Number
198+binaryOperatorConstraints ShiftLeft = symBinOpConstraints Number
199+binaryOperatorConstraints ShiftRight = symBinOpConstraints Number
200+binaryOperatorConstraints ZeroFillShiftRight = symBinOpConstraints Number
201+binaryOperatorConstraints EqualTo = equalityBinOpConstraints
202+binaryOperatorConstraints NotEqualTo = equalityBinOpConstraints
203+binaryOperatorConstraints And = symBinOpConstraints Boolean
204+binaryOperatorConstraints Or = symBinOpConstraints Boolean
205+binaryOperatorConstraints Concat = symBinOpConstraints String
206+
207+equalityBinOpConstraints :: Int -> Int -> Int -> [TypeConstraint]
208+equalityBinOpConstraints left right result = [TypeConstraint left (TUnknown right), TypeConstraint result Boolean]
209+
210+symBinOpConstraints :: Type -> Int -> Int -> Int -> [TypeConstraint]
211+symBinOpConstraints ty left right result = [TypeConstraint left ty, TypeConstraint right ty, TypeConstraint result ty]
212+
213+typeConstraintsForBinder :: Int -> M.Map String Int -> Int -> Binder -> Check ([TypeConstraint], Int, M.Map String Int)
214+typeConstraintsForBinder n m val (VarBinder name) =
215+ return ([TypeConstraint n (TUnknown val)], n, M.insert name n m)
216+typeConstraintsForBinder n m val (ConstructorBinder ctor binder) = do
217+ env <- get
218+ case M.lookup ctor (names env) of
219+ Just f@(Function [ty] ret) -> do
220+ let obj = n
221+ let (Function [ty'] ret', max1) = replaceVarsWithUnknowns n f
222+ (cs, max2, m1) <- typeConstraintsForBinder (max1 + 1) m obj binder
223+ return ((TypeConstraint val ret') : (TypeConstraint obj ty') : cs, max2, m1)
224+ Just _ -> throwError $ ctor ++ " is not a constructor"
225+ _ -> throwError $ "Constructor " ++ ctor ++ " is not defined"
226+typeConstraintsForBinder n m val (ObjectBinder props) = do undefined
227+
228+typeConstraintsForBinders :: Int -> M.Map String Int -> Int -> Int -> [(Binder, Value)] -> Check ([TypeConstraint], Int)
229+typeConstraintsForBinders n _ _ _ [] = return ([], n)
230+typeConstraintsForBinders n m nval ret ((binder, val):bs) = do
231+ (cs1, max1, m1) <- typeConstraintsForBinder n m nval binder
232+ (cs2, n2, max2) <- typeConstraints (max1 + 1) m1 val
233+ (cs3, max2) <- typeConstraintsForBinders (max2 + 1) m nval ret bs
234+ return ((TypeConstraint n2 (TUnknown ret)) : cs1 ++ cs2 ++ cs3, max2)
235+
236+typeConstraintsForStatement :: Int -> M.Map String Int -> M.Map String Int -> Int -> Statement -> Check ([TypeConstraint], Bool, Int, M.Map String Int)
237+typeConstraintsForStatement n m mass ret (VariableIntroduction name val) = do
238+ case M.lookup name (m `M.union` mass) of
239+ Nothing -> do
240+ (cs1, n1, max1) <- typeConstraints n m val
241+ return $ (cs1, False, max1, M.insert name n1 mass)
242+ Just ty -> throwError $ "Variable with name " ++ name ++ " already exists."
243+typeConstraintsForStatement n m mass ret (Assignment name val) = do
244+ case M.lookup name (m `M.union` mass) of
245+ Nothing -> throwError $ "No local variable with name " ++ name
246+ Just ty -> do
247+ (cs1, n1, max1) <- typeConstraints n m val
248+ return ((TypeConstraint n1 (TUnknown ty)) : cs1, False, max1, mass)
249+typeConstraintsForStatement n m mass ret (While val inner) = do
250+ (cs1, n1, max1) <- typeConstraints n m val
251+ (cs2, allCodePathsReturn, max2, _) <- typeConstraintsForBlock (max1 + 1) m mass ret inner
252+ return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2, allCodePathsReturn, max2, mass)
253+typeConstraintsForStatement n m mass ret (IfThenElse val thens Nothing) = do
254+ (cs1, n1, max1) <- typeConstraints n m val
255+ (cs2, allCodePathsReturn, max2, _) <- typeConstraintsForBlock (max1 + 1) m mass ret thens
256+ return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2, allCodePathsReturn, max2, mass)
257+typeConstraintsForStatement n m mass ret (IfThenElse val thens (Just elses)) = do
258+ (cs1, n1, max1) <- typeConstraints n m val
259+ (cs2, allCodePathsReturn1, max2, _) <- typeConstraintsForBlock (max1 + 1) m mass ret thens
260+ (cs3, allCodePathsReturn2, max3, _) <- typeConstraintsForBlock (max2 + 1) m mass ret elses
261+ return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2 ++ cs3, allCodePathsReturn1 && allCodePathsReturn2, max3, mass)
262+typeConstraintsForStatement n m mass ret (For (init, cond, cont) inner) = do
263+ (cs1, b1, max1, mass1) <- typeConstraintsForStatement n m mass ret init
264+ guardWith "Cannot return from inside for" $ not b1
265+ (cs2, n1, max2) <- typeConstraints (max1 + 1) (m `M.union` mass1) cond
266+ (cs3, b2, max3, mass2) <- typeConstraintsForStatement (max2 + 1) (m `M.union` mass1) mass1 ret cont
267+ guardWith "Cannot return from inside for" $ not b2
268+ (cs4, allCodePathsReturn, max4, _) <- typeConstraintsForBlock (max3 + 1) (m `M.union` mass2) mass2 ret inner
269+ return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2 ++ cs3 ++ cs4, allCodePathsReturn, max4, mass)
270+typeConstraintsForStatement n m mass ret (Return val) = do
271+ (cs1, n1, max1) <- typeConstraints n m val
272+ return ((TypeConstraint n1 (TUnknown ret)) : cs1, True, max1, mass)
273+
274+typeConstraintsForBlock :: Int -> M.Map String Int -> M.Map String Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, Int, M.Map String Int)
275+typeConstraintsForBlock n _ mass _ [] = return ([], False, n, mass)
276+typeConstraintsForBlock n m mass ret (s:ss) = do
277+ (cs1, b1, max1, mass1) <- typeConstraintsForStatement n (m `M.union` mass) mass ret s
278+ case (b1, ss) of
279+ (True, []) -> return (cs1, True, max1, mass1)
280+ (True, _) -> throwError "Unreachable code"
281+ (False, ss) -> do
282+ (cs2, b2, max2, mass2) <- typeConstraintsForBlock (max1 + 1) m mass1 ret ss
283+ return (cs1 ++ cs2, b2, max2, mass2)
284+
285+typeConstraintsAll :: Int -> M.Map String Int -> [Value] -> Check ([TypeConstraint], [Int], Int)
286+typeConstraintsAll n _ [] = return ([], [], n)
287+typeConstraintsAll n m (t:ts) = do
288+ (cs, n', max1) <- typeConstraints n m t
289+ (cs', ns, max2) <- typeConstraintsAll (max1 + 1) m ts
290+ return (cs ++ cs', n':ns, max2)
291+
292+solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
293+solveTypeConstraints [] s = return s
294+solveTypeConstraints (TypeConstraint n t:cs) s = do
295+ guardWith "Occurs check failed" $ not $ typeOccursCheck n t
296+ let s' = let (f, g) = runTypeSolution s
297+ in TypeSolution (replaceTypeInType n t . f, replaceTypeInRow n t . g)
298+ cs' <- fmap concat $ mapM (substituteTypeInConstraint n t) cs
299+ solveTypeConstraints cs' s'
300+solveTypeConstraints (RowConstraint n r:cs) s = do
301+ guardWith "Occurs check failed" $ not $ rowOccursCheck n r
302+ let s' = let (f, g) = runTypeSolution s
303+ in TypeSolution $ (replaceRowInType n r . f, replaceRowInRow n r . g)
304+ cs' <- fmap concat $ mapM (substituteRowInConstraint n r) cs
305+ solveTypeConstraints cs' s'
306+
307+substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
308+substituteTypeInConstraint n s (TypeConstraint m t)
309+ | n == m = unifyTypes s t
310+ | otherwise = return [TypeConstraint m (replaceTypeInType n s t)]
311+substituteTypeInConstraint n s (RowConstraint m r)
312+ = return [RowConstraint m (replaceTypeInRow n s r)]
313+
314+substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
315+substituteRowInConstraint n r (TypeConstraint m t)
316+ = return [TypeConstraint m (replaceRowInType n r t)]
317+substituteRowInConstraint n r (RowConstraint m r1)
318+ | m == n = unifyRows r r1
319+ | otherwise = return [RowConstraint m (replaceRowInRow n r r1)]
320+
321+replaceTypeInType :: Int -> Type -> Type -> Type
322+replaceTypeInType n t (TUnknown m) | m == n = t
323+replaceTypeInType n t (Array t1) = Array $ replaceTypeInType n t t1
324+replaceTypeInType n t (Object row) = Object $ replaceTypeInRow n t row
325+replaceTypeInType n t (Function args ret) = Function (map (replaceTypeInType n t) args) (replaceTypeInType n t ret)
326+replaceTypeInType n t (TypeApp t1 t2) = TypeApp (replaceTypeInType n t t1) (replaceTypeInType n t t2)
327+replaceTypeInType _ _ other = other
328+
329+replaceTypeInRow :: Int -> Type -> Row -> Row
330+replaceTypeInRow n t (RCons name ty row) = RCons name (replaceTypeInType n t ty) (replaceTypeInRow n t row)
331+replaceTypeInRow n t other = other
332+
333+replaceRowInType :: Int -> Row -> Type -> Type
334+replaceRowInType n r (Array t1) = Array $ replaceRowInType n r t1
335+replaceRowInType n r (Object row) = Object $ replaceRowInRow n r row
336+replaceRowInType n r (Function args ret) = Function (map (replaceRowInType n r) args) (replaceRowInType n r ret)
337+replaceRowInType n r (TypeApp t1 t2) = TypeApp (replaceRowInType n r t1) (replaceRowInType n r t2)
338+replaceRowInType _ _ other = other
339+
340+replaceRowInRow :: Int -> Row -> Row -> Row
341+replaceRowInRow n r (RUnknown m) | m == n = r
342+replaceRowInRow n r (RCons name ty row) = RCons name (replaceRowInType n r ty) (replaceRowInRow n r row)
343+replaceRowInRow _ _ other = other
344+
345+unifyTypes :: Type -> Type -> Check [TypeConstraint]
346+unifyTypes (TUnknown u) t = do
347+ guardWith "Occurs check failed" $ not $ typeOccursCheck u t
348+ return [TypeConstraint u t]
349+unifyTypes t (TUnknown u) = do
350+ guardWith "Occurs check failed" $ not $ typeOccursCheck u t
351+ return [TypeConstraint u t]
352+unifyTypes Number Number = return []
353+unifyTypes String String = return []
354+unifyTypes Boolean Boolean = return []
355+unifyTypes (Array s) (Array t) = unifyTypes s t
356+unifyTypes (Object row1) (Object row2) = unifyRows row1 row2
357+unifyTypes (Function args1 ret1) (Function args2 ret2) = do
358+ cs1 <- fmap concat $ zipWithM unifyTypes args1 args2
359+ cs2 <- unifyTypes ret1 ret2
360+ return $ cs1 ++ cs2
361+unifyTypes (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
362+unifyTypes (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = return []
363+unifyTypes (TypeVar v1) (TypeVar v2) = return []
364+unifyTypes (TypeApp t1 t2) (TypeApp t3 t4) = do
365+ cs1 <- unifyTypes t1 t3
366+ cs2 <- unifyTypes t2 t4
367+ return $ cs1 ++ cs2
368+unifyTypes t1 t2 = throwError $ "Cannot unify " ++ show t1 ++ " with " ++ show t2 ++ "."
369+
370+unifyRows :: Row -> Row -> Check [TypeConstraint]
371+unifyRows r1 r2 =
372+ let
373+ (s1, r1') = toList r1
374+ (s2, r2') = toList r2
375+ int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
376+ sd1 = [ (name, t1) | (name, t1) <- s1, not (elem name (map fst s2)) ]
377+ sd2 = [ (name, t2) | (name, t2) <- s2, not (elem name (map fst s1)) ]
378+ in rethrow (const $ "Cannot unify " ++ show r1 ++ " with " ++ show r2) $ do
379+ cs1 <- fmap concat $ mapM (uncurry unifyTypes) int
380+ cs2 <- unifyRows' (fromList (sd1, r1')) (fromList (sd2, r2'))
381+ return $ cs1 ++ cs2
382+ where
383+ unifyRows' :: Row -> Row -> Check [TypeConstraint]
384+ unifyRows' r (RUnknown u) = do
385+ guardWith "Occurs check failed" $ not $ rowOccursCheck u r
386+ return [RowConstraint u r]
387+ unifyRows' (RUnknown u) r = do
388+ guardWith "Occurs check failed" $ not $ rowOccursCheck u r
389+ return [RowConstraint u r]
390+ unifyRows' (RowVar v1) (RowVar v2) | v1 == v2 = return []
391+ unifyRows' REmpty REmpty = return []
392+ unifyRows' r1 r2 = throwError $ "Cannot unify " ++ show r1 ++ " with " ++ show r2 ++ "."
393+ toList :: Row -> ([(String, Type)], Row)
394+ toList (RCons name ty row) = let (tys, rest) = toList row
395+ in ((name, ty):tys, rest)
396+ toList r = ([], r)
397+ fromList :: ([(String, Type)], Row) -> Row
398+ fromList ([], r) = r
399+ fromList ((name, t):ts, r) = RCons name t (fromList (ts, r))
400+
401+typeOccursCheck :: Int -> Type -> Bool
402+typeOccursCheck u (TUnknown u') | u == u' = True
403+typeOccursCheck u (Array t) = typeOccursCheck u t
404+typeOccursCheck u (Object row) = rowOccursCheck u row
405+typeOccursCheck u (Function args ret) = any (typeOccursCheck u) args || typeOccursCheck u ret
406+typeOccursCheck u (TypeApp s t) = typeOccursCheck u s || typeOccursCheck u t
407+typeOccursCheck _ _ = False
408+
409+rowOccursCheck :: Int -> Row -> Bool
410+rowOccursCheck u (RUnknown u') | u == u' = True
411+rowOccursCheck u (RCons name ty row) = typeOccursCheck u ty || rowOccursCheck u row
412+rowOccursCheck _ _ = False