TcTyClsDecls.hs 162 KB
Newer Older
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
7
-}
8

9
{-# LANGUAGE CPP, TupleSections, MultiWayIf #-}
10
{-# LANGUAGE TypeFamilies #-}
11
{-# LANGUAGE ViewPatterns #-}
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 22
        unravelFamInstPats,
        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 42
import ClsInst( AssocInstInfo(..) )
import Inst( tcInstTyBinders )
43
import TcMType
44
import TysWiredIn ( unitTy )
45
import TcType
46
import RnEnv( lookupConstructorFields )
47
import FamInst
Jan Stolarek's avatar
Jan Stolarek committed
48
import FamInstEnv
49
import Coercion
50
import Type
51
import TyCoRep   -- for checkValidRoles
52
import Class
53
import CoAxiom
54 55
import TyCon
import DataCon
56
import Id
57
import Var
58
import VarEnv
59
import VarSet
60
import Module
61
import Name
62
import NameSet
63
import NameEnv
64
import Outputable
65 66 67 68 69 70
import Maybes
import Unify
import Util
import SrcLoc
import ListSetOps
import DynFlags
71
import Unique
72
import ConLike( ConLike(..) )
73
import BasicTypes
74
import qualified GHC.LanguageExtensions as LangExt
75

76
import Control.Monad
77
import Data.List
78
import Data.List.NonEmpty ( NonEmpty(..) )
79 80
import qualified Data.Set as Set

81

82 83 84
{-
************************************************************************
*                                                                      *
85
\subsection{Type checking for type and class declarations}
86 87
*                                                                      *
************************************************************************
88

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

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

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

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

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

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

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

178 179
       ; traceTc "---- end tcTyClGroup ---- }" empty

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

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

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

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

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

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

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

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

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

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

256 257 258
{-
************************************************************************
*                                                                      *
259
                Kind checking
260 261
*                                                                      *
************************************************************************
262

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

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

270
   2. Kind check the declarations
271

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

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

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

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.

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

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

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

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

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

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

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

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

366 367 368 369
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:
370 371 372
      - 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)
373

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

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

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

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

396 397 398 399 400
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)
401

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

414
      - Extend the type env with these initial kinds (monomorphic for
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 452
        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.
453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475

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.

476
-}
477

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

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

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

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

498
        ; poly_cusk_tcs <- getInitialKinds True cusk_decls
499

500 501 502 503 504 505 506 507
        ; 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
508

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

512 513 514 515 516 517 518 519 520 521
                    -- 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
522 523 524
        -- Finally, go through each tycon and give it its final kind,
        -- with all the required, specified, and inferred variables
        -- in order.
525
        ; poly_no_cusk_tcs <- mapAndReportM generaliseTcTyCon mono_tcs
526

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

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

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 598 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 632 633
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
             user_tyvars = tcTyConUserTyVars tc  -- ToDo: nuke

             (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
             tycon = mkTcTyCon tc_name user_tyvars final_tcbs tc_res_kind
                            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
634

635 636 637 638 639 640
       ; 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))
641

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

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

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

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

654 655 656 657
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.
658

659
Go read Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep.
660

661 662 663 664 665 666 667 668 669 670 671 672 673 674 675
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
676 677 678

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

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 730 731
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
732
is nicely handled by not mangling the res_kind. (Mangling res_kinds is done
733 734 735 736 737 738 739 740 741 742 743
*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
744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759

* 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.

760 761
Test cases (and tickets) relevant to these design decisions
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Tobias Dammers's avatar
Tobias Dammers committed
762 763 764
  T15591*
  T15592*
  T15743*
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 846 847
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
848 849
-}

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

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

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

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

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

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

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

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

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

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

923 924 925 926 927 928 929 930 931 932 933 934 935
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] }

getInitialKind _ (FamDecl { tcdFam = decl })
936 937
  = do { tc <- getFamDeclInitialKind Nothing decl
       ; return [tc] }
938

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

954 955
getInitialKind _ (DataDecl _ _ _ _ (XHsDataDefn _)) = panic "getInitialKind"
getInitialKind _ (XTyClDecl _) = panic "getInitialKind"
956

957
---------------------------------
958
getFamDeclInitialKinds
Tobias Dammers's avatar
Tobias Dammers committed
959
  :: Maybe TcTyCon -- ^ Enclosing class TcTyCon, if any
960 961
  -> [LFamilyDecl GhcRn]
  -> TcM [TcTyCon]
Tobias Dammers's avatar
Tobias Dammers committed
962 963
getFamDeclInitialKinds mb_parent_tycon decls
  = mapM (addLocM (getFamDeclInitialKind mb_parent_tycon)) decls
964 965

getFamDeclInitialKind
Tobias Dammers's avatar
Tobias Dammers committed
966
  :: Maybe TcTyCon -- ^ Enclosing class TcTyCon, if any
967 968
  -> FamilyDecl GhcRn
  -> TcM TcTyCon
Tobias Dammers's avatar
Tobias Dammers committed
969
getFamDeclInitialKind mb_parent_tycon
970
    decl@(FamilyDecl { fdLName     = (dL->L _ name)
971
                     , fdTyVars    = ktvs
972
                     , fdResultSig = (dL->L _ resultSig)
973
                     , fdInfo      = info })
Tobias Dammers's avatar
Tobias Dammers committed
974 975
  = kcLHsQTyVars name flav cusk ktvs $
    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
Tobias Dammers's avatar
Tobias Dammers committed
984 985
    mb_cusk = tcTyConIsPoly <$> mb_parent_tycon
    cusk    = famDeclHasCusk mb_cusk decl
986
    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)
998 999
  = setSrcSpan loc $
    tcAddDeclCtxt decl $
1000
    do { traceTc "kcTyClDecl {" (ppr tc_name)
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 1087 1088
    bindImplicitTKBndrs_Tv implicit_tkv_nms $
    bindExplicitTKBndrs_Tv explicit_tkv_nms $
        -- Why "_Tv"?  See Note [Kind-checking for GADTs]
1089 1090 1091 1092
    do { _ <- tcHsMbContext cxt
       ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args)
       ; _ <- tcHsOpenType res_ty
       ; return () }
1093 1094
kcConDecl (XConDecl _) = panic "kcConDecl"
kcConDecl (ConDeclGADT _ _ _ (XLHsQTyVars _) _ _ _ _) = panic "kcConDecl"
Alan Zimmerman's avatar
Alan Zimmerman committed
1095

1096
{-
1097 1098
Note [Recursion and promoting data constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1099 1100 1101 1102 1103 1104 1105 1106
We don't want to allow promotion in a strongly connected component
when kind checking.

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

When kind checking the `data T' declaration the local env contains the
mappings:
1107 1108
  T -> ATcTyCon <some initial kind>
  K -> APromotionErr
1109

1110
APromotionErr is only used for DataCons, and only used during type checking
1111 1112
in tcTyClGroup.

1113 1114
Note [Kind-checking for GADTs]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1115 1116 1117 1118 1119 1120 1121 1122 1123
Consider

  data Proxy a where
    MkProxy1 :: forall k (b :: k). Proxy b
    MkProxy2 :: forall j (c :: j). Proxy c

It seems reasonable that this should be accepted. But something very strange
is going on here: when we're kind-checking this declaration, we need to unify
the kind of `a` with k and j -- even though k and j's scopes are local to the type of
1124
MkProxy{1,2}. The best approach we've come up with is to use TyVarTvs during
1125 1126 1127 1128 1129 1130 1131 1132
the kind-checking pass. First off, note that it's OK if the kind-checking pass
is too permissive: we'll snag the problems in the type-checking pass later.
(This extra permissiveness might happen with something like

  data SameKind :: k -> k -> Type
  data Bad a where
    MkBad :: forall k1 k2 (a :: k1) (b :: k2). Bad (SameKind a b)

1133 1134
which would be accepted if k1 and k2 were TyVarTvs. This is correctly rejected
in the second pass, though. Test case: polykinds/TyVarTvKinds3)
1135 1136 1137
Recall that the kind-checking pass exists solely to collect constraints
on the kinds and to power unification.

1138 1139
To achieve the use of TyVarTvs, we must be careful to use specialized functions
that produce TyVarTvs, not ordinary skolems. This is why we need
1140 1141 1142 1143 1144 1145
kcExplicitTKBndrs and kcImplicitTKBndrs in TcHsType, separate from their
tc... variants.

The drawback of this approach is sometimes it will accept a definition that
a (hypothetical) declarative specification would likely reject. As a general
rule, we don't want to allow polymorphic recursion without a CUSK. Indeed,
1146
the whole point of CUSKs is to allow polymorphic recursion. Yet, the TyVarTvs
1147 1148 1149 1150 1151 1152 1153 1154 1155
approach allows a limited form of polymorphic recursion *without* a CUSK.

To wit:
  data T a = forall k (b :: k). MkT (T b) Int
  (test case: dependent/should_compile/T14066a)

Note that this is polymorphically recursive, with the recursive occurrence
of T used at a kind other than a's kind. The approach outlined here accepts
this definition, because this kind is still a kind variable (and so the
1156
TyVarTvs unify). Stepping back, I (Richard) have a hard time envisioning a
1157 1158 1159 1160
way to describe exactly what declarations will be accepted and which will
be rejected (without a CUSK). However, the accepted definitions are indeed
well-kinded and any rejected definitions would be accepted with a CUSK,
and so this wrinkle need not cause anyone to lose sleep.
1161

1162 1163
************************************************************************
*                                                                      *
1164
\subsection{Type checking}
1165 1166
*                                                                      *
************************************************************************
1167

dreixel's avatar
dreixel committed
1168 1169 1170 1171
Note [Type checking recursive type and class declarations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
At this point we have completed *kind-checking* of a mutually
recursive group of type/class decls (done in kcTyClGroup). However,
1172
we discarded the kind-checked types (eg RHSs of data type decls);
dreixel's avatar
dreixel committed
1173 1174 1175 1176 1177 1178 1179
note that kcTyClDecl returns ().  There are two reasons:

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

  * It's necessary, because after kind-generalisation, the
    TyCons/Classes may now be kind-polymorphic, and hence need
1180
    to be given kind arguments.
dreixel's avatar
dreixel committed
1181 1182 1183 1184 1185 1186 1187

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

dreixel's avatar
dreixel committed
1189 1190 1191 1192 1193 1194 1195
However, during tcTyClDecl of T (above) we will be in a recursive
"knot". So we aren't allowed to look at the TyCon T itself; we are only
allowed to put it (lazily) in the returned structures.  But when
kind-checking the RHS of T's decl, we *do* need to know T's kind (so
that we can correctly elaboarate (T k f a).  How can we get T's kind
without looking at T?  Delicate answer: during tcTyClDecl, we extend

1196 1197
  *Global* env with T -> ATyCon (the (not yet built) final TyCon for T)
  *Local*  env with T -> ATcTyCon (TcTyCon with the polymorphic kind of T)
dreixel's avatar
dreixel committed
1198 1199 1200

Then:

1201 1202
  * During TcHsType.tcTyVar we look in the *local* env, to get the
    fully-known, not knot-tied TcTyCon for T.
dreixel's avatar
dreixel committed
1203

Simon Peyton Jones's avatar
Simon Peyton Jones committed
1204 1205
  * Then, in TcHsSyn.zonkTcTypeToType (and zonkTcTyCon in particular)
    we look in the *global* env to get the TyCon.
dreixel's avatar
dreixel committed
1206

Gabor Greif's avatar
Gabor Greif committed
1207
This fancy footwork (with two bindings for T) is only necessary for the
dreixel's avatar
dreixel committed
1208 1209
TyCons or Classes of this recursive group.  Earlier, finished groups,
live in the global env only.
1210

1211 1212 1213 1214 1215 1216 1217 1218 1219
See also Note [Kind checking recursive type and class declarations]

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232
The initial kind is stored in exactly the same way during
kind-checking as it is during type-checking (Note [Type checking
recursive type and class declarations]): in the *local* environment,
with ATcTyCon. But we still must store *something* in the *global*
environment. Even though we discard the result of kind-checking, we
sometimes need to produce error messages. These error messages will
want to refer to the tycons being checked, except that they don't
exist yet, and it would be Terribly Annoying to get the error messages
to refer back to HsSyn. So we create a TcTyCon and put it in the
global env. This tycon can print out its name and knows its kind, but
any other action taken on it will panic. Note that TcTyCons are *not*
knot-tied, unlike the rather valid but knot-tied ones that occur
during type-checking.
1233

1234 1235 1236 1237 1238 1239
Note [Declarations for wired-in things]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For wired-in things we simply ignore the declaration
and take the wired-in information.  That avoids complications.
e.g. the need to make the data constructor worker name for
     a constraint tuple match the wired-in one
1240
-}
dreixel's avatar
dreixel committed
1241

1242
tcTyClDecl :: RolesInfo -> LTyClDecl GhcRn -> TcM TyCon
1243
tcTyClDecl roles_info (dL->L loc decl)
1244
  | Just thing <- wiredInNameTyThing_maybe (tcdName decl)
1245 1246 1247
  = case thing of -- See Note [Declarations for wired-in things]
      ATyCon tc -> return tc
      _ -> pprPanic "tcTyClDecl" (ppr thing)
1248 1249

  | otherwise
1250
  = setSrcSpan loc $ tcAddDeclCtxt decl $
1251 1252 1253 1254
    do { traceTc "---- tcTyClDecl ---- {" (ppr decl)
       ; tc <- tcTyClDecl1 Nothing roles_info decl
       ; traceTc "---- tcTyClDecl end ---- }" (ppr tc)
       ; return tc }
1255

1256
  -- "type family" declarations
1257
tcTyClDecl1 :: Maybe Class -> RolesInfo -> TyClDecl GhcRn -> TcM TyCon
Edward Z. Yang's avatar
Edward Z. Yang committed
1258
tcTyClDecl1 parent _roles_info (FamDecl { tcdFam = fd })
1259
  = tcFamDecl1 parent fd
1260

1261
  -- "type" synonym declaration
Edward Z. Yang's avatar
Edward Z. Yang committed
1262
tcTyClDecl1 _parent roles_info
1263 1264
            (SynDecl { tcdLName = (dL->L _ tc_name)
                     , tcdRhs   = rhs })
1265
  = ASSERT( isNothing _parent )
1266
    bindTyClTyVars tc_name $ \ binders res_kind ->
Edward Z. Yang's avatar
Edward Z. Yang committed
1267
    tcTySynRhs roles_info tc_name binders res_kind rhs
1268

1269
  -- "data/newtype" declaration
Edward Z. Yang's avatar
Edward Z. Yang committed
1270
tcTyClDecl1 _parent roles_info
1271
            (DataDecl { tcdLName = (dL->L _ tc_name)
1272
                      , tcdDataDefn = defn })
1273
  = ASSERT( isNothing _parent )
1274
    bindTyClTyVars tc_name $ \ tycon_binders res_kind ->
Edward Z. Yang's avatar
Edward Z. Yang committed
1275
    tcDataDefn roles_info tc_name tycon_binders res_kind defn
1276

Edward Z. Yang's avatar
Edward Z. Yang committed
1277
tcTyClDecl1 _parent roles_info
1278 1279 1280 1281 1282 1283 1284
            (ClassDecl { tcdLName = (dL->L _ class_name)
                       , tcdCtxt = hs_ctxt
                       , tcdMeths = meths
                       , tcdFDs = fundeps
                       , tcdSigs = sigs
                       , tcdATs = ats
                       , tcdATDefs = at_defs })
1285
  = ASSERT( isNothing _parent )
1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305
    do { clas <- tcClassDecl1 roles_info class_name hs_ctxt
                              meths fundeps sigs ats at_defs
       ; return (classTyCon clas) }

tcTyClDecl1 _ _ (XTyClDecl _) = panic "tcTyClDecl1"


{- *********************************************************************
*                                                                      *
          Class declarations
*                                                                      *
********************************************************************* -}

tcClassDecl1 :: RolesInfo -> Name -> LHsContext GhcRn
             -> LHsBinds GhcRn -> [LHsFunDep GhcRn] -> [LSig GhcRn]
             -> [LFamilyDecl GhcRn] -> [LTyFamDefltEqn GhcRn]
             -> TcM Class
tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
  = fixM $ \ clas ->
    -- We need the knot because 'clas' is passed into tcClassATs
1306
    bindTyClTyVars class_name $ \ binders res_kind ->
1307 1308 1309 1310 1311 1312 1313
    do { MASSERT2( tcIsConstraintKind res_kind
                 , ppr class_name $$ ppr res_kind )
       ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr binders)
       ; let tycon_name = class_name        -- We use the same name
             roles = roles_info tycon_name  -- for TyCon and Class

       ; (ctxt, fds, sig_stuff, at_stuff)
1314 1315
            <- pushTcLevelM_   $
               solveEqualities $
1316 1317 1318 1319 1320 1321 1322 1323 1324 1325 1326
               do { ctxt <- tcHsContext hs_ctxt
                  ; fds  <- mapM (addLocM tc_fundep) fundeps
                  ; sig_stuff <- tcClassSigs class_name sigs meths
                  ; at_stuff  <- tcClassATs class_name clas ats at_defs
                  ; return (ctxt, fds, sig_stuff, at_stuff) }

       -- The solveEqualities will report errors for any
       -- unsolved equalities, so these zonks should not encounter
       -- any unfilled coercion variables unless there is such an error
       -- The zonk also squeeze out the TcTyCons, and converts
       -- Skolems to tyvars.
1327 1328 1329
       ; ze        <- emptyZonkEnv
       ; ctxt      <- zonkTcTypesToTypesX ze ctxt
       ; sig_stuff <- mapM (zonkTcMethInfoToMethInfoX ze) sig_stuff
1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346
         -- ToDo: do we need to zonk at_stuff?

       -- TODO: Allow us to distinguish between abstract class,
       -- and concrete class with no methods (maybe by
       -- specifying a trailing where or not

       ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
       ; is_boot <- tcIsHsBootOrSig
       ; let body | is_boot, null ctxt, null at_stuff, null sig_stuff
                  = Nothing
                  | otherwise
                  = Just (ctxt, at_stuff, sig_stuff, mindef)

       ; clas <- buildClass class_name binders roles fds body
       ; traceTc "tcClassDecl" (ppr fundeps $$ ppr binders $$
                                ppr fds)
       ; return clas }
1347
  where
1348 1349
    tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM (tcLookupTyVar . unLoc) tvs1 ;
                                ; tvs2' <- mapM (tcLookupTyVar . unLoc) tvs2 ;
1350
                                ; return (tvs1', tvs2') }
Jan Stolarek's avatar
Jan Stolarek committed
1351

1352 1353 1354 1355 1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379

{- Note [Associated type defaults]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

               type F a b :: *
               type F a b = [a]        -- Default

Note that we can get default definitions only for type families, not data
families.
-}

tcClassATs :: Name                   -- The class name (not knot-tied)
           -> Class                  -- The class parent of this associated type
           -> [LFamilyDecl GhcRn]    -- Associated types.
           -> [LTyFamDefltEqn GhcRn] -- Associated type defaults.
           -> TcM [ClassATItem]
tcClassATs class_name cls ats at_defs
  = do {  -- Complain about associated type defaults for non associated-types
         sequence_ [ failWithTc (badATErr class_name n)
                   | n <- map at_def_tycon at_defs
                   , not (n `elemNameSet` at_names) ]
       ; mapM tc_at ats }
  where
    at_def_tycon :: LTyFamDefltEqn GhcRn -> Name
1380
    at_def_tycon (dL->L _ eqn) = unLoc (feqn_tycon eqn)
1381 1382

    at_fam_name :: LFamilyDecl GhcRn -> Name
1383
    at_fam_name (dL->L _ decl) = unLoc (fdLName decl)
1384 1385 1386 1387 1388 1389 1390 1391 1392 1393 1394 1395 1396 1397 1398 1399 1400 1401 1402 1403 1404 1405 1406 1407 1408 1409

    at_names = mkNameSet (map at_fam_name ats)

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

    tc_at at = do { fam_tc <- addLocM (tcFamDecl1 (Just cls)) at
                  ; let at_defs = lookupNameEnv at_defs_map (at_fam_name at)
                                  `orElse` []
                  ; atd <- tcDefaultAssocDecl fam_tc at_defs
                  ; return (ATI fam_tc atd) }

-------------------------
tcDefaultAssocDecl :: TyCon                    -- ^ Family TyCon (not knot-tied)
                   -> [LTyFamDefltEqn GhcRn]        -- ^ Defaults
                   -> TcM (Maybe (KnotTied Type, SrcSpan))   -- ^ Type checked RHS
tcDefaultAssocDecl _ []
  = return Nothing  -- No default declaration

tcDefaultAssocDecl _ (d1:_:_)
  = failWithTc (text "More than one default declaration for"
                <+> ppr (feqn_tycon (unLoc d1)))

1410
tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name
1411
                                             , feqn_pats = hs_tvs
1412
                                             , feqn_rhs = hs_rhs_ty })]
1413 1414 1415 1416 1417 1418 1419 1420 1421 1422 1423 1424 1425 1426 1427 1428 1429 1430
  | HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = imp_vars}
           , hsq_explicit = exp_vars } <- hs_tvs
  = -- See Note [Type-checking default assoc decls]
    setSrcSpan loc $
    tcAddFamInstCtxt (text "default type instance") tc_name $
    do { traceTc "tcDefaultAssocDecl" (ppr tc_name)
       ; let fam_tc_name = tyConName fam_tc
             fam_arity = length (tyConVisibleTyVars fam_tc)

       -- Kind of family check
       ; ASSERT( fam_tc_name == tc_name )
         checkTc (isTypeFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)

       -- Arity check
       ; checkTc (exp_vars `lengthIs` fam_arity)
                 (wrongNumberOfParmsErr fam_arity)

       -- Typecheck RHS
1431
       ; let hs_pats = map hsLTyVarBndrToType exp_vars
1432

1433
          -- NB: Use tcFamTyPats, not bindTyClTyVars. The latter expects to get
1434 1435 1436
          -- the LHsQTyVars used for declaring a tycon, but the names here
          -- are different.

1437
          -- You might think we should pass in some AssocInstInfo, as we're looking
1438 1439 1440
          -- at an associated type. But this would be wrong, because an associated
          -- type default LHS can mention *different* type variables than the
          -- enclosing class. So it's treated more as a freestanding beast.
1441 1442 1443
       ; (qtvs, pats, rhs_ty) <- tcTyFamInstEqnGuts fam_tc NotAssociated
                                                    imp_vars exp_vars
                                                    hs_pats hs_rhs_ty