git.iko.soy/rowtype-yoga/purescript-native
on f96c9a1 help sign in
rowtype-yoga/purescript-native/src/PureScript/TypeChecker/Types.hs
485 lines 21 kB history raw
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-----------------------------------------------------------------------------
15module PureScript.TypeChecker.Types (
16 TypeConstraint(..),
17 TypeSolution(..),
18 typeOf
19) where
21import Data.List
22import Data.Function
23import Data.Data (Data(..))
24import Data.Generics (everywhere, everywhereM, everything, mkT, mkM, mkQ, extM, extQ)
26import PureScript.Values
27import PureScript.Types
28import PureScript.Kinds
29import PureScript.TypeChecker.Monad
30import PureScript.TypeChecker.Kinds
31import PureScript.TypeChecker.Synonyms
33import Control.Monad.State
34import Control.Monad.Error
36import Control.Applicative
37import Control.Arrow (Kleisli(..), (***), (&&&))
38import qualified Control.Category as C
40import qualified Data.Map as M
42data TypeConstraint
43 = TypeConstraint Int Type
44 | RowConstraint Int Row deriving Show
46newtype TypeSolution = TypeSolution { runTypeSolution :: (Int -> Type, Int -> Row) }
48emptyTypeSolution :: TypeSolution
49emptyTypeSolution = TypeSolution (TUnknown, RUnknown)
51typeOf :: String -> Value -> Check Type
52typeOf 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
58varIfUnknown :: Type -> Type
59varIfUnknown 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
86replaceVarsWithUnknowns :: [String] -> Type -> Check Type
87replaceVarsWithUnknowns 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
110replaceType :: (Data d) => Int -> Type -> d -> d
111replaceType n t = everywhere (mkT go)
112 where
113 go (TUnknown m) | m == n = t
114 go t = t
116replaceRow :: (Data d) => Int -> Row -> d -> d
117replaceRow n r = everywhere (mkT go)
118 where
119 go (RUnknown m) | m == n = r
120 go r = r
122typeOccursCheck :: Int -> Type -> Check ()
123typeOccursCheck u (TUnknown _) = return ()
124typeOccursCheck u t = when (occursCheck u t) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ show t
126rowOccursCheck :: Int -> Row -> Check ()
127rowOccursCheck u (RUnknown _) = return ()
128rowOccursCheck u r = when (occursCheck u r) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ show r
130occursCheck :: (Data d) => Int -> d -> Bool
131occursCheck 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
138typeConstraints :: M.Map String Int -> Value -> Check ([TypeConstraint], Int)
139typeConstraints _ (NumericLiteral _) = do
140 me <- fresh
141 return ([TypeConstraint me Number], me)
142typeConstraints _ (StringLiteral _) = do
143 me <- fresh
144 return ([TypeConstraint me String], me)
145typeConstraints _ (BooleanLiteral _) = do
146 me <- fresh
147 return ([TypeConstraint me Boolean], me)
148typeConstraints 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)
153typeConstraints m (Unary op val) = do
154 (cs, n1) <- typeConstraints m val
155 me <- fresh
156 return (cs ++ unaryOperatorConstraints op n1 me, me)
157typeConstraints 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)
162typeConstraints 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)
171typeConstraints 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)
176typeConstraints 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)
181typeConstraints 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)
187typeConstraints 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)
193typeConstraints 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)
205typeConstraints 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)
210typeConstraints 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)
217typeConstraints 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)
222typeConstraints 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)
229replaceAllTypeSynonyms :: Type -> Check Type
230replaceAllTypeSynonyms 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'
239unaryOperatorConstraints :: UnaryOperator -> Int -> Int -> [TypeConstraint]
240unaryOperatorConstraints Negate val result = [TypeConstraint val Number, TypeConstraint result Number]
241unaryOperatorConstraints Not val result = [TypeConstraint val Boolean, TypeConstraint result Boolean]
242unaryOperatorConstraints BitwiseNot val result = [TypeConstraint val Number, TypeConstraint result Number]
244binaryOperatorConstraints :: BinaryOperator -> Int -> Int -> Int -> [TypeConstraint]
245binaryOperatorConstraints Add = symBinOpConstraints Number
246binaryOperatorConstraints Subtract = symBinOpConstraints Number
247binaryOperatorConstraints Multiply = symBinOpConstraints Number
248binaryOperatorConstraints Divide = symBinOpConstraints Number
249binaryOperatorConstraints Modulus = symBinOpConstraints Number
250binaryOperatorConstraints LessThan = asymBinOpConstraints Number Boolean
251binaryOperatorConstraints LessThanOrEqualTo = asymBinOpConstraints Number Boolean
252binaryOperatorConstraints GreaterThan = asymBinOpConstraints Number Boolean
253binaryOperatorConstraints GreaterThanOrEqualTo = asymBinOpConstraints Number Boolean
254binaryOperatorConstraints BitwiseAnd = symBinOpConstraints Number
255binaryOperatorConstraints BitwiseOr = symBinOpConstraints Number
256binaryOperatorConstraints BitwiseXor = symBinOpConstraints Number
257binaryOperatorConstraints ShiftLeft = symBinOpConstraints Number
258binaryOperatorConstraints ShiftRight = symBinOpConstraints Number
259binaryOperatorConstraints ZeroFillShiftRight = symBinOpConstraints Number
260binaryOperatorConstraints EqualTo = equalityBinOpConstraints
261binaryOperatorConstraints NotEqualTo = equalityBinOpConstraints
262binaryOperatorConstraints And = symBinOpConstraints Boolean
263binaryOperatorConstraints Or = symBinOpConstraints Boolean
264binaryOperatorConstraints Concat = symBinOpConstraints String
266equalityBinOpConstraints :: Int -> Int -> Int -> [TypeConstraint]
267equalityBinOpConstraints left right result = [TypeConstraint left (TUnknown right), TypeConstraint result Boolean]
269symBinOpConstraints :: Type -> Int -> Int -> Int -> [TypeConstraint]
270symBinOpConstraints ty left right result = asymBinOpConstraints ty ty left right result
272asymBinOpConstraints :: Type -> Type -> Int -> Int -> Int -> [TypeConstraint]
273asymBinOpConstraints ty res left right result = [TypeConstraint left ty, TypeConstraint right ty, TypeConstraint result res]
275typeConstraintsForBinder :: Int -> Binder -> Check ([TypeConstraint], M.Map String Int)
276typeConstraintsForBinder val (StringBinder _) = constantBinder val String
277typeConstraintsForBinder val (NumberBinder _) = constantBinder val Number
278typeConstraintsForBinder val (BooleanBinder _) = constantBinder val Boolean
279typeConstraintsForBinder val (VarBinder name) = do
280 me <- fresh
281 return ([TypeConstraint me (TUnknown val)], M.singleton name me)
282typeConstraintsForBinder 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"
289typeConstraintsForBinder 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"
299typeConstraintsForBinder 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)
312typeConstraintsForBinder 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)
323constantBinder :: Int -> Type -> Check ([TypeConstraint], M.Map String Int)
324constantBinder val ty = return ([TypeConstraint val ty], M.empty)
326typeConstraintsForBinders :: M.Map String Int -> Int -> Int -> [(Binder, Value)] -> Check [TypeConstraint]
327typeConstraintsForBinders _ _ _ [] = return []
328typeConstraintsForBinders 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)
334typeConstraintsForStatement :: M.Map String Int -> M.Map String Int -> Int -> Statement -> Check ([TypeConstraint], Bool, M.Map String Int)
335typeConstraintsForStatement 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."
341typeConstraintsForStatement 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)
345typeConstraintsForStatement 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)
349typeConstraintsForStatement 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)
353typeConstraintsForStatement 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)
358typeConstraintsForStatement 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)
366typeConstraintsForStatement m mass ret (Return val) = do
367 (cs1, n1) <- typeConstraints (m `M.union` mass) val
368 return ((TypeConstraint n1 (TUnknown ret)) : cs1, True, mass)
370typeConstraintsForAssignmentTarget :: M.Map String Int -> M.Map String Int -> Int -> AssignmentTarget -> Check [TypeConstraint]
371typeConstraintsForAssignmentTarget 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)]
376typeConstraintsForAssignmentTarget 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
381typeConstraintsForAssignmentTarget 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
387typeConstraintsForBlock :: M.Map String Int -> M.Map String Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, M.Map String Int)
388typeConstraintsForBlock _ mass _ [] = return ([], False, mass)
389typeConstraintsForBlock 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)
398solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
399solveTypeConstraints [] s = return s
400solveTypeConstraints 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'
406solveTypeConstraints (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'
413substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
414substituteTypeInConstraint n s (TypeConstraint m t)
415 | n == m = unifyTypes s t
416 | otherwise = return [TypeConstraint m (replaceType n s t)]
417substituteTypeInConstraint n s (RowConstraint m r)
418 = return [RowConstraint m (replaceType n s r)]
420substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
421substituteRowInConstraint n r (TypeConstraint m t)
422 = return [TypeConstraint m (replaceRow n r t)]
423substituteRowInConstraint n r (RowConstraint m r1)
424 | m == n = unifyRows r r1
425 | otherwise = return [RowConstraint m (replaceRow n r r1)]
427unifyTypes :: Type -> Type -> Check [TypeConstraint]
428unifyTypes (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
429unifyTypes (TUnknown u) t = do
430 typeOccursCheck u t
431 return [TypeConstraint u t]
432unifyTypes t (TUnknown u) = do
433 typeOccursCheck u t
434 return [TypeConstraint u t]
435unifyTypes (ForAll idents t1) t2 = join $ flip unifyTypes t2 <$> replaceVarsWithUnknowns idents t1
436unifyTypes t1 (ForAll idents t2) = join $ unifyTypes t1 <$> replaceVarsWithUnknowns idents t2
437unifyTypes Number Number = return []
438unifyTypes String String = return []
439unifyTypes Boolean Boolean = return []
440unifyTypes (Array s) (Array t) = unifyTypes s t
441unifyTypes (Object row1) (Object row2) = unifyRows row1 row2
442unifyTypes (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
447unifyTypes (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
448unifyTypes (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = return []
449unifyTypes (TypeVar v1) (TypeVar v2) = return []
450unifyTypes (TypeApp t1 t2) (TypeApp t3 t4) = do
451 cs1 <- unifyTypes t1 t3
452 cs2 <- unifyTypes t2 t4
453 return $ cs1 ++ cs2
454unifyTypes t1 t2 = throwError $ "Cannot unify " ++ show t1 ++ " with " ++ show t2 ++ "."
456unifyRows :: Row -> Row -> Check [TypeConstraint]
457unifyRows 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))