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