@@ -1,678 +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−-- This module implements the type checker
13−--
14−-----------------------------------------------------------------------------
15−
16−{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses #-}
17−
18−module Language.PureScript.TypeChecker.Types (
19− typesOf
20−) where
21−
22−{-
23− The following functions represent the corresponding type checking judgements:
24−
25− infer
26− Synthesize a type for a value
27−
28− check
29− Check a value has a given type
30−
31− checkProperties
32− Check an object with a given type contains specified properties
33−
34− checkFunctionApplication
35− Check a function of a given type returns a value of another type when applied to its arguments
36−-}
37−
38−import Data.Either (lefts, rights)
39−import Data.List
40−import Data.Maybe (fromMaybe)
41−import Data.Monoid
42−import qualified Data.Map as M
43−
44−import Control.Applicative
45−import Control.Monad.Error
46−import Control.Monad.State
47−import Control.Monad.Unify
48−
49−import Language.PureScript.AST
50−import Language.PureScript.Environment
51−import Language.PureScript.Errors
52−import Language.PureScript.Kinds
53−import Language.PureScript.Names
54−import Language.PureScript.Pretty
55−import Language.PureScript.TypeChecker.Entailment
56−import Language.PureScript.TypeChecker.Kinds
57−import Language.PureScript.TypeChecker.Monad
58−import Language.PureScript.TypeChecker.Rows
59−import Language.PureScript.TypeChecker.Skolems
60−import Language.PureScript.TypeChecker.Subsumption
61−import Language.PureScript.TypeChecker.Synonyms
62−import Language.PureScript.TypeChecker.Unify
63−import Language.PureScript.TypeClassDictionaries
64−import Language.PureScript.Types
65−import qualified Language.PureScript.Constants as C
66−
67−-- |
68−-- Infer the types of multiple mutually-recursive values, and return elaborated values including
69−-- type class dictionaries and type annotations.
70−--
71−typesOf :: Maybe ModuleName -> ModuleName -> [(Ident, Expr)] -> Check [(Ident, (Expr, Type))]
72−typesOf mainModuleName moduleName vals = do
73− tys <- fmap tidyUp . liftUnify $ do
74− (untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup moduleName vals
75− ds1 <- parU typed $ \e -> do
76− triple@(_, (_, ty)) <- checkTypedBindingGroupElement moduleName e dict
77− checkMain (fst e) ty
78− return triple
79− ds2 <- forM untyped $ \e -> do
80− triple@(_, (_, ty)) <- typeForBindingGroupElement e dict untypedDict
81− checkMain (fst e) ty
82− return triple
83− return $ ds1 ++ ds2
84−
85− forM tys $ \(ident, (val, ty)) -> do
86− -- Replace type class dictionary placeholders with actual dictionaries
87− val' <- replaceTypeClassDictionaries moduleName val
88− -- Check skolem variables did not escape their scope
89− skolemEscapeCheck val'
90− -- Check rows do not contain duplicate labels
91− checkDuplicateLabels val'
92− -- Remove type synonyms placeholders, and replace
93− -- top-level unification variables with named type variables.
94− let val'' = overTypes desaturateAllTypeSynonyms val'
95− ty' = varIfUnknown . desaturateAllTypeSynonyms $ ty
96− return (ident, (val'', ty'))
97− where
98− -- Apply the substitution that was returned from runUnify to both types and (type-annotated) values
99− tidyUp (ts, sub) = map (\(i, (val, ty)) -> (i, (overTypes (sub $?) val, sub $? ty))) ts
100− -- If --main is enabled, need to check that `main` has type Eff eff a for some eff, a
101− checkMain nm ty = when (Just moduleName == mainModuleName && nm == Ident C.main) $ do
102− [eff, a] <- replicateM 2 fresh
103− ty =?= TypeApp (TypeApp (TypeConstructor (Qualified (Just (ModuleName [ProperName "Control", ProperName "Monad", ProperName "Eff"])) (ProperName "Eff"))) eff) a
104−
105−type TypeData = M.Map (ModuleName, Ident) (Type, NameKind, NameVisibility)
106−
107−type UntypedData = [(Ident, Type)]
108−
109−typeDictionaryForBindingGroup :: ModuleName -> [(Ident, Expr)] -> UnifyT Type Check ([(Ident, Expr)], [(Ident, (Expr, Type, Bool))], TypeData, UntypedData)
110−typeDictionaryForBindingGroup moduleName vals = do
111− let
112− -- Map each declaration to a name/value pair, with an optional type, if the declaration is typed
113− es = map isTyped vals
114− -- Filter the typed and untyped declarations
115− untyped = lefts es
116− typed = rights es
117− -- Make a map of names to typed declarations
118− typedDict = map (\(ident, (_, ty, _)) -> (ident, ty)) typed
119−
120− -- Create fresh unification variables for the types of untyped declarations
121− untypedNames <- replicateM (length untyped) fresh
122−
123− let
124− -- Make a map of names to the unification variables of untyped declarations
125− untypedDict = zip (map fst untyped) untypedNames
126− -- Create the dictionary of all name/type pairs, which will be added to the environment during type checking
127− dict = M.fromList (map (\(ident, ty) -> ((moduleName, ident), (ty, LocalVariable, Undefined))) $ typedDict ++ untypedDict)
128− return (untyped, typed, dict, untypedDict)
129−
130−checkTypedBindingGroupElement :: ModuleName -> (Ident, (Expr, Type, Bool)) -> TypeData -> UnifyT Type Check (Ident, (Expr, Type))
131−checkTypedBindingGroupElement moduleName (ident, (val', ty, checkType)) dict = do
132− -- Replace type wildcards
133− ty' <- replaceTypeWildcards ty
134− -- Kind check
135− kind <- liftCheck $ kindOf moduleName ty
136− guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
137− -- Check the type with the new names in scope
138− ty'' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty'
139− val'' <- if checkType
140− then bindNames dict $ TypedValue True <$> check val' ty'' <*> pure ty''
141− else return (TypedValue False val' ty'')
142− return (ident, (val'', ty''))
143−
144−typeForBindingGroupElement :: (Ident, Expr) -> TypeData -> UntypedData -> UnifyT Type Check (Ident, (Expr, Type))
145−typeForBindingGroupElement (ident, val) dict untypedDict = do
146− -- Infer the type with the new names in scope
147− TypedValue _ val' ty <- bindNames dict $ infer val
148− ty =?= fromMaybe (error "name not found in dictionary") (lookup ident untypedDict)
149− return (ident, (TypedValue True val' ty, ty))
150−
151−-- |
152−-- Check if a value contains a type annotation
153−--
154−isTyped :: (Ident, Expr) -> Either (Ident, Expr) (Ident, (Expr, Type, Bool))
155−isTyped (name, TypedValue checkType value ty) = Right (name, (value, ty, checkType))
156−isTyped (name, value) = Left (name, value)
157−
158−-- |
159−-- Map a function over type annotations appearing inside a value
160−--
161−overTypes :: (Type -> Type) -> Expr -> Expr
162−overTypes f = let (_, f', _) = everywhereOnValues id g id in f'
163− where
164− g :: Expr -> Expr
165− g (TypedValue checkTy val t) = TypedValue checkTy val (f t)
166− g (TypeClassDictionary b (nm, tys) sco) = TypeClassDictionary b (nm, map f tys) sco
167− g other = other
168−
169−-- |
170−-- Replace type class dictionary placeholders with inferred type class dictionaries
171−--
172−replaceTypeClassDictionaries :: ModuleName -> Expr -> Check Expr
173−replaceTypeClassDictionaries mn =
174− let (_, f, _) = everywhereOnValuesTopDownM return go return
175− in f
176− where
177− go (TypeClassDictionary trySuperclasses constraint dicts) = do
178− env <- getEnv
179− entails env mn dicts constraint trySuperclasses
180− go other = return other
181−
182−-- |
183−-- Check the kind of a type, failing if it is not of kind *.
184−--
185−checkTypeKind :: ModuleName -> Type -> UnifyT t Check ()
186−checkTypeKind moduleName ty = do
187− kind <- liftCheck $ kindOf moduleName ty
188− guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
189−
190−-- |
191−-- Remove any ForAlls and ConstrainedType constructors in a type by introducing new unknowns
192−-- or TypeClassDictionary values.
193−--
194−-- This is necessary during type checking to avoid unifying a polymorphic type with a
195−-- unification variable.
196−--
197−instantiatePolyTypeWithUnknowns :: Expr -> Type -> UnifyT Type Check (Expr, Type)
198−instantiatePolyTypeWithUnknowns val (ForAll ident ty _) = do
199− ty' <- replaceVarWithUnknown ident ty
200− instantiatePolyTypeWithUnknowns val ty'
201−instantiatePolyTypeWithUnknowns val (ConstrainedType constraints ty) = do
202− dicts <- getTypeClassDictionaries
203− (_, ty') <- instantiatePolyTypeWithUnknowns (error "Types under a constraint cannot themselves be constrained") ty
204− return (foldl App val (map (flip (TypeClassDictionary True) dicts) constraints), ty')
205−instantiatePolyTypeWithUnknowns val ty = return (val, ty)
206−
207−-- |
208−-- Infer a type for a value, rethrowing any error to provide a more useful error message
209−--
210−infer :: Expr -> UnifyT Type Check Expr
211−infer val = rethrow (mkErrorStack "Error inferring type of value" (Just (ExprError val)) <>) $ infer' val
212−
213−-- |
214−-- Infer a type for a value
215−--
216−infer' :: Expr -> UnifyT Type Check Expr
217−infer' v@(NumericLiteral _) = return $ TypedValue True v tyNumber
218−infer' v@(StringLiteral _) = return $ TypedValue True v tyString
219−infer' v@(BooleanLiteral _) = return $ TypedValue True v tyBoolean
220−infer' (ArrayLiteral vals) = do
221− ts <- mapM infer vals
222− els <- fresh
223− forM_ ts $ \(TypedValue _ _ t) -> els =?= t
224− return $ TypedValue True (ArrayLiteral ts) (TypeApp tyArray els)
225−infer' (ObjectLiteral ps) = do
226− ensureNoDuplicateProperties ps
227− ts <- mapM (infer . snd) ps
228− let fields = zipWith (\name (TypedValue _ _ t) -> (name, t)) (map fst ps) ts
229− ty = TypeApp tyObject $ rowFromList (fields, REmpty)
230− return $ TypedValue True (ObjectLiteral (zip (map fst ps) ts)) ty
231−infer' (ObjectUpdate o ps) = do
232− ensureNoDuplicateProperties ps
233− row <- fresh
234− newVals <- zipWith (\(name, _) t -> (name, t)) ps <$> mapM (infer . snd) ps
235− let newTys = map (\(name, TypedValue _ _ ty) -> (name, ty)) newVals
236− oldTys <- zip (map fst ps) <$> replicateM (length ps) fresh
237− let oldTy = TypeApp tyObject $ rowFromList (oldTys, row)
238− o' <- TypedValue True <$> check o oldTy <*> pure oldTy
239− return $ TypedValue True (ObjectUpdate o' newVals) $ TypeApp tyObject $ rowFromList (newTys, row)
240−infer' (Accessor prop val) = do
241− typed@(TypedValue _ _ objTy) <- infer val
242− propTy <- inferProperty objTy prop
243− case propTy of
244− Nothing -> do
245− field <- fresh
246− rest <- fresh
247− _ <- subsumes Nothing objTy (TypeApp tyObject (RCons prop field rest))
248− return $ TypedValue True (Accessor prop typed) field
249− Just ty -> return $ TypedValue True (Accessor prop typed) ty
250−infer' (Abs (Left arg) ret) = do
251− ty <- fresh
252− Just moduleName <- checkCurrentModule <$> get
253− makeBindingGroupVisible $ bindLocalVariables moduleName [(arg, ty, Defined)] $ do
254− body@(TypedValue _ _ bodyTy) <- infer' ret
255− return $ TypedValue True (Abs (Left arg) body) $ function ty bodyTy
256−infer' (Abs (Right _) _) = error "Binder was not desugared"
257−infer' (App f arg) = do
258− f'@(TypedValue _ _ ft) <- infer f
259− (ret, app) <- checkFunctionApplication f' ft arg Nothing
260− return $ TypedValue True app ret
261−infer' (Var var) = do
262− Just moduleName <- checkCurrentModule <$> get
263− checkVisibility moduleName var
264− ty <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards <=< lookupVariable moduleName $ var
265− case ty of
266− ConstrainedType constraints ty' -> do
267− dicts <- getTypeClassDictionaries
268− return $ TypedValue True (foldl App (Var var) (map (flip (TypeClassDictionary True) dicts) constraints)) ty'
269− _ -> return $ TypedValue True (Var var) ty
270−infer' v@(Constructor c) = do
271− env <- getEnv
272− case M.lookup c (dataConstructors env) of
273− Nothing -> throwError . strMsg $ "Constructor " ++ show c ++ " is undefined"
274− Just (_, _, ty) -> do ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
275− return $ TypedValue True v ty'
276−infer' (Case vals binders) = do
277− ts <- mapM infer vals
278− ret <- fresh
279− binders' <- checkBinders (map (\(TypedValue _ _ t) -> t) ts) ret binders
280− return $ TypedValue True (Case ts binders') ret
281−infer' (IfThenElse cond th el) = do
282− cond' <- check cond tyBoolean
283− v2@(TypedValue _ _ t2) <- infer th
284− v3@(TypedValue _ _ t3) <- infer el
285− (v2', v3', t) <- meet v2 v3 t2 t3
286− return $ TypedValue True (IfThenElse cond' v2' v3') t
287−infer' (Let ds val) = do
288− (ds', val'@(TypedValue _ _ valTy)) <- inferLetBinding [] ds val infer
289− return $ TypedValue True (Let ds' val') valTy
290−infer' (SuperClassDictionary className tys) = do
291− dicts <- getTypeClassDictionaries
292− return $ TypeClassDictionary False (className, tys) dicts
293−infer' (TypedValue checkType val ty) = do
294− Just moduleName <- checkCurrentModule <$> get
295− checkTypeKind moduleName ty
296− ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
297− val' <- if checkType then check val ty' else return val
298− return $ TypedValue True val' ty'
299−infer' (PositionedValue pos val) = rethrowWithPosition pos $ infer' val
300−infer' _ = error "Invalid argument to infer"
301−
302−inferLetBinding :: [Declaration] -> [Declaration] -> Expr -> (Expr -> UnifyT Type Check Expr) -> UnifyT Type Check ([Declaration], Expr)
303−inferLetBinding seen [] ret j = (,) seen <$> makeBindingGroupVisible (j ret)
304−inferLetBinding seen (ValueDeclaration ident nameKind [] (Right (tv@(TypedValue checkType val ty))) : rest) ret j = do
305− Just moduleName <- checkCurrentModule <$> get
306− checkTypeKind moduleName ty
307− let dict = M.singleton (moduleName, ident) (ty, nameKind, Undefined)
308− ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
309− TypedValue _ val' ty'' <- if checkType then bindNames dict (check val ty') else return tv
310− bindNames (M.singleton (moduleName, ident) (ty'', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] (Right (TypedValue checkType val' ty''))]) rest ret j
311−inferLetBinding seen (ValueDeclaration ident nameKind [] (Right val) : rest) ret j = do
312− valTy <- fresh
313− Just moduleName <- checkCurrentModule <$> get
314− let dict = M.singleton (moduleName, ident) (valTy, nameKind, Undefined)
315− TypedValue _ val' valTy' <- bindNames dict $ infer val
316− valTy =?= valTy'
317− bindNames (M.singleton (moduleName, ident) (valTy', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] (Right val')]) rest ret j
318−inferLetBinding seen (BindingGroupDeclaration ds : rest) ret j = do
319− Just moduleName <- checkCurrentModule <$> get
320− (untyped, typed, dict, untypedDict) <- typeDictionaryForBindingGroup moduleName (map (\(i, _, v) -> (i, v)) ds)
321− ds1' <- parU typed $ \e -> checkTypedBindingGroupElement moduleName e dict
322− ds2' <- forM untyped $ \e -> typeForBindingGroupElement e dict untypedDict
323− let ds' = [(ident, LocalVariable, val') | (ident, (val', _)) <- ds1' ++ ds2']
324− makeBindingGroupVisible $ bindNames dict $ inferLetBinding (seen ++ [BindingGroupDeclaration ds']) rest ret j
325−inferLetBinding seen (PositionedDeclaration pos d : ds) ret j = rethrowWithPosition pos $ do
326− (d' : ds', val') <- inferLetBinding seen (d : ds) ret j
327− return (PositionedDeclaration pos d' : ds', val')
328−inferLetBinding _ _ _ _ = error "Invalid argument to inferLetBinding"
329−
330−-- |
331−-- Infer the type of a property inside a record with a given type
332−--
333−inferProperty :: Type -> String -> UnifyT Type Check (Maybe Type)
334−inferProperty (TypeApp obj row) prop | obj == tyObject = do
335− let (props, _) = rowToList row
336− return $ lookup prop props
337−inferProperty (SaturatedTypeSynonym name args) prop = do
338− replaced <- introduceSkolemScope <=< expandTypeSynonym name $ args
339− inferProperty replaced prop
340−inferProperty (ForAll ident ty _) prop = do
341− replaced <- replaceVarWithUnknown ident ty
342− inferProperty replaced prop
343−inferProperty _ _ = return Nothing
344−
345−-- |
346−-- Infer the types of variables brought into scope by a binder
347−--
348−inferBinder :: Type -> Binder -> UnifyT Type Check (M.Map Ident Type)
349−inferBinder _ NullBinder = return M.empty
350−inferBinder val (StringBinder _) = val =?= tyString >> return M.empty
351−inferBinder val (NumberBinder _) = val =?= tyNumber >> return M.empty
352−inferBinder val (BooleanBinder _) = val =?= tyBoolean >> return M.empty
353−inferBinder val (VarBinder name) = return $ M.singleton name val
354−inferBinder val (ConstructorBinder ctor binders) = do
355− env <- getEnv
356− case M.lookup ctor (dataConstructors env) of
357− Just (_, _, ty) -> do
358− (_, fn) <- instantiatePolyTypeWithUnknowns (error "Data constructor types cannot contain constraints") ty
359− fn' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ fn
360− go binders fn'
361− where
362− go [] ty' = do
363− _ <- subsumes Nothing val ty'
364− return M.empty
365− go (binder : binders') (TypeApp (TypeApp t obj) ret) | t == tyFunction =
366− M.union <$> inferBinder obj binder <*> go binders' ret
367− go _ _ = throwError . strMsg $ "Wrong number of arguments to constructor " ++ show ctor
368− _ -> throwError . strMsg $ "Constructor " ++ show ctor ++ " is not defined"
369−inferBinder val (ObjectBinder props) = do
370− row <- fresh
371− rest <- fresh
372− m1 <- inferRowProperties row rest props
373− val =?= TypeApp tyObject row
374− return m1
375− where
376− inferRowProperties :: Type -> Type -> [(String, Binder)] -> UnifyT Type Check (M.Map Ident Type)
377− inferRowProperties nrow row [] = nrow =?= row >> return M.empty
378− inferRowProperties nrow row ((name, binder):binders) = do
379− propTy <- fresh
380− m1 <- inferBinder propTy binder
381− m2 <- inferRowProperties nrow (RCons name propTy row) binders
382− return $ m1 `M.union` m2
383−inferBinder val (ArrayBinder binders) = do
384− el <- fresh
385− m1 <- M.unions <$> mapM (inferBinder el) binders
386− val =?= TypeApp tyArray el
387− return m1
388−inferBinder val (ConsBinder headBinder tailBinder) = do
389− el <- fresh
390− m1 <- inferBinder el headBinder
391− m2 <- inferBinder val tailBinder
392− val =?= TypeApp tyArray el
393− return $ m1 `M.union` m2
394−inferBinder val (NamedBinder name binder) = do
395− m <- inferBinder val binder
396− return $ M.insert name val m
397−inferBinder val (PositionedBinder pos binder) =
398− rethrowWithPosition pos $ inferBinder val binder
399−
400−-- |
401−-- Check the types of the return values in a set of binders in a case statement
402−--
403−checkBinders :: [Type] -> Type -> [CaseAlternative] -> UnifyT Type Check [CaseAlternative]
404−checkBinders _ _ [] = return []
405−checkBinders nvals ret (CaseAlternative binders result : bs) = do
406− guardWith (strMsg "Overlapping binders in case statement") $
407− let ns = concatMap binderNames binders in length (nub ns) == length ns
408− Just moduleName <- checkCurrentModule <$> get
409− m1 <- M.unions <$> zipWithM inferBinder nvals binders
410− r <- bindLocalVariables moduleName [ (name, ty, Defined) | (name, ty) <- M.toList m1 ] $
411− CaseAlternative binders <$>
412− case result of
413− Left gs -> do
414− gs' <- forM gs $ \(grd, val) -> do
415− grd' <- check grd tyBoolean
416− val' <- TypedValue True <$> check val ret <*> pure ret
417− return (grd', val')
418− return $ Left gs'
419− Right val -> do
420− val' <- TypedValue True <$> check val ret <*> pure ret
421− return $ Right val'
422− rs <- checkBinders nvals ret bs
423− return $ r : rs
424−
425−-- |
426−-- Check the type of a value, rethrowing errors to provide a better error message
427−--
428−check :: Expr -> Type -> UnifyT Type Check Expr
429−check val ty = rethrow (mkErrorStack errorMessage (Just (ExprError val)) <>) $ check' val ty
430− where
431− errorMessage =
432− "Error checking type of term " ++
433− prettyPrintValue val ++
434− " against type " ++
435− prettyPrintType ty
436−
437−-- |
438−-- Check the type of a value
439−--
440−check' :: Expr -> Type -> UnifyT Type Check Expr
441−check' val (ForAll ident ty _) = do
442− scope <- newSkolemScope
443− sko <- newSkolemConstant
444− let sk = skolemize ident sko scope ty
445− let skVal = skolemizeTypesInValue ident sko scope val
446− val' <- check skVal sk
447− return $ TypedValue True val' (ForAll ident ty (Just scope))
448−check' val t@(ConstrainedType constraints ty) = do
449− dictNames <- forM constraints $ \(Qualified _ (ProperName className), _) -> do
450− n <- liftCheck freshDictionaryName
451− return $ Ident $ "__dict_" ++ className ++ "_" ++ show n
452− val' <- makeBindingGroupVisible $ withTypeClassDictionaries (zipWith (\name (className, instanceTy) ->
453− TypeClassDictionaryInScope name className instanceTy Nothing TCDRegular False) (map (Qualified Nothing) dictNames)
454− constraints) $ check val ty
455− return $ TypedValue True (foldr (Abs . Left) val' dictNames) t
456−check' val (SaturatedTypeSynonym name args) = do
457− ty <- introduceSkolemScope <=< expandTypeSynonym name $ args
458− check val ty
459−check' val u@(TUnknown _) = do
460− val'@(TypedValue _ _ ty) <- infer val
461− -- Don't unify an unknown with an inferred polytype
462− (val'', ty') <- instantiatePolyTypeWithUnknowns val' ty
463− ty' =?= u
464− return $ TypedValue True val'' ty'
465−check' v@(NumericLiteral _) t | t == tyNumber =
466− return $ TypedValue True v t
467−check' v@(StringLiteral _) t | t == tyString =
468− return $ TypedValue True v t
469−check' v@(BooleanLiteral _) t | t == tyBoolean =
470− return $ TypedValue True v t
471−check' (ArrayLiteral vals) t@(TypeApp a ty) = do
472− a =?= tyArray
473− array <- ArrayLiteral <$> forM vals (`check` ty)
474− return $ TypedValue True array t
475−check' (Abs (Left arg) ret) ty@(TypeApp (TypeApp t argTy) retTy) | t == tyFunction = do
476− Just moduleName <- checkCurrentModule <$> get
477− ret' <- makeBindingGroupVisible $ bindLocalVariables moduleName [(arg, argTy, Defined)] $ check ret retTy
478− return $ TypedValue True (Abs (Left arg) ret') ty
479−check' (Abs (Right _) _) _ = error "Binder was not desugared"
480−check' (App f arg) ret = do
481− f'@(TypedValue _ _ ft) <- infer f
482− (_, app) <- checkFunctionApplication f' ft arg (Just ret)
483− return $ TypedValue True app ret
484−check' v@(Var var) ty = do
485− Just moduleName <- checkCurrentModule <$> get
486− checkVisibility moduleName var
487− repl <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable moduleName $ var
488− ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
489− v' <- subsumes (Just v) repl ty'
490− case v' of
491− Nothing -> throwError . strMsg $ "Unable to check type subsumption"
492− Just v'' -> return $ TypedValue True v'' ty'
493−check' (SuperClassDictionary className tys) _ = do
494− {-
495− -- Here, we replace a placeholder for a superclass dictionary with a regular
496− -- TypeClassDictionary placeholder. The reason we do this is that it is necessary to have the
497− -- correct super instance dictionaries in scope, and these are not available when the type class
498− -- declaration gets desugared.
499− --
500− -- Note also that the first argument to TypeClassDictionary is False, meaning we _do not_ want
501− -- to consider superclass instances when searching for this dictionary - doing so might lead
502− -- to traversing a cycle in the instance graph.
503− -}
504− dicts <- getTypeClassDictionaries
505− return $ TypeClassDictionary False (className, tys) dicts
506−check' (TypedValue checkType val ty1) ty2 = do
507− Just moduleName <- checkCurrentModule <$> get
508− checkTypeKind moduleName ty1
509− ty1' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty1
510− ty2' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty2
511− val' <- subsumes (Just val) ty1' ty2'
512− case val' of
513− Nothing -> throwError . strMsg $ "Unable to check type subsumption"
514− Just val'' -> do
515− val''' <- if checkType then check val'' ty2' else return val''
516− return $ TypedValue checkType (TypedValue True val''' ty1') ty2'
517−check' (Case vals binders) ret = do
518− vals' <- mapM infer vals
519− let ts = map (\(TypedValue _ _ t) -> t) vals'
520− binders' <- checkBinders ts ret binders
521− return $ TypedValue True (Case vals' binders') ret
522−check' (IfThenElse cond th el) ty = do
523− cond' <- check cond tyBoolean
524− th' <- check th ty
525− el' <- check el ty
526− return $ TypedValue True (IfThenElse cond' th' el') ty
527−check' (ObjectLiteral ps) t@(TypeApp obj row) | obj == tyObject = do
528− ensureNoDuplicateProperties ps
529− ps' <- checkProperties ps row False
530− return $ TypedValue True (ObjectLiteral ps') t
531−check' (TypeClassDictionaryConstructorApp name ps) t = do
532− ps' <- check' ps t
533− return $ TypedValue True (TypeClassDictionaryConstructorApp name ps') t
534−check' (ObjectUpdate obj ps) t@(TypeApp o row) | o == tyObject = do
535− ensureNoDuplicateProperties ps
536− -- We need to be careful to avoid duplicate labels here.
537− -- We check _obj_ agaist the type _t_ with the types in _ps_ replaced with unknowns.
538− let (propsToCheck, rest) = rowToList row
539− (removedProps, remainingProps) = partition (\(p, _) -> p `elem` map fst ps) propsToCheck
540− us <- zip (map fst removedProps) <$> replicateM (length ps) fresh
541− obj' <- check obj (TypeApp tyObject (rowFromList (us ++ remainingProps, rest)))
542− ps' <- checkProperties ps row True
543− return $ TypedValue True (ObjectUpdate obj' ps') t
544−check' (Accessor prop val) ty = do
545− rest <- fresh
546− val' <- check val (TypeApp tyObject (RCons prop ty rest))
547− return $ TypedValue True (Accessor prop val') ty
548−check' (Constructor c) ty = do
549− env <- getEnv
550− case M.lookup c (dataConstructors env) of
551− Nothing -> throwError . strMsg $ "Constructor " ++ show c ++ " is undefined"
552− Just (_, _, ty1) -> do
553− repl <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1
554− _ <- subsumes Nothing repl ty
555− return $ TypedValue True (Constructor c) ty
556−check' (Let ds val) ty = do
557− (ds', val') <- inferLetBinding [] ds val (`check` ty)
558− return $ TypedValue True (Let ds' val') ty
559−check' val ty | containsTypeSynonyms ty = do
560− ty' <- introduceSkolemScope <=< expandAllTypeSynonyms <=< replaceTypeWildcards $ ty
561− check val ty'
562−check' val kt@(KindedType ty kind) = do
563− guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
564− val' <- check' val ty
565− return $ TypedValue True val' kt
566−check' (PositionedValue pos val) ty =
567− rethrowWithPosition pos $ check val ty
568−check' val ty = throwError $ mkErrorStack ("Expr does not have type " ++ prettyPrintType ty) (Just (ExprError val))
569−
570−containsTypeSynonyms :: Type -> Bool
571−containsTypeSynonyms = everythingOnTypes (||) go where
572− go (SaturatedTypeSynonym _ _) = True
573− go _ = False
574−
575−-- |
576−-- Check the type of a collection of named record fields
577−--
578−-- The @lax@ parameter controls whether or not every record member has to be provided. For object updates, this is not the case.
579−--
580−checkProperties :: [(String, Expr)] -> Type -> Bool -> UnifyT Type Check [(String, Expr)]
581−checkProperties ps row lax = let (ts, r') = rowToList row in go ps ts r' where
582− go [] [] REmpty = return []
583− go [] [] u@(TUnknown _) = do u =?= REmpty
584− return []
585− go [] [] Skolem{} | lax = return []
586− go [] ((p, _): _) _ | lax = return []
587− | otherwise = throwError $ mkErrorStack ("Object does not have property " ++ p) (Just (ExprError (ObjectLiteral ps)))
588− go ((p,_):_) [] REmpty = throwError $ mkErrorStack ("Property " ++ p ++ " is not present in closed object type " ++ prettyPrintRow row) (Just (ExprError (ObjectLiteral ps)))
589− go ((p,v):ps') [] u@(TUnknown _) = do
590− v'@(TypedValue _ _ ty) <- infer v
591− rest <- fresh
592− u =?= RCons p ty rest
593− ps'' <- go ps' [] rest
594− return $ (p, v') : ps''
595− go ((p,v):ps') ts r =
596− case lookup p ts of
597− Nothing -> do
598− v'@(TypedValue _ _ ty) <- infer v
599− rest <- fresh
600− r =?= RCons p ty rest
601− ps'' <- go ps' ts rest
602− return $ (p, v') : ps''
603− Just ty -> do
604− v' <- check v ty
605− ps'' <- go ps' (delete (p, ty) ts) r
606− return $ (p, v') : ps''
607− go _ _ _ = throwError $ mkErrorStack ("Object does not have type " ++ prettyPrintType (TypeApp tyObject row)) (Just (ExprError (ObjectLiteral ps)))
608−
609−-- |
610−-- Check the type of a function application, rethrowing errors to provide a better error message
611−--
612−checkFunctionApplication :: Expr -> Type -> Expr -> Maybe Type -> UnifyT Type Check (Type, Expr)
613−checkFunctionApplication fn fnTy arg ret = rethrow (mkErrorStack errorMessage (Just (ExprError fn)) <>) $ do
614− subst <- unifyCurrentSubstitution <$> UnifyT get
615− checkFunctionApplication' fn (subst $? fnTy) arg (($?) subst <$> ret)
616− where
617− errorMessage = "Error applying function of type "
618− ++ prettyPrintType fnTy
619− ++ " to argument " ++ prettyPrintValue arg
620−
621−-- |
622−-- Check the type of a function application
623−--
624−checkFunctionApplication' :: Expr -> Type -> Expr -> Maybe Type -> UnifyT Type Check (Type, Expr)
625−checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg ret = do
626− tyFunction' =?= tyFunction
627− arg' <- check arg argTy
628− case ret of
629− Nothing -> return (retTy, App fn arg')
630− Just ret' -> do
631− Just app' <- subsumes (Just (App fn arg')) retTy ret'
632− return (retTy, app')
633−checkFunctionApplication' fn (ForAll ident ty _) arg ret = do
634− replaced <- replaceVarWithUnknown ident ty
635− checkFunctionApplication fn replaced arg ret
636−checkFunctionApplication' fn u@(TUnknown _) arg ret = do
637− arg' <- do
638− TypedValue _ arg' t <- infer arg
639− (arg'', t') <- instantiatePolyTypeWithUnknowns arg' t
640− return $ TypedValue True arg'' t'
641− let ty = (\(TypedValue _ _ t) -> t) arg'
642− ret' <- maybe fresh return ret
643− u =?= function ty ret'
644− return (ret', App fn arg')
645−checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) arg ret = do
646− ty <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs
647− checkFunctionApplication fn ty arg ret
648−checkFunctionApplication' fn (KindedType ty _) arg ret =
649− checkFunctionApplication fn ty arg ret
650−checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg ret = do
651− dicts <- getTypeClassDictionaries
652− checkFunctionApplication' (foldl App fn (map (flip (TypeClassDictionary True) dicts) constraints)) fnTy arg ret
653−checkFunctionApplication' fn fnTy dict@TypeClassDictionary{} _ =
654− return (fnTy, App fn dict)
655−checkFunctionApplication' _ fnTy arg _ = throwError . strMsg $ "Cannot apply a function of type "
656− ++ prettyPrintType fnTy
657− ++ " to argument " ++ prettyPrintValue arg
658−
659−-- |
660−-- Compute the meet of two types, i.e. the most general type which both types subsume.
661−-- TODO: handle constrained types
662−--
663−meet :: Expr -> Expr -> Type -> Type -> UnifyT Type Check (Expr, Expr, Type)
664−meet e1 e2 (ForAll ident t1 _) t2 = do
665− t1' <- replaceVarWithUnknown ident t1
666− meet e1 e2 t1' t2
667−meet e1 e2 t1 (ForAll ident t2 _) = do
668− t2' <- replaceVarWithUnknown ident t2
669− meet e1 e2 t1 t2'
670−meet e1 e2 t1 t2 = do
671− t1 =?= t2
672− return (e1, e2, t1)
673−
674−-- |
675−-- Ensure a set of property names and value does not contain duplicate labels
676−--
677−ensureNoDuplicateProperties :: (Error e, MonadError e m) => [(String, Expr)] -> m ()
678−ensureNoDuplicateProperties ps = guardWith (strMsg "Duplicate property names") $ length (nub . map fst $ ps) == length ps