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