@@ -0,0 +1,523 @@
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
34+import Control.Monad.State
35+import Control.Monad.Error
37+import Control.Applicative
38+import Control.Arrow (Kleisli(..), (***), (&&&))
39+import qualified Control.Category as C
41+import qualified Data.Map as M
44+ = TypeConstraint Int Type
45+ | RowConstraint Int Row deriving Show
47+newtype TypeSolution = TypeSolution { runTypeSolution :: (Int -> Type, Int -> Row) }
49+emptyTypeSolution :: TypeSolution
50+emptyTypeSolution = TypeSolution (TUnknown, RUnknown)
52+typeOf :: Ident -> Value -> Check PolyType
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
62+allUnknownsBecameQuantified :: [TypeConstraint] -> TypeSolution -> Type -> Check ()
63+allUnknownsBecameQuantified cs solution ty = do
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
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
79+findUnknownTypes :: (Data d) => d -> [Int]
80+findUnknownTypes = everything (++) (mkQ [] f)
86+findUnknownRows :: (Data d) => d -> [Int]
87+findUnknownRows = everything (++) (mkQ [] f)
93+varIfUnknown :: Type -> PolyType
96+ (ty', m) = flip runState M.empty $ everywhereM (flip extM g $ mkM f) ty
98+ PolyType (sort $ nub $ M.elems m) ty'
100+ f :: Type -> State (M.Map Int String) Type
103+ case M.lookup n m of
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
110+ g :: Row -> State (M.Map Int String) Row
113+ case M.lookup n m of
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
121+replaceVarsWithUnknowns :: [String] -> Type -> Check Type
122+replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)
124+ f :: Type -> StateT (M.Map String Int) Check Type
125+ f (TypeVar var) | var `elem` idents = do
128+ case M.lookup var m of
130+ put (M.insert var n m)
132+ Just u -> return $ TUnknown u
134+ g :: Row -> StateT (M.Map String Int) Check Row
135+ g (RowVar var) | var `elem` idents = do
138+ case M.lookup var m of
140+ put (M.insert var n m)
142+ Just u -> return $ RUnknown u
145+replaceType :: (Data d) => Int -> Type -> d -> d
146+replaceType n t = everywhere (mkT go)
148+ go (TUnknown m) | m == n = t
151+replaceRow :: (Data d) => Int -> Row -> d -> d
152+replaceRow n r = everywhere (mkT go)
154+ go (RUnknown m) | m == n = r
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
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
165+occursCheck :: (Data d) => Int -> d -> Bool
166+occursCheck u = everything (||) $ flip extQ g $ mkQ False f
168+ f (TUnknown u') | u' == u = True
170+ g (RUnknown u') | u' == u = True
173+typeConstraints :: M.Map Ident Int -> Value -> Check ([TypeConstraint], Int)
174+typeConstraints _ (NumericLiteral _) = do
176+ return ([TypeConstraint me Number], me)
177+typeConstraints _ (StringLiteral _) = do
179+ return ([TypeConstraint me String], me)
180+typeConstraints _ (BooleanLiteral _) = do
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
187+ return (cs ++ map (TypeConstraint me . Array . TUnknown) ns, me)
188+typeConstraints m (Unary op val) = do
189+ (cs, n1) <- typeConstraints m val
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
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
201+ let tys = zipWith (\(name, _) u -> (name, TUnknown u)) ps ns
202+ return ((TypeConstraint me (Object (typesToRow tys))) : cs, me)
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
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
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
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
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
232+ case M.lookup var (names env) of
233+ Nothing -> throwError $ show var ++ " is undefined"
234+ Just (PolyType idents ty, _) -> do
236+ replaced <- replaceVarsWithUnknowns idents ty
237+ return ([TypeConstraint me replaced], me)
240+ return ([TypeConstraint u (TUnknown me)], me)
241+typeConstraints m (Block ss) = do
243+ (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m M.empty ret ss
244+ guardWith "Block is missing a return statement" allCodePathsReturn
246+typeConstraints m (Constructor c) = do
248+ case M.lookup c (dataConstructors env) of
249+ Nothing -> throwError $ "Constructor " ++ c ++ " is undefined"
250+ Just (PolyType idents ty) -> do
252+ replaced <- replaceVarsWithUnknowns idents ty
253+ return ([TypeConstraint me replaced], me)
254+typeConstraints m (Case val binders) = do
255+ (cs1, n1) <- typeConstraints m val
257+ cs2 <- typeConstraintsForBinders m n1 ret binders
258+ return (cs1 ++ cs2, ret)
259+typeConstraints m (TypedValue val poly@(PolyType idents ty)) = do
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)
266+replaceAllTypeSynonyms :: Type -> Check Type
267+replaceAllTypeSynonyms ty = do
269+ go (M.toList $ typeSynonyms env) ty
271+ go [] ty = return ty
272+ go ((name, (args, repl)):rest) ty = do
273+ ty' <- either throwError return (substituteTypeSynonym name args repl ty)
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]
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
303+equalityBinOpConstraints :: Int -> Int -> Int -> [TypeConstraint]
304+equalityBinOpConstraints left right result = [TypeConstraint left (TUnknown right), TypeConstraint result Boolean]
306+symBinOpConstraints :: Type -> Int -> Int -> Int -> [TypeConstraint]
307+symBinOpConstraints ty left right result = asymBinOpConstraints ty ty left right result
309+asymBinOpConstraints :: Type -> Type -> Int -> Int -> Int -> [TypeConstraint]
310+asymBinOpConstraints ty res left right result = [TypeConstraint left ty, TypeConstraint right ty, TypeConstraint result res]
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
318+ return ([TypeConstraint me (TUnknown val)], M.singleton name me)
319+typeConstraintsForBinder val (NullaryBinder ctor) = do
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
328+ case M.lookup ctor (dataConstructors env) of
329+ Just (PolyType idents f@(Function [_] _)) -> do
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
339+ (cs, m1) <- typeConstraintsForProperties row (RUnknown rest) props
340+ return ((TypeConstraint val (Object (RUnknown row))) : cs, m1)
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
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
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))
355+ Nothing -> return (arrayConstraint : cs1, m1)
357+ (cs2, m2) <- typeConstraintsForBinder val binder
358+ return (arrayConstraint : cs1 ++ cs2, M.union m1 m2)
360+constantBinder :: Int -> Type -> Check ([TypeConstraint], M.Map Ident Int)
361+constantBinder val ty = return ([TypeConstraint val ty], M.empty)
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)
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
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)
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
412+ return [TypeConstraint nval (TUnknown ty)]
413+typeConstraintsForAssignmentTarget m mass nval (AssignArrayIndex index tgt) = do
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
421+ cs <- typeConstraintsForAssignmentTarget m mass obj tgt
422+ return $ (TypeConstraint obj (Object (RCons prop (TUnknown nval) $ RUnknown row))) : cs
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
429+ (True, []) -> return (cs1, True, mass1)
430+ (True, _) -> throwError "Unreachable code"
432+ (cs2, b2, mass2) <- typeConstraintsForBlock m mass1 ret ss
433+ return (cs1 ++ cs2, b2, mass2)
435+solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
436+solveTypeConstraints [] s = return s
437+solveTypeConstraints all@(TypeConstraint n t:cs) s = do
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
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'
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)]
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)]
464+unifyTypes :: Type -> Type -> Check [TypeConstraint]
465+unifyTypes (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
466+unifyTypes (TUnknown u) t = do
468+ return [TypeConstraint u t]
469+unifyTypes t (TUnknown u) = do
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
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
489+unifyTypes t1 t2 = throwError $ "Cannot unify " ++ show t1 ++ " with " ++ show t2 ++ "."
491+unifyRows :: Row -> Row -> Check [TypeConstraint]
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'
504+ unifyRows' :: [(String, Type)] -> Row -> [(String, Type)] -> Row -> Check [TypeConstraint]
505+ unifyRows' [] (RUnknown u) sd r = do
507+ return [RowConstraint u (fromList (sd, r))]
508+ unifyRows' sd r [] (RUnknown u) = do
510+ return [RowConstraint u (fromList (sd, r))]
511+ unifyRows' ((name, ty):row) r others (RUnknown u) = do
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)
521+ fromList :: ([(String, Type)], Row) -> Row
522+ fromList ([], r) = r
523+ fromList ((name, t):ts, r) = RCons name t (fromList (ts, r))