git.iko.soy/rowtype-yoga/purescript-native
on 1997015 help sign in
rowtype-yoga/purescript-native/src/PureScript/TypeChecker/Types.hs
571 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
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 (IfThenElse cond th el) = do
270 (cs1, n1) <- typeConstraints m cond
271 (cs2, n2) <- typeConstraints m th
272 (cs3, n3) <- typeConstraints m el
273 return (TypeConstraint n1 Boolean : TypeConstraint n2 (TUnknown n3) : cs1 ++ cs2 ++ cs3, n2)
274typeConstraints m (TypedValue val poly@(PolyType idents ty)) = do
275 kind <- kindOf poly
276 guardWith ("Expected type of kind *, was " ++ show kind) $ kind == Star
277 desugared <- replaceAllTypeSynonyms ty
278 (cs, n1) <- typeConstraints m val
279 return (TypeConstraint n1 desugared : cs, n1)
281replaceAllTypeSynonyms :: Type -> Check Type
282replaceAllTypeSynonyms ty = do
283 env <- getEnv
284 go (M.toList $ typeSynonyms env) ty
285 where
286 go [] ty = return ty
287 go ((name, (args, repl)):rest) ty = do
288 ty' <- either throwError return (substituteTypeSynonym name args repl ty)
289 go rest ty'
291unaryOperatorConstraints :: UnaryOperator -> Int -> Int -> [TypeConstraint]
292unaryOperatorConstraints Negate val result = [TypeConstraint val Number, TypeConstraint result Number]
293unaryOperatorConstraints Not val result = [TypeConstraint val Boolean, TypeConstraint result Boolean]
294unaryOperatorConstraints BitwiseNot val result = [TypeConstraint val Number, TypeConstraint result Number]
296binaryOperatorConstraints :: BinaryOperator -> Int -> Int -> Int -> [TypeConstraint]
297binaryOperatorConstraints Add = symBinOpConstraints Number
298binaryOperatorConstraints Subtract = symBinOpConstraints Number
299binaryOperatorConstraints Multiply = symBinOpConstraints Number
300binaryOperatorConstraints Divide = symBinOpConstraints Number
301binaryOperatorConstraints Modulus = symBinOpConstraints Number
302binaryOperatorConstraints LessThan = asymBinOpConstraints Number Boolean
303binaryOperatorConstraints LessThanOrEqualTo = asymBinOpConstraints Number Boolean
304binaryOperatorConstraints GreaterThan = asymBinOpConstraints Number Boolean
305binaryOperatorConstraints GreaterThanOrEqualTo = asymBinOpConstraints Number Boolean
306binaryOperatorConstraints BitwiseAnd = symBinOpConstraints Number
307binaryOperatorConstraints BitwiseOr = symBinOpConstraints Number
308binaryOperatorConstraints BitwiseXor = symBinOpConstraints Number
309binaryOperatorConstraints ShiftLeft = symBinOpConstraints Number
310binaryOperatorConstraints ShiftRight = symBinOpConstraints Number
311binaryOperatorConstraints ZeroFillShiftRight = symBinOpConstraints Number
312binaryOperatorConstraints EqualTo = equalityBinOpConstraints
313binaryOperatorConstraints NotEqualTo = equalityBinOpConstraints
314binaryOperatorConstraints And = symBinOpConstraints Boolean
315binaryOperatorConstraints Or = symBinOpConstraints Boolean
316binaryOperatorConstraints Concat = symBinOpConstraints String
318equalityBinOpConstraints :: Int -> Int -> Int -> [TypeConstraint]
319equalityBinOpConstraints left right result = [TypeConstraint left (TUnknown right), TypeConstraint result Boolean]
321symBinOpConstraints :: Type -> Int -> Int -> Int -> [TypeConstraint]
322symBinOpConstraints ty left right result = asymBinOpConstraints ty ty left right result
324asymBinOpConstraints :: Type -> Type -> Int -> Int -> Int -> [TypeConstraint]
325asymBinOpConstraints ty res left right result = [TypeConstraint left ty, TypeConstraint right ty, TypeConstraint result res]
327typeConstraintsForBinder :: Int -> Binder -> Check ([TypeConstraint], M.Map Ident Int)
328typeConstraintsForBinder _ NullBinder = return ([], M.empty)
329typeConstraintsForBinder val (StringBinder _) = constantBinder val String
330typeConstraintsForBinder val (NumberBinder _) = constantBinder val Number
331typeConstraintsForBinder val (BooleanBinder _) = constantBinder val Boolean
332typeConstraintsForBinder val (VarBinder name) = do
333 me <- fresh
334 return ([TypeConstraint me (TUnknown val)], M.singleton name me)
335typeConstraintsForBinder val (NullaryBinder ctor) = do
336 env <- getEnv
337 case M.lookup ctor (dataConstructors env) of
338 Just (PolyType args ret) -> do
339 ret' <- replaceVarsWithUnknowns args ret
340 return ([TypeConstraint val ret'], M.empty)
341 _ -> throwError $ "Constructor " ++ ctor ++ " is not defined"
342typeConstraintsForBinder val (UnaryBinder ctor binder) = do
343 env <- getEnv
344 case M.lookup ctor (dataConstructors env) of
345 Just (PolyType idents f@(Function [_] _)) -> do
346 obj <- fresh
347 (Function [ty] ret) <- replaceVarsWithUnknowns idents f
348 (cs, m1) <- typeConstraintsForBinder obj binder
349 return ((TypeConstraint val ret) : (TypeConstraint obj ty) : cs, m1)
350 Just _ -> throwError $ ctor ++ " is not a unary constructor"
351 _ -> throwError $ "Constructor " ++ ctor ++ " is not defined"
352typeConstraintsForBinder val (ObjectBinder props) = do
353 row <- fresh
354 rest <- fresh
355 (cs, m1) <- typeConstraintsForProperties row (RUnknown rest) props
356 return ((TypeConstraint val (Object (RUnknown row))) : cs, m1)
357 where
358 typeConstraintsForProperties :: Int -> Row -> [(String, Binder)] -> Check ([TypeConstraint], M.Map Ident Int)
359 typeConstraintsForProperties nrow row [] = return ([RowConstraint nrow row], M.empty)
360 typeConstraintsForProperties nrow row ((name, binder):binders) = do
361 propTy <- fresh
362 (cs1, m1) <- typeConstraintsForBinder propTy binder
363 (cs2, m2) <- typeConstraintsForProperties nrow (RCons name (TUnknown propTy) row) binders
364 return (cs1 ++ cs2, M.union m1 m2)
365typeConstraintsForBinder val (ArrayBinder binders rest) = do
366 el <- fresh
367 all <- mapM (typeConstraintsForBinder el) binders
368 let (cs1, m1) = (concat . map fst &&& M.unions . map snd) all
369 let arrayConstraint = TypeConstraint val (Array (TUnknown el))
370 case rest of
371 Nothing -> return (arrayConstraint : cs1, m1)
372 Just binder -> do
373 (cs2, m2) <- typeConstraintsForBinder val binder
374 return (arrayConstraint : cs1 ++ cs2, M.union m1 m2)
375typeConstraintsForBinder val (NamedBinder name binder) = do
376 me <- fresh
377 (cs, m) <- typeConstraintsForBinder val binder
378 return (TypeConstraint me (TUnknown val) : cs, M.insert name me m)
379typeConstraintsForBinder val (GuardedBinder cond binder) = do
380 (cs1, m) <- typeConstraintsForBinder val binder
381 (cs2, n) <- typeConstraints m cond
382 return (TypeConstraint n Boolean : cs1 ++ cs2, m)
384constantBinder :: Int -> Type -> Check ([TypeConstraint], M.Map Ident Int)
385constantBinder val ty = return ([TypeConstraint val ty], M.empty)
387typeConstraintsForBinders :: M.Map Ident Int -> Int -> Int -> [(Binder, Value)] -> Check [TypeConstraint]
388typeConstraintsForBinders _ _ _ [] = return []
389typeConstraintsForBinders m nval ret ((binder, val):bs) = do
390 (cs1, m1) <- typeConstraintsForBinder nval binder
391 (cs2, n2) <- typeConstraints (M.union m m1) val
392 cs3 <- typeConstraintsForBinders m nval ret bs
393 return ((TypeConstraint n2 (TUnknown ret)) : cs1 ++ cs2 ++ cs3)
395assignVariable :: Ident -> M.Map Ident Int -> Check ()
396assignVariable name m =
397 case M.lookup name m of
398 Nothing -> return ()
399 Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."
401typeConstraintsForStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> Statement -> Check ([TypeConstraint], Bool, M.Map Ident Int)
402typeConstraintsForStatement m mass ret (VariableIntroduction name val) = do
403 assignVariable name (m `M.union` mass)
404 (cs1, n1) <- typeConstraints m val
405 return $ (cs1, False, M.insert name n1 mass)
406typeConstraintsForStatement m mass ret (Assignment tgt val) = do
407 (cs1, n1) <- typeConstraints m val
408 cs2 <- typeConstraintsForAssignmentTarget m mass n1 tgt
409 return (cs1 ++ cs2, False, mass)
410typeConstraintsForStatement m mass ret (While val inner) = do
411 (cs1, n1) <- typeConstraints m val
412 (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret inner
413 return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2, allCodePathsReturn, mass)
414typeConstraintsForStatement m mass ret (If ifst) = do
415 (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
416 return $ (cs, allCodePathsReturn, mass)
417typeConstraintsForStatement m mass ret (For ident start end inner) = do
418 assignVariable ident (m `M.union` mass)
419 (cs1, n1) <- typeConstraints (m `M.union` mass) start
420 (cs2, n2) <- typeConstraints (m `M.union` mass) end
421 let mass1 = M.insert ident n1 mass
422 (cs3, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass1) mass1 ret inner
423 return $ ((TypeConstraint n1 Number) : (TypeConstraint n2 Number) : cs1 ++ cs2 ++ cs3, allCodePathsReturn, mass)
424typeConstraintsForStatement m mass ret (ForEach ident vals inner) = do
425 assignVariable ident (m `M.union` mass)
426 val <- fresh
427 (cs1, n1) <- typeConstraints (m `M.union` mass) vals
428 let mass1 = M.insert ident val mass
429 (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass1) mass1 ret inner
430 guardWith "Cannot return from within a foreach block" $ not allCodePathsReturn
431 return $ ((TypeConstraint n1 (Array (TUnknown val))) : cs1 ++ cs2, False, mass)
432typeConstraintsForStatement m mass ret (Return val) = do
433 (cs1, n1) <- typeConstraints (m `M.union` mass) val
434 return ((TypeConstraint n1 (TUnknown ret)) : cs1, True, mass)
436typeConstraintsForIfStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> IfStatement -> Check ([TypeConstraint], Bool)
437typeConstraintsForIfStatement m mass ret (IfStatement val thens Nothing) = do
438 (cs1, n1) <- typeConstraints m val
439 (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret thens
440 return ((TypeConstraint n1 Boolean) : cs1 ++ cs2, allCodePathsReturn)
441typeConstraintsForIfStatement m mass ret (IfStatement val thens (Just elses)) = do
442 (cs1, n1) <- typeConstraints m val
443 (cs2, allCodePathsReturn1, _) <- typeConstraintsForBlock m mass ret thens
444 (cs3, allCodePathsReturn2) <- typeConstraintsForElseStatement m mass ret elses
445 return ((TypeConstraint n1 Boolean) : cs1 ++ cs2 ++ cs3, allCodePathsReturn1 && allCodePathsReturn2)
447typeConstraintsForElseStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> ElseStatement -> Check ([TypeConstraint], Bool)
448typeConstraintsForElseStatement m mass ret (Else elses) = do
449 (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret elses
450 return (cs, allCodePathsReturn)
451typeConstraintsForElseStatement m mass ret (ElseIf ifst) = do
452 (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
453 return (cs, allCodePathsReturn)
455typeConstraintsForAssignmentTarget :: M.Map Ident Int -> M.Map Ident Int -> Int -> AssignmentTarget -> Check [TypeConstraint]
456typeConstraintsForAssignmentTarget m mass nval (AssignVariable var) =
457 case M.lookup var mass of
458 Nothing -> throwError $ "No local variable with name " ++ show var
459 Just ty -> do
460 return [TypeConstraint nval (TUnknown ty)]
461typeConstraintsForAssignmentTarget m mass nval (AssignArrayIndex index tgt) = do
462 arr <- fresh
463 (cs1, n1) <- typeConstraints (m `M.union` mass) index
464 cs2 <- typeConstraintsForAssignmentTarget m mass arr tgt
465 return $ (TypeConstraint arr (Array (TUnknown nval))) : (TypeConstraint n1 Number) : cs1 ++ cs2
466typeConstraintsForAssignmentTarget m mass nval (AssignObjectProperty prop tgt) = do
467 obj <- fresh
468 row <- fresh
469 cs <- typeConstraintsForAssignmentTarget m mass obj tgt
470 return $ (TypeConstraint obj (Object (RCons prop (TUnknown nval) $ RUnknown row))) : cs
472typeConstraintsForBlock :: M.Map Ident Int -> M.Map Ident Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, M.Map Ident Int)
473typeConstraintsForBlock _ mass _ [] = return ([], False, mass)
474typeConstraintsForBlock m mass ret (s:ss) = do
475 (cs1, b1, mass1) <- typeConstraintsForStatement (m `M.union` mass) mass ret s
476 case (b1, ss) of
477 (True, []) -> return (cs1, True, mass1)
478 (True, _) -> throwError "Unreachable code"
479 (False, ss) -> do
480 (cs2, b2, mass2) <- typeConstraintsForBlock m mass1 ret ss
481 return (cs1 ++ cs2, b2, mass2)
483solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
484solveTypeConstraints [] s = return s
485solveTypeConstraints all@(TypeConstraint n t:cs) s = do
486 typeOccursCheck n t
487 let s' = let (f, g) = runTypeSolution s
488 in TypeSolution (replaceType n t . f, replaceType n t . g)
489 cs' <- fmap concat $ mapM (substituteTypeInConstraint n t) cs
490 solveTypeConstraints cs' s'
491solveTypeConstraints (RowConstraint n r:cs) s = do
492 rowOccursCheck n r
493 let s' = let (f, g) = runTypeSolution s
494 in TypeSolution $ (replaceRow n r . f, replaceRow n r . g)
495 cs' <- fmap concat $ mapM (substituteRowInConstraint n r) cs
496 solveTypeConstraints cs' s'
498substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
499substituteTypeInConstraint n s (TypeConstraint m t)
500 | n == m = unifyTypes s t
501 | otherwise = return [TypeConstraint m (replaceType n s t)]
502substituteTypeInConstraint n s (RowConstraint m r)
503 = return [RowConstraint m (replaceType n s r)]
505substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
506substituteRowInConstraint n r (TypeConstraint m t)
507 = return [TypeConstraint m (replaceRow n r t)]
508substituteRowInConstraint n r (RowConstraint m r1)
509 | m == n = unifyRows r r1
510 | otherwise = return [RowConstraint m (replaceRow n r r1)]
512unifyTypes :: Type -> Type -> Check [TypeConstraint]
513unifyTypes (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
514unifyTypes (TUnknown u) t = do
515 typeOccursCheck u t
516 return [TypeConstraint u t]
517unifyTypes t (TUnknown u) = do
518 typeOccursCheck u t
519 return [TypeConstraint u t]
520unifyTypes Number Number = return []
521unifyTypes String String = return []
522unifyTypes Boolean Boolean = return []
523unifyTypes (Array s) (Array t) = unifyTypes s t
524unifyTypes (Object row1) (Object row2) = unifyRows row1 row2
525unifyTypes (Function args1 ret1) (Function args2 ret2) = do
526 guardWith "Function applied to incorrect number of args" $ length args1 == length args2
527 cs1 <- fmap concat $ zipWithM unifyTypes args1 args2
528 cs2 <- unifyTypes ret1 ret2
529 return $ cs1 ++ cs2
530unifyTypes (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
531unifyTypes (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = return []
532unifyTypes (TypeVar v1) (TypeVar v2) = return []
533unifyTypes (TypeApp t1 t2) (TypeApp t3 t4) = do
534 cs1 <- unifyTypes t1 t3
535 cs2 <- unifyTypes t2 t4
536 return $ cs1 ++ cs2
537unifyTypes t1 t2 = throwError $ "Cannot unify " ++ show t1 ++ " with " ++ show t2 ++ "."
539unifyRows :: Row -> Row -> Check [TypeConstraint]
540unifyRows r1 r2 =
541 let
542 (s1, r1') = toList r1
543 (s2, r2') = toList r2
544 int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
545 sd1 = [ (name, t1) | (name, t1) <- s1, not (elem name (map fst s2)) ]
546 sd2 = [ (name, t2) | (name, t2) <- s2, not (elem name (map fst s1)) ]
547 in rethrow (\e -> "Cannot unify " ++ show r1 ++ " with " ++ show r2 ++ ": " ++ e) $ do
548 cs1 <- fmap concat $ mapM (uncurry unifyTypes) int
549 cs2 <- unifyRows' sd1 r1' sd2 r2'
550 return $ cs1 ++ cs2
551 where
552 unifyRows' :: [(String, Type)] -> Row -> [(String, Type)] -> Row -> Check [TypeConstraint]
553 unifyRows' [] (RUnknown u) sd r = do
554 rowOccursCheck u r
555 return [RowConstraint u (fromList (sd, r))]
556 unifyRows' sd r [] (RUnknown u) = do
557 rowOccursCheck u r
558 return [RowConstraint u (fromList (sd, r))]
559 unifyRows' ((name, ty):row) r others (RUnknown u) = do
560 u' <- fresh
561 cs <- unifyRows' row r others (RUnknown u')
562 return (RowConstraint u (RCons name ty (RUnknown u')) : cs)
563 unifyRows' [] REmpty [] REmpty = return []
564 unifyRows' sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ show (fromList (sd1, r1)) ++ " with " ++ show (fromList (sd2, r2)) ++ "."
565 toList :: Row -> ([(String, Type)], Row)
566 toList (RCons name ty row) = let (tys, rest) = toList row
567 in ((name, ty):tys, rest)
568 toList r = ([], r)
569 fromList :: ([(String, Type)], Row) -> Row
570 fromList ([], r) = r
571 fromList ((name, t):ts, r) = RCons name t (fromList (ts, r))