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