git.iko.soy/rowtype-yoga/purescript-native
on d6ab2e7 help sign in
rowtype-yoga/purescript-native/src/PureScript/TypeChecker/Types.hs
487 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.Names
30import PureScript.TypeChecker.Monad
31import PureScript.TypeChecker.Kinds
32import PureScript.TypeChecker.Synonyms
34import Control.Monad.State
35import Control.Monad.Error
37import Control.Applicative
38import Control.Arrow (Kleisli(..), (***), (&&&))
39import qualified Control.Category as C
41import qualified Data.Map as M
43data TypeConstraint
44 = TypeConstraint Int Type
45 | RowConstraint Int Row deriving Show
47newtype TypeSolution = TypeSolution { runTypeSolution :: (Int -> Type, Int -> Row) }
49emptyTypeSolution :: TypeSolution
50emptyTypeSolution = TypeSolution (TUnknown, RUnknown)
52typeOf :: Ident -> Value -> Check PolyType
53typeOf 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
59varIfUnknown :: Type -> PolyType
60varIfUnknown 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
88replaceVarsWithUnknowns :: [String] -> Type -> Check Type
89replaceVarsWithUnknowns 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
112replaceType :: (Data d) => Int -> Type -> d -> d
113replaceType n t = everywhere (mkT go)
114 where
115 go (TUnknown m) | m == n = t
116 go t = t
118replaceRow :: (Data d) => Int -> Row -> d -> d
119replaceRow n r = everywhere (mkT go)
120 where
121 go (RUnknown m) | m == n = r
122 go r = r
124typeOccursCheck :: Int -> Type -> Check ()
125typeOccursCheck u (TUnknown _) = return ()
126typeOccursCheck u t = when (occursCheck u t) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ show t
128rowOccursCheck :: Int -> Row -> Check ()
129rowOccursCheck u (RUnknown _) = return ()
130rowOccursCheck u r = when (occursCheck u r) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ show r
132occursCheck :: (Data d) => Int -> d -> Bool
133occursCheck 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
140typeConstraints :: M.Map Ident Int -> Value -> Check ([TypeConstraint], Int)
141typeConstraints _ (NumericLiteral _) = do
142 me <- fresh
143 return ([TypeConstraint me Number], me)
144typeConstraints _ (StringLiteral _) = do
145 me <- fresh
146 return ([TypeConstraint me String], me)
147typeConstraints _ (BooleanLiteral _) = do
148 me <- fresh
149 return ([TypeConstraint me Boolean], me)
150typeConstraints 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)
155typeConstraints m (Unary op val) = do
156 (cs, n1) <- typeConstraints m val
157 me <- fresh
158 return (cs ++ unaryOperatorConstraints op n1 me, me)
159typeConstraints 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)
164typeConstraints 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)
173typeConstraints 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)
178typeConstraints 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)
183typeConstraints 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)
189typeConstraints 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)
195typeConstraints 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)
208typeConstraints 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)
213typeConstraints 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)
221typeConstraints 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)
226typeConstraints 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)
233replaceAllTypeSynonyms :: Type -> Check Type
234replaceAllTypeSynonyms 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'
243unaryOperatorConstraints :: UnaryOperator -> Int -> Int -> [TypeConstraint]
244unaryOperatorConstraints Negate val result = [TypeConstraint val Number, TypeConstraint result Number]
245unaryOperatorConstraints Not val result = [TypeConstraint val Boolean, TypeConstraint result Boolean]
246unaryOperatorConstraints BitwiseNot val result = [TypeConstraint val Number, TypeConstraint result Number]
248binaryOperatorConstraints :: BinaryOperator -> Int -> Int -> Int -> [TypeConstraint]
249binaryOperatorConstraints Add = symBinOpConstraints Number
250binaryOperatorConstraints Subtract = symBinOpConstraints Number
251binaryOperatorConstraints Multiply = symBinOpConstraints Number
252binaryOperatorConstraints Divide = symBinOpConstraints Number
253binaryOperatorConstraints Modulus = symBinOpConstraints Number
254binaryOperatorConstraints LessThan = asymBinOpConstraints Number Boolean
255binaryOperatorConstraints LessThanOrEqualTo = asymBinOpConstraints Number Boolean
256binaryOperatorConstraints GreaterThan = asymBinOpConstraints Number Boolean
257binaryOperatorConstraints GreaterThanOrEqualTo = asymBinOpConstraints Number Boolean
258binaryOperatorConstraints BitwiseAnd = symBinOpConstraints Number
259binaryOperatorConstraints BitwiseOr = symBinOpConstraints Number
260binaryOperatorConstraints BitwiseXor = symBinOpConstraints Number
261binaryOperatorConstraints ShiftLeft = symBinOpConstraints Number
262binaryOperatorConstraints ShiftRight = symBinOpConstraints Number
263binaryOperatorConstraints ZeroFillShiftRight = symBinOpConstraints Number
264binaryOperatorConstraints EqualTo = equalityBinOpConstraints
265binaryOperatorConstraints NotEqualTo = equalityBinOpConstraints
266binaryOperatorConstraints And = symBinOpConstraints Boolean
267binaryOperatorConstraints Or = symBinOpConstraints Boolean
268binaryOperatorConstraints Concat = symBinOpConstraints String
270equalityBinOpConstraints :: Int -> Int -> Int -> [TypeConstraint]
271equalityBinOpConstraints left right result = [TypeConstraint left (TUnknown right), TypeConstraint result Boolean]
273symBinOpConstraints :: Type -> Int -> Int -> Int -> [TypeConstraint]
274symBinOpConstraints ty left right result = asymBinOpConstraints ty ty left right result
276asymBinOpConstraints :: Type -> Type -> Int -> Int -> Int -> [TypeConstraint]
277asymBinOpConstraints ty res left right result = [TypeConstraint left ty, TypeConstraint right ty, TypeConstraint result res]
279typeConstraintsForBinder :: Int -> Binder -> Check ([TypeConstraint], M.Map Ident Int)
280typeConstraintsForBinder val (StringBinder _) = constantBinder val String
281typeConstraintsForBinder val (NumberBinder _) = constantBinder val Number
282typeConstraintsForBinder val (BooleanBinder _) = constantBinder val Boolean
283typeConstraintsForBinder val (VarBinder name) = do
284 me <- fresh
285 return ([TypeConstraint me (TUnknown val)], M.singleton name me)
286typeConstraintsForBinder 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"
293typeConstraintsForBinder 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"
303typeConstraintsForBinder 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)
316typeConstraintsForBinder 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)
327constantBinder :: Int -> Type -> Check ([TypeConstraint], M.Map Ident Int)
328constantBinder val ty = return ([TypeConstraint val ty], M.empty)
330typeConstraintsForBinders :: M.Map Ident Int -> Int -> Int -> [(Binder, Value)] -> Check [TypeConstraint]
331typeConstraintsForBinders _ _ _ [] = return []
332typeConstraintsForBinders 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)
338typeConstraintsForStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> Statement -> Check ([TypeConstraint], Bool, M.Map Ident Int)
339typeConstraintsForStatement 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."
345typeConstraintsForStatement 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)
349typeConstraintsForStatement 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)
353typeConstraintsForStatement 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)
357typeConstraintsForStatement 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)
362typeConstraintsForStatement 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)
370typeConstraintsForStatement m mass ret (Return val) = do
371 (cs1, n1) <- typeConstraints (m `M.union` mass) val
372 return ((TypeConstraint n1 (TUnknown ret)) : cs1, True, mass)
374typeConstraintsForAssignmentTarget :: M.Map Ident Int -> M.Map Ident Int -> Int -> AssignmentTarget -> Check [TypeConstraint]
375typeConstraintsForAssignmentTarget 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)]
380typeConstraintsForAssignmentTarget 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
385typeConstraintsForAssignmentTarget 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
391typeConstraintsForBlock :: M.Map Ident Int -> M.Map Ident Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, M.Map Ident Int)
392typeConstraintsForBlock _ mass _ [] = return ([], False, mass)
393typeConstraintsForBlock 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)
402solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
403solveTypeConstraints [] s = return s
404solveTypeConstraints 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'
410solveTypeConstraints (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'
417substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
418substituteTypeInConstraint n s (TypeConstraint m t)
419 | n == m = unifyTypes s t
420 | otherwise = return [TypeConstraint m (replaceType n s t)]
421substituteTypeInConstraint n s (RowConstraint m r)
422 = return [RowConstraint m (replaceType n s r)]
424substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
425substituteRowInConstraint n r (TypeConstraint m t)
426 = return [TypeConstraint m (replaceRow n r t)]
427substituteRowInConstraint n r (RowConstraint m r1)
428 | m == n = unifyRows r r1
429 | otherwise = return [RowConstraint m (replaceRow n r r1)]
431unifyTypes :: Type -> Type -> Check [TypeConstraint]
432unifyTypes (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
433unifyTypes (TUnknown u) t = do
434 typeOccursCheck u t
435 return [TypeConstraint u t]
436unifyTypes t (TUnknown u) = do
437 typeOccursCheck u t
438 return [TypeConstraint u t]
439unifyTypes Number Number = return []
440unifyTypes String String = return []
441unifyTypes Boolean Boolean = return []
442unifyTypes (Array s) (Array t) = unifyTypes s t
443unifyTypes (Object row1) (Object row2) = unifyRows row1 row2
444unifyTypes (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
449unifyTypes (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
450unifyTypes (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = return []
451unifyTypes (TypeVar v1) (TypeVar v2) = return []
452unifyTypes (TypeApp t1 t2) (TypeApp t3 t4) = do
453 cs1 <- unifyTypes t1 t3
454 cs2 <- unifyTypes t2 t4
455 return $ cs1 ++ cs2
456unifyTypes t1 t2 = throwError $ "Cannot unify " ++ show t1 ++ " with " ++ show t2 ++ "."
458unifyRows :: Row -> Row -> Check [TypeConstraint]
459unifyRows 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))