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