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