TcTyClsDecls.hs 93.7 KB
Newer Older
Austin Seipp's avatar
Austin Seipp committed
1
2
3
4
{-
(c) The University of Glasgow 2006
(c) The AQUA Project, Glasgow University, 1996-1998

5
6

TcTyClsDecls: Typecheck type and class declarations
Austin Seipp's avatar
Austin Seipp committed
7
-}
8

9
{-# LANGUAGE CPP, TupleSections #-}
Ian Lynagh's avatar
Ian Lynagh committed
10

11
module TcTyClsDecls (
12
        tcTyAndClassDecls, tcAddImplicits,
13

14
15
        -- Functions used by TcInstDcls to check
        -- data/type family instance declarations
16
        kcDataDefn, tcConDecls, dataDeclChecks, checkValidTyCon,
17
        tcFamTyPats, tcTyFamInstEqn, famTyConShape,
18
        tcAddTyFamInstCtxt, tcMkDataFamInstCtxt, tcAddDataFamInstCtxt,
19
        wrongKindOfFamily, dataConCtxt, badDataConTyCon
20
21
    ) where

22
#include "HsVersions.h"
23

24
25
26
import HsSyn
import HscTypes
import BuildTyCl
27
import TcRnMonad
28
import TcEnv
29
import TcValidity
30
import TcHsSyn
31
32
33
34
35
import TcTyDecls
import TcClassDcl
import TcHsType
import TcMType
import TcType
36
import FamInst
Jan Stolarek's avatar
Jan Stolarek committed
37
38
import FamInstEnv
import Coercion( ltRole )
39
import Type
40
import TypeRep   -- for checkValidRoles
dreixel's avatar
dreixel committed
41
import Kind
42
import Class
43
import CoAxiom
44
45
import TyCon
import DataCon
46
import Id
47
-- import IdInfo
48
import Var
49
import VarEnv
50
import VarSet
51
import Module
52
import Name
53
import NameSet
54
import NameEnv
Adam Gundry's avatar
Adam Gundry committed
55
import RnEnv
sof's avatar
sof committed
56
import Outputable
57
58
59
60
61
62
63
import Maybes
import Unify
import Util
import SrcLoc
import ListSetOps
import Digraph
import DynFlags
64
import FastString
65
import BasicTypes
66

Ian Lynagh's avatar
Ian Lynagh committed
67
import Control.Monad
68
import Data.List
69

Austin Seipp's avatar
Austin Seipp committed
70
71
72
{-
************************************************************************
*                                                                      *
73
\subsection{Type checking for type and class declarations}
Austin Seipp's avatar
Austin Seipp committed
74
75
*                                                                      *
************************************************************************
76

dreixel's avatar
dreixel committed
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
Note [Grouping of type and class declarations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
tcTyAndClassDecls is called on a list of `TyClGroup`s. Each group is a strongly
connected component of mutually dependent types and classes. We kind check and
type check each group separately to enhance kind polymorphism. Take the
following example:

  type Id a = a
  data X = X (Id Int)

If we were to kind check the two declarations together, we would give Id the
kind * -> *, since we apply it to an Int in the definition of X. But we can do
better than that, since Id really is kind polymorphic, and should get kind
forall (k::BOX). k -> k. Since it does not depend on anything else, it can be
kind-checked by itself, hence getting the most general kind. We then kind check
X, which works fine because we then know the polymorphic kind of Id, and simply
instantiate k to *.

95
96
97
98
99
100
101
102
103
Note [Check role annotations in a second pass]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Role inference potentially depends on the types of all of the datacons declared
in a mutually recursive group. The validity of a role annotation, in turn,
depends on the result of role inference. Because the types of datacons might
be ill-formed (see #7175 and Note [Checking GADT return types]) we must check
*all* the tycons in a group for validity before checking *any* of the roles.
Thus, we take two passes over the resulting tycons, first checking for general
validity and then checking for valid role annotations.
Austin Seipp's avatar
Austin Seipp committed
104
-}
105

Simon Peyton Jones's avatar
Simon Peyton Jones committed
106
tcTyAndClassDecls :: [TyClGroup Name]   -- Mutually-recursive groups in dependency order
107
108
                  -> TcM TcGblEnv       -- Input env extended by types and classes
                                        -- and their implicit Ids,DataCons
109
-- Fails if there are any errors
Simon Peyton Jones's avatar
Simon Peyton Jones committed
110
tcTyAndClassDecls tyclds_s
111
  = checkNoErrs $       -- The code recovers internally, but if anything gave rise to
dreixel's avatar
dreixel committed
112
                        -- an error we'd better stop now, to avoid a cascade
113
    fold_env tyclds_s   -- Type check each group in dependency order folding the global env
dreixel's avatar
dreixel committed
114
115
116
117
  where
    fold_env :: [TyClGroup Name] -> TcM TcGblEnv
    fold_env [] = getGblEnv
    fold_env (tyclds:tyclds_s)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
118
      = do { tcg_env <- tcTyClGroup tyclds
119
           ; setGblEnv tcg_env $ fold_env tyclds_s }
dreixel's avatar
dreixel committed
120
121
             -- remaining groups are typecheck in the extended global env

Simon Peyton Jones's avatar
Simon Peyton Jones committed
122
tcTyClGroup :: TyClGroup Name -> TcM TcGblEnv
dreixel's avatar
dreixel committed
123
-- Typecheck one strongly-connected component of type and class decls
Simon Peyton Jones's avatar
Simon Peyton Jones committed
124
tcTyClGroup tyclds
dreixel's avatar
dreixel committed
125
126
127
  = do {    -- Step 1: kind-check this group and returns the final
            -- (possibly-polymorphic) kind of each TyCon and Class
            -- See Note [Kind checking for type and class decls]
128
         names_w_poly_kinds <- kcTyClGroup tyclds
dreixel's avatar
dreixel committed
129
130
       ; traceTc "tcTyAndCl generalized kinds" (ppr names_w_poly_kinds)

131
132
            -- Step 2: type-check all groups together, returning
            -- the final TyCons and Classes
133
134
       ; let role_annots = extractRoleAnnots tyclds
             decls = group_tyclds tyclds
Jan Stolarek's avatar
Jan Stolarek committed
135
       ; tyclss <- fixM $ \ ~rec_tyclss -> do
Simon Peyton Jones's avatar
Simon Peyton Jones committed
136
137
138
           { is_boot   <- tcIsHsBootOrSig
           ; self_boot <- tcSelfBootInfo
           ; let rec_flags = calcRecFlags self_boot is_boot
139
                                          role_annots rec_tyclss
dreixel's avatar
dreixel committed
140
141
142

                 -- Populate environment with knot-tied ATyCon for TyCons
                 -- NB: if the decls mention any ill-staged data cons
Jan Stolarek's avatar
Jan Stolarek committed
143
                 -- (see Note [Recusion and promoting data constructors])
144
145
                 -- we will have failed already in kcTyClGroup, so no worries here
           ; tcExtendRecEnv (zipRecTyClss names_w_poly_kinds rec_tyclss) $
dreixel's avatar
dreixel committed
146
147
148

                 -- Also extend the local type envt with bindings giving
                 -- the (polymorphic) kind of each knot-tied TyCon or Class
149
150
                 -- See Note [Type checking recursive type and class declarations]
             tcExtendKindEnv names_w_poly_kinds              $
dreixel's avatar
dreixel committed
151
152

                 -- Kind and type check declarations for this group
153
             mapM (tcTyClDecl rec_flags) decls }
dreixel's avatar
dreixel committed
154

155
           -- Step 3: Perform the validity check
dreixel's avatar
dreixel committed
156
157
158
           -- We can do this now because we are done with the recursive knot
           -- Do it before Step 4 (adding implicit things) because the latter
           -- expects well-formed TyCons
159
160
161
       ; traceTc "Starting validity check" (ppr tyclss)
       ; tyclss <- mapM checkValidTyCl tyclss
       ; traceTc "Done validity check" (ppr tyclss)
162
163
       ; mapM_ (recoverM (return ()) . checkValidRoleAnnots role_annots) tyclss
           -- See Note [Check role annotations in a second pass]
dreixel's avatar
dreixel committed
164
165
166
167

           -- Step 4: Add the implicit things;
           -- we want them in the environment because
           -- they may be mentioned in interface files
168
169
       ; tcExtendTyConEnv tyclss $
         tcAddImplicits tyclss }
dreixel's avatar
dreixel committed
170

171
zipRecTyClss :: [(Name, Kind)]
172
             -> [TyCon]           -- Knot-tied
173
174
175
             -> [(Name,TyThing)]
-- Build a name-TyThing mapping for the things bound by decls
-- being careful not to look at the [TyThing]
batterseapower's avatar
batterseapower committed
176
-- The TyThings in the result list must have a visible ATyCon,
177
-- because typechecking types (in, say, tcTyClDecl) looks at this outer constructor
178
zipRecTyClss kind_pairs rec_tycons
179
  = [ (name, ATyCon (get name)) | (name, _kind) <- kind_pairs ]
180
  where
181
182
    rec_tc_env :: NameEnv TyCon
    rec_tc_env = foldr add_tc emptyNameEnv rec_tycons
183

184
185
186
187
188
189
190
191
192
    add_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon
    add_tc tc env = foldr add_one_tc env (tc : tyConATs tc)

    add_one_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon
    add_one_tc tc env = extendNameEnv env (tyConName tc) tc

    get name = case lookupNameEnv rec_tc_env name of
                 Just tc -> tc
                 other   -> pprPanic "zipRecTyClss" (ppr name <+> ppr other)
193

Austin Seipp's avatar
Austin Seipp committed
194
195
196
{-
************************************************************************
*                                                                      *
197
                Kind checking
Austin Seipp's avatar
Austin Seipp committed
198
199
*                                                                      *
************************************************************************
200

201
202
203
204
Note [Kind checking for type and class decls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Kind checking is done thus:

205
206
207
   1. Make up a kind variable for each parameter of the *data* type, class,
      and closed type family decls, and extend the kind environment (which is
      in the TcLclEnv)
208
209
210
211
212
213

   2. Dependency-analyse the type *synonyms* (which must be non-recursive),
      and kind-check them in dependency order.  Extend the kind envt.

   3. Kind check the data type and class decls

214
215
We need to kind check all types in the mutually recursive group
before we know the kind of the type variables.  For example:
216

217
218
  class C a where
     op :: D b => a -> b -> b
219

220
221
  class D c where
     bop :: (Monad c) => ...
222
223
224
225
226

Here, the kind of the locally-polymorphic type variable "b"
depends on *all the uses of class D*.  For example, the use of
Monad c in bop's type signature means that D must have kind Type->Type.

227
228
However type synonyms work differently.  They can have kinds which don't
just involve (->) and *:
229
230
231
        type R = Int#           -- Kind #
        type S a = Array# a     -- Kind * -> #
        type T a b = (# a,b #)  -- Kind * -> * -> (# a,b #)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
232
233
234
235
236
237
238
239
240
241
and a kind variable can't unify with UnboxedTypeKind.

So we must infer the kinds of type synonyms from their right-hand
sides *first* and then use them, whereas for the mutually recursive
data types D we bring into scope kind bindings D -> k, where k is a
kind variable, and do inference.

NB: synonyms can be mutually recursive with data type declarations though!
   type T = D -> D
   data D = MkD Int T
242

243
244
Open type families
~~~~~~~~~~~~~~~~~~
245
246
247
This treatment of type synonyms only applies to Haskell 98-style synonyms.
General type functions can be recursive, and hence, appear in `alg_decls'.

248
The kind of an open type family is solely determinded by its kind signature;
249
hence, only kind signatures participate in the construction of the initial
250
251
252
253
kind environment (as constructed by `getInitialKind'). In fact, we ignore
instances of families altogether in the following. However, we need to include
the kinds of *associated* families into the construction of the initial kind
environment. (This is handled by `allDecls').
Austin Seipp's avatar
Austin Seipp committed
254
-}
255

256
kcTyClGroup :: TyClGroup Name -> TcM [(Name,Kind)]
dreixel's avatar
dreixel committed
257
-- Kind check this group, kind generalize, and return the resulting local env
258
-- This bindds the TyCons and Classes of the group, but not the DataCons
dreixel's avatar
dreixel committed
259
-- See Note [Kind checking for type and class decls]
260
kcTyClGroup (TyClGroup { group_tyclds = decls })
261
262
  = do  { mod <- getModule
        ; traceTc "kcTyClGroup" (ptext (sLit "module") <+> ppr mod $$ vcat (map ppr decls))
dreixel's avatar
dreixel committed
263

264
265
          -- Kind checking;
          --    1. Bind kind variables for non-synonyms
dreixel's avatar
dreixel committed
266
267
          --    2. Kind-check synonyms, and bind kinds of those synonyms
          --    3. Kind-check non-synonyms
268
          --    4. Generalise the inferred kinds
dreixel's avatar
dreixel committed
269
270
          -- See Note [Kind checking for type and class decls]

271
          -- Step 1: Bind kind variables for non-synonyms
dreixel's avatar
dreixel committed
272
        ; let (syn_decls, non_syn_decls) = partition (isSynDecl . unLoc) decls
273
        ; initial_kinds <- getInitialKinds non_syn_decls
274
        ; traceTc "kcTyClGroup: initial kinds" (ppr initial_kinds)
275
276

        -- Step 2: Set initial envt, kind-check the synonyms
277
        ; lcl_env <- tcExtendKindEnv2 initial_kinds $
278
                     kcSynDecls (calcSynCycles syn_decls)
279
280
281
282

        -- Step 3: Set extended envt, kind-check the non-synonyms
        ; setLclEnv lcl_env $
          mapM_ kcLTyClDecl non_syn_decls
dreixel's avatar
dreixel committed
283

284
285
             -- Step 4: generalisation
             -- Kind checking done for this group
dreixel's avatar
dreixel committed
286
             -- Now we have to kind generalize the flexis
287
        ; res <- concatMapM (generaliseTCD (tcl_env lcl_env)) decls
288
289

        ; traceTc "kcTyClGroup result" (ppr res)
290
        ; return res }
291

292
  where
293
    generalise :: TcTypeEnv -> Name -> TcM (Name, Kind)
294
    -- For polymorphic things this is a no-op
295
    generalise kind_env name
296
      = do { let kc_kind = case lookupNameEnv kind_env name of
297
298
                               Just (AThing k) -> k
                               _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env)
299
           ; kvs <- kindGeneralize (tyVarsOfType kc_kind)
300
301
302
           ; kc_kind' <- zonkTcKind kc_kind    -- Make sure kc_kind' has the final,
                                               -- skolemised kind variables
           ; traceTc "Generalise kind" (vcat [ ppr name, ppr kc_kind, ppr kvs, ppr kc_kind' ])
dreixel's avatar
dreixel committed
303
304
           ; return (name, mkForAllTys kvs kc_kind') }

305
306
    generaliseTCD :: TcTypeEnv -> LTyClDecl Name -> TcM [(Name, Kind)]
    generaliseTCD kind_env (L _ decl)
307
308
      | ClassDecl { tcdLName = (L _ name), tcdATs = ats } <- decl
      = do { first <- generalise kind_env name
309
310
311
312
313
314
315
316
           ; rest <- mapM ((generaliseFamDecl kind_env) . unLoc) ats
           ; return (first : rest) }

      | FamDecl { tcdFam = fam } <- decl
      = do { res <- generaliseFamDecl kind_env fam
           ; return [res] }

      | otherwise
317
      = do { res <- generalise kind_env (tcdName decl)
318
319
320
           ; return [res] }

    generaliseFamDecl :: TcTypeEnv -> FamilyDecl Name -> TcM (Name, Kind)
321
322
    generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name })
      = generalise kind_env name
323

324
325
326
327
328
329
330
331
332
333
334
335
mk_thing_env :: [LTyClDecl Name] -> [(Name, TcTyThing)]
mk_thing_env [] = []
mk_thing_env (decl : decls)
  | L _ (ClassDecl { tcdLName = L _ nm, tcdATs = ats }) <- decl
  = (nm, APromotionErr ClassPE) :
    (map (, APromotionErr TyConPE) $ map (unLoc . fdLName . unLoc) ats) ++
    (mk_thing_env decls)

  | otherwise
  = (tcdName (unLoc decl), APromotionErr TyConPE) :
    (mk_thing_env decls)

336
getInitialKinds :: [LTyClDecl Name] -> TcM [(Name, TcTyThing)]
337
getInitialKinds decls
338
  = tcExtendKindEnv2 (mk_thing_env decls) $
339
340
    do { pairss <- mapM (addLocM getInitialKind) decls
       ; return (concat pairss) }
341

342
getInitialKind :: TyClDecl Name -> TcM [(Name, TcTyThing)]
dreixel's avatar
dreixel committed
343
344
345
346
347
348
-- Allocate a fresh kind variable for each TyCon and Class
-- For each tycon, return   (tc, AThing k)
--                 where k is the kind of tc, derived from the LHS
--                       of the definition (and probably including
--                       kind unification variables)
--      Example: data T a b = ...
349
--      return (T, kv1 -> kv2 -> kv3)
dreixel's avatar
dreixel committed
350
--
351
352
353
354
355
356
-- This pass deals with (ie incorporates into the kind it produces)
--   * The kind signatures on type-variable binders
--   * The result kinds signature on a TyClDecl
--
-- ALSO for each datacon, return (dc, APromotionErr RecDataConPE)
-- Note [ARecDataCon: Recursion and promoting data constructors]
357
--
358
-- No family instances are passed to getInitialKinds
dreixel's avatar
dreixel committed
359

360
getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
361
  = do { (cl_kind, inner_prs) <-
362
           kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $
363
364
365
           do { inner_prs <- getFamDeclInitialKinds ats
              ; return (constraintKind, inner_prs) }
       ; let main_pr = (name, AThing cl_kind)
366
       ; return (main_pr : inner_prs) }
367

368
getInitialKind decl@(DataDecl { tcdLName = L _ name
369
370
371
372
373
374
                              , tcdTyVars = ktvs
                              , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
                                                         , dd_cons = cons' } })
  = let cons = cons' -- AZ list monad coming
    in
     do { (decl_kind, _) <-
375
           kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $
376
377
378
           do { res_k <- case m_sig of
                           Just ksig -> tcLHsKind ksig
                           Nothing   -> return liftedTypeKind
379
              ; return (res_k, ()) }
380
       ; let main_pr = (name, AThing decl_kind)
381
382
             inner_prs = [ (unLoc con, APromotionErr RecDataConPE)
                         | L _ con' <- cons, con <- con_names con' ]
383
       ; return (main_pr : inner_prs) }
384

Jan Stolarek's avatar
Jan Stolarek committed
385
getInitialKind (FamDecl { tcdFam = decl })
386
  = getFamDeclInitialKind decl
387

Jan Stolarek's avatar
Jan Stolarek committed
388
getInitialKind decl@(SynDecl {})
389
390
391
  = pprPanic "getInitialKind" (ppr decl)

---------------------------------
392
393
getFamDeclInitialKinds :: [LFamilyDecl Name] -> TcM [(Name, TcTyThing)]
getFamDeclInitialKinds decls
394
395
  = tcExtendKindEnv2 [ (n, APromotionErr TyConPE)
                     | L _ (FamilyDecl { fdLName = L _ n }) <- decls] $
396
    concatMapM (addLocM getFamDeclInitialKind) decls
397

398
getFamDeclInitialKind :: FamilyDecl Name
399
                      -> TcM [(Name, TcTyThing)]
Jan Stolarek's avatar
Jan Stolarek committed
400
401
402
getFamDeclInitialKind decl@(FamilyDecl { fdLName     = L _ name
                                       , fdTyVars    = ktvs
                                       , fdResultSig = L _ resultSig })
403
  = do { (fam_kind, _) <-
404
           kcHsTyVarBndrs (famDeclHasCusk decl) ktvs $
Jan Stolarek's avatar
Jan Stolarek committed
405
406
407
408
409
410
411
412
           do { res_k <- case resultSig of
                      KindSig ki                        -> tcLHsKind ki
                      TyVarSig (L _ (KindedTyVar _ ki)) -> tcLHsKind ki
                      _ -- open type families have * return kind by default
                        | famDeclHasCusk decl      -> return liftedTypeKind
                        -- closed type families have their return kind inferred
                        -- by default
                        | otherwise                -> newMetaKindVar
413
414
              ; return (res_k, ()) }
       ; return [ (name, AThing fam_kind) ] }
415

416
----------------
417
kcSynDecls :: [SCC (LTyClDecl Name)]
418
419
           -> TcM TcLclEnv -- Kind bindings
kcSynDecls [] = getLclEnv
420
kcSynDecls (group : groups)
421
422
423
  = do  { (n,k) <- kcSynDecl1 group
        ; lcl_env <- tcExtendKindEnv [(n,k)] (kcSynDecls groups)
        ; return lcl_env }
dreixel's avatar
dreixel committed
424
425

kcSynDecl1 :: SCC (LTyClDecl Name)
426
           -> TcM (Name,TcKind) -- Kind bindings
dreixel's avatar
dreixel committed
427
428
kcSynDecl1 (AcyclicSCC (L _ decl)) = kcSynDecl decl
kcSynDecl1 (CyclicSCC decls)       = do { recSynErr decls; failM }
429
430
                                     -- Fail here to avoid error cascade
                                     -- of out-of-scope tycons
dreixel's avatar
dreixel committed
431

432
kcSynDecl :: TyClDecl Name -> TcM (Name, TcKind)
433
kcSynDecl decl@(SynDecl { tcdTyVars = hs_tvs, tcdLName = L _ name
434
                        , tcdRhs = rhs })
435
  -- Returns a possibly-unzonked kind
dreixel's avatar
dreixel committed
436
  = tcAddDeclCtxt decl $
437
    do { (syn_kind, _) <-
438
           kcHsTyVarBndrs (hsDeclHasCusk decl) hs_tvs $
439
440
441
442
           do { traceTc "kcd1" (ppr name <+> brackets (ppr hs_tvs))
              ; (_, rhs_kind) <- tcLHsType rhs
              ; traceTc "kcd2" (ppr name)
              ; return (rhs_kind, ()) }
443
       ; return (name, syn_kind) }
444
kcSynDecl decl = pprPanic "kcSynDecl" (ppr decl)
445

446
------------------------------------------------------------------------
447
kcLTyClDecl :: LTyClDecl Name -> TcM ()
448
  -- See Note [Kind checking for type and class decls]
449
450
451
kcLTyClDecl (L loc decl)
  = setSrcSpan loc $ tcAddDeclCtxt decl $ kcTyClDecl decl

dreixel's avatar
dreixel committed
452
453
kcTyClDecl :: TyClDecl Name -> TcM ()
-- This function is used solely for its side effect on kind variables
454
-- NB kind signatures on the type variables and
Gabor Greif's avatar
Gabor Greif committed
455
--    result kind signature have already been dealt with
456
--    by getInitialKind, so we can ignore them here.
dreixel's avatar
dreixel committed
457

458
459
kcTyClDecl (DataDecl { tcdLName = L _ name, tcdTyVars = hs_tvs, tcdDataDefn = defn })
  | HsDataDefn { dd_cons = cons, dd_kindSig = Just _ } <- defn
460
  = mapM_ (wrapLocM kcConDecl) cons
461
462
463
464
465
466
    -- hs_tvs and dd_kindSig already dealt with in getInitialKind
    -- If dd_kindSig is Just, this must be a GADT-style decl,
    --        (see invariants of DataDefn declaration)
    -- so (a) we don't need to bring the hs_tvs into scope, because the
    --        ConDecls bind all their own variables
    --    (b) dd_ctxt is not allowed for GADT-style decls, so we can ignore it
467

468
469
  | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
  = kcTyClTyVars name hs_tvs $
470
    do  { _ <- tcHsContext ctxt
471
        ; mapM_ (wrapLocM kcConDecl) cons }
472

473
kcTyClDecl decl@(SynDecl {}) = pprPanic "kcTyClDecl" (ppr decl)
474
475

kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs
476
477
                       , tcdCtxt = ctxt, tcdSigs = sigs })
  = kcTyClTyVars name hs_tvs $
478
    do  { _ <- tcHsContext ctxt
479
        ; mapM_ (wrapLocM kc_sig) sigs }
dreixel's avatar
dreixel committed
480
  where
thomasw's avatar
thomasw committed
481
    kc_sig (TypeSig _ op_ty _)  = discardResult (tcHsLiftedType op_ty)
482
    kc_sig (GenericSig _ op_ty) = discardResult (tcHsLiftedType op_ty)
dreixel's avatar
dreixel committed
483
    kc_sig _                    = return ()
484

485
486
-- closed type families look at their equations, but other families don't
-- do anything here
487
488
kcTyClDecl (FamDecl (FamilyDecl { fdLName  = L _ fam_tc_name
                                , fdTyVars = hs_tvs
489
                                , fdInfo   = ClosedTypeFamily (Just eqns) }))
490
491
492
  = do { tc_kind <- kcLookupKind fam_tc_name
       ; let fam_tc_shape = ( fam_tc_name, length (hsQTvBndrs hs_tvs), tc_kind)
       ; mapM_ (kcTyFamInstEqn fam_tc_shape) eqns }
493
kcTyClDecl (FamDecl {})    = return ()
dreixel's avatar
dreixel committed
494
495

-------------------
496
kcConDecl :: ConDecl Name -> TcM ()
497
kcConDecl (ConDecl { con_names = names, con_qvars = ex_tvs
498
499
                   , con_cxt = ex_ctxt, con_details = details
                   , con_res = res })
500
  = addErrCtxt (dataConCtxtName names) $
501
502
503
504
         -- the 'False' says that the existentials don't have a CUSK, as the
         -- concept doesn't really apply here. We just need to bring the variables
         -- into scope!
    do { _ <- kcHsTyVarBndrs False ex_tvs $
505
506
              do { _ <- tcHsContext ex_ctxt
                 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details)
507
                 ; _ <- tcConRes res
508
                 ; return (panic "kcConDecl", ()) }
509
       ; return () }
510

Austin Seipp's avatar
Austin Seipp committed
511
{-
512
513
Note [Recursion and promoting data constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
514
515
516
517
518
519
520
521
522
523
524
525
526
527
We don't want to allow promotion in a strongly connected component
when kind checking.

Consider:
  data T f = K (f (K Any))

When kind checking the `data T' declaration the local env contains the
mappings:
  T -> AThing <some initial kind>
  K -> ARecDataCon

ANothing is only used for DataCons, and only used during type checking
in tcTyClGroup.

528

Austin Seipp's avatar
Austin Seipp committed
529
530
************************************************************************
*                                                                      *
531
\subsection{Type checking}
Austin Seipp's avatar
Austin Seipp committed
532
533
*                                                                      *
************************************************************************
534

dreixel's avatar
dreixel committed
535
536
537
538
Note [Type checking recursive type and class declarations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
At this point we have completed *kind-checking* of a mutually
recursive group of type/class decls (done in kcTyClGroup). However,
539
we discarded the kind-checked types (eg RHSs of data type decls);
dreixel's avatar
dreixel committed
540
541
542
543
544
545
546
note that kcTyClDecl returns ().  There are two reasons:

  * It's convenient, because we don't have to rebuild a
    kinded HsDecl (a fairly elaborate type)

  * It's necessary, because after kind-generalisation, the
    TyCons/Classes may now be kind-polymorphic, and hence need
547
    to be given kind arguments.
dreixel's avatar
dreixel committed
548
549
550
551
552
553
554

Example:
       data T f a = MkT (f a) (T f a)
During kind-checking, we give T the kind T :: k1 -> k2 -> *
and figure out constraints on k1, k2 etc. Then we generalise
to get   T :: forall k. (k->*) -> k -> *
So now the (T f a) in the RHS must be elaborated to (T k f a).
555

dreixel's avatar
dreixel committed
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
However, during tcTyClDecl of T (above) we will be in a recursive
"knot". So we aren't allowed to look at the TyCon T itself; we are only
allowed to put it (lazily) in the returned structures.  But when
kind-checking the RHS of T's decl, we *do* need to know T's kind (so
that we can correctly elaboarate (T k f a).  How can we get T's kind
without looking at T?  Delicate answer: during tcTyClDecl, we extend

  *Global* env with T -> ATyCon (the (not yet built) TyCon for T)
  *Local*  env with T -> AThing (polymorphic kind of T)

Then:

  * During TcHsType.kcTyVar we look in the *local* env, to get the
    known kind for T.

  * But in TcHsType.ds_type (and ds_var_app in particular) we look in
    the *global* env to get the TyCon. But we must be careful not to
    force the TyCon or we'll get a loop.

Gabor Greif's avatar
Gabor Greif committed
575
This fancy footwork (with two bindings for T) is only necessary for the
dreixel's avatar
dreixel committed
576
577
TyCons or Classes of this recursive group.  Earlier, finished groups,
live in the global env only.
578
579
580
581
582
583
584

Note [Declarations for wired-in things]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For wired-in things we simply ignore the declaration
and take the wired-in information.  That avoids complications.
e.g. the need to make the data constructor worker name for
     a constraint tuple match the wired-in one
Austin Seipp's avatar
Austin Seipp committed
585
-}
dreixel's avatar
dreixel committed
586

587
tcTyClDecl :: RecTyInfo -> LTyClDecl Name -> TcM TyCon
588
tcTyClDecl rec_info (L loc decl)
589
  | Just thing <- wiredInNameTyThing_maybe (tcdName decl)
590
591
592
  = case thing of -- See Note [Declarations for wired-in things]
      ATyCon tc -> return tc
      _ -> pprPanic "tcTyClDecl" (ppr thing)
593
594

  | otherwise
595
  = setSrcSpan loc $ tcAddDeclCtxt decl $
596
    do { traceTc "tcTyAndCl-x" (ppr decl)
597
       ; tcTyClDecl1 Nothing rec_info decl }
598

599
  -- "type family" declarations
600
tcTyClDecl1 :: Maybe Class -> RecTyInfo -> TyClDecl Name -> TcM TyCon
601
tcTyClDecl1 parent _rec_info (FamDecl { tcdFam = fd })
602
  = tcFamDecl1 parent fd
603

604
  -- "type" synonym declaration
605
tcTyClDecl1 _parent rec_info
606
            (SynDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdRhs = rhs })
607
  = ASSERT( isNothing _parent )
608
    tcTyClTyVars tc_name tvs $ \ tvs' kind ->
609
    tcTySynRhs rec_info tc_name tvs' kind rhs
610

611
  -- "data/newtype" declaration
612
tcTyClDecl1 _parent rec_info
613
            (DataDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdDataDefn = defn })
614
  = ASSERT( isNothing _parent )
615
    tcTyClTyVars tc_name tvs $ \ tvs' kind ->
616
    tcDataDefn rec_info tc_name tvs' kind defn
617

618
tcTyClDecl1 _parent rec_info
dreixel's avatar
dreixel committed
619
            (ClassDecl { tcdLName = L _ class_name, tcdTyVars = tvs
620
            , tcdCtxt = ctxt, tcdMeths = meths
621
            , tcdFDs = fundeps, tcdSigs = sigs
622
            , tcdATs = ats, tcdATDefs = at_defs })
623
  = ASSERT( isNothing _parent )
624
    do { clas <- fixM $ \ clas ->
625
            tcTyClTyVars class_name tvs $ \ tvs' kind ->
626
            do { MASSERT( isConstraintKind kind )
627
628
629
                 -- This little knot is just so we can get
                 -- hold of the name of the class TyCon, which we
                 -- need to look up its recursiveness
Jan Stolarek's avatar
Jan Stolarek committed
630
               ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr tvs' $$ ppr kind)
631
632
633
               ; let tycon_name = tyConName (classTyCon clas)
                     tc_isrec = rti_is_rec rec_info tycon_name
                     roles = rti_roles rec_info tycon_name
dreixel's avatar
dreixel committed
634

635
               ; ctxt' <- tcHsContext ctxt
636
               ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'
637
638
                       -- Squeeze out any kind unification variables
               ; fds'  <- mapM (addLocM tc_fundep) fundeps
639
               ; sig_stuff <- tcClassSigs class_name sigs meths
640
               ; at_stuff <- tcClassATs class_name clas ats at_defs
641
               ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
642
               ; clas <- buildClass
643
                            class_name tvs' roles ctxt' fds' at_stuff
644
                            sig_stuff mindef tc_isrec
645
               ; traceTc "tcClassDecl" (ppr fundeps $$ ppr tvs' $$ ppr fds')
646
647
648
               ; return clas }

         ; return (classTyCon clas) }
649
  where
Jan Stolarek's avatar
Jan Stolarek committed
650
651
    tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM tcFdTyVar tvs1
                                ; tvs2' <- mapM tcFdTyVar tvs2
652
                                ; return (tvs1', tvs2') }
Jan Stolarek's avatar
Jan Stolarek committed
653
654
655
656
657
658
659
660
661
662
663
664
665

tcFdTyVar :: Located Name -> TcM TcTyVar
-- Look up a type/kind variable in a functional dependency
-- or injectivity annotation.  In the case of kind variables,
-- the environment contains a binding of the kind var to a
-- a SigTv unification variables, which has now fixed.
-- So we must zonk to get the real thing.  Ugh!
tcFdTyVar (L _ name)
  = do { tv <- tcLookupTyVar name
       ; ty <- zonkTyVarOcc emptyZonkEnv tv
       ; case getTyVar_maybe ty of
           Just tv' -> return tv'
           Nothing  -> pprPanic "tcFdTyVar" (ppr name $$ ppr tv $$ ppr ty) }
666

667
tcFamDecl1 :: Maybe Class -> FamilyDecl Name -> TcM TyCon
668
669
670
671
tcFamDecl1 parent
            (FamilyDecl { fdInfo = OpenTypeFamily, fdLName = L _ tc_name
                        , fdTyVars = tvs, fdResultSig = L _ sig
                        , fdInjectivityAnn = inj })
672
  = tcTyClTyVars tc_name tvs $ \ tvs' kind -> do
673
  { traceTc "open type family:" (ppr tc_name)
674
  ; checkFamFlag tc_name
Jan Stolarek's avatar
Jan Stolarek committed
675
676
677
  ; inj' <- tcInjectivity tvs' inj
  ; let tycon = buildFamilyTyCon tc_name tvs' (resultVariableName sig)
                                 OpenSynFamilyTyCon kind parent inj'
678
  ; return tycon }
679
680

tcFamDecl1 parent
681
            (FamilyDecl { fdInfo = ClosedTypeFamily mb_eqns
Jan Stolarek's avatar
Jan Stolarek committed
682
683
                        , fdLName = L _ tc_name, fdTyVars = tvs
                        , fdResultSig = L _ sig, fdInjectivityAnn = inj })
684
685
-- Closed type families are a little tricky, because they contain the definition
-- of both the type family and the equations for a CoAxiom.
Jan Stolarek's avatar
Jan Stolarek committed
686
687
688
689
690
691
  = do { traceTc "Closed type family:" (ppr tc_name)
         -- the variables in the header scope only over the injectivity
         -- declaration but this is not involved here
       ; (tvs', inj', kind) <- tcTyClTyVars tc_name tvs $ \ tvs' kind ->
                               do { inj' <- tcInjectivity tvs' inj
                                  ; return (tvs', inj', kind) }
692
693
694

       ; checkFamFlag tc_name -- make sure we have -XTypeFamilies

695
696
697
         -- If Nothing, this is an abstract family in a hs-boot file;
         -- but eqns might be empty in the Just case as well
       ; case mb_eqns of
698
699
700
           Nothing   -> return $
                        buildFamilyTyCon tc_name tvs' (resultVariableName sig)
                                 AbstractClosedSynFamilyTyCon kind parent inj'
701
702
           Just eqns -> do {

703
704
         -- Process the equations, creating CoAxBranches
       ; tc_kind <- kcLookupKind tc_name
Jan Stolarek's avatar
Jan Stolarek committed
705
706
       ; let fam_tc_shape = (tc_name, length (hsQTvBndrs tvs), tc_kind)

707
       ; branches <- mapM (tcTyFamInstEqn fam_tc_shape Nothing) eqns
Jan Stolarek's avatar
Jan Stolarek committed
708
709
710
711
712
         -- Do not attempt to drop equations dominated by earlier
         -- ones here; in the case of mutual recursion with a data
         -- type, we get a knot-tying failure.  Instead we check
         -- for this afterwards, in TcValidity.checkValidCoAxiom
         -- Example: tc265
713

Jan Stolarek's avatar
Jan Stolarek committed
714
         -- Create a CoAxiom, with the correct src location. It is Vitally
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
715
716
717
718
719
720
         -- Important that we do not pass the branches into
         -- newFamInstAxiomName. They have types that have been zonked inside
         -- the knot and we will die if we look at them. This is OK here
         -- because there will only be one axiom, so we don't need to
         -- differentiate names.
         -- See [Zonking inside the knot] in TcHsType
721
       ; loc <- getSrcSpanM
722
       ; co_ax_name <- newFamInstAxiomName loc tc_name []
723

724
       ; let mb_co_ax
Jan Stolarek's avatar
Jan Stolarek committed
725
726
727
728
729
730
              | null eqns = Nothing   -- mkBranchedCoAxiom fails on empty list
              | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches)

             fam_tc = buildFamilyTyCon tc_name tvs' (resultVariableName sig)
                      (ClosedSynFamilyTyCon mb_co_ax) kind parent inj'

731
       ; return fam_tc } }
732
733

-- We check for instance validity later, when doing validity checking for
Jan Stolarek's avatar
Jan Stolarek committed
734
-- the tycon. Exception: checking equations overlap done by dropDominatedAxioms
735
736

tcFamDecl1 parent
737
738
739
           (FamilyDecl { fdInfo = DataFamily
                       , fdLName = L _ tc_name, fdTyVars = tvs
                       , fdResultSig = L _ sig })
740
741
742
743
  = tcTyClTyVars tc_name tvs $ \ tvs' kind -> do
  { traceTc "data family:" (ppr tc_name)
  ; checkFamFlag tc_name
  ; extra_tvs <- tcDataKindSig kind
744
  ; tc_rep_name <- newTyConRepName tc_name
745
  ; let final_tvs = tvs' ++ extra_tvs    -- we may not need these
746
747
748
749
750
751
        tycon = buildFamilyTyCon tc_name final_tvs
                                 (resultVariableName sig)
                                 (DataFamilyTyCon tc_rep_name)
                                 liftedTypeKind -- RHS kind
                                 parent
                                 NotInjective
752
  ; return tycon }
753

Jan Stolarek's avatar
Jan Stolarek committed
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
-- | Maybe return a list of Bools that say whether a type family was declared
-- injective in the corresponding type arguments. Length of the list is equal to
-- the number of arguments (including implicit kind arguments). True on position
-- N means that a function is injective in its Nth argument. False means it is
-- not.
tcInjectivity :: [TyVar] -> Maybe (LInjectivityAnn Name)
              -> TcM Injectivity
tcInjectivity _ Nothing
  = return NotInjective

  -- User provided an injectivity annotation, so for each tyvar argument we
  -- check whether a type family was declared injective in that argument. We
  -- return a list of Bools, where True means that corresponding type variable
  -- was mentioned in lInjNames (type family is injective in that argument) and
  -- False means that it was not mentioned in lInjNames (type family is not
  -- injective in that type variable). We also extend injectivity information to
  -- kind variables, so if a user declares:
  --
  --   type family F (a :: k1) (b :: k2) = (r :: k3) | r -> a
  --
  -- then we mark both `a` and `k1` as injective.
  -- NB: the return kind is considered to be *input* argument to a type family.
  -- Since injectivity allows to infer input arguments from the result in theory
  -- we should always mark the result kind variable (`k3` in this example) as
  -- injective.  The reason is that result type has always an assigned kind and
  -- therefore we can always infer the result kind if we know the result type.
  -- But this does not seem to be useful in any way so we don't do it.  (Another
  -- reason is that the implementation would not be straightforward.)
tcInjectivity tvs (Just (L loc (InjectivityAnn _ lInjNames)))
  = setSrcSpan loc $
    do { inj_tvs <- mapM tcFdTyVar lInjNames
       ; let inj_ktvs = closeOverKinds (mkVarSet inj_tvs)
       ; let inj_bools = map (`elemVarSet` inj_ktvs) tvs
       ; traceTc "tcInjectivity" (vcat [ ppr tvs, ppr lInjNames, ppr inj_tvs
                                       , ppr inj_ktvs, ppr inj_bools ])
       ; return $ Injective inj_bools }

791
792
tcTySynRhs :: RecTyInfo
           -> Name
793
           -> [TyVar] -> Kind
794
           -> LHsType Name -> TcM TyCon
795
tcTySynRhs rec_info tc_name tvs kind hs_ty
796
797
798
799
  = do { env <- getLclEnv
       ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
       ; rhs_ty <- tcCheckLHsType hs_ty kind
       ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
800
       ; let roles = rti_roles rec_info tc_name
Jan Stolarek's avatar
Jan Stolarek committed
801
             tycon = buildSynonymTyCon tc_name tvs roles rhs_ty kind
802
       ; return tycon }
803

804
tcDataDefn :: RecTyInfo -> Name
805
           -> [TyVar] -> Kind
806
           -> HsDataDefn Name -> TcM TyCon
807
  -- NB: not used for newtype/data instances (whether associated or not)
808
809
810
811
812
tcDataDefn rec_info          -- Knot-tied; don't look at this eagerly
           tc_name tvs kind
           (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
                       , dd_ctxt = ctxt, dd_kindSig = mb_ksig
                       , dd_cons = cons' })
813
814
 = let cons = cons' -- AZ List monad coming
   in do { extra_tvs <- tcDataKindSig kind
815
       ; let final_tvs  = tvs ++ extra_tvs
816
             roles      = rti_roles rec_info tc_name
817
             is_prom    = rti_promotable rec_info  -- Knot-tied
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
818
819
       ; stupid_tc_theta <- tcHsContext ctxt
       ; stupid_theta    <- zonkTcTypeToTypes emptyZonkEnv stupid_tc_theta
820
       ; kind_signatures <- xoptM Opt_KindSignatures
821
       ; is_boot         <- tcIsHsBootOrSig -- Are we compiling an hs-boot file?
822
823

             -- Check that we don't use kind signatures without Glasgow extensions
824
825
826
827
       ; case mb_ksig of
           Nothing   -> return ()
           Just hs_k -> do { checkTc (kind_signatures) (badSigTyDecl tc_name)
                           ; tc_kind <- tcLHsKind hs_k
828
                           ; checkKind kind tc_kind
829
                           ; return () }
830

831
       ; gadt_syntax <- dataDeclChecks tc_name new_or_data stupid_theta cons
832
833
834

       ; tycon <- fixM $ \ tycon -> do
             { let res_ty = mkTyConApp tycon (mkTyVarTys final_tvs)
835
836
837
             ; data_cons <- tcConDecls new_or_data is_prom tycon (final_tvs, res_ty) cons
             ; tc_rhs    <- mk_tc_rhs is_boot tycon data_cons
             ; tc_rep_nm <- newTyConRepName tc_name
838
839
             ; return (buildAlgTyCon tc_name final_tvs roles (fmap unLoc cType)
                                     stupid_theta tc_rhs
840
                                     (rti_is_rec rec_info tc_name)
841
842
843
                                     is_prom
                                     gadt_syntax
                                     (VanillaAlgTyCon tc_rep_nm)) }
844
       ; return tycon }
845
846
847
848
849
850
851
852
853
  where
    mk_tc_rhs is_boot tycon data_cons
      | null data_cons, is_boot         -- In a hs-boot file, empty cons means
      = return totallyAbstractTyConRhs  -- "don't know"; hence totally Abstract
      | otherwise
      = case new_or_data of
          DataType -> return (mkDataTyConRhs data_cons)
          NewType  -> ASSERT( not (null data_cons) )
                      mkNewTyConRhs tc_name tycon (head data_cons)
854

Austin Seipp's avatar
Austin Seipp committed
855
856
857
{-
************************************************************************
*                                                                      *
858
               Typechecking associated types (in class decls)
859
               (including the associated-type defaults)
Austin Seipp's avatar
Austin Seipp committed
860
861
*                                                                      *
************************************************************************
862

dreixel's avatar
dreixel committed
863
864
865
866
867
Note [Associated type defaults]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

The following is an example of associated type defaults:
             class C a where
868
               data D a
869
870

               type F a b :: *
Jan Stolarek's avatar
Jan Stolarek committed
871
               type F a b = [a]        -- Default
872

Jan Stolarek's avatar
Jan Stolarek committed
873
874
Note that we can get default definitions only for type families, not data
families.
Austin Seipp's avatar
Austin Seipp committed
875
-}
dreixel's avatar
dreixel committed
876

877
tcClassATs :: Name                  -- The class name (not knot-tied)
878
           -> Class                 -- The class parent of this associated type
879
880
           -> [LFamilyDecl Name]    -- Associated types.
           -> [LTyFamDefltEqn Name] -- Associated type defaults.
881
           -> TcM [ClassATItem]
882
tcClassATs class_name cls ats at_defs
883
  = do {  -- Complain about associated type defaults for non associated-types
dreixel's avatar
dreixel committed
884
         sequence_ [ failWithTc (badATErr class_name n)
885
                   | n <- map at_def_tycon at_defs
886
887
                   , not (n `elemNameSet` at_names) ]
       ; mapM tc_at ats }
888
  where
889
890
891
892
893
894
895
    at_def_tycon :: LTyFamDefltEqn Name -> Name
    at_def_tycon (L _ eqn) = unLoc (tfe_tycon eqn)

    at_fam_name :: LFamilyDecl Name -> Name
    at_fam_name (L _ decl) = unLoc (fdLName decl)

    at_names = mkNameSet (map at_fam_name ats)
896

897
    at_defs_map :: NameEnv [LTyFamDefltEqn Name]
898
    -- Maps an AT in 'ats' to a list of all its default defs in 'at_defs'