TypeCheck.lhs 53.4 KB
Newer Older
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
1
2
3
4
5
6
% $Id: TypeCheck.lhs,v 1.90 2004/11/06 18:34:07 wlux Exp $
%
% Copyright (c) 1999-2004, Wolfgang Lux
% See LICENSE for the full license.
%
% Modified by Martin Engelke (men@informatik.uni-kiel.de)
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
18
19
20
21
22
23
%
\nwfilename{TypeCheck.lhs}
\section{Type Checking Curry Programs}
This module implements the type checker of the Curry compiler. The
type checker is invoked after the syntactic correctness of the program
has been verified. Local variables have been renamed already. Thus the
compiler can maintain a flat type environment (which is necessary in
order to pass the type information to later phases of the compiler).
The type checker now checks the correct typing of all expressions and
also verifies that the type signatures given by the user match the
inferred types. The type checker uses algorithm
W~\cite{DamasMilner82:Principal} for inferring the types of
unannotated declarations, but allows for polymorphic recursion when a
type annotation is present.
\begin{verbatim}

Björn Peemöller 's avatar
Björn Peemöller committed
24
> module Checks.TypeCheck (typeCheck) where
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
25

26
27
> import Control.Monad (liftM, liftM2, liftM3, replicateM, unless)
> import qualified Control.Monad.State as S (State, execState, gets, modify)
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
28
29
> import Data.List (nub, partition)
> import qualified Data.Map as Map (Map, empty, insert, lookup)
30
> import Data.Maybe (catMaybes, fromJust, fromMaybe, isJust, listToMaybe, maybeToList)
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
31
32
33
> import qualified Data.Set as Set (Set, fromList, member, notMember, unions)

> import Curry.Base.Ident
Björn Peemöller 's avatar
Björn Peemöller committed
34
> import Curry.Base.Position
35
> import Curry.Base.Pretty
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
36
37
38
> import Curry.Syntax
> import Curry.Syntax.Pretty

Björn Peemöller 's avatar
Björn Peemöller committed
39
> import Base.CurryTypes (fromQualType, toType, toTypes)
40
> import Base.Expr
41
> import Base.Messages (Message, posMessage, internalError)
Björn Peemöller 's avatar
Björn Peemöller committed
42
> import Base.SCC
Björn Peemöller 's avatar
Björn Peemöller committed
43
> import Base.TopEnv
Björn Peemöller 's avatar
Björn Peemöller committed
44
45
> import Base.Types
> import Base.TypeSubst
Björn Peemöller 's avatar
Björn Peemöller committed
46
> import Base.Utils (foldr2)
Björn Peemöller 's avatar
Björn Peemöller committed
47

48
> import Env.TypeConstructor (TCEnv, TypeInfo (..), bindTypeInfo
49
>   , qualLookupTC)
Björn Peemöller 's avatar
Björn Peemöller committed
50
51
> import Env.Value ( ValueEnv, ValueInfo (..), bindFun, rebindFun
>   , bindGlobalInfo, bindLabel, lookupValue, qualLookupValue )
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
52
53
54
55
56
57
58
59
60
61
62
63

> infixl 5 $-$

> ($-$) :: Doc -> Doc -> Doc
> x $-$ y = x $$ space $$ y

\end{verbatim}
Type checking proceeds as follows. First, the type constructor
environment is initialized by adding all types defined in the current
module. Next, the types of all data constructors and field labels
are entered into the type environment and then a type inference
for all function and value definitions is performed.
64
The type checker returns the resulting type constructor and type environments.
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
65
66
\begin{verbatim}

67
68
69
> typeCheck :: ModuleIdent -> TCEnv -> ValueEnv -> [Decl]
>           -> (TCEnv, ValueEnv, [Message])
> typeCheck m tcEnv tyEnv decls = execTCM check initState
70
>   where
71
72
>   check      = checkTypeSynonyms m tds `andIfOkay` checkDecls
>   checkDecls = do
73
74
75
76
77
78
>     bindTypes tds
>     bindConstrs
>     bindLabels
>     tcDecls vds
>   (tds, vds) = partition isTypeDecl decls
>   initState  = TcState m tcEnv tyEnv idSubst emptySigEnv 0 []
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
79
80
81

\end{verbatim}

82
83
84
The type checker makes use of a state monad in order to maintain the type
environment, the current substitution, and a counter which is used for
generating fresh type variables.
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
85
86
\begin{verbatim}

87
> data TcState = TcState
88
>   { moduleIdent :: ModuleIdent -- read only
89
90
91
92
>   , tyConsEnv   :: TCEnv
>   , valueEnv    :: ValueEnv
>   , typeSubst   :: TypeSubst
>   , sigEnv      :: SigEnv
93
>   , nextId      :: Int         -- automatic counter
94
>   , errors      :: [Message]
95
96
97
98
>   }

> type TCM = S.State TcState

99
100
> getModuleIdent :: TCM ModuleIdent
> getModuleIdent = S.gets moduleIdent
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
101

102
103
104
105
106
107
108
109
> getTyConsEnv :: TCM TCEnv
> getTyConsEnv = S.gets tyConsEnv

> setTyConsEnv :: TCEnv -> TCM ()
> setTyConsEnv tcEnv = S.modify $ \ s -> s { tyConsEnv = tcEnv }

> getValueEnv :: TCM ValueEnv
> getValueEnv = S.gets valueEnv
110
111
112
113
114
115
116

> modifyValueEnv :: (ValueEnv -> ValueEnv) -> TCM ()
> modifyValueEnv f = S.modify $ \ s -> s { valueEnv = f $ valueEnv s }

> getTypeSubst :: TCM TypeSubst
> getTypeSubst = S.gets typeSubst

117
118
119
120
121
122
123
124
125
126
127
128
129
130
> modifyTypeSubst :: (TypeSubst -> TypeSubst) -> TCM ()
> modifyTypeSubst f = S.modify $ \ s -> s { typeSubst = f $ typeSubst s }

> getSigEnv :: TCM SigEnv
> getSigEnv = S.gets sigEnv

> modifySigEnv :: (SigEnv -> SigEnv) -> TCM ()
> modifySigEnv f = S.modify $ \ s -> s { sigEnv = f $ sigEnv s }

> getNextId :: TCM Int
> getNextId = do
>   nid <- S.gets nextId
>   S.modify $ \ s -> s { nextId = succ nid }
>   return nid
131

132
133
134
> report :: Message -> TCM ()
> report err = S.modify $ \ s -> s { errors = err : errors s }

135
136
137
138
139
> andIfOkay :: TCM () -> TCM () -> TCM ()
> andIfOkay pre suf = do
>   errs <- pre >> S.gets errors
>   if null errs then suf else return ()

140
141
142
143
144
145
> execTCM :: TCM a -> TcState -> (TCEnv, ValueEnv, [Message])
> execTCM tcm s = let s' = S.execState tcm s
>                 in  ( tyConsEnv s'
>                     , typeSubst s' `subst` valueEnv s'
>                     , reverse $ errors s'
>                     )
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172

\end{verbatim}
\paragraph{Defining Types}
Before type checking starts, the types defined in the local module
have to be entered into the type constructor environment. All type
synonyms occurring in the definitions are fully expanded and all type
constructors are qualified with the name of the module in which they
are defined. This is possible because Curry does not allow (mutually)
recursive type synonyms. In order to simplify the expansion of type
synonyms, the compiler first performs a dependency analysis on the
type definitions. This also makes it easy to identify (mutually)
recursive synonyms.

Note that \texttt{bindTC} is passed the \emph{final} type constructor
environment in order to handle the expansion of type synonyms. This
does not lead to a termination problem because \texttt{sortTypeDecls}
already has checked that there are no recursive type synonyms.

We have to be careful with existentially quantified type variables for
data constructors. An existentially quantified type variable may
shadow a universally quantified variable from the left hand side of
the type declaration. In order to avoid wrong indices being assigned
to these variables, we replace all shadowed variables in the left hand
side by \texttt{anonId} before passing them to \texttt{expandMonoType}
and \texttt{expandMonoTypes}, respectively.
\begin{verbatim}

173
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
> checkTypeSynonyms :: ModuleIdent -> [Decl] -> TCM ()
> checkTypeSynonyms m = mapM_ (checkTypeDecls m) . scc bound free
>   where
>   bound (DataDecl    _ tc _ _) = [tc]
>   bound (NewtypeDecl _ tc _ _) = [tc]
>   bound (TypeDecl    _ tc _ _) = [tc]
>   bound _                      = []
>   free  (DataDecl     _ _ _ _) = []
>   free  (NewtypeDecl  _ _ _ _) = []
>   free  (TypeDecl    _ _ _ ty) = ft m ty []
>   free _                       = []

> checkTypeDecls :: ModuleIdent -> [Decl] -> TCM ()
> checkTypeDecls _ []                    =
>   internalError "TypeCheck.checkTypeDecls: empty list"
> checkTypeDecls _ [DataDecl    _ _ _ _] = return ()
> checkTypeDecls _ [NewtypeDecl _ _ _ _] = return ()
> checkTypeDecls m [TypeDecl  _ tc _ ty]
>   | tc `elem` ft m ty [] = report $ errRecursiveTypes [tc]
>   | otherwise            = return ()
> checkTypeDecls _ (TypeDecl _ tc _ _ : ds) =
>   report $ errRecursiveTypes $ tc : [tc' | TypeDecl _ tc' _ _ <- ds]
> checkTypeDecls _ _                     =
>   internalError "TypeCheck.checkTypeDecls: no type synonym"

> ft :: ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
> ft m (ConstructorType tc tys) tcs =
>   maybe id (:) (localIdent m tc) (foldr (ft m) tcs tys)
> ft _ (VariableType         _) tcs = tcs
> ft m (TupleType          tys) tcs = foldr (ft m) tcs tys
> ft m (ListType            ty) tcs = ft m ty tcs
> ft m (ArrowType      ty1 ty2) tcs = ft m ty1 $ ft m ty2 $ tcs
> ft m (RecordType      fs rty) tcs =
>   foldr (ft m) (maybe tcs (\ty -> ft m ty tcs) rty) (map snd fs)

> bindTypes :: [Decl] -> TCM ()
> bindTypes ds = do
>   m     <- getModuleIdent
>   tcEnv <- getTyConsEnv
>   let tcEnv' = foldr (bindTC m tcEnv') tcEnv ds
>   setTyConsEnv tcEnv'
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
214
215
216
217

> bindTC :: ModuleIdent -> TCEnv -> Decl -> TCEnv -> TCEnv
> bindTC m tcEnv (DataDecl _ tc tvs cs) =
>   bindTypeInfo DataType m tc tvs (map (Just . mkData) cs)
218
>   where
219
220
221
222
>   mkData (ConstrDecl _ evs     c  tys) = mkData' evs c  tys
>   mkData (ConOpDecl  _ evs ty1 op ty2) = mkData' evs op [ty1, ty2]
>   mkData' evs c tys = DataConstr c (length evs) $
>     expandMonoTypes m tcEnv (cleanTVars tvs evs) tys
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
223
> bindTC m tcEnv (NewtypeDecl _ tc tvs (NewConstrDecl _ evs c ty)) =
Björn Peemöller 's avatar
Björn Peemöller committed
224
>   bindTypeInfo RenamingType m tc tvs (DataConstr c (length evs) [ty'])
225
>   where ty' = expandMonoType' m tcEnv (cleanTVars tvs evs) ty
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
226
> bindTC m tcEnv (TypeDecl _ tc tvs ty) =
227
>   bindTypeInfo AliasType m tc tvs (expandMonoType' m tcEnv tvs ty)
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
228
229
230
231
232
233
234
235
236
237
238
239
240
> bindTC _ _ _ = id

> cleanTVars :: [Ident] -> [Ident] -> [Ident]
> cleanTVars tvs evs = [if tv `elem` evs then anonId else tv | tv <- tvs]

\end{verbatim}
\paragraph{Defining Data Constructors}
In the next step, the types of all data constructors are entered into
the type environment using the information just entered into the type
constructor environment. Thus, we can be sure that all type variables
have been properly renamed and all type synonyms are already expanded.
\begin{verbatim}

241
242
243
244
245
246
247
248
> bindConstrs :: TCM ()
> bindConstrs = do
>   m <- getModuleIdent
>   tcEnv <- getTyConsEnv
>   modifyValueEnv $ bindConstrs' m tcEnv

> bindConstrs' :: ModuleIdent -> TCEnv -> ValueEnv -> ValueEnv
> bindConstrs' m tcEnv tyEnv = foldr (bindData . snd) tyEnv
249
>                            $ localBindings tcEnv
Björn Peemöller 's avatar
Björn Peemöller committed
250
>   where
251
252
253
254
255
256
257
258
259
260
>   bindData (DataType tc n cs) tyEnv' =
>     foldr (bindConstr m n (constrType' tc n)) tyEnv' (catMaybes cs)
>   bindData (RenamingType tc n (DataConstr c n' [ty])) tyEnv' =
>     bindGlobalInfo NewtypeConstructor m c
>                    (ForAllExist n n' (TypeArrow ty (constrType' tc n)))
>                    tyEnv'
>   bindData (RenamingType _ _ (DataConstr _ _ _)) _ =
>     internalError "TypeCheck.bindConstrs: newtype with illegal constructors"
>   bindData (AliasType _ _ _) tyEnv' = tyEnv'
>   bindConstr m' n ty (DataConstr c n' tys) =
261
>     bindGlobalInfo (flip DataConstructor (length tys)) m' c
262
263
>                    (ForAllExist n n' (foldr TypeArrow ty tys))
>   constrType' tc n = TypeConstructor tc $ map TypeVariable [0 .. n - 1]
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
264
265
266
267
268
269
270
271
272
273
274

\end{verbatim}
\paragraph{Defining Field Labels}
Records can only be declared as type aliases. So currently there is
nothing more to do than entering all typed record fields (labels)
which occur in record types on the right-hand-side of type aliases
into the type environment. Since we use the type constructor environment
again, we can be sure that all type variables
have been properly renamed and all type synonyms are already expanded.
\begin{verbatim}

275
276
277
278
279
280
281
282
> bindLabels :: TCM ()
> bindLabels = do
>   tcEnv <- getTyConsEnv
>   modifyValueEnv $ bindLabels' tcEnv

> bindLabels' :: TCEnv -> ValueEnv -> ValueEnv
> bindLabels' tcEnv tyEnv = foldr (bindFieldLabels . snd) tyEnv
>                         $ localBindings tcEnv
283
284
285
286
>   where
>   bindFieldLabels (AliasType r _ (TypeRecord fs _)) env =
>     foldr (bindField r) env fs
>   bindFieldLabels _ env = env
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
287
>
288
289
290
>   bindField r (l, ty) env = case lookupValue l env of
>     [] -> bindLabel l r (polyType ty) env
>     _  -> env
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
291
292
293
294
295
296
297
298
299
300
301
302

\end{verbatim}
\paragraph{Type Signatures}
The type checker collects type signatures in a flat environment. All
anonymous variables occurring in a signature are replaced by fresh
names. However, the type is not expanded so that the signature is
available for use in the error message that is printed when the
inferred type is less general than the signature.
\begin{verbatim}

> type SigEnv = Map.Map Ident TypeExpr

303
304
305
> emptySigEnv :: SigEnv
> emptySigEnv = Map.empty

Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
> bindTypeSig :: Ident -> TypeExpr -> SigEnv -> SigEnv
> bindTypeSig = Map.insert

> bindTypeSigs :: Decl -> SigEnv -> SigEnv
> bindTypeSigs (TypeSig _ vs ty) env =
>   foldr (flip bindTypeSig (nameSigType ty)) env vs
> bindTypeSigs _ env = env

> lookupTypeSig :: Ident -> SigEnv -> Maybe TypeExpr
> lookupTypeSig = Map.lookup

> qualLookupTypeSig :: ModuleIdent -> QualIdent -> SigEnv -> Maybe TypeExpr
> qualLookupTypeSig m f sigs = localIdent m f >>= flip lookupTypeSig sigs

> nameSigType :: TypeExpr -> TypeExpr
321
322
323
324
325
326
327
328
329
330
331
332
> nameSigType ty = fst $ nameType ty $ filter (`notElem` fv ty) identSupply

> nameTypes :: [TypeExpr] -> [Ident] -> ([TypeExpr], [Ident])
> nameTypes []         tvs = ([]        , tvs  )
> nameTypes (ty : tys) tvs = (ty' : tys', tvs'')
>   where (ty' , tvs' ) = nameType ty tvs
>         (tys', tvs'') = nameTypes tys tvs'

> nameType :: TypeExpr -> [Ident] -> (TypeExpr, [Ident])
> nameType (ConstructorType tc tys) tvs = (ConstructorType tc tys', tvs')
>   where (tys', tvs') = nameTypes tys tvs
> nameType (VariableType tv) (tv' : tvs)
333
334
>   | isAnonId tv = (VariableType tv', tvs      )
>   | otherwise   = (VariableType tv , tv' : tvs)
335
336
337
338
339
340
341
> nameType (TupleType tys) tvs = (TupleType tys', tvs')
>   where (tys', tvs') = nameTypes tys tvs
> nameType (ListType ty) tvs = (ListType ty', tvs')
>   where (ty', tvs') = nameType ty tvs
> nameType (ArrowType ty1 ty2) tvs = (ArrowType ty1' ty2', tvs'')
>   where (ty1', tvs' ) = nameType ty1 tvs
>         (ty2', tvs'') = nameType ty2 tvs'
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
342
343
> nameType (RecordType fs rty) tvs =
>   (RecordType (zip ls tys') (listToMaybe rty'), tvs)
344
345
346
347
348
>   where (ls  , tys) = unzip fs
>         (tys', _  ) = nameTypes tys tvs
>         (rty', _  ) = nameTypes (maybeToList rty) tvs
> nameType (VariableType _) [] = internalError
>  "TypeCheck.nameType: empty ident list"
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372

\end{verbatim}
\paragraph{Type Inference}
Before type checking a group of declarations, a dependency analysis is
performed and the declaration group is eventually transformed into
nested declaration groups which are checked separately. Within each
declaration group, first the left hand sides of all declarations are
typed. Next, the right hand sides of the declarations are typed in the
extended type environment. Finally, the types for the left and right
hand sides are unified and the types of all defined functions are
generalized. The generalization step will also check that the type
signatures given by the user match the inferred types.

Argument and result types of foreign functions using the
\texttt{ccall} calling convention are restricted to the basic types
\texttt{Bool}, \texttt{Char}, \texttt{Int}, and \texttt{Float}. In
addition, \texttt{IO}~$t$ is a legitimate result type when $t$ is
either one of the basic types or \texttt{()}.

\ToDo{Extend the set of legitimate types to match the types admitted
  by the Haskell Foreign Function Interface
  Addendum.~\cite{Chakravarty03:FFI}}
\begin{verbatim}

373
374
375
376
377
378
379
> tcDecls :: [Decl] -> TCM ()
> tcDecls ds = do
>   m <- getModuleIdent
>   oldSig <- getSigEnv
>   modifySigEnv $ \ sigs -> foldr bindTypeSigs sigs ods
>   mapM_ tcDeclGroup $ scc bv (qfv m) vds
>   modifySigEnv (const oldSig)
380
381
>   where (vds, ods) = partition isValueDecl ds

382
> tcDeclGroup :: [Decl] -> TCM ()
383
384
385
> tcDeclGroup [ForeignDecl _ _ _ f ty] = tcForeign f ty
> tcDeclGroup [ExternalDecl      _ fs] = mapM_ tcExternal fs
> tcDeclGroup [FreeDecl          _ vs] = mapM_ tcFree     vs
386
> tcDeclGroup ds                       = do
387
>   tyEnv0 <- getValueEnv
388
389
390
>   tysLhs <- mapM tcDeclLhs ds
>   tysRhs <- mapM (tcDeclRhs tyEnv0) ds
>   sequence_ (zipWith3 unifyDecl ds tysLhs tysRhs)
391
>   theta <- getTypeSubst
392
>   mapM_ (genDecl (fvEnv (subst theta tyEnv0)) theta) ds
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
393
> --tcDeclGroup m tcEnv _ [ForeignDecl p cc _ f ty] =
394
> --  tcForeign m tcEnv p cc f ty
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
395

396
> --tcForeign :: ModuleIdent -> TCEnv -> Position -> CallConv -> Ident
397
> --               -> TypeExpr -> TCM ()
398
> --tcForeign m tcEnv p cc f ty =
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
> --  S.modify (bindFun m f (checkForeignType cc (expandPolyType tcEnv ty)))
> --  where checkForeignType CallConvPrimitive ty = ty
> --        checkForeignType CallConvCCall (ForAll n ty) =
> --          ForAll n (checkCCallType ty)
> --        checkCCallType (TypeArrow ty1 ty2)
> --          | isCArgType ty1 = TypeArrow ty1 (checkCCallType ty2)
> --          | otherwise = errorAt p (invalidCType "argument" m ty1)
> --        checkCCallType ty
> --          | isCResultType ty = ty
> --          | otherwise = errorAt p (invalidCType "result" m ty)
> --        isCArgType (TypeConstructor tc []) = tc `elem` basicTypeId
> --        isCArgType _ = False
> --        isCResultType (TypeConstructor tc []) = tc `elem` basicTypeId
> --        isCResultType (TypeConstructor tc [ty]) =
> --          tc == qIOId && (ty == unitType || isCArgType ty)
> --        isCResultType _ = False
> --        basicTypeId = [qBoolId,qCharId,qIntId,qFloatId]

417
418
> tcForeign :: Ident -> TypeExpr -> TCM ()
> tcForeign f ty = do
419
420
421
422
>   m <- getModuleIdent
>   tySc@(ForAll _ ty') <- expandPolyType ty
>   modifyValueEnv $ bindFun m f (arrowArity ty') tySc

423
424
> tcExternal :: Ident -> TCM ()
> tcExternal f = do
425
426
>   sigs <- getSigEnv
>   case lookupTypeSig f sigs of
427
428
>     Nothing -> internalError "TypeCheck.tcExternal"
>     Just ty -> tcForeign f ty
429

430
431
> tcFree :: Ident -> TCM ()
> tcFree v = do
432
433
>   sigs <- getSigEnv
>   m  <- getModuleIdent
434
435
436
437
>   ty <- case lookupTypeSig v sigs of
>     Nothing -> freshTypeVar
>     Just t  -> do
>       ForAll n ty' <- expandPolyType t
438
>       unless (n == 0) $ report $ errPolymorphicFreeVar v
439
440
>       return ty'
>   modifyValueEnv $ bindFun m v (arrowArity ty) $ monoType ty
441
442

> tcDeclLhs :: Decl -> TCM Type
443
> tcDeclLhs (FunctionDecl _ f _) = tcFunDecl f
444
> tcDeclLhs (PatternDecl  p t _) = tcPattern p t
445
446
> tcDeclLhs _ = internalError "TypeCheck.tcDeclLhs: no pattern match"

447
448
449
450
451
452
453
454
455
456
> tcFunDecl :: Ident -> TCM Type
> tcFunDecl v = do
>   sigs <- getSigEnv
>   m <- getModuleIdent
>   ty <- case lookupTypeSig v sigs of
>     Nothing -> freshTypeVar
>     Just t  -> expandPolyType t >>= inst
>   modifyValueEnv $ bindFun m v (arrowArity ty) (monoType ty)
>   return ty

457
458
459
> tcDeclRhs :: ValueEnv -> Decl -> TCM Type
> tcDeclRhs tyEnv0 (FunctionDecl _ f (eq:eqs)) = do
>   tcEquation tyEnv0 eq >>= flip tcEqns eqs
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
460
>   where tcEqns ty [] = return ty
461
462
463
464
465
466
467
468
469
470
471
>         tcEqns ty (eq1@(Equation p _ _):eqs1) = do
>           tcEquation tyEnv0 eq1 >>=
>             unify p "equation" (ppDecl (FunctionDecl p f [eq1])) ty >>
>             tcEqns ty eqs1
> tcDeclRhs tyEnv0 (PatternDecl _ _ rhs) = tcRhs tyEnv0 rhs
> tcDeclRhs _ _ = internalError "TypeCheck.tcDeclRhs: no pattern match"

> unifyDecl :: Decl -> Type -> Type -> TCM ()
> unifyDecl (FunctionDecl p f _) =
>   unify p "function binding" (text "Function:" <+> ppIdent f)
> unifyDecl (PatternDecl  p t _) =
472
>   unify p "pattern binding" (ppPattern 0 t)
473
> unifyDecl _ = internalError "TypeCheck.unifyDecl: no pattern match"
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498

\end{verbatim}
In Curry we cannot generalize the types of let-bound variables because
they can refer to logic variables. Without this monomorphism
restriction unsound code like
\begin{verbatim}
bug = x =:= 1 & x =:= 'a'
  where x :: a
        x = fresh
fresh :: a
fresh = x where x free
\end{verbatim}
could be written. Note that \texttt{fresh} has the polymorphic type
$\forall\alpha.\alpha$. This is correct because \texttt{fresh} is a
function and therefore returns a different variable at each
invocation.

The code in \texttt{genVar} below also verifies that the inferred type
for a variable or function matches the type declared in a type
signature. As the declared type is already used for assigning an initial
type to a variable when it is used, the inferred type can only be more
specific. Therefore, if the inferred type does not match the type
signature the declared type must be too general.
\begin{verbatim}

499
500
501
> genDecl :: Set.Set Int -> TypeSubst -> Decl -> TCM ()
> genDecl lvs theta (FunctionDecl _ f (Equation _ lhs _ : _)) =
>   genVar True lvs theta arity f
502
>   where arity = Just $ length $ snd $ flatLhs lhs
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
> genDecl lvs theta (PatternDecl  _ t   _) =
>   mapM_ (genVar False lvs theta Nothing) (bv t)
> genDecl _ _ _ = internalError "TypeCheck.genDecl: no pattern match"

> genVar :: Bool -> Set.Set Int -> TypeSubst -> Maybe Int -> Ident -> TCM ()
> genVar poly lvs theta ma v = do
>   sigs <- getSigEnv
>   m <- getModuleIdent
>   tyEnv <- getValueEnv
>   let sigma = genType poly $ subst theta $ varType v tyEnv
>       arity  = fromMaybe (varArity v tyEnv) ma
>   case lookupTypeSig v sigs of
>     Nothing    -> modifyValueEnv $ rebindFun m v arity sigma
>     Just sigTy -> do
>       sigma' <- expandPolyType sigTy
518
519
>       unless (eqTyScheme sigma sigma') $ report
>         $ errTypeSigTooGeneral (idPosition v) m what sigTy sigma
520
521
522
523
>       modifyValueEnv $ rebindFun m v arity sigma
>   where
>   what = text (if poly then "Function:" else "Variable:") <+> ppIdent v
>   genType poly' (ForAll n ty)
524
>     | n > 0 = internalError $ "TypeCheck.genVar: " ++ showLine (idPosition v) ++ show v ++ " :: " ++ show ty
525
526
527
528
529
530
>     | poly' = gen lvs ty
>     | otherwise = monoType ty
>   eqTyScheme (ForAll _ t1) (ForAll _ t2) = equTypes t1 t2

> tcEquation :: ValueEnv -> Equation -> TCM Type
> tcEquation tyEnv0 (Equation p lhs rhs) = do
531
>   tys <- mapM (tcPattern p) ts
532
533
534
>   ty <- tcRhs tyEnv0 rhs
>   checkSkolems p (text "Function: " <+> ppIdent f) tyEnv0
>                  (foldr TypeArrow ty tys)
535
536
>   where (f, ts) = flatLhs lhs

537
538
539
540
> tcLiteral :: Literal -> TCM Type
> tcLiteral (Char   _ _) = return charType
> tcLiteral (Int    v _)  = do --return intType
>   m  <- getModuleIdent
541
>   ty <- freshConstrained [intType, floatType]
542
>   modifyValueEnv $ bindFun m v (arrowArity ty) $ monoType ty
543
>   return ty
544
545
546
> tcLiteral (Float  _ _) = return floatType
> tcLiteral (String _ _) = return stringType

547
548
549
550
> tcPattern :: Position -> Pattern -> TCM Type
> tcPattern _ (LiteralPattern    l) = tcLiteral l
> tcPattern _ (NegativePattern _ l) = tcLiteral l
> tcPattern _ (VariablePattern   v) = do
551
>   sigs <- getSigEnv
552
553
>   ty <- case lookupTypeSig v sigs of
>     Nothing -> freshTypeVar
554
>     Just t  -> expandPolyType t >>= inst
555
>   tyEnv <- getValueEnv
556
>   m  <- getModuleIdent
557
558
559
>   maybe (modifyValueEnv (bindFun m v (arrowArity ty) (monoType ty)) >> return ty)
>         (\ (ForAll _ t) -> return t)
>         (sureVarType v tyEnv)
560
> tcPattern p t@(ConstructorPattern c ts) = do
561
>   m     <- getModuleIdent
562
563
>   tyEnv <- getValueEnv
>   ty <- skol $ constrType m c tyEnv
564
>   unifyArgs (ppPattern 0 t) ts ty
565
>   where unifyArgs _   []       ty = return ty
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
566
>         unifyArgs doc (t1:ts1) (TypeArrow ty1 ty2) =
567
568
>           tcPattern p t1 >>=
>           unify p "pattern" (doc $-$ text "Term:" <+> ppPattern 0 t1)
569
>                 ty1 >>
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
570
>           unifyArgs doc ts1 ty2
571
572
>         unifyArgs _ _ _ = internalError "TypeCheck.tcPattern"
> tcPattern p t@(InfixPattern t1 op t2) = do
573
>   m     <- getModuleIdent
574
575
>   tyEnv <- getValueEnv
>   ty <- skol (constrType m op tyEnv)
576
>   unifyArgs (ppPattern 0 t) [t1,t2] ty
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
577
578
>   where unifyArgs _ [] ty = return ty
>         unifyArgs doc (t':ts') (TypeArrow ty1 ty2) =
579
580
>           tcPattern p t' >>=
>           unify p "pattern" (doc $-$ text "Term:" <+> ppPattern 0 t')
581
>                 ty1 >>
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
582
>           unifyArgs doc ts' ty2
583
584
585
>         unifyArgs _ _ _ = internalError "TypeCheck.tcPattern"
> tcPattern p (ParenPattern t) = tcPattern p t
> tcPattern p (TuplePattern _ ts)
586
>  | null ts   = return unitType
587
588
589
>  | otherwise = liftM tupleType $ mapM (tcPattern p) ts
> tcPattern p t@(ListPattern _ ts) =
>   freshTypeVar >>= flip (tcElems (ppPattern 0 t)) ts
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
590
591
>   where tcElems _ ty [] = return (listType ty)
>         tcElems doc ty (t1:ts1) =
592
593
>           tcPattern p t1 >>=
>           unify p "pattern" (doc $-$ text "Term:" <+> ppPattern 0 t1)
594
>                 ty >>
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
595
>           tcElems doc ty ts1
596
597
598
599
> tcPattern p t@(AsPattern v t') = do
>   ty1 <- tcPattern p (VariablePattern v)
>   ty2 <- tcPattern p t'
>   unify p "pattern" (ppPattern 0 t) ty1 ty2
600
>   return ty1
601
602
> tcPattern p (LazyPattern _ t) = tcPattern p t
> tcPattern p t@(FunctionPattern f ts) = do
603
604
605
>   m     <- getModuleIdent
>   tyEnv <- getValueEnv
>   ty <- inst (funType m f tyEnv) --skol (constrType m c tyEnv)
606
>   unifyArgs (ppPattern 0 t) ts ty
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
607
>   where unifyArgs _ [] ty = return ty
608
609
>         unifyArgs doc (t1:ts1) ty@(TypeVariable _) = do
>              (alpha,beta) <- tcArrow p "function pattern" doc ty
610
>	       ty' <- tcPatternFP p t1
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
611
>	       unify p "function pattern"
612
>	             (doc $-$ text "Term:" <+> ppPattern 0 t1)
613
>	             ty' alpha
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
614
>	       unifyArgs doc ts1 beta
615
>         unifyArgs doc (t1:ts1) (TypeArrow ty1 ty2) = do
616
>           tcPatternFP p t1 >>=
617
>             unify p "function pattern"
618
>	          (doc $-$ text "Term:" <+> ppPattern 0 t1)
619
620
>                 ty1 >>
>             unifyArgs doc ts1 ty2
621
622
623
624
>         unifyArgs _ _ ty = internalError $ "TypeCheck.tcPattern: " ++ show ty
> tcPattern p (InfixFuncPattern t1 op t2) =
>   tcPattern p (FunctionPattern op [t1,t2])
> tcPattern p r@(RecordPattern fs rt)
625
>   | isJust rt = do
626
>       ty <- tcPattern p (fromJust rt)
627
>       fts <- mapM (tcFieldPatt tcPattern) fs
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
628
>       alpha <- freshVar id
629
630
>       let rty = TypeRecord fts (Just alpha)
>       unify p "record pattern" (ppPattern 0 r) ty rty
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
631
>       return rty
632
>   | otherwise = do
633
>       fts <- mapM (tcFieldPatt tcPattern) fs
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
634
635
636
637
>       return (TypeRecord fts Nothing)

\end{verbatim}
In contrast to usual patterns, the type checking routine for arguments of
638
function patterns \texttt{tcPatternFP} differs from \texttt{tcPattern}
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
639
640
641
because of possibly multiple occurrences of variables.
\begin{verbatim}

642
643
644
> tcPatternFP :: Position -> Pattern -> TCM Type
> tcPatternFP _ (LiteralPattern    l) = tcLiteral l
> tcPatternFP _ (NegativePattern _ l) = tcLiteral l
645
> tcPatternFP _ (VariablePattern   v) = do
646
647
>   sigs <- getSigEnv
>   m <- getModuleIdent
648
649
650
>   ty <- case lookupTypeSig v sigs of
>     Nothing -> freshTypeVar
>     Just t  -> expandPolyType t >>= inst
651
>   tyEnv <- getValueEnv
652
653
654
>   maybe (modifyValueEnv (bindFun m v (arrowArity ty) (monoType ty)) >> return ty)
>         (\ (ForAll _ t) -> return t)
>         (sureVarType v tyEnv)
655
> tcPatternFP p t@(ConstructorPattern c ts) = do
656
657
658
>   m <- getModuleIdent
>   tyEnv <- getValueEnv
>   ty <- skol (constrType m c tyEnv)
659
>   unifyArgs (ppPattern 0 t) ts ty
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
660
>   where unifyArgs _ [] ty = return ty
661
>         unifyArgs doc (t1:ts1) (TypeArrow ty1 ty2) = do
662
663
>           tcPatternFP p t1 >>=
>             unify p "pattern" (doc $-$ text "Term:" <+> ppPattern 0 t1)
664
665
>                 ty1 >>
>             unifyArgs doc ts1 ty2
666
667
>         unifyArgs _ _ _ = internalError "TypeCheck.tcPatternFP"
> tcPatternFP p t@(InfixPattern t1 op t2) = do
668
669
670
>   m <- getModuleIdent
>   tyEnv <- getValueEnv
>   ty <- skol (constrType m op tyEnv)
671
>   unifyArgs (ppPattern 0 t) [t1,t2] ty
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
672
>   where unifyArgs _ [] ty = return ty
673
>         unifyArgs doc (t':ts') (TypeArrow ty1 ty2) = do
674
675
>           tcPatternFP p t' >>=
>             unify p "pattern" (doc $-$ text "Term:" <+> ppPattern 0 t')
676
677
>                   ty1 >>
>             unifyArgs doc ts' ty2
678
679
680
>         unifyArgs _ _ _ = internalError "TypeCheck.tcPatternFP"
> tcPatternFP p (ParenPattern t) = tcPatternFP p t
> tcPatternFP p (TuplePattern _ ts)
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
681
>  | null ts = return unitType
682
683
684
>  | otherwise = liftM tupleType $ mapM (tcPatternFP p) ts
> tcPatternFP p t@(ListPattern _ ts) =
>   freshTypeVar >>= flip (tcElems (ppPattern 0 t)) ts
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
685
686
>   where tcElems _ ty [] = return (listType ty)
>         tcElems doc ty (t1:ts1) =
687
688
>           tcPatternFP p t1 >>=
>           unify p "pattern" (doc $-$ text "Term:" <+> ppPattern 0 t1)
689
>                 ty >>
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
690
>           tcElems doc ty ts1
691
> tcPatternFP p t@(AsPattern v t') =
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
692
>   do
693
694
695
>     ty1 <- tcPatternFP p (VariablePattern v)
>     ty2 <- tcPatternFP p t'
>     unify p "pattern" (ppPattern 0 t) ty1 ty2
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
696
>     return ty1
697
698
> tcPatternFP p (LazyPattern _ t) = tcPatternFP p t
> tcPatternFP p t@(FunctionPattern f ts) = do
699
>     m <- getModuleIdent
700
>     tyEnv <- getValueEnv
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
701
>     ty <- inst (funType m f tyEnv) --skol (constrType m c tyEnv)
702
>     unifyArgs (ppPattern 0 t) ts ty
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
703
>   where unifyArgs _ [] ty = return ty
704
705
>         unifyArgs doc (t1:ts1) ty@(TypeVariable _) = do
>              (alpha,beta) <- tcArrow p "function pattern" doc ty
706
>	       ty' <- tcPatternFP p t1
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
707
>	       unify p "function pattern"
708
>	             (doc $-$ text "Term:" <+> ppPattern 0 t1)
709
>	             ty' alpha
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
710
711
>	       unifyArgs doc ts1 beta
>         unifyArgs doc (t1:ts1) (TypeArrow ty1 ty2) =
712
713
>           tcPatternFP p t1 >>=
>           unify p "pattern" (doc $-$ text "Term:" <+> ppPattern 0 t1)
714
>                 ty1 >>
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
715
>           unifyArgs doc ts1 ty2
716
717
718
719
>         unifyArgs _ _ _ = internalError "TypeCheck.tcPatternFP"
> tcPatternFP p (InfixFuncPattern t1 op t2) =
>   tcPatternFP p (FunctionPattern op [t1,t2])
> tcPatternFP p r@(RecordPattern fs rt)
720
>   | isJust rt = do
721
>       ty <- tcPatternFP p (fromJust rt)
722
>       fts <- mapM (tcFieldPatt tcPatternFP) fs
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
723
>       alpha <- freshVar id
724
725
>       let rty = TypeRecord fts (Just alpha)
>       unify p "record pattern" (ppPattern 0 r) ty rty
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
726
>       return rty
727
>   | otherwise = do
728
>       fts <- mapM (tcFieldPatt tcPatternFP) fs
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
729
730
>       return (TypeRecord fts Nothing)

731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
> tcFieldPatt :: (Position -> Pattern -> TCM Type) -> Field Pattern
>             -> TCM (Ident, Type)
> tcFieldPatt tcPatt f@(Field _ l t) = do
>   m <- getModuleIdent
>   tyEnv <- getValueEnv
>   let p = idPosition l
>   lty <- maybe (freshTypeVar >>= \lty' ->
>                 modifyValueEnv
>                 (bindLabel l (qualifyWith m (mkIdent "#Rec")) (polyType lty'))
>                 >> return lty')
>                inst
>                (sureLabelType l tyEnv)
>   ty <- tcPatt p t
>   unify p "record" (text "Field:" <+> ppFieldPatt f) lty ty
>   return (l, ty)
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
746

747
748
749
750
751
752
753
754
755
756
757
> tcRhs ::ValueEnv -> Rhs -> TCM Type
> tcRhs tyEnv0 (SimpleRhs p e ds) = do
>   tcDecls ds
>   ty <- tcExpr p e
>   checkSkolems p (text "Expression:" <+> ppExpr 0 e) tyEnv0 ty
> tcRhs tyEnv0 (GuardedRhs es ds) = do
>   tcDecls ds
>   tcCondExprs tyEnv0 es

> tcCondExprs :: ValueEnv -> [CondExpr] -> TCM Type
> tcCondExprs tyEnv0 es = do
758
>   gty <- if length es > 1 then return boolType
759
>                           else freshConstrained [successType, boolType]
760
>   ty <- freshTypeVar
761
762
763
764
765
766
767
>   mapM_ (tcCondExpr gty ty) es
>   return ty
>   where
>   tcCondExpr gty ty (CondExpr p g e) = do
>     tcExpr p g >>= unify p "guard" (ppExpr 0 g) gty
>     tcExpr p e >>= checkSkolems p (text "Expression:" <+> ppExpr 0 e) tyEnv0
>                >>= unify p "guarded expression" (ppExpr 0 e) ty
768
769
770
771

> tcExpr :: Position -> Expression -> TCM Type
> tcExpr _ (Literal     l) = tcLiteral l
> tcExpr _ (Variable    v)
772
773
774
775
776
777
778
779
780
781
782
>   | isAnonId v' = do -- anonymous free variable
>     m <- getModuleIdent
>     ty <- freshTypeVar
>     modifyValueEnv $ bindFun m v' (arrowArity ty) $ monoType ty
>     return ty
>   | otherwise   = do
>     sigs <- getSigEnv
>     m <- getModuleIdent
>     case qualLookupTypeSig m v sigs of
>       Just ty -> expandPolyType ty >>= inst
>       Nothing -> getValueEnv >>= inst . funType m v
783
>   where v' = unqualify v
784
> tcExpr _ (Constructor c) = do
785
786
>   m <- getModuleIdent
>   getValueEnv >>= instExist . constrType m c
787
788
> tcExpr p (Typed   e sig) = do
>   m <- getModuleIdent
789
>   tyEnv0 <- getValueEnv
790
791
792
>   ty <- tcExpr p e
>   sigma' <- expandPolyType sig'
>   inst sigma' >>= flip (unify p "explicitly typed expression" (ppExpr 0 e)) ty
793
>   theta <- getTypeSubst
794
>   let sigma  = gen (fvEnv (subst theta tyEnv0)) (subst theta ty)
795
796
>   unless (sigma == sigma') $ report $
>     errTypeSigTooGeneral p m (text "Expression:" <+> ppExpr 0 e) sig' sigma
797
>   return ty
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
798
>   where sig' = nameSigType sig
799
> tcExpr p (Paren    e) = tcExpr p e
800
> tcExpr p (Tuple _ es)
801
>   | null es   = return unitType
802
803
>   | otherwise = liftM tupleType $ mapM (tcExpr p) es
> tcExpr p e@(List _ es) = freshTypeVar >>= tcElems (ppExpr 0 e) es
804
>   where tcElems _   []       ty = return (listType ty)
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
805
>         tcElems doc (e1:es1) ty =
806
>           tcExpr p e1 >>=
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
807
>           unify p "expression" (doc $-$ text "Term:" <+> ppExpr 0 e1)
808
>                 ty >>
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
809
>           tcElems doc es1 ty
810
> tcExpr p (ListCompr _ e qs) = do
811
>     tyEnv0 <- getValueEnv
812
813
814
815
>     mapM_ (tcQual p) qs
>     ty <- tcExpr p e
>     checkSkolems p (text "Expression:" <+> ppExpr 0 e) tyEnv0 (listType ty)
> tcExpr p e@(EnumFrom e1) = do
816
817
818
819
>   ty1 <- tcExpr p e1
>   unify p "arithmetic sequence"
>         (ppExpr 0 e $-$ text "Term:" <+> ppExpr 0 e1) intType ty1
>   return (listType intType)
820
> tcExpr p e@(EnumFromThen e1 e2) = do
821
822
823
824
825
826
827
>   ty1 <- tcExpr p e1
>   ty2 <- tcExpr p e2
>   unify p "arithmetic sequence"
>         (ppExpr 0 e $-$ text "Term:" <+> ppExpr 0 e1) intType ty1
>   unify p "arithmetic sequence"
>         (ppExpr 0 e $-$ text "Term:" <+> ppExpr 0 e2) intType ty2
>   return (listType intType)
828
> tcExpr p e@(EnumFromTo e1 e2) = do
829
830
831
832
833
834
835
>   ty1 <- tcExpr p e1
>   ty2 <- tcExpr p e2
>   unify p "arithmetic sequence"
>         (ppExpr 0 e $-$ text "Term:" <+> ppExpr 0 e1) intType ty1
>   unify p "arithmetic sequence"
>         (ppExpr 0 e $-$ text "Term:" <+> ppExpr 0 e2) intType ty2
>   return (listType intType)
836
> tcExpr p e@(EnumFromThenTo e1 e2 e3) = do
837
838
839
840
841
842
843
844
845
846
>   ty1 <- tcExpr p e1
>   ty2 <- tcExpr p e2
>   ty3 <- tcExpr p e3
>   unify p "arithmetic sequence"
>         (ppExpr 0 e $-$ text "Term:" <+> ppExpr 0 e1) intType ty1
>   unify p "arithmetic sequence"
>         (ppExpr 0 e $-$ text "Term:" <+> ppExpr 0 e2) intType ty2
>   unify p "arithmetic sequence"
>         (ppExpr 0 e $-$ text "Term:" <+> ppExpr 0 e3) intType ty3
>   return (listType intType)
847
> tcExpr p e@(UnaryMinus op e1) = do
848
849
850
851
852
>   opTy <- opType op
>   ty1 <- tcExpr p e1
>   unify p "unary negation" (ppExpr 0 e $-$ text "Term:" <+> ppExpr 0 e1)
>         opTy ty1
>   return ty1
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
853
>   where opType op'
854
>           | op' == minusId  = freshConstrained [intType,floatType]
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
855
>           | op' == fminusId = return floatType
856
>           | otherwise = internalError $ "TypeCheck.tcExpr unary " ++ idName op'
857
> tcExpr p e@(Apply e1 e2) = do
858
859
860
861
862
863
864
865
>   ty1 <- tcExpr p e1
>   ty2 <- tcExpr p e2
>   (alpha,beta) <-
>     tcArrow p "application" (ppExpr 0 e $-$ text "Term:" <+> ppExpr 0 e1)
>            ty1
>   unify p "application" (ppExpr 0 e $-$ text "Term:" <+> ppExpr 0 e2)
>         alpha ty2
>   return beta
866
> tcExpr p e@(InfixApply e1 op e2) = do
867
868
869
870
871
872
873
874
875
876
877
>   opTy <- tcExpr p (infixOp op)
>   ty1  <- tcExpr p e1
>   ty2  <- tcExpr p e2
>   (alpha,beta,gamma) <-
>     tcBinary p "infix application"
>              (ppExpr 0 e $-$ text "Operator:" <+> ppOp op) opTy
>   unify p "infix application" (ppExpr 0 e $-$ text "Term:" <+> ppExpr 0 e1)
>         alpha ty1
>   unify p "infix application" (ppExpr 0 e $-$ text "Term:" <+> ppExpr 0 e2)
>         beta ty2
>   return gamma
878
> tcExpr p e@(LeftSection e1 op) = do
879
880
881
882
883
884
885
886
>   opTy <- tcExpr p (infixOp op)
>   ty1  <- tcExpr p e1
>   (alpha,beta) <-
>     tcArrow p "left section" (ppExpr 0 e $-$ text "Operator:" <+> ppOp op)
>             opTy
>   unify p "left section" (ppExpr 0 e $-$ text "Term:" <+> ppExpr 0 e1)
>         alpha ty1
>   return beta
887
> tcExpr p e@(RightSection op e1) = do
888
889
890
891
892
893
894
895
>   opTy <- tcExpr p (infixOp op)
>   ty1  <- tcExpr p e1
>   (alpha,beta,gamma) <-
>     tcBinary p "right section"
>              (ppExpr 0 e $-$ text "Operator:" <+> ppOp op) opTy
>   unify p "right section" (ppExpr 0 e $-$ text "Term:" <+> ppExpr 0 e1)
>         beta ty1
>   return (TypeArrow alpha gamma)
896
> tcExpr p expr@(Lambda _ ts e) = do
897
898
899
900
901
>   tyEnv0 <- getValueEnv
>   tys <- mapM (tcPattern p) ts
>   ty <- tcExpr p e
>   checkSkolems p (text "Expression:" <+> ppExpr 0 expr) tyEnv0
>                (foldr TypeArrow ty tys)
902
> tcExpr p (Let ds e) = do
903
904
905
906
>   tyEnv0 <- getValueEnv
>   tcDecls ds
>   ty <- tcExpr p e
>   checkSkolems p (text "Expression:" <+> ppExpr 0 e) tyEnv0 ty
907
> tcExpr p (Do sts e) = do
908
909
910
911
912
913
>   tyEnv0 <- getValueEnv
>   mapM_ (tcStmt p) sts
>   alpha <- freshTypeVar
>   ty <- tcExpr p e
>   unify p "statement" (ppExpr 0 e) (ioType alpha) ty
>   checkSkolems p (text "Expression:" <+> ppExpr 0 e) tyEnv0 ty
914
> tcExpr p e@(IfThenElse _ e1 e2 e3) = do
915
916
917
918
919
920
921
922
>   ty1 <- tcExpr p e1
>   unify p "expression" (ppExpr 0 e $-$ text "Term:" <+> ppExpr 0 e1)
>         boolType ty1
>   ty2 <- tcExpr p e2
>   ty3 <- tcExpr p e3
>   unify p "expression" (ppExpr 0 e $-$ text "Term:" <+> ppExpr 0 e3)
>         ty2 ty3
>   return ty3
923
> tcExpr p (Case _ _ e alts) = do
924
925
926
927
>   tyEnv0 <- getValueEnv
>   ty <- tcExpr p e
>   alpha <- freshTypeVar
>   tcAlts tyEnv0 ty alpha alts
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
928
929
930
931
>   where tcAlts _      _   ty [] = return ty
>         tcAlts tyEnv0 ty1 ty2 (alt1:alts1) =
>           tcAlt (ppAlt alt1) tyEnv0 ty1 ty2 alt1 >> tcAlts tyEnv0 ty1 ty2 alts1
>         tcAlt doc tyEnv0 ty1 ty2 (Alt p1 t rhs) =
932
933
>           tcPattern p1 t >>=
>           unify p1 "case pattern" (doc $-$ text "Term:" <+> ppPattern 0 t)
934
935
936
>                 ty1 >>
>           tcRhs tyEnv0 rhs >>=
>           unify p1 "case branch" doc ty2
937
> tcExpr _ (RecordConstr fs) = do
938
939
>   fts <- mapM tcFieldExpr fs
>   return (TypeRecord fts Nothing)
940
> tcExpr p r@(RecordSelection e l) = do
941
942
943
944
945
946
>   lty <- instLabel l
>   ety <- tcExpr p e
>   alpha <- freshVar id
>   let rty = TypeRecord [(l, lty)] (Just alpha)
>   unify p "record selection" (ppExpr 0 r) ety rty
>   return lty
947
> tcExpr p r@(RecordUpdate fs e) = do
948
949
950
951
952
953
>   ty    <- tcExpr p e
>   fts   <- mapM tcFieldExpr fs
>   alpha <- freshVar id
>   let rty = TypeRecord fts (Just alpha)
>   unify p "record update" (ppExpr 0 r) ty rty
>   return ty
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
954

955
> tcQual :: Position -> Statement -> TCM ()
956
> tcQual p (StmtExpr     _ e) =
957
958
>   tcExpr p e >>= unify p "guard" (ppExpr 0 e) boolType
> tcQual p q@(StmtBind _ t e) = do
959
>   ty1 <- tcPattern p t
960
961
962
>   ty2 <- tcExpr p e
>   unify p "generator" (ppStmt q $-$ text "Term:" <+> ppExpr 0 e)
>         (listType ty1) ty2
963
> tcQual _ (StmtDecl      ds) = tcDecls ds
964
965
966
967
968
969
970

> tcStmt ::Position -> Statement -> TCM ()
> tcStmt p (StmtExpr _ e) = do
>   alpha <- freshTypeVar
>   ty    <- tcExpr p e
>   unify p "statement" (ppExpr 0 e) (ioType alpha) ty
> tcStmt p st@(StmtBind _ t e) = do
971
>   ty1 <- tcPattern p t
972
973
974
975
>   ty2 <- tcExpr p e
>   unify p "statement" (ppStmt st $-$ text "Term:" <+> ppExpr 0 e) (ioType ty1) ty2
> tcStmt _ (StmtDecl ds) = tcDecls ds

976
> tcFieldExpr :: Field Expression -> TCM (Ident, Type)
977
978
979
980
981
> tcFieldExpr f@(Field p l e) = do
>   lty <- instLabel l
>   ety <- tcExpr p e
>   unify p "record" (text "Field:" <+> ppFieldExpr f) lty ety
>   return (l, ety)
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
982
983
984
985
986
987
988
989
990
991

\end{verbatim}
The function \texttt{tcArrow} checks that its argument can be used as
an arrow type $\alpha\rightarrow\beta$ and returns the pair
$(\alpha,\beta)$. Similarly, the function \texttt{tcBinary} checks
that its argument can be used as an arrow type
$\alpha\rightarrow\beta\rightarrow\gamma$ and returns the triple
$(\alpha,\beta,\gamma)$.
\begin{verbatim}

992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
> tcArrow :: Position -> String -> Doc -> Type -> TCM (Type, Type)
> tcArrow p what doc ty = do
>   theta <- getTypeSubst
>   unaryArrow (subst theta ty)
>   where
>   unaryArrow (TypeArrow ty1 ty2) = return (ty1, ty2)
>   unaryArrow (TypeVariable   tv) = do
>     alpha <- freshTypeVar
>     beta  <- freshTypeVar
>     modifyTypeSubst $ bindVar tv $ TypeArrow alpha beta
>     return (alpha, beta)
>   unaryArrow ty'                 = do
>     m <- getModuleIdent
>     report $ errNonFunctionType p what doc m ty'
>     liftM2 (,) freshTypeVar freshTypeVar

> tcBinary :: Position -> String -> Doc -> Type -> TCM (Type, Type, Type)
> tcBinary p what doc ty = tcArrow p what doc ty >>= uncurry binaryArrow
>   where
>   binaryArrow ty1 (TypeArrow ty2 ty3) = return (ty1, ty2, ty3)
>   binaryArrow ty1 (TypeVariable   tv) = do
>     beta  <- freshTypeVar
>     gamma <- freshTypeVar
>     modifyTypeSubst $ bindVar tv $ TypeArrow beta gamma
>     return (ty1, beta, gamma)
>   binaryArrow ty1 ty2 = do
>     m <- getModuleIdent
>     report $ errNonBinaryOp p what doc m (TypeArrow ty1 ty2)
>     liftM3 (,,) (return ty1) freshTypeVar freshTypeVar
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
1021
1022
1023
1024
1025
1026
1027

\end{verbatim}
\paragraph{Unification}
The unification uses Robinson's algorithm (cf., e.g., Chap.~9
of~\cite{PeytonJones87:Book}).
\begin{verbatim}

1028
1029
1030
1031
1032
1033
1034
1035
1036
> unify :: Position -> String -> Doc -> Type -> Type -> TCM ()
> unify p what doc ty1 ty2 = do
>   theta <- getTypeSubst
>   let ty1' = subst theta ty1
>   let ty2' = subst theta ty2
>   m <- getModuleIdent
>   case unifyTypes m ty1' ty2' of
>     Left reason -> report $ errTypeMismatch p what doc m ty1' ty2' reason
>     Right sigma -> modifyTypeSubst (compose sigma)
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
1037
1038
1039

> unifyTypes :: ModuleIdent -> Type -> Type -> Either Doc TypeSubst
> unifyTypes _ (TypeVariable tv1) (TypeVariable tv2)
1040
1041
>   | tv1 == tv2            = Right idSubst
>   | otherwise             = Right (singleSubst tv1 (TypeVariable tv2))
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
1042
> unifyTypes m (TypeVariable tv) ty
1043
1044
>   | tv `elem` typeVars ty = Left  (errRecursiveType m tv ty)
>   | otherwise             = Right (singleSubst tv ty)
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
1045
> unifyTypes m ty (TypeVariable tv)
1046
1047
>   | tv `elem` typeVars ty = Left  (errRecursiveType m tv ty)
>   | otherwise             = Right (singleSubst tv ty)
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
1048
> unifyTypes _ (TypeConstrained tys1 tv1) (TypeConstrained tys2 tv2)
1049
1050
>   | tv1  == tv2           = Right idSubst
>   | tys1 == tys2          = Right (singleSubst tv1 (TypeConstrained tys2 tv2))
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
1051
> unifyTypes m (TypeConstrained tys tv) ty =
1052
>   foldr (choose . unifyTypes m ty) (Left (errIncompatibleTypes m ty (head tys)))
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
1053
1054
1055
1056
>         tys
>   where choose (Left _) theta' = theta'
>         choose (Right theta) _ = Right (bindSubst tv ty theta)
> unifyTypes m ty (TypeConstrained tys tv) =
1057
>   foldr (choose . unifyTypes m ty) (Left (errIncompatibleTypes m ty (head tys)))
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
1058
1059
1060
1061
1062
1063
>         tys
>   where choose (Left _) theta' = theta'
>         choose (Right theta) _ = Right (bindSubst tv ty theta)
> unifyTypes m (TypeConstructor tc1 tys1) (TypeConstructor tc2 tys2)
>   | tc1 == tc2 = unifyTypeLists m tys1 tys2
> unifyTypes m (TypeArrow ty11 ty12) (TypeArrow ty21 ty22) =
1064
>   unifyTypeLists m [ty11, ty12] [ty21, ty22]
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
> unifyTypes _ (TypeSkolem k1) (TypeSkolem k2)
>   | k1 == k2 = Right idSubst
> unifyTypes m (TypeRecord fs1 Nothing) tr2@(TypeRecord fs2 Nothing)
>   | length fs1 == length fs2 = unifyTypedLabels m fs1 tr2
> unifyTypes m tr1@(TypeRecord _ Nothing) (TypeRecord fs2 (Just a2)) =
>   either Left
>          (\res -> either Left
>	                   (Right . compose res)
>                          (unifyTypes m (TypeVariable a2) tr1))
>          (unifyTypedLabels m fs2 tr1)
> unifyTypes m tr1@(TypeRecord _ (Just _)) tr2@(TypeRecord _ Nothing) =
>   unifyTypes m tr2 tr1
> unifyTypes m (TypeRecord fs1 (Just a1)) tr2@(TypeRecord fs2 (Just a2)) =
>   let (fs1', rs1, rs2) = splitFields fs1 fs2
>   in  either
>         Left
>         (\res ->
>           either
>             Left
>	      (\res' -> Right (compose res res'))
>	      (unifyTypeLists m [TypeVariable a1,
>			         TypeRecord (fs1 ++ rs2) Nothing]
>	                        [TypeVariable a2,
>			         TypeRecord (fs2 ++ rs1) Nothing]))
>         (unifyTypedLabels m fs1' tr2)
>   where
>   splitFields fsx fsy = split' [] [] fsy fsx
>   split' fs1' rs1 rs2 [] = (fs1',rs1,rs2)
>   split' fs1' rs1 rs2 ((l,ty):ltys) =
>     maybe (split' fs1' ((l,ty):rs1) rs2 ltys)
>           (const (split' ((l,ty):fs1') rs1 (remove l rs2) ltys))
>           (lookup l rs2)
1097
> unifyTypes m ty1 ty2 = Left (errIncompatibleTypes m ty1 ty2)
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
1098
1099

> unifyTypeLists :: ModuleIdent -> [Type] -> [Type] -> Either Doc TypeSubst
1100
1101
1102
1103
1104
> unifyTypeLists _ []          _             = Right idSubst
> unifyTypeLists _ _           []            = Right idSubst
> unifyTypeLists m (ty1 : tys1) (ty2 : tys2) =
>   either Left unifyTypesTheta (unifyTypeLists m tys1 tys2)
>   where unifyTypesTheta theta =
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
1105
>           either Left (Right . flip compose theta)
1106
>                  (unifyTypes m (subst theta ty1) (subst theta ty2))
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
1107

1108
> unifyTypedLabels :: ModuleIdent -> [(Ident,Type)] -> Type -> Either Doc TypeSubst
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
1109
1110
1111
1112
> unifyTypedLabels _ [] (TypeRecord _ _) = Right idSubst
> unifyTypedLabels m ((l,ty):fs1) tr@(TypeRecord fs2 _) =
>   either Left
>          (\r ->
1113
>            maybe (Left (errMissingLabel m l tr))
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
1114
>                  (\ty' ->
1115
>		     either (const (Left (errIncompatibleLabelTypes m l ty ty')))
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
1116
1117
1118
1119
>	                    (Right . flip compose r)
>	                    (unifyTypes m ty ty'))
>                  (lookup l fs2))
>          (unifyTypedLabels m fs1 tr)
1120
> unifyTypedLabels _ _ _ = internalError "TypeCheck.unifyTypedLabels"
Bjoern Peemoeller's avatar
Bjoern Peemoeller committed
1121
1122
1123
1124
1125
1126

\end{verbatim}
For each declaration group, the type checker has to ensure that no
skolem type escapes its scope.
\begin{verbatim}