git.iko.soy/rowtype-yoga/purescript-native
on eec09d8 help sign in
rowtype-yoga/purescript-native/src/PureScript/TypeChecker/Types.hs
536 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 (If ifst) = do
387 (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
388 return $ (cs, allCodePathsReturn, mass)
389typeConstraintsForStatement m mass ret (For (init, cond, cont) inner) = do
390 (cs1, b1, mass1) <- typeConstraintsForStatement m mass ret init
391 guardWith "Cannot return from inside for" $ not b1
392 (cs2, n1) <- typeConstraints (m `M.union` mass1) cond
393 (cs3, b2, mass2) <- typeConstraintsForStatement (m `M.union` mass1) mass1 ret cont
394 guardWith "Cannot return from inside for" $ not b2
395 (cs4, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass2) mass2 ret inner
396 return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2 ++ cs3 ++ cs4, allCodePathsReturn, mass)
397typeConstraintsForStatement m mass ret (Return val) = do
398 (cs1, n1) <- typeConstraints (m `M.union` mass) val
399 return ((TypeConstraint n1 (TUnknown ret)) : cs1, True, mass)
401typeConstraintsForIfStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> IfStatement -> Check ([TypeConstraint], Bool)
402typeConstraintsForIfStatement m mass ret (IfStatement val thens Nothing) = do
403 (cs1, n1) <- typeConstraints m val
404 (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret thens
405 return ((TypeConstraint n1 Boolean) : cs1 ++ cs2, allCodePathsReturn)
406typeConstraintsForIfStatement m mass ret (IfStatement val thens (Just elses)) = do
407 (cs1, n1) <- typeConstraints m val
408 (cs2, allCodePathsReturn1, _) <- typeConstraintsForBlock m mass ret thens
409 (cs3, allCodePathsReturn2) <- typeConstraintsForElseStatement m mass ret elses
410 return ((TypeConstraint n1 Boolean) : cs1 ++ cs2 ++ cs3, allCodePathsReturn1 && allCodePathsReturn2)
412typeConstraintsForElseStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> ElseStatement -> Check ([TypeConstraint], Bool)
413typeConstraintsForElseStatement m mass ret (Else elses) = do
414 (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret elses
415 return (cs, allCodePathsReturn)
416typeConstraintsForElseStatement m mass ret (ElseIf ifst) = do
417 (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
418 return (cs, allCodePathsReturn)
420typeConstraintsForAssignmentTarget :: M.Map Ident Int -> M.Map Ident Int -> Int -> AssignmentTarget -> Check [TypeConstraint]
421typeConstraintsForAssignmentTarget m mass nval (AssignVariable var) =
422 case M.lookup var mass of
423 Nothing -> throwError $ "No local variable with name " ++ show var
424 Just ty -> do
425 return [TypeConstraint nval (TUnknown ty)]
426typeConstraintsForAssignmentTarget m mass nval (AssignArrayIndex index tgt) = do
427 arr <- fresh
428 (cs1, n1) <- typeConstraints (m `M.union` mass) index
429 cs2 <- typeConstraintsForAssignmentTarget m mass arr tgt
430 return $ (TypeConstraint arr (Array (TUnknown nval))) : (TypeConstraint n1 Number) : cs1 ++ cs2
431typeConstraintsForAssignmentTarget m mass nval (AssignObjectProperty prop tgt) = do
432 obj <- fresh
433 row <- fresh
434 cs <- typeConstraintsForAssignmentTarget m mass obj tgt
435 return $ (TypeConstraint obj (Object (RCons prop (TUnknown nval) $ RUnknown row))) : cs
437typeConstraintsForBlock :: M.Map Ident Int -> M.Map Ident Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, M.Map Ident Int)
438typeConstraintsForBlock _ mass _ [] = return ([], False, mass)
439typeConstraintsForBlock m mass ret (s:ss) = do
440 (cs1, b1, mass1) <- typeConstraintsForStatement (m `M.union` mass) mass ret s
441 case (b1, ss) of
442 (True, []) -> return (cs1, True, mass1)
443 (True, _) -> throwError "Unreachable code"
444 (False, ss) -> do
445 (cs2, b2, mass2) <- typeConstraintsForBlock m mass1 ret ss
446 return (cs1 ++ cs2, b2, mass2)
448solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
449solveTypeConstraints [] s = return s
450solveTypeConstraints all@(TypeConstraint n t:cs) s = do
451 typeOccursCheck n t
452 let s' = let (f, g) = runTypeSolution s
453 in TypeSolution (replaceType n t . f, replaceType n t . g)
454 cs' <- fmap concat $ mapM (substituteTypeInConstraint n t) cs
455 solveTypeConstraints cs' s'
456solveTypeConstraints (RowConstraint n r:cs) s = do
457 rowOccursCheck n r
458 let s' = let (f, g) = runTypeSolution s
459 in TypeSolution $ (replaceRow n r . f, replaceRow n r . g)
460 cs' <- fmap concat $ mapM (substituteRowInConstraint n r) cs
461 solveTypeConstraints cs' s'
463substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
464substituteTypeInConstraint n s (TypeConstraint m t)
465 | n == m = unifyTypes s t
466 | otherwise = return [TypeConstraint m (replaceType n s t)]
467substituteTypeInConstraint n s (RowConstraint m r)
468 = return [RowConstraint m (replaceType n s r)]
470substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
471substituteRowInConstraint n r (TypeConstraint m t)
472 = return [TypeConstraint m (replaceRow n r t)]
473substituteRowInConstraint n r (RowConstraint m r1)
474 | m == n = unifyRows r r1
475 | otherwise = return [RowConstraint m (replaceRow n r r1)]
477unifyTypes :: Type -> Type -> Check [TypeConstraint]
478unifyTypes (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
479unifyTypes (TUnknown u) t = do
480 typeOccursCheck u t
481 return [TypeConstraint u t]
482unifyTypes t (TUnknown u) = do
483 typeOccursCheck u t
484 return [TypeConstraint u t]
485unifyTypes Number Number = return []
486unifyTypes String String = return []
487unifyTypes Boolean Boolean = return []
488unifyTypes (Array s) (Array t) = unifyTypes s t
489unifyTypes (Object row1) (Object row2) = unifyRows row1 row2
490unifyTypes (Function args1 ret1) (Function args2 ret2) = do
491 guardWith "Function applied to incorrect number of args" $ length args1 == length args2
492 cs1 <- fmap concat $ zipWithM unifyTypes args1 args2
493 cs2 <- unifyTypes ret1 ret2
494 return $ cs1 ++ cs2
495unifyTypes (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
496unifyTypes (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = return []
497unifyTypes (TypeVar v1) (TypeVar v2) = return []
498unifyTypes (TypeApp t1 t2) (TypeApp t3 t4) = do
499 cs1 <- unifyTypes t1 t3
500 cs2 <- unifyTypes t2 t4
501 return $ cs1 ++ cs2
502unifyTypes t1 t2 = throwError $ "Cannot unify " ++ show t1 ++ " with " ++ show t2 ++ "."
504unifyRows :: Row -> Row -> Check [TypeConstraint]
505unifyRows r1 r2 =
506 let
507 (s1, r1') = toList r1
508 (s2, r2') = toList r2
509 int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
510 sd1 = [ (name, t1) | (name, t1) <- s1, not (elem name (map fst s2)) ]
511 sd2 = [ (name, t2) | (name, t2) <- s2, not (elem name (map fst s1)) ]
512 in rethrow (\e -> "Cannot unify " ++ show r1 ++ " with " ++ show r2 ++ ": " ++ e) $ do
513 cs1 <- fmap concat $ mapM (uncurry unifyTypes) int
514 cs2 <- unifyRows' sd1 r1' sd2 r2'
515 return $ cs1 ++ cs2
516 where
517 unifyRows' :: [(String, Type)] -> Row -> [(String, Type)] -> Row -> Check [TypeConstraint]
518 unifyRows' [] (RUnknown u) sd r = do
519 rowOccursCheck u r
520 return [RowConstraint u (fromList (sd, r))]
521 unifyRows' sd r [] (RUnknown u) = do
522 rowOccursCheck u r
523 return [RowConstraint u (fromList (sd, r))]
524 unifyRows' ((name, ty):row) r others (RUnknown u) = do
525 u' <- fresh
526 cs <- unifyRows' row r others (RUnknown u')
527 return (RowConstraint u (RCons name ty (RUnknown u')) : cs)
528 unifyRows' [] REmpty [] REmpty = return []
529 unifyRows' sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ show (fromList (sd1, r1)) ++ " with " ++ show (fromList (sd2, r2)) ++ "."
530 toList :: Row -> ([(String, Type)], Row)
531 toList (RCons name ty row) = let (tys, rest) = toList row
532 in ((name, ty):tys, rest)
533 toList r = ([], r)
534 fromList :: ([(String, Type)], Row) -> Row
535 fromList ([], r) = r
536 fromList ((name, t):ts, r) = RCons name t (fromList (ts, r))