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