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