TcTyClsDecls.hs 169 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, makeRecoveryTyCon )
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

75
import Control.Monad
76
import Data.Foldable
77
import Data.Function ( on )
78
import Data.List
79
import qualified Data.List.NonEmpty as NE
80
import Data.List.NonEmpty ( NonEmpty(..) )
81 82
import qualified Data.Set as Set

83

Austin Seipp's avatar
Austin Seipp committed
84 85 86
{-
************************************************************************
*                                                                      *
87
\subsection{Type checking for type and class declarations}
Austin Seipp's avatar
Austin Seipp committed
88 89
*                                                                      *
************************************************************************
90

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

109 110 111 112 113 114 115 116 117
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
118
-}
119

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

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

           -- Step 1: Typecheck the type/class declarations
160
       ; traceTc "---- tcTyClGroup ---- {" empty
161
       ; traceTc "Decls for" (ppr (map (tcdName . unLoc) tyclds))
162 163
       ; tyclss <- tcTyClDecls tyclds role_annots

164 165 166 167 168 169
           -- 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)

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)
175
       ; tyclss <- concatMapM checkValidTyCl tyclss
176 177 178 179
       ; traceTc "Done validity check" (ppr tyclss)
       ; mapM_ (recoverM (return ()) . checkValidRoleAnnots role_annots) tyclss
           -- See Note [Check role annotations in a second pass]

180 181
       ; traceTc "---- end tcTyClGroup ---- }" empty

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

           -- Step 4: check instance declarations
188
       ; setGblEnv gbl_env $
189
         tcInstDecls1 instds }
190

191
tcTyClGroup (XTyClGroup _) = panic "tcTyClGroup"
192

193
tcTyClDecls :: [LTyClDecl GhcRn] -> RoleAnnotEnv -> TcM [TyCon]
194
tcTyClDecls tyclds role_annots
195 196
  = 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
197 198
            -- (possibly-polymorphic) kind of each TyCon and Class
            -- See Note [Kind checking for type and class decls]
199 200
         tc_tycons <- kcTyClGroup tyclds
       ; traceTc "tcTyAndCl generalized kinds" (vcat (map ppr_tc_tycon tc_tycons))
dreixel's avatar
dreixel committed
201

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

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

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

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

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

248 249 250 251 252 253 254 255 256
    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)
257

Austin Seipp's avatar
Austin Seipp committed
258 259 260
{-
************************************************************************
*                                                                      *
261
                Kind checking
Austin Seipp's avatar
Austin Seipp committed
262 263
*                                                                      *
************************************************************************
264

265 266 267 268
Note [Kind checking for type and class decls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Kind checking is done thus:

269 270
   1. Make up a kind variable for each parameter of the declarations,
      and extend the kind environment (which is in the TcLclEnv)
271

272
   2. Kind check the declarations
273

274 275
We need to kind check all types in the mutually recursive group
before we know the kind of the type variables.  For example:
276

277 278
  class C a where
     op :: D b => a -> b -> b
279

280 281
  class D c where
     bop :: (Monad c) => ...
282 283 284 285 286

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.

287 288 289 290 291 292
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
293

294
The downside of not directly reading off the kinds of the RHS of
295 296 297 298
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.
299

300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319
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.

320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336
However, we only want to do so when we have PolyKinds.
When we have NoPolyKinds, we don't skip those decls, because we have defaulting
(#16609). Skipping won't bring us more polymorphism when we have defaulting.
Consider

  data T1 a = MkT1 T2        -- No CUSK
  data T2 = MkT2 (T1 Maybe)  -- Has CUSK

If we skip the rhs of T2 during kind-checking, the kind of a remains unsolved.
With PolyKinds, we do generalization to get T1 :: forall a. a -> *. And the
program type-checks.
But with NoPolyKinds, we do defaulting to get T1 :: * -> *. Defaulting happens
in quantifyTyVars, which is called from generaliseTcTyCon. Then type-checking
(T1 Maybe) will throw a type error.

Summary: with PolyKinds, we must skip; with NoPolyKinds, we must /not/ skip.

337 338
Open type families
~~~~~~~~~~~~~~~~~~
339 340 341
This treatment of type synonyms only applies to Haskell 98-style synonyms.
General type functions can be recursive, and hence, appear in `alg_decls'.

342
The kind of an open type family is solely determinded by its kind signature;
343
hence, only kind signatures participate in the construction of the initial
344 345 346 347
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').
348 349 350

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

351
Note [How TcTyCons work]
352
~~~~~~~~~~~~~~~~~~~~~~~~
353 354 355 356 357 358 359 360 361 362 363 364 365 366 367
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
368 369 370 371
          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.

372 373 374 375
      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
376
      S3) We then generalize to get the (non-CUSK) tycon's final, fixed
377 378 379 380 381 382 383 384
          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.

385 386 387 388
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:
389 390 391
      - 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)
392

393 394 395 396 397
    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
398 399 400 401
    TcHsType.splitTelescopeTvs!)

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

404 405 406 407 408 409 410 411
    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.
412

413
See also Note [Type checking recursive type and class declarations].
414

415 416 417 418 419
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)
420

421 422 423 424 425 426 427
We do the following steps:

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

428
  2. kcTyCLGroup
429
      - Do getInitialKinds, which will signal a promotion
430
        error if B is used in any of the kinds needed to initialise
431 432
        B's kind (e.g. (a :: Type)) here

433
      - Extend the type env with these initial kinds (monomorphic for
434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471
        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.
472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494

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.

495
-}
496

497
kcTyClGroup :: [LTyClDecl GhcRn] -> TcM [TcTyCon]
498

dreixel's avatar
dreixel committed
499
-- Kind check this group, kind generalize, and return the resulting local env
500
-- This binds the TyCons and Classes of the group, but not the DataCons
dreixel's avatar
dreixel committed
501
-- See Note [Kind checking for type and class decls]
502
-- and Note [Inferring kinds for type declarations]
503
kcTyClGroup decls
504
  = do  { mod <- getModule
505
        ; traceTc "---- kcTyClGroup ---- {"
506
                  (text "module" <+> ppr mod $$ vcat (map ppr decls))
dreixel's avatar
dreixel committed
507

508
          -- Kind checking;
509 510 511
          --    1. Bind kind variables for decls
          --    2. Kind-check decls
          --    3. Generalise the inferred kinds
dreixel's avatar
dreixel committed
512 513
          -- See Note [Kind checking for type and class decls]

514
        ; cusks_enabled <- xoptM LangExt.CUSKs
515
        ; let (cusk_decls, no_cusk_decls)
516
                 = partition (hsDeclHasCusk cusks_enabled . unLoc) decls
517

518
        ; poly_cusk_tcs <- getInitialKinds True cusk_decls
519

520 521 522 523 524 525 526 527
        ; 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
528

529 530
                  ; traceTc "kcTyClGroup: initial kinds" $
                    ppr_tc_kinds mono_tcs
Tobias Dammers's avatar
Tobias Dammers committed
531

532 533 534 535
                    -- Step 2: Set extended envt, kind-check the decls
                    -- NB: the environment extension overrides the tycon
                    --     promotion-errors bindings
                    --     See Note [Type environment evolution]
536
                  ; poly_kinds  <- xoptM LangExt.PolyKinds
537
                  ; tcExtendKindEnvWithTyCons mono_tcs $
538 539
                    mapM_ kcLTyClDecl (if poly_kinds then no_cusk_decls else decls)
                    -- See Note [Skip decls with CUSKs in kcLTyClDecl]
540 541 542 543

                  ; return mono_tcs }

        -- Step 3: generalisation
Tobias Dammers's avatar
Tobias Dammers committed
544 545 546
        -- Finally, go through each tycon and give it its final kind,
        -- with all the required, specified, and inferred variables
        -- in order.
547
        ; poly_no_cusk_tcs <- mapAndReportM generaliseTcTyCon mono_tcs
548

549
        ; let poly_tcs = poly_cusk_tcs ++ poly_no_cusk_tcs
550 551
        ; traceTc "---- kcTyClGroup end ---- }" (ppr_tc_kinds poly_tcs)
        ; return poly_tcs }
552

553
  where
554 555 556
    ppr_tc_kinds tcs = vcat (map pp_tc tcs)
    pp_tc tc = ppr (tyConName tc) <+> dcolon <+> ppr (tyConKind tc)

557 558 559 560 561
generaliseTcTyCon :: TcTyCon -> TcM TcTyCon
generaliseTcTyCon tc
  -- See Note [Required, Specified, and Inferred for types]
  = setSrcSpan (getSrcSpan tc) $
    addTyConCtxt tc $
562 563 564 565 566 567 568 569 570
    do { let tc_name      = tyConName tc
             tc_res_kind  = tyConResKind tc
             spec_req_prs = tcTyConScopedTyVars tc

             (spec_req_names, spec_req_tvs) = unzip spec_req_prs
             -- NB: spec_req_tvs includes both Specified and Required
             -- Running example in Note [Inferring kinds for type declarations]
             --    spec_req_prs = [ ("k1",kk1), ("a", (aa::kk1))
             --                   , ("k2",kk2), ("x", (xx::kk2))]
571
             -- where "k1" dnotes the Name k1, and kk1, aa, etc are MetaTyVars,
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 598 599 600 601 602 603 604 605 606 607 608 609 610
             -- specifically TyVarTvs

       -- Step 0: zonk and skolemise the Specified and Required binders
       -- It's essential that they are skolems, not MetaTyVars,
       -- for Step 3 to work right
       ; spec_req_tvs <- mapM zonkAndSkolemise spec_req_tvs
             -- Running example, where kk1 := kk2, so we get
             --   [kk2,kk2]

       -- Step 1: 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
       -- If this happens, things get very confused later, so fail fast
       ; checkDuplicateTyConBinders spec_req_names spec_req_tvs

       -- Step 2a: find all the Inferred variables we want to quantify over
       -- NB: candidateQTyVarsOfKinds zonks as it goes
       ; dvs1 <- candidateQTyVarsOfKinds $
                (tc_res_kind : map tyVarKind spec_req_tvs)
       ; let dvs2 = dvs1 `delCandidates` spec_req_tvs

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

       -- Step 3a: rename all the Specified and Required tyvars back to
       -- TyVars with their oroginal user-specified name.  Example
       --     class C a_r23 where ....
       -- By this point we have scoped_prs = [(a_r23, a_r89[TyVarTv])]
       -- We return with the TyVar a_r23[TyVar],
       --    and ze mapping a_r89 :-> a_r23[TyVar]
       ; traceTc "generaliseTcTyCon: before zonkRec"
           (vcat [ text "spec_req_tvs =" <+> pprTyVars spec_req_tvs
                 , text "inferred =" <+> pprTyVars inferred ])
       ; (ze, final_spec_req_tvs) <- zonkRecTyVarBndrs spec_req_names spec_req_tvs
           -- So ze maps from the tyvars that have ended up

       -- Step 3b: Apply that mapping to the other variables
611 612
       -- (remember they all started as TyVarTvs).
       -- They have been skolemised by quantifyTyVars.
613 614
       ; (ze, inferred) <- zonkTyBndrsX ze inferred
       ; tc_res_kind    <- zonkTcTypeToTypeX ze tc_res_kind
615

616
       ; traceTc "generaliseTcTyCon: post zonk" $
617
         vcat [ text "tycon =" <+> ppr tc
618 619 620 621 622
              , text "inferred =" <+> pprTyVars inferred
              , text "ze =" <+> ppr ze
              , text "spec_req_prs =" <+> ppr spec_req_prs
              , text "spec_req_tvs =" <+> pprTyVars spec_req_tvs
              , text "final_spec_req_tvs =" <+> pprTyVars final_spec_req_tvs ]
623 624

       -- Step 4: Find the Specified and Inferred variables
625 626 627 628 629 630
       -- NB: spec_req_tvs = spec_tvs ++ req_tvs
       --     And req_tvs is 1-1 with tyConTyVars
       --     See Note [Scoped tyvars in a TcTyCon] in TyCon
       ; let n_spec        = length final_spec_req_tvs - tyConArity tc
             (spec_tvs, req_tvs) = splitAt n_spec final_spec_req_tvs
             specified     = scopedSort spec_tvs
631 632 633
                             -- NB: maintain the L-R order of scoped_tvs

       -- Step 5: Make the TyConBinders.
634 635
             to_user tv     = lookupTyVarOcc ze tv `orElse` tv
             dep_fv_set     = mapVarSet to_user (candidateKindVars dvs1)
636 637
             inferred_tcbs  = mkNamedTyConBinders Inferred inferred
             specified_tcbs = mkNamedTyConBinders Specified specified
638
             required_tcbs  = map (mkRequiredTyConBinder dep_fv_set) req_tvs
639 640 641 642 643 644 645

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

       -- Step 7: Make the result TcTyCon
646
             tycon = mkTcTyCon tc_name final_tcbs tc_res_kind
647
                            (mkTyVarNamePairs final_spec_req_tvs)
648 649 650
                            True {- it's generalised now -}
                            (tyConFlavour tc)

651
       ; traceTc "generaliseTcTyCon done" $
652 653
         vcat [ text "tycon =" <+> ppr tc
              , text "tc_res_kind =" <+> ppr tc_res_kind
654 655
              , text "dep_fv_set =" <+> ppr dep_fv_set
              , text "final_spec_req_tvs =" <+> pprTyVars final_spec_req_tvs
656 657 658 659 660
              , text "inferred =" <+> pprTyVars inferred
              , text "specified =" <+> pprTyVars specified
              , text "required_tcbs =" <+> ppr required_tcbs
              , text "final_tcbs =" <+> ppr final_tcbs ]

661 662 663 664
       -- Step 8: Check for validity.
       -- We do this here because we're about to put the tycon into the
       -- the environment, and we don't want anything malformed there
       ; checkTyConTelescope tycon
dreixel's avatar
dreixel committed
665

666
       ; return tycon }
667 668 669 670 671

checkDuplicateTyConBinders :: [Name] -> [TcTyVar] -> TcM ()
checkDuplicateTyConBinders spec_req_names spec_req_tvs
  | null dups = return ()
  | otherwise = mapM_ report_dup dups >> failM
672
  where
673 674 675 676
    dups :: [(Name,Name)]
    dups = findDupTyVarTvs $ spec_req_names `zip` spec_req_tvs

    report_dup (n1, n2)
677 678 679
      = setSrcSpan (getSrcSpan n2) $
        addErrTc (text "Couldn't match" <+> quotes (ppr n1)
                        <+> text "with" <+> quotes (ppr n2))
680

681 682 683
{- Note [Required, Specified, and Inferred for types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Each forall'd type variable in a type or kind is one of
684

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

687 688
  * Specified: the argument can be inferred at call sites, but
    may be instantiated with visible type/kind application
689

690 691
  * Inferred: the must be inferred at call sites; it
    is unavailable for use with visible type/kind application.
692

693 694 695 696
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.
697

698
Go read Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep.
699

700 701 702 703 704 705 706 707 708 709 710 711 712 713 714
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
715 716 717

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

718 719 720 721
Example:
  data SameKind :: k -> k -> *
  data Bad a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)

722
For Bad:
723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740
  - 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.
741
Here is an example (#15592)
742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763
  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

764
  * Declarations with a complete user-specified kind signature (CUSK)
765 766 767 768 769 770
    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
771
is nicely handled by not mangling the res_kind. (Mangling res_kinds is done
772 773 774 775 776 777 778 779 780
*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
781
  methods. But it got too compilicated; see #15592, comment:21ff.
Tobias Dammers's avatar
Tobias Dammers committed
782 783 784

* We rigidly require the ordering above, even though we could be much more
  permissive. Relevant musings are at
785
  https://gitlab.haskell.org/ghc/ghc/issues/15743#note_161623
Tobias Dammers's avatar
Tobias Dammers committed
786 787 788 789 790 791 792 793 794 795 796 797
  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.

798 799
Test cases (and tickets) relevant to these design decisions
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Tobias Dammers's avatar
Tobias Dammers committed
800 801 802
  T15591*
  T15592*
  T15743*
803

804 805 806 807 808 809 810 811 812
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:

813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835
* Step 1: getInitialKinds, and in particular kcLHsQTyVars_NonCusk.
  Make a unification variable for each of the Required and Specified
  type varialbes in the header.

  Record the connection between the Names the user wrote and the
  fresh unification variables in the tcTyConScopedTyVars field
  of the TcTyCon we are making
      [ (a,  aa)
      , (k1, kk1)
      , (k2, kk2)
      , (x,  xx) ]
  (I'm using the convention that double letter like 'aa' or 'kk'
  mean a unification variable.)

  These unification variables
    - Are TyVarTvs: that is, unification variables that can
      unify only with other type variables.
      See Note [Signature skolems] in TcType

    - Have complete fresh Names; see TcMType
      Note [Unification variables need fresh Names]

  Assign initial monomorophic kinds to S, T
836 837
          T :: kk1 -> * -> kk2 -> *
          S :: kk3 -> * -> kk4 -> *
838

839 840 841 842
* Step 2: kcTyClDecl. 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.
843 844 845 846 847 848

  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.

849
* Step 3: generaliseTcTyCon. Generalise each TyCon in turn.
850 851 852 853 854
  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.

855
  This makes the utterly-final TyConBinders for the TyCon.
856 857 858 859

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

860 861
  But there some tricky corners: Note [Tricky scoping in generaliseTcTyCon]

862 863 864 865 866
* 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.

867 868
The first three steps are in kcTyClGroup; the fourth is in
tcTyClDecls.
869 870 871 872 873 874 875

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
876
  TcMType.defaultTyVar.  Here's another example (#14555):
877 878 879
     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.
880
  #14563 is another example.
881

882
* Duplicate type variables. Consider #11203
883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906
    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
907 908 909

Note [Tricky scoping in generaliseTcTyCon]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
910
Consider #16342
911 912 913 914 915 916 917 918 919 920 921 922 923 924 925
  class C (a::ka) x where
    cop :: D a x => x -> Proxy a -> Proxy a
    cop _ x = x :: Proxy (a::ka)

  class D (b::kb) y where
    dop :: C b y => y -> Proxy b -> Proxy b
    dop _ x = x :: Proxy (b::kb)

C and D are mutually recursive, by the time we get to
generaliseTcTyCon we'll have unified kka := kkb.

But when typechecking the default declarations for 'cop' and 'dop' in
tcDlassDecl2 we need {a, ka} and {b, kb} respectively to be in scope.
But at that point all we have is the utterly-final Class itself.

926
Conclusion: the classTyVars of a class must have the same Name as
927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951
that originally assigned by the user.  In our example, C must have
classTyVars {a, ka, x} while D has classTyVars {a, kb, y}.  Despite
the fact that kka and kkb got unified!

We achieve this sleight of hand in generaliseTcTyCon, using
the specialised function zonkRecTyVarBndrs.  We make the call
   zonkRecTyVarBndrs [ka,a,x] [kkb,aa,xxx]
where the [ka,a,x] are the Names originally assigned by the user, and
[kkb,aa,xx] are the corresponding (post-zonking, skolemised) TcTyVars.
zonkRecTyVarBndrs builds a recursive ZonkEnv that binds
   kkb :-> (ka :: <zonked kind of kkb>)
   aa  :-> (a  :: <konked kind of aa>)
   etc
That is, it maps each skolemised TcTyVars to the utterly-final
TyVar to put in the class, with its correct user-specified name.
When generalising D we'll do the same thing, but the ZonkEnv will map
   kkb :-> (kb :: <zonked kind of kkb>)
   bb  :-> (b  :: <konked kind of bb>)
   etc
Note that 'kkb' again appears in the domain of the mapping, but this
time mapped to 'kb'.  That's how C and D end up with differently-named
final TyVars despite the fact that we unified kka:=kkb

zonkRecTyVarBndrs we need to do knot-tying because of the need to
apply this same substitution to the kind of each.  -}
952

953
--------------
954 955 956
tcExtendKindEnvWithTyCons :: [TcTyCon] -> TcM a -> TcM a
tcExtendKindEnvWithTyCons tcs
  = tcExtendKindEnvList [ (tyConName tc, ATcTyCon tc) | tc <- tcs ]
957 958

--------------
959
mkPromotionErrorEnv :: [LTyClDecl GhcRn] -> TcTypeEnv
960 961 962
-- Maps each tycon/datacon to a suitable promotion error
--    tc :-> APromotionErr TyConPE
--    dc :-> APromotionErr RecDataConPE
963
--    See Note [Recursion and promoting data constructors]
964 965 966 967 968

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

969
mk_prom_err_env :: TyClDecl GhcRn -> TcTypeEnv
970 971 972 973
mk_prom_err_env (ClassDecl { tcdLName = L _ nm, tcdATs = ats })
  = unitNameEnv nm (APromotionErr ClassPE)
    `plusNameEnv`
    mkNameEnv [ (name, APromotionErr TyConPE)
974
              | (dL->L _ (FamilyDecl { fdLName = (dL->L _ name) })) <- ats ]
975

976
mk_prom_err_env (DataDecl { tcdLName = (dL->L _ name)
977 978 979 980
                          , tcdDataDefn = HsDataDefn { dd_cons = cons } })
  = unitNameEnv name (APromotionErr TyConPE)
    `plusNameEnv`
    mkNameEnv [ (con, APromotionErr RecDataConPE)
981 982
              | (dL->L _ con') <- cons
              , (dL->L _ con)  <- getConNames con' ]
983 984 985 986 987 988

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

--------------
989
getInitialKinds :: Bool -> [LTyClDecl GhcRn] -> TcM [TcTyCon]
990 991
-- Returns a TcTyCon for each TyCon bound by the decls,
-- each with its initial kind
992

993 994 995 996 997
getInitialKinds cusk decls
  = do { traceTc "getInitialKinds {" empty
       ; tcs <- concatMapM (addLocM (getInitialKind cusk)) decls
       ; traceTc "getInitialKinds done }" empty
       ; return tcs }
998

999
getInitialKind :: Bool -> TyClDecl GhcRn -> TcM [TcTyCon]
dreixel's avatar
dreixel committed
1000
-- Allocate a fresh kind variable for each TyCon and Class
1001
-- For each tycon, return a TcTyCon with kind k
1002
-- where k is the kind of tc, derived from the LHS
1003 1004
--         of the definition (and probably including
--         kind unification variables)
dreixel's avatar
dreixel committed
1005
--      Example: data T a b = ...
1006
--      return (T, kv1 -> kv2 -> kv3)
dreixel's avatar
dreixel committed
1007
--
1008 1009 1010 1011
-- 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
--
1012
-- No family instances are passed to getInitialKinds
dreixel's avatar
dreixel committed
1013

1014 1015 1016 1017 1018
getInitialKind cusk
    (ClassDecl { tcdLName = dL->L _ name
               , tcdTyVars = ktvs
               , tcdATs = ats })
  = do { tycon <- kcLHsQTyVars name ClassFlavour cusk ktvs $
1019
                  return constraintKind
1020
       ; let parent_tv_prs = tcTyConScopedTyVars tycon
1021
            -- See Note [Don't process associated types in kcLHsQTyVars]
1022
       ; inner_tcs <- tcExtendNameTyVarEnv parent_tv_prs $
1023
                      getFamDeclInitialKinds cusk (Just tycon) ats
1024
       ; return (tycon : inner_tcs) }
1025

1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037
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] }

1038 1039
getInitialKind cusk (FamDecl { tcdFam = decl })
  = do { tc <- getFamDeclInitialKind cusk Nothing decl
1040
       ; return [tc] }
1041

1042
getInitialKind cusk (SynDecl { tcdLName = dL->L _ name
1043 1044
                             , tcdTyVars = ktvs
                             , tcdRhs = rhs })
1045 1046 1047
  = do  { cusks_enabled <- xoptM LangExt.CUSKs
        ; tycon <- kcLHsQTyVars name TypeSynonymFlavour cusk ktvs $
                   case kind_annotation cusks_enabled rhs of
1048
                     Just ksig -> tcLHsKindSig (TySynKindCtxt name) ksig
1049
                     Nothing -> newMetaKindVar
1050
        ; return [tycon] }
1051 1052
  where
    -- Keep this synchronized with 'hsDeclHasCusk'.
1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063
    kind_annotation
      :: Bool           --  cusks_enabled?
      -> LHsType GhcRn  --  rhs
      -> Maybe (LHsKind GhcRn)
    kind_annotation False = const Nothing
    kind_annotation True = go
      where
        go (dL->L _ ty) = case ty of
          HsParTy _ lty     -> go lty
          HsKindSig _ _ k   -> Just k
          _                 -> Nothing
1064

1065 1066
getInitialKind _ (DataDecl _ _ _ _ (XHsDataDefn _)) = panic "getInitialKind"
getInitialKind _ (XTyClDecl _) = panic "getInitialKind"
1067

1068
---------------------------------
1069
getFamDeclInitialKinds
1070 1071
  :: Bool        -- ^ True <=> cusk
  -> Maybe TyCon -- ^ Just cls <=> this is an associated family of class cls
1072 1073
  -> [LFamilyDecl GhcRn]
  -> TcM [TcTyCon]
1074 1075
getFamDeclInitialKinds cusk mb_parent_tycon decls
  = mapM (addLocM (getFamDeclInitialKind cusk mb_parent_tycon)) decls
1076 1077

getFamDeclInitialKind
1078 1079
  :: Bool        -- ^ True <=> cusk
  -> Maybe TyCon -- ^ Just cls <=> this is an associated family of class cls
1080 1081
  -> FamilyDecl GhcRn
  -> TcM TcTyCon
1082
getFamDeclInitialKind parent_cusk mb_parent_tycon
1083
    decl@(FamilyDecl { fdLName     = (dL->L _ name)
1084
                     , fdTyVars    = ktvs
1085
                     , fdResultSig = (dL->L _ resultSig)
1086
                     , fdInfo      = info })
1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097
  = do { cusks_enabled <- xoptM LangExt.CUSKs
       ; kcLHsQTyVars name flav (fam_cusk cusks_enabled) ktvs $
         case resultSig of
           KindSig _ ki                              -> tcLHsKindSig ctxt ki
           TyVarSig _ (dL->L _ (KindedTyVar _ _ ki)) -> tcLHsKindSig ctxt ki
           _ -- open type families have * return kind by default
             | tcFlavourIsOpen flav              -> return liftedTypeKind
                    -- closed type families have their return kind inferred
                    -- by default
             | otherwise                         -> newMetaKindVar
       }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1098
  where
1099
    assoc_with_no_cusk = isJust mb_parent_tycon && not parent_cusk
1100
    fam_cusk cusks_enabled = famDeclHasCusk cusks_enabled assoc_with_no_cusk decl
1101
    flav = case info of
Tobias Dammers's avatar
Tobias Dammers committed
1102 1103 1104 1105
      DataFamily         -> DataFamilyFlavour mb_parent_tycon
      OpenTypeFamily     -> OpenTypeFamilyFlavour mb_parent_tycon
      ClosedTypeFamily _ -> ASSERT( isNothing mb_parent_tycon )
                            ClosedTypeFamilyFlavour
1106
    ctxt  = TyFamResKindCtxt name
1107
getFamDeclInitialKind _ _ (XFamilyDecl _) = panic "getFamDeclInitialKind"
1108

1109
------------------------------------------------------------------------
1110
kcLTyClDecl :: LTyClDecl GhcRn -> TcM ()
1111
  -- See Note [Kind checking for type and class decls]
1112
kcLTyClDecl (dL->L loc decl)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1113 1114
  = setSrcSpan loc $
    tcAddDeclCtxt decl $
1115
    do { traceTc "kcTyClDecl {" (ppr tc_name)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1116
       ; kcTyClDecl decl
1117 1118 1119
       ; traceTc "kcTyClDecl done }" (ppr tc_name) }
  where
    tc_name = tyClDeclLName decl
1120

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

1127 1128 1129 1130 1131
kcTyClDecl (DataDecl { tcdLName    = (dL->L _ name)
                     , tcdDataDefn = defn })
  | HsDataDefn { dd_cons = cons@((dL->L _ (ConDeclGADT {})) : _)
               , dd_ctxt = (dL->L _ []) } <- defn
  = mapM_ (wrapLocM_ kcConDecl) cons
1132
    -- hs_tvs and dd_kindSig already dealt with in getInitialKind
1133
    -- This must be a GADT-style decl,
1134 1135 1136 1137
    --        (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
1138

1139
  | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
1140
  = bindTyClTyVars name $ \ _ _ ->
1141
    do  { _ <- tcHsContext ctxt
1142
        ; mapM_ (wrapLocM_ kcConDecl) cons }
1143

1144 1145 1146
kcTyClDecl (SynDecl { tcdLName = dL->L _ name, tcdRhs = rhs })
  = bindTyClTyVars name $ \ _ res_kind ->
    discardResult $ tcCheckLHsType rhs res_kind
1147 1148
        -- NB: check against the result kind that we allocated
        -- in getInitialKinds.
1149

1150
kcTyClDecl (ClassDecl { tcdLName = (dL->L _ name)
1151
                      , tcdCtxt = ctxt, tcdSigs = sigs })
1152
  = bindTyClTyVars name $ \ _ _ ->
1153
    do  { _ <- tcHsContext ctxt
1154
        ; mapM_ (wrapLocM_ kc_sig) sigs }
dreixel's avatar
dreixel committed
1155
  where
1156
    kc_sig (ClassOpSig _ _ nms op_ty) = kcClassSigType skol_info nms op_ty
1157
    kc_sig _                          = return ()
1158

1159 1160
    skol_info = TyConSkol ClassFlavour name

1161
kcTyClDecl (FamDecl _ (FamilyDecl { fdLName  = (dL->L _ fam_tc_name)
1162
                                  , fdInfo   = fd_info }))
1163 1164 1165 1166
-- closed type families look at their equations, but other families don't
-- do anything here
  = case fd_info of
      ClosedTypeFamily (Just eqns) ->
1167
        do { fam_tc <- kcLookupTcTyCon fam_tc_name
1168
           ; mapM_ (kcTyFamInstEqn fam_tc) eqns }
1169
      _ -> return ()
1170
kcTyClDecl (FamDecl _ (XFamilyDecl _))              = panic "kcTyClDecl"
1171
kcTyClDecl (DataDecl _ _ _ _ (XHsDataDefn _)) = panic "kcTyClDecl"
1172
kcTyClDecl (XTyClDecl _)                            = panic "kcTyClDecl"
dreixel's avatar
dreixel committed
1173 1174

-------------------
1175
kcConDecl :: ConDecl GhcRn -> TcM ()
1176 1177
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
1178
  = addErrCtxt (dataConCtxtName [name]) $
1179
    discardResult                   $