@@ -0,0 +1,750 @@
1+-----------------------------------------------------------------------------
2+--
3+-- Module : Language.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+-----------------------------------------------------------------------------
14+
15+{-# LANGUAGE DeriveDataTypeable #-}
16+
17+module Language.PureScript.TypeChecker.Types (
18+ typeOf
19+) where
20+
21+import Data.List
22+import Data.Maybe (isJust, fromMaybe)
23+import Data.Function
24+import qualified Data.Data as D
25+import Data.Generics (everywhere, everywhereM, everything, everywhereBut, mkT, mkM, mkQ, extM, extQ)
26+
27+import Language.PureScript.Values
28+import Language.PureScript.Types
29+import Language.PureScript.Kinds
30+import Language.PureScript.Names
31+import Language.PureScript.TypeChecker.Monad
32+import Language.PureScript.TypeChecker.Kinds
33+import Language.PureScript.TypeChecker.Synonyms
34+import Language.PureScript.Pretty
35+import Language.PureScript.Unknown
36+
37+import Control.Monad.State
38+import Control.Monad.Error
39+
40+import Control.Applicative
41+import Control.Arrow (Arrow(..), Kleisli(..), (***), (&&&), second)
42+import qualified Control.Category as C
43+
44+import qualified Data.Map as M
45+
46+instance Unifiable Type where
47+ unknown = TUnknown
48+ isUnknown (TUnknown u) = Just u
49+ isUnknown _ = Nothing
50+ (~~) = unifyTypes
51+ apply s (TUnknown u) = runSubstitution s u
52+ apply s (SaturatedTypeSynonym name tys) = SaturatedTypeSynonym name $ map (apply s) tys
53+ apply s (ForAll idents ty) = ForAll idents $ apply s ty
54+ apply s (Array t) = Array (apply s t)
55+ apply s (Object r) = Object (apply s r)
56+ apply s (Function args ret) = Function (map (apply s) args) (apply s ret)
57+ apply s (TypeApp t1 t2) = TypeApp (apply s t1) (apply s t2)
58+ apply _ t = t
59+ unknowns (TUnknown (Unknown u)) = [u]
60+ unknowns (SaturatedTypeSynonym _ tys) = concatMap unknowns tys
61+ unknowns (ForAll idents ty) = unknowns ty
62+ unknowns (Array t) = unknowns t
63+ unknowns (Object r) = unknowns r
64+ unknowns (Function args ret) = concatMap unknowns args ++ unknowns ret
65+ unknowns (TypeApp t1 t2) = unknowns t1 ++ unknowns t2
66+ unknowns _ = []
67+
68+instance Unifiable Row where
69+ unknown = RUnknown
70+ isUnknown (RUnknown u) = Just u
71+ isUnknown _ = Nothing
72+ r1 ~~ r2 =
73+ let
74+ (s1, r1') = rowToList r1
75+ (s2, r2') = rowToList r2
76+ int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
77+ sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
78+ sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
79+ in do
80+ forM_ int (uncurry (~~))
81+ unifyRows sd1 r1' sd2 r2'
82+ where
83+ unifyRows :: [(String, Type)] -> Row -> [(String, Type)] -> Row -> Subst Check ()
84+ unifyRows [] (RUnknown u) sd r = replace u (rowFromList (sd, r))
85+ unifyRows sd r [] (RUnknown u) = replace u (rowFromList (sd, r))
86+ unifyRows ns@((name, ty):row) r others u@(RUnknown un) = do
87+ occursCheck un ty
88+ forM row $ \(_, ty) -> occursCheck un ty
89+ u' <- fresh
90+ u ~~ RCons name ty u'
91+ unifyRows row r others u'
92+ unifyRows [] REmpty [] REmpty = return ()
93+ unifyRows [] (RowVar v1) [] (RowVar v2) | v1 == v2 = return ()
94+ unifyRows [] (RSkolem s1) [] (RSkolem s2) | s1 == s2 = return ()
95+ unifyRows sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd1, r1)) ++ " with " ++ prettyPrintRow (rowFromList (sd2, r2)) ++ "."
96+ apply s (RUnknown u) = runSubstitution s u
97+ apply s (RCons name ty r) = RCons name (apply s ty) (apply s r)
98+ apply _ r = r
99+ unknowns (RUnknown (Unknown u)) = [u]
100+ unknowns (RCons _ ty r) = unknowns ty ++ unknowns r
101+ unknowns _ = []
102+
103+unifyTypes :: Type -> Type -> Subst Check ()
104+unifyTypes t1 t2 = rethrow (\e -> "Error unifying type " ++ prettyPrintType t1 ++ " with type " ++ prettyPrintType t2 ++ ":\n" ++ e) $ do
105+ unifyTypes' t1 t2
106+ where
107+ unifyTypes' (TUnknown u1) (TUnknown u2) | u1 == u2 = return ()
108+ unifyTypes' (TUnknown u) t = replace u t
109+ unifyTypes' t (TUnknown u) = replace u t
110+ unifyTypes' (SaturatedTypeSynonym name1 args1) (SaturatedTypeSynonym name2 args2)
111+ | name1 == name2 = zipWithM_ unifyTypes args1 args2
112+ unifyTypes' (SaturatedTypeSynonym name args) ty = do
113+ ty1 <- expandTypeSynonym name args
114+ ty1 `unifyTypes` ty
115+ unifyTypes' ty s@(SaturatedTypeSynonym _ _) = s `unifyTypes` ty
116+ unifyTypes' (ForAll ident1 ty1) (ForAll ident2 ty2) = do
117+ sk <- skolemize ident1 ty1
118+ replaced <- replaceVarsWithUnknowns [ident2] ty2
119+ sk `unifyTypes` replaced
120+ unifyTypes' (ForAll ident ty1) ty2 = do
121+ sk <- skolemize ident ty1
122+ sk `unifyTypes` ty2
123+ unifyTypes' ty f@(ForAll _ _) = f `unifyTypes` ty
124+ unifyTypes' Number Number = return ()
125+ unifyTypes' String String = return ()
126+ unifyTypes' Boolean Boolean = return ()
127+ unifyTypes' (Array s) (Array t) = s `unifyTypes` t
128+ unifyTypes' (Object row1) (Object row2) = row1 ~~ row2
129+ unifyTypes' (Function args1 ret1) (Function args2 ret2) = do
130+ guardWith "Function applied to incorrect number of args" $ length args1 == length args2
131+ zipWithM_ unifyTypes args1 args2
132+ ret1 `unifyTypes` ret2
133+ unifyTypes' (TypeVar v1) (TypeVar v2) | v1 == v2 = return ()
134+ unifyTypes' (TypeConstructor c1) (TypeConstructor c2) = do
135+ modulePath <- checkModulePath `fmap` lift get
136+ guardWith ("Cannot unify " ++ show c1 ++ " with " ++ show c2 ++ ".") (qualify modulePath c1 == qualify modulePath c2)
137+ unifyTypes' (TypeApp t1 t2) (TypeApp t3 t4) = do
138+ t1 `unifyTypes` t3
139+ t2 `unifyTypes` t4
140+ unifyTypes' (Skolem s1) (Skolem s2) | s1 == s2 = return ()
141+ unifyTypes' t1 t2 = throwError $ "Cannot unify " ++ prettyPrintType t1 ++ " with " ++ prettyPrintType t2 ++ "."
142+
143+isFunction :: Value -> Bool
144+isFunction (Abs _ _) = True
145+isFunction (TypedValue untyped _) = isFunction untyped
146+isFunction _ = False
147+
148+-- TODO: check skolems don't escape
149+typeOf :: Maybe Ident -> Value -> Check Type
150+typeOf name val = do
151+ (ty, sub, checks) <- runSubst $ case name of
152+ Just ident | isFunction val ->
153+ case val of
154+ TypedValue val ty -> do
155+ kind <- lift $ kindOf ty
156+ guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
157+ ty' <- lift $ replaceAllTypeSynonyms ty
158+ check (M.singleton ident ty) val ty'
159+ return ty'
160+ _ -> do
161+ me <- fresh
162+ ty <- infer (M.singleton ident me) val
163+ ty ~~ me
164+ return ty
165+ _ -> infer M.empty val
166+ escapeCheck checks ty sub
167+ return $ varIfUnknown $ desaturateAllTypeSynonyms $ setifyAll ty
168+
169+escapeCheck :: [AnyUnifiable] -> Type -> Substitution -> Check ()
170+escapeCheck checks ty sub =
171+ let
172+ visibleUnknowns = nub $ unknowns ty
173+ in
174+ forM_ checks $ \check -> case check of
175+ AnyUnifiable t -> do
176+ let unsolvedUnknowns = nub . unknowns $ apply sub t
177+ guardWith "Escape check fails" $ null $ unsolvedUnknowns \\ visibleUnknowns
178+
179+setify :: Row -> Row
180+setify = rowFromList . first (M.toList . M.fromList) . rowToList
181+
182+setifyAll :: (D.Data d) => d -> d
183+setifyAll = everywhere (mkT setify)
184+
185+varIfUnknown :: Type -> Type
186+varIfUnknown ty = mkForAll (sort . map ((:) 'u' . show) . nub $ unknowns ty) ty
187+
188+replaceAllTypeVars :: (D.Data d) => [(String, Type)] -> d -> d
189+replaceAllTypeVars = foldl' (\f (name, ty) -> replaceTypeVars name ty . f) id
190+
191+replaceTypeVars :: (D.Data d) => String -> Type -> d -> d
192+replaceTypeVars name t = everywhereBut (mkQ False isShadowed) (mkT replace)
193+ where
194+ replace (TypeVar v) | v == name = t
195+ replace t = t
196+ isShadowed (ForAll v _) | v == name = True
197+ isShadowed _ = False
198+
199+replaceRowVars :: (D.Data d) => String -> Row -> d -> d
200+replaceRowVars name r = everywhere (mkT replace)
201+ where
202+ replace (RowVar v) | v == name = r
203+ replace t = t
204+
205+replaceAllVarsWithUnknowns :: Type -> Subst Check Type
206+replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarsWithUnknowns [ident] ty >>= replaceAllVarsWithUnknowns
207+replaceAllVarsWithUnknowns ty = return ty
208+
209+replaceVarsWithUnknowns :: [String] -> Type -> Subst Check Type
210+replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)
211+ where
212+ f :: Type -> StateT (M.Map String Int) (Subst Check) Type
213+ f (TypeVar var) | var `elem` idents = do
214+ m <- get
215+ n <- lift fresh'
216+ case M.lookup var m of
217+ Nothing -> do
218+ put (M.insert var n m)
219+ return $ TUnknown (Unknown n)
220+ Just u -> return $ TUnknown (Unknown u)
221+ f t = return t
222+ g :: Row -> StateT (M.Map String Int) (Subst Check) Row
223+ g (RowVar var) | var `elem` idents = do
224+ m <- get
225+ n <- lift fresh'
226+ case M.lookup var m of
227+ Nothing -> do
228+ put (M.insert var n m)
229+ return $ RUnknown (Unknown n)
230+ Just u -> return $ RUnknown (Unknown u)
231+ g r = return r
232+
233+replaceAllTypeSynonyms :: (D.Data d) => d -> Check d
234+replaceAllTypeSynonyms d = do
235+ env <- getEnv
236+ let syns = map (\((path, name), (args, _)) -> (Qualified path name, length args)) . M.toList $ typeSynonyms env
237+ either throwError return $ saturateAllTypeSynonyms syns d
238+
239+desaturateAllTypeSynonyms :: (D.Data d) => d -> d
240+desaturateAllTypeSynonyms = everywhere (mkT replace)
241+ where
242+ replace (SaturatedTypeSynonym name args) = foldl TypeApp (TypeConstructor name) args
243+ replace t = t
244+
245+expandAllTypeSynonyms :: Type -> Subst Check Type
246+expandAllTypeSynonyms (SaturatedTypeSynonym name args) = expandTypeSynonym name args >>= expandAllTypeSynonyms
247+expandAllTypeSynonyms ty = return ty
248+
249+expandTypeSynonym :: Qualified ProperName -> [Type] -> Subst Check Type
250+expandTypeSynonym name args = do
251+ env <- lift getEnv
252+ modulePath <- checkModulePath `fmap` lift get
253+ case M.lookup (qualify modulePath name) (typeSynonyms env) of
254+ Just (synArgs, body) -> return $ replaceAllTypeVars (zip synArgs args) body
255+ Nothing -> error "Type synonym was not defined"
256+
257+ensureNoDuplicateProperties :: [(String, Value)] -> Check ()
258+ensureNoDuplicateProperties ps = guardWith "Duplicate property names" $ length (nub . map fst $ ps) == length ps
259+
260+infer :: M.Map Ident Type -> Value -> Subst Check Type
261+infer m val = rethrow (\e -> "Error inferring type of term " ++ prettyPrintValue val ++ ":\n" ++ e) $ do
262+ ty <- infer' m val
263+ escapeCheckLater ty
264+ return ty
265+
266+infer' _ (NumericLiteral _) = return Number
267+infer' _ (StringLiteral _) = return String
268+infer' _ (BooleanLiteral _) = return Boolean
269+infer' m (ArrayLiteral vals) = do
270+ ts <- mapM (infer m) vals
271+ arr <- fresh
272+ forM_ ts $ \t -> arr ~~ Array t
273+ return arr
274+infer' m (Unary op val) = do
275+ t <- infer m val
276+ inferUnary op t
277+infer' m (Binary op left right) = do
278+ t1 <- infer m left
279+ t2 <- infer m right
280+ inferBinary op t1 t2
281+infer' m (ObjectLiteral ps) = do
282+ lift $ ensureNoDuplicateProperties ps
283+ ts <- mapM (infer m . snd) ps
284+ let fields = zipWith (\(name, _) t -> (name, t)) ps ts
285+ return $ Object $ typesToRow fields
286+infer' m (ObjectUpdate o ps) = do
287+ lift $ ensureNoDuplicateProperties ps
288+ obj <- infer m o
289+ row <- fresh
290+ ts <- mapM (infer m . snd) ps
291+ let tys = zipWith (\(name, _) t -> (name, t)) ps ts
292+ obj ~~ Object (rowFromList (tys, row))
293+ return obj
294+infer' m (Indexer index val) = do
295+ el <- fresh
296+ check m index Number
297+ check m val (Array el)
298+ return el
299+infer' m (Accessor prop val) = do
300+ obj <- infer m val
301+ propTy <- inferProperty obj prop
302+ case propTy of
303+ Nothing -> do
304+ field <- fresh
305+ rest <- fresh
306+ obj `subsumes` Object (RCons prop field rest)
307+ return field
308+ Just ty -> return ty
309+infer' m (Abs args ret) = do
310+ ts <- replicateM (length args) fresh
311+ let m' = m `M.union` M.fromList (zip args ts)
312+ body <- infer m' ret
313+ return $ Function ts body
314+infer' m app@(App _ _) = do
315+ let (f, argss) = unfoldApplication app
316+ ft <- infer m f
317+ ret <- fresh
318+ checkFunctionApplications m ft argss ret
319+ return ret
320+infer' m (Var var@(Qualified mp name)) = do
321+ case mp of
322+ ModulePath [] ->
323+ case M.lookup name m of
324+ Just ty -> lift $ replaceAllTypeSynonyms ty
325+ Nothing -> lookupGlobal
326+ _ -> lookupGlobal
327+ where
328+ lookupGlobal = do
329+ env <- lift getEnv
330+ modulePath <- checkModulePath `fmap` lift get
331+ case M.lookup (qualify modulePath var) (names env) of
332+ Nothing -> throwError $ show var ++ " is undefined"
333+ Just (ty, _) -> lift $ replaceAllTypeSynonyms ty
334+infer' m (Block ss) = do
335+ ret <- fresh
336+ (allCodePathsReturn, _) <- checkBlock m M.empty ret ss
337+ guardWith "Block is missing a return statement" allCodePathsReturn
338+ return ret
339+infer' m (Constructor c) = do
340+ env <- lift getEnv
341+ modulePath <- checkModulePath `fmap` lift get
342+ case M.lookup (qualify modulePath c) (dataConstructors env) of
343+ Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
344+ Just ty -> lift $ replaceAllTypeSynonyms ty
345+infer' m (Case val binders) = do
346+ t1 <- infer m val
347+ ret <- fresh
348+ checkBinders m t1 ret binders
349+ return ret
350+infer' m (IfThenElse cond th el) = do
351+ check m cond Boolean
352+ t2 <- infer m th
353+ t3 <- infer m el
354+ t2 ~~ t3
355+ return t2
356+infer' m (TypedValue val ty) = do
357+ kind <- lift $ kindOf ty
358+ guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
359+ ty' <- lift $ replaceAllTypeSynonyms ty
360+ check m val ty'
361+ return ty'
362+
363+inferProperty :: Type -> String -> Subst Check (Maybe Type)
364+inferProperty (Object row) prop = do
365+ let (props, _) = rowToList row
366+ return $ lookup prop props
367+inferProperty (SaturatedTypeSynonym name args) prop = do
368+ replaced <- expandTypeSynonym name args
369+ inferProperty replaced prop
370+inferProperty (ForAll ident ty) prop = do
371+ replaced <- replaceVarsWithUnknowns [ident] ty
372+ inferProperty replaced prop
373+inferProperty _ prop = return Nothing
374+
375+inferUnary :: UnaryOperator -> Type -> Subst Check Type
376+inferUnary op val =
377+ case fromMaybe (error "Invalid operator") $ lookup op unaryOps of
378+ (valTy, resTy) -> do
379+ val ~~ valTy
380+ return resTy
381+
382+checkUnary :: M.Map Ident Type -> UnaryOperator -> Value -> Type -> Subst Check ()
383+checkUnary m op val res =
384+ case fromMaybe (error "Invalid operator") $ lookup op unaryOps of
385+ (valTy, resTy) -> do
386+ res ~~ resTy
387+ check m val valTy
388+
389+unaryOps :: [(UnaryOperator, (Type, Type))]
390+unaryOps = [ (Negate, (Number, Number))
391+ , (Not, (Boolean, Boolean))
392+ , (BitwiseNot, (Number, Number))
393+ ]
394+
395+inferBinary :: BinaryOperator -> Type -> Type -> Subst Check Type
396+inferBinary op left right | isEqualityTest op = do
397+ left ~~ right
398+ return Boolean
399+inferBinary op left right =
400+ case fromMaybe (error "Invalid operator") $ lookup op binaryOps of
401+ (valTy, resTy) -> do
402+ left ~~ valTy
403+ right ~~ valTy
404+ return resTy
405+
406+checkBinary :: M.Map Ident Type -> BinaryOperator -> Value -> Value -> Type -> Subst Check ()
407+checkBinary m op left right res | isEqualityTest op = do
408+ res ~~ Boolean
409+ t1 <- infer m left
410+ t2 <- infer m right
411+ t1 ~~ t2
412+checkBinary m op left right res =
413+ case fromMaybe (error "Invalid operator") $ lookup op binaryOps of
414+ (valTy, resTy) -> do
415+ res ~~ resTy
416+ check m left valTy
417+ check m right valTy
418+
419+isEqualityTest :: BinaryOperator -> Bool
420+isEqualityTest EqualTo = True
421+isEqualityTest NotEqualTo = True
422+isEqualityTest _ = False
423+
424+binaryOps :: [(BinaryOperator, (Type, Type))]
425+binaryOps = [ (Add, (Number, Number))
426+ , (Subtract, (Number, Number))
427+ , (Multiply, (Number, Number))
428+ , (Divide, (Number, Number))
429+ , (Modulus, (Number, Number))
430+ , (BitwiseAnd, (Number, Number))
431+ , (BitwiseOr, (Number, Number))
432+ , (BitwiseXor, (Number, Number))
433+ , (ShiftRight, (Number, Number))
434+ , (ZeroFillShiftRight, (Number, Number))
435+ , (And, (Boolean, Boolean))
436+ , (Or, (Boolean, Boolean))
437+ , (Concat, (String, String))
438+ , (Modulus, (Number, Number))
439+ , (LessThan, (Number, Boolean))
440+ , (LessThanOrEqualTo, (Number, Boolean))
441+ , (GreaterThan, (Number, Boolean))
442+ , (GreaterThanOrEqualTo, (Number, Boolean))
443+ ]
444+
445+inferBinder :: Type -> Binder -> Subst Check (M.Map Ident Type)
446+inferBinder _ NullBinder = return M.empty
447+inferBinder val (StringBinder _) = val ~~ String >> return M.empty
448+inferBinder val (NumberBinder _) = val ~~ Number >> return M.empty
449+inferBinder val (BooleanBinder _) = val ~~ Boolean >> return M.empty
450+inferBinder val (VarBinder name) = return $ M.singleton name val
451+inferBinder val (NullaryBinder ctor) = do
452+ env <- lift getEnv
453+ modulePath <- checkModulePath `fmap` lift get
454+ case M.lookup (qualify modulePath ctor) (dataConstructors env) of
455+ Just ty -> do
456+ ty `subsumes` val
457+ return M.empty
458+ _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
459+inferBinder val (UnaryBinder ctor binder) = do
460+ env <- lift getEnv
461+ modulePath <- checkModulePath `fmap` lift get
462+ case M.lookup (qualify modulePath ctor) (dataConstructors env) of
463+ Just ty -> do
464+ obj <- fresh
465+ ty `subsumes` (Function [obj] val)
466+ inferBinder obj binder
467+ _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
468+inferBinder val (ObjectBinder props) = do
469+ row <- fresh
470+ rest <- fresh
471+ m1 <- inferRowProperties row rest props
472+ val ~~ Object row
473+ return m1
474+ where
475+ inferRowProperties :: Row -> Row -> [(String, Binder)] -> Subst Check (M.Map Ident Type)
476+ inferRowProperties nrow row [] = nrow ~~ row >> return M.empty
477+ inferRowProperties nrow row ((name, binder):binders) = do
478+ propTy <- fresh
479+ m1 <- inferBinder propTy binder
480+ m2 <- inferRowProperties nrow (RCons name propTy row) binders
481+ return $ m1 `M.union` m2
482+inferBinder val (ArrayBinder binders rest) = do
483+ el <- fresh
484+ m1 <- M.unions <$> mapM (inferBinder el) binders
485+ val ~~ Array el
486+ case rest of
487+ Nothing -> return m1
488+ Just binder -> do
489+ m2 <- inferBinder val binder
490+ return $ m1 `M.union` m2
491+inferBinder val (NamedBinder name binder) = do
492+ m <- inferBinder val binder
493+ return $ M.insert name val m
494+
495+inferGuardedBinder :: M.Map Ident Type -> Type -> Binder -> Subst Check (M.Map Ident Type)
496+inferGuardedBinder m val (GuardedBinder cond binder) = do
497+ m1 <- inferBinder val binder
498+ check (m1 `M.union` m) cond Boolean
499+ return m1
500+inferGuardedBinder m val b = inferBinder val b
501+
502+checkBinders :: M.Map Ident Type -> Type -> Type -> [(Binder, Value)] -> Subst Check ()
503+checkBinders _ _ _ [] = return ()
504+checkBinders m nval ret ((binder, val):bs) = do
505+ m1 <- inferGuardedBinder m nval binder
506+ check (m1 `M.union` m) val ret
507+ checkBinders m nval ret bs
508+
509+assignVariable :: Ident -> M.Map Ident Type -> Subst Check ()
510+assignVariable name m =
511+ case M.lookup name m of
512+ Nothing -> return ()
513+ Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."
514+
515+checkStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> Statement -> Subst Check (Bool, M.Map Ident Type)
516+checkStatement m mass ret (VariableIntroduction name val) = do
517+ assignVariable name (m `M.union` mass)
518+ t <- infer m val
519+ return (False, M.insert name t mass)
520+checkStatement m mass ret (Assignment ident val) = do
521+ t <- infer m val
522+ case M.lookup ident mass of
523+ Nothing -> throwError $ "No local variable with name " ++ show ident
524+ Just ty -> do t ~~ ty
525+ return (False, mass)
526+checkStatement m mass ret (While val inner) = do
527+ check m val Boolean
528+ (allCodePathsReturn, _) <- checkBlock m mass ret inner
529+ return (allCodePathsReturn, mass)
530+checkStatement m mass ret (If ifst) = do
531+ allCodePathsReturn <- checkIfStatement m mass ret ifst
532+ return (allCodePathsReturn, mass)
533+checkStatement m mass ret (For ident start end inner) = do
534+ assignVariable ident (m `M.union` mass)
535+ check (m `M.union` mass) start Number
536+ check (m `M.union` mass) end Number
537+ let mass1 = M.insert ident Number mass
538+ (allCodePathsReturn, _) <- checkBlock (m `M.union` mass1) mass1 ret inner
539+ return (allCodePathsReturn, mass)
540+checkStatement m mass ret (ForEach ident vals inner) = do
541+ assignVariable ident (m `M.union` mass)
542+ val <- fresh
543+ check (m `M.union` mass) vals (Array val)
544+ let mass1 = M.insert ident val mass
545+ (allCodePathsReturn, _) <- checkBlock (m `M.union` mass1) mass1 ret inner
546+ guardWith "Cannot return from within a foreach block" $ not allCodePathsReturn
547+ return (False, mass)
548+checkStatement m mass ret (Return val) = do
549+ check (m `M.union` mass) val ret
550+ return (True, mass)
551+
552+checkIfStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> IfStatement -> Subst Check Bool
553+checkIfStatement m mass ret (IfStatement val thens Nothing) = do
554+ check m val Boolean
555+ _ <- checkBlock m mass ret thens
556+ return False
557+checkIfStatement m mass ret (IfStatement val thens (Just elses)) = do
558+ check m val Boolean
559+ (allCodePathsReturn1, _) <- checkBlock m mass ret thens
560+ allCodePathsReturn2 <- checkElseStatement m mass ret elses
561+ return $ allCodePathsReturn1 && allCodePathsReturn2
562+
563+checkElseStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> ElseStatement -> Subst Check Bool
564+checkElseStatement m mass ret (Else elses) = fst <$> checkBlock m mass ret elses
565+checkElseStatement m mass ret (ElseIf ifst) = checkIfStatement m mass ret ifst
566+
567+checkBlock :: M.Map Ident Type -> M.Map Ident Type -> Type -> [Statement] -> Subst Check (Bool, M.Map Ident Type)
568+checkBlock _ mass _ [] = return (False, mass)
569+checkBlock m mass ret (s:ss) = do
570+ (b1, mass1) <- checkStatement (m `M.union` mass) mass ret s
571+ case (b1, ss) of
572+ (True, []) -> return (True, mass1)
573+ (True, _) -> throwError "Unreachable code"
574+ (False, ss) -> do
575+ (b2, mass2) <- checkBlock m mass1 ret ss
576+ return (b2, mass2)
577+
578+skolemize :: String -> Type -> Subst Check Type
579+skolemize ident ty = do
580+ tsk <- Skolem <$> fresh'
581+ rsk <- RSkolem <$> fresh'
582+ return $ replaceRowVars ident rsk $ replaceTypeVars ident tsk ty
583+
584+check :: M.Map Ident Type -> Value -> Type -> Subst Check ()
585+check m val ty = rethrow errorMessage $ check' m val ty
586+ where
587+ errorMessage msg =
588+ "Error checking type of term " ++
589+ prettyPrintValue val ++
590+ " against type " ++
591+ prettyPrintType ty ++
592+ ":\n" ++
593+ msg
594+
595+check' :: M.Map Ident Type -> Value -> Type -> Subst Check ()
596+check' m val (ForAll idents ty) = do
597+ sk <- skolemize idents ty
598+ check m val sk
599+check' m val u@(TUnknown _) = do
600+ ty <- infer m val
601+ -- Don't unify an unknown with an inferred polytype
602+ ty' <- replaceAllVarsWithUnknowns ty
603+ ty' ~~ u
604+check' m (NumericLiteral _) Number = return ()
605+check' m (StringLiteral _) String = return ()
606+check' m (BooleanLiteral _) Boolean = return ()
607+check' m (Unary op val) ty = checkUnary m op val ty
608+check' m (Binary op left right) ty = checkBinary m op left right ty
609+check' m (ArrayLiteral vals) (Array ty) = forM_ vals (\val -> check m val ty)
610+check' m (Indexer index vals) ty = check m index Number >> check m vals (Array ty)
611+check' m (Abs args ret) (Function argTys retTy) = do
612+ guardWith "Incorrect number of function arguments" (length args == length argTys)
613+ let bindings = M.fromList (zip args argTys)
614+ check (bindings `M.union` m) ret retTy
615+check' m app@(App _ _) ret = do
616+ let (f, argss) = unfoldApplication app
617+ ft <- infer m f
618+ checkFunctionApplications m ft argss ret
619+check' m v@(Var var@(Qualified mp name)) ty = do
620+ case mp of
621+ ModulePath [] ->
622+ case M.lookup name m of
623+ Just ty1 -> do
624+ repl <- lift $ replaceAllTypeSynonyms ty1
625+ repl `subsumes` ty
626+ Nothing -> lookupGlobal
627+ _ -> lookupGlobal
628+ where
629+ lookupGlobal = do
630+ env <- lift getEnv
631+ modulePath <- checkModulePath `fmap` lift get
632+ case M.lookup (qualify modulePath var) (names env) of
633+ Nothing -> throwError $ show var ++ " is undefined"
634+ Just (ty1, _) -> do
635+ repl <- lift $ replaceAllTypeSynonyms ty1
636+ repl `subsumes` ty
637+check' m (TypedValue val ty1) ty2 = do
638+ kind <- lift $ kindOf ty1
639+ guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
640+ ty1 `subsumes` ty2
641+ check m val ty1
642+check' m (Case val binders) ret = do
643+ t1 <- infer m val
644+ checkBinders m t1 ret binders
645+check' m (IfThenElse cond th el) ty = do
646+ check m cond Boolean
647+ check m th ty
648+ check m el ty
649+check' m (ObjectLiteral ps) (Object row) = do
650+ lift $ ensureNoDuplicateProperties ps
651+ checkProperties m ps row False
652+check' m (ObjectUpdate obj ps) objTy@(Object row) = do
653+ lift $ ensureNoDuplicateProperties ps
654+ check m obj objTy
655+ checkProperties m ps row True
656+check' m (Accessor prop val) ty = do
657+ rest <- fresh
658+ check m val (Object (RCons prop ty rest))
659+check' m (Block ss) ret = do
660+ (allCodePathsReturn, _) <- checkBlock m M.empty ret ss
661+ guardWith "Block is missing a return statement" allCodePathsReturn
662+check' m (Constructor c) ty = do
663+ env <- lift getEnv
664+ modulePath <- checkModulePath `fmap` lift get
665+ case M.lookup (qualify modulePath c) (dataConstructors env) of
666+ Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
667+ Just ty1 -> do
668+ repl <- lift $ replaceAllTypeSynonyms ty1
669+ repl `subsumes` ty
670+check' m val (SaturatedTypeSynonym name args) = do
671+ ty <- expandTypeSynonym name args
672+ check m val ty
673+check' _ val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty
674+
675+checkProperties :: M.Map Ident Type -> [(String, Value)] -> Row -> Bool -> Subst Check ()
676+checkProperties m ps row lax = let (ts, r') = rowToList row in go ps ts r' where
677+ go [] [] REmpty = return ()
678+ go [] [] u@(RUnknown _) = u ~~ REmpty
679+ go [] [] (RSkolem _) | lax = return ()
680+ go [] ((p, _): _) _ | lax = return ()
681+ | otherwise = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have property " ++ p
682+ go ((p,_):_) [] REmpty = throwError $ "Property " ++ p ++ " is not present in closed object type " ++ prettyPrintRow row
683+ go ((p,v):ps) [] u@(RUnknown _) = do
684+ ty <- infer m v
685+ rest <- fresh
686+ u ~~ RCons p ty rest
687+ go ps [] rest
688+ go ((p,v):ps) ts r =
689+ case lookup p ts of
690+ Nothing -> do
691+ ty <- infer m v
692+ rest <- fresh
693+ r ~~ RCons p ty rest
694+ go ps ts rest
695+ Just ty -> do
696+ check m v ty
697+ go ps (delete (p, ty) ts) r
698+ go _ _ _ = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have type " ++ prettyPrintType (Object row)
699+
700+unfoldApplication :: Value -> (Value, [[Value]])
701+unfoldApplication = go []
702+ where
703+ go argss (App f args) = go (args:argss) f
704+ go argss f = (f, argss)
705+
706+checkFunctionApplications :: M.Map Ident Type -> Type -> [[Value]] -> Type -> Subst Check ()
707+checkFunctionApplications _ _ [] _ = error "Nullary function application"
708+checkFunctionApplications m fnTy [args] ret = checkFunctionApplication m fnTy args ret
709+checkFunctionApplications m fnTy (args:argss) ret = do
710+ f <- fresh
711+ checkFunctionApplication m fnTy args f
712+ checkFunctionApplications m f argss ret
713+
714+checkFunctionApplication :: M.Map Ident Type -> Type -> [Value] -> Type -> Subst Check ()
715+checkFunctionApplication m fnTy args ret = rethrow errorMessage $ checkFunctionApplication' m fnTy args ret
716+ where
717+ errorMessage msg = "Error applying function of type "
718+ ++ prettyPrintType fnTy
719+ ++ " to arguments " ++ intercalate ", " (map prettyPrintValue args)
720+ ++ ", expecting value of type "
721+ ++ prettyPrintType ret ++ ":\n" ++ msg
722+
723+checkFunctionApplication' :: M.Map Ident Type -> Type -> [Value] -> Type -> Subst Check ()
724+checkFunctionApplication' m (Function argTys retTy) args ret = do
725+ guardWith "Incorrect number of function arguments" (length args == length argTys)
726+ zipWithM (check m) args argTys
727+ retTy `subsumes` ret
728+checkFunctionApplication' m (ForAll ident ty) args ret = do
729+ replaced <- replaceVarsWithUnknowns [ident] ty
730+ checkFunctionApplication m replaced args ret
731+checkFunctionApplication' m u@(TUnknown _) args ret = do
732+ tyArgs <- mapM (\arg -> infer m arg >>= replaceAllVarsWithUnknowns) args
733+ u ~~ Function tyArgs ret
734+checkFunctionApplication' m (SaturatedTypeSynonym name tyArgs) args ret = do
735+ ty <- expandTypeSynonym name tyArgs
736+ checkFunctionApplication' m ty args ret
737+checkFunctionApplication' _ fnTy args ret = throwError $ "Cannot apply function of type "
738+ ++ prettyPrintType fnTy
739+ ++ " to arguments " ++ intercalate ", " (map prettyPrintValue args)
740+ ++ ". Expecting value of type " ++ prettyPrintType ret ++ "."
741+
742+subsumes :: Type -> Type -> Subst Check ()
743+subsumes (ForAll ident ty1) ty2 = do
744+ replaced <- replaceVarsWithUnknowns [ident] ty1
745+ replaced `subsumes` ty2
746+subsumes (Function args1 ret1) (Function args2 ret2) = do
747+ zipWithM subsumes args2 args1
748+ ret1 `subsumes` ret2
749+subsumes ty1 ty2 = ty1 ~~ ty2
750+