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