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