@@ -1,483 +0,0 @@
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 : cs, 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