@@ -1,523 +0,0 @@
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−-----------------------------------------------------------------------------
14−
15−module PureScript.TypeChecker.Types (
16− TypeConstraint(..),
17− TypeSolution(..),
18− typeOf
19−) where
20−
21−import Data.List
22−import Data.Function
23−import Data.Data (Data(..))
24−import Data.Generics (everywhere, everywhereM, everything, mkT, mkM, mkQ, extM, extQ)
25−
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−
34−import Control.Monad.State
35−import Control.Monad.Error
36−
37−import Control.Applicative
38−import Control.Arrow (Kleisli(..), (***), (&&&))
39−import qualified Control.Category as C
40−
41−import qualified Data.Map as M
42−
43−data TypeConstraint
44− = TypeConstraint Int Type
45− | RowConstraint Int Row deriving Show
46−
47−newtype TypeSolution = TypeSolution { runTypeSolution :: (Int -> Type, Int -> Row) }
48−
49−emptyTypeSolution :: TypeSolution
50−emptyTypeSolution = TypeSolution (TUnknown, RUnknown)
51−
52−typeOf :: Ident -> Value -> Check PolyType
53−typeOf 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
61−
62−allUnknownsBecameQuantified :: [TypeConstraint] -> TypeSolution -> Type -> Check ()
63−allUnknownsBecameQuantified 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
78−
79−findUnknownTypes :: (Data d) => d -> [Int]
80−findUnknownTypes = everything (++) (mkQ [] f)
81− where
82− f :: Type -> [Int]
83− f (TUnknown n) = [n]
84− f _ = []
85−
86−findUnknownRows :: (Data d) => d -> [Int]
87−findUnknownRows = everything (++) (mkQ [] f)
88− where
89− f :: Row -> [Int]
90− f (RUnknown n) = [n]
91− f _ = []
92−
93−varIfUnknown :: Type -> PolyType
94−varIfUnknown 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
120−
121−replaceVarsWithUnknowns :: [String] -> Type -> Check Type
122−replaceVarsWithUnknowns 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
144−
145−replaceType :: (Data d) => Int -> Type -> d -> d
146−replaceType n t = everywhere (mkT go)
147− where
148− go (TUnknown m) | m == n = t
149− go t = t
150−
151−replaceRow :: (Data d) => Int -> Row -> d -> d
152−replaceRow n r = everywhere (mkT go)
153− where
154− go (RUnknown m) | m == n = r
155− go r = r
156−
157−typeOccursCheck :: Int -> Type -> Check ()
158−typeOccursCheck u (TUnknown _) = return ()
159−typeOccursCheck u t = when (occursCheck u t) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ show t
160−
161−rowOccursCheck :: Int -> Row -> Check ()
162−rowOccursCheck u (RUnknown _) = return ()
163−rowOccursCheck u r = when (occursCheck u r) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ show r
164−
165−occursCheck :: (Data d) => Int -> d -> Bool
166−occursCheck 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
172−
173−typeConstraints :: M.Map Ident Int -> Value -> Check ([TypeConstraint], Int)
174−typeConstraints _ (NumericLiteral _) = do
175− me <- fresh
176− return ([TypeConstraint me Number], me)
177−typeConstraints _ (StringLiteral _) = do
178− me <- fresh
179− return ([TypeConstraint me String], me)
180−typeConstraints _ (BooleanLiteral _) = do
181− me <- fresh
182− return ([TypeConstraint me Boolean], me)
183−typeConstraints 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)
188−typeConstraints m (Unary op val) = do
189− (cs, n1) <- typeConstraints m val
190− me <- fresh
191− return (cs ++ unaryOperatorConstraints op n1 me, me)
192−typeConstraints 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)
197−typeConstraints 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)
206−typeConstraints 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)
211−typeConstraints 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)
216−typeConstraints 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)
222−typeConstraints 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)
228−typeConstraints 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)
241−typeConstraints 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)
246−typeConstraints 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)
254−typeConstraints 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)
259−typeConstraints 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)
265−
266−replaceAllTypeSynonyms :: Type -> Check Type
267−replaceAllTypeSynonyms 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'
275−
276−unaryOperatorConstraints :: UnaryOperator -> Int -> Int -> [TypeConstraint]
277−unaryOperatorConstraints Negate val result = [TypeConstraint val Number, TypeConstraint result Number]
278−unaryOperatorConstraints Not val result = [TypeConstraint val Boolean, TypeConstraint result Boolean]
279−unaryOperatorConstraints BitwiseNot val result = [TypeConstraint val Number, TypeConstraint result Number]
280−
281−binaryOperatorConstraints :: BinaryOperator -> Int -> Int -> Int -> [TypeConstraint]
282−binaryOperatorConstraints Add = symBinOpConstraints Number
283−binaryOperatorConstraints Subtract = symBinOpConstraints Number
284−binaryOperatorConstraints Multiply = symBinOpConstraints Number
285−binaryOperatorConstraints Divide = symBinOpConstraints Number
286−binaryOperatorConstraints Modulus = symBinOpConstraints Number
287−binaryOperatorConstraints LessThan = asymBinOpConstraints Number Boolean
288−binaryOperatorConstraints LessThanOrEqualTo = asymBinOpConstraints Number Boolean
289−binaryOperatorConstraints GreaterThan = asymBinOpConstraints Number Boolean
290−binaryOperatorConstraints GreaterThanOrEqualTo = asymBinOpConstraints Number Boolean
291−binaryOperatorConstraints BitwiseAnd = symBinOpConstraints Number
292−binaryOperatorConstraints BitwiseOr = symBinOpConstraints Number
293−binaryOperatorConstraints BitwiseXor = symBinOpConstraints Number
294−binaryOperatorConstraints ShiftLeft = symBinOpConstraints Number
295−binaryOperatorConstraints ShiftRight = symBinOpConstraints Number
296−binaryOperatorConstraints ZeroFillShiftRight = symBinOpConstraints Number
297−binaryOperatorConstraints EqualTo = equalityBinOpConstraints
298−binaryOperatorConstraints NotEqualTo = equalityBinOpConstraints
299−binaryOperatorConstraints And = symBinOpConstraints Boolean
300−binaryOperatorConstraints Or = symBinOpConstraints Boolean
301−binaryOperatorConstraints Concat = symBinOpConstraints String
302−
303−equalityBinOpConstraints :: Int -> Int -> Int -> [TypeConstraint]
304−equalityBinOpConstraints left right result = [TypeConstraint left (TUnknown right), TypeConstraint result Boolean]
305−
306−symBinOpConstraints :: Type -> Int -> Int -> Int -> [TypeConstraint]
307−symBinOpConstraints ty left right result = asymBinOpConstraints ty ty left right result
308−
309−asymBinOpConstraints :: Type -> Type -> Int -> Int -> Int -> [TypeConstraint]
310−asymBinOpConstraints ty res left right result = [TypeConstraint left ty, TypeConstraint right ty, TypeConstraint result res]
311−
312−typeConstraintsForBinder :: Int -> Binder -> Check ([TypeConstraint], M.Map Ident Int)
313−typeConstraintsForBinder val (StringBinder _) = constantBinder val String
314−typeConstraintsForBinder val (NumberBinder _) = constantBinder val Number
315−typeConstraintsForBinder val (BooleanBinder _) = constantBinder val Boolean
316−typeConstraintsForBinder val (VarBinder name) = do
317− me <- fresh
318− return ([TypeConstraint me (TUnknown val)], M.singleton name me)
319−typeConstraintsForBinder 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"
326−typeConstraintsForBinder 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"
336−typeConstraintsForBinder 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)
349−typeConstraintsForBinder 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)
359−
360−constantBinder :: Int -> Type -> Check ([TypeConstraint], M.Map Ident Int)
361−constantBinder val ty = return ([TypeConstraint val ty], M.empty)
362−
363−typeConstraintsForBinders :: M.Map Ident Int -> Int -> Int -> [(Binder, Value)] -> Check [TypeConstraint]
364−typeConstraintsForBinders _ _ _ [] = return []
365−typeConstraintsForBinders 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)
370−
371−typeConstraintsForStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> Statement -> Check ([TypeConstraint], Bool, M.Map Ident Int)
372−typeConstraintsForStatement 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."
378−typeConstraintsForStatement 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)
382−typeConstraintsForStatement 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)
386−typeConstraintsForStatement m mass ret (IfThenElse val thens Nothing) = do
387− (cs1, n1) <- typeConstraints m val
388− (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret thens
389− return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2, allCodePathsReturn, mass)
390−typeConstraintsForStatement m mass ret (IfThenElse val thens (Just elses)) = do
391− (cs1, n1) <- typeConstraints m val
392− (cs2, allCodePathsReturn1, _) <- typeConstraintsForBlock m mass ret thens
393− (cs3, allCodePathsReturn2, _) <- typeConstraintsForBlock m mass ret elses
394− return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2 ++ cs3, allCodePathsReturn1 && allCodePathsReturn2, mass)
395−typeConstraintsForStatement m mass ret (For (init, cond, cont) inner) = do
396− (cs1, b1, mass1) <- typeConstraintsForStatement m mass ret init
397− guardWith "Cannot return from inside for" $ not b1
398− (cs2, n1) <- typeConstraints (m `M.union` mass1) cond
399− (cs3, b2, mass2) <- typeConstraintsForStatement (m `M.union` mass1) mass1 ret cont
400− guardWith "Cannot return from inside for" $ not b2
401− (cs4, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass2) mass2 ret inner
402− return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2 ++ cs3 ++ cs4, allCodePathsReturn, mass)
403−typeConstraintsForStatement m mass ret (Return val) = do
404− (cs1, n1) <- typeConstraints (m `M.union` mass) val
405− return ((TypeConstraint n1 (TUnknown ret)) : cs1, True, mass)
406−
407−typeConstraintsForAssignmentTarget :: M.Map Ident Int -> M.Map Ident Int -> Int -> AssignmentTarget -> Check [TypeConstraint]
408−typeConstraintsForAssignmentTarget m mass nval (AssignVariable var) =
409− case M.lookup var mass of
410− Nothing -> throwError $ "No local variable with name " ++ show var
411− Just ty -> do
412− return [TypeConstraint nval (TUnknown ty)]
413−typeConstraintsForAssignmentTarget m mass nval (AssignArrayIndex index tgt) = do
414− arr <- fresh
415− (cs1, n1) <- typeConstraints (m `M.union` mass) index
416− cs2 <- typeConstraintsForAssignmentTarget m mass arr tgt
417− return $ (TypeConstraint arr (Array (TUnknown nval))) : (TypeConstraint n1 Number) : cs1 ++ cs2
418−typeConstraintsForAssignmentTarget m mass nval (AssignObjectProperty prop tgt) = do
419− obj <- fresh
420− row <- fresh
421− cs <- typeConstraintsForAssignmentTarget m mass obj tgt
422− return $ (TypeConstraint obj (Object (RCons prop (TUnknown nval) $ RUnknown row))) : cs
423−
424−typeConstraintsForBlock :: M.Map Ident Int -> M.Map Ident Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, M.Map Ident Int)
425−typeConstraintsForBlock _ mass _ [] = return ([], False, mass)
426−typeConstraintsForBlock m mass ret (s:ss) = do
427− (cs1, b1, mass1) <- typeConstraintsForStatement (m `M.union` mass) mass ret s
428− case (b1, ss) of
429− (True, []) -> return (cs1, True, mass1)
430− (True, _) -> throwError "Unreachable code"
431− (False, ss) -> do
432− (cs2, b2, mass2) <- typeConstraintsForBlock m mass1 ret ss
433− return (cs1 ++ cs2, b2, mass2)
434−
435−solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
436−solveTypeConstraints [] s = return s
437−solveTypeConstraints all@(TypeConstraint n t:cs) s = do
438− typeOccursCheck n t
439− let s' = let (f, g) = runTypeSolution s
440− in TypeSolution (replaceType n t . f, replaceType n t . g)
441− cs' <- fmap concat $ mapM (substituteTypeInConstraint n t) cs
442− solveTypeConstraints cs' s'
443−solveTypeConstraints (RowConstraint n r:cs) s = do
444− rowOccursCheck n r
445− let s' = let (f, g) = runTypeSolution s
446− in TypeSolution $ (replaceRow n r . f, replaceRow n r . g)
447− cs' <- fmap concat $ mapM (substituteRowInConstraint n r) cs
448− solveTypeConstraints cs' s'
449−
450−substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
451−substituteTypeInConstraint n s (TypeConstraint m t)
452− | n == m = unifyTypes s t
453− | otherwise = return [TypeConstraint m (replaceType n s t)]
454−substituteTypeInConstraint n s (RowConstraint m r)
455− = return [RowConstraint m (replaceType n s r)]
456−
457−substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
458−substituteRowInConstraint n r (TypeConstraint m t)
459− = return [TypeConstraint m (replaceRow n r t)]
460−substituteRowInConstraint n r (RowConstraint m r1)
461− | m == n = unifyRows r r1
462− | otherwise = return [RowConstraint m (replaceRow n r r1)]
463−
464−unifyTypes :: Type -> Type -> Check [TypeConstraint]
465−unifyTypes (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
466−unifyTypes (TUnknown u) t = do
467− typeOccursCheck u t
468− return [TypeConstraint u t]
469−unifyTypes t (TUnknown u) = do
470− typeOccursCheck u t
471− return [TypeConstraint u t]
472−unifyTypes Number Number = return []
473−unifyTypes String String = return []
474−unifyTypes Boolean Boolean = return []
475−unifyTypes (Array s) (Array t) = unifyTypes s t
476−unifyTypes (Object row1) (Object row2) = unifyRows row1 row2
477−unifyTypes (Function args1 ret1) (Function args2 ret2) = do
478− guardWith "Function applied to incorrect number of args" $ length args1 == length args2
479− cs1 <- fmap concat $ zipWithM unifyTypes args1 args2
480− cs2 <- unifyTypes ret1 ret2
481− return $ cs1 ++ cs2
482−unifyTypes (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
483−unifyTypes (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = return []
484−unifyTypes (TypeVar v1) (TypeVar v2) = return []
485−unifyTypes (TypeApp t1 t2) (TypeApp t3 t4) = do
486− cs1 <- unifyTypes t1 t3
487− cs2 <- unifyTypes t2 t4
488− return $ cs1 ++ cs2
489−unifyTypes t1 t2 = throwError $ "Cannot unify " ++ show t1 ++ " with " ++ show t2 ++ "."
490−
491−unifyRows :: Row -> Row -> Check [TypeConstraint]
492−unifyRows r1 r2 =
493− let
494− (s1, r1') = toList r1
495− (s2, r2') = toList r2
496− int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
497− sd1 = [ (name, t1) | (name, t1) <- s1, not (elem name (map fst s2)) ]
498− sd2 = [ (name, t2) | (name, t2) <- s2, not (elem name (map fst s1)) ]
499− in rethrow (\e -> "Cannot unify " ++ show r1 ++ " with " ++ show r2 ++ ": " ++ e) $ do
500− cs1 <- fmap concat $ mapM (uncurry unifyTypes) int
501− cs2 <- unifyRows' sd1 r1' sd2 r2'
502− return $ cs1 ++ cs2
503− where
504− unifyRows' :: [(String, Type)] -> Row -> [(String, Type)] -> Row -> Check [TypeConstraint]
505− unifyRows' [] (RUnknown u) sd r = do
506− rowOccursCheck u r
507− return [RowConstraint u (fromList (sd, r))]
508− unifyRows' sd r [] (RUnknown u) = do
509− rowOccursCheck u r
510− return [RowConstraint u (fromList (sd, r))]
511− unifyRows' ((name, ty):row) r others (RUnknown u) = do
512− u' <- fresh
513− cs <- unifyRows' row r others (RUnknown u')
514− return (RowConstraint u (RCons name ty (RUnknown u')) : cs)
515− unifyRows' [] REmpty [] REmpty = return []
516− unifyRows' sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ show (fromList (sd1, r1)) ++ " with " ++ show (fromList (sd2, r2)) ++ "."
517− toList :: Row -> ([(String, Type)], Row)
518− toList (RCons name ty row) = let (tys, rest) = toList row
519− in ((name, ty):tys, rest)
520− toList r = ([], r)
521− fromList :: ([(String, Type)], Row) -> Row
522− fromList ([], r) = r
523− fromList ((name, t):ts, r) = RCons name t (fromList (ts, r))