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