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