@@ -1,554 +0,0 @@
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−findTypeVars :: (Data d) => d -> [String]
87−findTypeVars = everything (++) (mkQ [] f)
89− f :: Type -> [String]
93−findUnknownRows :: (Data d) => d -> [Int]
94−findUnknownRows = everything (++) (mkQ [] f)
100−varIfUnknown :: Type -> PolyType
103− (ty', m) = flip runState M.empty $ everywhereM (flip extM g $ mkM f) ty
105− PolyType (sort $ nub $ M.elems m ++ findTypeVars ty) ty'
107− f :: Type -> State (M.Map Int String) Type
110− case M.lookup n m of
112− let name = "t" ++ show (M.size m)
113− put $ M.insert n name m
114− return $ TypeVar name
115− Just name -> return $ TypeVar name
117− g :: Row -> State (M.Map Int String) Row
120− case M.lookup n m of
122− let name = "r" ++ show (M.size m)
123− put $ M.insert n name m
124− return $ RowVar name
125− Just name -> return $ RowVar name
128−replaceVarsWithUnknowns :: [String] -> Type -> Check Type
129−replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)
131− f :: Type -> StateT (M.Map String Int) Check Type
132− f (TypeVar var) | var `elem` idents = do
135− case M.lookup var m of
137− put (M.insert var n m)
139− Just u -> return $ TUnknown u
141− g :: Row -> StateT (M.Map String Int) Check Row
142− g (RowVar var) | var `elem` idents = do
145− case M.lookup var m of
147− put (M.insert var n m)
149− Just u -> return $ RUnknown u
152−replaceType :: (Data d) => Int -> Type -> d -> d
153−replaceType n t = everywhere (mkT go)
155− go (TUnknown m) | m == n = t
158−replaceRow :: (Data d) => Int -> Row -> d -> d
159−replaceRow n r = everywhere (mkT go)
161− go (RUnknown m) | m == n = r
164−typeOccursCheck :: Int -> Type -> Check ()
165−typeOccursCheck u (TUnknown _) = return ()
166−typeOccursCheck u t = when (occursCheck u t) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ show t
168−rowOccursCheck :: Int -> Row -> Check ()
169−rowOccursCheck u (RUnknown _) = return ()
170−rowOccursCheck u r = when (occursCheck u r) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ show r
172−occursCheck :: (Data d) => Int -> d -> Bool
173−occursCheck u = everything (||) $ flip extQ g $ mkQ False f
175− f (TUnknown u') | u' == u = True
177− g (RUnknown u') | u' == u = True
180−typeConstraints :: M.Map Ident Int -> Value -> Check ([TypeConstraint], Int)
181−typeConstraints _ (NumericLiteral _) = do
183− return ([TypeConstraint me Number], me)
184−typeConstraints _ (StringLiteral _) = do
186− return ([TypeConstraint me String], me)
187−typeConstraints _ (BooleanLiteral _) = do
189− return ([TypeConstraint me Boolean], me)
190−typeConstraints m (ArrayLiteral vals) = do
191− all <- mapM (typeConstraints m) vals
192− let (cs, ns) = (concat . map fst &&& map snd) all
194− return (cs ++ map (TypeConstraint me . Array . TUnknown) ns, me)
195−typeConstraints m (Unary op val) = do
196− (cs, n1) <- typeConstraints m val
198− return (cs ++ unaryOperatorConstraints op n1 me, me)
199−typeConstraints m (Binary op left right) = do
200− (cs1, n1) <- typeConstraints m left
201− (cs2, n2) <- typeConstraints m right
203− return (cs1 ++ cs2 ++ binaryOperatorConstraints op n1 n2 me, me)
204−typeConstraints m (ObjectLiteral ps) = do
205− all <- mapM (typeConstraints m . snd) ps
206− let (cs, ns) = (concat . map fst &&& map snd) all
208− let tys = zipWith (\(name, _) u -> (name, TUnknown u)) ps ns
209− return ((TypeConstraint me (Object (typesToRow tys))) : cs, me)
211− typesToRow [] = REmpty
212− typesToRow ((name, ty):tys) = RCons name ty (typesToRow tys)
213−typeConstraints m (Indexer index val) = do
214− (cs1, n1) <- typeConstraints m index
215− (cs2, n2) <- typeConstraints m val
217− return ((TypeConstraint n1 Number) : (TypeConstraint n2 (Array (TUnknown me))) : cs1 ++ cs2, me)
218−typeConstraints m (Accessor prop val) = do
219− (cs, n1) <- typeConstraints m val
222− return ((TypeConstraint n1 (Object (RCons prop (TUnknown me) (RUnknown rest)))) : cs, me)
223−typeConstraints m (Abs args ret) = do
224− ns <- replicateM (length args) fresh
225− let m' = m `M.union` M.fromList (zipWith (,) args ns)
226− (cs, n') <- typeConstraints m' ret
228− return ((TypeConstraint me (Function (map TUnknown ns) (TUnknown n'))) : cs, me)
229−typeConstraints m (App f xs) = do
230− (cs1, n1) <- typeConstraints m f
231− all <- mapM (typeConstraints m) xs
232− let (cs2, ns) = (concat . map fst &&& map snd) all
234− return ((TypeConstraint n1 (Function (map TUnknown ns) (TUnknown me))) : cs1 ++ cs2, me)
235−typeConstraints m (Var var) =
236− case M.lookup var m of
239− case M.lookup var (names env) of
240− Nothing -> throwError $ show var ++ " is undefined"
241− Just (PolyType idents ty, _) -> do
243− replaced <- replaceVarsWithUnknowns idents ty
244− return ([TypeConstraint me replaced], me)
247− return ([TypeConstraint u (TUnknown me)], me)
248−typeConstraints m (Block ss) = do
250− (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m M.empty ret ss
251− guardWith "Block is missing a return statement" allCodePathsReturn
253−typeConstraints m (Constructor c) = do
255− case M.lookup c (dataConstructors env) of
256− Nothing -> throwError $ "Constructor " ++ c ++ " is undefined"
257− Just (PolyType idents ty) -> do
259− replaced <- replaceVarsWithUnknowns idents ty
260− return ([TypeConstraint me replaced], me)
261−typeConstraints m (Case val binders) = do
262− (cs1, n1) <- typeConstraints m val
264− cs2 <- typeConstraintsForBinders m n1 ret binders
265− return (cs1 ++ cs2, ret)
266−typeConstraints m (TypedValue val poly@(PolyType idents ty)) = do
268− guardWith ("Expected type of kind *, was " ++ show kind) $ kind == Star
269− desugared <- replaceAllTypeSynonyms ty
270− (cs, n1) <- typeConstraints m val
271− return (TypeConstraint n1 desugared : cs, n1)
273−replaceAllTypeSynonyms :: Type -> Check Type
274−replaceAllTypeSynonyms ty = do
276− go (M.toList $ typeSynonyms env) ty
278− go [] ty = return ty
279− go ((name, (args, repl)):rest) ty = do
280− ty' <- either throwError return (substituteTypeSynonym name args repl ty)
283−unaryOperatorConstraints :: UnaryOperator -> Int -> Int -> [TypeConstraint]
284−unaryOperatorConstraints Negate val result = [TypeConstraint val Number, TypeConstraint result Number]
285−unaryOperatorConstraints Not val result = [TypeConstraint val Boolean, TypeConstraint result Boolean]
286−unaryOperatorConstraints BitwiseNot val result = [TypeConstraint val Number, TypeConstraint result Number]
288−binaryOperatorConstraints :: BinaryOperator -> Int -> Int -> Int -> [TypeConstraint]
289−binaryOperatorConstraints Add = symBinOpConstraints Number
290−binaryOperatorConstraints Subtract = symBinOpConstraints Number
291−binaryOperatorConstraints Multiply = symBinOpConstraints Number
292−binaryOperatorConstraints Divide = symBinOpConstraints Number
293−binaryOperatorConstraints Modulus = symBinOpConstraints Number
294−binaryOperatorConstraints LessThan = asymBinOpConstraints Number Boolean
295−binaryOperatorConstraints LessThanOrEqualTo = asymBinOpConstraints Number Boolean
296−binaryOperatorConstraints GreaterThan = asymBinOpConstraints Number Boolean
297−binaryOperatorConstraints GreaterThanOrEqualTo = asymBinOpConstraints Number Boolean
298−binaryOperatorConstraints BitwiseAnd = symBinOpConstraints Number
299−binaryOperatorConstraints BitwiseOr = symBinOpConstraints Number
300−binaryOperatorConstraints BitwiseXor = symBinOpConstraints Number
301−binaryOperatorConstraints ShiftLeft = symBinOpConstraints Number
302−binaryOperatorConstraints ShiftRight = symBinOpConstraints Number
303−binaryOperatorConstraints ZeroFillShiftRight = symBinOpConstraints Number
304−binaryOperatorConstraints EqualTo = equalityBinOpConstraints
305−binaryOperatorConstraints NotEqualTo = equalityBinOpConstraints
306−binaryOperatorConstraints And = symBinOpConstraints Boolean
307−binaryOperatorConstraints Or = symBinOpConstraints Boolean
308−binaryOperatorConstraints Concat = symBinOpConstraints String
310−equalityBinOpConstraints :: Int -> Int -> Int -> [TypeConstraint]
311−equalityBinOpConstraints left right result = [TypeConstraint left (TUnknown right), TypeConstraint result Boolean]
313−symBinOpConstraints :: Type -> Int -> Int -> Int -> [TypeConstraint]
314−symBinOpConstraints ty left right result = asymBinOpConstraints ty ty left right result
316−asymBinOpConstraints :: Type -> Type -> Int -> Int -> Int -> [TypeConstraint]
317−asymBinOpConstraints ty res left right result = [TypeConstraint left ty, TypeConstraint right ty, TypeConstraint result res]
319−typeConstraintsForBinder :: Int -> Binder -> Check ([TypeConstraint], M.Map Ident Int)
320−typeConstraintsForBinder val (StringBinder _) = constantBinder val String
321−typeConstraintsForBinder val (NumberBinder _) = constantBinder val Number
322−typeConstraintsForBinder val (BooleanBinder _) = constantBinder val Boolean
323−typeConstraintsForBinder val (VarBinder name) = do
325− return ([TypeConstraint me (TUnknown val)], M.singleton name me)
326−typeConstraintsForBinder val (NullaryBinder ctor) = do
328− case M.lookup ctor (dataConstructors env) of
329− Just (PolyType args ret) -> do
330− ret' <- replaceVarsWithUnknowns args ret
331− return ([TypeConstraint val ret'], M.empty)
332− _ -> throwError $ "Constructor " ++ ctor ++ " is not defined"
333−typeConstraintsForBinder val (UnaryBinder ctor binder) = do
335− case M.lookup ctor (dataConstructors env) of
336− Just (PolyType idents f@(Function [_] _)) -> do
338− (Function [ty] ret) <- replaceVarsWithUnknowns idents f
339− (cs, m1) <- typeConstraintsForBinder obj binder
340− return ((TypeConstraint val ret) : (TypeConstraint obj ty) : cs, m1)
341− Just _ -> throwError $ ctor ++ " is not a unary constructor"
342− _ -> throwError $ "Constructor " ++ ctor ++ " is not defined"
343−typeConstraintsForBinder val (ObjectBinder props) = do
346− (cs, m1) <- typeConstraintsForProperties row (RUnknown rest) props
347− return ((TypeConstraint val (Object (RUnknown row))) : cs, m1)
349− typeConstraintsForProperties :: Int -> Row -> [(String, Binder)] -> Check ([TypeConstraint], M.Map Ident Int)
350− typeConstraintsForProperties nrow row [] = return ([RowConstraint nrow row], M.empty)
351− typeConstraintsForProperties nrow row ((name, binder):binders) = do
353− (cs1, m1) <- typeConstraintsForBinder propTy binder
354− (cs2, m2) <- typeConstraintsForProperties nrow (RCons name (TUnknown propTy) row) binders
355− return (cs1 ++ cs2, M.union m1 m2)
356−typeConstraintsForBinder val (ArrayBinder binders rest) = do
358− all <- mapM (typeConstraintsForBinder el) binders
359− let (cs1, m1) = (concat . map fst &&& M.unions . map snd) all
360− let arrayConstraint = TypeConstraint val (Array (TUnknown el))
362− Nothing -> return (arrayConstraint : cs1, m1)
364− (cs2, m2) <- typeConstraintsForBinder val binder
365− return (arrayConstraint : cs1 ++ cs2, M.union m1 m2)
367−constantBinder :: Int -> Type -> Check ([TypeConstraint], M.Map Ident Int)
368−constantBinder val ty = return ([TypeConstraint val ty], M.empty)
370−typeConstraintsForBinders :: M.Map Ident Int -> Int -> Int -> [(Binder, Value)] -> Check [TypeConstraint]
371−typeConstraintsForBinders _ _ _ [] = return []
372−typeConstraintsForBinders m nval ret ((binder, val):bs) = do
373− (cs1, m1) <- typeConstraintsForBinder nval binder
374− (cs2, n2) <- typeConstraints (M.union m m1) val
375− cs3 <- typeConstraintsForBinders m nval ret bs
376− return ((TypeConstraint n2 (TUnknown ret)) : cs1 ++ cs2 ++ cs3)
378−assignVariable :: Ident -> M.Map Ident Int -> Check ()
379−assignVariable name m =
380− case M.lookup name m of
381− Nothing -> return ()
382− Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."
384−typeConstraintsForStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> Statement -> Check ([TypeConstraint], Bool, M.Map Ident Int)
385−typeConstraintsForStatement m mass ret (VariableIntroduction name val) = do
386− assignVariable name (m `M.union` mass)
387− (cs1, n1) <- typeConstraints m val
388− return $ (cs1, False, M.insert name n1 mass)
389−typeConstraintsForStatement m mass ret (Assignment tgt val) = do
390− (cs1, n1) <- typeConstraints m val
391− cs2 <- typeConstraintsForAssignmentTarget m mass n1 tgt
392− return (cs1 ++ cs2, False, mass)
393−typeConstraintsForStatement m mass ret (While val inner) = do
394− (cs1, n1) <- typeConstraints m val
395− (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret inner
396− return $ ((TypeConstraint n1 Boolean) : cs1 ++ cs2, allCodePathsReturn, mass)
397−typeConstraintsForStatement m mass ret (If ifst) = do
398− (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
399− return $ (cs, allCodePathsReturn, mass)
400−typeConstraintsForStatement m mass ret (For ident start end inner) = do
401− assignVariable ident (m `M.union` mass)
402− (cs1, n1) <- typeConstraints (m `M.union` mass) start
403− (cs2, n2) <- typeConstraints (m `M.union` mass) end
404− let mass1 = M.insert ident n1 mass
405− (cs3, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass1) mass1 ret inner
406− return $ ((TypeConstraint n1 Number) : (TypeConstraint n2 Number) : cs1 ++ cs2 ++ cs3, allCodePathsReturn, mass)
407−typeConstraintsForStatement m mass ret (ForEach ident vals inner) = do
408− assignVariable ident (m `M.union` mass)
410− (cs1, n1) <- typeConstraints (m `M.union` mass) vals
411− let mass1 = M.insert ident val mass
412− (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass1) mass1 ret inner
413− guardWith "Cannot return from within a foreach block" $ not allCodePathsReturn
414− return $ ((TypeConstraint n1 (Array (TUnknown val))) : cs1 ++ cs2, False, mass)
415−typeConstraintsForStatement m mass ret (Return val) = do
416− (cs1, n1) <- typeConstraints (m `M.union` mass) val
417− return ((TypeConstraint n1 (TUnknown ret)) : cs1, True, mass)
419−typeConstraintsForIfStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> IfStatement -> Check ([TypeConstraint], Bool)
420−typeConstraintsForIfStatement m mass ret (IfStatement val thens Nothing) = do
421− (cs1, n1) <- typeConstraints m val
422− (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret thens
423− return ((TypeConstraint n1 Boolean) : cs1 ++ cs2, allCodePathsReturn)
424−typeConstraintsForIfStatement m mass ret (IfStatement val thens (Just elses)) = do
425− (cs1, n1) <- typeConstraints m val
426− (cs2, allCodePathsReturn1, _) <- typeConstraintsForBlock m mass ret thens
427− (cs3, allCodePathsReturn2) <- typeConstraintsForElseStatement m mass ret elses
428− return ((TypeConstraint n1 Boolean) : cs1 ++ cs2 ++ cs3, allCodePathsReturn1 && allCodePathsReturn2)
430−typeConstraintsForElseStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> ElseStatement -> Check ([TypeConstraint], Bool)
431−typeConstraintsForElseStatement m mass ret (Else elses) = do
432− (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret elses
433− return (cs, allCodePathsReturn)
434−typeConstraintsForElseStatement m mass ret (ElseIf ifst) = do
435− (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
436− return (cs, allCodePathsReturn)
438−typeConstraintsForAssignmentTarget :: M.Map Ident Int -> M.Map Ident Int -> Int -> AssignmentTarget -> Check [TypeConstraint]
439−typeConstraintsForAssignmentTarget m mass nval (AssignVariable var) =
440− case M.lookup var mass of
441− Nothing -> throwError $ "No local variable with name " ++ show var
443− return [TypeConstraint nval (TUnknown ty)]
444−typeConstraintsForAssignmentTarget m mass nval (AssignArrayIndex index tgt) = do
446− (cs1, n1) <- typeConstraints (m `M.union` mass) index
447− cs2 <- typeConstraintsForAssignmentTarget m mass arr tgt
448− return $ (TypeConstraint arr (Array (TUnknown nval))) : (TypeConstraint n1 Number) : cs1 ++ cs2
449−typeConstraintsForAssignmentTarget m mass nval (AssignObjectProperty prop tgt) = do
452− cs <- typeConstraintsForAssignmentTarget m mass obj tgt
453− return $ (TypeConstraint obj (Object (RCons prop (TUnknown nval) $ RUnknown row))) : cs
455−typeConstraintsForBlock :: M.Map Ident Int -> M.Map Ident Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, M.Map Ident Int)
456−typeConstraintsForBlock _ mass _ [] = return ([], False, mass)
457−typeConstraintsForBlock m mass ret (s:ss) = do
458− (cs1, b1, mass1) <- typeConstraintsForStatement (m `M.union` mass) mass ret s
460− (True, []) -> return (cs1, True, mass1)
461− (True, _) -> throwError "Unreachable code"
463− (cs2, b2, mass2) <- typeConstraintsForBlock m mass1 ret ss
464− return (cs1 ++ cs2, b2, mass2)
466−solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
467−solveTypeConstraints [] s = return s
468−solveTypeConstraints all@(TypeConstraint n t:cs) s = do
470− let s' = let (f, g) = runTypeSolution s
471− in TypeSolution (replaceType n t . f, replaceType n t . g)
472− cs' <- fmap concat $ mapM (substituteTypeInConstraint n t) cs
473− solveTypeConstraints cs' s'
474−solveTypeConstraints (RowConstraint n r:cs) s = do
476− let s' = let (f, g) = runTypeSolution s
477− in TypeSolution $ (replaceRow n r . f, replaceRow n r . g)
478− cs' <- fmap concat $ mapM (substituteRowInConstraint n r) cs
479− solveTypeConstraints cs' s'
481−substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
482−substituteTypeInConstraint n s (TypeConstraint m t)
483− | n == m = unifyTypes s t
484− | otherwise = return [TypeConstraint m (replaceType n s t)]
485−substituteTypeInConstraint n s (RowConstraint m r)
486− = return [RowConstraint m (replaceType n s r)]
488−substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
489−substituteRowInConstraint n r (TypeConstraint m t)
490− = return [TypeConstraint m (replaceRow n r t)]
491−substituteRowInConstraint n r (RowConstraint m r1)
492− | m == n = unifyRows r r1
493− | otherwise = return [RowConstraint m (replaceRow n r r1)]
495−unifyTypes :: Type -> Type -> Check [TypeConstraint]
496−unifyTypes (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
497−unifyTypes (TUnknown u) t = do
499− return [TypeConstraint u t]
500−unifyTypes t (TUnknown u) = do
502− return [TypeConstraint u t]
503−unifyTypes Number Number = return []
504−unifyTypes String String = return []
505−unifyTypes Boolean Boolean = return []
506−unifyTypes (Array s) (Array t) = unifyTypes s t
507−unifyTypes (Object row1) (Object row2) = unifyRows row1 row2
508−unifyTypes (Function args1 ret1) (Function args2 ret2) = do
509− guardWith "Function applied to incorrect number of args" $ length args1 == length args2
510− cs1 <- fmap concat $ zipWithM unifyTypes args1 args2
511− cs2 <- unifyTypes ret1 ret2
513−unifyTypes (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
514−unifyTypes (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = return []
515−unifyTypes (TypeVar v1) (TypeVar v2) = return []
516−unifyTypes (TypeApp t1 t2) (TypeApp t3 t4) = do
517− cs1 <- unifyTypes t1 t3
518− cs2 <- unifyTypes t2 t4
520−unifyTypes t1 t2 = throwError $ "Cannot unify " ++ show t1 ++ " with " ++ show t2 ++ "."
522−unifyRows :: Row -> Row -> Check [TypeConstraint]
525− (s1, r1') = toList r1
526− (s2, r2') = toList r2
527− int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
528− sd1 = [ (name, t1) | (name, t1) <- s1, not (elem name (map fst s2)) ]
529− sd2 = [ (name, t2) | (name, t2) <- s2, not (elem name (map fst s1)) ]
530− in rethrow (\e -> "Cannot unify " ++ show r1 ++ " with " ++ show r2 ++ ": " ++ e) $ do
531− cs1 <- fmap concat $ mapM (uncurry unifyTypes) int
532− cs2 <- unifyRows' sd1 r1' sd2 r2'
535− unifyRows' :: [(String, Type)] -> Row -> [(String, Type)] -> Row -> Check [TypeConstraint]
536− unifyRows' [] (RUnknown u) sd r = do
538− return [RowConstraint u (fromList (sd, r))]
539− unifyRows' sd r [] (RUnknown u) = do
541− return [RowConstraint u (fromList (sd, r))]
542− unifyRows' ((name, ty):row) r others (RUnknown u) = do
544− cs <- unifyRows' row r others (RUnknown u')
545− return (RowConstraint u (RCons name ty (RUnknown u')) : cs)
546− unifyRows' [] REmpty [] REmpty = return []
547− unifyRows' sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ show (fromList (sd1, r1)) ++ " with " ++ show (fromList (sd2, r2)) ++ "."
548− toList :: Row -> ([(String, Type)], Row)
549− toList (RCons name ty row) = let (tys, rest) = toList row
550− in ((name, ty):tys, rest)
552− fromList :: ([(String, Type)], Row) -> Row
553− fromList ([], r) = r
554− fromList ((name, t):ts, r) = RCons name t (fromList (ts, r))