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