TcTyClsDecls.hs 97.2 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, tcAddDataFamInstCtxt,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
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
import TcSimplify( growThetaTyVars )
32
import TcBinds( tcRecSelBinds )
33
34
35
36
37
import TcTyDecls
import TcClassDcl
import TcHsType
import TcMType
import TcType
38
import TysWiredIn( unitTy )
39
import FamInst
40
import FamInstEnv( isDominatedBy, mkCoAxBranch, mkBranchedCoAxiom )
41
import Coercion( pprCoAxBranch, ltRole )
42
import Type
43
import TypeRep   -- for checkValidRoles
dreixel's avatar
dreixel committed
44
import Kind
45
import Class
46
import CoAxiom
47
48
import TyCon
import DataCon
49
import Id
50
import MkCore           ( rEC_SEL_ERROR_ID )
51
import IdInfo
52
import Var
53
import VarEnv
54
import VarSet
55
import Module
56
import Name
57
import NameSet
58
import NameEnv
sof's avatar
sof committed
59
import Outputable
60
61
62
63
64
65
66
import Maybes
import Unify
import Util
import SrcLoc
import ListSetOps
import Digraph
import DynFlags
67
import FastString
68
import Unique           ( mkBuiltinUnique )
69
import BasicTypes
70

71
import Bag
Ian Lynagh's avatar
Ian Lynagh committed
72
import Control.Monad
73
import Data.List
74

Austin Seipp's avatar
Austin Seipp committed
75
76
77
{-
************************************************************************
*                                                                      *
78
\subsection{Type checking for type and class declarations}
Austin Seipp's avatar
Austin Seipp committed
79
80
*                                                                      *
************************************************************************
81

dreixel's avatar
dreixel committed
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
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 *.

100
101
102
103
104
105
106
107
108
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
109
-}
110

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

tcTyClGroup :: ModDetails -> TyClGroup Name -> TcM TcGblEnv
-- Typecheck one strongly-connected component of type and class decls
tcTyClGroup boot_details tyclds
  = 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]
134
         names_w_poly_kinds <- kcTyClGroup tyclds
dreixel's avatar
dreixel committed
135
136
       ; traceTc "tcTyAndCl generalized kinds" (ppr names_w_poly_kinds)

137
138
            -- Step 2: type-check all groups together, returning
            -- the final TyCons and Classes
139
140
       ; let role_annots = extractRoleAnnots tyclds
             decls = group_tyclds tyclds
dreixel's avatar
dreixel committed
141
       ; tyclss <- fixM $ \ rec_tyclss -> do
142
           { is_boot <- tcIsHsBootOrSig
143
144
           ; let rec_flags = calcRecFlags boot_details is_boot
                                          role_annots rec_tyclss
dreixel's avatar
dreixel committed
145
146
147

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

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

                 -- Kind and type check declarations for this group
158
             concatMapM (tcTyClDecl rec_flags) decls }
dreixel's avatar
dreixel committed
159

160
           -- Step 3: Perform the validity check
dreixel's avatar
dreixel committed
161
162
163
           -- 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
164
       ; tcExtendGlobalEnv tyclss $ do
dreixel's avatar
dreixel committed
165
       { traceTc "Starting validity check" (ppr tyclss)
166
167
       ; checkNoErrs $
         mapM_ (recoverM (return ()) . checkValidTyCl) tyclss
168
           -- We recover, which allows us to report multiple validity errors
169
170
171
           -- the checkNoErrs is necessary to fix #7175.
       ; mapM_ (recoverM (return ()) . checkValidRoleAnnots role_annots) tyclss
           -- See Note [Check role annotations in a second pass]
dreixel's avatar
dreixel committed
172
173
174
175

           -- Step 4: Add the implicit things;
           -- we want them in the environment because
           -- they may be mentioned in interface files
176
177
178
179
180
       ; tcExtendGlobalValEnv (mkDefaultMethodIds tyclss) $
         tcAddImplicits tyclss } }

tcAddImplicits :: [TyThing] -> TcM TcGblEnv
tcAddImplicits tyclss
181
 = tcExtendGlobalEnvImplicit implicit_things $
182
183
184
185
   tcRecSelBinds rec_sel_binds
 where
   implicit_things = concatMap implicitTyThings tyclss
   rec_sel_binds   = mkRecSelBinds tyclss
dreixel's avatar
dreixel committed
186

187
zipRecTyClss :: [(Name, Kind)]
188
189
190
191
             -> [TyThing]           -- Knot-tied
             -> [(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
192
-- The TyThings in the result list must have a visible ATyCon,
193
-- because typechecking types (in, say, tcTyClDecl) looks at this outer constructor
194
195
zipRecTyClss kind_pairs rec_things
  = [ (name, ATyCon (get name)) | (name, _kind) <- kind_pairs ]
196
  where
197
198
199
    rec_type_env :: TypeEnv
    rec_type_env = mkTypeEnv rec_things

dreixel's avatar
dreixel committed
200
201
202
    get name = case lookupTypeEnv rec_type_env name of
                 Just (ATyCon tc) -> tc
                 other            -> pprPanic "zipRecTyClss" (ppr name <+> ppr other)
203

Austin Seipp's avatar
Austin Seipp committed
204
205
206
{-
************************************************************************
*                                                                      *
207
                Kind checking
Austin Seipp's avatar
Austin Seipp committed
208
209
*                                                                      *
************************************************************************
210

211
212
213
214
Note [Kind checking for type and class decls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Kind checking is done thus:

215
216
217
   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)
218
219
220
221
222
223
224
225

   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

Synonyms are treated differently to data type and classes,
because a type synonym can be an unboxed type
226
        type Foo = Int#
227
228
229
and a kind variable can't unify with UnboxedTypeKind
So we infer their kinds in dependency order

230
231
We need to kind check all types in the mutually recursive group
before we know the kind of the type variables.  For example:
232

233
234
  class C a where
     op :: D b => a -> b -> b
235

236
237
  class D c where
     bop :: (Monad c) => ...
238
239
240
241
242

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.

243
244
However type synonyms work differently.  They can have kinds which don't
just involve (->) and *:
245
246
247
        type R = Int#           -- Kind #
        type S a = Array# a     -- Kind * -> #
        type T a b = (# a,b #)  -- Kind * -> * -> (# a,b #)
248
249
250
So we must infer their kinds 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.
251

252
253
Open type families
~~~~~~~~~~~~~~~~~~
254
255
256
This treatment of type synonyms only applies to Haskell 98-style synonyms.
General type functions can be recursive, and hence, appear in `alg_decls'.

257
The kind of an open type family is solely determinded by its kind signature;
258
hence, only kind signatures participate in the construction of the initial
259
260
261
262
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
263
-}
264

265
kcTyClGroup :: TyClGroup Name -> TcM [(Name,Kind)]
dreixel's avatar
dreixel committed
266
-- Kind check this group, kind generalize, and return the resulting local env
267
-- This bindds the TyCons and Classes of the group, but not the DataCons
dreixel's avatar
dreixel committed
268
-- See Note [Kind checking for type and class decls]
269
kcTyClGroup (TyClGroup { group_tyclds = decls })
270
271
  = do  { mod <- getModule
        ; traceTc "kcTyClGroup" (ptext (sLit "module") <+> ppr mod $$ vcat (map ppr decls))
dreixel's avatar
dreixel committed
272

273
274
          -- Kind checking;
          --    1. Bind kind variables for non-synonyms
dreixel's avatar
dreixel committed
275
276
          --    2. Kind-check synonyms, and bind kinds of those synonyms
          --    3. Kind-check non-synonyms
277
          --    4. Generalise the inferred kinds
dreixel's avatar
dreixel committed
278
279
          -- See Note [Kind checking for type and class decls]

280
          -- Step 1: Bind kind variables for non-synonyms
dreixel's avatar
dreixel committed
281
        ; let (syn_decls, non_syn_decls) = partition (isSynDecl . unLoc) decls
282
        ; initial_kinds <- getInitialKinds non_syn_decls
283
        ; traceTc "kcTyClGroup: initial kinds" (ppr initial_kinds)
284
285

        -- Step 2: Set initial envt, kind-check the synonyms
286
        ; lcl_env <- tcExtendKindEnv2 initial_kinds $
287
                     kcSynDecls (calcSynCycles syn_decls)
288
289
290
291

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

293
294
             -- Step 4: generalisation
             -- Kind checking done for this group
dreixel's avatar
dreixel committed
295
             -- Now we have to kind generalize the flexis
296
        ; res <- concatMapM (generaliseTCD (tcl_env lcl_env)) decls
297
298

        ; traceTc "kcTyClGroup result" (ppr res)
299
        ; return res }
300

301
  where
302
    generalise :: TcTypeEnv -> Name -> TcM (Name, Kind)
303
    -- For polymorphic things this is a no-op
304
    generalise kind_env name
305
      = do { let kc_kind = case lookupNameEnv kind_env name of
306
307
                               Just (AThing k) -> k
                               _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env)
308
           ; kvs <- kindGeneralize (tyVarsOfType kc_kind)
309
310
311
           ; 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
312
313
           ; return (name, mkForAllTys kvs kc_kind') }

314
315
    generaliseTCD :: TcTypeEnv -> LTyClDecl Name -> TcM [(Name, Kind)]
    generaliseTCD kind_env (L _ decl)
316
317
      | ClassDecl { tcdLName = (L _ name), tcdATs = ats } <- decl
      = do { first <- generalise kind_env name
318
319
320
321
322
323
324
325
           ; rest <- mapM ((generaliseFamDecl kind_env) . unLoc) ats
           ; return (first : rest) }

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

      | otherwise
326
      = do { res <- generalise kind_env (tcdName decl)
327
328
329
           ; return [res] }

    generaliseFamDecl :: TcTypeEnv -> FamilyDecl Name -> TcM (Name, Kind)
330
331
    generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name })
      = generalise kind_env name
332

333
334
335
336
337
338
339
340
341
342
343
344
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)

345
getInitialKinds :: [LTyClDecl Name] -> TcM [(Name, TcTyThing)]
346
getInitialKinds decls
347
  = tcExtendKindEnv2 (mk_thing_env decls) $
348
349
    do { pairss <- mapM (addLocM getInitialKind) decls
       ; return (concat pairss) }
350

351
getInitialKind :: TyClDecl Name -> TcM [(Name, TcTyThing)]
dreixel's avatar
dreixel committed
352
353
354
355
356
357
-- 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 = ...
358
--      return (T, kv1 -> kv2 -> kv3)
dreixel's avatar
dreixel committed
359
--
360
361
362
363
364
365
-- 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]
366
--
367
-- No family instances are passed to getInitialKinds
dreixel's avatar
dreixel committed
368

369
getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
370
  = do { (cl_kind, inner_prs) <-
371
           kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $
372
373
374
           do { inner_prs <- getFamDeclInitialKinds ats
              ; return (constraintKind, inner_prs) }
       ; let main_pr = (name, AThing cl_kind)
375
       ; return (main_pr : inner_prs) }
376

377
getInitialKind decl@(DataDecl { tcdLName = L _ name
378
379
380
381
382
383
                              , tcdTyVars = ktvs
                              , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
                                                         , dd_cons = cons' } })
  = let cons = cons' -- AZ list monad coming
    in
     do { (decl_kind, _) <-
384
           kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $
385
386
387
           do { res_k <- case m_sig of
                           Just ksig -> tcLHsKind ksig
                           Nothing   -> return liftedTypeKind
388
              ; return (res_k, ()) }
389
       ; let main_pr = (name, AThing decl_kind)
390
391
             inner_prs = [ (unLoc con, APromotionErr RecDataConPE)
                         | L _ con' <- cons, con <- con_names con' ]
392
       ; return (main_pr : inner_prs) }
393

Jan Stolarek's avatar
Jan Stolarek committed
394
getInitialKind (FamDecl { tcdFam = decl })
395
  = getFamDeclInitialKind decl
396

Jan Stolarek's avatar
Jan Stolarek committed
397
getInitialKind decl@(SynDecl {})
398
399
400
  = pprPanic "getInitialKind" (ppr decl)

---------------------------------
401
402
getFamDeclInitialKinds :: [LFamilyDecl Name] -> TcM [(Name, TcTyThing)]
getFamDeclInitialKinds decls
403
404
  = tcExtendKindEnv2 [ (n, APromotionErr TyConPE)
                     | L _ (FamilyDecl { fdLName = L _ n }) <- decls] $
405
    concatMapM (addLocM getFamDeclInitialKind) decls
406

407
getFamDeclInitialKind :: FamilyDecl Name
408
                      -> TcM [(Name, TcTyThing)]
409
410
411
getFamDeclInitialKind decl@(FamilyDecl { fdLName = L _ name
                                       , fdTyVars = ktvs
                                       , fdKindSig = ksig })
412
  = do { (fam_kind, _) <-
413
           kcHsTyVarBndrs (famDeclHasCusk decl) ktvs $
414
415
416
           do { res_k <- case ksig of
                           Just k  -> tcLHsKind k
                           Nothing
417
418
                             | famDeclHasCusk decl -> return liftedTypeKind
                             | otherwise           -> newMetaKindVar
419
420
              ; return (res_k, ()) }
       ; return [ (name, AThing fam_kind) ] }
421

422
----------------
423
kcSynDecls :: [SCC (LTyClDecl Name)]
424
425
           -> TcM TcLclEnv -- Kind bindings
kcSynDecls [] = getLclEnv
426
kcSynDecls (group : groups)
427
428
429
  = do  { (n,k) <- kcSynDecl1 group
        ; lcl_env <- tcExtendKindEnv [(n,k)] (kcSynDecls groups)
        ; return lcl_env }
dreixel's avatar
dreixel committed
430
431

kcSynDecl1 :: SCC (LTyClDecl Name)
432
           -> TcM (Name,TcKind) -- Kind bindings
dreixel's avatar
dreixel committed
433
434
kcSynDecl1 (AcyclicSCC (L _ decl)) = kcSynDecl decl
kcSynDecl1 (CyclicSCC decls)       = do { recSynErr decls; failM }
435
436
                                     -- Fail here to avoid error cascade
                                     -- of out-of-scope tycons
dreixel's avatar
dreixel committed
437

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

452
------------------------------------------------------------------------
453
kcLTyClDecl :: LTyClDecl Name -> TcM ()
454
  -- See Note [Kind checking for type and class decls]
455
456
457
kcLTyClDecl (L loc decl)
  = setSrcSpan loc $ tcAddDeclCtxt decl $ kcTyClDecl decl

dreixel's avatar
dreixel committed
458
459
kcTyClDecl :: TyClDecl Name -> TcM ()
-- This function is used solely for its side effect on kind variables
460
-- NB kind signatures on the type variables and
461
462
--    result kind signature have aready been dealt with
--    by getInitialKind, so we can ignore them here.
dreixel's avatar
dreixel committed
463

464
465
kcTyClDecl (DataDecl { tcdLName = L _ name, tcdTyVars = hs_tvs, tcdDataDefn = defn })
  | HsDataDefn { dd_cons = cons, dd_kindSig = Just _ } <- defn
466
  = mapM_ (wrapLocM kcConDecl) cons
467
468
469
470
471
472
    -- 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
473

474
475
  | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
  = kcTyClTyVars name hs_tvs $
476
    do  { _ <- tcHsContext ctxt
477
        ; mapM_ (wrapLocM kcConDecl) cons }
478

479
kcTyClDecl decl@(SynDecl {}) = pprPanic "kcTyClDecl" (ppr decl)
480
481

kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs
482
483
                       , tcdCtxt = ctxt, tcdSigs = sigs })
  = kcTyClTyVars name hs_tvs $
484
485
    do  { _ <- tcHsContext ctxt
        ; mapM_ (wrapLocM kc_sig)     sigs }
dreixel's avatar
dreixel committed
486
  where
thomasw's avatar
thomasw committed
487
    kc_sig (TypeSig _ op_ty _)  = discardResult (tcHsLiftedType op_ty)
488
    kc_sig (GenericSig _ op_ty) = discardResult (tcHsLiftedType op_ty)
dreixel's avatar
dreixel committed
489
    kc_sig _                    = return ()
490

491
492
-- closed type families look at their equations, but other families don't
-- do anything here
493
494
495
496
497
498
kcTyClDecl (FamDecl (FamilyDecl { fdLName  = L _ fam_tc_name
                                , fdTyVars = hs_tvs
                                , fdInfo   = ClosedTypeFamily eqns }))
  = 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 }
499
kcTyClDecl (FamDecl {})    = return ()
dreixel's avatar
dreixel committed
500
501

-------------------
502
kcConDecl :: ConDecl Name -> TcM ()
503
kcConDecl (ConDecl { con_names = names, con_qvars = ex_tvs
504
505
                   , con_cxt = ex_ctxt, con_details = details
                   , con_res = res })
506
  = addErrCtxt (dataConCtxtName names) $
507
508
509
510
         -- 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 $
511
512
              do { _ <- tcHsContext ex_ctxt
                 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details)
513
                 ; _ <- tcConRes res
514
                 ; return (panic "kcConDecl", ()) }
515
       ; return () }
516

Austin Seipp's avatar
Austin Seipp committed
517
{-
518
519
Note [Recursion and promoting data constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
520
521
522
523
524
525
526
527
528
529
530
531
532
533
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.

534

Austin Seipp's avatar
Austin Seipp committed
535
536
************************************************************************
*                                                                      *
537
\subsection{Type checking}
Austin Seipp's avatar
Austin Seipp committed
538
539
*                                                                      *
************************************************************************
540

dreixel's avatar
dreixel committed
541
542
543
544
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,
545
we discarded the kind-checked types (eg RHSs of data type decls);
dreixel's avatar
dreixel committed
546
547
548
549
550
551
552
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
553
    to be given kind arguments.
dreixel's avatar
dreixel committed
554
555
556
557
558
559
560

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).
561

dreixel's avatar
dreixel committed
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
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.

This fancy footwork (with two bindings for T) is only necesary for the
TyCons or Classes of this recursive group.  Earlier, finished groups,
live in the global env only.
Austin Seipp's avatar
Austin Seipp committed
584
-}
dreixel's avatar
dreixel committed
585

586
587
tcTyClDecl :: RecTyInfo -> LTyClDecl Name -> TcM [TyThing]
tcTyClDecl rec_info (L loc decl)
588
  = setSrcSpan loc $ tcAddDeclCtxt decl $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
589
    traceTc "tcTyAndCl-x" (ppr decl) >>
590
    tcTyClDecl1 NoParentTyCon rec_info decl
591

592
  -- "type family" declarations
593
594
tcTyClDecl1 :: TyConParent -> RecTyInfo -> TyClDecl Name -> TcM [TyThing]
tcTyClDecl1 parent _rec_info (FamDecl { tcdFam = fd })
595
  = tcFamDecl1 parent fd
596

597
  -- "type" synonym declaration
598
tcTyClDecl1 _parent rec_info
599
600
            (SynDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdRhs = rhs })
  = ASSERT( isNoParent _parent )
601
    tcTyClTyVars tc_name tvs $ \ tvs' kind ->
602
    tcTySynRhs rec_info tc_name tvs' kind rhs
603

604
  -- "data/newtype" declaration
605
tcTyClDecl1 _parent rec_info
606
            (DataDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdDataDefn = defn })
607
  = ASSERT( isNoParent _parent )
608
    tcTyClTyVars tc_name tvs $ \ tvs' kind ->
609
    tcDataDefn rec_info tc_name tvs' kind defn
610

611
tcTyClDecl1 _parent rec_info
dreixel's avatar
dreixel committed
612
            (ClassDecl { tcdLName = L _ class_name, tcdTyVars = tvs
613
            , tcdCtxt = ctxt, tcdMeths = meths
614
            , tcdFDs = fundeps, tcdSigs = sigs
615
            , tcdATs = ats, tcdATDefs = at_defs })
616
  = ASSERT( isNoParent _parent )
617
    do { (clas, tvs', gen_dm_env) <- fixM $ \ ~(clas,_,_) ->
618
            tcTyClTyVars class_name tvs $ \ tvs' kind ->
619
            do { MASSERT( isConstraintKind kind )
620
621
622
623
624
625
                 -- 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
               ; 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
626

627
               ; ctxt' <- tcHsContext ctxt
628
               ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'
629
630
631
632
                       -- Squeeze out any kind unification variables
               ; fds'  <- mapM (addLocM tc_fundep) fundeps
               ; (sig_stuff, gen_dm_env) <- tcClassSigs class_name sigs meths
               ; at_stuff <- tcClassATs class_name (AssocFamilyTyCon clas) ats at_defs
633
               ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
634
               ; clas <- buildClass
635
                            class_name tvs' roles ctxt' fds' at_stuff
636
                            sig_stuff mindef tc_isrec
637
638
639
               ; traceTc "tcClassDecl" (ppr fundeps $$ ppr tvs' $$ ppr fds')
               ; return (clas, tvs', gen_dm_env) }

640
       ; let { gen_dm_ids = [ AnId (mkExportedLocalId VanillaId gen_dm_name gen_dm_ty)
641
                            | (sel_id, GenDefMeth gen_dm_name) <- classOpItems clas
642
643
644
645
646
647
                            , let gen_dm_tau = expectJust "tcTyClDecl1" $
                                               lookupNameEnv gen_dm_env (idName sel_id)
                            , let gen_dm_ty = mkSigmaTy tvs'
                                                      [mkClassPred clas (mkTyVarTys tvs')]
                                                      gen_dm_tau
                            ]
648
649
650
651
652
             ; class_ats = map ATyCon (classATs clas) }

       ; return (ATyCon (classTyCon clas) : gen_dm_ids ++ class_ats ) }
         -- NB: Order is important due to the call to `mkGlobalThings' when
         --     tying the the type and class declaration type checking knot.
653
  where
654
    tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM tc_fd_tyvar tvs1 ;
655
656
                                ; tvs2' <- mapM tc_fd_tyvar tvs2 ;
                                ; return (tvs1', tvs2') }
657
658
659
660
661
662
663
664
    tc_fd_tyvar name   -- Scoped kind variables are bound to unification variables
                       -- which are now fixed, so we can zonk
      = do { tv <- tcLookupTyVar name
           ; ty <- zonkTyVarOcc emptyZonkEnv tv
                  -- Squeeze out any kind unification variables
           ; case getTyVar_maybe ty of
               Just tv' -> return tv'
               Nothing  -> pprPanic "tc_fd_tyvar" (ppr name $$ ppr tv $$ ppr ty) }
665

666
667
tcFamDecl1 :: TyConParent -> FamilyDecl Name -> TcM [TyThing]
tcFamDecl1 parent
668
            (FamilyDecl {fdInfo = OpenTypeFamily, fdLName = L _ tc_name, fdTyVars = tvs})
669
  = tcTyClTyVars tc_name tvs $ \ tvs' kind -> do
670
  { traceTc "open type family:" (ppr tc_name)
671
  ; checkFamFlag tc_name
672
  ; tycon <- buildFamilyTyCon tc_name tvs' OpenSynFamilyTyCon kind parent
673
674
675
  ; return [ATyCon tycon] }

tcFamDecl1 parent
676
677
678
679
            (FamilyDecl { fdInfo = ClosedTypeFamily eqns
                        , fdLName = lname@(L _ tc_name), fdTyVars = tvs })
-- Closed type families are a little tricky, because they contain the definition
-- of both the type family and the equations for a CoAxiom.
680
-- Note: eqns might be empty, in a hs-boot file!
681
682
683
684
685
686
687
  = do { traceTc "closed type family:" (ppr tc_name)
         -- the variables in the header have no scope:
       ; (tvs', kind) <- tcTyClTyVars tc_name tvs $ \ tvs' kind ->
                         return (tvs', kind)

       ; checkFamFlag tc_name -- make sure we have -XTypeFamilies

688
689
         -- Process the equations, creating CoAxBranches
       ; tc_kind <- kcLookupKind tc_name
Jan Stolarek's avatar
Jan Stolarek committed
690
691
       ; let fam_tc_shape = (tc_name, length (hsQTvBndrs tvs), tc_kind)

692
       ; branches <- mapM (tcTyFamInstEqn fam_tc_shape) eqns
693
694
695
696
697

         -- we need the tycon that we will be creating, but it's in scope.
         -- just look it up.
       ; fam_tc <- tcLookupLocatedTyCon lname

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
698
699
700
701
702
703
704
         -- create a CoAxiom, with the correct src location. It is Vitally
         -- 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
705
       ; loc <- getSrcSpanM
706
       ; co_ax_name <- newFamInstAxiomName loc tc_name []
707
708
709

         -- mkBranchedCoAxiom will fail on an empty list of branches, but
         -- we'll never look at co_ax in this case
710
711
712
       ; let co_ax = mkBranchedCoAxiom co_ax_name fam_tc branches

         -- now, finally, build the TyCon
713
714
715
       ; let syn_rhs = if null eqns
                       then AbstractClosedSynFamilyTyCon
                       else ClosedSynFamilyTyCon co_ax
716
       ; tycon <- buildFamilyTyCon tc_name tvs' syn_rhs kind parent
717

718
719
720
721
       ; let result = if null eqns
                      then [ATyCon tycon]
                      else [ATyCon tycon, ACoAxiom co_ax]
       ; return result }
722
723
724
725
726
-- We check for instance validity later, when doing validity checking for
-- the tycon

tcFamDecl1 parent
           (FamilyDecl {fdInfo = DataFamily, fdLName = L _ tc_name, fdTyVars = tvs})
727
728
729
730
731
  = tcTyClTyVars tc_name tvs $ \ tvs' kind -> do
  { traceTc "data family:" (ppr tc_name)
  ; checkFamFlag tc_name
  ; extra_tvs <- tcDataKindSig kind
  ; let final_tvs = tvs' ++ extra_tvs    -- we may not need these
732
733
        roles     = map (const Nominal) final_tvs
        tycon = buildAlgTyCon tc_name final_tvs roles Nothing []
734
                              DataFamilyTyCon Recursive
735
736
737
                              False   -- Not promotable to the kind level
                              True    -- GADT syntax
                              parent
738
739
  ; return [ATyCon tycon] }

740
741
tcTySynRhs :: RecTyInfo
           -> Name
742
743
           -> [TyVar] -> Kind
           -> LHsType Name -> TcM [TyThing]
744
tcTySynRhs rec_info tc_name tvs kind hs_ty
745
746
747
748
  = 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
749
       ; let roles = rti_roles rec_info tc_name
750
       ; tycon <- buildSynonymTyCon tc_name tvs roles rhs_ty kind
751
752
       ; return [ATyCon tycon] }

753
tcDataDefn :: RecTyInfo -> Name
754
755
756
           -> [TyVar] -> Kind
           -> HsDataDefn Name -> TcM [TyThing]
  -- NB: not used for newtype/data instances (whether associated or not)
757
tcDataDefn rec_info tc_name tvs kind
758
759
         (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
                     , dd_ctxt = ctxt, dd_kindSig = mb_ksig
760
761
762
                     , dd_cons = cons' })
 = let cons = cons' -- AZ List monad coming
   in do { extra_tvs <- tcDataKindSig kind
763
       ; let final_tvs  = tvs ++ extra_tvs
764
             roles      = rti_roles rec_info tc_name
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
765
766
       ; stupid_tc_theta <- tcHsContext ctxt
       ; stupid_theta    <- zonkTcTypeToTypes emptyZonkEnv stupid_tc_theta
767
       ; kind_signatures <- xoptM Opt_KindSignatures
768
       ; is_boot         <- tcIsHsBootOrSig -- Are we compiling an hs-boot file?
769
770

             -- Check that we don't use kind signatures without Glasgow extensions
771
772
773
774
       ; case mb_ksig of
           Nothing   -> return ()
           Just hs_k -> do { checkTc (kind_signatures) (badSigTyDecl tc_name)
                           ; tc_kind <- tcLHsKind hs_k
775
                           ; checkKind kind tc_kind
776
                           ; return () }
777

778
       ; gadt_syntax <- dataDeclChecks tc_name new_or_data stupid_theta cons
779
780
781

       ; tycon <- fixM $ \ tycon -> do
             { let res_ty = mkTyConApp tycon (mkTyVarTys final_tvs)
782
             ; data_cons <- tcConDecls new_or_data tycon (final_tvs, res_ty) cons
783
             ; tc_rhs <-
784
                 if null cons && is_boot              -- In a hs-boot file, empty cons means
785
786
                 then return totallyAbstractTyConRhs  -- "don't know"; hence totally Abstract
                 else case new_or_data of
787
788
                   DataType -> return (mkDataTyConRhs data_cons)
                   NewType  -> ASSERT( not (null data_cons) )
789
                                    mkNewTyConRhs tc_name tycon (head data_cons)
790
791
             ; return (buildAlgTyCon tc_name final_tvs roles (fmap unLoc cType)
                                     stupid_theta tc_rhs
792
793
                                     (rti_is_rec rec_info tc_name)
                                     (rti_promotable rec_info)
794
                                     gadt_syntax NoParentTyCon) }
795
796
       ; return [ATyCon tycon] }

Austin Seipp's avatar
Austin Seipp committed
797
798
799
{-
************************************************************************
*                                                                      *
800
               Typechecking associated types (in class decls)
801
               (including the associated-type defaults)
Austin Seipp's avatar
Austin Seipp committed
802
803
*                                                                      *
************************************************************************
804

dreixel's avatar
dreixel committed
805
806
807
808
809
Note [Associated type defaults]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

The following is an example of associated type defaults:
             class C a where
810
               data D a
811
812
813
814
815

               type F a b :: *
               type F a Z = [a]        -- Default
               type F a (S n) = F a n  -- Default

dreixel's avatar
dreixel committed
816
817
818
819
Note that:
  - We can have more than one default definition for a single associated type,
    as long as they do not overlap (same rules as for instances)
  - We can get default definitions only for type families, not data families
Austin Seipp's avatar
Austin Seipp committed
820
-}
dreixel's avatar
dreixel committed
821

822
823
824
825
tcClassATs :: Name                  -- The class name (not knot-tied)
           -> TyConParent           -- The class parent of this associated type
           -> [LFamilyDecl Name]    -- Associated types.
           -> [LTyFamDefltEqn Name] -- Associated type defaults.
826
           -> TcM [ClassATItem]
dreixel's avatar
dreixel committed
827
tcClassATs class_name parent ats at_defs
828
  = do {  -- Complain about associated type defaults for non associated-types
dreixel's avatar
dreixel committed
829
         sequence_ [ failWithTc (badATErr class_name n)
830
                   | n <- map at_def_tycon at_defs
831
832
                   , not (n `elemNameSet` at_names) ]
       ; mapM tc_at ats }
833
  where
834
835
836
837
838
839
840
    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)
841

842
    at_defs_map :: NameEnv [LTyFamDefltEqn Name]
843
    -- Maps an AT in 'ats' to a list of all its default defs in 'at_defs'
844
    at_defs_map = foldr (\at_def nenv -> extendNameEnv_C (++) nenv
845
                                          (at_def_tycon at_def) [at_def])
846
                        emptyNameEnv at_defs
847

848
    tc_at at = do { [ATyCon fam_tc] <- addLocM (tcFamDecl1 parent) at
849
850
851
852
                  ; let at_defs = lookupNameEnv at_defs_map (at_fam_name at)
                                  `orElse` []
                  ; atd <- tcDefaultAssocDecl fam_tc at_defs
                  ; return (ATI fam_tc atd) }
853

854
-------------------------
855
856
857
858
859
860
861
tcDefaultAssocDecl :: TyCon                  -- ^ Family TyCon
                   -> [LTyFamDefltEqn Name]  -- ^ Defaults
                   -> TcM (Maybe Type)       -- ^ Type checked RHS
tcDefaultAssocDecl _ []
  = return Nothing  -- No default declaration

tcDefaultAssocDecl _ (d1:_:_)
Jan Stolarek's avatar
Jan Stolarek committed
862
  = failWithTc (ptext (sLit "More than one default declaration for")
863
864
865
866
867
                <+> ppr (tfe_tycon (unLoc d1)))

tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = L _ tc_name
                                           , tfe_pats = hs_tvs
                                           , tfe_rhs = rhs })]
868
  = setSrcSpan loc $
869
870
871
    tcAddFamInstCtxt (ptext (sLit "default type instance")) tc_name $
    tcTyClTyVars tc_name hs_tvs $ \ tvs rhs_kind ->
    do { traceTc "tcDefaultAssocDecl" (ppr tc_name)
872
       ; checkTc (isTypeFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
873
874
875
876
877
878
879
880
881
882
       ; let (fam_name, fam_pat_arity, _) = famTyConShape fam_tc
       ; ASSERT( fam_name == tc_name )
         checkTc (length (hsQTvBndrs hs_tvs) == fam_pat_arity)
                 (wrongNumberOfParmsErr fam_pat_arity)
       ; rhs_ty <- tcCheckLHsType rhs rhs_kind
       ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
       ; let fam_tc_tvs = tyConTyVars fam_tc
             subst = zipTopTvSubst tvs (mkTyVarTys fam_tc_tvs)
       ; return ( ASSERT( equalLength fam_tc_tvs tvs )
                  Just (substTy subst rhs_ty) ) }
883
    -- We check for well-formedness and validity later, in checkValidClass
dreixel's avatar
dreixel committed
884

885
-------------------------
886
887
888
kcTyFamInstEqn :: FamTyConShape -> LTyFamInstEqn Name -> TcM ()
kcTyFamInstEqn fam_tc_shape
    (L loc (TyFamEqn { tfe_pats = pats, tfe_rhs = hs_ty }))
889
890
  = setSrcSpan loc $
    discardResult $
891
892
893
894
895
896
897
898
899
    tc_fam_ty_pats fam_tc_shape pats (discardResult . (tcCheckLHsType hs_ty))

tcTyFamInstEqn :: FamTyConShape -> LTyFamInstEqn Name -> TcM CoAxBranch
-- Needs to be here, not in TcInstDcls, because closed families
-- (typechecked here) have TyFamInstEqns
tcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_)
    (L loc (TyFamEqn { tfe_tycon = L _ eqn_tc_name
                     , tfe_pats = pats
                     , tfe_rhs = hs_ty }))
900
  = setSrcSpan loc $
901
    tcFamTyPats fam_tc_shape pats (discardResult . (tcCheckLHsType hs_ty)) $
902
       \tvs' pats' res_kind ->
Jan Stolarek's avatar
Jan Stolarek committed