git.iko.soy/rowtype-yoga/purescript-native
on ae6037f help sign in
rowtype-yoga/purescript-native/src/PureScript/TypeChecker/Types.hs
465 lines 22 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 Data.List
22import Data.Function
24import PureScript.Values
25import PureScript.Types
26import PureScript.TypeChecker.Monad
28import Control.Monad.State
29import Control.Monad.Error
31import Control.Applicative
32import Control.Arrow (Kleisli(..), (***), (&&&))
33import qualified Control.Category as C
35import qualified Data.Map as M
37data TypeConstraint
38 = TypeConstraint Int Type
39 | RowConstraint Int Row deriving Show
41newtype TypeSolution = TypeSolution { runTypeSolution :: (Int -> Type, Int -> Row) }
43emptyTypeSolution :: TypeSolution
44emptyTypeSolution = TypeSolution (TUnknown, RUnknown)
46typeOf :: String -> Value -> Check Type
47typeOf 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
53varIfUnknown :: Type -> Type
54varIfUnknown = 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
82replaceVarsWithUnknowns :: Type -> Check Type
83replaceVarsWithUnknowns = 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
111typeConstraints :: M.Map String Int -> Value -> Check ([TypeConstraint], Int)
112typeConstraints _ (NumericLiteral _) = do
113 me <- fresh
114 return ([TypeConstraint me Number], me)
115typeConstraints _ (StringLiteral _) = do
116 me <- fresh
117 return ([TypeConstraint me String], me)
118typeConstraints _ (BooleanLiteral _) = do
119 me <- fresh
120 return ([TypeConstraint me Boolean], me)
121typeConstraints 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)
126typeConstraints m (Unary op val) = do
127 (cs, n1) <- typeConstraints m val
128 me <- fresh
129 return (cs ++ unaryOperatorConstraints op n1 me, me)
130typeConstraints 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)
135typeConstraints 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)
144typeConstraints 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)
149typeConstraints 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)
154typeConstraints 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)
160typeConstraints 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)
166typeConstraints 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)
179typeConstraints 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)
184typeConstraints 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)
192typeConstraints 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)
197typeConstraints m (TypedValue val ty) = do
198 (cs, n1) <- typeConstraints m val
199 return ([TypeConstraint n1 ty], n1)
200 -- TODO: Kind-check the type
202unaryOperatorConstraints :: UnaryOperator -> Int -> Int -> [TypeConstraint]
203unaryOperatorConstraints Negate val result = [TypeConstraint val Number, TypeConstraint result Number]
204unaryOperatorConstraints Not val result = [TypeConstraint val Boolean, TypeConstraint result Boolean]
205unaryOperatorConstraints BitwiseNot val result = [TypeConstraint val Number, TypeConstraint result Number]
207binaryOperatorConstraints :: BinaryOperator -> Int -> Int -> Int -> [TypeConstraint]
208binaryOperatorConstraints Add = symBinOpConstraints Number
209binaryOperatorConstraints Subtract = symBinOpConstraints Number
210binaryOperatorConstraints Multiply = symBinOpConstraints Number
211binaryOperatorConstraints Divide = symBinOpConstraints Number
212binaryOperatorConstraints Modulus = symBinOpConstraints Number
213binaryOperatorConstraints LessThan = symBinOpConstraints Number
214binaryOperatorConstraints LessThanOrEqualTo = symBinOpConstraints Number
215binaryOperatorConstraints GreaterThan = symBinOpConstraints Number
216binaryOperatorConstraints GreaterThanOrEqualTo = symBinOpConstraints Number
217binaryOperatorConstraints BitwiseAnd = symBinOpConstraints Number
218binaryOperatorConstraints BitwiseOr = symBinOpConstraints Number
219binaryOperatorConstraints BitwiseXor = symBinOpConstraints Number
220binaryOperatorConstraints ShiftLeft = symBinOpConstraints Number
221binaryOperatorConstraints ShiftRight = symBinOpConstraints Number
222binaryOperatorConstraints ZeroFillShiftRight = symBinOpConstraints Number
223binaryOperatorConstraints EqualTo = equalityBinOpConstraints
224binaryOperatorConstraints NotEqualTo = equalityBinOpConstraints
225binaryOperatorConstraints And = symBinOpConstraints Boolean
226binaryOperatorConstraints Or = symBinOpConstraints Boolean
227binaryOperatorConstraints Concat = symBinOpConstraints String
229equalityBinOpConstraints :: Int -> Int -> Int -> [TypeConstraint]
230equalityBinOpConstraints left right result = [TypeConstraint left (TUnknown right), TypeConstraint result Boolean]
232symBinOpConstraints :: Type -> Int -> Int -> Int -> [TypeConstraint]
233symBinOpConstraints ty left right result = [TypeConstraint left ty, TypeConstraint right ty, TypeConstraint result ty]
235typeConstraintsForBinder :: Int -> Binder -> Check ([TypeConstraint], M.Map String Int)
236typeConstraintsForBinder val (StringBinder _) = constantBinder val String
237typeConstraintsForBinder val (NumberBinder _) = constantBinder val Number
238typeConstraintsForBinder val (BooleanBinder _) = constantBinder val Boolean
239typeConstraintsForBinder val (VarBinder name) = do
240 me <- fresh
241 return ([TypeConstraint me (TUnknown val)], M.singleton name me)
242typeConstraintsForBinder val (NullaryBinder ctor) = do
243 env <- getEnv
244 case M.lookup ctor (names env) of
245 Just ret -> do
246 ret' <- replaceVarsWithUnknowns ret
247 return ([TypeConstraint val ret'], M.empty)
248 _ -> throwError $ "Constructor " ++ ctor ++ " is not defined"
249typeConstraintsForBinder val (UnaryBinder ctor binder) = do
250 env <- getEnv
251 case M.lookup ctor (names env) of
252 Just f@(Function [ty] ret) -> do
253 obj <- fresh
254 Function [ty'] ret' <- replaceVarsWithUnknowns f
255 (cs, m1) <- typeConstraintsForBinder obj binder
256 return ((TypeConstraint val ret') : (TypeConstraint obj ty') : cs, m1)
257 Just _ -> throwError $ ctor ++ " is not a unary constructor"
258 _ -> throwError $ "Constructor " ++ ctor ++ " is not defined"
259typeConstraintsForBinder val (ObjectBinder props) = do
260 row <- fresh
261 rest <- fresh
262 (cs, m1) <- typeConstraintsForProperties row (RUnknown rest) props
263 return ((TypeConstraint val (Object (RUnknown row))) : cs, m1)
264 where
265 typeConstraintsForProperties :: Int -> Row -> [(String, Binder)] -> Check ([TypeConstraint], M.Map String Int)
266 typeConstraintsForProperties nrow row [] = return ([RowConstraint nrow row], M.empty)
267 typeConstraintsForProperties nrow row ((name, binder):binders) = do
268 propTy <- fresh
269 (cs1, m1) <- typeConstraintsForBinder propTy binder
270 (cs2, m2) <- typeConstraintsForProperties nrow (RCons name (TUnknown propTy) row) binders
271 return (cs1 ++ cs2, M.union m1 m2)
272typeConstraintsForBinder val (ArrayBinder binders rest) = do
273 el <- fresh
274 all <- mapM (typeConstraintsForBinder el) binders
275 let (cs1, m1) = (concat . map fst &&& M.unions . map snd) all
276 let arrayConstraint = TypeConstraint val (Array (TUnknown el))
277 case rest of
278 Nothing -> return (arrayConstraint : cs1, m1)
279 Just binder -> do
280 (cs2, m2) <- typeConstraintsForBinder val binder
281 return (arrayConstraint : cs1 ++ cs2, M.union m1 m2)
283constantBinder :: Int -> Type -> Check ([TypeConstraint], M.Map String Int)
284constantBinder val ty = return ([TypeConstraint val ty], M.empty)
286typeConstraintsForBinders :: M.Map String Int -> Int -> Int -> [(Binder, Value)] -> Check [TypeConstraint]
287typeConstraintsForBinders _ _ _ [] = return []
288typeConstraintsForBinders m nval ret ((binder, val):bs) = do
289 (cs1, m1) <- typeConstraintsForBinder nval binder
290 (cs2, n2) <- typeConstraints (M.union m m1) val
291 cs3 <- typeConstraintsForBinders m nval ret bs
292 return ((TypeConstraint n2 (TUnknown ret)) : cs1 ++ cs2 ++ cs3)
294typeConstraintsForStatement :: M.Map String Int -> M.Map String Int -> Int -> Statement -> Check ([TypeConstraint], Bool, M.Map String Int)
295typeConstraintsForStatement m mass ret (VariableIntroduction name val) = do
296 case M.lookup name (m `M.union` mass) of
297 Nothing -> do
298 (cs1, n1) <- typeConstraints m val
299 return $ (cs1, False, M.insert name n1 mass)
300 Just ty -> throwError $ "Variable with name " ++ name ++ " already exists."
301typeConstraintsForStatement m mass ret (Assignment name val) = do
302 case M.lookup name (m `M.union` mass) of
303 Nothing -> throwError $ "No local variable with name " ++ name
304 Just ty -> do
305 (cs1, n1) <- typeConstraints m val
306 return ((TypeConstraint n1 (TUnknown ty)) : cs1, False, mass)
307typeConstraintsForStatement m mass ret (While val inner) = do
308 (cs1, n1) <- typeConstraints m val
309 (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret inner
310 return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2, allCodePathsReturn, mass)
311typeConstraintsForStatement m mass ret (IfThenElse val thens Nothing) = do
312 (cs1, n1) <- typeConstraints m val
313 (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret thens
314 return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2, allCodePathsReturn, mass)
315typeConstraintsForStatement m mass ret (IfThenElse val thens (Just elses)) = do
316 (cs1, n1) <- typeConstraints m val
317 (cs2, allCodePathsReturn1, _) <- typeConstraintsForBlock m mass ret thens
318 (cs3, allCodePathsReturn2, _) <- typeConstraintsForBlock m mass ret elses
319 return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2 ++ cs3, allCodePathsReturn1 && allCodePathsReturn2, mass)
320typeConstraintsForStatement m mass ret (For (init, cond, cont) inner) = do
321 (cs1, b1, mass1) <- typeConstraintsForStatement m mass ret init
322 guardWith "Cannot return from inside for" $ not b1
323 (cs2, n1) <- typeConstraints (m `M.union` mass1) cond
324 (cs3, b2, mass2) <- typeConstraintsForStatement (m `M.union` mass1) mass1 ret cont
325 guardWith "Cannot return from inside for" $ not b2
326 (cs4, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass2) mass2 ret inner
327 return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2 ++ cs3 ++ cs4, allCodePathsReturn, mass)
328typeConstraintsForStatement m mass ret (Return val) = do
329 (cs1, n1) <- typeConstraints m val
330 return ((TypeConstraint n1 (TUnknown ret)) : cs1, True, mass)
332typeConstraintsForBlock :: M.Map String Int -> M.Map String Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, M.Map String Int)
333typeConstraintsForBlock _ mass _ [] = return ([], False, mass)
334typeConstraintsForBlock m mass ret (s:ss) = do
335 (cs1, b1, mass1) <- typeConstraintsForStatement (m `M.union` mass) mass ret s
336 case (b1, ss) of
337 (True, []) -> return (cs1, True, mass1)
338 (True, _) -> throwError "Unreachable code"
339 (False, ss) -> do
340 (cs2, b2, mass2) <- typeConstraintsForBlock m mass1 ret ss
341 return (cs1 ++ cs2, b2, mass2)
343solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
344solveTypeConstraints [] s = return s
345solveTypeConstraints all@(TypeConstraint n t:cs) s = do
346 guardWith "Occurs check failed" $ not $ typeOccursCheck False n t
347 let s' = let (f, g) = runTypeSolution s
348 in TypeSolution (replaceTypeInType n t . f, replaceTypeInRow n t . g)
349 cs' <- fmap concat $ mapM (substituteTypeInConstraint n t) cs
350 solveTypeConstraints cs' s'
351solveTypeConstraints (RowConstraint n r:cs) s = do
352 guardWith "Occurs check failed" $ not $ rowOccursCheck False n r
353 let s' = let (f, g) = runTypeSolution s
354 in TypeSolution $ (replaceRowInType n r . f, replaceRowInRow n r . g)
355 cs' <- fmap concat $ mapM (substituteRowInConstraint n r) cs
356 solveTypeConstraints cs' s'
358substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
359substituteTypeInConstraint n s (TypeConstraint m t)
360 | n == m = unifyTypes s t
361 | otherwise = return [TypeConstraint m (replaceTypeInType n s t)]
362substituteTypeInConstraint n s (RowConstraint m r)
363 = return [RowConstraint m (replaceTypeInRow n s r)]
365substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
366substituteRowInConstraint n r (TypeConstraint m t)
367 = return [TypeConstraint m (replaceRowInType n r t)]
368substituteRowInConstraint n r (RowConstraint m r1)
369 | m == n = unifyRows r r1
370 | otherwise = return [RowConstraint m (replaceRowInRow n r r1)]
372replaceTypeInType :: Int -> Type -> Type -> Type
373replaceTypeInType n t (TUnknown m) | m == n = t
374replaceTypeInType n t (Array t1) = Array $ replaceTypeInType n t t1
375replaceTypeInType n t (Object row) = Object $ replaceTypeInRow n t row
376replaceTypeInType n t (Function args ret) = Function (map (replaceTypeInType n t) args) (replaceTypeInType n t ret)
377replaceTypeInType n t (TypeApp t1 t2) = TypeApp (replaceTypeInType n t t1) (replaceTypeInType n t t2)
378replaceTypeInType _ _ other = other
380replaceTypeInRow :: Int -> Type -> Row -> Row
381replaceTypeInRow n t (RCons name ty row) = RCons name (replaceTypeInType n t ty) (replaceTypeInRow n t row)
382replaceTypeInRow n t other = other
384replaceRowInType :: Int -> Row -> Type -> Type
385replaceRowInType n r (Array t1) = Array $ replaceRowInType n r t1
386replaceRowInType n r (Object row) = Object $ replaceRowInRow n r row
387replaceRowInType n r (Function args ret) = Function (map (replaceRowInType n r) args) (replaceRowInType n r ret)
388replaceRowInType n r (TypeApp t1 t2) = TypeApp (replaceRowInType n r t1) (replaceRowInType n r t2)
389replaceRowInType _ _ other = other
391replaceRowInRow :: Int -> Row -> Row -> Row
392replaceRowInRow n r (RUnknown m) | m == n = r
393replaceRowInRow n r (RCons name ty row) = RCons name (replaceRowInType n r ty) (replaceRowInRow n r row)
394replaceRowInRow _ _ other = other
396unifyTypes :: Type -> Type -> Check [TypeConstraint]
397unifyTypes (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
398unifyTypes (TUnknown u) t = do
399 guardWith "Occurs check failed" $ not $ typeOccursCheck False u t
400 return [TypeConstraint u t]
401unifyTypes t (TUnknown u) = do
402 guardWith "Occurs check failed" $ not $ typeOccursCheck False u t
403 return [TypeConstraint u t]
404unifyTypes Number Number = return []
405unifyTypes String String = return []
406unifyTypes Boolean Boolean = return []
407unifyTypes (Array s) (Array t) = unifyTypes s t
408unifyTypes (Object row1) (Object row2) = unifyRows row1 row2
409unifyTypes (Function args1 ret1) (Function args2 ret2) = do
410 guardWith "Function applied to incorrect number of args" $ length args1 == length args2
411 cs1 <- fmap concat $ zipWithM unifyTypes args1 args2
412 cs2 <- unifyTypes ret1 ret2
413 return $ cs1 ++ cs2
414unifyTypes (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
415unifyTypes (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = return []
416unifyTypes (TypeVar v1) (TypeVar v2) = return []
417unifyTypes (TypeApp t1 t2) (TypeApp t3 t4) = do
418 cs1 <- unifyTypes t1 t3
419 cs2 <- unifyTypes t2 t4
420 return $ cs1 ++ cs2
421unifyTypes t1 t2 = throwError $ "Cannot unify " ++ show t1 ++ " with " ++ show t2 ++ "."
423unifyRows :: Row -> Row -> Check [TypeConstraint]
424unifyRows r1 r2 =
425 let
426 (s1, r1') = toList r1
427 (s2, r2') = toList r2
428 int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
429 sd1 = [ (name, t1) | (name, t1) <- s1, not (elem name (map fst s2)) ]
430 sd2 = [ (name, t2) | (name, t2) <- s2, not (elem name (map fst s1)) ]
431 in rethrow (const $ "Cannot unify " ++ show r1 ++ " with " ++ show r2) $ do
432 cs1 <- fmap concat $ mapM (uncurry unifyTypes) int
433 cs2 <- unifyRows' sd1 r1' sd2 r2'
434 return $ cs1 ++ cs2
435 where
436 unifyRows' :: [(String, Type)] -> Row -> [(String, Type)] -> Row -> Check [TypeConstraint]
437 unifyRows' [] (RUnknown u) sd r = do
438 guardWith "Occurs check failed" $ not $ rowOccursCheck False u r
439 return [RowConstraint u (fromList (sd, r))]
440 unifyRows' ((name, ty):row) r others (RUnknown u) = do
441 u' <- fresh
442 cs <- unifyRows' row r others (RUnknown u')
443 return [ RowConstraint u (RCons name ty (RUnknown u')) ]
444 unifyRows' [] REmpty [] REmpty = return []
445 unifyRows' sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ show (fromList (sd1, r1)) ++ " with " ++ show (fromList (sd2, r2)) ++ "."
446 toList :: Row -> ([(String, Type)], Row)
447 toList (RCons name ty row) = let (tys, rest) = toList row
448 in ((name, ty):tys, rest)
449 toList r = ([], r)
450 fromList :: ([(String, Type)], Row) -> Row
451 fromList ([], r) = r
452 fromList ((name, t):ts, r) = RCons name t (fromList (ts, r))
454typeOccursCheck :: Bool -> Int -> Type -> Bool
455typeOccursCheck b u (TUnknown u') | u == u' = b
456typeOccursCheck _ u (Array t) = typeOccursCheck True u t
457typeOccursCheck _ u (Object row) = rowOccursCheck True u row
458typeOccursCheck _ u (Function args ret) = any (typeOccursCheck True u) args || typeOccursCheck True u ret
459typeOccursCheck _ u (TypeApp s t) = typeOccursCheck True u s || typeOccursCheck True u t
460typeOccursCheck _ _ _ = False
462rowOccursCheck :: Bool -> Int -> Row -> Bool
463rowOccursCheck b u (RUnknown u') | u == u' = b
464rowOccursCheck _ u (RCons name ty row) = typeOccursCheck True u ty || rowOccursCheck True u row
465rowOccursCheck _ _ _ = False