KindCheck.lhs 13.3 KB
Newer Older
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
1
2
3
4
5
6
% $Id: KindCheck.lhs,v 1.33 2004/02/13 19:24:04 wlux Exp $
%
% Copyright (c) 1999-2004, Wolfgang Lux
% See LICENSE for the full license.
%
% Modified by Martin Engelke (men@informatik.uni-kiel.de)
Björn Peemöller 's avatar
Björn Peemöller committed
7
% Modified by Björn Peemöller (bjp@informatik.uni-kiel.de)
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
8
9
10
11
12
13
14
15
16
17
%
\nwfilename{KindCheck.lhs}
\section{Checking Type Definitions}
After the source file has been parsed and all modules have been
imported, the compiler first performs kind checking on all type
definitions and signatures. Because Curry currently does not support
type classes, kind checking is rather trivial. All types must be of
first order kind ($\star$), i.e., all type constructor applications
must be saturated.

Björn Peemöller 's avatar
Björn Peemöller committed
18
During kind checking, this module will also disambiguate nullary type
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
19
20
21
22
23
24
25
constructors and type variables which -- in contrast to Haskell -- is
not possible on purely syntactic criteria. In addition it is checked
that all type constructors and type variables occurring on the right
hand side of a type declaration are actually defined and no identifier
is defined more than once.
\begin{verbatim}

Björn Peemöller 's avatar
Björn Peemöller committed
26
> module Checks.KindCheck (kindCheck) where
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
27

Björn Peemöller 's avatar
Björn Peemöller committed
28
29
> import Control.Monad (forM, liftM, liftM2, liftM3, when)
> import qualified Control.Monad.State as S (State, runState, gets, modify)
30

Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
31
32
33
34
> import Curry.Base.Position
> import Curry.Base.Ident
> import Curry.Syntax

Björn Peemöller 's avatar
Björn Peemöller committed
35
36
37
> import Base.Messages (Message, posErr, qposErr, internalError)
> import Base.TopEnv
> import Base.Utils (findMultiples)
Björn Peemöller 's avatar
Björn Peemöller committed
38
39

> import Env.TypeConstructors (TCEnv, tcArity)
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
40
41
42
43
44
45
46
47
48
49
50

\end{verbatim}
In order to check type constructor applications, the compiler
maintains an environment containing the kind information for all type
constructors. The function \texttt{kindCheck} first initializes this
environment by filtering out the arity of each type constructor from
the imported type environment. Next, the arities of all locally
defined type constructors are inserted into the environment, and,
finally, the declarations are checked within this environment.
\begin{verbatim}

Björn Peemöller 's avatar
Björn Peemöller committed
51
52
53
54
55
56
57
> kindCheck :: ModuleIdent -> TCEnv -> [Decl] -> ([Decl], [Message])
> kindCheck m tcEnv decls = case findMultiples $ map typeConstr tds of
>   [] -> runKCM (mapM checkDecl decls) initState
>   ms -> (decls, map errMultipleDeclaration ms)
>   where tds       = filter isTypeDecl decls
>         kEnv      = foldr (bindKind m) (fmap tcArity tcEnv) tds
>         initState = KCState m kEnv []
58

Björn Peemöller 's avatar
Björn Peemöller committed
59
60
61
\end{verbatim}
The kind check monad.
\begin{verbatim}
62

Björn Peemöller 's avatar
Björn Peemöller committed
63
> data KCState = KCState
64
65
>   { moduleIdent :: ModuleIdent
>   , kindEnv     :: KindEnv
Björn Peemöller 's avatar
Björn Peemöller committed
66
>   , errors      :: [Message]
67
68
>   }

Björn Peemöller 's avatar
Björn Peemöller committed
69
70
71
72
73
74
75
> type KCM = S.State KCState -- the Kind Check Monad

> runKCM :: KCM a -> KCState -> (a, [Message])
> runKCM kcm s = let (a, s') = S.runState kcm s in (a, reverse $ errors s')

> getModuleIdent :: KCM ModuleIdent
> getModuleIdent = S.gets moduleIdent
76

Björn Peemöller 's avatar
Björn Peemöller committed
77
78
> getKindEnv :: KCM KindEnv
> getKindEnv = S.gets kindEnv
79

Björn Peemöller 's avatar
Björn Peemöller committed
80
81
> report :: Message -> KCM ()
> report err = S.modify (\ s -> s { errors = err : errors s })
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
82
83
84
85
86
87
88

\end{verbatim}
The kind environment only needs to record the arity of each type constructor.
\begin{verbatim}

> type KindEnv = TopEnv Int

89
90
91
92
93
> bindKind :: ModuleIdent -> Decl -> KindEnv -> KindEnv
> bindKind m (DataDecl    _ tc tvs _) = bindKind' m tc tvs
> bindKind m (NewtypeDecl _ tc tvs _) = bindKind' m tc tvs
> bindKind m (TypeDecl    _ tc tvs _) = bindKind' m tc tvs
> bindKind _ _                        = id
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
94

95
> bindKind' :: ModuleIdent -> Ident -> [Ident] -> KindEnv -> KindEnv
Björn Peemöller 's avatar
Björn Peemöller committed
96
97
98
99
> bindKind' m tc tvs = bindTopEnv     "KindCheck.bindKind'"  tc arity
>                    . qualBindTopEnv "KindCheck.bindKind'" qtc arity
>   where arity = length tvs
>         qtc   = qualifyWith m tc
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
100
101
102
103
104
105
106
107
108
109
110
111
112
113

> lookupKind :: Ident -> KindEnv -> [Int]
> lookupKind = lookupTopEnv

> qualLookupKind :: QualIdent -> KindEnv -> [Int]
> qualLookupKind = qualLookupTopEnv

\end{verbatim}
When type declarations are checked, the compiler will allow anonymous
type variables on the left hand side of the declaration, but not on
the right hand side. Function and pattern declarations must be
traversed because they can contain local type signatures.
\begin{verbatim}

Björn Peemöller 's avatar
Björn Peemöller committed
114
> checkDecl :: Decl -> KCM Decl
115
116
117
118
119
120
121
122
123
124
125
126
> checkDecl (DataDecl      p tc tvs cs) = do
>   tvs' <- checkTypeLhs tvs
>   cs'  <- mapM (checkConstrDecl tvs') cs
>   return $ DataDecl p tc tvs' cs'
> checkDecl (NewtypeDecl   p tc tvs nc) = do
>   tvs' <- checkTypeLhs tvs
>   nc'  <- checkNewConstrDecl tvs' nc
>   return $ NewtypeDecl p tc tvs' nc'
> checkDecl (TypeDecl      p tc tvs ty) = do
>   tvs' <- checkTypeLhs tvs
>   ty'  <- checkClosedType tvs' ty
>   return $ TypeDecl p tc tvs' ty'
Björn Peemöller 's avatar
Björn Peemöller committed
127
128
129
130
131
132
133
134
> checkDecl (TypeSig           p vs ty) =
>   TypeSig p vs `liftM` checkType ty
> checkDecl (FunctionDecl      p f eqs) =
>   FunctionDecl p f `liftM` mapM checkEquation eqs
> checkDecl (PatternDecl       p t rhs) =
>   PatternDecl p t `liftM` checkRhs rhs
> checkDecl (ExternalDecl p cc ie f ty) =
>   ExternalDecl p cc ie f `liftM` checkType ty
135
136
> checkDecl d                           = return d

Björn Peemöller 's avatar
Björn Peemöller committed
137
> checkConstrDecl :: [Ident] -> ConstrDecl -> KCM ConstrDecl
138
139
140
141
142
143
144
145
146
147
148
> checkConstrDecl tvs (ConstrDecl p evs c tys) = do
>   evs' <- checkTypeLhs evs
>   tys' <- mapM (checkClosedType (evs' ++ tvs)) tys
>   return $ ConstrDecl p evs' c tys'
> checkConstrDecl tvs (ConOpDecl p evs ty1 op ty2) = do
>   evs' <- checkTypeLhs evs
>   let tvs' = evs' ++ tvs
>   ty1' <- checkClosedType tvs' ty1
>   ty2' <- checkClosedType tvs' ty2
>   return $ ConOpDecl p evs' ty1' op ty2'

Björn Peemöller 's avatar
Björn Peemöller committed
149
> checkNewConstrDecl :: [Ident] -> NewConstrDecl -> KCM NewConstrDecl
150
151
152
153
154
155
156
157
158
> checkNewConstrDecl tvs (NewConstrDecl p evs c ty) = do
>   evs' <- checkTypeLhs evs
>   ty'  <- checkClosedType (evs' ++ tvs) ty
>   return $ NewConstrDecl p evs' c ty'

> -- |Check the left-hand-side of a type declaration for
> -- * Anonymous type variables are allowed
> -- * only type variables (no type constructors)
> -- * linearity
Björn Peemöller 's avatar
Björn Peemöller committed
159
> checkTypeLhs :: [Ident] -> KCM [Ident]
160
161
162
> checkTypeLhs []         = return []
> checkTypeLhs (tv : tvs) = do
>   when (tv /= anonId) $ do
Björn Peemöller 's avatar
Björn Peemöller committed
163
164
165
166
>     isTyCons <- (not . null . lookupKind tv) `liftM` getKindEnv
>     when isTyCons        $ report $ errNoVariable tv
>     when (tv `elem` tvs) $ report $ errNonLinear  tv
>   (tv :) `liftM` checkTypeLhs tvs
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
167
168
169
170
171
172
173

\end{verbatim}
Checking expressions is rather straight forward. The compiler must
only traverse the structure of expressions in order to find local
declaration groups.
\begin{verbatim}

Björn Peemöller 's avatar
Björn Peemöller committed
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
> checkEquation :: Equation -> KCM Equation
> checkEquation (Equation p lhs rhs) = Equation p lhs `liftM` checkRhs rhs

> checkRhs :: Rhs -> KCM Rhs
> checkRhs (SimpleRhs p e ds) =
>   liftM2 (SimpleRhs p) (checkExpr e) (mapM checkDecl ds)
> checkRhs (GuardedRhs es ds) =
>   liftM2 GuardedRhs (mapM checkCondExpr es) (mapM checkDecl ds)

> checkCondExpr :: CondExpr -> KCM CondExpr
> checkCondExpr (CondExpr p g e) =
>   liftM2 (CondExpr p) (checkExpr g) (checkExpr e)

> checkExpr :: Expression -> KCM Expression
> checkExpr l@(Literal         _) = return l
> checkExpr v@(Variable        _) = return v
> checkExpr c@(Constructor     _) = return c
> checkExpr (Paren             e) = Paren `liftM` checkExpr e
> checkExpr (Typed          e ty) = liftM2 Typed (checkExpr e) (checkType ty)
> checkExpr (Tuple          p es) = Tuple p `liftM` mapM checkExpr es
> checkExpr (List           p es) = List  p `liftM` mapM checkExpr es
> checkExpr (ListCompr    p e qs) =
>   liftM2 (ListCompr p) (checkExpr e) (mapM checkStmt qs)
> checkExpr (EnumFrom         e) = EnumFrom `liftM` checkExpr e
> checkExpr (EnumFromThen  e1 e2) =
>   liftM2 EnumFromThen (checkExpr e1) (checkExpr e2)
> checkExpr (EnumFromTo    e1 e2) =
>   liftM2 EnumFromTo (checkExpr e1) (checkExpr e2)
> checkExpr (EnumFromThenTo e1 e2 e3) =
>   liftM3 EnumFromThenTo (checkExpr e1) (checkExpr e2) (checkExpr e3)
> checkExpr (UnaryMinus     op e) = UnaryMinus op `liftM` checkExpr e
> checkExpr (Apply         e1 e2) = liftM2 Apply (checkExpr e1) (checkExpr e2)
> checkExpr (InfixApply e1 op e2) =
>   liftM2 (\f1 f2 -> InfixApply f1 op f2) (checkExpr e1) (checkExpr e2)
> checkExpr (LeftSection    e op) = flip LeftSection op `liftM` checkExpr e
> checkExpr (RightSection   op e) = RightSection op `liftM` checkExpr e
> checkExpr (Lambda       r ts e) = Lambda r ts `liftM` checkExpr e
> checkExpr (Let            ds e) =
>   liftM2 Let (mapM checkDecl ds) (checkExpr e)
> checkExpr (Do            sts e) =
>   liftM2 Do (mapM checkStmt sts) (checkExpr e)
> checkExpr (IfThenElse r e1 e2 e3) =
>   liftM3 (IfThenElse r) (checkExpr e1) (checkExpr e2) (checkExpr e3)
> checkExpr (Case       r e alts) =
>   liftM2 (Case r) (checkExpr e) (mapM checkAlt alts)
> checkExpr (RecordConstr     fs) =
>   RecordConstr `liftM` mapM checkFieldExpr fs
> checkExpr (RecordSelection e l) =
>   flip RecordSelection l `liftM` checkExpr e
> checkExpr (RecordUpdate   fs e) =
>   liftM2 RecordUpdate (mapM checkFieldExpr fs) (checkExpr e)

> checkStmt :: Statement -> KCM Statement
> checkStmt (StmtExpr   p e) = StmtExpr p   `liftM` checkExpr e
> checkStmt (StmtBind p t e) = StmtBind p t `liftM` checkExpr e
> checkStmt (StmtDecl    ds) = StmtDecl     `liftM` mapM checkDecl ds

> checkAlt :: Alt -> KCM Alt
> checkAlt (Alt p t rhs) = Alt p t `liftM` checkRhs rhs

> checkFieldExpr :: Field Expression -> KCM (Field Expression)
> checkFieldExpr (Field p l e) = Field p l `liftM` checkExpr e
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
236
237
238
239
240
241
242
243

\end{verbatim}
The parser cannot distinguish unqualified nullary type constructors
and type variables. Therefore, if the compiler finds an unbound
identifier in a position where a type variable is admissible, it will
interpret the identifier as such.
\begin{verbatim}

Björn Peemöller 's avatar
Björn Peemöller committed
244
> checkClosedType :: [Ident] -> TypeExpr -> KCM TypeExpr
245
> checkClosedType tvs ty = checkType ty >>= checkClosed tvs
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
246

Björn Peemöller 's avatar
Björn Peemöller committed
247
> checkType :: TypeExpr -> KCM TypeExpr
248
> checkType c@(ConstructorType tc tys) = do
Björn Peemöller 's avatar
Björn Peemöller committed
249
250
>   m <- getModuleIdent
>   kEnv <- getKindEnv
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
251
252
>   case qualLookupKind tc kEnv of
>     []
Björn Peemöller 's avatar
Björn Peemöller committed
253
254
255
>       | not (isQualified tc) && null tys ->
>           return $ VariableType $ unqualify tc
>       | otherwise -> report (errUndefinedType tc) >> return c
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
256
>     [n]
Björn Peemöller 's avatar
Björn Peemöller committed
257
258
>       | n == n'   -> ConstructorType tc `liftM` mapM checkType tys
>       | otherwise -> report (errWrongArity tc n n') >> return c
259
>     _ -> case qualLookupKind (qualQualify m tc) kEnv of
Björn Peemöller 's avatar
Björn Peemöller committed
260
261
262
263
>       [n]
>         | n == n'   -> ConstructorType tc `liftM` mapM checkType tys
>         | otherwise -> report (errWrongArity tc n n') >> return c
>       _ -> report (errAmbiguousType tc) >> return c
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
264
>  where n' = length tys
Björn Peemöller 's avatar
Björn Peemöller committed
265
266
267
268
269
270
271
272
273
274
275
> checkType v@(VariableType tv)
>   | tv == anonId = return v
>   | otherwise    = checkType $ ConstructorType (qualify tv) []
> checkType (TupleType     tys) = TupleType `liftM` mapM checkType tys
> checkType (ListType       ty) = ListType  `liftM` checkType ty
> checkType (ArrowType ty1 ty2) =
>   liftM2 ArrowType (checkType ty1) (checkType ty2)
> checkType (RecordType   fs r) = do
>   fs' <- forM fs $ \ (l, ty) -> do
>     ty' <- checkType ty
>     return (l, ty')
276
277
278
279
280
>   r'  <- case r of
>     Nothing -> return Nothing
>     Just ar -> Just `liftM` checkType ar
>   return $ RecordType fs' r'

Björn Peemöller 's avatar
Björn Peemöller committed
281
282
283
284
285
286
287
288
289
290
291
292
> checkClosed :: [Ident] -> TypeExpr -> KCM TypeExpr
> checkClosed tvs (ConstructorType tc tys) =
>   ConstructorType tc `liftM` mapM (checkClosed tvs) tys
> checkClosed tvs v@(VariableType      tv) = do
>   when (tv == anonId || tv `notElem` tvs) $ report $ errUnboundVariable tv
>   return v
> checkClosed tvs (TupleType     tys) =
>   TupleType `liftM` mapM (checkClosed tvs) tys
> checkClosed tvs (ListType       ty) =
>   ListType `liftM` checkClosed tvs ty
> checkClosed tvs (ArrowType ty1 ty2) =
>   liftM2 ArrowType (checkClosed tvs ty1) (checkClosed tvs ty2)
293
> checkClosed tvs (RecordType   fs r) = do
Björn Peemöller 's avatar
Björn Peemöller committed
294
295
296
>   fs' <- forM fs $ \ (l, ty) -> do
>     ty' <- checkClosed tvs ty
>     return (l, ty')
297
298
299
300
>   r'  <- case r of
>     Nothing -> return Nothing
>     Just ar -> Just `liftM` checkClosed tvs ar
>   return $ RecordType fs' r'
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
301
302
303
304
305

\end{verbatim}
Auxiliary definitions
\begin{verbatim}

306
307
308
309
310
> typeConstr :: Decl -> Ident
> typeConstr (DataDecl    _ tc _ _) = tc
> typeConstr (NewtypeDecl _ tc _ _) = tc
> typeConstr (TypeDecl    _ tc _ _) = tc
> typeConstr _ = internalError "KindCheck.typeConstr: no type declaration"
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
311
312
313
314
315

\end{verbatim}
Error messages:
\begin{verbatim}

Björn Peemöller 's avatar
Björn Peemöller committed
316
> errUndefinedType :: QualIdent -> Message
317
318
> errUndefinedType tc = qposErr tc $ "Undefined type " ++ qualName tc

Björn Peemöller 's avatar
Björn Peemöller committed
319
> errAmbiguousType :: QualIdent -> Message
320
321
> errAmbiguousType tc = qposErr tc $ "Ambiguous type " ++ qualName tc

Björn Peemöller 's avatar
Björn Peemöller committed
322
323
324
325
326
327
328
> errMultipleDeclaration :: [Ident] -> Message
> errMultipleDeclaration []     = internalError
>   "KindCheck.errMultipleDeclaration: empty list"
> errMultipleDeclaration (i:is) = posErr i $
>   "Multiple declarations for type `" ++ name i ++ "` at:\n"
>   ++ unlines (map showPos (i:is))
>   where showPos = ("    " ++) . showLine . positionOfIdent
329

Björn Peemöller 's avatar
Björn Peemöller committed
330
> errNonLinear :: Ident -> Message
331
332
333
> errNonLinear tv = posErr tv $ "Type variable " ++ name tv ++
>   " occurs more than once on left hand side of type declaration"

Björn Peemöller 's avatar
Björn Peemöller committed
334
> errNoVariable :: Ident -> Message
335
336
337
> errNoVariable tv = posErr tv $ "Type constructor " ++ name tv ++
>   " used in left hand side of type declaration"

Björn Peemöller 's avatar
Björn Peemöller committed
338
> errWrongArity :: QualIdent -> Int -> Int -> Message
339
> errWrongArity tc arity argc = qposErr tc $
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
340
>   "Type constructor " ++ qualName tc ++ " expects " ++ arguments arity ++
341
>   " but is applied to " ++ show argc
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
342
343
344
345
>   where arguments 0 = "no arguments"
>         arguments 1 = "1 argument"
>         arguments n = show n ++ " arguments"

Björn Peemöller 's avatar
Björn Peemöller committed
346
> errUnboundVariable :: Ident -> Message
347
348
> errUnboundVariable tv = posErr tv $ "Unbound type variable " ++ name tv

Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
349
\end{verbatim}