@@ -15,8 +15,6 @@
1515{-# LANGUAGE DeriveDataTypeable #-}
1616
1717module Language.PureScript.TypeChecker.Types (
18− TypeConstraint(..),
19− TypeSolution(..),
2018 typeOf
2119) where
2220
@@ -35,56 +33,127 @@ import Language.PureScript.TypeChecker.Monad
3533import Language.PureScript.TypeChecker.Kinds
3634import Language.PureScript.TypeChecker.Synonyms
3735import Language.PureScript.Pretty
36+import Language.PureScript.Unknown
3837
3938import Control.Monad.State
4039import Control.Monad.Error
4140
4241import Control.Applicative
43−import Control.Arrow (Kleisli(..), (***), (&&&), first)
42+import Control.Arrow (Arrow(..), Kleisli(..), (***), (&&&), second)
4443import qualified Control.Category as C
4544
4645import qualified Data.Map as M
4746
48−data TypeConstraintOrigin
49− = ValueOrigin Value
50− | BinderOrigin Binder
51− | AssignmentTargetOrigin Ident deriving (Show, D.Data, D.Typeable)
52−
53−prettyPrintOrigin :: TypeConstraintOrigin -> String
54−prettyPrintOrigin (ValueOrigin val) = prettyPrintValue val
55−prettyPrintOrigin (BinderOrigin binder) = prettyPrintBinder binder
56−prettyPrintOrigin (AssignmentTargetOrigin ident) = show ident
57−
58−data TypeConstraint
59− = TypeConstraint Int Type TypeConstraintOrigin
60− | RowConstraint Int Row TypeConstraintOrigin deriving (Show, D.Data, D.Typeable)
61−
62−newtype TypeSolution = TypeSolution { runTypeSolution :: (Int -> Type, Int -> Row) }
63−
64−emptyTypeSolution :: TypeSolution
65−emptyTypeSolution = TypeSolution (TUnknown, RUnknown)
47+instance Unifiable Type where
48+ unknown = TUnknown
49+ isUnknown (TUnknown u) = Just u
50+ isUnknown _ = Nothing
51+ TUnknown u1 ~~ TUnknown u2 | u1 == u2 = return ()
52+ TUnknown u ~~ t = replace u t
53+ t ~~ TUnknown u = replace u t
54+ SaturatedTypeSynonym name1 args1 ~~ SaturatedTypeSynonym name2 args2 | name1 == name2 =
55+ zipWithM_ (~~) args1 args2
56+ SaturatedTypeSynonym name args ~~ ty = do
57+ env <- lift getEnv
58+ modulePath <- checkModulePath `fmap` lift get
59+ case M.lookup (qualify modulePath name) (typeSynonyms env) of
60+ Just (synArgs, body) -> do
61+ let m = M.fromList $ zip synArgs args
62+ let replaced = replaceTypeVars m body
63+ replaced ~~ ty
64+ Nothing -> error "Type synonym was not defined"
65+ ty ~~ s@(SaturatedTypeSynonym _ _) = s ~~ ty
66+ ForAll idents ty1 ~~ ty2 = do
67+ sk <- skolemize idents ty1
68+ sk ~~ ty2
69+ ty ~~ f@(ForAll _ _) = f ~~ ty
70+ Number ~~ Number = return ()
71+ String ~~ String = return ()
72+ Boolean ~~ Boolean = return ()
73+ Array s ~~ Array t = s ~~ t
74+ Object row1 ~~ Object row2 = row1 ~~ row2
75+ Function args1 ret1 ~~ Function args2 ret2 = do
76+ guardWith "Function applied to incorrect number of args" $ length args1 == length args2
77+ zipWithM_ (~~) args1 args2
78+ ret1 ~~ ret2
79+ TypeVar v1 ~~ TypeVar v2 | v1 == v2 = return ()
80+ TypeConstructor c1 ~~ TypeConstructor c2 = do
81+ modulePath <- checkModulePath `fmap` lift get
82+ guardWith ("Cannot unify " ++ show c1 ++ " with " ++ show c2 ++ ".") (qualify modulePath c1 == qualify modulePath c2)
83+ TypeApp t1 t2 ~~ TypeApp t3 t4 = do
84+ t1 ~~ t3
85+ t2 ~~ t4
86+ Skolem s1 ~~ Skolem s2 | s1 == s2 = return ()
87+ t1 ~~ t2 = throwError $ "Cannot unify " ++ prettyPrintType t1 ++ " with " ++ prettyPrintType t2 ++ "."
88+ apply s (TUnknown u) = runSubstitution s u
89+ apply s (SaturatedTypeSynonym name tys) = SaturatedTypeSynonym name $ map (apply s) tys
90+ apply s (ForAll idents ty) = ForAll idents $ apply s ty
91+ apply s (Array t) = Array (apply s t)
92+ apply s (Object r) = Object (apply s r)
93+ apply s (Function args ret) = Function (map (apply s) args) (apply s ret)
94+ apply s (TypeApp t1 t2) = TypeApp (apply s t1) (apply s t2)
95+ apply _ t = t
96+ unknowns (TUnknown (Unknown u)) = [u]
97+ unknowns (SaturatedTypeSynonym _ tys) = concatMap unknowns tys
98+ unknowns (ForAll idents ty) = unknowns ty
99+ unknowns (Array t) = unknowns t
100+ unknowns (Object r) = unknowns r
101+ unknowns (Function args ret) = concatMap unknowns args ++ unknowns ret
102+ unknowns (TypeApp t1 t2) = unknowns t1 ++ unknowns t2
103+ unknowns _ = []
104+
105+instance Unifiable Row where
106+ unknown = RUnknown
107+ isUnknown (RUnknown u) = Just u
108+ isUnknown _ = Nothing
109+ r1 ~~ r2 =
110+ let
111+ (s1, r1') = rowToList r1
112+ (s2, r2') = rowToList r2
113+ int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
114+ sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
115+ sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
116+ in do
117+ forM_ int (uncurry (~~))
118+ unifyRows sd1 r1' sd2 r2'
119+ where
120+ unifyRows :: [(String, Type)] -> Row -> [(String, Type)] -> Row -> Subst Check ()
121+ unifyRows [] (RUnknown u) sd r = replace u (rowFromList (sd, r))
122+ unifyRows sd r [] (RUnknown u) = replace u (rowFromList (sd, r))
123+ unifyRows ns@((name, ty):row) r others u@(RUnknown un) = do
124+ occursCheck un ty
125+ forM row $ \(_, ty) -> occursCheck un ty
126+ u' <- fresh
127+ u ~~ RCons name ty u'
128+ unifyRows row r others u'
129+ unifyRows [] REmpty [] REmpty = return ()
130+ unifyRows [] (RowVar v1) [] (RowVar v2) | v1 == v2 = return ()
131+ unifyRows sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd1, r1)) ++ " with " ++ prettyPrintRow (rowFromList (sd2, r2)) ++ "."
132+ apply s (RUnknown u) = runSubstitution s u
133+ apply s (RCons name ty r) = RCons name (apply s ty) (apply s r)
134+ apply _ r = r
135+ unknowns (RUnknown (Unknown u)) = [u]
136+ unknowns (RCons _ ty r) = unknowns ty ++ unknowns r
137+ unknowns _ = []
66138
67139isFunction :: Value -> Bool
68140isFunction (Abs _ _) = True
69141isFunction (TypedValue untyped _) = isFunction untyped
70142isFunction _ = False
71143
72−allConstraints :: Ident -> Value -> Check ([TypeConstraint], Int)
73−allConstraints name val | isFunction val = do
74− me <- fresh
75− (cs, n) <- typeConstraints (M.singleton name me) val
76− return (TypeConstraint me (TUnknown n) (ValueOrigin val): cs, n)
77−allConstraints _ val = typeConstraints M.empty val
78−
79−typeOf :: Ident -> Value -> Check Type
144+typeOf :: Maybe Ident -> Value -> Check Type
80145typeOf name val = do
81− (cs, n) <- allConstraints name val
82− desugared <- replaceAllTypeSynonyms cs
83− solution <- solveTypeConstraints desugared emptyTypeSolution
84− let ty = fst (runTypeSolution solution) n
85− allUnknownsBecameQuantified desugared solution ty
146+ ty <- runSubst $ case name of
147+ Just ident -> do me <- fresh
148+ ty <- infer (M.singleton ident me) val
149+ me ~~ ty
150+ return ty
151+ Nothing -> infer M.empty val
152+ --desugared <- replaceAllTypeSynonyms cs
153+ --TODO: allUnknownsBecameQuantified desugared solution ty
86154 return $ varIfUnknown $ desaturateAllTypeSynonyms $ setifyAll ty
87155
156+{-
88157allUnknownsBecameQuantified :: [TypeConstraint] -> TypeSolution -> Type -> Check ()
89158allUnknownsBecameQuantified cs solution ty = do
90159 let
@@ -102,19 +171,27 @@ allUnknownsBecameQuantified cs solution ty = do
102171 unsolvedRows = filter (\n -> RUnknown n == snd (runTypeSolution solution) n) unknownRows
103172 guardWith "Unsolved row variable" $ null $ unsolvedRows \\ rowsMentioned
104173
174+findUnknownTypes :: (D.Data d) => d -> [Unknown Type]
175+findUnknownTypes = everything (++) (mkQ [] f)
176+ where
177+ f :: Type -> [Unknown Type]
178+ f (TUnknown n) = [n]
179+ f _ = []
180+
181+findUnknownRows :: (D.Data d) => d -> [Unknown Row]
182+findUnknownRows = everything (++) (mkQ [] f)
183+ where
184+ f :: Row -> [Unknown Row]
185+ f (RUnknown n) = [n]
186+ f _ = []
187+-}
188+
105189setify :: Row -> Row
106190setify = rowFromList . first (M.toList . M.fromList) . rowToList
107191
108192setifyAll :: (D.Data d) => d -> d
109193setifyAll = everywhere (mkT setify)
110194
111−findUnknownTypes :: (D.Data d) => d -> [Int]
112−findUnknownTypes = everything (++) (mkQ [] f)
113− where
114− f :: Type -> [Int]
115− f (TUnknown n) = [n]
116− f _ = []
117−
118195findTypeVars :: (D.Data d) => d -> [String]
119196findTypeVars = everything (++) (mkQ [] f)
120197 where
@@ -122,13 +199,6 @@ findTypeVars = everything (++) (mkQ [] f)
122199 f (TypeVar v) = [v]
123200 f _ = []
124201
125−findUnknownRows :: (D.Data d) => d -> [Int]
126−findUnknownRows = everything (++) (mkQ [] f)
127− where
128− f :: Row -> [Int]
129− f (RUnknown n) = [n]
130− f _ = []
131−
132202varIfUnknown :: Type -> Type
133203varIfUnknown ty =
134204 let
@@ -137,7 +207,7 @@ varIfUnknown ty =
137207 ForAll (sort $ nub $ M.elems m ++ findTypeVars ty) ty'
138208 where
139209 f :: Type -> State (M.Map Int String) Type
140− f (TUnknown n) = do
210+ f (TUnknown (Unknown n)) = do
141211 m <- get
142212 case M.lookup n m of
143213 Nothing -> do
@@ -147,7 +217,7 @@ varIfUnknown ty =
147217 Just name -> return $ TypeVar name
148218 f t = return t
149219 g :: Row -> State (M.Map Int String) Row
150− g (RUnknown n) = do
220+ g (RUnknown (Unknown n)) = do
151221 m <- get
152222 case M.lookup n m of
153223 Nothing -> do
@@ -165,28 +235,28 @@ replaceTypeVars m = everywhere (mkT replace)
165235 _ -> TypeVar v
166236 replace t = t
167237
168−replaceVarsWithUnknowns :: [String] -> Type -> Check Type
238+replaceVarsWithUnknowns :: [String] -> Type -> Subst Check Type
169239replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)
170240 where
171− f :: Type -> StateT (M.Map String Int) Check Type
241+ f :: Type -> StateT (M.Map String Int) (Subst Check) Type
172242 f (TypeVar var) | var `elem` idents = do
173243 m <- get
174− n <- lift fresh
244+ n <- lift fresh'
175245 case M.lookup var m of
176246 Nothing -> do
177247 put (M.insert var n m)
178− return $ TUnknown n
179− Just u -> return $ TUnknown u
248+ return $ TUnknown (Unknown n)
249+ Just u -> return $ TUnknown (Unknown u)
180250 f t = return t
181− g :: Row -> StateT (M.Map String Int) Check Row
251+ g :: Row -> StateT (M.Map String Int) (Subst Check) Row
182252 g (RowVar var) | var `elem` idents = do
183253 m <- get
184− n <- lift fresh
254+ n <- lift fresh'
185255 case M.lookup var m of
186256 Nothing -> do
187257 put (M.insert var n m)
188− return $ RUnknown n
189− Just u -> return $ RUnknown u
258+ return $ RUnknown (Unknown n)
259+ Just u -> return $ RUnknown (Unknown u)
190260 g r = return r
191261
192262replaceAllTypeSynonyms :: (D.Data d) => d -> Check d
@@ -201,443 +271,352 @@ desaturateAllTypeSynonyms = everywhere (mkT replace)
201271 replace (SaturatedTypeSynonym name args) = foldl TypeApp (TypeConstructor name) args
202272 replace t = t
203273
204−replaceType :: (D.Data d) => Int -> Type -> d -> d
205−replaceType n t = everywhere (mkT go)
206− where
207− go (TUnknown m) | m == n = t
208− go t = t
209−
210−replaceRow :: (D.Data d) => Int -> Row -> d -> d
211−replaceRow n r = everywhere (mkT go)
212− where
213− go (RUnknown m) | m == n = r
214− go r = r
215−
216−typeOccursCheck :: Int -> Type -> Check ()
217−typeOccursCheck u (TUnknown _) = return ()
218−typeOccursCheck u t = when (occursCheck u t) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintType t
219−
220−rowOccursCheck :: Int -> Row -> Check ()
221−rowOccursCheck u (RUnknown _) = return ()
222−rowOccursCheck u r = when (occursCheck u r) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintRow r
223−
224−occursCheck :: (D.Data d) => Int -> d -> Bool
225−occursCheck u = everything (||) $ flip extQ g $ mkQ False f
226− where
227− f (TUnknown u') | u' == u = True
228− f _ = False
229− g (RUnknown u') | u' == u = True
230− g _ = False
231−
232274ensureNoDuplicateProperties :: [(String, Value)] -> Check ()
233275ensureNoDuplicateProperties ps = guardWith "Duplicate property names" $ length (nub . map fst $ ps) == length ps
234276
235−typeConstraints :: M.Map Ident Int -> Value -> Check ([TypeConstraint], Int)
236−typeConstraints _ v@(NumericLiteral _) = do
237− me <- fresh
238− return ([TypeConstraint me Number (ValueOrigin v)], me)
239−typeConstraints _ v@(StringLiteral _) = do
240− me <- fresh
241− return ([TypeConstraint me String (ValueOrigin v)], me)
242−typeConstraints _ v@(BooleanLiteral _) = do
243− me <- fresh
244− return ([TypeConstraint me Boolean (ValueOrigin v)], me)
245−typeConstraints m v@(ArrayLiteral vals) = do
246− all <- mapM (typeConstraints m) vals
247− let (cs, ns) = (concatMap fst &&& map snd) all
248− me <- fresh
249− return (cs ++ zipWith (\n el -> TypeConstraint me (Array $ TUnknown n) (ValueOrigin el)) ns vals, me)
250−typeConstraints m u@(Unary op val) = do
251− (cs, n1) <- typeConstraints m val
252− me <- fresh
253− return (cs ++ unaryOperatorConstraints u op n1 me, me)
254−typeConstraints m b@(Binary op left right) = do
255− (cs1, n1) <- typeConstraints m left
256− (cs2, n2) <- typeConstraints m right
257− me <- fresh
258− return (cs1 ++ cs2 ++ binaryOperatorConstraints b op n1 n2 me, me)
259−typeConstraints m v@(ObjectLiteral ps) = do
260− ensureNoDuplicateProperties ps
261− all <- mapM (typeConstraints m . snd) ps
262− let (cs, ns) = (concatMap fst &&& map snd) all
263− me <- fresh
264− let tys = zipWith (\(name, _) u -> (name, TUnknown u)) ps ns
265− return (TypeConstraint me (Object (typesToRow tys)) (ValueOrigin v) : cs, me)
266−typeConstraints m v@(ObjectUpdate o ps) = do
267− ensureNoDuplicateProperties ps
268− (cs1, n1) <- typeConstraints m o
269− all <- mapM (typeConstraints m . snd) ps
270− let (cs2, ns) = (concatMap fst &&& map snd) all
277+infer :: M.Map Ident Type -> Value -> Subst Check Type
278+infer _ (NumericLiteral _) = return Number
279+infer _ (StringLiteral _) = return String
280+infer _ (BooleanLiteral _) = return Boolean
281+infer m (ArrayLiteral vals) = do
282+ ts <- mapM (infer m) vals
283+ arr <- fresh
284+ forM_ ts $ \t -> arr ~~ Array t
285+ return arr
286+infer m (Unary op val) = do
287+ t <- infer m val
288+ inferUnary op t
289+infer m (Binary op left right) = do
290+ t1 <- infer m left
291+ t2 <- infer m right
292+ inferBinary op t1 t2
293+infer m (ObjectLiteral ps) = do
294+ lift $ ensureNoDuplicateProperties ps
295+ ts <- mapM (infer m . snd) ps
296+ let fields = zipWith (\(name, _) t -> (name, t)) ps ts
297+ return $ Object $ typesToRow fields
298+infer m (ObjectUpdate o ps) = do
299+ lift $ ensureNoDuplicateProperties ps
300+ obj <- infer m o
271301 row <- fresh
272− let tys = zipWith (\(name, _) u -> (name, TUnknown u)) ps ns
273− return (TypeConstraint n1 (Object (rowFromList (tys, RUnknown row))) (ValueOrigin v) : cs1 ++ cs2, n1)
274−typeConstraints m v@(Indexer index val) = do
275− (cs1, n1) <- typeConstraints m index
276− (cs2, n2) <- typeConstraints m val
277− me <- fresh
278− return (TypeConstraint n1 Number (ValueOrigin index) : TypeConstraint n2 (Array (TUnknown me)) (ValueOrigin v) : cs1 ++ cs2, me)
279−typeConstraints m v@(Accessor prop val) = do
280− (cs, n1) <- typeConstraints m val
281− me <- fresh
302+ ts <- mapM (infer m . snd) ps
303+ let tys = zipWith (\(name, _) t -> (name, t)) ps ts
304+ obj ~~ Object (rowFromList (tys, row))
305+ return obj
306+infer m (Indexer index val) = do
307+ el <- fresh
308+ t1 <- infer m index
309+ t2 <- infer m val
310+ t1 ~~ Number
311+ t2 ~~ Array el
312+ return el
313+infer m (Accessor prop val) = do
314+ obj <- infer m val
315+ field <- fresh
282316 rest <- fresh
283− return (TypeConstraint n1 (Object (RCons prop (TUnknown me) (RUnknown rest))) (ValueOrigin v) : cs, me)
284−typeConstraints m v@(Abs args ret) = do
285− ns <- replicateM (length args) fresh
286− let m' = m `M.union` M.fromList (zip args ns)
287− (cs, n') <- typeConstraints m' ret
317+ obj ~~ Object (RCons prop field rest)
318+ return field
319+infer m v@(Abs args ret) = do
320+ ts <- replicateM (length args) fresh
321+ let m' = m `M.union` M.fromList (zip args ts)
322+ body <- infer m' ret
323+ return $ Function ts body
324+infer m v@(App f xs) = do
325+ t1 <- infer m f
326+ ts <- mapM (infer m) xs
288327 me <- fresh
289− return (TypeConstraint me (Function (map TUnknown ns) (TUnknown n')) (ValueOrigin v) : cs, me)
290−typeConstraints m v@(App f xs) = do
291− (cs1, n1) <- typeConstraints m f
292− all <- mapM (typeConstraints m) xs
293− let (cs2, ns) = (concatMap fst &&& map snd) all
294− me <- fresh
295− return (TypeConstraint n1 (Function (map TUnknown ns) (TUnknown me)) (ValueOrigin v) : cs1 ++ cs2, me)
296−typeConstraints m v@(Var var@(Qualified mp name)) = do
328+ t1 ~~ Function ts me
329+ return me
330+infer m v@(Var var@(Qualified mp name)) = do
297331 case mp of
298332 ModulePath [] ->
299333 case M.lookup name m of
300− Just u -> do
301− me <- fresh
302− return ([TypeConstraint u (TUnknown me) (ValueOrigin v)], me)
334+ Just ty -> lift $ replaceAllTypeSynonyms ty
303335 Nothing -> lookupGlobal
304336 _ -> lookupGlobal
305337 where
306338 lookupGlobal = do
307− env <- getEnv
308− modulePath <- checkModulePath `fmap` get
339+ env <- lift getEnv
340+ modulePath <- checkModulePath `fmap` lift get
309341 case M.lookup (qualify modulePath var) (names env) of
310342 Nothing -> throwError $ show var ++ " is undefined"
311− Just (ForAll idents ty, _) -> do
312− me <- fresh
313− replaced <- replaceVarsWithUnknowns idents ty
314− return ([TypeConstraint me replaced (ValueOrigin v)], me)
315−typeConstraints m (Block ss) = do
343+ Just (ty, _) -> lift $ replaceAllTypeSynonyms ty
344+infer m (Block ss) = do
316345 ret <- fresh
317− (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m M.empty ret ss
346+ (allCodePathsReturn, _) <- checkBlock m M.empty ret ss
318347 guardWith "Block is missing a return statement" allCodePathsReturn
319− return (cs, ret)
320−typeConstraints m v@(Constructor c) = do
321− env <- getEnv
322− modulePath <- checkModulePath `fmap` get
348+ return ret
349+infer m v@(Constructor c) = do
350+ env <- lift getEnv
351+ modulePath <- checkModulePath `fmap` lift get
323352 case M.lookup (qualify modulePath c) (dataConstructors env) of
324353 Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
325− Just (ForAll idents ty) -> do
326− me <- fresh
327− replaced <- replaceVarsWithUnknowns idents ty
328− return ([TypeConstraint me replaced (ValueOrigin v)], me)
329−typeConstraints m (Case val binders) = do
330− (cs1, n1) <- typeConstraints m val
354+ Just (ForAll idents ty) -> replaceVarsWithUnknowns idents ty
355+infer m (Case val binders) = do
356+ t1 <- infer m val
331357 ret <- fresh
332− cs2 <- typeConstraintsForBinders m n1 ret binders
333− return (cs1 ++ cs2, ret)
334−typeConstraints m v@(IfThenElse cond th el) = do
335− (cs1, n1) <- typeConstraints m cond
336− (cs2, n2) <- typeConstraints m th
337− (cs3, n3) <- typeConstraints m el
338− return (TypeConstraint n1 Boolean (ValueOrigin cond) : TypeConstraint n2 (TUnknown n3) (ValueOrigin v) : cs1 ++ cs2 ++ cs3, n2)
339−typeConstraints m v@(TypedValue val ty) = do
340− kind <- kindOf ty
358+ cs2 <- checkBinders m t1 ret binders
359+ return ret
360+infer m v@(IfThenElse cond th el) = do
361+ t1 <- infer m cond
362+ t2 <- infer m th
363+ t3 <- infer m el
364+ t1 ~~ Boolean
365+ t2 ~~ t3
366+ return t2
367+infer m v@(TypedValue val ty) = do
368+ kind <- lift $ kindOf ty
341369 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
342− typeCheck m val ty
343− me <- fresh
344− return ([TypeConstraint me ty (ValueOrigin v)], me)
345−
346−typeCheck :: M.Map Ident Int -> Value -> Type -> Check ()
347−typeCheck _ _ _ = return ()
348−
349−unaryOperatorConstraints :: Value -> UnaryOperator -> Int -> Int -> [TypeConstraint]
350−unaryOperatorConstraints v Negate val result = [TypeConstraint val Number (ValueOrigin v), TypeConstraint result Number (ValueOrigin v)]
351−unaryOperatorConstraints v Not val result = [TypeConstraint val Boolean (ValueOrigin v), TypeConstraint result Boolean (ValueOrigin v)]
352−unaryOperatorConstraints v BitwiseNot val result = [TypeConstraint val Number (ValueOrigin v), TypeConstraint result Number (ValueOrigin v)]
353−
354−binaryOperatorConstraints :: Value -> BinaryOperator -> Int -> Int -> Int -> [TypeConstraint]
355−binaryOperatorConstraints v Add = symBinOpConstraints v Number
356−binaryOperatorConstraints v Subtract = symBinOpConstraints v Number
357−binaryOperatorConstraints v Multiply = symBinOpConstraints v Number
358−binaryOperatorConstraints v Divide = symBinOpConstraints v Number
359−binaryOperatorConstraints v Modulus = symBinOpConstraints v Number
360−binaryOperatorConstraints v LessThan = asymBinOpConstraints v Number Boolean
361−binaryOperatorConstraints v LessThanOrEqualTo = asymBinOpConstraints v Number Boolean
362−binaryOperatorConstraints v GreaterThan = asymBinOpConstraints v Number Boolean
363−binaryOperatorConstraints v GreaterThanOrEqualTo = asymBinOpConstraints v Number Boolean
364−binaryOperatorConstraints v BitwiseAnd = symBinOpConstraints v Number
365−binaryOperatorConstraints v BitwiseOr = symBinOpConstraints v Number
366−binaryOperatorConstraints v BitwiseXor = symBinOpConstraints v Number
367−binaryOperatorConstraints v ShiftLeft = symBinOpConstraints v Number
368−binaryOperatorConstraints v ShiftRight = symBinOpConstraints v Number
369−binaryOperatorConstraints v ZeroFillShiftRight = symBinOpConstraints v Number
370−binaryOperatorConstraints v EqualTo = equalityBinOpConstraints v
371−binaryOperatorConstraints v NotEqualTo = equalityBinOpConstraints v
372−binaryOperatorConstraints v And = symBinOpConstraints v Boolean
373−binaryOperatorConstraints v Or = symBinOpConstraints v Boolean
374−binaryOperatorConstraints v Concat = symBinOpConstraints v String
375−
376−equalityBinOpConstraints :: Value -> Int -> Int -> Int -> [TypeConstraint]
377−equalityBinOpConstraints v left right result = [TypeConstraint left (TUnknown right) (ValueOrigin v), TypeConstraint result Boolean (ValueOrigin v)]
378−
379−symBinOpConstraints :: Value -> Type -> Int -> Int -> Int -> [TypeConstraint]
380−symBinOpConstraints v ty = asymBinOpConstraints v ty ty
381−
382−asymBinOpConstraints :: Value -> Type -> Type -> Int -> Int -> Int -> [TypeConstraint]
383−asymBinOpConstraints v ty res left right result = [TypeConstraint left ty (ValueOrigin v), TypeConstraint right ty (ValueOrigin v), TypeConstraint result res (ValueOrigin v)]
384−
385−typeConstraintsForBinder :: Int -> Binder -> Check ([TypeConstraint], M.Map Ident Int)
386−typeConstraintsForBinder _ NullBinder = return ([], M.empty)
387−typeConstraintsForBinder val b@(StringBinder _) = constantBinder b val String
388−typeConstraintsForBinder val b@(NumberBinder _) = constantBinder b val Number
389−typeConstraintsForBinder val b@(BooleanBinder _) = constantBinder b val Boolean
390−typeConstraintsForBinder val b@(VarBinder name) = do
391− me <- fresh
392− return ([TypeConstraint me (TUnknown val) (BinderOrigin b)], M.singleton name me)
393−typeConstraintsForBinder val b@(NullaryBinder ctor) = do
394− env <- getEnv
395− modulePath <- checkModulePath `fmap` get
370+ ty' <- lift $ replaceAllTypeSynonyms ty
371+ cs <- check m val ty'
372+ return ty'
373+
374+inferUnary :: UnaryOperator -> Type -> Subst Check Type
375+inferUnary Negate val = do
376+ val ~~ Number
377+ return Number
378+inferUnary Not val = do
379+ val ~~ Boolean
380+ return Boolean
381+inferUnary BitwiseNot val = do
382+ val ~~ Number
383+ return Number
384+
385+inferBinary :: BinaryOperator -> Type -> Type -> Subst Check Type
386+inferBinary Add = inferSymBinary Number
387+inferBinary Subtract = inferSymBinary Number
388+inferBinary Multiply = inferSymBinary Number
389+inferBinary Divide = inferSymBinary Number
390+inferBinary Modulus = inferSymBinary Number
391+inferBinary LessThan = inferAsymBinary Number Boolean
392+inferBinary LessThanOrEqualTo = inferAsymBinary Number Boolean
393+inferBinary GreaterThan = inferAsymBinary Number Boolean
394+inferBinary GreaterThanOrEqualTo = inferAsymBinary Number Boolean
395+inferBinary BitwiseAnd = inferSymBinary Number
396+inferBinary BitwiseOr = inferSymBinary Number
397+inferBinary BitwiseXor = inferSymBinary Number
398+inferBinary ShiftLeft = inferSymBinary Number
399+inferBinary ShiftRight = inferSymBinary Number
400+inferBinary ZeroFillShiftRight = inferSymBinary Number
401+inferBinary EqualTo = inferEqBinary
402+inferBinary NotEqualTo = inferEqBinary
403+inferBinary And = inferSymBinary Boolean
404+inferBinary Or = inferSymBinary Boolean
405+inferBinary Concat = inferSymBinary String
406+
407+inferEqBinary :: Type -> Type -> Subst Check Type
408+inferEqBinary left right = do
409+ left ~~ right
410+ return Boolean
411+
412+inferSymBinary :: Type -> Type -> Type -> Subst Check Type
413+inferSymBinary ty = inferAsymBinary ty ty
414+
415+inferAsymBinary :: Type -> Type -> Type -> Type -> Subst Check Type
416+inferAsymBinary input output left right = do
417+ left ~~ input
418+ right ~~ input
419+ return output
420+
421+inferBinder :: Type -> Binder -> Subst Check (M.Map Ident Type)
422+inferBinder _ NullBinder = return M.empty
423+inferBinder val (StringBinder _) = val ~~ String >> return M.empty
424+inferBinder val (NumberBinder _) = val ~~ Number >> return M.empty
425+inferBinder val (BooleanBinder _) = val ~~ Boolean >> return M.empty
426+inferBinder val (VarBinder name) = return $ M.singleton name val
427+inferBinder val (NullaryBinder ctor) = do
428+ env <- lift getEnv
429+ modulePath <- checkModulePath `fmap` lift get
396430 case M.lookup (qualify modulePath ctor) (dataConstructors env) of
397431 Just (ForAll args ret) -> do
398432 ret' <- replaceVarsWithUnknowns args ret
399− return ([TypeConstraint val ret' (BinderOrigin b)], M.empty)
433+ val ~~ ret'
434+ return M.empty
400435 _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
401−typeConstraintsForBinder val b@(UnaryBinder ctor binder) = do
402− env <- getEnv
403− modulePath <- checkModulePath `fmap` get
436+inferBinder val b@(UnaryBinder ctor binder) = do
437+ env <- lift getEnv
438+ modulePath <- checkModulePath `fmap` lift get
404439 case M.lookup (qualify modulePath ctor) (dataConstructors env) of
405440 Just (ForAll idents f@(Function [_] _)) -> do
406441 obj <- fresh
407442 (Function [ty] ret) <- replaceVarsWithUnknowns idents f
408− (cs, m1) <- typeConstraintsForBinder obj binder
409− return (TypeConstraint val ret (BinderOrigin b) : TypeConstraint obj ty (BinderOrigin b) : cs, m1)
443+ m1 <- inferBinder obj binder
444+ val ~~ ret
445+ obj ~~ ty
446+ return m1
410447 Just _ -> throwError $ show ctor ++ " is not a unary constructor"
411448 _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
412−typeConstraintsForBinder val b@(ObjectBinder props) = do
449+inferBinder val b@(ObjectBinder props) = do
413450 row <- fresh
414451 rest <- fresh
415− (cs, m1) <- typeConstraintsForProperties row (RUnknown rest) props
416− return (TypeConstraint val (Object (RUnknown row)) (BinderOrigin b) : cs, m1)
452+ m1 <- inferRowProperties row rest props
453+ val ~~ Object row
454+ return m1
417455 where
418− typeConstraintsForProperties :: Int -> Row -> [(String, Binder)] -> Check ([TypeConstraint], M.Map Ident Int)
419− typeConstraintsForProperties nrow row [] = return ([RowConstraint nrow row (BinderOrigin b)], M.empty)
420− typeConstraintsForProperties nrow row ((name, binder):binders) = do
456+ inferRowProperties :: Row -> Row -> [(String, Binder)] -> Subst Check (M.Map Ident Type)
457+ inferRowProperties nrow row [] = nrow ~~ row >> return M.empty
458+ inferRowProperties nrow row ((name, binder):binders) = do
421459 propTy <- fresh
422− (cs1, m1) <- typeConstraintsForBinder propTy binder
423− (cs2, m2) <- typeConstraintsForProperties nrow (RCons name (TUnknown propTy) row) binders
424− return (cs1 ++ cs2, m1 `M.union` m2)
425−typeConstraintsForBinder val b@(ArrayBinder binders rest) = do
460+ m1 <- inferBinder propTy binder
461+ m2 <- inferRowProperties nrow (RCons name propTy row) binders
462+ return $ m1 `M.union` m2
463+inferBinder val (ArrayBinder binders rest) = do
426464 el <- fresh
427− all <- mapM (typeConstraintsForBinder el) binders
428− let (cs1, m1) = (concatMap fst &&& M.unions . map snd) all
429− let arrayConstraint = TypeConstraint val (Array (TUnknown el)) (BinderOrigin b)
465+ m1 <- M.unions <$> mapM (inferBinder el) binders
466+ val ~~ Array el
430467 case rest of
431− Nothing -> return (arrayConstraint : cs1, m1)
468+ Nothing -> return m1
432469 Just binder -> do
433− (cs2, m2) <- typeConstraintsForBinder val binder
434− return (arrayConstraint : cs1 ++ cs2, m1 `M.union` m2)
435−typeConstraintsForBinder val b@(NamedBinder name binder) = do
436− me <- fresh
437− (cs, m) <- typeConstraintsForBinder val binder
438− return (TypeConstraint me (TUnknown val) (BinderOrigin b) : cs, M.insert name me m)
439−
440−typeConstraintsForGuardedBinder :: M.Map Ident Int -> Int -> Binder -> Check ([TypeConstraint], M.Map Ident Int)
441−typeConstraintsForGuardedBinder m val b@(GuardedBinder cond binder) = do
442− (cs1, m1) <- typeConstraintsForBinder val binder
443− (cs2, n) <- typeConstraints (m `M.union` m1) cond
444− return (TypeConstraint n Boolean (ValueOrigin cond) : cs1 ++ cs2, m1)
445−typeConstraintsForGuardedBinder m val b = typeConstraintsForBinder val b >>= return
446−
447−constantBinder :: Binder -> Int -> Type -> Check ([TypeConstraint], M.Map Ident Int)
448−constantBinder b val ty = return ([TypeConstraint val ty (BinderOrigin b)], M.empty)
449−
450−typeConstraintsForBinders :: M.Map Ident Int -> Int -> Int -> [(Binder, Value)] -> Check [TypeConstraint]
451−typeConstraintsForBinders _ _ _ [] = return []
452−typeConstraintsForBinders m nval ret ((binder, val):bs) = do
453− (cs1, m1) <- typeConstraintsForGuardedBinder m nval binder
454− (cs2, n2) <- typeConstraints (m `M.union` m1) val
455− cs3 <- typeConstraintsForBinders m nval ret bs
456− return (TypeConstraint n2 (TUnknown ret) (BinderOrigin binder) : cs1 ++ cs2 ++ cs3)
457−
458−assignVariable :: Ident -> M.Map Ident Int -> Check ()
470+ m2 <- inferBinder val binder
471+ return $ m1 `M.union` m2
472+inferBinder val (NamedBinder name binder) = do
473+ m <- inferBinder val binder
474+ return $ M.insert name val m
475+
476+inferGuardedBinder :: M.Map Ident Type -> Type -> Binder -> Subst Check (M.Map Ident Type)
477+inferGuardedBinder m val b@(GuardedBinder cond binder) = do
478+ m1 <- inferBinder val binder
479+ ty <- infer (m `M.union` m1) cond
480+ ty ~~ Boolean
481+ return m1
482+inferGuardedBinder m val b = inferBinder val b >>= return
483+
484+checkBinders :: M.Map Ident Type -> Type -> Type -> [(Binder, Value)] -> Subst Check ()
485+checkBinders _ _ _ [] = return ()
486+checkBinders m nval ret ((binder, val):bs) = do
487+ m1 <- inferGuardedBinder m nval binder
488+ t <- infer (m `M.union` m1) val
489+ t ~~ ret
490+ checkBinders m nval ret bs
491+
492+assignVariable :: Ident -> M.Map Ident Type -> Subst Check ()
459493assignVariable name m =
460494 case M.lookup name m of
461495 Nothing -> return ()
462496 Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."
463497
464−typeConstraintsForStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> Statement -> Check ([TypeConstraint], Bool, M.Map Ident Int)
465−typeConstraintsForStatement m mass ret (VariableIntroduction name val) = do
498+checkStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> Statement -> Subst Check (Bool, M.Map Ident Type)
499+checkStatement m mass ret (VariableIntroduction name val) = do
466500 assignVariable name (m `M.union` mass)
467− (cs1, n1) <- typeConstraints m val
468− return (cs1, False, M.insert name n1 mass)
469−typeConstraintsForStatement m mass ret (Assignment ident val) = do
470− (cs1, n1) <- typeConstraints m val
501+ t <- infer m val
502+ return (False, M.insert name t mass)
503+checkStatement m mass ret (Assignment ident val) = do
504+ t <- infer m val
471505 case M.lookup ident mass of
472506 Nothing -> throwError $ "No local variable with name " ++ show ident
473− Just ty ->
474− return (TypeConstraint n1 (TUnknown ty) (AssignmentTargetOrigin ident) : cs1, False, mass)
475−typeConstraintsForStatement m mass ret (While val inner) = do
476− (cs1, n1) <- typeConstraints m val
477− (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret inner
478− return (TypeConstraint n1 Boolean (ValueOrigin val) : cs1 ++ cs2, allCodePathsReturn, mass)
479−typeConstraintsForStatement m mass ret (If ifst) = do
480− (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
481− return (cs, allCodePathsReturn, mass)
482−typeConstraintsForStatement m mass ret (For ident start end inner) = do
507+ Just ty -> do t ~~ ty
508+ return (False, mass)
509+checkStatement m mass ret (While val inner) = do
510+ t1 <- infer m val
511+ t1 ~~ Boolean
512+ (allCodePathsReturn, _) <- checkBlock m mass ret inner
513+ return (allCodePathsReturn, mass)
514+checkStatement m mass ret (If ifst) = do
515+ allCodePathsReturn <- checkIfStatement m mass ret ifst
516+ return (allCodePathsReturn, mass)
517+checkStatement m mass ret (For ident start end inner) = do
483518 assignVariable ident (m `M.union` mass)
484− (cs1, n1) <- typeConstraints (m `M.union` mass) start
485− (cs2, n2) <- typeConstraints (m `M.union` mass) end
486− let mass1 = M.insert ident n1 mass
487− (cs3, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass1) mass1 ret inner
488− return (TypeConstraint n1 Number (ValueOrigin start) : TypeConstraint n2 Number (ValueOrigin end) : cs1 ++ cs2 ++ cs3, allCodePathsReturn, mass)
489−typeConstraintsForStatement m mass ret (ForEach ident vals inner) = do
519+ t1 <- infer (m `M.union` mass) start
520+ t1 ~~ Number
521+ t2 <- infer (m `M.union` mass) end
522+ t2 ~~ Number
523+ let mass1 = M.insert ident Number mass
524+ (allCodePathsReturn, _) <- checkBlock (m `M.union` mass1) mass1 ret inner
525+ return (allCodePathsReturn, mass)
526+checkStatement m mass ret (ForEach ident vals inner) = do
490527 assignVariable ident (m `M.union` mass)
491528 val <- fresh
492− (cs1, n1) <- typeConstraints (m `M.union` mass) vals
529+ t1 <- infer (m `M.union` mass) vals
530+ t1 ~~ Array val
493531 let mass1 = M.insert ident val mass
494− (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass1) mass1 ret inner
532+ (allCodePathsReturn, _) <- checkBlock (m `M.union` mass1) mass1 ret inner
495533 guardWith "Cannot return from within a foreach block" $ not allCodePathsReturn
496− return (TypeConstraint n1 (Array (TUnknown val)) (ValueOrigin vals) : cs1 ++ cs2, False, mass)
497−typeConstraintsForStatement m mass ret (Return val) = do
498− (cs1, n1) <- typeConstraints (m `M.union` mass) val
499− return (TypeConstraint n1 (TUnknown ret) (ValueOrigin val) : cs1, True, mass)
500−
501−typeConstraintsForIfStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> IfStatement -> Check ([TypeConstraint], Bool)
502−typeConstraintsForIfStatement m mass ret (IfStatement val thens Nothing) = do
503− (cs1, n1) <- typeConstraints m val
504− (cs2, _, _) <- typeConstraintsForBlock m mass ret thens
505− return (TypeConstraint n1 Boolean (ValueOrigin val) : cs1 ++ cs2, False)
506−typeConstraintsForIfStatement m mass ret (IfStatement val thens (Just elses)) = do
507− (cs1, n1) <- typeConstraints m val
508− (cs2, allCodePathsReturn1, _) <- typeConstraintsForBlock m mass ret thens
509− (cs3, allCodePathsReturn2) <- typeConstraintsForElseStatement m mass ret elses
510− return (TypeConstraint n1 Boolean (ValueOrigin val) : cs1 ++ cs2 ++ cs3, allCodePathsReturn1 && allCodePathsReturn2)
511−
512−typeConstraintsForElseStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> ElseStatement -> Check ([TypeConstraint], Bool)
513−typeConstraintsForElseStatement m mass ret (Else elses) = do
514− (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret elses
515− return (cs, allCodePathsReturn)
516−typeConstraintsForElseStatement m mass ret (ElseIf ifst) = do
517− (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
518− return (cs, allCodePathsReturn)
519−
520−typeConstraintsForBlock :: M.Map Ident Int -> M.Map Ident Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, M.Map Ident Int)
521−typeConstraintsForBlock _ mass _ [] = return ([], False, mass)
522−typeConstraintsForBlock m mass ret (s:ss) = do
523− (cs1, b1, mass1) <- typeConstraintsForStatement (m `M.union` mass) mass ret s
534+ return (False, mass)
535+checkStatement m mass ret (Return val) = do
536+ check (m `M.union` mass) val ret
537+ return (True, mass)
538+
539+checkIfStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> IfStatement -> Subst Check Bool
540+checkIfStatement m mass ret (IfStatement val thens Nothing) = do
541+ t1 <- infer m val
542+ t1 ~~ Boolean
543+ _ <- checkBlock m mass ret thens
544+ return False
545+checkIfStatement m mass ret (IfStatement val thens (Just elses)) = do
546+ t1 <- infer m val
547+ t1 ~~ Boolean
548+ (allCodePathsReturn1, _) <- checkBlock m mass ret thens
549+ allCodePathsReturn2 <- checkElseStatement m mass ret elses
550+ return $ allCodePathsReturn1 && allCodePathsReturn2
551+
552+checkElseStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> ElseStatement -> Subst Check Bool
553+checkElseStatement m mass ret (Else elses) = fst <$> checkBlock m mass ret elses
554+checkElseStatement m mass ret (ElseIf ifst) = checkIfStatement m mass ret ifst
555+
556+checkBlock :: M.Map Ident Type -> M.Map Ident Type -> Type -> [Statement] -> Subst Check (Bool, M.Map Ident Type)
557+checkBlock _ mass _ [] = return (False, mass)
558+checkBlock m mass ret (s:ss) = do
559+ (b1, mass1) <- checkStatement (m `M.union` mass) mass ret s
524560 case (b1, ss) of
525− (True, []) -> return (cs1, True, mass1)
561+ (True, []) -> return (True, mass1)
526562 (True, _) -> throwError "Unreachable code"
527563 (False, ss) -> do
528− (cs2, b2, mass2) <- typeConstraintsForBlock m mass1 ret ss
529− return (cs1 ++ cs2, b2, mass2)
530−
531−solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
532−solveTypeConstraints [] s = return s
533−solveTypeConstraints all@(TypeConstraint n t o:cs) s = do
534− (cs', s') <- rethrow (\err -> "Error in " ++ prettyPrintOrigin o ++ ": " ++ err) $ do
535− typeOccursCheck n t
536− let s' = let (f, g) = runTypeSolution s
537− in TypeSolution (replaceType n t . f, replaceType n t . g)
538− cs' <- fmap concat $ mapM (substituteTypeInConstraint n t) cs
539− return (cs', s')
540− solveTypeConstraints cs' s'
541−solveTypeConstraints (RowConstraint n r o:cs) s = do
542− (cs', s') <- rethrow (\err -> "Error in " ++ prettyPrintOrigin o ++ ": " ++ err) $ do
543− rowOccursCheck n r
544− let s' = let (f, g) = runTypeSolution s
545− in TypeSolution (replaceRow n r . f, replaceRow n r . g)
546− cs' <- fmap concat $ mapM (substituteRowInConstraint n r) cs
547− return (cs', s')
548− solveTypeConstraints cs' s'
549−
550−substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
551−substituteTypeInConstraint n s (TypeConstraint m t v)
552− | n == m = unifyTypes v s t
553− | otherwise = return [TypeConstraint m (replaceType n s t) v]
554−substituteTypeInConstraint n s (RowConstraint m r v)
555− = return [RowConstraint m (replaceType n s r) v]
556−
557−substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
558−substituteRowInConstraint n r (TypeConstraint m t v)
559− = return [TypeConstraint m (replaceRow n r t) v]
560−substituteRowInConstraint n r (RowConstraint m r1 v)
561− | m == n = unifyRows v r r1
562− | otherwise = return [RowConstraint m (replaceRow n r r1) v]
563−
564−unifyTypes :: TypeConstraintOrigin -> Type -> Type -> Check [TypeConstraint]
565−unifyTypes _ (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
566−unifyTypes o (TUnknown u) t = do
567− typeOccursCheck u t
568− return [TypeConstraint u t o]
569−unifyTypes o t (TUnknown u) = do
570− typeOccursCheck u t
571− return [TypeConstraint u t o]
572−unifyTypes o (SaturatedTypeSynonym name1 args1) (SaturatedTypeSynonym name2 args2) | name1 == name2 =
573− fmap concat $ zipWithM (unifyTypes o) args1 args2
574−unifyTypes o (SaturatedTypeSynonym name args) ty = do
575− env <- getEnv
576− modulePath <- checkModulePath `fmap` get
577− case M.lookup (qualify modulePath name) (typeSynonyms env) of
578− Just (synArgs, body) -> do
579− let m = M.fromList $ zip synArgs args
580− let replaced = replaceTypeVars m body
581− unifyTypes o replaced ty
582− Nothing -> error "Type synonym was not defined"
583−unifyTypes o ty s@(SaturatedTypeSynonym _ _) = unifyTypes o s ty
584−unifyTypes o (ForAll idents ty1) ty2 =do
585− sk <- skolemize idents ty1
586− unifyTypes o sk ty2
587−unifyTypes o ty f@(ForAll _ _) = unifyTypes o f ty
588−unifyTypes _ Number Number = return []
589−unifyTypes _ String String = return []
590−unifyTypes _ Boolean Boolean = return []
591−unifyTypes o (Array s) (Array t) = unifyTypes o s t
592−unifyTypes o (Object row1) (Object row2) = unifyRows o row1 row2
593−unifyTypes o (Function args1 ret1) (Function args2 ret2) = do
594− guardWith "Function applied to incorrect number of args" $ length args1 == length args2
595− cs1 <- fmap concat $ zipWithM (unifyTypes o) args1 args2
596− cs2 <- unifyTypes o ret1 ret2
597− return $ cs1 ++ cs2
598−unifyTypes _ (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
599−unifyTypes _ (TypeConstructor c1) (TypeConstructor c2) = do
600− modulePath <- checkModulePath `fmap` get
601− guardWith ("Cannot unify " ++ show c1 ++ " with " ++ show c2 ++ ".") (qualify modulePath c1 == qualify modulePath c2)
602− return []
603−unifyTypes o (TypeApp t1 t2) (TypeApp t3 t4) = do
604− cs1 <- unifyTypes o t1 t3
605− cs2 <- unifyTypes o t2 t4
606− return $ cs1 ++ cs2
607−unifyTypes _ (Skolem s1) (Skolem s2) | s1 == s2 = return []
608−unifyTypes _ t1 t2 = throwError $ "Cannot unify " ++ prettyPrintType t1 ++ " with " ++ prettyPrintType t2 ++ "."
609−
610−unifyRows :: TypeConstraintOrigin -> Row -> Row -> Check [TypeConstraint]
611−unifyRows o r1 r2 =
612− let
613− (s1, r1') = rowToList r1
614− (s2, r2') = rowToList r2
615− int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
616− sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
617− sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
618− in do
619− cs1 <- fmap concat $ mapM (uncurry $ unifyTypes o) int
620− cs2 <- unifyRows' o sd1 r1' sd2 r2'
621− return $ cs1 ++ cs2
622− where
623− unifyRows' :: TypeConstraintOrigin -> [(String, Type)] -> Row -> [(String, Type)] -> Row -> Check [TypeConstraint]
624− unifyRows' o [] (RUnknown u) sd r = do
625− rowOccursCheck u r
626− return [RowConstraint u (rowFromList (sd, r)) o]
627− unifyRows' o sd r [] (RUnknown u) = do
628− rowOccursCheck u r
629− return [RowConstraint u (rowFromList (sd, r)) o]
630− unifyRows' o ns@((name, ty):row) r others (RUnknown u) | not (occursCheck u (ty, row)) = do
631− u' <- fresh
632− cs <- unifyRows' o row r others (RUnknown u')
633− return (RowConstraint u (RCons name ty (RUnknown u')) o : cs)
634− unifyRows' _ [] REmpty [] REmpty = return []
635− unifyRows' _ [] (RowVar v1) [] (RowVar v2) | v1 == v2 = return []
636− unifyRows' _ sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd1, r1)) ++ " with " ++ prettyPrintRow (rowFromList (sd2, r2)) ++ "."
637−
638−skolemize :: [String] -> Type -> Check Type
564+ (b2, mass2) <- checkBlock m mass1 ret ss
565+ return (b2, mass2)
566+
567+skolemize :: [String] -> Type -> Subst Check Type
639568skolemize idents ty = do
640− sks <- replicateM (length idents) fresh
569+ sks <- replicateM (length idents) fresh'
641570 let m = M.fromList (zip idents (map Skolem sks))
642571 return $ replaceTypeVars m ty
643572
573+check :: M.Map Ident Type -> Value -> Type -> Subst Check ()
574+check m (NumericLiteral _) Number = return ()
575+check m (StringLiteral _) String = return ()
576+check m (BooleanLiteral _) Boolean = return ()
577+check m (Unary Negate val) Number = check m val Number
578+check m (Unary Not val) Boolean = check m val Boolean
579+check m (Unary BitwiseNot val) Number = check m val Number
580+check m (Binary _ t1 t2) Number = check m t1 Number >> check m t2 Number
581+check m (ArrayLiteral vals) (Array ty) = forM_ vals (\val -> check m val ty)
582+check m (Indexer index vals) ty = check m index Number >> check m vals (Array ty)
583+check m (Abs args ret) (Function argTys retTy) = do
584+ guardWith "Incorrect number of function arguments" (length args == length argTys)
585+ let bindings = M.fromList (zip args argTys)
586+ check (bindings `M.union` m) ret retTy
587+check m (App f xs) ret = do
588+ ft <- infer m f
589+ checkFunctionApplication m ft xs ret
590+check m val (ForAll idents ty) = do
591+ sk <- skolemize idents ty
592+ check m val sk
593+check m val u@(TUnknown _) = do
594+ t <- infer m val
595+ t ~~ u
596+check _ val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty
597+
598+checkFunctionApplication :: M.Map Ident Type -> Type -> [Value] -> Type -> Subst Check ()
599+checkFunctionApplication m (Function argTys retTy) args ret = do
600+ guardWith "Incorrect number of function arguments" (length args == length argTys)
601+ zipWithM (check m) args argTys
602+ ret ~~ retTy
603+checkFunctionApplication m (ForAll idents ty) args ret = do
604+ replaced <- replaceVarsWithUnknowns idents ty
605+ checkFunctionApplication m replaced args ret
606+checkFunctionApplication _ fnTy args ret = throwError $ "Cannot apply function of type "
607+ ++ prettyPrintType fnTy
608+ ++ " to arguments " ++ intercalate ", " (map prettyPrintValue args)
609+ ++ ". Expecting value of type " ++ prettyPrintType ret ++ "."
610+
611+{-
612+ | Binary BinaryOperator Value Value
613+ | ObjectLiteral [(String, Value)]
614+ | Accessor String Value
615+ | ObjectUpdate Value [(String, Value)]
616+ | Var (Qualified Ident)
617+ | IfThenElse Value Value Value
618+ | Block [Statement]
619+ | Constructor (Qualified ProperName)
620+ | Case Value [(Binder, Value)]
621+ | TypedValue Value PolyType
622+-}