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