KindCheck.hs 28.8 KB
Newer Older
1
2
{- |
    Module      :  $Header$
Finn Teegen's avatar
Finn Teegen committed
3
    Description :  Checks type kinds
4
    Copyright   :  (c) 2016 - 2017 Finn Teegen
5
    License     :  BSD-3-clause
6
7
8
9
10

    Maintainer  :  bjp@informatik.uni-kiel.de
    Stability   :  experimental
    Portability :  portable

Finn Teegen's avatar
Finn Teegen committed
11
12
13
14
   After the type syntax has been checked und nullary type constructors and
   type variables have been disambiguated, the compiler infers kinds for all
   type constructors and type classes defined in the current module and
   performs kind checking on all type definitions and type signatures.
15
-}
16
{-# LANGUAGE CPP #-}
17
18
module Checks.KindCheck (kindCheck) where

Finn Teegen's avatar
Finn Teegen committed
19
20
21
22
#if __GLASGOW_HASKELL__ >= 804
import Prelude hiding ((<>))
#endif

23
#if __GLASGOW_HASKELL__ < 710
24
import           Control.Applicative      ((<$>), (<*>))
25
#endif
Finn Teegen's avatar
Finn Teegen committed
26
import           Control.Monad            (when, foldM)
Finn Teegen's avatar
Finn Teegen committed
27
import           Control.Monad.Fix        (mfix)
28
import qualified Control.Monad.State as S (State, runState, gets, modify)
Finn Teegen's avatar
Finn Teegen committed
29
import           Data.List                (partition, nub)
30
31
32
33
34

import Curry.Base.Ident
import Curry.Base.Position
import Curry.Base.Pretty
import Curry.Syntax
Finn Teegen's avatar
Finn Teegen committed
35
import Curry.Syntax.Pretty
36

Finn Teegen's avatar
Finn Teegen committed
37
38
39
40
import Base.CurryKinds
import Base.Expr
import Base.Kinds
import Base.KindSubst
41
import Base.Messages (Message, posMessage, internalError)
Finn Teegen's avatar
Finn Teegen committed
42
import Base.SCC
43
import Base.TopEnv
Finn Teegen's avatar
Finn Teegen committed
44
import Base.Types
Finn Teegen's avatar
Finn Teegen committed
45
import Base.TypeExpansion
Finn Teegen's avatar
Finn Teegen committed
46

Finn Teegen's avatar
Finn Teegen committed
47
import Env.Class
Finn Teegen's avatar
Finn Teegen committed
48
49
50
51
52
53
54
55
import Env.TypeConstructor

-- In order to infer kinds for type constructors and type classes, the
-- compiler sorts the module's type and class declarations into minimal
-- recursive binding groups and then applies kind inference to each
-- declaration group. Besides inferring kinds for the type constructors
-- and type classes of a group, the compiler also checks that there are
-- no mutually recursive type synonym definitions and that the super class
Finn Teegen's avatar
Finn Teegen committed
56
57
-- hierarchy is acyclic. The former allows entering fully expanded type
-- synonyms into the type constructor environment.
Finn Teegen's avatar
Finn Teegen committed
58

Finn Teegen's avatar
Finn Teegen committed
59
60
kindCheck :: TCEnv -> ClassEnv -> Module a -> ((TCEnv, ClassEnv), [Message])
kindCheck tcEnv clsEnv (Module _ m _ _ ds) = runKCM check initState
Finn Teegen's avatar
Finn Teegen committed
61
62
  where
    check = do
63
      checkNonRecursiveTypes tds &&> checkAcyclicSuperClasses cds
Finn Teegen's avatar
Finn Teegen committed
64
65
66
      errs <- S.gets errors
      if null errs
         then checkDecls
Finn Teegen's avatar
Finn Teegen committed
67
         else return (tcEnv, clsEnv)
Finn Teegen's avatar
Finn Teegen committed
68
    checkDecls = do
Finn Teegen's avatar
Finn Teegen committed
69
      (tcEnv', clsEnv') <- kcDecls tcEnv clsEnv tcds
Finn Teegen's avatar
Finn Teegen committed
70
      mapM_ (kcDecl tcEnv') ods
Finn Teegen's avatar
Finn Teegen committed
71
      return (tcEnv', clsEnv')
Finn Teegen's avatar
Finn Teegen committed
72
73
74
75
    tds = filter isTypeDecl tcds
    cds = filter isClassDecl tcds
    (tcds, ods) = partition isTypeOrClassDecl ds
    initState  = KCState m idSubst 0 []
Björn Peemöller 's avatar
Björn Peemöller committed
76
77
78
79

-- Kind Check Monad
type KCM = S.State KCState

80
-- |Internal state of the Kind Check
81
data KCState = KCState
Finn Teegen's avatar
Finn Teegen committed
82
83
84
  { moduleIdent :: ModuleIdent -- read only
  , kindSubst   :: KindSubst
  , nextId      :: Int         -- automatic counter
85
86
87
  , errors      :: [Message]
  }

Finn Teegen's avatar
Finn Teegen committed
88
89
90
91
92
(&&>) :: KCM () -> KCM () -> KCM ()
pre &&> suf = do
  errs <- pre >> S.gets errors
  if null errs then suf else return ()

93
94
95
96
97
98
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

Finn Teegen's avatar
Finn Teegen committed
99
100
101
102
103
104
105
106
107
108
109
getKindSubst :: KCM KindSubst
getKindSubst = S.gets kindSubst

modifyKindSubst :: (KindSubst -> KindSubst) -> KCM ()
modifyKindSubst f = S.modify $ \s -> s { kindSubst = f $ kindSubst s }

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

report :: Message -> KCM ()
Finn Teegen's avatar
Finn Teegen committed
112
113
114
115
116
117
118
119
report err = S.modify (\s -> s { errors = err : errors s })

ok :: KCM ()
ok = return ()

-- Minimal recursive declaration groups are computed using the sets of bound
-- and free type constructor and type class identifiers of the declarations.

Finn Teegen's avatar
Finn Teegen committed
120
bt :: Decl a -> [Ident]
Finn Teegen's avatar
Finn Teegen committed
121
bt (DataDecl     _ tc _ _ _) = [tc]
122
bt (ExternalDataDecl _ tc _) = [tc]
Finn Teegen's avatar
Finn Teegen committed
123
bt (NewtypeDecl  _ tc _ _ _) = [tc]
Finn Teegen's avatar
Finn Teegen committed
124
125
126
127
bt (TypeDecl       _ tc _ _) = [tc]
bt (ClassDecl   _ _ cls _ _) = [cls]
bt _                         = []

Finn Teegen's avatar
Finn Teegen committed
128
ft :: ModuleIdent -> Decl a -> [Ident]
Finn Teegen's avatar
Finn Teegen committed
129
130
131
132
133
134
135
136
137
138
139
ft m d = fts m d []

class HasType a where
  fts :: ModuleIdent -> a -> [Ident] -> [Ident]

instance HasType a => HasType [a] where
  fts m = flip $ foldr $ fts m

instance HasType a => HasType (Maybe a) where
  fts m = maybe id $ fts m

Finn Teegen's avatar
Finn Teegen committed
140
instance HasType (Decl a) where
Finn Teegen's avatar
Finn Teegen committed
141
  fts _ (InfixDecl             _ _ _ _) = id
Finn Teegen's avatar
Finn Teegen committed
142
  fts m (DataDecl        _ _ _ cs clss) = fts m cs . fts m clss
143
  fts _ (ExternalDataDecl        _ _ _) = id
Finn Teegen's avatar
Finn Teegen committed
144
  fts m (NewtypeDecl     _ _ _ nc clss) = fts m nc . fts m clss
Finn Teegen's avatar
Finn Teegen committed
145
146
  fts m (TypeDecl             _ _ _ ty) = fts m ty
  fts m (TypeSig                _ _ ty) = fts m ty
Finn Teegen's avatar
Finn Teegen committed
147
  fts m (FunctionDecl        _ _ _ eqs) = fts m eqs
Finn Teegen's avatar
Finn Teegen committed
148
149
150
  fts _ (ExternalDecl              _ _) = id
  fts m (PatternDecl           _ _ rhs) = fts m rhs
  fts _ (FreeDecl                  _ _) = id
Finn Teegen's avatar
Finn Teegen committed
151
  fts m (DefaultDecl             _ tys) = fts m tys
Finn Teegen's avatar
Finn Teegen committed
152
153
154
  fts m (ClassDecl         _ cx _ _ ds) = fts m cx . fts m ds
  fts m (InstanceDecl _ cx cls inst ds) =
    fts m cx . fts m cls . fts m inst . fts m ds
Finn Teegen's avatar
Finn Teegen committed
155
156

instance HasType ConstrDecl where
Finn Teegen's avatar
Finn Teegen committed
157
158
159
  fts m (ConstrDecl     _ _ cx _ tys) = fts m cx . fts m tys
  fts m (ConOpDecl  _ _ cx ty1 _ ty2) = fts m cx . fts m ty1 . fts m ty2
  fts m (RecordDecl      _ _ cx _ fs) = fts m cx . fts m fs
Finn Teegen's avatar
Finn Teegen committed
160
161
162
163
164

instance HasType FieldDecl where
  fts m (FieldDecl _ _ ty) = fts m ty

instance HasType NewConstrDecl where
Finn Teegen's avatar
Finn Teegen committed
165
166
  fts m (NewConstrDecl      _ _ ty) = fts m ty
  fts m (NewRecordDecl _ _ (_, ty)) = fts m ty
Finn Teegen's avatar
Finn Teegen committed
167

Finn Teegen's avatar
Finn Teegen committed
168
169
instance HasType Constraint where
  fts m (Constraint qcls _) = fts m qcls
Finn Teegen's avatar
Finn Teegen committed
170

171
172
173
instance HasType QualTypeExpr where
  fts m (QualTypeExpr cx ty) = fts m cx . fts m ty

Finn Teegen's avatar
Finn Teegen committed
174
175
176
177
178
179
instance HasType TypeExpr where
  fts m (ConstructorType      tc) = fts m tc
  fts m (ApplyType       ty1 ty2) = fts m ty1 . fts m ty2
  fts _ (VariableType          _) = id
  fts m (TupleType           tys) = (tupleId (length tys) :) . fts m tys
  fts m (ListType             ty) = (listId :) . fts m ty
Finn Teegen's avatar
Finn Teegen committed
180
  fts m (ArrowType       ty1 ty2) = (arrowId :) . fts m ty1 . fts m ty2
Finn Teegen's avatar
Finn Teegen committed
181
  fts m (ParenType            ty) = fts m ty
182
  fts m (ForallType         _ ty) = fts m ty
Finn Teegen's avatar
Finn Teegen committed
183

Finn Teegen's avatar
Finn Teegen committed
184
instance HasType (Equation a) where
Finn Teegen's avatar
Finn Teegen committed
185
186
  fts m (Equation _ _ rhs) = fts m rhs

Finn Teegen's avatar
Finn Teegen committed
187
instance HasType (Rhs a) where
Finn Teegen's avatar
Finn Teegen committed
188
189
190
  fts m (SimpleRhs  _ e ds) = fts m e . fts m ds
  fts m (GuardedRhs  es ds) = fts m es . fts m ds

Finn Teegen's avatar
Finn Teegen committed
191
instance HasType (CondExpr a) where
Finn Teegen's avatar
Finn Teegen committed
192
193
  fts m (CondExpr _ g e) = fts m g . fts m e

Finn Teegen's avatar
Finn Teegen committed
194
195
196
197
instance HasType (Expression a) where
  fts _ (Literal             _ _) = id
  fts _ (Variable            _ _) = id
  fts _ (Constructor         _ _) = id
Finn Teegen's avatar
Finn Teegen committed
198
199
  fts m (Paren                 e) = fts m e
  fts m (Typed              e ty) = fts m e . fts m ty
Finn Teegen's avatar
Finn Teegen committed
200
  fts m (Record           _ _ fs) = fts m fs
Finn Teegen's avatar
Finn Teegen committed
201
  fts m (RecordUpdate       e fs) = fts m e . fts m fs
Finn Teegen's avatar
Finn Teegen committed
202
203
204
  fts m (Tuple                es) = fts m es
  fts m (List               _ es) = fts m es
  fts m (ListCompr        e stms) = fts m e . fts m stms
Finn Teegen's avatar
Finn Teegen committed
205
206
207
208
  fts m (EnumFrom              e) = fts m e
  fts m (EnumFromThen      e1 e2) = fts m e1 . fts m e2
  fts m (EnumFromTo        e1 e2) = fts m e1 . fts m e2
  fts m (EnumFromThenTo e1 e2 e3) = fts m e1 . fts m e2 . fts m e3
Finn Teegen's avatar
Finn Teegen committed
209
  fts m (UnaryMinus            e) = fts m e
Finn Teegen's avatar
Finn Teegen committed
210
211
212
213
  fts m (Apply             e1 e2) = fts m e1 . fts m e2
  fts m (InfixApply      e1 _ e2) = fts m e1 . fts m e2
  fts m (LeftSection         e _) = fts m e
  fts m (RightSection        _ e) = fts m e
Finn Teegen's avatar
Finn Teegen committed
214
  fts m (Lambda              _ e) = fts m e
Finn Teegen's avatar
Finn Teegen committed
215
216
  fts m (Let                ds e) = fts m ds . fts m e
  fts m (Do               stms e) = fts m stms . fts m e
Finn Teegen's avatar
Finn Teegen committed
217
218
  fts m (IfThenElse     e1 e2 e3) = fts m e1 . fts m e2 . fts m e3
  fts m (Case             _ e as) = fts m e . fts m as
Finn Teegen's avatar
Finn Teegen committed
219

Finn Teegen's avatar
Finn Teegen committed
220
instance HasType (Statement a) where
Finn Teegen's avatar
Finn Teegen committed
221
222
223
  fts m (StmtExpr   e) = fts m e
  fts m (StmtDecl  ds) = fts m ds
  fts m (StmtBind _ e) = fts m e
Finn Teegen's avatar
Finn Teegen committed
224

Finn Teegen's avatar
Finn Teegen committed
225
instance HasType (Alt a) where
Finn Teegen's avatar
Finn Teegen committed
226
227
228
229
230
231
232
233
  fts m (Alt _ _ rhs) = fts m rhs

instance HasType a => HasType (Field a) where
  fts m (Field _ _ x) = fts m x

instance HasType QualIdent where
  fts m qident = maybe id (:) (localIdent m qident)

Finn Teegen's avatar
Finn Teegen committed
234
235
236
237
238
239
-- When types are entered into the type constructor environment, all type
-- synonyms occuring in the definitions are fully expanded (except for
-- record types) and all type constructors and type classes 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 or
-- newtypes, which is checked in the function 'checkNonRecursiveTypes' below.
Finn Teegen's avatar
Finn Teegen committed
240

Finn Teegen's avatar
Finn Teegen committed
241
ft' :: ModuleIdent -> Decl a -> [Ident]
Finn Teegen's avatar
Finn Teegen committed
242
ft' _ (DataDecl     _ _ _ _ _) = []
243
ft' _ (ExternalDataDecl _ _ _) = []
Finn Teegen's avatar
Finn Teegen committed
244
245
246
ft' m (NewtypeDecl _ _ _ nc _) = fts m nc []
ft' m (TypeDecl      _ _ _ ty) = fts m ty []
ft' _ _                        = []
247

Finn Teegen's avatar
Finn Teegen committed
248
checkNonRecursiveTypes :: [Decl a] -> KCM ()
249
checkNonRecursiveTypes ds = do
Finn Teegen's avatar
Finn Teegen committed
250
  m <- getModuleIdent
251
  mapM_ checkTypeAndNewtypeDecls $ scc bt (ft' m) ds
Finn Teegen's avatar
Finn Teegen committed
252

Finn Teegen's avatar
Finn Teegen committed
253
checkTypeAndNewtypeDecls :: [Decl a] -> KCM ()
254
255
checkTypeAndNewtypeDecls [] =
  internalError "Checks.KindCheck.checkTypeAndNewtypeDecls: empty list"
Finn Teegen's avatar
Finn Teegen committed
256
checkTypeAndNewtypeDecls [DataDecl _ _ _ _ _] = ok
257
checkTypeAndNewtypeDecls [ExternalDataDecl _ _ _] = ok
258
259
checkTypeAndNewtypeDecls [d] | isTypeOrNewtypeDecl d = do
  m <- getModuleIdent
Finn Teegen's avatar
Finn Teegen committed
260
  let tc = typeConstructor d
261
262
263
  when (tc `elem` ft m d) $ report $ errRecursiveTypes [tc]
checkTypeAndNewtypeDecls (d:ds) | isTypeOrNewtypeDecl d =
  report $ errRecursiveTypes $
Finn Teegen's avatar
Finn Teegen committed
264
    typeConstructor d : [typeConstructor d' | d' <- ds, isTypeOrNewtypeDecl d']
265
266
267
268
269
checkTypeAndNewtypeDecls _ = internalError
  "Checks.KindCheck.checkTypeAndNewtypeDecls: no type or newtype declarations"

-- The function 'checkAcyclicSuperClasses' checks that the super class
-- hierarchy is acyclic.
Finn Teegen's avatar
Finn Teegen committed
270

Finn Teegen's avatar
Finn Teegen committed
271
272
fc :: ModuleIdent -> Context -> [Ident]
fc m = foldr fc' []
Finn Teegen's avatar
Finn Teegen committed
273
  where
Finn Teegen's avatar
Finn Teegen committed
274
    fc' (Constraint qcls _) = maybe id (:) (localIdent m qcls)
Finn Teegen's avatar
Finn Teegen committed
275

Finn Teegen's avatar
Finn Teegen committed
276
checkAcyclicSuperClasses :: [Decl a] -> KCM ()
277
checkAcyclicSuperClasses ds = do
278
  m <- getModuleIdent
Finn Teegen's avatar
Finn Teegen committed
279
  mapM_ checkClassDecl $ scc bt (\(ClassDecl _ cx _ _ _) -> fc m cx) ds
280

Finn Teegen's avatar
Finn Teegen committed
281
checkClassDecl :: [Decl a] -> KCM ()
Finn Teegen's avatar
Finn Teegen committed
282
checkClassDecl [] =
283
  internalError "Checks.KindCheck.checkClassDecl: empty list"
Finn Teegen's avatar
Finn Teegen committed
284
285
286
287
288
289
checkClassDecl [ClassDecl _ cx cls _ _] = do
  m <- getModuleIdent
  when (cls `elem` fc m cx) $ report $ errRecursiveClasses [cls]
checkClassDecl (ClassDecl _ _ cls _ _ : ds) =
  report $ errRecursiveClasses $ cls : [cls' | ClassDecl _ _ cls' _ _ <- ds]
checkClassDecl _ =
290
  internalError "Checks.KindCheck.checkClassDecl: no class declaration"
Finn Teegen's avatar
Finn Teegen committed
291
292
293
294
295
296
297

-- For each declaration group, the kind checker first enters new
-- assumptions into the type constructor environment. For a type
-- constructor with arity n, we enter kind k_1 -> ... -> k_n -> k,
-- where k_i are fresh kind variables and k is * for data and newtype
-- type constructors and a fresh kind variable for type synonym type
-- constructors. For a type class we enter kind k, where k is a fresh
Finn Teegen's avatar
Finn Teegen committed
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
-- kind variable. We also add a type class to the class environment.
-- Next, the kind checker checks the declarations of the group within
-- the extended environment, and finally the kind checker instantiates
-- all remaining free kind variables to *.

-- As noted above, type synonyms are fully expanded while types are
-- entered into the type constructor environment. Furthermore, we uses
-- original names for classes and super classes in the class environment.
-- Unfortunately, both of this requires either sorting type declarations
-- properly or using the final type constructor environment for the expansion
-- and original names. We have chosen the latter option here, which requires
-- recursive monadic bindings which are supported using the 'mfix' method
-- from the 'MonadFix' type class.

bindKind :: ModuleIdent -> TCEnv -> ClassEnv -> TCEnv -> Decl a -> KCM TCEnv
Finn Teegen's avatar
Finn Teegen committed
313
bindKind m tcEnv' clsEnv tcEnv (DataDecl _ tc tvs cs _) = do
Finn Teegen's avatar
Finn Teegen committed
314
315
  bindTypeConstructor DataType tc tvs (Just KindStar) (map mkData cs) tcEnv
  where
Finn Teegen's avatar
Finn Teegen committed
316
317
318
    mkData (ConstrDecl _ evs cx     c  tys) = mkData' evs cx c  tys
    mkData (ConOpDecl  _ evs cx ty1 op ty2) = mkData' evs cx op [ty1, ty2]
    mkData (RecordDecl _ evs cx     c   fs) =
Finn Teegen's avatar
Finn Teegen committed
319
      let (labels, tys) = unzip [(l, ty) | FieldDecl _ ls ty <- fs, l <- ls]
Finn Teegen's avatar
Finn Teegen committed
320
321
322
323
324
325
326
327
328
329
330
331
      in  mkRec evs cx c labels tys
    mkData' evs cx c tys = DataConstr c (length evs) ps tys'
      where qtc = qualifyWith m tc
            tvs' = tvs ++ evs
            PredType ps ty = expandConstrType m tcEnv' clsEnv qtc tvs' cx tys
            tys' = arrowArgs ty
    mkRec evs cx c ls tys =
      RecordConstr c (length evs) ps ls tys'
      where qtc = qualifyWith m tc
            tvs' = tvs ++ evs
            PredType ps ty = expandConstrType m tcEnv' clsEnv qtc tvs' cx tys
            tys' = arrowArgs ty
Finn Teegen's avatar
Finn Teegen committed
332
bindKind _ _     _       tcEnv (ExternalDataDecl _ tc tvs) = do
333
  bindTypeConstructor DataType tc tvs (Just KindStar) [] tcEnv
Finn Teegen's avatar
Finn Teegen committed
334
bindKind m tcEnv' _      tcEnv (NewtypeDecl _ tc tvs nc _) =
Finn Teegen's avatar
Finn Teegen committed
335
336
  bindTypeConstructor RenamingType tc tvs (Just KindStar) (mkData nc) tcEnv
  where
Finn Teegen's avatar
Finn Teegen committed
337
338
339
340
341
342
    mkData (NewConstrDecl _ c      ty) = DataConstr c 0 emptyPredSet [ty']
      where ty'  = expandMonoType m tcEnv' tvs ty
    mkData (NewRecordDecl _ c (l, ty)) = RecordConstr c 0 emptyPredSet [l] [ty']
      where ty'  = expandMonoType m tcEnv' tvs ty
bindKind m tcEnv' _      tcEnv (TypeDecl _ tc tvs ty) =
  bindTypeConstructor aliasType tc tvs Nothing ty' tcEnv
Finn Teegen's avatar
Finn Teegen committed
343
344
  where
    aliasType tc' k = AliasType tc' k $ length tvs
Finn Teegen's avatar
Finn Teegen committed
345
346
347
    ty' = expandMonoType m tcEnv' tvs ty
bindKind m tcEnv' clsEnv tcEnv (ClassDecl _ _ cls tv ds) =
  bindTypeClass cls (concatMap mkMethods ds) tcEnv
Finn Teegen's avatar
Finn Teegen committed
348
  where
Finn Teegen's avatar
Finn Teegen committed
349
350
351
352
    mkMethods (TypeSig _ fs qty) = map (mkMethod qty) fs
    mkMethods _                  = []
    mkMethod qty f = ClassMethod f (findArity f ds) $
                       expandMethodType m tcEnv' clsEnv (qualify cls) tv qty
353
354
355
    findArity _ []                                    = Nothing
    findArity f (FunctionDecl _ _ f' eqs:_) | f == f' =
      Just $ eqnArity $ head eqs
Finn Teegen's avatar
Finn Teegen committed
356
357
    findArity f (_:ds')                               = findArity f ds'
bindKind _ _      _      tcEnv _                          = return tcEnv
Finn Teegen's avatar
Finn Teegen committed
358
359
360
361
362
363
364
365
366
367
368

bindTypeConstructor :: (QualIdent -> Kind -> a -> TypeInfo) -> Ident
                    -> [Ident] -> Maybe Kind -> a -> TCEnv -> KCM TCEnv
bindTypeConstructor f tc tvs k x tcEnv = do
  m <- getModuleIdent
  k' <- maybe freshKindVar return k
  ks <- mapM (const freshKindVar) tvs
  let qtc = qualifyWith m tc
      ti = f qtc (foldr KindArrow k' ks) x
  return $ bindTypeInfo m tc ti tcEnv

Finn Teegen's avatar
Finn Teegen committed
369
370
bindTypeClass :: Ident -> [ClassMethod] -> TCEnv -> KCM TCEnv
bindTypeClass cls ms tcEnv = do
Finn Teegen's avatar
Finn Teegen committed
371
372
373
  m <- getModuleIdent
  k <- freshKindVar
  let qcls = qualifyWith m cls
Finn Teegen's avatar
Finn Teegen committed
374
      ti = TypeClass qcls k ms
Finn Teegen's avatar
Finn Teegen committed
375
376
377
378
379
380
381
382
383
384
385
386
  return $ bindTypeInfo m cls ti tcEnv

bindFreshKind :: TCEnv -> Ident -> KCM TCEnv
bindFreshKind tcEnv tv = do
  k <- freshKindVar
  return $ bindTypeVar tv k tcEnv

bindTypeVars :: Ident -> [Ident] -> TCEnv -> KCM (Kind, TCEnv)
bindTypeVars tc tvs tcEnv = do
  m <- getModuleIdent
  return $ foldl (\(KindArrow k1 k2, tcEnv') tv ->
                   (k2, bindTypeVar tv k1 tcEnv'))
Finn Teegen's avatar
Finn Teegen committed
387
                 (tcKind m (qualifyWith m tc) tcEnv, tcEnv)
Finn Teegen's avatar
Finn Teegen committed
388
389
390
391
392
                 tvs

bindTypeVar :: Ident -> Kind -> TCEnv -> TCEnv
bindTypeVar ident k = bindTopEnv ident (TypeVar k)

Finn Teegen's avatar
Finn Teegen committed
393
394
395
396
bindClass :: ModuleIdent -> TCEnv -> ClassEnv -> Decl a -> ClassEnv
bindClass m tcEnv clsEnv (ClassDecl _  cx cls _ ds) =
  bindClassInfo qcls (sclss, ms) clsEnv
  where qcls = qualifyWith m cls
397
398
        ms = map (\f -> (f, f `elem` fs)) $ concatMap methods ds
        fs = concatMap impls ds
Finn Teegen's avatar
Finn Teegen committed
399
400
401
        sclss = nub $ map (\(Constraint cls' _) -> getOrigName m cls' tcEnv) cx
bindClass _ _ clsEnv _ = clsEnv

Finn Teegen's avatar
Finn Teegen committed
402
403
404
405
406
407
408
instantiateWithDefaultKind :: TypeInfo -> TypeInfo
instantiateWithDefaultKind (DataType tc k cs) =
  DataType tc (defaultKind k) cs
instantiateWithDefaultKind (RenamingType tc k nc) =
  RenamingType tc (defaultKind k) nc
instantiateWithDefaultKind (AliasType tc k n ty) =
  AliasType tc (defaultKind k) n ty
Finn Teegen's avatar
Finn Teegen committed
409
410
instantiateWithDefaultKind (TypeClass cls k ms) =
  TypeClass cls (defaultKind k) ms
Finn Teegen's avatar
Finn Teegen committed
411
412
413
instantiateWithDefaultKind (TypeVar _) =
  internalError "Checks.KindCheck.instantiateWithDefaultKind: type variable"

Finn Teegen's avatar
Finn Teegen committed
414
415
kcDecls :: TCEnv -> ClassEnv -> [Decl a] -> KCM (TCEnv, ClassEnv)
kcDecls tcEnv clsEnv ds = do
Finn Teegen's avatar
Finn Teegen committed
416
  m <- getModuleIdent
Finn Teegen's avatar
Finn Teegen committed
417
  foldM (uncurry kcDeclGroup) (tcEnv, clsEnv) $ scc bt (ft m) ds
Finn Teegen's avatar
Finn Teegen committed
418

Finn Teegen's avatar
Finn Teegen committed
419
420
421
422
423
424
kcDeclGroup :: TCEnv -> ClassEnv -> [Decl a] -> KCM (TCEnv, ClassEnv)
kcDeclGroup tcEnv clsEnv ds = do
  m <- getModuleIdent
  (tcEnv', clsEnv') <- mfix (\ ~(tcEnv', clsEnv') ->
    flip (,) (foldl (bindClass m tcEnv') clsEnv ds) <$>
      foldM (bindKind m tcEnv' clsEnv') tcEnv ds)
Finn Teegen's avatar
Finn Teegen committed
425
426
  mapM_ (kcDecl tcEnv') ds
  theta <- getKindSubst
Finn Teegen's avatar
Finn Teegen committed
427
  return (fmap (instantiateWithDefaultKind . subst theta) tcEnv', clsEnv')
Finn Teegen's avatar
Finn Teegen committed
428
429
430
431
432
433
434
435
436

-- After adding new assumptions to the environment, kind inference is
-- applied to all declarations. The type environment may be extended
-- temporarily with bindings for type variables occurring in the left
-- hand side of type declarations and free type variables of type
-- signatures. While the kinds of the former are determined already by
-- the kinds of their type constructors and type classes, respectively,
-- fresh kind variables are added for the latter.

Finn Teegen's avatar
Finn Teegen committed
437
kcDecl :: TCEnv -> Decl a -> KCM ()
Finn Teegen's avatar
Finn Teegen committed
438
kcDecl _     (InfixDecl _ _ _ _) = ok
Finn Teegen's avatar
Finn Teegen committed
439
kcDecl tcEnv (DataDecl _ tc tvs cs _) = do
Finn Teegen's avatar
Finn Teegen committed
440
441
  (_, tcEnv') <- bindTypeVars tc tvs tcEnv
  mapM_ (kcConstrDecl tcEnv') cs
442
kcDecl _     (ExternalDataDecl _ _ _) = ok
Finn Teegen's avatar
Finn Teegen committed
443
kcDecl tcEnv (NewtypeDecl _ tc tvs nc _) = do
Finn Teegen's avatar
Finn Teegen committed
444
445
446
447
448
  (_, tcEnv') <- bindTypeVars tc tvs tcEnv
  kcNewConstrDecl tcEnv' nc
kcDecl tcEnv t@(TypeDecl p tc tvs ty) = do
  (k, tcEnv') <- bindTypeVars tc tvs tcEnv
  kcType tcEnv' p "type declaration" (ppDecl t) k ty
449
kcDecl tcEnv (TypeSig p _ qty) = kcTypeSig tcEnv p qty
Finn Teegen's avatar
Finn Teegen committed
450
451
kcDecl tcEnv (FunctionDecl _ _ _ eqs) = mapM_ (kcEquation tcEnv) eqs
kcDecl _     (ExternalDecl _ _) = ok
Finn Teegen's avatar
Finn Teegen committed
452
453
kcDecl tcEnv (PatternDecl _ _ rhs) = kcRhs tcEnv rhs
kcDecl _     (FreeDecl _ _) = ok
Finn Teegen's avatar
Finn Teegen committed
454
455
456
kcDecl tcEnv (DefaultDecl p tys) = do
  tcEnv' <- foldM bindFreshKind tcEnv $ nub $ fv tys
  mapM_ (kcValueType tcEnv' p "default declaration" empty) tys
Finn Teegen's avatar
Finn Teegen committed
457
kcDecl tcEnv (ClassDecl p cx cls tv ds) = do
Finn Teegen's avatar
Finn Teegen committed
458
  m <- getModuleIdent
Finn Teegen's avatar
Finn Teegen committed
459
  let tcEnv' = bindTypeVar tv (clsKind m (qualifyWith m cls) tcEnv) tcEnv
Finn Teegen's avatar
Finn Teegen committed
460
461
462
  kcContext tcEnv' p cx
  mapM_ (kcDecl tcEnv') ds
kcDecl tcEnv (InstanceDecl p cx qcls inst ds) = do
Finn Teegen's avatar
Finn Teegen committed
463
  m <- getModuleIdent
Finn Teegen's avatar
Finn Teegen committed
464
465
  tcEnv' <- foldM bindFreshKind tcEnv $ fv inst
  kcContext tcEnv' p cx
Finn Teegen's avatar
Finn Teegen committed
466
  kcType tcEnv' p what doc (clsKind m qcls tcEnv) inst
Finn Teegen's avatar
Finn Teegen committed
467
468
469
470
  mapM_ (kcDecl tcEnv') ds
    where
      what = "instance declaration"
      doc = ppDecl (InstanceDecl p cx qcls inst [])
Finn Teegen's avatar
Finn Teegen committed
471
472

kcConstrDecl :: TCEnv -> ConstrDecl -> KCM ()
Finn Teegen's avatar
Finn Teegen committed
473
kcConstrDecl tcEnv d@(ConstrDecl p evs cx _ tys) = do
Finn Teegen's avatar
Finn Teegen committed
474
  tcEnv' <- foldM bindFreshKind tcEnv evs
Finn Teegen's avatar
Finn Teegen committed
475
  kcContext tcEnv' p cx
Finn Teegen's avatar
Finn Teegen committed
476
477
478
479
  mapM_ (kcValueType tcEnv' p what doc) tys
    where
      what = "data constructor declaration"
      doc = ppConstr d
Finn Teegen's avatar
Finn Teegen committed
480
kcConstrDecl tcEnv d@(ConOpDecl p evs cx ty1 _ ty2) = do
Finn Teegen's avatar
Finn Teegen committed
481
  tcEnv' <- foldM bindFreshKind tcEnv evs
Finn Teegen's avatar
Finn Teegen committed
482
  kcContext tcEnv' p cx
Finn Teegen's avatar
Finn Teegen committed
483
484
485
486
487
  kcValueType tcEnv' p what doc ty1
  kcValueType tcEnv' p what doc ty2
    where
      what = "data constructor declaration"
      doc = ppConstr d
Finn Teegen's avatar
Finn Teegen committed
488
kcConstrDecl tcEnv (RecordDecl p evs cx _ fs) = do
Finn Teegen's avatar
Finn Teegen committed
489
  tcEnv' <- foldM bindFreshKind tcEnv evs
Finn Teegen's avatar
Finn Teegen committed
490
  kcContext tcEnv' p cx
Finn Teegen's avatar
Finn Teegen committed
491
492
493
494
495
496
497
  mapM_ (kcFieldDecl tcEnv') fs

kcFieldDecl :: TCEnv -> FieldDecl -> KCM ()
kcFieldDecl tcEnv d@(FieldDecl p _ ty) =
  kcValueType tcEnv p "field declaration" (ppFieldDecl d) ty

kcNewConstrDecl :: TCEnv -> NewConstrDecl -> KCM ()
Finn Teegen's avatar
Finn Teegen committed
498
499
500
501
kcNewConstrDecl tcEnv d@(NewConstrDecl p _ ty) =
  kcValueType tcEnv p "newtype constructor declaration" (ppNewConstr d) ty
kcNewConstrDecl tcEnv (NewRecordDecl p _ (l, ty)) =
  kcFieldDecl tcEnv (FieldDecl p [l] ty)
Finn Teegen's avatar
Finn Teegen committed
502

Finn Teegen's avatar
Finn Teegen committed
503
kcEquation :: TCEnv -> Equation a -> KCM ()
Finn Teegen's avatar
Finn Teegen committed
504
505
kcEquation tcEnv (Equation _ _ rhs) = kcRhs tcEnv rhs

Finn Teegen's avatar
Finn Teegen committed
506
kcRhs :: TCEnv -> Rhs a -> KCM ()
Finn Teegen's avatar
Finn Teegen committed
507
508
509
510
511
512
513
kcRhs tcEnv (SimpleRhs p e ds) = do
  kcExpr tcEnv p e
  mapM_ (kcDecl tcEnv) ds
kcRhs tcEnv (GuardedRhs es ds) = do
  mapM_ (kcCondExpr tcEnv) es
  mapM_ (kcDecl tcEnv) ds

Finn Teegen's avatar
Finn Teegen committed
514
kcCondExpr :: TCEnv -> CondExpr a -> KCM ()
Finn Teegen's avatar
Finn Teegen committed
515
516
kcCondExpr tcEnv (CondExpr p g e) = kcExpr tcEnv p g >> kcExpr tcEnv p e

Finn Teegen's avatar
Finn Teegen committed
517
518
519
520
kcExpr :: TCEnv -> Position -> Expression a -> KCM ()
kcExpr _     _ (Literal _ _) = ok
kcExpr _     _ (Variable _ _) = ok
kcExpr _     _ (Constructor _ _) = ok
Finn Teegen's avatar
Finn Teegen committed
521
kcExpr tcEnv p (Paren e) = kcExpr tcEnv p e
522
kcExpr tcEnv p (Typed e qty) = do
Finn Teegen's avatar
Finn Teegen committed
523
  kcExpr tcEnv p e
524
  kcTypeSig tcEnv p qty
Finn Teegen's avatar
Finn Teegen committed
525
kcExpr tcEnv p (Record _ _ fs) = mapM_ (kcField tcEnv p) fs
Finn Teegen's avatar
Finn Teegen committed
526
527
528
kcExpr tcEnv p (RecordUpdate e fs) = do
  kcExpr tcEnv p e
  mapM_ (kcField tcEnv p) fs
Finn Teegen's avatar
Finn Teegen committed
529
530
531
kcExpr tcEnv p (Tuple es) = mapM_ (kcExpr tcEnv p) es
kcExpr tcEnv p (List _ es) = mapM_ (kcExpr tcEnv p) es
kcExpr tcEnv p (ListCompr e stms) = do
Finn Teegen's avatar
Finn Teegen committed
532
533
534
535
536
537
538
539
540
541
542
543
544
  kcExpr tcEnv p e
  mapM_ (kcStmt tcEnv p) stms
kcExpr tcEnv p (EnumFrom e) = kcExpr tcEnv p e
kcExpr tcEnv p (EnumFromThen e1 e2) = do
  kcExpr tcEnv p e1
  kcExpr tcEnv p e2
kcExpr tcEnv p (EnumFromTo e1 e2) = do
  kcExpr tcEnv p e1
  kcExpr tcEnv p e2
kcExpr tcEnv p (EnumFromThenTo e1 e2 e3) = do
  kcExpr tcEnv p e1
  kcExpr tcEnv p e2
  kcExpr tcEnv p e3
Finn Teegen's avatar
Finn Teegen committed
545
kcExpr tcEnv p (UnaryMinus e) = kcExpr tcEnv p e
Finn Teegen's avatar
Finn Teegen committed
546
547
548
549
550
551
552
553
kcExpr tcEnv p (Apply e1 e2) = do
  kcExpr tcEnv p e1
  kcExpr tcEnv p e2
kcExpr tcEnv p (InfixApply e1 _ e2) = do
  kcExpr tcEnv p e1
  kcExpr tcEnv p e2
kcExpr tcEnv p (LeftSection e _) = kcExpr tcEnv p e
kcExpr tcEnv p (RightSection _ e) = kcExpr tcEnv p e
Finn Teegen's avatar
Finn Teegen committed
554
kcExpr tcEnv p (Lambda _ e) = kcExpr tcEnv p e
Finn Teegen's avatar
Finn Teegen committed
555
556
557
558
559
560
kcExpr tcEnv p (Let ds e) = do
  mapM_ (kcDecl tcEnv) ds
  kcExpr tcEnv p e
kcExpr tcEnv p (Do stms e) = do
  mapM_ (kcStmt tcEnv p) stms
  kcExpr tcEnv p e
Finn Teegen's avatar
Finn Teegen committed
561
kcExpr tcEnv p (IfThenElse e1 e2 e3) = do
Finn Teegen's avatar
Finn Teegen committed
562
563
564
  kcExpr tcEnv p e1
  kcExpr tcEnv p e2
  kcExpr tcEnv p e3
Finn Teegen's avatar
Finn Teegen committed
565
kcExpr tcEnv p (Case _ e alts) = do
Finn Teegen's avatar
Finn Teegen committed
566
567
568
  kcExpr tcEnv p e
  mapM_ (kcAlt tcEnv) alts

Finn Teegen's avatar
Finn Teegen committed
569
kcStmt :: TCEnv -> Position -> Statement a -> KCM ()
Finn Teegen's avatar
Finn Teegen committed
570
kcStmt tcEnv p (StmtExpr e) = kcExpr tcEnv p e
Finn Teegen's avatar
Finn Teegen committed
571
kcStmt tcEnv _ (StmtDecl ds) = mapM_ (kcDecl tcEnv) ds
Finn Teegen's avatar
Finn Teegen committed
572
kcStmt tcEnv p (StmtBind _ e) = kcExpr tcEnv p e
Finn Teegen's avatar
Finn Teegen committed
573

Finn Teegen's avatar
Finn Teegen committed
574
kcAlt :: TCEnv -> Alt a -> KCM ()
Finn Teegen's avatar
Finn Teegen committed
575
576
kcAlt tcEnv (Alt _ _ rhs) = kcRhs tcEnv rhs

Finn Teegen's avatar
Finn Teegen committed
577
kcField :: TCEnv -> Position -> Field (Expression a) -> KCM ()
Finn Teegen's avatar
Finn Teegen committed
578
579
kcField tcEnv p (Field _ _ e) = kcExpr tcEnv p e

Finn Teegen's avatar
Finn Teegen committed
580
581
kcContext :: TCEnv -> Position -> Context -> KCM ()
kcContext tcEnv p = mapM_ (kcConstraint tcEnv p)
Finn Teegen's avatar
Finn Teegen committed
582

Finn Teegen's avatar
Finn Teegen committed
583
kcConstraint :: TCEnv -> Position -> Constraint -> KCM ()
Finn Teegen's avatar
Finn Teegen committed
584
585
586
kcConstraint tcEnv p sc@(Constraint qcls ty) = do
  m <- getModuleIdent
  kcType tcEnv p "class constraint" doc (clsKind m qcls tcEnv) ty
Finn Teegen's avatar
Finn Teegen committed
587
  where
Finn Teegen's avatar
Finn Teegen committed
588
    doc = ppConstraint sc
Finn Teegen's avatar
Finn Teegen committed
589

590
591
kcTypeSig :: TCEnv -> Position -> QualTypeExpr -> KCM ()
kcTypeSig tcEnv p (QualTypeExpr cx ty) = do
Finn Teegen's avatar
Finn Teegen committed
592
  tcEnv' <- foldM bindFreshKind tcEnv free
593
  kcContext tcEnv' p cx
Finn Teegen's avatar
Finn Teegen committed
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
  kcValueType tcEnv' p "type signature" doc ty
  where
    free = filter (null . flip lookupTypeInfo tcEnv) $ nub $ fv ty
    doc = ppTypeExpr 0 ty

kcValueType :: TCEnv -> Position -> String -> Doc -> TypeExpr -> KCM ()
kcValueType tcEnv p what doc = kcType tcEnv p what doc KindStar

kcType :: TCEnv -> Position -> String -> Doc -> Kind -> TypeExpr -> KCM ()
kcType tcEnv p what doc k ty = do
  k' <- kcTypeExpr tcEnv p "type expression" doc' 0 ty
  unify p what (doc $-$ text "Type:" <+> doc') k k'
  where
    doc' = ppTypeExpr 0 ty

kcTypeExpr :: TCEnv -> Position -> String -> Doc -> Int -> TypeExpr -> KCM Kind
Finn Teegen's avatar
Finn Teegen committed
610
611
kcTypeExpr tcEnv p _ _ n (ConstructorType tc) = do
  m <- getModuleIdent
Finn Teegen's avatar
Finn Teegen committed
612
613
  case qualLookupTypeInfo tc tcEnv of
    [AliasType _ _ n' _] -> case n >= n' of
Finn Teegen's avatar
Finn Teegen committed
614
      True -> return $ tcKind m tc tcEnv
Finn Teegen's avatar
Finn Teegen committed
615
616
617
      False -> do
        report $ errPartialAlias p tc n' n
        freshKindVar
Finn Teegen's avatar
Finn Teegen committed
618
    _ -> return $ tcKind m tc tcEnv
Finn Teegen's avatar
Finn Teegen committed
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
kcTypeExpr tcEnv p what doc n (ApplyType ty1 ty2) = do
  (alpha, beta) <- kcTypeExpr tcEnv p what doc (n + 1) ty1 >>=
    kcArrow p what (doc $-$ text "Type:" <+> ppTypeExpr 0 ty1)
  kcTypeExpr tcEnv p what doc 0 ty2 >>=
    unify p what (doc $-$ text "Type:" <+> ppTypeExpr 0 ty2) alpha
  return beta
kcTypeExpr tcEnv _ _ _ _ (VariableType tv) = return (varKind tv tcEnv)
kcTypeExpr tcEnv p what doc _ (TupleType tys) = do
  mapM_ (kcValueType tcEnv p what doc) tys
  return KindStar
kcTypeExpr tcEnv p what doc _ (ListType ty) = do
  kcValueType tcEnv p what doc ty
  return KindStar
kcTypeExpr tcEnv p what doc _ (ArrowType ty1 ty2) = do
  kcValueType tcEnv p what doc ty1
  kcValueType tcEnv p what doc ty2
  return KindStar
kcTypeExpr tcEnv p what doc n (ParenType ty) = kcTypeExpr tcEnv p what doc n ty
637
638
639
kcTypeExpr tcEnv p what doc n (ForallType vs ty) = do
  tcEnv' <- foldM bindFreshKind tcEnv $ vs
  kcTypeExpr tcEnv' p what doc n ty
Finn Teegen's avatar
Finn Teegen committed
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656

kcArrow :: Position -> String -> Doc -> Kind -> KCM (Kind, Kind)
kcArrow p what doc k = do
  theta <- getKindSubst
  case subst theta k of
    KindStar -> do
      report $ errNonArrowKind p what doc KindStar
      (,) <$> freshKindVar <*> freshKindVar
    KindVariable kv -> do
      alpha <- freshKindVar
      beta <- freshKindVar
      modifyKindSubst $ bindVar kv $ KindArrow alpha beta
      return (alpha, beta)
    KindArrow k1 k2 -> return (k1, k2)

-- ---------------------------------------------------------------------------
-- Unification
657
-- ---------------------------------------------------------------------------
Finn Teegen's avatar
Finn Teegen committed
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685

-- The unification uses Robinson's algorithm.
unify :: Position -> String -> Doc -> Kind -> Kind -> KCM ()
unify p what doc k1 k2 = do
  theta <- getKindSubst
  let k1' = subst theta k1
  let k2' = subst theta k2
  case unifyKinds k1' k2' of
    Nothing -> report $ errKindMismatch p what doc k1' k2'
    Just sigma -> modifyKindSubst (compose sigma)

unifyKinds :: Kind -> Kind -> Maybe KindSubst
unifyKinds KindStar KindStar = Just idSubst
unifyKinds (KindVariable kv1) (KindVariable kv2)
  | kv1 == kv2 = Just idSubst
  | otherwise  = Just (singleSubst kv1 (KindVariable kv2))
unifyKinds (KindVariable kv) k
  | kv `elem` kindVars k = Nothing
  | otherwise            = Just (singleSubst kv k)
unifyKinds k (KindVariable kv)
  | kv `elem` kindVars k = Nothing
  | otherwise            = Just (singleSubst kv k)
unifyKinds (KindArrow k11 k12) (KindArrow k21 k22) = do
  theta <- unifyKinds k11 k21
  theta' <- unifyKinds (subst theta k12) (subst theta k22)
  Just (compose theta' theta)
unifyKinds _ _ = Nothing

686
-- ---------------------------------------------------------------------------
Finn Teegen's avatar
Finn Teegen committed
687
688
689
690
691
-- Fresh variables
-- ---------------------------------------------------------------------------

fresh :: (Int -> a) -> KCM a
fresh f = f <$> getNextId
692

Finn Teegen's avatar
Finn Teegen committed
693
694
freshKindVar :: KCM Kind
freshKindVar = fresh KindVariable
695

696
697
698
699
-- ---------------------------------------------------------------------------
-- Auxiliary definitions
-- ---------------------------------------------------------------------------

Finn Teegen's avatar
Finn Teegen committed
700
typeConstructor :: Decl a -> Ident
701
702
703
704
typeConstructor (DataDecl     _ tc _ _ _) = tc
typeConstructor (ExternalDataDecl _ tc _) = tc
typeConstructor (NewtypeDecl  _ tc _ _ _) = tc
typeConstructor (TypeDecl     _ tc _ _  ) = tc
Finn Teegen's avatar
Finn Teegen committed
705
typeConstructor _                        =
Finn Teegen's avatar
Finn Teegen committed
706
  internalError "Checks.KindCheck.typeConstructor: no type declaration"
707

Finn Teegen's avatar
Finn Teegen committed
708
isTypeOrNewtypeDecl :: Decl a -> Bool
Finn Teegen's avatar
Finn Teegen committed
709
710
711
isTypeOrNewtypeDecl (NewtypeDecl _ _ _ _ _) = True
isTypeOrNewtypeDecl (TypeDecl      _ _ _ _) = True
isTypeOrNewtypeDecl _                       = False
712

713
-- ---------------------------------------------------------------------------
Finn Teegen's avatar
Finn Teegen committed
714
-- Error messages
715
716
-- ---------------------------------------------------------------------------

Finn Teegen's avatar
Finn Teegen committed
717
718
719
720
errRecursiveTypes :: [Ident] -> Message
errRecursiveTypes []       = internalError
  "KindCheck.errRecursiveTypes: empty list"
errRecursiveTypes [tc]     = posMessage tc $ hsep $ map text
721
  ["Recursive synonym or renaming type", idName tc]
Finn Teegen's avatar
Finn Teegen committed
722
errRecursiveTypes (tc:tcs) = posMessage tc $
Finn Teegen's avatar
Finn Teegen committed
723
724
  text "Mutually recursive synonym and/or renaming types" <+>
    text (idName tc) <> types empty tcs
Finn Teegen's avatar
Finn Teegen committed
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
  where
    types _   []         = empty
    types del [tc']      = del <> space <> text "and" <+> typePos tc'
    types _   (tc':tcs') = comma <+> typePos tc' <> types comma tcs'
    typePos tc' =
      text (idName tc') <+> parens (text $ showLine $ idPosition tc')

errRecursiveClasses :: [Ident] -> Message
errRecursiveClasses []         = internalError
  "KindCheck.errRecursiveClasses: empty list"
errRecursiveClasses [cls]      = posMessage cls $ hsep $ map text
  ["Recursive type class", idName cls]
errRecursiveClasses (cls:clss) = posMessage cls $
  text "Mutually recursive type classes" <+> text (idName cls) <>
    classes empty clss
  where
    classes _   []           = empty
    classes del [cls']       = del <> space <> text "and" <+> classPos cls'
    classes _   (cls':clss') = comma <+> classPos cls' <> classes comma clss'
    classPos cls' =
      text (idName cls') <+> parens (text $ showLine $ idPosition cls')

errNonArrowKind :: Position -> String -> Doc -> Kind -> Message
errNonArrowKind p what doc k = posMessage p $ vcat
  [ text "Kind error in" <+> text what, doc
  , text "Kind:" <+> ppKind k
  , text "Cannot be applied"
  ]

errPartialAlias :: Position -> QualIdent -> Int -> Int -> Message
errPartialAlias p tc arity argc = posMessage p $ hsep
  [ text "Type synonym", ppQIdent tc
  , text "requires at least"
  , int arity, text (plural arity "argument") <> comma
  , text "but is applied to only", int argc
  ]
  where
    plural n x = if n == 1 then x else x ++ "s"

errKindMismatch :: Position -> String -> Doc -> Kind -> Kind -> Message
errKindMismatch p what doc k1 k2 = posMessage p $ vcat
  [ text "Kind error in"  <+> text what, doc
  , text "Inferred kind:" <+> ppKind k2
  , text "Expected kind:" <+> ppKind k1
  ]