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