git.iko.soy/rowtype-yoga/purescript-native
on fca3655 help sign in
rowtype-yoga/purescript-native/src/Language/PureScript/TypeChecker.hs
457 lines 19 kB history raw
1{-# LANGUAGE FlexibleInstances #-}
3-- |
4-- The top-level type checker, which checks all declarations in a module.
5--
6module Language.PureScript.TypeChecker
7 ( module T
8 , typeCheckModule
9 , checkNewtype
10 ) where
12import Prelude.Compat
14import Control.Monad (when, unless, void, forM)
15import Control.Monad.Error.Class (MonadError(..))
16import Control.Monad.State.Class (MonadState(..), modify)
17import Control.Monad.Supply.Class (MonadSupply)
18import Control.Monad.Writer.Class (MonadWriter(..))
19import Control.Lens ((^..), _1, _2)
21import Data.Foldable (for_, traverse_)
22import Data.List (nub, nubBy, (\\), sort, group)
23import Data.Maybe
24import qualified Data.Map as M
25import qualified Data.Set as S
26import Data.Monoid ((<>))
27import qualified Data.Text as T
28import Data.Text (Text)
30import Language.PureScript.AST
31import Language.PureScript.Crash
32import Language.PureScript.Environment
33import Language.PureScript.Errors
34import Language.PureScript.Kinds
35import Language.PureScript.Linter
36import Language.PureScript.Names
37import Language.PureScript.Traversals
38import Language.PureScript.TypeChecker.Kinds as T
39import Language.PureScript.TypeChecker.Monad as T
40import Language.PureScript.TypeChecker.Synonyms as T
41import Language.PureScript.TypeChecker.Types as T
42import Language.PureScript.TypeClassDictionaries
43import Language.PureScript.Types
45addDataType
46 :: (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
47 => ModuleName
48 -> DataDeclType
49 -> ProperName 'TypeName
50 -> [(Text, Maybe Kind)]
51 -> [(ProperName 'ConstructorName, [Type])]
52 -> Kind
53 -> m ()
54addDataType moduleName dtype name args dctors ctorKind = do
55 env <- getEnv
56 putEnv $ env { types = M.insert (Qualified (Just moduleName) name) (ctorKind, DataType args dctors) (types env) }
57 for_ dctors $ \(dctor, tys) ->
58 warnAndRethrow (addHint (ErrorInDataConstructor dctor)) $
59 addDataConstructor moduleName dtype name (map fst args) dctor tys
61addDataConstructor
62 :: (MonadState CheckState m, MonadError MultipleErrors m)
63 => ModuleName
64 -> DataDeclType
65 -> ProperName 'TypeName
66 -> [Text]
67 -> ProperName 'ConstructorName
68 -> [Type]
69 -> m ()
70addDataConstructor moduleName dtype name args dctor tys = do
71 env <- getEnv
72 traverse_ checkTypeSynonyms tys
73 let retTy = foldl TypeApp (TypeConstructor (Qualified (Just moduleName) name)) (map TypeVar args)
74 let dctorTy = foldr function retTy tys
75 let polyType = mkForAll args dctorTy
76 let fields = [Ident ("value" <> T.pack (show n)) | n <- [0..(length tys - 1)]]
77 putEnv $ env { dataConstructors = M.insert (Qualified (Just moduleName) dctor) (dtype, name, polyType, fields) (dataConstructors env) }
79addTypeSynonym
80 :: (MonadState CheckState m, MonadError MultipleErrors m)
81 => ModuleName
82 -> ProperName 'TypeName
83 -> [(Text, Maybe Kind)]
84 -> Type
85 -> Kind
86 -> m ()
87addTypeSynonym moduleName name args ty kind = do
88 env <- getEnv
89 checkTypeSynonyms ty
90 putEnv $ env { types = M.insert (Qualified (Just moduleName) name) (kind, TypeSynonym) (types env)
91 , typeSynonyms = M.insert (Qualified (Just moduleName) name) (args, ty) (typeSynonyms env) }
93valueIsNotDefined
94 :: (MonadState CheckState m, MonadError MultipleErrors m)
95 => ModuleName
96 -> Ident
97 -> m ()
98valueIsNotDefined moduleName name = do
99 env <- getEnv
100 case M.lookup (Qualified (Just moduleName) name) (names env) of
101 Just _ -> throwError . errorMessage $ RedefinedIdent name
102 Nothing -> return ()
104addValue
105 :: (MonadState CheckState m)
106 => ModuleName
107 -> Ident
108 -> Type
109 -> NameKind
110 -> m ()
111addValue moduleName name ty nameKind = do
112 env <- getEnv
113 putEnv (env { names = M.insert (Qualified (Just moduleName) name) (ty, nameKind, Defined) (names env) })
115addTypeClass
116 :: (MonadState CheckState m)
117 => ModuleName
118 -> ProperName 'ClassName
119 -> [(Text, Maybe Kind)]
120 -> [Constraint]
121 -> [FunctionalDependency]
122 -> [Declaration]
123 -> m ()
124addTypeClass moduleName pn args implies dependencies ds =
125 modify $ \st -> st { checkEnv = (checkEnv st) { typeClasses = M.insert (Qualified (Just moduleName) pn) newClass (typeClasses . checkEnv $ st) } }
126 where
127 newClass :: TypeClassData
128 newClass = makeTypeClassData args (map toPair ds) implies dependencies
130 toPair (TypeDeclaration ident ty) = (ident, ty)
131 toPair (PositionedDeclaration _ _ d) = toPair d
132 toPair _ = internalError "Invalid declaration in TypeClassDeclaration"
134addTypeClassDictionaries
135 :: (MonadState CheckState m)
136 => Maybe ModuleName
137 -> M.Map (Qualified (ProperName 'ClassName)) (M.Map (Qualified Ident) NamedDict)
138 -> m ()
139addTypeClassDictionaries mn entries =
140 modify $ \st -> st { checkEnv = (checkEnv st) { typeClassDictionaries = insertState st } }
141 where insertState st = M.insertWith (M.unionWith M.union) mn entries (typeClassDictionaries . checkEnv $ st)
143checkDuplicateTypeArguments
144 :: (MonadState CheckState m, MonadError MultipleErrors m)
145 => [Text]
146 -> m ()
147checkDuplicateTypeArguments args = for_ firstDup $ \dup ->
148 throwError . errorMessage $ DuplicateTypeArgument dup
149 where
150 firstDup :: Maybe Text
151 firstDup = listToMaybe $ args \\ nub args
153checkTypeClassInstance
154 :: (MonadState CheckState m, MonadError MultipleErrors m)
155 => TypeClassData
156 -> Int -- ^ index of type class argument
157 -> Type
158 -> m ()
159checkTypeClassInstance cls i = check where
160 -- If the argument is determined via fundeps then we are less restrictive in
161 -- what type is allowed. This is because the type cannot be used to influence
162 -- which instance is selected. Currently the only weakened restriction is that
163 -- row types are allowed in determined type class arguments.
164 isFunDepDetermined = S.member i (typeClassDeterminedArguments cls)
165 check = \case
166 TypeVar _ -> return ()
167 TypeLevelString _ -> return ()
168 TypeConstructor ctor -> do
169 env <- getEnv
170 when (ctor `M.member` typeSynonyms env) . throwError . errorMessage $ TypeSynonymInstance
171 return ()
172 TypeApp t1 t2 -> check t1 >> check t2
173 REmpty | isFunDepDetermined -> return ()
174 RCons _ hd tl | isFunDepDetermined -> check hd >> check tl
175 ty -> throwError . errorMessage $ InvalidInstanceHead ty
177-- |
178-- Check that type synonyms are fully-applied in a type
179--
180checkTypeSynonyms
181 :: (MonadState CheckState m, MonadError MultipleErrors m)
182 => Type
183 -> m ()
184checkTypeSynonyms = void . replaceAllTypeSynonyms
186-- |
187-- Type check all declarations in a module
188--
189-- At this point, many declarations will have been desugared, but it is still necessary to
190--
191-- * Kind-check all types and add them to the @Environment@
192--
193-- * Type-check all values and add them to the @Environment@
194--
195-- * Bring type class instances into scope
196--
197-- * Process module imports
198--
199typeCheckAll
200 :: forall m
201 . (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
202 => ModuleName
203 -> [DeclarationRef]
204 -> [Declaration]
205 -> m [Declaration]
206typeCheckAll moduleName _ = traverse go
207 where
208 go :: Declaration -> m Declaration
209 go (DataDeclaration dtype name args dctors) = do
210 warnAndRethrow (addHint (ErrorInTypeConstructor name)) $ do
211 when (dtype == Newtype) $ checkNewtype name dctors
212 checkDuplicateTypeArguments $ map fst args
213 ctorKind <- kindsOf True moduleName name args (concatMap snd dctors)
214 let args' = args `withKinds` ctorKind
215 addDataType moduleName dtype name args' dctors ctorKind
216 return $ DataDeclaration dtype name args dctors
217 go (d@(DataBindingGroupDeclaration tys)) = do
218 let syns = mapMaybe toTypeSynonym tys
219 dataDecls = mapMaybe toDataDecl tys
220 bindingGroupNames = nub ((syns^..traverse._1) ++ (dataDecls^..traverse._2))
221 warnAndRethrow (addHint (ErrorInDataBindingGroup bindingGroupNames)) $ do
222 (syn_ks, data_ks) <- kindsOfAll moduleName syns (map (\(_, name, args, dctors) -> (name, args, concatMap snd dctors)) dataDecls)
223 for_ (zip dataDecls data_ks) $ \((dtype, name, args, dctors), ctorKind) -> do
224 when (dtype == Newtype) $ checkNewtype name dctors
225 checkDuplicateTypeArguments $ map fst args
226 let args' = args `withKinds` ctorKind
227 addDataType moduleName dtype name args' dctors ctorKind
228 for_ (zip syns syn_ks) $ \((name, args, ty), kind) -> do
229 checkDuplicateTypeArguments $ map fst args
230 let args' = args `withKinds` kind
231 addTypeSynonym moduleName name args' ty kind
232 return d
233 where
234 toTypeSynonym (TypeSynonymDeclaration nm args ty) = Just (nm, args, ty)
235 toTypeSynonym (PositionedDeclaration _ _ d') = toTypeSynonym d'
236 toTypeSynonym _ = Nothing
237 toDataDecl (DataDeclaration dtype nm args dctors) = Just (dtype, nm, args, dctors)
238 toDataDecl (PositionedDeclaration _ _ d') = toDataDecl d'
239 toDataDecl _ = Nothing
240 go (TypeSynonymDeclaration name args ty) = do
241 warnAndRethrow (addHint (ErrorInTypeSynonym name)) $ do
242 checkDuplicateTypeArguments $ map fst args
243 kind <- kindsOf False moduleName name args [ty]
244 let args' = args `withKinds` kind
245 addTypeSynonym moduleName name args' ty kind
246 return $ TypeSynonymDeclaration name args ty
247 go TypeDeclaration{} =
248 internalError "Type declarations should have been removed before typeCheckAlld"
249 go (ValueDeclaration name nameKind [] (Right val)) = do
250 env <- getEnv
251 warnAndRethrow (addHint (ErrorInValueDeclaration name)) $ do
252 val' <- checkExhaustiveExpr env moduleName val
253 valueIsNotDefined moduleName name
254 [(_, (val'', ty))] <- typesOf NonRecursiveBindingGroup moduleName [(name, val')]
255 addValue moduleName name ty nameKind
256 return $ ValueDeclaration name nameKind [] $ Right val''
257 go ValueDeclaration{} = internalError "Binders were not desugared"
258 go (BindingGroupDeclaration vals) = do
259 env <- getEnv
260 warnAndRethrow (addHint (ErrorInBindingGroup (map (\(ident, _, _) -> ident) vals))) $ do
261 for_ vals $ \(ident, _, _) ->
262 valueIsNotDefined moduleName ident
263 vals' <- mapM (thirdM (checkExhaustiveExpr env moduleName)) vals
264 tys <- typesOf RecursiveBindingGroup moduleName $ map (\(ident, _, ty) -> (ident, ty)) vals'
265 vals'' <- forM [ (name, val, nameKind, ty)
266 | (name, nameKind, _) <- vals'
267 , (name', (val, ty)) <- tys
268 , name == name'
269 ] $ \(name, val, nameKind, ty) -> do
270 addValue moduleName name ty nameKind
271 return (name, nameKind, val)
272 return $ BindingGroupDeclaration vals''
273 go (d@(ExternDataDeclaration name kind)) = do
274 env <- getEnv
275 putEnv $ env { types = M.insert (Qualified (Just moduleName) name) (kind, ExternData) (types env) }
276 return d
277 go (d@(ExternKindDeclaration name)) = do
278 env <- getEnv
279 putEnv $ env { kinds = S.insert (Qualified (Just moduleName) name) (kinds env) }
280 return d
281 go (d@(ExternDeclaration name ty)) = do
282 warnAndRethrow (addHint (ErrorInForeignImport name)) $ do
283 env <- getEnv
284 kind <- kindOf ty
285 guardWith (errorMessage (ExpectedType ty kind)) $ kind == kindType
286 case M.lookup (Qualified (Just moduleName) name) (names env) of
287 Just _ -> throwError . errorMessage $ RedefinedIdent name
288 Nothing -> putEnv (env { names = M.insert (Qualified (Just moduleName) name) (ty, External, Defined) (names env) })
289 return d
290 go d@FixityDeclaration{} = return d
291 go d@ImportDeclaration{} = return d
292 go d@(TypeClassDeclaration pn args implies deps tys) = do
293 addTypeClass moduleName pn args implies deps tys
294 return d
295 go (d@(TypeInstanceDeclaration dictName deps className tys body)) = rethrow (addHint (ErrorInInstance className tys)) $ do
296 env <- getEnv
297 case M.lookup className (typeClasses env) of
298 Nothing -> internalError "typeCheckAll: Encountered unknown type class in instance declaration"
299 Just typeClass -> do
300 sequence_ (zipWith (checkTypeClassInstance typeClass) [0..] tys)
301 checkOrphanInstance dictName className tys
302 _ <- traverseTypeInstanceBody checkInstanceMembers body
303 let dict = TypeClassDictionaryInScope (Qualified (Just moduleName) dictName) [] className tys (Just deps)
304 addTypeClassDictionaries (Just moduleName) . M.singleton className $ M.singleton (tcdValue dict) dict
305 return d
306 go (PositionedDeclaration pos com d) =
307 warnAndRethrowWithPosition pos $ PositionedDeclaration pos com <$> go d
309 checkInstanceMembers :: [Declaration] -> m [Declaration]
310 checkInstanceMembers instDecls = do
311 let idents = sort . map head . group . map memberName $ instDecls
312 for_ (firstDuplicate idents) $ \ident ->
313 throwError . errorMessage $ DuplicateValueDeclaration ident
314 return instDecls
315 where
316 memberName :: Declaration -> Ident
317 memberName (ValueDeclaration ident _ _ _) = ident
318 memberName (PositionedDeclaration _ _ d) = memberName d
319 memberName _ = internalError "checkInstanceMembers: Invalid declaration in type instance definition"
321 firstDuplicate :: (Eq a) => [a] -> Maybe a
322 firstDuplicate (x : xs@(y : _))
323 | x == y = Just x
324 | otherwise = firstDuplicate xs
325 firstDuplicate _ = Nothing
327 checkOrphanInstance :: Ident -> Qualified (ProperName 'ClassName) -> [Type] -> m ()
328 checkOrphanInstance dictName className@(Qualified (Just mn') _) tys'
329 | moduleName == mn' || any checkType tys' = return ()
330 | otherwise = throwError . errorMessage $ OrphanInstance dictName className tys'
331 where
332 checkType :: Type -> Bool
333 checkType (TypeVar _) = False
334 checkType (TypeLevelString _) = False
335 checkType (TypeConstructor (Qualified (Just mn'') _)) = moduleName == mn''
336 checkType (TypeConstructor (Qualified Nothing _)) = internalError "Unqualified type name in checkOrphanInstance"
337 checkType (TypeApp t1 _) = checkType t1
338 checkType _ = internalError "Invalid type in instance in checkOrphanInstance"
339 checkOrphanInstance _ _ _ = internalError "Unqualified class name in checkOrphanInstance"
341 -- |
342 -- This function adds the argument kinds for a type constructor so that they may appear in the externs file,
343 -- extracted from the kind of the type constructor itself.
344 --
345 withKinds :: [(Text, Maybe Kind)] -> Kind -> [(Text, Maybe Kind)]
346 withKinds [] _ = []
347 withKinds (s@(_, Just _ ):ss) (FunKind _ k) = s : withKinds ss k
348 withKinds ( (s, Nothing):ss) (FunKind k1 k2) = (s, Just k1) : withKinds ss k2
349 withKinds _ _ = internalError "Invalid arguments to peelKinds"
351checkNewtype
352 :: forall m
353 . MonadError MultipleErrors m
354 => ProperName 'TypeName
355 -> [(ProperName 'ConstructorName, [Type])]
356 -> m ()
357checkNewtype _ [(_, [_])] = return ()
358checkNewtype name _ = throwError . errorMessage $ InvalidNewtype name
360-- |
361-- Type check an entire module and ensure all types and classes defined within the module that are
362-- required by exported members are also exported.
363--
364typeCheckModule
365 :: forall m
366 . (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
367 => Module
368 -> m Module
369typeCheckModule (Module _ _ _ _ Nothing) =
370 internalError "exports should have been elaborated before typeCheckModule"
371typeCheckModule (Module ss coms mn decls (Just exps)) =
372 warnAndRethrow (addHint (ErrorInModule mn)) $ do
373 modify (\s -> s { checkCurrentModule = Just mn })
374 decls' <- typeCheckAll mn exps decls
375 for_ exps $ \e -> do
376 checkTypesAreExported e
377 checkClassMembersAreExported e
378 checkClassesAreExported e
379 return $ Module ss coms mn decls' (Just exps)
380 where
382 checkMemberExport :: (Type -> [DeclarationRef]) -> DeclarationRef -> m ()
383 checkMemberExport extract dr@(TypeRef name dctors) = do
384 env <- getEnv
385 case M.lookup (Qualified (Just mn) name) (typeSynonyms env) of
386 Nothing -> return ()
387 Just (_, ty) -> checkExport dr extract ty
388 case dctors of
389 Nothing -> return ()
390 Just dctors' -> for_ dctors' $ \dctor ->
391 case M.lookup (Qualified (Just mn) dctor) (dataConstructors env) of
392 Nothing -> return ()
393 Just (_, _, ty, _) -> checkExport dr extract ty
394 return ()
395 checkMemberExport extract dr@(ValueRef name) = do
396 ty <- lookupVariable (Qualified (Just mn) name)
397 checkExport dr extract ty
398 checkMemberExport _ _ = return ()
400 checkExport :: DeclarationRef -> (Type -> [DeclarationRef]) -> Type -> m ()
401 checkExport dr extract ty = case filter (not . exported) (extract ty) of
402 [] -> return ()
403 hidden -> throwError . errorMessage $ TransitiveExportError dr (nubBy nubEq hidden)
404 where
405 exported e = any (exports e) exps
406 exports (TypeRef pn1 _) (TypeRef pn2 _) = pn1 == pn2
407 exports (ValueRef id1) (ValueRef id2) = id1 == id2
408 exports (TypeClassRef pn1) (TypeClassRef pn2) = pn1 == pn2
409 exports (PositionedDeclarationRef _ _ r1) r2 = exports r1 r2
410 exports r1 (PositionedDeclarationRef _ _ r2) = exports r1 r2
411 exports _ _ = False
412 -- We avoid Eq for `nub`bing as the dctor part of `TypeRef` evaluates to
413 -- `error` for the values generated here (we don't need them anyway)
414 nubEq (TypeRef pn1 _) (TypeRef pn2 _) = pn1 == pn2
415 nubEq r1 r2 = r1 == r2
418 -- Check that all the type constructors defined in the current module that appear in member types
419 -- have also been exported from the module
420 checkTypesAreExported :: DeclarationRef -> m ()
421 checkTypesAreExported = checkMemberExport findTcons
422 where
423 findTcons :: Type -> [DeclarationRef]
424 findTcons = everythingOnTypes (++) go
425 where
426 go (TypeConstructor (Qualified (Just mn') name)) | mn' == mn = [TypeRef name (internalError "Data constructors unused in checkTypesAreExported")]
427 go _ = []
429 -- Check that all the classes defined in the current module that appear in member types have also
430 -- been exported from the module
431 checkClassesAreExported :: DeclarationRef -> m ()
432 checkClassesAreExported = checkMemberExport findClasses
433 where
434 findClasses :: Type -> [DeclarationRef]
435 findClasses = everythingOnTypes (++) go
436 where
437 go (ConstrainedType cs _) = mapMaybe (fmap TypeClassRef . extractCurrentModuleClass . constraintClass) cs
438 go _ = []
439 extractCurrentModuleClass :: Qualified (ProperName 'ClassName) -> Maybe (ProperName 'ClassName)
440 extractCurrentModuleClass (Qualified (Just mn') name) | mn == mn' = Just name
441 extractCurrentModuleClass _ = Nothing
443 checkClassMembersAreExported :: DeclarationRef -> m ()
444 checkClassMembersAreExported dr@(TypeClassRef name) = do
445 let members = ValueRef `map` head (mapMaybe findClassMembers decls)
446 let missingMembers = members \\ exps
447 unless (null missingMembers) $ throwError . errorMessage $ TransitiveExportError dr members
448 where
449 findClassMembers :: Declaration -> Maybe [Ident]
450 findClassMembers (TypeClassDeclaration name' _ _ _ ds) | name == name' = Just $ map extractMemberName ds
451 findClassMembers (PositionedDeclaration _ _ d) = findClassMembers d
452 findClassMembers _ = Nothing
453 extractMemberName :: Declaration -> Ident
454 extractMemberName (PositionedDeclaration _ _ d) = extractMemberName d
455 extractMemberName (TypeDeclaration memberName _) = memberName
456 extractMemberName _ = internalError "Unexpected declaration in typeclass member list"
457 checkClassMembersAreExported _ = return ()