git.iko.soy/rowtype-yoga/purescript-native
on f98236e help sign in
rowtype-yoga/purescript-native/src/PureScript/TypeChecker/Types.hs
626 lines 28 kB history raw
1-----------------------------------------------------------------------------
2--
3-- Module : PureScript.TypeChecker.Types
4-- Copyright : (c) Phil Freeman 2013
5-- License : MIT
6--
7-- Maintainer : Phil Freeman <paf31@cantab.net>
8-- Stability : experimental
9-- Portability :
10--
11-- |
12--
13-----------------------------------------------------------------------------
15{-# LANGUAGE DeriveDataTypeable #-}
17module PureScript.TypeChecker.Types (
18 TypeConstraint(..),
19 TypeSolution(..),
20 typeOf
21) where
23import Debug.Trace
25import Data.List
26import Data.Function
27import qualified Data.Data as D
28import Data.Generics (everywhere, everywhereM, everything, mkT, mkM, mkQ, extM, extQ)
30import PureScript.Values
31import PureScript.Types
32import PureScript.Kinds
33import PureScript.Names
34import PureScript.TypeChecker.Monad
35import PureScript.TypeChecker.Kinds
36import PureScript.TypeChecker.Synonyms
37import PureScript.CodeGen.Pretty.Types
38import PureScript.CodeGen.Pretty.Kinds
39import PureScript.CodeGen.Pretty.Values
41import Control.Monad.State
42import Control.Monad.Error
44import Control.Applicative
45import Control.Arrow (Kleisli(..), (***), (&&&), first)
46import qualified Control.Category as C
48import qualified Data.Map as M
50data TypeConstraintOrigin
51 = ValueOrigin Value
52 | BinderOrigin Binder
53 | AssignmentTargetOrigin Ident deriving (Show, D.Data, D.Typeable)
55prettyPrintOrigin :: TypeConstraintOrigin -> String
56prettyPrintOrigin (ValueOrigin val) = prettyPrintValue val
57prettyPrintOrigin (BinderOrigin binder) = prettyPrintBinder binder
58prettyPrintOrigin (AssignmentTargetOrigin ident) = show ident
60data TypeConstraint
61 = TypeConstraint Int Type TypeConstraintOrigin
62 | RowConstraint Int Row TypeConstraintOrigin deriving (Show, D.Data, D.Typeable)
64newtype TypeSolution = TypeSolution { runTypeSolution :: (Int -> Type, Int -> Row) }
66emptyTypeSolution :: TypeSolution
67emptyTypeSolution = TypeSolution (TUnknown, RUnknown)
69isFunction :: Value -> Bool
70isFunction (Abs _ _) = True
71isFunction (TypedValue untyped _) = isFunction untyped
72isFunction _ = False
74allConstraints :: Ident -> Value -> Check ([TypeConstraint], Int)
75allConstraints name val | isFunction val = do
76 me <- fresh
77 (cs, n) <- typeConstraints (M.singleton name me) val
78 return (TypeConstraint me (TUnknown n) (ValueOrigin val): cs, n)
79allConstraints _ val = typeConstraints M.empty val
81typeOf :: Ident -> Value -> Check PolyType
82typeOf name val = do
83 (cs, n) <- allConstraints name val
84 desugared <- replaceAllTypeSynonyms cs
85 solution <- solveTypeConstraints desugared emptyTypeSolution
86 let ty = fst (runTypeSolution solution) n
87 allUnknownsBecameQuantified desugared solution ty
88 return $ varIfUnknown $ desaturateAllTypeSynonyms $ setifyAll ty
90allUnknownsBecameQuantified :: [TypeConstraint] -> TypeSolution -> Type -> Check ()
91allUnknownsBecameQuantified cs solution ty = do
92 let
93 typesMentioned = findUnknownTypes ty
94 unknownTypes = nub $ flip concatMap cs $ \c -> case c of
95 TypeConstraint u t _ -> u : findUnknownTypes t
96 RowConstraint _ r _ -> findUnknownTypes r
97 unsolvedTypes = filter (\n -> TUnknown n == fst (runTypeSolution solution) n) unknownTypes
98 guardWith "Unsolved type variable" $ null $ unsolvedTypes \\ typesMentioned
99 let
100 rowsMentioned = findUnknownRows ty
101 unknownRows = nub $ flip concatMap cs $ \c -> case c of
102 TypeConstraint _ t _ -> findUnknownRows t
103 RowConstraint u r _ -> u : findUnknownRows r
104 unsolvedRows = filter (\n -> RUnknown n == snd (runTypeSolution solution) n) unknownRows
105 guardWith "Unsolved row variable" $ null $ unsolvedRows \\ rowsMentioned
107setify :: Row -> Row
108setify = rowFromList . first (M.toList . M.fromList) . rowToList
110setifyAll :: (D.Data d) => d -> d
111setifyAll = everywhere (mkT setify)
113findUnknownTypes :: (D.Data d) => d -> [Int]
114findUnknownTypes = everything (++) (mkQ [] f)
115 where
116 f :: Type -> [Int]
117 f (TUnknown n) = [n]
118 f _ = []
120findTypeVars :: (D.Data d) => d -> [String]
121findTypeVars = everything (++) (mkQ [] f)
122 where
123 f :: Type -> [String]
124 f (TypeVar v) = [v]
125 f _ = []
127findUnknownRows :: (D.Data d) => d -> [Int]
128findUnknownRows = everything (++) (mkQ [] f)
129 where
130 f :: Row -> [Int]
131 f (RUnknown n) = [n]
132 f _ = []
134varIfUnknown :: Type -> PolyType
135varIfUnknown ty =
136 let
137 (ty', m) = flip runState M.empty $ everywhereM (flip extM g $ mkM f) ty
138 in
139 PolyType (sort $ nub $ M.elems m ++ findTypeVars ty) ty'
140 where
141 f :: Type -> State (M.Map Int String) Type
142 f (TUnknown n) = do
143 m <- get
144 case M.lookup n m of
145 Nothing -> do
146 let name = 't' : show (M.size m)
147 put $ M.insert n name m
148 return $ TypeVar name
149 Just name -> return $ TypeVar name
150 f t = return t
151 g :: Row -> State (M.Map Int String) Row
152 g (RUnknown n) = do
153 m <- get
154 case M.lookup n m of
155 Nothing -> do
156 let name = 'r' : show (M.size m)
157 put $ M.insert n name m
158 return $ RowVar name
159 Just name -> return $ RowVar name
160 g r = return r
162replaceTypeVars :: M.Map String Type -> Type -> Type
163replaceTypeVars m = everywhere (mkT replace)
164 where
165 replace (TypeVar v) = case M.lookup v m of
166 Just ty -> ty
167 _ -> TypeVar v
168 replace t = t
170replaceVarsWithUnknowns :: [String] -> Type -> Check Type
171replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)
172 where
173 f :: Type -> StateT (M.Map String Int) Check Type
174 f (TypeVar var) | var `elem` idents = do
175 m <- get
176 n <- lift fresh
177 case M.lookup var m of
178 Nothing -> do
179 put (M.insert var n m)
180 return $ TUnknown n
181 Just u -> return $ TUnknown u
182 f t = return t
183 g :: Row -> StateT (M.Map String Int) Check Row
184 g (RowVar var) | var `elem` idents = do
185 m <- get
186 n <- lift fresh
187 case M.lookup var m of
188 Nothing -> do
189 put (M.insert var n m)
190 return $ RUnknown n
191 Just u -> return $ RUnknown u
192 g r = return r
194replaceAllTypeSynonyms :: (D.Data d) => d -> Check d
195replaceAllTypeSynonyms d = do
196 env <- getEnv
197 let syns = map (\(name, (args, _)) -> (name, length args)) . M.toList $ typeSynonyms env
198 either throwError return $ saturateAllTypeSynonyms syns d
200desaturateAllTypeSynonyms :: (D.Data d) => d -> d
201desaturateAllTypeSynonyms = everywhere (mkT replace)
202 where
203 replace (SaturatedTypeSynonym name args) = foldl TypeApp (TypeConstructor name) args
204 replace t = t
206replaceType :: (D.Data d) => Int -> Type -> d -> d
207replaceType n t = everywhere (mkT go)
208 where
209 go (TUnknown m) | m == n = t
210 go t = t
212replaceRow :: (D.Data d) => Int -> Row -> d -> d
213replaceRow n r = everywhere (mkT go)
214 where
215 go (RUnknown m) | m == n = r
216 go r = r
218typeOccursCheck :: Int -> Type -> Check ()
219typeOccursCheck u (TUnknown _) = return ()
220typeOccursCheck u t = when (occursCheck u t) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintType t
222rowOccursCheck :: Int -> Row -> Check ()
223rowOccursCheck u (RUnknown _) = return ()
224rowOccursCheck u r = when (occursCheck u r) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintRow r
226occursCheck :: (D.Data d) => Int -> d -> Bool
227occursCheck u = everything (||) $ flip extQ g $ mkQ False f
228 where
229 f (TUnknown u') | u' == u = True
230 f _ = False
231 g (RUnknown u') | u' == u = True
232 g _ = False
234typesToRow :: [(String, Type)] -> Row
235typesToRow [] = REmpty
236typesToRow ((name, ty):tys) = RCons name ty (typesToRow tys)
238rowToList :: Row -> ([(String, Type)], Row)
239rowToList (RCons name ty row) = let (tys, rest) = rowToList row
240 in ((name, ty):tys, rest)
241rowToList r = ([], r)
243rowFromList :: ([(String, Type)], Row) -> Row
244rowFromList ([], r) = r
245rowFromList ((name, t):ts, r) = RCons name t (rowFromList (ts, r))
247ensureNoDuplicateProperties :: [(String, Value)] -> Check ()
248ensureNoDuplicateProperties ps = guardWith "Duplicate property names" $ length (nub . map fst $ ps) == length ps
250typeConstraints :: M.Map Ident Int -> Value -> Check ([TypeConstraint], Int)
251typeConstraints _ v@(NumericLiteral _) = do
252 me <- fresh
253 return ([TypeConstraint me Number (ValueOrigin v)], me)
254typeConstraints _ v@(StringLiteral _) = do
255 me <- fresh
256 return ([TypeConstraint me String (ValueOrigin v)], me)
257typeConstraints _ v@(BooleanLiteral _) = do
258 me <- fresh
259 return ([TypeConstraint me Boolean (ValueOrigin v)], me)
260typeConstraints m v@(ArrayLiteral vals) = do
261 all <- mapM (typeConstraints m) vals
262 let (cs, ns) = (concatMap fst &&& map snd) all
263 me <- fresh
264 return (cs ++ zipWith (\n el -> TypeConstraint me (Array $ TUnknown n) (ValueOrigin el)) ns vals, me)
265typeConstraints m u@(Unary op val) = do
266 (cs, n1) <- typeConstraints m val
267 me <- fresh
268 return (cs ++ unaryOperatorConstraints u op n1 me, me)
269typeConstraints m b@(Binary op left right) = do
270 (cs1, n1) <- typeConstraints m left
271 (cs2, n2) <- typeConstraints m right
272 me <- fresh
273 return (cs1 ++ cs2 ++ binaryOperatorConstraints b op n1 n2 me, me)
274typeConstraints m v@(ObjectLiteral ps) = do
275 ensureNoDuplicateProperties ps
276 all <- mapM (typeConstraints m . snd) ps
277 let (cs, ns) = (concatMap fst &&& map snd) all
278 me <- fresh
279 let tys = zipWith (\(name, _) u -> (name, TUnknown u)) ps ns
280 return (TypeConstraint me (Object (typesToRow tys)) (ValueOrigin v) : cs, me)
281typeConstraints m v@(ObjectUpdate o ps) = do
282 ensureNoDuplicateProperties ps
283 (cs1, n1) <- typeConstraints m o
284 all <- mapM (typeConstraints m . snd) ps
285 let (cs2, ns) = (concatMap fst &&& map snd) all
286 row <- fresh
287 let tys = zipWith (\(name, _) u -> (name, TUnknown u)) ps ns
288 return (TypeConstraint n1 (Object (rowFromList (tys, RUnknown row))) (ValueOrigin v) : cs1 ++ cs2, n1)
289typeConstraints m v@(Indexer index val) = do
290 (cs1, n1) <- typeConstraints m index
291 (cs2, n2) <- typeConstraints m val
292 me <- fresh
293 return (TypeConstraint n1 Number (ValueOrigin index) : TypeConstraint n2 (Array (TUnknown me)) (ValueOrigin v) : cs1 ++ cs2, me)
294typeConstraints m v@(Accessor prop val) = do
295 (cs, n1) <- typeConstraints m val
296 me <- fresh
297 rest <- fresh
298 return (TypeConstraint n1 (Object (RCons prop (TUnknown me) (RUnknown rest))) (ValueOrigin v) : cs, me)
299typeConstraints m v@(Abs args ret) = do
300 ns <- replicateM (length args) fresh
301 let m' = m `M.union` M.fromList (zip args ns)
302 (cs, n') <- typeConstraints m' ret
303 me <- fresh
304 return (TypeConstraint me (Function (map TUnknown ns) (TUnknown n')) (ValueOrigin v) : cs, me)
305typeConstraints m v@(App f xs) = do
306 (cs1, n1) <- typeConstraints m f
307 all <- mapM (typeConstraints m) xs
308 let (cs2, ns) = (concatMap fst &&& map snd) all
309 me <- fresh
310 return (TypeConstraint n1 (Function (map TUnknown ns) (TUnknown me)) (ValueOrigin v) : cs1 ++ cs2, me)
311typeConstraints m v@(Var var) =
312 case M.lookup var m of
313 Nothing -> do
314 env <- getEnv
315 case M.lookup var (names env) of
316 Nothing -> throwError $ show var ++ " is undefined"
317 Just (PolyType idents ty, _) -> do
318 me <- fresh
319 replaced <- replaceVarsWithUnknowns idents ty
320 return ([TypeConstraint me replaced (ValueOrigin v)], me)
321 Just u -> do
322 me <- fresh
323 return ([TypeConstraint u (TUnknown me) (ValueOrigin v)], me)
324typeConstraints m (Block ss) = do
325 ret <- fresh
326 (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m M.empty ret ss
327 guardWith "Block is missing a return statement" allCodePathsReturn
328 return (cs, ret)
329typeConstraints m v@(Constructor c) = do
330 env <- getEnv
331 case M.lookup c (dataConstructors env) of
332 Nothing -> throwError $ "Constructor " ++ c ++ " is undefined"
333 Just (PolyType idents ty) -> do
334 me <- fresh
335 replaced <- replaceVarsWithUnknowns idents ty
336 return ([TypeConstraint me replaced (ValueOrigin v)], me)
337typeConstraints m (Case val binders) = do
338 (cs1, n1) <- typeConstraints m val
339 ret <- fresh
340 cs2 <- typeConstraintsForBinders m n1 ret binders
341 return (cs1 ++ cs2, ret)
342typeConstraints m v@(IfThenElse cond th el) = do
343 (cs1, n1) <- typeConstraints m cond
344 (cs2, n2) <- typeConstraints m th
345 (cs3, n3) <- typeConstraints m el
346 return (TypeConstraint n1 Boolean (ValueOrigin cond) : TypeConstraint n2 (TUnknown n3) (ValueOrigin v) : cs1 ++ cs2 ++ cs3, n2)
347typeConstraints m v@(TypedValue val poly@(PolyType idents ty)) = do
348 kind <- kindOf poly
349 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
350 (cs, n1) <- typeConstraints m val
351 return (TypeConstraint n1 ty (ValueOrigin v) : cs, n1)
353unaryOperatorConstraints :: Value -> UnaryOperator -> Int -> Int -> [TypeConstraint]
354unaryOperatorConstraints v Negate val result = [TypeConstraint val Number (ValueOrigin v), TypeConstraint result Number (ValueOrigin v)]
355unaryOperatorConstraints v Not val result = [TypeConstraint val Boolean (ValueOrigin v), TypeConstraint result Boolean (ValueOrigin v)]
356unaryOperatorConstraints v BitwiseNot val result = [TypeConstraint val Number (ValueOrigin v), TypeConstraint result Number (ValueOrigin v)]
358binaryOperatorConstraints :: Value -> BinaryOperator -> Int -> Int -> Int -> [TypeConstraint]
359binaryOperatorConstraints v Add = symBinOpConstraints v Number
360binaryOperatorConstraints v Subtract = symBinOpConstraints v Number
361binaryOperatorConstraints v Multiply = symBinOpConstraints v Number
362binaryOperatorConstraints v Divide = symBinOpConstraints v Number
363binaryOperatorConstraints v Modulus = symBinOpConstraints v Number
364binaryOperatorConstraints v LessThan = asymBinOpConstraints v Number Boolean
365binaryOperatorConstraints v LessThanOrEqualTo = asymBinOpConstraints v Number Boolean
366binaryOperatorConstraints v GreaterThan = asymBinOpConstraints v Number Boolean
367binaryOperatorConstraints v GreaterThanOrEqualTo = asymBinOpConstraints v Number Boolean
368binaryOperatorConstraints v BitwiseAnd = symBinOpConstraints v Number
369binaryOperatorConstraints v BitwiseOr = symBinOpConstraints v Number
370binaryOperatorConstraints v BitwiseXor = symBinOpConstraints v Number
371binaryOperatorConstraints v ShiftLeft = symBinOpConstraints v Number
372binaryOperatorConstraints v ShiftRight = symBinOpConstraints v Number
373binaryOperatorConstraints v ZeroFillShiftRight = symBinOpConstraints v Number
374binaryOperatorConstraints v EqualTo = equalityBinOpConstraints v
375binaryOperatorConstraints v NotEqualTo = equalityBinOpConstraints v
376binaryOperatorConstraints v And = symBinOpConstraints v Boolean
377binaryOperatorConstraints v Or = symBinOpConstraints v Boolean
378binaryOperatorConstraints v Concat = symBinOpConstraints v String
380equalityBinOpConstraints :: Value -> Int -> Int -> Int -> [TypeConstraint]
381equalityBinOpConstraints v left right result = [TypeConstraint left (TUnknown right) (ValueOrigin v), TypeConstraint result Boolean (ValueOrigin v)]
383symBinOpConstraints :: Value -> Type -> Int -> Int -> Int -> [TypeConstraint]
384symBinOpConstraints v ty = asymBinOpConstraints v ty ty
386asymBinOpConstraints :: Value -> Type -> Type -> Int -> Int -> Int -> [TypeConstraint]
387asymBinOpConstraints v ty res left right result = [TypeConstraint left ty (ValueOrigin v), TypeConstraint right ty (ValueOrigin v), TypeConstraint result res (ValueOrigin v)]
389typeConstraintsForBinder :: Int -> Binder -> Check ([TypeConstraint], M.Map Ident Int)
390typeConstraintsForBinder _ NullBinder = return ([], M.empty)
391typeConstraintsForBinder val b@(StringBinder _) = constantBinder b val String
392typeConstraintsForBinder val b@(NumberBinder _) = constantBinder b val Number
393typeConstraintsForBinder val b@(BooleanBinder _) = constantBinder b val Boolean
394typeConstraintsForBinder val b@(VarBinder name) = do
395 me <- fresh
396 return ([TypeConstraint me (TUnknown val) (BinderOrigin b)], M.singleton name me)
397typeConstraintsForBinder val b@(NullaryBinder ctor) = do
398 env <- getEnv
399 case M.lookup ctor (dataConstructors env) of
400 Just (PolyType args ret) -> do
401 ret' <- replaceVarsWithUnknowns args ret
402 return ([TypeConstraint val ret' (BinderOrigin b)], M.empty)
403 _ -> throwError $ "Constructor " ++ ctor ++ " is not defined"
404typeConstraintsForBinder val b@(UnaryBinder ctor binder) = do
405 env <- getEnv
406 case M.lookup ctor (dataConstructors env) of
407 Just (PolyType idents f@(Function [_] _)) -> do
408 obj <- fresh
409 (Function [ty] ret) <- replaceVarsWithUnknowns idents f
410 (cs, m1) <- typeConstraintsForBinder obj binder
411 return (TypeConstraint val ret (BinderOrigin b) : TypeConstraint obj ty (BinderOrigin b) : cs, m1)
412 Just _ -> throwError $ ctor ++ " is not a unary constructor"
413 _ -> throwError $ "Constructor " ++ ctor ++ " is not defined"
414typeConstraintsForBinder val b@(ObjectBinder props) = do
415 row <- fresh
416 rest <- fresh
417 (cs, m1) <- typeConstraintsForProperties row (RUnknown rest) props
418 return (TypeConstraint val (Object (RUnknown row)) (BinderOrigin b) : cs, m1)
419 where
420 typeConstraintsForProperties :: Int -> Row -> [(String, Binder)] -> Check ([TypeConstraint], M.Map Ident Int)
421 typeConstraintsForProperties nrow row [] = return ([RowConstraint nrow row (BinderOrigin b)], M.empty)
422 typeConstraintsForProperties nrow row ((name, binder):binders) = do
423 propTy <- fresh
424 (cs1, m1) <- typeConstraintsForBinder propTy binder
425 (cs2, m2) <- typeConstraintsForProperties nrow (RCons name (TUnknown propTy) row) binders
426 return (cs1 ++ cs2, m1 `M.union` m2)
427typeConstraintsForBinder val b@(ArrayBinder binders rest) = do
428 el <- fresh
429 all <- mapM (typeConstraintsForBinder el) binders
430 let (cs1, m1) = (concatMap fst &&& M.unions . map snd) all
431 let arrayConstraint = TypeConstraint val (Array (TUnknown el)) (BinderOrigin b)
432 case rest of
433 Nothing -> return (arrayConstraint : cs1, m1)
434 Just binder -> do
435 (cs2, m2) <- typeConstraintsForBinder val binder
436 return (arrayConstraint : cs1 ++ cs2, m1 `M.union` m2)
437typeConstraintsForBinder val b@(NamedBinder name binder) = do
438 me <- fresh
439 (cs, m) <- typeConstraintsForBinder val binder
440 return (TypeConstraint me (TUnknown val) (BinderOrigin b) : cs, M.insert name me m)
441typeConstraintsForBinder val b@(GuardedBinder cond binder) = do
442 (cs1, m) <- typeConstraintsForBinder val binder
443 (cs2, n) <- typeConstraints m cond
444 return (TypeConstraint n Boolean (ValueOrigin cond) : cs1 ++ cs2, m)
446constantBinder :: Binder -> Int -> Type -> Check ([TypeConstraint], M.Map Ident Int)
447constantBinder b val ty = return ([TypeConstraint val ty (BinderOrigin b)], M.empty)
449typeConstraintsForBinders :: M.Map Ident Int -> Int -> Int -> [(Binder, Value)] -> Check [TypeConstraint]
450typeConstraintsForBinders _ _ _ [] = return []
451typeConstraintsForBinders m nval ret ((binder, val):bs) = do
452 (cs1, m1) <- typeConstraintsForBinder nval binder
453 (cs2, n2) <- typeConstraints (m `M.union` m1) val
454 cs3 <- typeConstraintsForBinders m nval ret bs
455 return (TypeConstraint n2 (TUnknown ret) (BinderOrigin binder) : cs1 ++ cs2 ++ cs3)
457assignVariable :: Ident -> M.Map Ident Int -> Check ()
458assignVariable name m =
459 case M.lookup name m of
460 Nothing -> return ()
461 Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."
463typeConstraintsForStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> Statement -> Check ([TypeConstraint], Bool, M.Map Ident Int)
464typeConstraintsForStatement m mass ret (VariableIntroduction name val) = do
465 assignVariable name (m `M.union` mass)
466 (cs1, n1) <- typeConstraints m val
467 return (cs1, False, M.insert name n1 mass)
468typeConstraintsForStatement m mass ret (Assignment ident val) = do
469 (cs1, n1) <- typeConstraints m val
470 case M.lookup ident mass of
471 Nothing -> throwError $ "No local variable with name " ++ show ident
472 Just ty ->
473 return (TypeConstraint n1 (TUnknown ty) (AssignmentTargetOrigin ident) : cs1, False, mass)
474typeConstraintsForStatement m mass ret (While val inner) = do
475 (cs1, n1) <- typeConstraints m val
476 (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret inner
477 return (TypeConstraint n1 Boolean (ValueOrigin val) : cs1 ++ cs2, allCodePathsReturn, mass)
478typeConstraintsForStatement m mass ret (If ifst) = do
479 (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
480 return (cs, allCodePathsReturn, mass)
481typeConstraintsForStatement m mass ret (For ident start end inner) = do
482 assignVariable ident (m `M.union` mass)
483 (cs1, n1) <- typeConstraints (m `M.union` mass) start
484 (cs2, n2) <- typeConstraints (m `M.union` mass) end
485 let mass1 = M.insert ident n1 mass
486 (cs3, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass1) mass1 ret inner
487 return (TypeConstraint n1 Number (ValueOrigin start) : TypeConstraint n2 Number (ValueOrigin end) : cs1 ++ cs2 ++ cs3, allCodePathsReturn, mass)
488typeConstraintsForStatement m mass ret (ForEach ident vals inner) = do
489 assignVariable ident (m `M.union` mass)
490 val <- fresh
491 (cs1, n1) <- typeConstraints (m `M.union` mass) vals
492 let mass1 = M.insert ident val mass
493 (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass1) mass1 ret inner
494 guardWith "Cannot return from within a foreach block" $ not allCodePathsReturn
495 return (TypeConstraint n1 (Array (TUnknown val)) (ValueOrigin vals) : cs1 ++ cs2, False, mass)
496typeConstraintsForStatement m mass ret (Return val) = do
497 (cs1, n1) <- typeConstraints (m `M.union` mass) val
498 return (TypeConstraint n1 (TUnknown ret) (ValueOrigin val) : cs1, True, mass)
500typeConstraintsForIfStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> IfStatement -> Check ([TypeConstraint], Bool)
501typeConstraintsForIfStatement m mass ret (IfStatement val thens Nothing) = do
502 (cs1, n1) <- typeConstraints m val
503 (cs2, _, _) <- typeConstraintsForBlock m mass ret thens
504 return (TypeConstraint n1 Boolean (ValueOrigin val) : cs1 ++ cs2, False)
505typeConstraintsForIfStatement m mass ret (IfStatement val thens (Just elses)) = do
506 (cs1, n1) <- typeConstraints m val
507 (cs2, allCodePathsReturn1, _) <- typeConstraintsForBlock m mass ret thens
508 (cs3, allCodePathsReturn2) <- typeConstraintsForElseStatement m mass ret elses
509 return (TypeConstraint n1 Boolean (ValueOrigin val) : cs1 ++ cs2 ++ cs3, allCodePathsReturn1 && allCodePathsReturn2)
511typeConstraintsForElseStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> ElseStatement -> Check ([TypeConstraint], Bool)
512typeConstraintsForElseStatement m mass ret (Else elses) = do
513 (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret elses
514 return (cs, allCodePathsReturn)
515typeConstraintsForElseStatement m mass ret (ElseIf ifst) = do
516 (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
517 return (cs, allCodePathsReturn)
519typeConstraintsForBlock :: M.Map Ident Int -> M.Map Ident Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, M.Map Ident Int)
520typeConstraintsForBlock _ mass _ [] = return ([], False, mass)
521typeConstraintsForBlock m mass ret (s:ss) = do
522 (cs1, b1, mass1) <- typeConstraintsForStatement (m `M.union` mass) mass ret s
523 case (b1, ss) of
524 (True, []) -> return (cs1, True, mass1)
525 (True, _) -> throwError "Unreachable code"
526 (False, ss) -> do
527 (cs2, b2, mass2) <- typeConstraintsForBlock m mass1 ret ss
528 return (cs1 ++ cs2, b2, mass2)
530solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
531solveTypeConstraints [] s = return s
532solveTypeConstraints all@(TypeConstraint n t o:cs) s = do
533 (cs', s') <- rethrow (\err -> "Error in " ++ prettyPrintOrigin o ++ ": " ++ err) $ do
534 typeOccursCheck n t
535 let s' = let (f, g) = runTypeSolution s
536 in TypeSolution (replaceType n t . f, replaceType n t . g)
537 cs' <- fmap concat $ mapM (substituteTypeInConstraint n t) cs
538 return (cs', s')
539 solveTypeConstraints cs' s'
540solveTypeConstraints (RowConstraint n r o:cs) s = do
541 (cs', s') <- rethrow (\err -> "Error in " ++ prettyPrintOrigin o ++ ": " ++ err) $ do
542 rowOccursCheck n r
543 let s' = let (f, g) = runTypeSolution s
544 in TypeSolution (replaceRow n r . f, replaceRow n r . g)
545 cs' <- fmap concat $ mapM (substituteRowInConstraint n r) cs
546 return (cs', s')
547 solveTypeConstraints cs' s'
549substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
550substituteTypeInConstraint n s (TypeConstraint m t v)
551 | n == m = unifyTypes v s t
552 | otherwise = return [TypeConstraint m (replaceType n s t) v]
553substituteTypeInConstraint n s (RowConstraint m r v)
554 = return [RowConstraint m (replaceType n s r) v]
556substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
557substituteRowInConstraint n r (TypeConstraint m t v)
558 = return [TypeConstraint m (replaceRow n r t) v]
559substituteRowInConstraint n r (RowConstraint m r1 v)
560 | m == n = unifyRows v r r1
561 | otherwise = return [RowConstraint m (replaceRow n r r1) v]
563unifyTypes :: TypeConstraintOrigin -> Type -> Type -> Check [TypeConstraint]
564unifyTypes _ (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
565unifyTypes o (TUnknown u) t = do
566 typeOccursCheck u t
567 return [TypeConstraint u t o]
568unifyTypes o t (TUnknown u) = do
569 typeOccursCheck u t
570 return [TypeConstraint u t o]
571unifyTypes o (SaturatedTypeSynonym name1 args1) (SaturatedTypeSynonym name2 args2) | name1 == name2 =
572 fmap concat $ zipWithM (unifyTypes o) args1 args2
573unifyTypes o (SaturatedTypeSynonym name args) ty = do
574 env <- getEnv
575 case M.lookup name (typeSynonyms env) of
576 Just (synArgs, body) -> do
577 let m = M.fromList $ zip synArgs args
578 let replaced = replaceTypeVars m body
579 unifyTypes o replaced ty
580 Nothing -> error "Type synonym was not defined"
581unifyTypes o ty s@(SaturatedTypeSynonym _ _) = unifyTypes o s ty
582unifyTypes _ Number Number = return []
583unifyTypes _ String String = return []
584unifyTypes _ Boolean Boolean = return []
585unifyTypes o (Array s) (Array t) = unifyTypes o s t
586unifyTypes o (Object row1) (Object row2) = unifyRows o row1 row2
587unifyTypes o (Function args1 ret1) (Function args2 ret2) = do
588 guardWith "Function applied to incorrect number of args" $ length args1 == length args2
589 cs1 <- fmap concat $ zipWithM (unifyTypes o) args1 args2
590 cs2 <- unifyTypes o ret1 ret2
591 return $ cs1 ++ cs2
592unifyTypes _ (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
593unifyTypes _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = return []
594unifyTypes o (TypeApp t1 t2) (TypeApp t3 t4) = do
595 cs1 <- unifyTypes o t1 t3
596 cs2 <- unifyTypes o t2 t4
597 return $ cs1 ++ cs2
598unifyTypes _ t1 t2 = throwError $ "Cannot unify " ++ prettyPrintType t1 ++ " with " ++ prettyPrintType t2 ++ "."
600unifyRows :: TypeConstraintOrigin -> Row -> Row -> Check [TypeConstraint]
601unifyRows o r1 r2 =
602 let
603 (s1, r1') = rowToList r1
604 (s2, r2') = rowToList r2
605 int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
606 sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
607 sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
608 in do
609 cs1 <- fmap concat $ mapM (uncurry $ unifyTypes o) int
610 cs2 <- unifyRows' o sd1 r1' sd2 r2'
611 return $ cs1 ++ cs2
612 where
613 unifyRows' :: TypeConstraintOrigin -> [(String, Type)] -> Row -> [(String, Type)] -> Row -> Check [TypeConstraint]
614 unifyRows' o [] (RUnknown u) sd r = do
615 rowOccursCheck u r
616 return [RowConstraint u (rowFromList (sd, r)) o]
617 unifyRows' o sd r [] (RUnknown u) = do
618 rowOccursCheck u r
619 return [RowConstraint u (rowFromList (sd, r)) o]
620 unifyRows' o ns@((name, ty):row) r others (RUnknown u) | not (occursCheck u (ty, row)) = do
621 u' <- fresh
622 cs <- unifyRows' o row r others (RUnknown u')
623 return (RowConstraint u (RCons name ty (RUnknown u')) o : cs)
624 unifyRows' _ [] REmpty [] REmpty = return []
625 unifyRows' _ [] (RowVar v1) [] (RowVar v2) | v1 == v2 = return []
626 unifyRows' _ sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd1, r1)) ++ " with " ++ prettyPrintRow (rowFromList (sd2, r2)) ++ "."