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