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