TcTyClsDecls.hs 161 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 #-}
11
{-# LANGUAGE ViewPatterns #-}
Ian Lynagh's avatar
Ian Lynagh committed
12

13
module TcTyClsDecls (
14
        tcTyAndClassDecls,
15

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

25
#include "HsVersions.h"
26

27 28
import GhcPrelude

29 30 31
import HsSyn
import HscTypes
import BuildTyCl
32
import TcRnMonad
33
import TcEnv
34
import TcValidity
35
import TcHsSyn
36 37
import TcTyDecls
import TcClassDcl
38
import {-# SOURCE #-} TcInstDcls( tcInstDecls1 )
39
import TcDeriv (DerivInfo)
40
import TcHsType
41
import ClsInst( AssocInstInfo(..) )
42
import TcMType
43
import TysWiredIn ( unitTy )
44
import TcType
45
import RnEnv( lookupConstructorFields )
46
import FamInst
Jan Stolarek's avatar
Jan Stolarek committed
47
import FamInstEnv
48
import Coercion
49
import Type
50
import TyCoRep   -- for checkValidRoles
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 67 68 69
import Maybes
import Unify
import Util
import SrcLoc
import ListSetOps
import DynFlags
70
import Unique
71
import ConLike( ConLike(..) )
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 79
import qualified Data.Set as Set

80

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

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

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

117
tcTyAndClassDecls :: [TyClGroup GhcRn]      -- Mutually-recursive groups in
118 119 120 121
                                            -- dependency order
                  -> TcM ( TcGblEnv         -- Input env extended by types and
                                            -- classes
                                            -- and their implicit Ids,DataCons
122
                         , [InstInfo GhcRn] -- Source-code instance decls info
123 124
                         , [DerivInfo]      -- data family deriving info
                         )
125
-- Fails if there are any errors
Simon Peyton Jones's avatar
Simon Peyton Jones committed
126
tcTyAndClassDecls tyclds_s
127 128 129 130
  -- 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
131
  where
132
    fold_env :: [InstInfo GhcRn]
133
             -> [DerivInfo]
134 135
             -> [TyClGroup GhcRn]
             -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo])
136 137 138 139 140 141 142 143 144 145 146
    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 }

147 148
tcTyClGroup :: TyClGroup GhcRn
            -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo])
149
-- Typecheck one strongly-connected component of type, class, and instance decls
Simon Peyton Jones's avatar
Simon Peyton Jones committed
150
-- See Note [TyClGroups and dependency analysis] in HsDecls
151 152 153 154 155 156
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
157
       ; traceTc "---- tcTyClGroup ---- {" empty
158
       ; traceTc "Decls for" (ppr (map (tcdName . unLoc) tyclds))
159 160
       ; tyclss <- tcTyClDecls tyclds role_annots

161 162 163 164 165 166
           -- 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)

167 168 169 170 171
           -- 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)
172
       ; tyclss <- concatMapM checkValidTyCl tyclss
173 174 175 176
       ; 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
177 178
       ; traceTc "---- end tcTyClGroup ---- }" empty

179 180 181
           -- Step 3: Add the implicit things;
           -- we want them in the environment because
           -- they may be mentioned in interface files
182 183 184
       ; gbl_env <- addTyConsToGblEnv tyclss

           -- Step 4: check instance declarations
185
       ; setGblEnv gbl_env $
186
         tcInstDecls1 instds }
187

188
tcTyClGroup (XTyClGroup _) = panic "tcTyClGroup"
189

190
tcTyClDecls :: [LTyClDecl GhcRn] -> RoleAnnotEnv -> TcM [TyCon]
191
tcTyClDecls tyclds role_annots
192 193
  = tcExtendKindEnv promotion_err_env $   --- See Note [Type environment evolution]
    do {    -- Step 1: kind-check this group and returns the final
dreixel's avatar
dreixel committed
194 195
            -- (possibly-polymorphic) kind of each TyCon and Class
            -- See Note [Kind checking for type and class decls]
196 197
         tc_tycons <- kcTyClGroup tyclds
       ; traceTc "tcTyAndCl generalized kinds" (vcat (map ppr_tc_tycon tc_tycons))
dreixel's avatar
dreixel committed
198

199 200
            -- Step 2: type-check all groups together, returning
            -- the final TyCons and Classes
201 202 203 204
            --
            -- 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.
205
       ; fixM $ \ ~rec_tyclss -> do
206 207
           { tcg_env <- getGblEnv
           ; let roles = inferRoles (tcg_src tcg_env) role_annots rec_tyclss
dreixel's avatar
dreixel committed
208 209 210

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

                 -- Also extend the local type envt with bindings giving
216
                 -- a TcTyCon for each each knot-tied TyCon or Class
217
                 -- See Note [Type checking recursive type and class declarations]
218 219
                 -- and Note [Type environment evolution]
             tcExtendKindEnvWithTyCons tc_tycons $
dreixel's avatar
dreixel committed
220 221

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

231
zipRecTyClss :: [TcTyCon]
232
             -> [TyCon]           -- Knot-tied
233
             -> [(Name,TyThing)]
234 235
-- 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
236
-- The TyThings in the result list must have a visible ATyCon,
237 238
-- because typechecking types (in, say, tcTyClDecl) looks at
-- this outer constructor
239 240
zipRecTyClss tc_tycons rec_tycons
  = [ (name, ATyCon (get name)) | tc_tycon <- tc_tycons, let name = getName tc_tycon ]
241
  where
242 243
    rec_tc_env :: NameEnv TyCon
    rec_tc_env = foldr add_tc emptyNameEnv rec_tycons
244

245 246 247 248 249 250 251 252 253
    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)
254

Austin Seipp's avatar
Austin Seipp committed
255 256 257
{-
************************************************************************
*                                                                      *
258
                Kind checking
Austin Seipp's avatar
Austin Seipp committed
259 260
*                                                                      *
************************************************************************
261

262 263 264 265
Note [Kind checking for type and class decls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Kind checking is done thus:

266 267
   1. Make up a kind variable for each parameter of the declarations,
      and extend the kind environment (which is in the TcLclEnv)
268

269
   2. Kind check the declarations
270

271 272
We need to kind check all types in the mutually recursive group
before we know the kind of the type variables.  For example:
273

274 275
  class C a where
     op :: D b => a -> b -> b
276

277 278
  class D c where
     bop :: (Monad c) => ...
279 280 281 282 283

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.

284 285 286 287 288 289
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
290

291 292 293 294 295
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.
296

297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316
Note [Skip decls with CUSKs in kcLTyClDecl]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider

    data T (a :: *) = MkT (S a)   -- Has CUSK
    data S a = MkS (T Int) (S a)  -- No CUSK

Via getInitialKinds we get
  T :: * -> *
  S :: kappa -> *

Then we call kcTyClDecl on each decl in the group, to constrain the
kind unification variables.  BUT we /skip/ the RHS of any decl with
a CUSK.  Here we skip the RHS of T, so we eventually get
  S :: forall k. k -> *

This gets us more polymorphism than we would otherwise get, similar
(but implemented strangely differently from) the treatment of type
signatures in value declarations.

317 318
Open type families
~~~~~~~~~~~~~~~~~~
319 320 321
This treatment of type synonyms only applies to Haskell 98-style synonyms.
General type functions can be recursive, and hence, appear in `alg_decls'.

322
The kind of an open type family is solely determinded by its kind signature;
323
hence, only kind signatures participate in the construction of the initial
324 325 326 327
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').
328 329 330

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

331
Note [How TcTyCons work]
332
~~~~~~~~~~~~~~~~~~~~~~~~
333 334 335 336 337 338 339 340 341 342 343 344 345 346 347
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.

Tobias Dammers's avatar
Tobias Dammers committed
348 349 350 351
          For CUSK tycons, the TcTyCon has the final, generalised kind.
          For non-CUSK tycons, the TcTyCon has as its tyConBinders only
          the explicit arguments given -- no kind variables, etc.

352 353 354 355
      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.

Tobias Dammers's avatar
Tobias Dammers committed
356
      S3) We then generalize to get the (non-CUSK) tycon's final, fixed
357 358 359 360 361 362 363 364
          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.

365 366 367 368
3.  In a TcTyCon, everything is zonked after the kind-checking pass (S2).

4.  tyConScopedTyVars.  A challenging piece in all of this is that we
    end up taking three separate passes over every declaration:
369 370 371
      - 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)
372

373 374 375 376 377
    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
378 379 380 381
    TcHsType.splitTelescopeTvs!)

    Instead of trying, we just store the list of type variables to
    bring into scope, in the tyConScopedTyVars field of the TcTyCon.
382
    These tyvars are brought into scope in TcHsType.bindTyClTyVars.
383

384 385 386 387 388 389 390 391
    In a TcTyCon, why is tyConScopedTyVars :: [(Name,TcTyVar)] rather
    than just [TcTyVar]?  Consider these mutually-recursive decls
       data T (a :: k1) b = MkT (S a b)
       data S (c :: k2) d = MkS (T c d)
    We start with k1 bound to kappa1, and k2 to kappa2; so initially
    in the (Name,TcTyVar) pairs the Name is that of the TcTyVar. But
    then kappa1 and kappa2 get unified; so after the zonking in
    'generalise' in 'kcTyClGroup' the Name and TcTyVar may differ.
392

393
See also Note [Type checking recursive type and class declarations].
394

395 396 397 398 399
Note [Type environment evolution]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
As we typecheck a group of declarations the type environment evolves.
Consider for example:
  data B (a :: Type) = MkB (Proxy 'MkB)
400

401 402 403 404 405 406 407 408 409 410 411 412
We do the following steps:

  1. Start of tcTyClDecls: use mkPromotionErrorEnv to initialise the
     type env with promotion errors
            B   :-> TyConPE
            MkB :-> DataConPE

  2. kcTyCLGruup
      - Do getInitialKinds, which will signal a promotion
        error if B is used in any of the kinds needed to initialse
        B's kind (e.g. (a :: Type)) here

413
      - Extend the type env with these initial kinds (monomorphic for
414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451
        decls that lack a CUSK)
            B :-> TcTyCon <initial kind>
        (thereby overriding the B :-> TyConPE binding)
        and do kcLTyClDecl on each decl to get equality constraints on
        all those inital kinds

      - Generalise the inital kind, making a poly-kinded TcTyCon

  3. Back in tcTyDecls, extend the envt with bindings of the poly-kinded
     TcTyCons, again overriding the promotion-error bindings.

     But note that the data constructor promotion errors are still in place
     so that (in our example) a use of MkB will sitll be signalled as
     an error.

  4. Typecheck the decls.

  5. In tcTyClGroup, extend the envt with bindings for TyCon and DataCons


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.
452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474

Note [Don't process associated types in kcLHsQTyVars]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Previously, we processed associated types in the thing_inside in kcLHsQTyVars,
but this was wrong -- we want to do ATs sepearately.
The consequence for not doing it this way is #15142:

  class ListTuple (tuple :: Type) (as :: [(k, Type)]) where
    type ListToTuple as :: Type

We assign k a kind kappa[1]. When checking the tuple (k, Type), we try to unify
kappa ~ Type, but this gets deferred because we bumped the TcLevel as we bring
`tuple` into scope. Thus, when we check ListToTuple, kappa[1] still hasn't
unified with Type. And then, when we generalize the kind of ListToTuple (which
indeed has a CUSK, according to the rules), we skolemize the free metavariable
kappa. Note that we wouldn't skolemize kappa when generalizing the kind of ListTuple,
because the solveEqualities in kcLHsQTyVars is at TcLevel 1 and so kappa[1]
will unify with Type.

Bottom line: as associated types should have no effect on a CUSK enclosing class,
we move processing them to a separate action, run after the outer kind has
been generalized.

475
-}
476

477
kcTyClGroup :: [LTyClDecl GhcRn] -> TcM [TcTyCon]
478

dreixel's avatar
dreixel committed
479
-- Kind check this group, kind generalize, and return the resulting local env
480
-- This binds the TyCons and Classes of the group, but not the DataCons
dreixel's avatar
dreixel committed
481
-- See Note [Kind checking for type and class decls]
482
-- and Note [Inferring kinds for type declarations]
483
kcTyClGroup decls
484
  = do  { mod <- getModule
485
        ; traceTc "---- kcTyClGroup ---- {"
486
                  (text "module" <+> ppr mod $$ vcat (map ppr decls))
dreixel's avatar
dreixel committed
487

488
          -- Kind checking;
489 490 491
          --    1. Bind kind variables for decls
          --    2. Kind-check decls
          --    3. Generalise the inferred kinds
dreixel's avatar
dreixel committed
492 493
          -- See Note [Kind checking for type and class decls]

494 495
        ; let (cusk_decls, no_cusk_decls)
                 = partition (hsDeclHasCusk . unLoc) decls
496

497
        ; poly_cusk_tcs <- getInitialKinds True cusk_decls
498

499 500 501 502 503 504 505 506
        ; mono_tcs
            <- tcExtendKindEnvWithTyCons poly_cusk_tcs $
               pushTcLevelM_   $  -- We are going to kind-generalise, so
                                  -- unification variables in here must
                                  -- be one level in
               solveEqualities $
               do {  -- Step 1: Bind kind variables for all decls
                    mono_tcs <- getInitialKinds False no_cusk_decls
507

508 509
                  ; traceTc "kcTyClGroup: initial kinds" $
                    ppr_tc_kinds mono_tcs
Tobias Dammers's avatar
Tobias Dammers committed
510

511 512 513 514 515 516 517 518 519 520
                    -- Step 2: Set extended envt, kind-check the decls
                    -- NB: the environment extension overrides the tycon
                    --     promotion-errors bindings
                    --     See Note [Type environment evolution]
                  ; tcExtendKindEnvWithTyCons mono_tcs $
                    mapM_ kcLTyClDecl no_cusk_decls

                  ; return mono_tcs }

        -- Step 3: generalisation
Tobias Dammers's avatar
Tobias Dammers committed
521 522 523
        -- Finally, go through each tycon and give it its final kind,
        -- with all the required, specified, and inferred variables
        -- in order.
524
        ; poly_no_cusk_tcs <- mapAndReportM generaliseTcTyCon mono_tcs
525

526
        ; let poly_tcs = poly_cusk_tcs ++ poly_no_cusk_tcs
527 528
        ; traceTc "---- kcTyClGroup end ---- }" (ppr_tc_kinds poly_tcs)
        ; return poly_tcs }
529

530
  where
531 532 533
    ppr_tc_kinds tcs = vcat (map pp_tc tcs)
    pp_tc tc = ppr (tyConName tc) <+> dcolon <+> ppr (tyConKind tc)

534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597
generaliseTcTyCon :: TcTyCon -> TcM TcTyCon
generaliseTcTyCon tc
  -- See Note [Required, Specified, and Inferred for types]
  = setSrcSpan (getSrcSpan tc) $
    addTyConCtxt tc $
    do { let tc_name     = tyConName tc
             tc_flav     = tyConFlavour tc
             tc_res_kind = tyConResKind tc
             tc_tvs      = tyConTyVars  tc

             (scoped_tv_names, scoped_tvs) = unzip (tcTyConScopedTyVars tc)
             -- NB: scoped_tvs includes both specified and required (tc_tvs)
             -- ToDo: Is this a good idea?

       -- Step 1: find all the variables we want to quantify over,
       --         including Inferred, Specfied, and Required
       ; dvs <- candidateQTyVarsOfKinds $
                (tc_res_kind : map tyVarKind scoped_tvs)
       ; tc_tvs      <- mapM zonkTcTyVarToTyVar tc_tvs
       ; let full_dvs = dvs { dv_tvs = mkDVarSet tc_tvs }

       -- Step 2: quantify, mainly meaning skolemise the free variables
       ; qtkvs <- quantifyTyVars emptyVarSet full_dvs
                  -- Returned 'qtkvs' are scope-sorted and skolemised

       -- Step 3: find the final identity of the Specified and Required tc_tvs
       -- (remember they all started as TyVarTvs).
       -- They have been skolemised by quantifyTyVars.
       ; scoped_tvs  <- mapM zonkTcTyVarToTyVar scoped_tvs
       ; tc_tvs      <- mapM zonkTcTyVarToTyVar tc_tvs
       ; tc_res_kind <- zonkTcType tc_res_kind

       ; traceTc "Generalise kind pre" $
         vcat [ text "tycon =" <+> ppr tc
              , text "tc_tvs =" <+> pprTyVars tc_tvs
              , text "scoped_tvs =" <+> pprTyVars scoped_tvs ]

       -- Step 4: Find the Specified and Inferred variables
       -- First, delete the Required tc_tvs from qtkvs; then
       -- partition by whether they are scoped (if so, Specified)
       ; let qtkv_set      = mkVarSet qtkvs
             tc_tv_set     = mkVarSet tc_tvs
             specified     = scopedSort $
                             [ tv | tv <- scoped_tvs
                                  , not (tv `elemVarSet` tc_tv_set)
                                  , tv `elemVarSet` qtkv_set ]
                             -- NB: maintain the L-R order of scoped_tvs
             spec_req_set  = mkVarSet specified `unionVarSet` tc_tv_set
             inferred      = filterOut (`elemVarSet` spec_req_set) qtkvs

       -- Step 5: Make the TyConBinders.
             dep_fv_set     = candidateKindVars dvs
             inferred_tcbs  = mkNamedTyConBinders Inferred inferred
             specified_tcbs = mkNamedTyConBinders Specified specified
             required_tcbs  = map (mkRequiredTyConBinder dep_fv_set) tc_tvs

       -- Step 6: Assemble the final list.
             final_tcbs = concat [ inferred_tcbs
                                 , specified_tcbs
                                 , required_tcbs ]

             scoped_tv_pairs = scoped_tv_names `zip` scoped_tvs

       -- Step 7: Make the result TcTyCon
Simon Peyton Jones's avatar
Simon Peyton Jones committed
598
             tycon = mkTcTyCon tc_name final_tcbs tc_res_kind
599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631
                            scoped_tv_pairs
                            True {- it's generalised now -}
                            (tyConFlavour tc)

       ; traceTc "Generalise kind" $
         vcat [ text "tycon =" <+> ppr tc
              , text "tc_tvs =" <+> pprTyVars tc_tvs
              , text "tc_res_kind =" <+> ppr tc_res_kind
              , text "scoped_tvs =" <+> pprTyVars scoped_tvs
              , text "inferred =" <+> pprTyVars inferred
              , text "specified =" <+> pprTyVars specified
              , text "required_tcbs =" <+> ppr required_tcbs
              , text "final_tcbs =" <+> ppr final_tcbs ]

       -- Step 8: check for floating kind vars
       -- See Note [Free-floating kind vars]
       -- They are easily identified by the fact that they
       -- have not been skolemised by quantifyTyVars
       ; let floating_specified = filter isTyVarTyVar scoped_tvs
       ; reportFloatingKvs tc_name tc_flav
                           scoped_tvs floating_specified

       -- Step 9: Check for duplicates
       -- E.g. data SameKind (a::k) (b::k)
       --      data T (a::k1) (b::k2) = MkT (SameKind a b)
       -- Here k1 and k2 start as TyVarTvs, and get unified with each other
       ; mapM_ report_sig_tv_err (findDupTyVarTvs scoped_tv_pairs)

       -- Step 10: Check for validity.
       -- We do this here because we're about to put the tycon into
       -- the environment, and we don't want anything malformed in the
       -- environment.
       ; checkValidTelescope tycon
dreixel's avatar
dreixel committed
632

633 634 635 636 637 638
       ; return tycon }
  where
    report_sig_tv_err (n1, n2)
      = setSrcSpan (getSrcSpan n2) $
        addErrTc (text "Couldn't match" <+> quotes (ppr n1)
                        <+> text "with" <+> quotes (ppr n2))
639

640 641 642
{- Note [Required, Specified, and Inferred for types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Each forall'd type variable in a type or kind is one of
643

644
  * Required: an argument must be provided at every call site
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
645

646 647
  * Specified: the argument can be inferred at call sites, but
    may be instantiated with visible type/kind application
648

649 650
  * Inferred: the must be inferred at call sites; it
    is unavailable for use with visible type/kind application.
651

652 653 654 655
Why have Inferred at all? Because we just can't make user-facing
promises about the ordering of some variables. These might swizzle
around even between minor released. By forbidding visible type
application, we ensure users aren't caught unawares.
656

657
Go read Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep.
658

659 660 661 662 663 664 665 666 667 668 669 670 671 672 673
The question for this Note is this:
   given a TyClDecl, how are its quantified type variables classified?
Much of the debate is memorialized in #15743.

Here is our design choice. When inferring the ordering of variables
for a TyCl declaration (that is, for those variables that he user
has not specified the order with an explicit `forall`), we use the
following order:

 1. Inferred variables
 2. Specified variables; in the left-to-right order in which
    the user wrote them, modified by scopedSort (see below)
    to put them in depdendency order.
 3. Required variables before a top-level ::
 4. All variables after a top-level ::
Tobias Dammers's avatar
Tobias Dammers committed
674 675 676

If this ordering does not make a valid telescope, we reject the definition.

677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729
Example:
  data SameKind :: k -> k -> *
  data Bad a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)

For X:
  - a, c, d, x are Required; they are explicitly listed by the user
    as the positional arguments of Bad
  - b is Specified; it appears explicitly in a kind signature
  - k, the kind of a, is Inferred; it is not mentioned explicitly at all

Putting variables in the order Inferred, Specified, Required
gives us this telescope:
  Inferred:  k
  Specified: b : Proxy a
  Required : (a : k) (c : Proxy b) (d : Proxy a) (x : SameKind b d)

But this order is ill-scoped, because b's kind mentions a, which occurs
after b in the telescope. So we reject Bad.

Associated types
~~~~~~~~~~~~~~~~
For associated types everything above is determined by the
associated-type declaration alone, ignoring the class header.
Here is an example (Trac #15592)
  class C (a :: k) b where
    type F (x :: b a)

In the kind of C, 'k' is Specified.  But what about F?
In the kind of F,

 * Should k be Inferred or Specified?  It's Specified for C,
   but not mentioned in F's declaration.

 * In which order should the Specified variables a and b occur?
   It's clearly 'a' then 'b' in C's declaration, but the L-R ordering
   in F's declaration is 'b' then 'a'.

In both cases we make the choice by looking at F's declaration alone,
so it gets the kind
   F :: forall {k}. forall b a. b a -> Type

How it works
~~~~~~~~~~~~
These design choices are implemented by two completely different code
paths for

  * Declarations with a compulete user-specified kind signature (CUSK)
    Handed by the CUSK case of kcLHsQTyVars.

  * Declarations without a CUSK are handled by kcTyClDecl; see
    Note [Inferring kinds for type declarations].

Note that neither code path worries about point (4) above, as this
Tobias Dammers's avatar
Tobias Dammers committed
730
is nicely handled by not mangling the res_kind. (Mangling res_kinds is done
731 732 733 734 735 736 737 738 739 740 741
*after* all this stuff, in tcDataDefn's call to etaExpandAlgTyCon.)

We can tell Inferred apart from Specified by looking at the scoped
tyvars; Specified are always included there.

Design alternatives
~~~~~~~~~~~~~~~~~~~

* For associated types we considered putting the class variables
  before the local variables, in a nod to the treatment for class
  methods. But it got too compilicated; see Trac #15592, comment:21ff.
Tobias Dammers's avatar
Tobias Dammers committed
742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757

* We rigidly require the ordering above, even though we could be much more
  permissive. Relevant musings are at
  https://ghc.haskell.org/trac/ghc/ticket/15743#comment:7
  The bottom line conclusion is that, if the user wants a different ordering,
  then can specify it themselves, and it is better to be predictable and dumb
  than clever and capricious.

  I (Richard) conjecture we could be fully permissive, allowing all classes
  of variables to intermix. We would have to augment ScopedSort to refuse to
  reorder Required variables (or check that it wouldn't have). But this would
  allow more programs. See #15743 for examples. Interestingly, Idris seems
  to allow this intermixing. The intermixing would be fully specified, in that
  we can be sure that inference wouldn't change between versions. However,
  would users be able to predict it? That I cannot answer.

758 759
Test cases (and tickets) relevant to these design decisions
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Tobias Dammers's avatar
Tobias Dammers committed
760 761 762
  T15591*
  T15592*
  T15743*
763

764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845
Note [Inferring kinds for type declarations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This note deals with /inference/ for type declarations
that do not have a CUSK.  Consider
  data T (a :: k1) k2 (x :: k2) = MkT (S a k2 x)
  data S (b :: k3) k4 (y :: k4) = MkS (T b k4 y)

We do kind inference as follows:

* Step 1: Assign initial monomorophic kinds to S, T
          S :: kk1 -> * -> kk2 -> *
          T :: kk3 -> * -> kk4 -> *
  Here kk1 etc are TyVarTvs: that is, unification variables that
  are allowed to unify only with other type variables. See
  Note [Signature skolems] in TcType

* Step 2: Extend the environment with a TcTyCon for S and T, with
  these monomophic kinds.  Now kind-check the declarations, and solve
  the resulting equalities.  The goal here is to discover constraints
  on all these unification variables.

  Here we find that kk1 := kk3, and kk2 := kk4.

  This is why we can't use skolems for kk1 etc; they have to
  unify with each other.

* Step 3. Generalise each TyCon in turn (generaliseTcTyCon).
  We find the free variables of the kind, skolemise them,
  sort them out into Inferred/Required/Specified (see the above
  Note [Required, Specified, and Inferred for types]),
  and perform some validity checks.

  This makes the utterly-final TyConBinders for the TyCon

  All this is very similar at the level of terms: see TcBinds
  Note [Quantified variables in partial type signatures]

* Step 4.  Extend the type environment with a TcTyCon for S and T, now
  with their utterly-final polymorphic kinds (needed for recursive
  occurrences of S, T).  Now typecheck the declarations, and build the
  final AlgTyCOn for S and T resp.

The first three steps are in kcTyClGroup;
the fourth is in tcTyClDecls.

There are some wrinkles

* Do not default TyVarTvs.  We always want to kind-generalise over
  TyVarTvs, and /not/ default them to Type. By definition a TyVarTv is
  not allowed to unify with a type; it must stand for a type
  variable. Hence the check in TcSimplify.defaultTyVarTcS, and
  TcMType.defaultTyVar.  Here's another example (Trac #14555):
     data Exp :: [TYPE rep] -> TYPE rep -> Type where
        Lam :: Exp (a:xs) b -> Exp xs (a -> b)
  We want to kind-generalise over the 'rep' variable.
  Trac #14563 is another example.

* Duplicate type variables. Consider Trac #11203
    data SameKind :: k -> k -> *
    data Q (a :: k1) (b :: k2) c = MkQ (SameKind a b)
  Here we will unify k1 with k2, but this time doing so is an error,
  because k1 and k2 are bound in the same declaration.

  We spot this during validity checking (findDupTyVarTvs),
  in generaliseTcTyCon.

* Required arguments.  Even the Required arguments should be made
  into TyVarTvs, not skolems.  Consider
    data T k (a :: k)
  Here, k is a Required, dependent variable. For uniformity, it is helpful
  to have k be a TyVarTv, in parallel with other dependent variables.

* Duplicate skolemisation is expected.  When generalising in Step 3,
  we may find that one of the variables we want to quantify has
  already been skolemised.  For example, suppose we have already
  generalise S. When we come to T we'll find that kk1 (now the same as
  kk3) has already been skolemised.

  That's fine -- but it means that
    a) when collecting quantification candidates, in
       candidateQTyVarsOfKind, we must collect skolems
    b) quantifyTyVars should be a no-op on such a skolem
846 847
-}

848
--------------
849 850 851
tcExtendKindEnvWithTyCons :: [TcTyCon] -> TcM a -> TcM a
tcExtendKindEnvWithTyCons tcs
  = tcExtendKindEnvList [ (tyConName tc, ATcTyCon tc) | tc <- tcs ]
852 853

--------------
854
mkPromotionErrorEnv :: [LTyClDecl GhcRn] -> TcTypeEnv
855 856 857
-- Maps each tycon/datacon to a suitable promotion error
--    tc :-> APromotionErr TyConPE
--    dc :-> APromotionErr RecDataConPE
858
--    See Note [Recursion and promoting data constructors]
859 860 861 862 863

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

864
mk_prom_err_env :: TyClDecl GhcRn -> TcTypeEnv
865 866 867 868
mk_prom_err_env (ClassDecl { tcdLName = L _ nm, tcdATs = ats })
  = unitNameEnv nm (APromotionErr ClassPE)
    `plusNameEnv`
    mkNameEnv [ (name, APromotionErr TyConPE)
869
              | (dL->L _ (FamilyDecl { fdLName = (dL->L _ name) })) <- ats ]
870

871
mk_prom_err_env (DataDecl { tcdLName = (dL->L _ name)
872 873 874 875
                          , tcdDataDefn = HsDataDefn { dd_cons = cons } })
  = unitNameEnv name (APromotionErr TyConPE)
    `plusNameEnv`
    mkNameEnv [ (con, APromotionErr RecDataConPE)
876 877
              | (dL->L _ con') <- cons
              , (dL->L _ con)  <- getConNames con' ]
878 879 880 881 882 883

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

--------------
884
getInitialKinds :: Bool -> [LTyClDecl GhcRn] -> TcM [TcTyCon]
885 886
-- Returns a TcTyCon for each TyCon bound by the decls,
-- each with its initial kind
887

888 889 890 891 892
getInitialKinds cusk decls
  = do { traceTc "getInitialKinds {" empty
       ; tcs <- concatMapM (addLocM (getInitialKind cusk)) decls
       ; traceTc "getInitialKinds done }" empty
       ; return tcs }
893

894
getInitialKind :: Bool -> TyClDecl GhcRn -> TcM [TcTyCon]
dreixel's avatar
dreixel committed
895
-- Allocate a fresh kind variable for each TyCon and Class
896
-- For each tycon, return a TcTyCon with kind k
897
-- where k is the kind of tc, derived from the LHS
898 899
--         of the definition (and probably including
--         kind unification variables)
dreixel's avatar
dreixel committed
900
--      Example: data T a b = ...
901
--      return (T, kv1 -> kv2 -> kv3)
dreixel's avatar
dreixel committed
902
--
903 904 905 906
-- 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
--
907
-- No family instances are passed to getInitialKinds
dreixel's avatar
dreixel committed
908

909 910 911 912 913
getInitialKind cusk
    (ClassDecl { tcdLName = dL->L _ name
               , tcdTyVars = ktvs
               , tcdATs = ats })
  = do { tycon <- kcLHsQTyVars name ClassFlavour cusk ktvs $
914
                  return constraintKind
915
       ; let parent_tv_prs = tcTyConScopedTyVars tycon
916
            -- See Note [Don't process associated types in kcLHsQTyVars]
917
       ; inner_tcs <- tcExtendNameTyVarEnv parent_tv_prs $
918
                      getFamDeclInitialKinds cusk (Just tycon) ats
919
       ; return (tycon : inner_tcs) }
920

921 922 923 924 925 926 927 928 929 930 931 932
getInitialKind cusk
    (DataDecl { tcdLName = dL->L _ name
              , tcdTyVars = ktvs
              , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
                                         , dd_ND = new_or_data } })
  = do  { let flav = newOrDataToFlavour new_or_data
        ; tc <- kcLHsQTyVars name flav cusk ktvs $
                case m_sig of
                   Just ksig -> tcLHsKindSig (DataKindCtxt name) ksig
                   Nothing   -> return liftedTypeKind
        ; return [tc] }

933 934
getInitialKind cusk (FamDecl { tcdFam = decl })
  = do { tc <- getFamDeclInitialKind cusk Nothing decl
935
       ; return [tc] }
936

937
getInitialKind cusk (SynDecl { tcdLName = dL->L _ name
938 939
                             , tcdTyVars = ktvs
                             , tcdRhs = rhs })
940 941 942 943
  = do  { tycon <- kcLHsQTyVars name TypeSynonymFlavour cusk ktvs $
                   case kind_annotation rhs of
                     Just ksig -> tcLHsKindSig (TySynKindCtxt name) ksig
                     Nothing   -> newMetaKindVar
944
        ; return [tycon] }
945 946
  where
    -- Keep this synchronized with 'hsDeclHasCusk'.
947
    kind_annotation (dL->L _ ty) = case ty of
948 949 950
        HsParTy _ lty     -> kind_annotation lty
        HsKindSig _ _ k   -> Just k
        _                 -> Nothing
951

952 953
getInitialKind _ (DataDecl _ _ _ _ (XHsDataDefn _)) = panic "getInitialKind"
getInitialKind _ (XTyClDecl _) = panic "getInitialKind"
954

955
---------------------------------
956
getFamDeclInitialKinds
957 958
  :: Bool        -- ^ True <=> cusk
  -> Maybe TyCon -- ^ Just cls <=> this is an associated family of class cls
959 960
  -> [LFamilyDecl GhcRn]
  -> TcM [TcTyCon]
961 962
getFamDeclInitialKinds cusk mb_parent_tycon decls
  = mapM (addLocM (getFamDeclInitialKind cusk mb_parent_tycon)) decls
963 964

getFamDeclInitialKind
965 966
  :: Bool        -- ^ True <=> cusk
  -> Maybe TyCon -- ^ Just cls <=> this is an associated family of class cls
967 968
  -> FamilyDecl GhcRn
  -> TcM TcTyCon
969
getFamDeclInitialKind parent_cusk mb_parent_tycon
970
    decl@(FamilyDecl { fdLName     = (dL->L _ name)
971
                     , fdTyVars    = ktvs
972
                     , fdResultSig = (dL->L _ resultSig)
973
                     , fdInfo      = info })
974
  = kcLHsQTyVars name flav fam_cusk ktvs $
Tobias Dammers's avatar
Tobias Dammers committed
975
    case resultSig of
976 977
      KindSig _ ki                              -> tcLHsKindSig ctxt ki
      TyVarSig _ (dL->L _ (KindedTyVar _ _ ki)) -> tcLHsKindSig ctxt ki
Tobias Dammers's avatar
Tobias Dammers committed
978 979
      _ -- open type families have * return kind by default
        | tcFlavourIsOpen flav              -> return liftedTypeKind
980 981
               -- closed type families have their return kind inferred
               -- by default
Tobias Dammers's avatar
Tobias Dammers committed
982
        | otherwise                         -> newMetaKindVar
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
983
  where
984 985 986
    assoc_with_no_cusk = isJust mb_parent_tycon && not parent_cusk
    fam_cusk = famDeclHasCusk assoc_with_no_cusk decl
    flav = case info of
Tobias Dammers's avatar
Tobias Dammers committed
987 988 989 990
      DataFamily         -> DataFamilyFlavour mb_parent_tycon
      OpenTypeFamily     -> OpenTypeFamilyFlavour mb_parent_tycon
      ClosedTypeFamily _ -> ASSERT( isNothing mb_parent_tycon )
                            ClosedTypeFamilyFlavour
991
    ctxt  = TyFamResKindCtxt name
992
getFamDeclInitialKind _ _ (XFamilyDecl _) = panic "getFamDeclInitialKind"
993

994
------------------------------------------------------------------------
995
kcLTyClDecl :: LTyClDecl GhcRn -> TcM ()
996
  -- See Note [Kind checking for type and class decls]
997
kcLTyClDecl (dL->L loc decl)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
998 999
  = setSrcSpan loc $
    tcAddDeclCtxt decl $
1000
    do { traceTc "kcTyClDecl {" (ppr tc_name)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1001
       ; kcTyClDecl decl
1002 1003 1004
       ; traceTc "kcTyClDecl done }" (ppr tc_name) }
  where
    tc_name = tyClDeclLName decl
1005

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

1012 1013 1014 1015 1016
kcTyClDecl (DataDecl { tcdLName    = (dL->L _ name)
                     , tcdDataDefn = defn })
  | HsDataDefn { dd_cons = cons@((dL->L _ (ConDeclGADT {})) : _)
               , dd_ctxt = (dL->L _ []) } <- defn
  = mapM_ (wrapLocM_ kcConDecl) cons
1017
    -- hs_tvs and dd_kindSig already dealt with in getInitialKind
1018
    -- This must be a GADT-style decl,
1019 1020 1021 1022
    --        (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
1023

1024
  | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
1025
  = bindTyClTyVars name $ \ _ _ ->
1026
    do  { _ <- tcHsContext ctxt
1027
        ; mapM_ (wrapLocM_ kcConDecl) cons }
1028

1029 1030 1031
kcTyClDecl (SynDecl { tcdLName = dL->L _ name, tcdRhs = rhs })
  = bindTyClTyVars name $ \ _ res_kind ->
    discardResult $ tcCheckLHsType rhs res_kind
1032 1033
        -- NB: check against the result kind that we allocated
        -- in getInitialKinds.
1034

1035
kcTyClDecl (ClassDecl { tcdLName = (dL->L _ name)
1036
                      , tcdCtxt = ctxt, tcdSigs = sigs })
1037
  = bindTyClTyVars name $ \ _ _ ->
1038
    do  { _ <- tcHsContext ctxt
1039
        ; mapM_ (wrapLocM_ kc_sig) sigs }
dreixel's avatar
dreixel committed
1040
  where
1041 1042
    kc_sig (ClassOpSig _ _ nms op_ty) = kcHsSigType nms op_ty
    kc_sig _                          = return ()
1043

1044
kcTyClDecl (FamDecl _ (FamilyDecl { fdLName  = (dL->L _ fam_tc_name)
1045
                                  , fdInfo   = fd_info }))
1046 1047 1048 1049
-- closed type families look at their equations, but other families don't
-- do anything here
  = case fd_info of
      ClosedTypeFamily (Just eqns) ->
1050
        do { fam_tc <- kcLookupTcTyCon fam_tc_name
1051
           ; mapM_ (kcTyFamInstEqn fam_tc) eqns }
1052
      _ -> return ()
1053
kcTyClDecl (FamDecl _ (XFamilyDecl _))              = panic "kcTyClDecl"
1054
kcTyClDecl (DataDecl _ _ _ _ (XHsDataDefn _)) = panic "kcTyClDecl"
1055
kcTyClDecl (XTyClDecl _)                            = panic "kcTyClDecl"
dreixel's avatar
dreixel committed
1056 1057

-------------------
1058
kcConDecl :: ConDecl GhcRn -> TcM ()
1059 1060
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
1061
  = addErrCtxt (dataConCtxtName [name]) $
1062 1063
    discardResult                   $
    bindExplicitTKBndrs_Skol ex_tvs $
1064
    do { _ <- tcHsMbContext ex_ctxt
1065 1066 1067 1068
       ; traceTc "kcConDecl {" (ppr name $$ ppr args)
       ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args)
       ; traceTc "kcConDecl }" (ppr name)
       }
1069 1070
              -- We don't need to check the telescope here, because that's
              -- done in tcConDecl
1071

Alan Zimmerman's avatar
Alan Zimmerman committed
1072
kcConDecl (ConDeclGADT { con_names = names
1073 1074
                       , con_qvars = qtvs, con_mb_cxt = cxt
                       , con_args = args, con_res_ty = res_ty })
1075
  | HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = implicit_tkv_nms }
1076 1077 1078 1079 1080 1081 1082 1083 1084
           , 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) $
1085
    discardResult $
1086