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