git.iko.soy/rowtype-yoga/purescript-native
on 73a773e help sign in
rowtype-yoga/purescript-native/src/PureScript/TypeChecker/Types.hs
573 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-----------------------------------------------------------------------------
15module PureScript.TypeChecker.Types (
16 TypeConstraint(..),
17 TypeSolution(..),
18 typeOf
19) where
21import Data.List
22import Data.Function
23import Data.Data (Data(..))
24import Data.Generics (everywhere, everywhereM, everything, mkT, mkM, mkQ, extM, extQ)
26import PureScript.Values
27import PureScript.Types
28import PureScript.Kinds
29import PureScript.Names
30import PureScript.TypeChecker.Monad
31import PureScript.TypeChecker.Kinds
32import PureScript.TypeChecker.Synonyms
33import PureScript.CodeGen.Pretty.Types
34import PureScript.CodeGen.Pretty.Kinds
36import Control.Monad.State
37import Control.Monad.Error
39import Control.Applicative
40import Control.Arrow (Kleisli(..), (***), (&&&))
41import qualified Control.Category as C
43import qualified Data.Map as M
45data TypeConstraint
46 = TypeConstraint Int Type
47 | RowConstraint Int Row deriving Show
49newtype TypeSolution = TypeSolution { runTypeSolution :: (Int -> Type, Int -> Row) }
51emptyTypeSolution :: TypeSolution
52emptyTypeSolution = TypeSolution (TUnknown, RUnknown)
54typeOf :: Ident -> Value -> Check PolyType
55typeOf 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
67allUnknownsBecameQuantified :: [TypeConstraint] -> TypeSolution -> Type -> Check ()
68allUnknownsBecameQuantified 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
84findUnknownTypes :: (Data d) => d -> [Int]
85findUnknownTypes = everything (++) (mkQ [] f)
86 where
87 f :: Type -> [Int]
88 f (TUnknown n) = [n]
89 f _ = []
91findTypeVars :: (Data d) => d -> [String]
92findTypeVars = everything (++) (mkQ [] f)
93 where
94 f :: Type -> [String]
95 f (TypeVar v) = [v]
96 f _ = []
98findUnknownRows :: (Data d) => d -> [Int]
99findUnknownRows = everything (++) (mkQ [] f)
100 where
101 f :: Row -> [Int]
102 f (RUnknown n) = [n]
103 f _ = []
105varIfUnknown :: Type -> PolyType
106varIfUnknown 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
133replaceVarsWithUnknowns :: [String] -> Type -> Check Type
134replaceVarsWithUnknowns 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
157replaceType :: (Data d) => Int -> Type -> d -> d
158replaceType n t = everywhere (mkT go)
159 where
160 go (TUnknown m) | m == n = t
161 go t = t
163replaceRow :: (Data d) => Int -> Row -> d -> d
164replaceRow n r = everywhere (mkT go)
165 where
166 go (RUnknown m) | m == n = r
167 go r = r
169typeOccursCheck :: Int -> Type -> Check ()
170typeOccursCheck u (TUnknown _) = return ()
171typeOccursCheck u t = when (occursCheck u t) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintType t
173rowOccursCheck :: Int -> Row -> Check ()
174rowOccursCheck u (RUnknown _) = return ()
175rowOccursCheck u r = when (occursCheck u r) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintRow r
177occursCheck :: (Data d) => Int -> d -> Bool
178occursCheck 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
185typeConstraints :: M.Map Ident Int -> Value -> Check ([TypeConstraint], Int)
186typeConstraints _ (NumericLiteral _) = do
187 me <- fresh
188 return ([TypeConstraint me Number], me)
189typeConstraints _ (StringLiteral _) = do
190 me <- fresh
191 return ([TypeConstraint me String], me)
192typeConstraints _ (BooleanLiteral _) = do
193 me <- fresh
194 return ([TypeConstraint me Boolean], me)
195typeConstraints 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)
200typeConstraints m (Unary op val) = do
201 (cs, n1) <- typeConstraints m val
202 me <- fresh
203 return (cs ++ unaryOperatorConstraints op n1 me, me)
204typeConstraints 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)
209typeConstraints 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)
218typeConstraints 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)
223typeConstraints 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)
228typeConstraints 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)
234typeConstraints 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)
240typeConstraints 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)
253typeConstraints 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)
258typeConstraints 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)
266typeConstraints 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)
271typeConstraints 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)
276typeConstraints 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)
283replaceAllTypeSynonyms :: Type -> Check Type
284replaceAllTypeSynonyms 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'
293unaryOperatorConstraints :: UnaryOperator -> Int -> Int -> [TypeConstraint]
294unaryOperatorConstraints Negate val result = [TypeConstraint val Number, TypeConstraint result Number]
295unaryOperatorConstraints Not val result = [TypeConstraint val Boolean, TypeConstraint result Boolean]
296unaryOperatorConstraints BitwiseNot val result = [TypeConstraint val Number, TypeConstraint result Number]
298binaryOperatorConstraints :: BinaryOperator -> Int -> Int -> Int -> [TypeConstraint]
299binaryOperatorConstraints Add = symBinOpConstraints Number
300binaryOperatorConstraints Subtract = symBinOpConstraints Number
301binaryOperatorConstraints Multiply = symBinOpConstraints Number
302binaryOperatorConstraints Divide = symBinOpConstraints Number
303binaryOperatorConstraints Modulus = symBinOpConstraints Number
304binaryOperatorConstraints LessThan = asymBinOpConstraints Number Boolean
305binaryOperatorConstraints LessThanOrEqualTo = asymBinOpConstraints Number Boolean
306binaryOperatorConstraints GreaterThan = asymBinOpConstraints Number Boolean
307binaryOperatorConstraints GreaterThanOrEqualTo = asymBinOpConstraints Number Boolean
308binaryOperatorConstraints BitwiseAnd = symBinOpConstraints Number
309binaryOperatorConstraints BitwiseOr = symBinOpConstraints Number
310binaryOperatorConstraints BitwiseXor = symBinOpConstraints Number
311binaryOperatorConstraints ShiftLeft = symBinOpConstraints Number
312binaryOperatorConstraints ShiftRight = symBinOpConstraints Number
313binaryOperatorConstraints ZeroFillShiftRight = symBinOpConstraints Number
314binaryOperatorConstraints EqualTo = equalityBinOpConstraints
315binaryOperatorConstraints NotEqualTo = equalityBinOpConstraints
316binaryOperatorConstraints And = symBinOpConstraints Boolean
317binaryOperatorConstraints Or = symBinOpConstraints Boolean
318binaryOperatorConstraints Concat = symBinOpConstraints String
320equalityBinOpConstraints :: Int -> Int -> Int -> [TypeConstraint]
321equalityBinOpConstraints left right result = [TypeConstraint left (TUnknown right), TypeConstraint result Boolean]
323symBinOpConstraints :: Type -> Int -> Int -> Int -> [TypeConstraint]
324symBinOpConstraints ty left right result = asymBinOpConstraints ty ty left right result
326asymBinOpConstraints :: Type -> Type -> Int -> Int -> Int -> [TypeConstraint]
327asymBinOpConstraints ty res left right result = [TypeConstraint left ty, TypeConstraint right ty, TypeConstraint result res]
329typeConstraintsForBinder :: Int -> Binder -> Check ([TypeConstraint], M.Map Ident Int)
330typeConstraintsForBinder _ NullBinder = return ([], M.empty)
331typeConstraintsForBinder val (StringBinder _) = constantBinder val String
332typeConstraintsForBinder val (NumberBinder _) = constantBinder val Number
333typeConstraintsForBinder val (BooleanBinder _) = constantBinder val Boolean
334typeConstraintsForBinder val (VarBinder name) = do
335 me <- fresh
336 return ([TypeConstraint me (TUnknown val)], M.singleton name me)
337typeConstraintsForBinder 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"
344typeConstraintsForBinder 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"
354typeConstraintsForBinder 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)
367typeConstraintsForBinder 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)
377typeConstraintsForBinder 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)
381typeConstraintsForBinder 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)
386constantBinder :: Int -> Type -> Check ([TypeConstraint], M.Map Ident Int)
387constantBinder val ty = return ([TypeConstraint val ty], M.empty)
389typeConstraintsForBinders :: M.Map Ident Int -> Int -> Int -> [(Binder, Value)] -> Check [TypeConstraint]
390typeConstraintsForBinders _ _ _ [] = return []
391typeConstraintsForBinders 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)
397assignVariable :: Ident -> M.Map Ident Int -> Check ()
398assignVariable name m =
399 case M.lookup name m of
400 Nothing -> return ()
401 Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."
403typeConstraintsForStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> Statement -> Check ([TypeConstraint], Bool, M.Map Ident Int)
404typeConstraintsForStatement 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)
408typeConstraintsForStatement 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)
412typeConstraintsForStatement 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)
416typeConstraintsForStatement m mass ret (If ifst) = do
417 (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
418 return $ (cs, allCodePathsReturn, mass)
419typeConstraintsForStatement 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)
426typeConstraintsForStatement 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)
434typeConstraintsForStatement m mass ret (Return val) = do
435 (cs1, n1) <- typeConstraints (m `M.union` mass) val
436 return ((TypeConstraint n1 (TUnknown ret)) : cs1, True, mass)
438typeConstraintsForIfStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> IfStatement -> Check ([TypeConstraint], Bool)
439typeConstraintsForIfStatement 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)
443typeConstraintsForIfStatement 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)
449typeConstraintsForElseStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> ElseStatement -> Check ([TypeConstraint], Bool)
450typeConstraintsForElseStatement m mass ret (Else elses) = do
451 (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret elses
452 return (cs, allCodePathsReturn)
453typeConstraintsForElseStatement m mass ret (ElseIf ifst) = do
454 (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
455 return (cs, allCodePathsReturn)
457typeConstraintsForAssignmentTarget :: M.Map Ident Int -> M.Map Ident Int -> Int -> AssignmentTarget -> Check [TypeConstraint]
458typeConstraintsForAssignmentTarget 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)]
463typeConstraintsForAssignmentTarget 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
468typeConstraintsForAssignmentTarget 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
474typeConstraintsForBlock :: M.Map Ident Int -> M.Map Ident Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, M.Map Ident Int)
475typeConstraintsForBlock _ mass _ [] = return ([], False, mass)
476typeConstraintsForBlock 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)
485solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
486solveTypeConstraints [] s = return s
487solveTypeConstraints 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'
493solveTypeConstraints (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'
500substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
501substituteTypeInConstraint n s (TypeConstraint m t)
502 | n == m = unifyTypes s t
503 | otherwise = return [TypeConstraint m (replaceType n s t)]
504substituteTypeInConstraint n s (RowConstraint m r)
505 = return [RowConstraint m (replaceType n s r)]
507substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
508substituteRowInConstraint n r (TypeConstraint m t)
509 = return [TypeConstraint m (replaceRow n r t)]
510substituteRowInConstraint n r (RowConstraint m r1)
511 | m == n = unifyRows r r1
512 | otherwise = return [RowConstraint m (replaceRow n r r1)]
514unifyTypes :: Type -> Type -> Check [TypeConstraint]
515unifyTypes (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
516unifyTypes (TUnknown u) t = do
517 typeOccursCheck u t
518 return [TypeConstraint u t]
519unifyTypes t (TUnknown u) = do
520 typeOccursCheck u t
521 return [TypeConstraint u t]
522unifyTypes Number Number = return []
523unifyTypes String String = return []
524unifyTypes Boolean Boolean = return []
525unifyTypes (Array s) (Array t) = unifyTypes s t
526unifyTypes (Object row1) (Object row2) = unifyRows row1 row2
527unifyTypes (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
532unifyTypes (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
533unifyTypes (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = return []
534unifyTypes (TypeVar v1) (TypeVar v2) = return []
535unifyTypes (TypeApp t1 t2) (TypeApp t3 t4) = do
536 cs1 <- unifyTypes t1 t3
537 cs2 <- unifyTypes t2 t4
538 return $ cs1 ++ cs2
539unifyTypes t1 t2 = throwError $ "Cannot unify " ++ prettyPrintType t1 ++ " with " ++ prettyPrintType t2 ++ "."
541unifyRows :: Row -> Row -> Check [TypeConstraint]
542unifyRows 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))