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