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