@@ -0,0 +1,573 @@
1+-----------------------------------------------------------------------------
3+-- Module : PureScript.TypeChecker.Types
4+-- Copyright : (c) Phil Freeman 2013
7+-- Maintainer : Phil Freeman <paf31@cantab.net>
8+-- Stability : experimental
13+-----------------------------------------------------------------------------
15+module PureScript.TypeChecker.Types (
23+import Data.Data (Data(..))
24+import Data.Generics (everywhere, everywhereM, everything, mkT, mkM, mkQ, extM, extQ)
26+import PureScript.Values
27+import PureScript.Types
28+import PureScript.Kinds
29+import PureScript.Names
30+import PureScript.TypeChecker.Monad
31+import PureScript.TypeChecker.Kinds
32+import PureScript.TypeChecker.Synonyms
33+import PureScript.CodeGen.Pretty.Types
34+import PureScript.CodeGen.Pretty.Kinds
36+import Control.Monad.State
37+import Control.Monad.Error
39+import Control.Applicative
40+import Control.Arrow (Kleisli(..), (***), (&&&))
41+import qualified Control.Category as C
43+import qualified Data.Map as M
46+ = TypeConstraint Int Type
47+ | RowConstraint Int Row deriving Show
49+newtype TypeSolution = TypeSolution { runTypeSolution :: (Int -> Type, Int -> Row) }
51+emptyTypeSolution :: TypeSolution
52+emptyTypeSolution = TypeSolution (TUnknown, RUnknown)
54+typeOf :: Ident -> Value -> Check PolyType
56+ (cs, n) <- case val of
59+ (cs, n) <- typeConstraints (M.singleton name me) val
60+ return (TypeConstraint me (TUnknown n) : cs, n)
61+ _ -> typeConstraints M.empty val
62+ solution <- solveTypeConstraints cs emptyTypeSolution
63+ let ty = fst (runTypeSolution solution) n
64+ allUnknownsBecameQuantified cs solution ty
65+ return $ varIfUnknown ty
67+allUnknownsBecameQuantified :: [TypeConstraint] -> TypeSolution -> Type -> Check ()
68+allUnknownsBecameQuantified cs solution ty = do
70+ typesMentioned = findUnknownTypes ty
71+ unknownTypes = nub $ flip concatMap cs $ \c -> case c of
72+ TypeConstraint u t -> u : findUnknownTypes t
73+ RowConstraint _ r -> findUnknownTypes r
74+ unsolvedTypes = filter (\n -> TUnknown n == fst (runTypeSolution solution) n) unknownTypes
75+ guardWith "Unsolved type variable" $ null $ unsolvedTypes \\ typesMentioned
77+ rowsMentioned = findUnknownRows ty
78+ unknownRows = nub $ flip concatMap cs $ \c -> case c of
79+ TypeConstraint _ t -> findUnknownRows t
80+ RowConstraint u r -> u : findUnknownRows r
81+ unsolvedRows = filter (\n -> RUnknown n == snd (runTypeSolution solution) n) unknownRows
82+ guardWith "Unsolved row variable" $ null $ unsolvedRows \\ rowsMentioned
84+findUnknownTypes :: (Data d) => d -> [Int]
85+findUnknownTypes = everything (++) (mkQ [] f)
91+findTypeVars :: (Data d) => d -> [String]
92+findTypeVars = everything (++) (mkQ [] f)
94+ f :: Type -> [String]
98+findUnknownRows :: (Data d) => d -> [Int]
99+findUnknownRows = everything (++) (mkQ [] f)
102+ f (RUnknown n) = [n]
105+varIfUnknown :: Type -> PolyType
108+ (ty', m) = flip runState M.empty $ everywhereM (flip extM g $ mkM f) ty
110+ PolyType (sort $ nub $ M.elems m ++ findTypeVars ty) ty'
112+ f :: Type -> State (M.Map Int String) Type
115+ case M.lookup n m of
117+ let name = "t" ++ show (M.size m)
118+ put $ M.insert n name m
119+ return $ TypeVar name
120+ Just name -> return $ TypeVar name
122+ g :: Row -> State (M.Map Int String) Row
125+ case M.lookup n m of
127+ let name = "r" ++ show (M.size m)
128+ put $ M.insert n name m
129+ return $ RowVar name
130+ Just name -> return $ RowVar name
133+replaceVarsWithUnknowns :: [String] -> Type -> Check Type
134+replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)
136+ f :: Type -> StateT (M.Map String Int) Check Type
137+ f (TypeVar var) | var `elem` idents = do
140+ case M.lookup var m of
142+ put (M.insert var n m)
144+ Just u -> return $ TUnknown u
146+ g :: Row -> StateT (M.Map String Int) Check Row
147+ g (RowVar var) | var `elem` idents = do
150+ case M.lookup var m of
152+ put (M.insert var n m)
154+ Just u -> return $ RUnknown u
157+replaceType :: (Data d) => Int -> Type -> d -> d
158+replaceType n t = everywhere (mkT go)
160+ go (TUnknown m) | m == n = t
163+replaceRow :: (Data d) => Int -> Row -> d -> d
164+replaceRow n r = everywhere (mkT go)
166+ go (RUnknown m) | m == n = r
169+typeOccursCheck :: Int -> Type -> Check ()
170+typeOccursCheck u (TUnknown _) = return ()
171+typeOccursCheck u t = when (occursCheck u t) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintType t
173+rowOccursCheck :: Int -> Row -> Check ()
174+rowOccursCheck u (RUnknown _) = return ()
175+rowOccursCheck u r = when (occursCheck u r) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintRow r
177+occursCheck :: (Data d) => Int -> d -> Bool
178+occursCheck u = everything (||) $ flip extQ g $ mkQ False f
180+ f (TUnknown u') | u' == u = True
182+ g (RUnknown u') | u' == u = True
185+typeConstraints :: M.Map Ident Int -> Value -> Check ([TypeConstraint], Int)
186+typeConstraints _ (NumericLiteral _) = do
188+ return ([TypeConstraint me Number], me)
189+typeConstraints _ (StringLiteral _) = do
191+ return ([TypeConstraint me String], me)
192+typeConstraints _ (BooleanLiteral _) = do
194+ return ([TypeConstraint me Boolean], me)
195+typeConstraints m (ArrayLiteral vals) = do
196+ all <- mapM (typeConstraints m) vals
197+ let (cs, ns) = (concat . map fst &&& map snd) all
199+ return (cs ++ map (TypeConstraint me . Array . TUnknown) ns, me)
200+typeConstraints m (Unary op val) = do
201+ (cs, n1) <- typeConstraints m val
203+ return (cs ++ unaryOperatorConstraints op n1 me, me)
204+typeConstraints m (Binary op left right) = do
205+ (cs1, n1) <- typeConstraints m left
206+ (cs2, n2) <- typeConstraints m right
208+ return (cs1 ++ cs2 ++ binaryOperatorConstraints op n1 n2 me, me)
209+typeConstraints m (ObjectLiteral ps) = do
210+ all <- mapM (typeConstraints m . snd) ps
211+ let (cs, ns) = (concat . map fst &&& map snd) all
213+ let tys = zipWith (\(name, _) u -> (name, TUnknown u)) ps ns
214+ return ((TypeConstraint me (Object (typesToRow tys))) : cs, me)
216+ typesToRow [] = REmpty
217+ typesToRow ((name, ty):tys) = RCons name ty (typesToRow tys)
218+typeConstraints m (Indexer index val) = do
219+ (cs1, n1) <- typeConstraints m index
220+ (cs2, n2) <- typeConstraints m val
222+ return ((TypeConstraint n1 Number) : (TypeConstraint n2 (Array (TUnknown me))) : cs1 ++ cs2, me)
223+typeConstraints m (Accessor prop val) = do
224+ (cs, n1) <- typeConstraints m val
227+ return ((TypeConstraint n1 (Object (RCons prop (TUnknown me) (RUnknown rest)))) : cs, me)
228+typeConstraints m (Abs args ret) = do
229+ ns <- replicateM (length args) fresh
230+ let m' = m `M.union` M.fromList (zipWith (,) args ns)
231+ (cs, n') <- typeConstraints m' ret
233+ return ((TypeConstraint me (Function (map TUnknown ns) (TUnknown n'))) : cs, me)
234+typeConstraints m (App f xs) = do
235+ (cs1, n1) <- typeConstraints m f
236+ all <- mapM (typeConstraints m) xs
237+ let (cs2, ns) = (concat . map fst &&& map snd) all
239+ return ((TypeConstraint n1 (Function (map TUnknown ns) (TUnknown me))) : cs1 ++ cs2, me)
240+typeConstraints m (Var var) =
241+ case M.lookup var m of
244+ case M.lookup var (names env) of
245+ Nothing -> throwError $ show var ++ " is undefined"
246+ Just (PolyType idents ty, _) -> do
248+ replaced <- replaceVarsWithUnknowns idents ty
249+ return ([TypeConstraint me replaced], me)
252+ return ([TypeConstraint u (TUnknown me)], me)
253+typeConstraints m (Block ss) = do
255+ (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m M.empty ret ss
256+ guardWith "Block is missing a return statement" allCodePathsReturn
258+typeConstraints m (Constructor c) = do
260+ case M.lookup c (dataConstructors env) of
261+ Nothing -> throwError $ "Constructor " ++ c ++ " is undefined"
262+ Just (PolyType idents ty) -> do
264+ replaced <- replaceVarsWithUnknowns idents ty
265+ return ([TypeConstraint me replaced], me)
266+typeConstraints m (Case val binders) = do
267+ (cs1, n1) <- typeConstraints m val
269+ cs2 <- typeConstraintsForBinders m n1 ret binders
270+ return (cs1 ++ cs2, ret)
271+typeConstraints m (IfThenElse cond th el) = do
272+ (cs1, n1) <- typeConstraints m cond
273+ (cs2, n2) <- typeConstraints m th
274+ (cs3, n3) <- typeConstraints m el
275+ return (TypeConstraint n1 Boolean : TypeConstraint n2 (TUnknown n3) : cs1 ++ cs2 ++ cs3, n2)
276+typeConstraints m (TypedValue val poly@(PolyType idents ty)) = do
278+ guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
279+ desugared <- replaceAllTypeSynonyms ty
280+ (cs, n1) <- typeConstraints m val
281+ return (TypeConstraint n1 desugared : cs, n1)
283+replaceAllTypeSynonyms :: Type -> Check Type
284+replaceAllTypeSynonyms ty = do
286+ go (M.toList $ typeSynonyms env) ty
288+ go [] ty = return ty
289+ go ((name, (args, repl)):rest) ty = do
290+ ty' <- either throwError return (substituteTypeSynonym name args repl ty)
293+unaryOperatorConstraints :: UnaryOperator -> Int -> Int -> [TypeConstraint]
294+unaryOperatorConstraints Negate val result = [TypeConstraint val Number, TypeConstraint result Number]
295+unaryOperatorConstraints Not val result = [TypeConstraint val Boolean, TypeConstraint result Boolean]
296+unaryOperatorConstraints BitwiseNot val result = [TypeConstraint val Number, TypeConstraint result Number]
298+binaryOperatorConstraints :: BinaryOperator -> Int -> Int -> Int -> [TypeConstraint]
299+binaryOperatorConstraints Add = symBinOpConstraints Number
300+binaryOperatorConstraints Subtract = symBinOpConstraints Number
301+binaryOperatorConstraints Multiply = symBinOpConstraints Number
302+binaryOperatorConstraints Divide = symBinOpConstraints Number
303+binaryOperatorConstraints Modulus = symBinOpConstraints Number
304+binaryOperatorConstraints LessThan = asymBinOpConstraints Number Boolean
305+binaryOperatorConstraints LessThanOrEqualTo = asymBinOpConstraints Number Boolean
306+binaryOperatorConstraints GreaterThan = asymBinOpConstraints Number Boolean
307+binaryOperatorConstraints GreaterThanOrEqualTo = asymBinOpConstraints Number Boolean
308+binaryOperatorConstraints BitwiseAnd = symBinOpConstraints Number
309+binaryOperatorConstraints BitwiseOr = symBinOpConstraints Number
310+binaryOperatorConstraints BitwiseXor = symBinOpConstraints Number
311+binaryOperatorConstraints ShiftLeft = symBinOpConstraints Number
312+binaryOperatorConstraints ShiftRight = symBinOpConstraints Number
313+binaryOperatorConstraints ZeroFillShiftRight = symBinOpConstraints Number
314+binaryOperatorConstraints EqualTo = equalityBinOpConstraints
315+binaryOperatorConstraints NotEqualTo = equalityBinOpConstraints
316+binaryOperatorConstraints And = symBinOpConstraints Boolean
317+binaryOperatorConstraints Or = symBinOpConstraints Boolean
318+binaryOperatorConstraints Concat = symBinOpConstraints String
320+equalityBinOpConstraints :: Int -> Int -> Int -> [TypeConstraint]
321+equalityBinOpConstraints left right result = [TypeConstraint left (TUnknown right), TypeConstraint result Boolean]
323+symBinOpConstraints :: Type -> Int -> Int -> Int -> [TypeConstraint]
324+symBinOpConstraints ty left right result = asymBinOpConstraints ty ty left right result
326+asymBinOpConstraints :: Type -> Type -> Int -> Int -> Int -> [TypeConstraint]
327+asymBinOpConstraints ty res left right result = [TypeConstraint left ty, TypeConstraint right ty, TypeConstraint result res]
329+typeConstraintsForBinder :: Int -> Binder -> Check ([TypeConstraint], M.Map Ident Int)
330+typeConstraintsForBinder _ NullBinder = return ([], M.empty)
331+typeConstraintsForBinder val (StringBinder _) = constantBinder val String
332+typeConstraintsForBinder val (NumberBinder _) = constantBinder val Number
333+typeConstraintsForBinder val (BooleanBinder _) = constantBinder val Boolean
334+typeConstraintsForBinder val (VarBinder name) = do
336+ return ([TypeConstraint me (TUnknown val)], M.singleton name me)
337+typeConstraintsForBinder val (NullaryBinder ctor) = do
339+ case M.lookup ctor (dataConstructors env) of
340+ Just (PolyType args ret) -> do
341+ ret' <- replaceVarsWithUnknowns args ret
342+ return ([TypeConstraint val ret'], M.empty)
343+ _ -> throwError $ "Constructor " ++ ctor ++ " is not defined"
344+typeConstraintsForBinder val (UnaryBinder ctor binder) = do
346+ case M.lookup ctor (dataConstructors env) of
347+ Just (PolyType idents f@(Function [_] _)) -> do
349+ (Function [ty] ret) <- replaceVarsWithUnknowns idents f
350+ (cs, m1) <- typeConstraintsForBinder obj binder
351+ return ((TypeConstraint val ret) : (TypeConstraint obj ty) : cs, m1)
352+ Just _ -> throwError $ ctor ++ " is not a unary constructor"
353+ _ -> throwError $ "Constructor " ++ ctor ++ " is not defined"
354+typeConstraintsForBinder val (ObjectBinder props) = do
357+ (cs, m1) <- typeConstraintsForProperties row (RUnknown rest) props
358+ return ((TypeConstraint val (Object (RUnknown row))) : cs, m1)
360+ typeConstraintsForProperties :: Int -> Row -> [(String, Binder)] -> Check ([TypeConstraint], M.Map Ident Int)
361+ typeConstraintsForProperties nrow row [] = return ([RowConstraint nrow row], M.empty)
362+ typeConstraintsForProperties nrow row ((name, binder):binders) = do
364+ (cs1, m1) <- typeConstraintsForBinder propTy binder
365+ (cs2, m2) <- typeConstraintsForProperties nrow (RCons name (TUnknown propTy) row) binders
366+ return (cs1 ++ cs2, M.union m1 m2)
367+typeConstraintsForBinder val (ArrayBinder binders rest) = do
369+ all <- mapM (typeConstraintsForBinder el) binders
370+ let (cs1, m1) = (concat . map fst &&& M.unions . map snd) all
371+ let arrayConstraint = TypeConstraint val (Array (TUnknown el))
373+ Nothing -> return (arrayConstraint : cs1, m1)
375+ (cs2, m2) <- typeConstraintsForBinder val binder
376+ return (arrayConstraint : cs1 ++ cs2, M.union m1 m2)
377+typeConstraintsForBinder val (NamedBinder name binder) = do
379+ (cs, m) <- typeConstraintsForBinder val binder
380+ return (TypeConstraint me (TUnknown val) : cs, M.insert name me m)
381+typeConstraintsForBinder val (GuardedBinder cond binder) = do
382+ (cs1, m) <- typeConstraintsForBinder val binder
383+ (cs2, n) <- typeConstraints m cond
384+ return (TypeConstraint n Boolean : cs1 ++ cs2, m)
386+constantBinder :: Int -> Type -> Check ([TypeConstraint], M.Map Ident Int)
387+constantBinder val ty = return ([TypeConstraint val ty], M.empty)
389+typeConstraintsForBinders :: M.Map Ident Int -> Int -> Int -> [(Binder, Value)] -> Check [TypeConstraint]
390+typeConstraintsForBinders _ _ _ [] = return []
391+typeConstraintsForBinders m nval ret ((binder, val):bs) = do
392+ (cs1, m1) <- typeConstraintsForBinder nval binder
393+ (cs2, n2) <- typeConstraints (M.union m m1) val
394+ cs3 <- typeConstraintsForBinders m nval ret bs
395+ return ((TypeConstraint n2 (TUnknown ret)) : cs1 ++ cs2 ++ cs3)
397+assignVariable :: Ident -> M.Map Ident Int -> Check ()
398+assignVariable name m =
399+ case M.lookup name m of
400+ Nothing -> return ()
401+ Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."
403+typeConstraintsForStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> Statement -> Check ([TypeConstraint], Bool, M.Map Ident Int)
404+typeConstraintsForStatement m mass ret (VariableIntroduction name val) = do
405+ assignVariable name (m `M.union` mass)
406+ (cs1, n1) <- typeConstraints m val
407+ return $ (cs1, False, M.insert name n1 mass)
408+typeConstraintsForStatement m mass ret (Assignment tgt val) = do
409+ (cs1, n1) <- typeConstraints m val
410+ cs2 <- typeConstraintsForAssignmentTarget m mass n1 tgt
411+ return (cs1 ++ cs2, False, mass)
412+typeConstraintsForStatement m mass ret (While val inner) = do
413+ (cs1, n1) <- typeConstraints m val
414+ (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret inner
415+ return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2, allCodePathsReturn, mass)
416+typeConstraintsForStatement m mass ret (If ifst) = do
417+ (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
418+ return $ (cs, allCodePathsReturn, mass)
419+typeConstraintsForStatement m mass ret (For ident start end inner) = do
420+ assignVariable ident (m `M.union` mass)
421+ (cs1, n1) <- typeConstraints (m `M.union` mass) start
422+ (cs2, n2) <- typeConstraints (m `M.union` mass) end
423+ let mass1 = M.insert ident n1 mass
424+ (cs3, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass1) mass1 ret inner
425+ return $ ((TypeConstraint n1 Number) : (TypeConstraint n2 Number) : cs1 ++ cs2 ++ cs3, allCodePathsReturn, mass)
426+typeConstraintsForStatement m mass ret (ForEach ident vals inner) = do
427+ assignVariable ident (m `M.union` mass)
429+ (cs1, n1) <- typeConstraints (m `M.union` mass) vals
430+ let mass1 = M.insert ident val mass
431+ (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass1) mass1 ret inner
432+ guardWith "Cannot return from within a foreach block" $ not allCodePathsReturn
433+ return $ ((TypeConstraint n1 (Array (TUnknown val))) : cs1 ++ cs2, False, mass)
434+typeConstraintsForStatement m mass ret (Return val) = do
435+ (cs1, n1) <- typeConstraints (m `M.union` mass) val
436+ return ((TypeConstraint n1 (TUnknown ret)) : cs1, True, mass)
438+typeConstraintsForIfStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> IfStatement -> Check ([TypeConstraint], Bool)
439+typeConstraintsForIfStatement m mass ret (IfStatement val thens Nothing) = do
440+ (cs1, n1) <- typeConstraints m val
441+ (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret thens
442+ return ((TypeConstraint n1 Boolean) : cs1 ++ cs2, allCodePathsReturn)
443+typeConstraintsForIfStatement m mass ret (IfStatement val thens (Just elses)) = do
444+ (cs1, n1) <- typeConstraints m val
445+ (cs2, allCodePathsReturn1, _) <- typeConstraintsForBlock m mass ret thens
446+ (cs3, allCodePathsReturn2) <- typeConstraintsForElseStatement m mass ret elses
447+ return ((TypeConstraint n1 Boolean) : cs1 ++ cs2 ++ cs3, allCodePathsReturn1 && allCodePathsReturn2)
449+typeConstraintsForElseStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> ElseStatement -> Check ([TypeConstraint], Bool)
450+typeConstraintsForElseStatement m mass ret (Else elses) = do
451+ (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret elses
452+ return (cs, allCodePathsReturn)
453+typeConstraintsForElseStatement m mass ret (ElseIf ifst) = do
454+ (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
455+ return (cs, allCodePathsReturn)
457+typeConstraintsForAssignmentTarget :: M.Map Ident Int -> M.Map Ident Int -> Int -> AssignmentTarget -> Check [TypeConstraint]
458+typeConstraintsForAssignmentTarget m mass nval (AssignVariable var) =
459+ case M.lookup var mass of
460+ Nothing -> throwError $ "No local variable with name " ++ show var
462+ return [TypeConstraint nval (TUnknown ty)]
463+typeConstraintsForAssignmentTarget m mass nval (AssignArrayIndex index tgt) = do
465+ (cs1, n1) <- typeConstraints (m `M.union` mass) index
466+ cs2 <- typeConstraintsForAssignmentTarget m mass arr tgt
467+ return $ (TypeConstraint arr (Array (TUnknown nval))) : (TypeConstraint n1 Number) : cs1 ++ cs2
468+typeConstraintsForAssignmentTarget m mass nval (AssignObjectProperty prop tgt) = do
471+ cs <- typeConstraintsForAssignmentTarget m mass obj tgt
472+ return $ (TypeConstraint obj (Object (RCons prop (TUnknown nval) $ RUnknown row))) : cs
474+typeConstraintsForBlock :: M.Map Ident Int -> M.Map Ident Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, M.Map Ident Int)
475+typeConstraintsForBlock _ mass _ [] = return ([], False, mass)
476+typeConstraintsForBlock m mass ret (s:ss) = do
477+ (cs1, b1, mass1) <- typeConstraintsForStatement (m `M.union` mass) mass ret s
479+ (True, []) -> return (cs1, True, mass1)
480+ (True, _) -> throwError "Unreachable code"
482+ (cs2, b2, mass2) <- typeConstraintsForBlock m mass1 ret ss
483+ return (cs1 ++ cs2, b2, mass2)
485+solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
486+solveTypeConstraints [] s = return s
487+solveTypeConstraints all@(TypeConstraint n t:cs) s = do
489+ let s' = let (f, g) = runTypeSolution s
490+ in TypeSolution (replaceType n t . f, replaceType n t . g)
491+ cs' <- fmap concat $ mapM (substituteTypeInConstraint n t) cs
492+ solveTypeConstraints cs' s'
493+solveTypeConstraints (RowConstraint n r:cs) s = do
495+ let s' = let (f, g) = runTypeSolution s
496+ in TypeSolution $ (replaceRow n r . f, replaceRow n r . g)
497+ cs' <- fmap concat $ mapM (substituteRowInConstraint n r) cs
498+ solveTypeConstraints cs' s'
500+substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
501+substituteTypeInConstraint n s (TypeConstraint m t)
502+ | n == m = unifyTypes s t
503+ | otherwise = return [TypeConstraint m (replaceType n s t)]
504+substituteTypeInConstraint n s (RowConstraint m r)
505+ = return [RowConstraint m (replaceType n s r)]
507+substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
508+substituteRowInConstraint n r (TypeConstraint m t)
509+ = return [TypeConstraint m (replaceRow n r t)]
510+substituteRowInConstraint n r (RowConstraint m r1)
511+ | m == n = unifyRows r r1
512+ | otherwise = return [RowConstraint m (replaceRow n r r1)]
514+unifyTypes :: Type -> Type -> Check [TypeConstraint]
515+unifyTypes (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
516+unifyTypes (TUnknown u) t = do
518+ return [TypeConstraint u t]
519+unifyTypes t (TUnknown u) = do
521+ return [TypeConstraint u t]
522+unifyTypes Number Number = return []
523+unifyTypes String String = return []
524+unifyTypes Boolean Boolean = return []
525+unifyTypes (Array s) (Array t) = unifyTypes s t
526+unifyTypes (Object row1) (Object row2) = unifyRows row1 row2
527+unifyTypes (Function args1 ret1) (Function args2 ret2) = do
528+ guardWith "Function applied to incorrect number of args" $ length args1 == length args2
529+ cs1 <- fmap concat $ zipWithM unifyTypes args1 args2
530+ cs2 <- unifyTypes ret1 ret2
532+unifyTypes (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
533+unifyTypes (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = return []
534+unifyTypes (TypeVar v1) (TypeVar v2) = return []
535+unifyTypes (TypeApp t1 t2) (TypeApp t3 t4) = do
536+ cs1 <- unifyTypes t1 t3
537+ cs2 <- unifyTypes t2 t4
539+unifyTypes t1 t2 = throwError $ "Cannot unify " ++ prettyPrintType t1 ++ " with " ++ prettyPrintType t2 ++ "."
541+unifyRows :: Row -> Row -> Check [TypeConstraint]
544+ (s1, r1') = toList r1
545+ (s2, r2') = toList r2
546+ int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
547+ sd1 = [ (name, t1) | (name, t1) <- s1, not (elem name (map fst s2)) ]
548+ sd2 = [ (name, t2) | (name, t2) <- s2, not (elem name (map fst s1)) ]
549+ in rethrow (\e -> "Cannot unify " ++ prettyPrintRow r1 ++ " with " ++ prettyPrintRow r2 ++ ": " ++ e) $ do
550+ cs1 <- fmap concat $ mapM (uncurry unifyTypes) int
551+ cs2 <- unifyRows' sd1 r1' sd2 r2'
554+ unifyRows' :: [(String, Type)] -> Row -> [(String, Type)] -> Row -> Check [TypeConstraint]
555+ unifyRows' [] (RUnknown u) sd r = do
557+ return [RowConstraint u (fromList (sd, r))]
558+ unifyRows' sd r [] (RUnknown u) = do
560+ return [RowConstraint u (fromList (sd, r))]
561+ unifyRows' ((name, ty):row) r others (RUnknown u) = do
563+ cs <- unifyRows' row r others (RUnknown u')
564+ return (RowConstraint u (RCons name ty (RUnknown u')) : cs)
565+ unifyRows' [] REmpty [] REmpty = return []
566+ unifyRows' sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ prettyPrintRow (fromList (sd1, r1)) ++ " with " ++ prettyPrintRow (fromList (sd2, r2)) ++ "."
567+ toList :: Row -> ([(String, Type)], Row)
568+ toList (RCons name ty row) = let (tys, rest) = toList row
569+ in ((name, ty):tys, rest)
571+ fromList :: ([(String, Type)], Row) -> Row
572+ fromList ([], r) = r
573+ fromList ((name, t):ts, r) = RCons name t (fromList (ts, r))