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