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