TcTyClsDecls.hs 147 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, MultiWayIf #-}
10
{-# LANGUAGE TypeFamilies #-}
Ian Lynagh's avatar
Ian Lynagh committed
11

12
module TcTyClsDecls (
13
        tcTyAndClassDecls, tcAddImplicits,
14

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

23
#include "HsVersions.h"
24

25
26
import GhcPrelude

27
28
29
import HsSyn
import HscTypes
import BuildTyCl
30
import TcRnMonad
31
import TcEnv
32
import TcValidity
33
import TcHsSyn
34
35
import TcTyDecls
import TcClassDcl
36
import {-# SOURCE #-} TcInstDcls( tcInstDecls1 )
37
import TcDeriv (DerivInfo)
38
39
import TcEvidence  ( tcCoercionKind, isEmptyTcEvBinds )
import TcUnify     ( checkConstraints )
40
41
import TcHsType
import TcMType
42
import TysWiredIn ( unitTy )
43
import TcType
44
import RnEnv( lookupConstructorFields )
45
import FamInst
Jan Stolarek's avatar
Jan Stolarek committed
46
import FamInstEnv
47
import Coercion
48
import Type
49
import TyCoRep   -- for checkValidRoles
dreixel's avatar
dreixel committed
50
import Kind
51
import Class
52
import CoAxiom
53
54
import TyCon
import DataCon
55
import Id
56
import Var
57
import VarEnv
58
import VarSet
59
import Module
60
import Name
61
import NameSet
62
import NameEnv
sof's avatar
sof committed
63
import Outputable
64
65
66
import Maybes
import Unify
import Util
67
import Pair
68
69
70
import SrcLoc
import ListSetOps
import DynFlags
71
import Unique
72
import BasicTypes
73
import qualified GHC.LanguageExtensions as LangExt
74

Ian Lynagh's avatar
Ian Lynagh committed
75
import Control.Monad
76
import Data.List
77
import Data.List.NonEmpty ( NonEmpty(..) )
78

Austin Seipp's avatar
Austin Seipp committed
79
80
81
{-
************************************************************************
*                                                                      *
82
\subsection{Type checking for type and class declarations}
Austin Seipp's avatar
Austin Seipp committed
83
84
*                                                                      *
************************************************************************
85

dreixel's avatar
dreixel committed
86
87
88
89
90
91
92
93
94
95
96
97
98
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
99
forall (k::*). k -> k. Since it does not depend on anything else, it can be
dreixel's avatar
dreixel committed
100
101
102
103
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 *.

104
105
106
107
108
109
110
111
112
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
113
-}
114

115
tcTyAndClassDecls :: [TyClGroup GhcRn]      -- Mutually-recursive groups in
116
117
118
119
                                            -- dependency order
                  -> TcM ( TcGblEnv         -- Input env extended by types and
                                            -- classes
                                            -- and their implicit Ids,DataCons
120
                         , [InstInfo GhcRn] -- Source-code instance decls info
121
122
                         , [DerivInfo]      -- data family deriving info
                         )
123
-- Fails if there are any errors
Simon Peyton Jones's avatar
Simon Peyton Jones committed
124
tcTyAndClassDecls tyclds_s
125
126
127
128
  -- The code recovers internally, but if anything gave rise to
  -- an error we'd better stop now, to avoid a cascade
  -- Type check each group in dependency order folding the global env
  = checkNoErrs $ fold_env [] [] tyclds_s
dreixel's avatar
dreixel committed
129
  where
130
    fold_env :: [InstInfo GhcRn]
131
             -> [DerivInfo]
132
133
             -> [TyClGroup GhcRn]
             -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo])
134
135
136
137
138
139
140
141
142
143
144
    fold_env inst_info deriv_info []
      = do { gbl_env <- getGblEnv
           ; return (gbl_env, inst_info, deriv_info) }
    fold_env inst_info deriv_info (tyclds:tyclds_s)
      = do { (tcg_env, inst_info', deriv_info') <- tcTyClGroup tyclds
           ; setGblEnv tcg_env $
               -- remaining groups are typechecked in the extended global env.
             fold_env (inst_info' ++ inst_info)
                      (deriv_info' ++ deriv_info)
                      tyclds_s }

145
146
tcTyClGroup :: TyClGroup GhcRn
            -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo])
147
-- Typecheck one strongly-connected component of type, class, and instance decls
Simon Peyton Jones's avatar
Simon Peyton Jones committed
148
-- See Note [TyClGroups and dependency analysis] in HsDecls
149
150
151
152
153
154
tcTyClGroup (TyClGroup { group_tyclds = tyclds
                       , group_roles  = roles
                       , group_instds = instds })
  = do { let role_annots = mkRoleAnnotEnv roles

           -- Step 1: Typecheck the type/class declarations
Simon Peyton Jones's avatar
Simon Peyton Jones committed
155
       ; traceTc "---- tcTyClGroup ---- {" empty
156
       ; traceTc "Decls for" (ppr (map (tcdName . unLoc) tyclds))
157
158
       ; tyclss <- tcTyClDecls tyclds role_annots

159
160
161
162
163
164
           -- Step 1.5: Make sure we don't have any type synonym cycles
       ; traceTc "Starting synonym cycle check" (ppr tyclss)
       ; this_uid <- fmap thisPackage getDynFlags
       ; checkSynCycles this_uid tyclss tyclds
       ; traceTc "Done synonym cycle check" (ppr tyclss)

165
166
167
168
169
170
171
172
173
174
           -- Step 2: Perform the validity check on those types/classes
           -- We can do this now because we are done with the recursive knot
           -- Do it before Step 3 (adding implicit things) because the latter
           -- expects well-formed TyCons
       ; traceTc "Starting validity check" (ppr tyclss)
       ; tyclss <- mapM checkValidTyCl tyclss
       ; traceTc "Done validity check" (ppr tyclss)
       ; mapM_ (recoverM (return ()) . checkValidRoleAnnots role_annots) tyclss
           -- See Note [Check role annotations in a second pass]

Simon Peyton Jones's avatar
Simon Peyton Jones committed
175
176
       ; traceTc "---- end tcTyClGroup ---- }" empty

177
178
179
180
181
182
183
184
185
186
187
188
           -- Step 3: Add the implicit things;
           -- we want them in the environment because
           -- they may be mentioned in interface files
       ; tcExtendTyConEnv tyclss $
    do { gbl_env <- tcAddImplicits tyclss
       ; setGblEnv gbl_env $
    do {
            -- Step 4: check instance declarations
       ; (gbl_env, inst_info, datafam_deriv_info) <- tcInstDecls1 instds

       ; return (gbl_env, inst_info, datafam_deriv_info) } } }

189
tcTyClDecls :: [LTyClDecl GhcRn] -> RoleAnnotEnv -> TcM [TyCon]
190
tcTyClDecls tyclds role_annots
dreixel's avatar
dreixel committed
191
192
193
  = 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]
194
195
         tc_tycons <- kcTyClGroup tyclds
       ; traceTc "tcTyAndCl generalized kinds" (vcat (map ppr_tc_tycon tc_tycons))
dreixel's avatar
dreixel committed
196

197
198
            -- Step 2: type-check all groups together, returning
            -- the final TyCons and Classes
199
200
201
202
            --
            -- NB: We have to be careful here to NOT eagerly unfold
            -- type synonyms, as we have not tested for type synonym
            -- loops yet and could fall into a black hole.
203
       ; fixM $ \ ~rec_tyclss -> do
204
205
           { tcg_env <- getGblEnv
           ; let roles = inferRoles (tcg_src tcg_env) role_annots rec_tyclss
dreixel's avatar
dreixel committed
206
207
208

                 -- Populate environment with knot-tied ATyCon for TyCons
                 -- NB: if the decls mention any ill-staged data cons
209
                 -- (see Note [Recursion and promoting data constructors])
210
                 -- we will have failed already in kcTyClGroup, so no worries here
211
           ; tcExtendRecEnv (zipRecTyClss tc_tycons rec_tyclss) $
dreixel's avatar
dreixel committed
212
213
214

                 -- Also extend the local type envt with bindings giving
                 -- the (polymorphic) kind of each knot-tied TyCon or Class
215
                 -- See Note [Type checking recursive type and class declarations]
216
             tcExtendKindEnv (foldl extendEnvWithTcTyCon emptyNameEnv tc_tycons) $
dreixel's avatar
dreixel committed
217
218

                 -- Kind and type check declarations for this group
Edward Z. Yang's avatar
Edward Z. Yang committed
219
               mapM (tcTyClDecl roles) tyclds
220
           } }
221
222
223
224
  where
    ppr_tc_tycon tc = parens (sep [ ppr (tyConName tc) <> comma
                                  , ppr (tyConBinders tc) <> comma
                                  , ppr (tyConResKind tc) ])
dreixel's avatar
dreixel committed
225

226
zipRecTyClss :: [TcTyCon]
227
             -> [TyCon]           -- Knot-tied
228
             -> [(Name,TyThing)]
229
230
-- Build a name-TyThing mapping for the TyCons bound by decls
-- being careful not to look at the knot-tied [TyThing]
batterseapower's avatar
batterseapower committed
231
-- The TyThings in the result list must have a visible ATyCon,
232
233
-- because typechecking types (in, say, tcTyClDecl) looks at
-- this outer constructor
234
235
zipRecTyClss tc_tycons rec_tycons
  = [ (name, ATyCon (get name)) | tc_tycon <- tc_tycons, let name = getName tc_tycon ]
236
  where
237
238
    rec_tc_env :: NameEnv TyCon
    rec_tc_env = foldr add_tc emptyNameEnv rec_tycons
239

240
241
242
243
244
245
246
247
248
    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)
249

Austin Seipp's avatar
Austin Seipp committed
250
251
252
{-
************************************************************************
*                                                                      *
253
                Kind checking
Austin Seipp's avatar
Austin Seipp committed
254
255
*                                                                      *
************************************************************************
256

257
258
259
260
Note [Kind checking for type and class decls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Kind checking is done thus:

261
262
   1. Make up a kind variable for each parameter of the declarations,
      and extend the kind environment (which is in the TcLclEnv)
263

264
   2. Kind check the declarations
265

266
267
We need to kind check all types in the mutually recursive group
before we know the kind of the type variables.  For example:
268

269
270
  class C a where
     op :: D b => a -> b -> b
271

272
273
  class D c where
     bop :: (Monad c) => ...
274
275
276
277
278

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.

279
280
281
282
283
284
Note: we don't treat type synonyms specially (we used to, in the past);
in particular, even if we have a type synonym cycle, we still kind check
it normally, and test for cycles later (checkSynCycles).  The reason
we can get away with this is because we have more systematic TYPE r
inference, which means that we can do unification between kinds that
aren't lifted (this historically was not true.)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
285

286
287
288
289
290
The downside of not directly reading off the kinds off the RHS of
type synonyms in topological order is that we don't transparently
support making synonyms of types with higher-rank kinds.  But
you can always specify a CUSK directly to make this work out.
See tc269 for an example.
291

292
293
Open type families
~~~~~~~~~~~~~~~~~~
294
295
296
This treatment of type synonyms only applies to Haskell 98-style synonyms.
General type functions can be recursive, and hence, appear in `alg_decls'.

297
The kind of an open type family is solely determinded by its kind signature;
298
hence, only kind signatures participate in the construction of the initial
299
300
301
302
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').
303
304
305
306


See also Note [Kind checking recursive type and class declarations]

307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
Note [How TcTyCons work]
o~~~~~~~~~~~~~~~~~~~~~~~~
TcTyCons are used for two distinct purposes

1.  When recovering from a type error in a type declaration,
    we want to put the erroneous TyCon in the environment in a
    way that won't lead to more errors.  We use a TcTyCon for this;
    see makeRecoveryTyCon.

2.  When checking a type/class declaration (in module TcTyClsDecls), we come
    upon knowledge of the eventual tycon in bits and pieces.

      S1) First, we use getInitialKinds to look over the user-provided
          kind signature of a tycon (including, for example, the number
          of parameters written to the tycon) to get an initial shape of
          the tycon's kind.  We record that shape in a TcTyCon.

      S2) Then, using these initial kinds, we kind-check the body of the
          tycon (class methods, data constructors, etc.), filling in the
          metavariables in the tycon's initial kind.

      S3) We then generalize to get the tycon's final, fixed
          kind. Finally, once this has happened for all tycons in a
          mutually recursive group, we can desugar the lot.

    For convenience, we store partially-known tycons in TcTyCons, which
    might store meta-variables. These TcTyCons are stored in the local
    environment in TcTyClsDecls, until the real full TyCons can be created
    during desugaring. A desugared program should never have a TcTyCon.

    A challenging piece in all of this is that we end up taking three separate
    passes over every declaration:
      - one in getInitialKind (this pass look only at the head, not the body)
      - one in kcTyClDecls (to kind-check the body)
      - a final one in tcTyClDecls (to desugar)
    In the latter two passes, we need to connect the user-written type
    variables in an LHsQTyVars with the variables in the tycon's
    inferred kind. Because the tycon might not have a CUSK, this
    matching up is, in general, quite hard to do.  (Look through the
    git history between Dec 2015 and Apr 2016 for
    TcHsType.splitTelescopeTvs!) Instead of trying, we just store the
    list of type variables to bring into scope, in the
    tyConScopedTyVars field of the TcTyCon.  These tyvars are brought
    into scope in kcTyClTyVars and tcTyClTyVars, both in TcHsType.

    In a TcTyCon, everything is zonked after the kind-checking pass (S2).
Austin Seipp's avatar
Austin Seipp committed
353
-}
354

355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374

-- Note [Missed opportunity to retain higher-rank kinds]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- In 'kcTyClGroup', there is a missed opportunity to make kind
-- inference work in a few more cases.  The idea is analogous
-- to Note [Single function non-recursive binding special-case]:
--
--      * If we have an SCC with a single decl, which is non-recursive,
--        instead of creating a unification variable representing the
--        kind of the decl and unifying it with the rhs, we can just
--        read the type directly of the rhs.
--
--      * Furthermore, we can update our SCC analysis to ignore
--        dependencies on declarations which have CUSKs: we don't
--        have to kind-check these all at once, since we can use
--        the CUSK to initialize the kind environment.
--
-- Unfortunately this requires reworking a bit of the code in
-- 'kcLTyClDecl' so I've decided to punt unless someone shouts about it.
--
375
kcTyClGroup :: [LTyClDecl GhcRn] -> TcM [TcTyCon]
376

dreixel's avatar
dreixel committed
377
-- Kind check this group, kind generalize, and return the resulting local env
378
-- This binds the TyCons and Classes of the group, but not the DataCons
dreixel's avatar
dreixel committed
379
-- See Note [Kind checking for type and class decls]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
380
381
-- Third return value is Nothing if the tycon be unsaturated; otherwise,
-- the arity
382
kcTyClGroup decls
383
  = do  { mod <- getModule
Simon Peyton Jones's avatar
Simon Peyton Jones committed
384
        ; traceTc "---- kcTyClGroup ---- {" (text "module" <+> ppr mod $$ vcat (map ppr decls))
dreixel's avatar
dreixel committed
385

386
          -- Kind checking;
387
388
389
          --    1. Bind kind variables for decls
          --    2. Kind-check decls
          --    3. Generalise the inferred kinds
dreixel's avatar
dreixel committed
390
391
          -- See Note [Kind checking for type and class decls]

392
        ; lcl_env <- solveEqualities $
393
394
395
396
397
398
399
400
401
402
403
404
405
                     do { -- Step 1: Bind kind variables for all decls
                          initial_kinds <- getInitialKinds decls
                        ; traceTc "kcTyClGroup: initial kinds" $
                          ppr initial_kinds

                        -- Step 2: Set extended envt, kind-check the decls
                        ; tcExtendKindEnv initial_kinds $
                          do { mapM_ kcLTyClDecl decls
                             ; getLclEnv } }

        -- Step 3: generalisation
        -- Kind checking done for this group
        -- Now we have to kind generalize the flexis
406
        ; res <- concatMapM (generaliseTCD (tcl_env lcl_env)) decls
407

Simon Peyton Jones's avatar
Simon Peyton Jones committed
408
        ; traceTc "---- kcTyClGroup end ---- }" (vcat (map pp_res res))
409
        ; return res }
410

411
  where
412
    generalise :: TcTypeEnv -> Name -> TcM TcTyCon
413
    -- For polymorphic things this is a no-op
414
    generalise kind_env name
415
416
417
      = do { let tc = case lookupNameEnv kind_env name of
                        Just (ATcTyCon tc) -> tc
                        _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env)
418
419
420
421
422
423
424
425
                 tc_binders  = tyConBinders tc
                 tc_res_kind = tyConResKind tc
                 tc_tyvars   = tyConTyVars tc
                 scoped_tvs  = tcTyConScopedTyVars tc

           ; kvs <- kindGeneralize (mkTyConKind tc_binders tc_res_kind)

           ; let all_binders = mkNamedTyConBinders Inferred kvs ++ tc_binders
426

Simon Peyton Jones's avatar
Simon Peyton Jones committed
427
           ; (env, all_binders') <- zonkTyVarBindersX emptyZonkEnv all_binders
428
429
           ; tc_res_kind'        <- zonkTcTypeToType env tc_res_kind
           ; scoped_tvs'         <- zonkSigTyVarPairs scoped_tvs
430

431
                      -- Make sure tc_kind' has the final, zonked kind variables
432
           ; traceTc "Generalise kind" $
433
434
435
436
             vcat [ ppr name, ppr tc_binders, ppr (mkTyConKind tc_binders tc_res_kind)
                  , ppr kvs, ppr all_binders, ppr tc_res_kind
                  , ppr all_binders', ppr tc_res_kind'
                  , ppr tc_tyvars, ppr (tcTyConScopedTyVars tc)]
437

438
439
           ; return (mkTcTyCon name all_binders' tc_res_kind'
                               scoped_tvs'
440
                               (tyConFlavour tc)) }
dreixel's avatar
dreixel committed
441

442
    generaliseTCD :: TcTypeEnv
443
                  -> LTyClDecl GhcRn -> TcM [TcTyCon]
444
    generaliseTCD kind_env (L _ decl)
445
446
      | ClassDecl { tcdLName = (L _ name), tcdATs = ats } <- decl
      = do { first <- generalise kind_env name
447
448
449
450
451
452
453
454
           ; rest <- mapM ((generaliseFamDecl kind_env) . unLoc) ats
           ; return (first : rest) }

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

      | otherwise
455
      = do { res <- generalise kind_env (tcdName decl)
456
457
           ; return [res] }

458
    generaliseFamDecl :: TcTypeEnv
459
                      -> FamilyDecl GhcRn -> TcM TcTyCon
460
461
    generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name })
      = generalise kind_env name
462

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
463
464
    pp_res tc = ppr (tyConName tc) <+> dcolon <+> ppr (tyConKind tc)

465
466
467
468
469
--------------
mkTcTyConEnv :: TcTyCon -> TcTypeEnv
mkTcTyConEnv tc = unitNameEnv (getName tc) (ATcTyCon tc)

extendEnvWithTcTyCon :: TcTypeEnv -> TcTyCon -> TcTypeEnv
470
-- Makes a binding to put in the local envt, binding
471
-- a name to a TcTyCon
472
473
474
475
extendEnvWithTcTyCon env tc
  = extendNameEnv env (getName tc) (ATcTyCon tc)

--------------
476
mkPromotionErrorEnv :: [LTyClDecl GhcRn] -> TcTypeEnv
477
478
479
-- Maps each tycon/datacon to a suitable promotion error
--    tc :-> APromotionErr TyConPE
--    dc :-> APromotionErr RecDataConPE
480
--    See Note [Recursion and promoting data constructors]
481
482
483
484
485

mkPromotionErrorEnv decls
  = foldr (plusNameEnv . mk_prom_err_env . unLoc)
          emptyNameEnv decls

486
mk_prom_err_env :: TyClDecl GhcRn -> TcTypeEnv
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
mk_prom_err_env (ClassDecl { tcdLName = L _ nm, tcdATs = ats })
  = unitNameEnv nm (APromotionErr ClassPE)
    `plusNameEnv`
    mkNameEnv [ (name, APromotionErr TyConPE)
              | L _ (FamilyDecl { fdLName = L _ name }) <- ats ]

mk_prom_err_env (DataDecl { tcdLName = L _ name
                          , tcdDataDefn = HsDataDefn { dd_cons = cons } })
  = unitNameEnv name (APromotionErr TyConPE)
    `plusNameEnv`
    mkNameEnv [ (con, APromotionErr RecDataConPE)
              | L _ con' <- cons, L _ con <- getConNames con' ]

mk_prom_err_env decl
  = unitNameEnv (tcdName decl) (APromotionErr TyConPE)
    -- Works for family declarations too

--------------
505
getInitialKinds :: [LTyClDecl GhcRn] -> TcM (NameEnv TcTyThing)
506
507
508
509
-- Maps each tycon to its initial kind,
-- and each datacon to a suitable promotion error
--    tc :-> ATcTyCon (tc:initial_kind)
--    dc :-> APromotionErr RecDataConPE
510
--    See Note [Recursion and promoting data constructors]
511

512
getInitialKinds decls
513
514
515
516
517
  = tcExtendKindEnv promotion_err_env $
    do { tc_kinds <- mapM (addLocM getInitialKind) decls
       ; return (foldl plusNameEnv promotion_err_env tc_kinds) }
  where
    promotion_err_env = mkPromotionErrorEnv decls
518

519
getInitialKind :: TyClDecl GhcRn
520
               -> TcM (NameEnv TcTyThing)
dreixel's avatar
dreixel committed
521
-- Allocate a fresh kind variable for each TyCon and Class
522
523
524
525
526
-- For each tycon, return a NameEnv with
--      name :-> ATcTyCon (TcCyCon with kind k))
-- where k is the kind of tc, derived from the LHS
--       of the definition (and probably including
--       kind unification variables)
dreixel's avatar
dreixel committed
527
--      Example: data T a b = ...
528
--      return (T, kv1 -> kv2 -> kv3)
dreixel's avatar
dreixel committed
529
--
530
531
532
533
-- 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
--
534
-- No family instances are passed to getInitialKinds
dreixel's avatar
dreixel committed
535

536
getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
537
538
  = do { let cusk = hsDeclHasCusk decl
       ; (tycon, inner_prs) <-
Simon Peyton Jones's avatar
Simon Peyton Jones committed
539
           kcLHsQTyVars name ClassFlavour cusk True ktvs $
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
540
           do { inner_prs <- getFamDeclInitialKinds (Just cusk) ats
541
              ; return (constraintKind, inner_prs) }
542
       ; return (extendEnvWithTcTyCon inner_prs tycon) }
543

544
getInitialKind decl@(DataDecl { tcdLName = L _ name
545
                              , tcdTyVars = ktvs
546
547
                              , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
                                                         , dd_ND = new_or_data } })
548
  = do  { (tycon, _) <-
Simon Peyton Jones's avatar
Simon Peyton Jones committed
549
           kcLHsQTyVars name flav (hsDeclHasCusk decl) True ktvs $
550
           do { res_k <- case m_sig of
551
                           Just ksig -> tcLHsKindSig ksig
552
                           Nothing   -> return liftedTypeKind
553
              ; return (res_k, ()) }
554
        ; return (mkTcTyConEnv tycon) }
555
556
557
558
  where
    flav = case new_or_data of
             NewType  -> NewtypeFlavour
             DataType -> DataTypeFlavour
559

Jan Stolarek's avatar
Jan Stolarek committed
560
getInitialKind (FamDecl { tcdFam = decl })
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
561
  = getFamDeclInitialKind Nothing decl
562

563
564
565
getInitialKind decl@(SynDecl { tcdLName = L _ name
                             , tcdTyVars = ktvs
                             , tcdRhs = rhs })
Simon Peyton Jones's avatar
Simon Peyton Jones committed
566
  = do  { (tycon, _) <- kcLHsQTyVars name TypeSynonymFlavour
567
568
                            (hsDeclHasCusk decl)
                            True ktvs $
569
570
            do  { res_k <- case kind_annotation rhs of
                            Nothing -> newMetaKindVar
571
                            Just ksig -> tcLHsKindSig ksig
572
                ; return (res_k, ()) }
573
        ; return (mkTcTyConEnv tycon) }
574
575
576
  where
    -- Keep this synchronized with 'hsDeclHasCusk'.
    kind_annotation (L _ ty) = case ty of
Ben Gamari's avatar
Ben Gamari committed
577
578
579
        HsParTy lty     -> kind_annotation lty
        HsKindSig _ k   -> Just k
        _               -> Nothing
580
581

---------------------------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
582
getFamDeclInitialKinds :: Maybe Bool  -- if assoc., CUSKness of assoc. class
583
                       -> [LFamilyDecl GhcRn]
584
                       -> TcM TcTypeEnv
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
585
getFamDeclInitialKinds mb_cusk decls
586
587
  = do { tc_kinds <- mapM (addLocM (getFamDeclInitialKind mb_cusk)) decls
       ; return (foldr plusNameEnv emptyNameEnv tc_kinds) }
588

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
589
getFamDeclInitialKind :: Maybe Bool  -- if assoc., CUSKness of assoc. class
590
                      -> FamilyDecl GhcRn
591
                      -> TcM TcTypeEnv
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
592
593
594
595
getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName     = L _ name
                                               , fdTyVars    = ktvs
                                               , fdResultSig = L _ resultSig
                                               , fdInfo      = info })
596
  = do { (tycon, _) <-
Simon Peyton Jones's avatar
Simon Peyton Jones committed
597
           kcLHsQTyVars name flav cusk True ktvs $
Jan Stolarek's avatar
Jan Stolarek committed
598
           do { res_k <- case resultSig of
Ben Gamari's avatar
Ben Gamari committed
599
600
                      KindSig ki                        -> tcLHsKindSig ki
                      TyVarSig (L _ (KindedTyVar _ ki)) -> tcLHsKindSig ki
Jan Stolarek's avatar
Jan Stolarek committed
601
                      _ -- open type families have * return kind by default
602
                        | tcFlavourIsOpen flav     -> return liftedTypeKind
Jan Stolarek's avatar
Jan Stolarek committed
603
604
605
                        -- closed type families have their return kind inferred
                        -- by default
                        | otherwise                -> newMetaKindVar
606
              ; return (res_k, ()) }
607
       ; return (mkTcTyConEnv tycon) }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
608
  where
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
609
    cusk  = famDeclHasCusk mb_cusk decl
610
611
612
613
    flav  = case info of
      DataFamily         -> DataFamilyFlavour
      OpenTypeFamily     -> OpenTypeFamilyFlavour
      ClosedTypeFamily _ -> ClosedTypeFamilyFlavour
614

615
------------------------------------------------------------------------
616
kcLTyClDecl :: LTyClDecl GhcRn -> TcM ()
617
  -- See Note [Kind checking for type and class decls]
618
kcLTyClDecl (L loc decl)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
619
620
621
622
623
  = setSrcSpan loc $
    tcAddDeclCtxt decl $
    do { traceTc "kcTyClDecl {" (ppr (tyClDeclLName decl))
       ; kcTyClDecl decl
       ; traceTc "kcTyClDecl done }" (ppr (tyClDeclLName decl)) }
624

625
kcTyClDecl :: TyClDecl GhcRn -> TcM ()
dreixel's avatar
dreixel committed
626
-- This function is used solely for its side effect on kind variables
627
-- NB kind signatures on the type variables and
Gabor Greif's avatar
Gabor Greif committed
628
--    result kind signature have already been dealt with
629
--    by getInitialKind, so we can ignore them here.
dreixel's avatar
dreixel committed
630

631
kcTyClDecl (DataDecl { tcdLName = L _ name, tcdDataDefn = defn })
632
  | HsDataDefn { dd_cons = cons, dd_kindSig = Just _ } <- defn
633
  = mapM_ (wrapLocM kcConDecl) cons
634
635
636
637
638
639
    -- 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
640

641
  | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
642
  = kcTyClTyVars name $
643
    do  { _ <- tcHsContext ctxt
644
        ; mapM_ (wrapLocM kcConDecl) cons }
645

646
647
648
649
650
651
kcTyClDecl (SynDecl { tcdLName = L _ name, tcdRhs = lrhs })
  = kcTyClTyVars name $
    do  { syn_tc <- kcLookupTcTyCon name
        -- NB: check against the result kind that we allocated
        -- in getInitialKinds.
        ; discardResult $ tcCheckLHsType lrhs (tyConResKind syn_tc) }
652

653
654
655
kcTyClDecl (ClassDecl { tcdLName = L _ name
                      , tcdCtxt = ctxt, tcdSigs = sigs })
  = kcTyClTyVars name $
656
    do  { _ <- tcHsContext ctxt
657
        ; mapM_ (wrapLocM kc_sig)     sigs }
dreixel's avatar
dreixel committed
658
  where
Alan Zimmerman's avatar
Alan Zimmerman committed
659
    kc_sig (ClassOpSig _ nms op_ty) = kcHsSigType nms op_ty
660
    kc_sig _                        = return ()
661

662
kcTyClDecl (FamDecl (FamilyDecl { fdLName  = L _ fam_tc_name
663
664
665
666
667
                                , fdInfo   = fd_info }))
-- closed type families look at their equations, but other families don't
-- do anything here
  = case fd_info of
      ClosedTypeFamily (Just eqns) ->
668
        do { fam_tc <- kcLookupTcTyCon fam_tc_name
669
           ; mapM_ (kcTyFamInstEqn fam_tc) eqns }
670
      _ -> return ()
dreixel's avatar
dreixel committed
671
672

-------------------
673
kcConDecl :: ConDecl GhcRn -> TcM ()
674
675
kcConDecl (ConDeclH98 { con_name = name, con_ex_tvs = ex_tvs
                      , con_mb_cxt = ex_ctxt, con_args = args })
Alan Zimmerman's avatar
Alan Zimmerman committed
676
  = addErrCtxt (dataConCtxtName [name]) $
677
678
679
680
    do { _ <- tcExplicitTKBndrs ex_tvs $ \ _ ->
              do { _ <- tcHsMbContext ex_ctxt
                 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args)
                 ; return (panic "kcConDecl", emptyVarSet) }
681
       ; return () }
682

Alan Zimmerman's avatar
Alan Zimmerman committed
683
kcConDecl (ConDeclGADT { con_names = names
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
                       , con_qvars = qtvs, con_mb_cxt = cxt
                       , con_args = args, con_res_ty = res_ty })
  | HsQTvs { hsq_implicit = implicit_tkv_nms
           , hsq_explicit = explicit_tkv_nms } <- qtvs
  = -- Even though the data constructor's type is closed, we
    -- must still kind-check the type, because that may influence
    -- the inferred kind of the /type/ constructor.  Example:
    --    data T f a where
    --      MkT :: f a -> T f a
    -- If we don't look at MkT we won't get the correct kind
    -- for the type constructor T
    addErrCtxt (dataConCtxtName names) $
    do { _ <- tcImplicitTKBndrs implicit_tkv_nms $
              tcExplicitTKBndrs explicit_tkv_nms $ \ _ ->
              do { _ <- tcHsMbContext cxt
                 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args)
                 ; _ <- tcHsOpenType res_ty
                 ; return (panic "kcConDecl", emptyVarSet) }
Alan Zimmerman's avatar
Alan Zimmerman committed
702
703
         ; return () }

Austin Seipp's avatar
Austin Seipp committed
704
{-
705
706
Note [Recursion and promoting data constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
707
708
709
710
711
712
713
714
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:
715
716
  T -> ATcTyCon <some initial kind>
  K -> APromotionErr
717

718
APromotionErr is only used for DataCons, and only used during type checking
719
720
in tcTyClGroup.

721

Austin Seipp's avatar
Austin Seipp committed
722
723
************************************************************************
*                                                                      *
724
\subsection{Type checking}
Austin Seipp's avatar
Austin Seipp committed
725
726
*                                                                      *
************************************************************************
727

dreixel's avatar
dreixel committed
728
729
730
731
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,
732
we discarded the kind-checked types (eg RHSs of data type decls);
dreixel's avatar
dreixel committed
733
734
735
736
737
738
739
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
740
    to be given kind arguments.
dreixel's avatar
dreixel committed
741
742
743
744
745
746
747

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

dreixel's avatar
dreixel committed
749
750
751
752
753
754
755
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

756
757
  *Global* env with T -> ATyCon (the (not yet built) final TyCon for T)
  *Local*  env with T -> ATcTyCon (TcTyCon with the polymorphic kind of T)
dreixel's avatar
dreixel committed
758
759
760
761
762
763
764
765
766
767

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
768
This fancy footwork (with two bindings for T) is only necessary for the
dreixel's avatar
dreixel committed
769
770
TyCons or Classes of this recursive group.  Earlier, finished groups,
live in the global env only.
771

772
773
774
775
776
777
778
779
780
781
782
See also Note [Kind checking recursive type and class declarations]

Note [Kind checking recursive type and class declarations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Before we can type-check the decls, we must kind check them. This
is done by establishing an "initial kind", which is a rather uninformed
guess at a tycon's kind (by counting arguments, mainly) and then
using this initial kind for recursive occurrences.

The initial kind is stored in exactly the same way during kind-checking
as it is during type-checking (Note [Type checking recursive type and class
783
declarations]): in the *local* environment, with ATcTyCon. But we still
784
785
786
787
788
789
790
791
792
793
794
must store *something* in the *global* environment. Even though we
discard the result of kind-checking, we sometimes need to produce error
messages. These error messages will want to refer to the tycons being
checked, except that they don't exist yet, and it would be Terribly
Annoying to get the error messages to refer back to HsSyn. So we
create a TcTyCon and put it in the global env. This tycon can
print out its name and knows its kind,
but any other action taken on it will panic. Note
that TcTyCons are *not* knot-tied, unlike the rather valid but
knot-tied ones that occur during type-checking.

795
796
797
798
799
800
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
801
-}
dreixel's avatar
dreixel committed
802

803
tcTyClDecl :: RolesInfo -> LTyClDecl GhcRn -> TcM TyCon
Edward Z. Yang's avatar
Edward Z. Yang committed
804
tcTyClDecl roles_info (L loc decl)
805
  | Just thing <- wiredInNameTyThing_maybe (tcdName decl)
806
807
808
  = case thing of -- See Note [Declarations for wired-in things]
      ATyCon tc -> return tc
      _ -> pprPanic "tcTyClDecl" (ppr thing)
809
810

  | otherwise
811
  = setSrcSpan loc $ tcAddDeclCtxt decl $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
812
813
814
815
    do { traceTc "---- tcTyClDecl ---- {" (ppr decl)
       ; tc <- tcTyClDecl1 Nothing roles_info decl
       ; traceTc "---- tcTyClDecl end ---- }" (ppr tc)
       ; return tc }
816

817
  -- "type family" declarations
818
tcTyClDecl1 :: Maybe Class -> RolesInfo -> TyClDecl GhcRn -> TcM TyCon
Edward Z. Yang's avatar
Edward Z. Yang committed
819
tcTyClDecl1 parent _roles_info (FamDecl { tcdFam = fd })
820
  = tcFamDecl1 parent fd
821

822
  -- "type" synonym declaration
Edward Z. Yang's avatar
Edward Z. Yang committed
823
tcTyClDecl1 _parent roles_info
824
            (SynDecl { tcdLName = L _ tc_name, tcdRhs = rhs })
825
  = ASSERT( isNothing _parent )
826
    tcTyClTyVars tc_name $ \ binders res_kind ->
Edward Z. Yang's avatar
Edward Z. Yang committed
827
    tcTySynRhs roles_info tc_name binders res_kind rhs
828

829
  -- "data/newtype" declaration
Edward Z. Yang's avatar
Edward Z. Yang committed
830
tcTyClDecl1 _parent roles_info
831
            (DataDecl { tcdLName = L _ tc_name, tcdDataDefn = defn })
832
  = ASSERT( isNothing _parent )
833
    tcTyClTyVars tc_name $ \ tycon_binders res_kind ->
Edward Z. Yang's avatar
Edward Z. Yang committed
834
    tcDataDefn roles_info tc_name tycon_binders res_kind defn
835

Edward Z. Yang's avatar
Edward Z. Yang committed
836
tcTyClDecl1 _parent roles_info
837
            (ClassDecl { tcdLName = L _ class_name
838
            , tcdCtxt = ctxt, tcdMeths = meths
839
            , tcdFDs = fundeps, tcdSigs = sigs
840
            , tcdATs = ats, tcdATDefs = at_defs })
841
  = ASSERT( isNothing _parent )
842
    do { clas <- fixM $ \ clas ->
Gabor Greif's avatar
Gabor Greif committed
843
            -- We need the knot because 'clas' is passed into tcClassATs
844
            tcTyClTyVars class_name $ \ binders res_kind ->
845
            do { MASSERT( isConstraintKind res_kind )
846
               ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr binders)
847
848
               ; let tycon_name = class_name        -- We use the same name
                     roles = roles_info tycon_name  -- for TyCon and Class
dreixel's avatar
dreixel committed
849

850
               ; ctxt' <- solveEqualities $ tcHsContext ctxt
851
               ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'
852
853
                       -- Squeeze out any kind unification variables
               ; fds'  <- mapM (addLocM tc_fundep) fundeps
854
               ; sig_stuff <- tcClassSigs class_name sigs meths
855
               ; at_stuff <- tcClassATs class_name clas ats at_defs
856
               ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
857
858
859
860
861
862
863
864
865
               -- TODO: Allow us to distinguish between abstract class,
               -- and concrete class with no methods (maybe by
               -- specifying a trailing where or not
               ; is_boot <- tcIsHsBootOrSig
               ; let body | is_boot, null ctxt', null at_stuff, null sig_stuff
                          = Nothing
                          | otherwise
                          = Just (ctxt', at_stuff, sig_stuff, mindef)
               ; clas <- buildClass class_name binders roles fds' body
866
               ; traceTc "tcClassDecl" (ppr fundeps $$ ppr binders $$
867
                                        ppr fds')
868
869
870
               ; return clas }

         ; return (classTyCon clas) }
871
  where
872
873
    tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM (tcLookupTyVar . unLoc) tvs1 ;
                                ; tvs2' <- mapM (tcLookupTyVar . unLoc) tvs2 ;
874
                                ; return (tvs1', tvs2') }
Jan Stolarek's avatar
Jan Stolarek committed
875

876
tcFamDecl1 :: Maybe Class -> FamilyDecl GhcRn -> TcM TyCon
877
tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_name)
878
                              , fdResultSig = L _ sig
879
                              , fdInjectivityAnn = inj })
880
  | DataFamily <- fam_info
881
  = tcTyClTyVars tc_name $ \ binders res_kind -> do
882
883
  { traceTc "data family:" (ppr tc_name)
  ; checkFamFlag tc_name
Simon Peyton Jones's avatar
Simon Peyton Jones committed
884
885
886
887
888
889
890
891
892

  -- Check the kind signature, if any.
  -- Data families might have a variable return kind.
  -- See See Note [Arity of data families] in FamInstEnv.
  ; (extra_binders, final_res_kind) <- tcDataKindSig binders res_kind
  ; checkTc (isLiftedTypeKind final_res_kind
             || isJust (tcGetCastedTyVar_maybe final_res_kind))
            (badKindSig False res_kind)

893
  ; tc_rep_name <- newTyConRepName tc_name
894
  ; let tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
895
                              final_res_kind
896
897
898
899
900
901
                              (resultVariableName sig)
                              (DataFamilyTyCon tc_rep_name)
                              parent NotInjective
  ; return tycon }

  | OpenTypeFamily <- fam_info
902
  = tcTyClTyVars tc_name $ \ binders res_kind -> do
903
  { traceTc "open type family:" (ppr tc_name)
904
  ; checkFamFlag tc_name
905
906
  ; inj' <- tcInjectivity binders inj
  ; let tycon = mkFamilyTyCon tc_name binders res_kind
907
908
                               (resultVariableName sig) OpenSynFamilyTyCon
                               parent inj'
909
  ; return tycon }
910

911
912
913
914
  | ClosedTypeFamily mb_eqns <- fam_info
  = -- Closed type families are a little tricky, because they contain the definition
    -- of both the type family and the equations for a CoAxiom.
    do { traceTc "Closed type family:" (ppr tc_name)
Jan Stolarek's avatar
Jan Stolarek committed
915
916
         -- the variables in the header scope only over the injectivity
         -- declaration but this is not involved here
917
       ; (inj', binders, res_kind)
918
            <- tcTyClTyVars tc_name
919
920
921
               $ \ binders res_kind ->
               do { inj' <- tcInjectivity binders inj
                  ; return (inj', binders, res_kind) }
922
923
924

       ; checkFamFlag tc_name -- make sure we have -XTypeFamilies

925
926
927
         -- 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
928
           Nothing   ->
929
               return $ mkFamilyTyCon tc_name binders res_kind
930
931
932
                                      (resultVariableName sig)
                                      AbstractClosedSynFamilyTyCon parent
                                      inj'
933
934
           Just eqns -> do {

935
         -- Process the equations, creating CoAxBranches
936
937
       ; let tc_fam_tc = mkTcTyCon tc_name binders res_kind
                                   [] ClosedTypeFamilyFlavour
Jan Stolarek's avatar
Jan Stolarek committed
938

939
       ; branches <- mapM (tcTyFamInstEqn tc_fam_tc Nothing) eqns
Jan Stolarek's avatar
Jan Stolarek committed
940
941
942
943
944
         -- 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
945

Jan Stolarek's avatar
Jan Stolarek committed
946
         -- Create a CoAxiom, with the correct src location. It is Vitally
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
947
948
949
950
951
952
         -- 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
953
       ; co_ax_name <- newFamInstAxiomName tc_lname []
954

955
       ; let mb_co_ax
Jan Stolarek's avatar
Jan Stolarek committed
956
957
958
              | null eqns = Nothing   -- mkBranchedCoAxiom fails on empty list
              | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches)

959
             fam_tc = mkFamilyTyCon tc_name binders res_kind (resultVariableName sig)
960
                      (ClosedSynFamilyTyCon mb_co_ax) parent inj'
Jan Stolarek's avatar
Jan Stolarek committed
961

962
963
964
         -- We check for instance validity later, when doing validity
         -- checking for the tycon. Exception: checking equations
         -- overlap done by dropDominatedAxioms
965
       ; return fam_tc } }
966