TcTyClsDecls.hs 188 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
        kcConDecls, 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
import GHC.Hs
30 31
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 TcUnify ( unifyKind )
41
import TcHsType
42
import ClsInst( AssocInstInfo(..) )
43
import TcMType
44
import TysWiredIn ( unitTy, makeRecoveryTyCon )
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 TcOrigin
51
import Type
52
import TyCoRep   -- for checkValidRoles
53
import TyCoPpr( pprTyVars, pprWithExplicitKindsWhen )
54
import Class
55
import CoAxiom
56 57
import TyCon
import DataCon
58
import Id
59
import Var
60
import VarEnv
61
import VarSet
62
import Module
63
import Name
64
import NameSet
65
import NameEnv
66
import Outputable
67 68 69 70 71 72
import Maybes
import Unify
import Util
import SrcLoc
import ListSetOps
import DynFlags
73
import Unique
74
import ConLike( ConLike(..) )
75
import BasicTypes
76
import qualified GHC.LanguageExtensions as LangExt
77

78
import Control.Monad
79
import Data.Foldable
80
import Data.Function ( on )
81
import Data.List
82
import qualified Data.List.NonEmpty as NE
83
import Data.List.NonEmpty ( NonEmpty(..) )
84 85
import qualified Data.Set as Set

86

87 88 89
{-
************************************************************************
*                                                                      *
90
\subsection{Type checking for type and class declarations}
91 92
*                                                                      *
************************************************************************
93

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

112 113 114 115 116 117 118 119 120
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.
121
-}
122

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

153 154
tcTyClGroup :: TyClGroup GhcRn
            -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo])
155
-- Typecheck one strongly-connected component of type, class, and instance decls
156
-- See Note [TyClGroups and dependency analysis] in GHC.Hs.Decls
157 158
tcTyClGroup (TyClGroup { group_tyclds = tyclds
                       , group_roles  = roles
159
                       , group_kisigs = kisigs
160 161 162
                       , group_instds = instds })
  = do { let role_annots = mkRoleAnnotEnv roles

163
           -- Step 1: Typecheck the standalone kind signatures and type/class declarations
164
       ; traceTc "---- tcTyClGroup ---- {" empty
165
       ; traceTc "Decls for" (ppr (map (tcdName . unLoc) tyclds))
166 167 168 169
       ; (tyclss, data_deriv_info) <-
           tcExtendKindEnv (mkPromotionErrorEnv tyclds) $ -- See Note [Type environment evolution]
           do { kisig_env <- mkNameEnv <$> traverse tcStandaloneKindSig kisigs
              ; tcTyClDecls tyclds kisig_env role_annots }
170

171 172 173 174 175 176
           -- 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)

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

187 188
       ; traceTc "---- end tcTyClGroup ---- }" empty

189 190 191
           -- Step 3: Add the implicit things;
           -- we want them in the environment because
           -- they may be mentioned in interface files
192 193 194
       ; gbl_env <- addTyConsToGblEnv tyclss

           -- Step 4: check instance declarations
195 196 197 198 199 200 201
       ; (gbl_env', inst_info, datafam_deriv_info) <-
         setGblEnv gbl_env $
         tcInstDecls1 instds

       ; let deriv_info = datafam_deriv_info ++ data_deriv_info
       ; return (gbl_env', inst_info, deriv_info) }

202

203
tcTyClGroup (XTyClGroup nec) = noExtCon nec
204

205 206 207
-- Gives the kind for every TyCon that has a standalone kind signature
type KindSigEnv = NameEnv Kind

208 209
tcTyClDecls
  :: [LTyClDecl GhcRn]
210
  -> KindSigEnv
211 212
  -> RoleAnnotEnv
  -> TcM ([TyCon], [DerivInfo])
213 214
tcTyClDecls tyclds kisig_env role_annots
  = do {    -- Step 1: kind-check this group and returns the final
dreixel's avatar
dreixel committed
215 216
            -- (possibly-polymorphic) kind of each TyCon and Class
            -- See Note [Kind checking for type and class decls]
217
         tc_tycons <- kcTyClGroup kisig_env tyclds
218
       ; traceTc "tcTyAndCl generalized kinds" (vcat (map ppr_tc_tycon tc_tycons))
dreixel's avatar
dreixel committed
219

220 221
            -- Step 2: type-check all groups together, returning
            -- the final TyCons and Classes
222 223 224 225
            --
            -- 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.
226
       ; fixM $ \ ~(rec_tyclss, _) -> do
227 228
           { tcg_env <- getGblEnv
           ; let roles = inferRoles (tcg_src tcg_env) role_annots rec_tyclss
dreixel's avatar
dreixel committed
229 230 231

                 -- Populate environment with knot-tied ATyCon for TyCons
                 -- NB: if the decls mention any ill-staged data cons
232
                 -- (see Note [Recursion and promoting data constructors])
233
                 -- we will have failed already in kcTyClGroup, so no worries here
234 235
           ; (tycons, data_deriv_infos) <-
             tcExtendRecEnv (zipRecTyClss tc_tycons rec_tyclss) $
dreixel's avatar
dreixel committed
236 237

                 -- Also extend the local type envt with bindings giving
238
                 -- a TcTyCon for each each knot-tied TyCon or Class
239
                 -- See Note [Type checking recursive type and class declarations]
240 241
                 -- and Note [Type environment evolution]
             tcExtendKindEnvWithTyCons tc_tycons $
dreixel's avatar
dreixel committed
242 243

                 -- Kind and type check declarations for this group
244 245
               mapAndUnzipM (tcTyClDecl roles) tyclds
           ; return (tycons, concat data_deriv_infos)
246
           } }
247 248 249
  where
    ppr_tc_tycon tc = parens (sep [ ppr (tyConName tc) <> comma
                                  , ppr (tyConBinders tc) <> comma
250 251
                                  , ppr (tyConResKind tc)
                                  , ppr (isTcTyCon tc) ])
dreixel's avatar
dreixel committed
252

253
zipRecTyClss :: [TcTyCon]
254
             -> [TyCon]           -- Knot-tied
255
             -> [(Name,TyThing)]
256 257
-- Build a name-TyThing mapping for the TyCons bound by decls
-- being careful not to look at the knot-tied [TyThing]
258
-- The TyThings in the result list must have a visible ATyCon,
259 260
-- because typechecking types (in, say, tcTyClDecl) looks at
-- this outer constructor
261 262
zipRecTyClss tc_tycons rec_tycons
  = [ (name, ATyCon (get name)) | tc_tycon <- tc_tycons, let name = getName tc_tycon ]
263
  where
264 265
    rec_tc_env :: NameEnv TyCon
    rec_tc_env = foldr add_tc emptyNameEnv rec_tycons
266

267 268 269 270 271 272 273 274 275
    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)
276

277 278 279
{-
************************************************************************
*                                                                      *
280
                Kind checking
281 282
*                                                                      *
************************************************************************
283

284 285 286 287
Note [Kind checking for type and class decls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Kind checking is done thus:

288 289
   1. Make up a kind variable for each parameter of the declarations,
      and extend the kind environment (which is in the TcLclEnv)
290

291
   2. Kind check the declarations
292

293 294
We need to kind check all types in the mutually recursive group
before we know the kind of the type variables.  For example:
295

296 297
  class C a where
     op :: D b => a -> b -> b
298

299 300
  class D c where
     bop :: (Monad c) => ...
301 302 303 304 305

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.

306 307 308 309 310 311
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
312

313
The downside of not directly reading off the kinds of the RHS of
314 315 316 317
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.
318

319 320
Note [CUSKs and PolyKinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~
321 322 323 324 325
Consider

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

326
Via inferInitialKinds we get
327 328 329 330 331 332 333 334 335 336 337 338
  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.

339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355
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.

356 357
Open type families
~~~~~~~~~~~~~~~~~~
358 359 360
This treatment of type synonyms only applies to Haskell 98-style synonyms.
General type functions can be recursive, and hence, appear in `alg_decls'.

361
The kind of an open type family is solely determinded by its kind signature;
362
hence, only kind signatures participate in the construction of the initial
363
kind environment (as constructed by `inferInitialKind'). In fact, we ignore
364 365 366
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').
367 368 369

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

370
Note [How TcTyCons work]
371
~~~~~~~~~~~~~~~~~~~~~~~~
372 373 374 375 376 377 378 379 380 381
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.

382
      S1) First, we use inferInitialKinds to look over the user-provided
383 384 385 386
          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
387 388 389 390
          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.

391 392 393 394
      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
395
      S3) We then generalize to get the (non-CUSK) tycon's final, fixed
396 397 398 399 400 401 402 403
          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.

404 405 406 407
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:
408
      - one in inferInitialKind (this pass look only at the head, not the body)
409 410
      - one in kcTyClDecls (to kind-check the body)
      - a final one in tcTyClDecls (to desugar)
411

412 413 414 415 416
    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
417 418 419 420
    TcHsType.splitTelescopeTvs!)

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

423 424 425 426 427 428 429 430
    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.
431

432
See also Note [Type checking recursive type and class declarations].
433

434 435 436 437 438
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)
439

440 441 442 443 444 445 446
We do the following steps:

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

447
  2. kcTyCLGroup
448
      - Do inferInitialKinds, which will signal a promotion
449
        error if B is used in any of the kinds needed to initialise
450 451
        B's kind (e.g. (a :: Type)) here

452
      - Extend the type env with these initial kinds (monomorphic for
453 454 455 456
        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
457
        all those initial kinds
458

459
      - Generalise the initial kind, making a poly-kinded TcTyCon
460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490

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

492 493 494
Note [Don't process associated types in getInitialKind]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Previously, we processed associated types in the thing_inside in getInitialKind,
495 496 497 498 499 500 501 502 503 504 505 506
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,
507
because the solveEqualities in kcInferDeclHeader is at TcLevel 1 and so kappa[1]
508 509 510 511 512 513
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.

514
-}
515

516
kcTyClGroup :: KindSigEnv -> [LTyClDecl GhcRn] -> TcM [TcTyCon]
517

dreixel's avatar
dreixel committed
518
-- Kind check this group, kind generalize, and return the resulting local env
519
-- This binds the TyCons and Classes of the group, but not the DataCons
dreixel's avatar
dreixel committed
520
-- See Note [Kind checking for type and class decls]
521
-- and Note [Inferring kinds for type declarations]
522
kcTyClGroup kisig_env decls
523
  = do  { mod <- getModule
524
        ; traceTc "---- kcTyClGroup ---- {"
525
                  (text "module" <+> ppr mod $$ vcat (map ppr decls))
dreixel's avatar
dreixel committed
526

527
          -- Kind checking;
528 529 530
          --    1. Bind kind variables for decls
          --    2. Kind-check decls
          --    3. Generalise the inferred kinds
dreixel's avatar
dreixel committed
531 532
          -- See Note [Kind checking for type and class decls]

533 534
        ; cusks_enabled <- xoptM LangExt.CUSKs <&&> xoptM LangExt.PolyKinds
                    -- See Note [CUSKs and PolyKinds]
535 536 537 538 539 540 541 542
        ; let (kindless_decls, kinded_decls) = partitionWith get_kind decls

              get_kind d
                | Just ki <- lookupNameEnv kisig_env (tcdName (unLoc d))
                = Right (d, SAKS ki)

                | cusks_enabled && hsDeclHasCusk (unLoc d)
                = Right (d, CUSK)
543

544
                | otherwise = Left d
545

546 547 548
        ; checked_tcs <- checkInitialKinds kinded_decls
        ; inferred_tcs
            <- tcExtendKindEnvWithTyCons checked_tcs $
549 550 551 552 553
               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
554
                    mono_tcs <- inferInitialKinds kindless_decls
555

556 557
                  ; traceTc "kcTyClGroup: initial kinds" $
                    ppr_tc_kinds mono_tcs
Tobias Dammers's avatar
Tobias Dammers committed
558

559 560 561 562 563
                    -- 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 $
564
                    mapM_ kcLTyClDecl kindless_decls
565 566 567 568

                  ; return mono_tcs }

        -- Step 3: generalisation
Tobias Dammers's avatar
Tobias Dammers committed
569 570 571
        -- Finally, go through each tycon and give it its final kind,
        -- with all the required, specified, and inferred variables
        -- in order.
572
        ; generalized_tcs <- mapAndReportM generaliseTcTyCon inferred_tcs
573

574
        ; let poly_tcs = checked_tcs ++ generalized_tcs
575 576
        ; traceTc "---- kcTyClGroup end ---- }" (ppr_tc_kinds poly_tcs)
        ; return poly_tcs }
577

578
  where
579 580 581
    ppr_tc_kinds tcs = vcat (map pp_tc tcs)
    pp_tc tc = ppr (tyConName tc) <+> dcolon <+> ppr (tyConKind tc)

582 583 584 585 586
generaliseTcTyCon :: TcTyCon -> TcM TcTyCon
generaliseTcTyCon tc
  -- See Note [Required, Specified, and Inferred for types]
  = setSrcSpan (getSrcSpan tc) $
    addTyConCtxt tc $
587 588 589 590 591 592 593 594 595
    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))]
596
             -- where "k1" dnotes the Name k1, and kk1, aa, etc are MetaTyVars,
597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620
             -- 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
621
       ; inferred <- quantifyTyVars dvs2
622 623 624 625 626 627 628 629 630 631 632 633 634 635

       -- 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
636 637
       -- (remember they all started as TyVarTvs).
       -- They have been skolemised by quantifyTyVars.
638 639
       ; (ze, inferred) <- zonkTyBndrsX ze inferred
       ; tc_res_kind    <- zonkTcTypeToTypeX ze tc_res_kind
640

641
       ; traceTc "generaliseTcTyCon: post zonk" $
642
         vcat [ text "tycon =" <+> ppr tc
643 644 645 646 647
              , 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 ]
648 649

       -- Step 4: Find the Specified and Inferred variables
650 651 652 653 654 655
       -- 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
656 657 658
                             -- NB: maintain the L-R order of scoped_tvs

       -- Step 5: Make the TyConBinders.
659 660
             to_user tv     = lookupTyVarOcc ze tv `orElse` tv
             dep_fv_set     = mapVarSet to_user (candidateKindVars dvs1)
661 662
             inferred_tcbs  = mkNamedTyConBinders Inferred inferred
             specified_tcbs = mkNamedTyConBinders Specified specified
663
             required_tcbs  = map (mkRequiredTyConBinder dep_fv_set) req_tvs
664 665 666 667 668 669 670

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

       -- Step 7: Make the result TcTyCon
671
             tycon = mkTcTyCon tc_name final_tcbs tc_res_kind
672
                            (mkTyVarNamePairs final_spec_req_tvs)
673 674 675
                            True {- it's generalised now -}
                            (tyConFlavour tc)

676
       ; traceTc "generaliseTcTyCon done" $
677 678
         vcat [ text "tycon =" <+> ppr tc
              , text "tc_res_kind =" <+> ppr tc_res_kind
679 680
              , text "dep_fv_set =" <+> ppr dep_fv_set
              , text "final_spec_req_tvs =" <+> pprTyVars final_spec_req_tvs
681 682 683 684 685
              , text "inferred =" <+> pprTyVars inferred
              , text "specified =" <+> pprTyVars specified
              , text "required_tcbs =" <+> ppr required_tcbs
              , text "final_tcbs =" <+> ppr final_tcbs ]

686 687 688 689
       -- 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
690

691
       ; return tycon }
692 693 694 695 696

checkDuplicateTyConBinders :: [Name] -> [TcTyVar] -> TcM ()
checkDuplicateTyConBinders spec_req_names spec_req_tvs
  | null dups = return ()
  | otherwise = mapM_ report_dup dups >> failM
697
  where
698 699 700 701
    dups :: [(Name,Name)]
    dups = findDupTyVarTvs $ spec_req_names `zip` spec_req_tvs

    report_dup (n1, n2)
702 703 704
      = setSrcSpan (getSrcSpan n2) $
        addErrTc (text "Couldn't match" <+> quotes (ppr n1)
                        <+> text "with" <+> quotes (ppr n2))
705

706 707 708
{- Note [Required, Specified, and Inferred for types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Each forall'd type variable in a type or kind is one of
709

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

712 713
  * Specified: the argument can be inferred at call sites, but
    may be instantiated with visible type/kind application
714

715 716
  * Inferred: the must be inferred at call sites; it
    is unavailable for use with visible type/kind application.
717

718 719 720 721
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.
722

723
Go read Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep.
724

725 726 727 728 729 730 731 732 733 734 735 736 737 738 739
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
740 741 742

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

743 744 745 746
Example:
  data SameKind :: k -> k -> *
  data Bad a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)

747
For Bad:
748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765
  - 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.
766
Here is an example (#15592)
767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788
  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

789 790
  * Declarations with a standalone kind signature or a complete user-specified
    kind signature (CUSK). Handled by the kcCheckDeclHeader.
791

792 793
  * Declarations without a kind signature (standalone or CUSK) are handled by
    kcInferDeclHeader; see Note [Inferring kinds for type declarations].
794 795

Note that neither code path worries about point (4) above, as this
Tobias Dammers's avatar
Tobias Dammers committed
796
is nicely handled by not mangling the res_kind. (Mangling res_kinds is done
797 798 799 800 801 802 803 804 805
*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
806
  methods. But it got too compilicated; see #15592, comment:21ff.
Tobias Dammers's avatar
Tobias Dammers committed
807 808 809

* We rigidly require the ordering above, even though we could be much more
  permissive. Relevant musings are at
810
  https://gitlab.haskell.org/ghc/ghc/issues/15743#note_161623
Tobias Dammers's avatar
Tobias Dammers committed
811 812 813 814 815 816 817 818 819 820 821 822
  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.

823 824
Test cases (and tickets) relevant to these design decisions
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Tobias Dammers's avatar
Tobias Dammers committed
825 826 827
  T15591*
  T15592*
  T15743*
828

829 830 831 832 833 834 835 836 837
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:

838
* Step 1: inferInitialKinds, and in particular kcInferDeclHeader.
839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860
  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
861 862
          T :: kk1 -> * -> kk2 -> *
          S :: kk3 -> * -> kk4 -> *
863

864 865 866 867
* 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.
868 869 870 871 872 873

  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.

874
* Step 3: generaliseTcTyCon. Generalise each TyCon in turn.
875 876 877 878 879
  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.

880
  This makes the utterly-final TyConBinders for the TyCon.
881 882 883 884

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

885 886
  But there some tricky corners: Note [Tricky scoping in generaliseTcTyCon]

887 888 889 890 891
* 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.

892 893
The first three steps are in kcTyClGroup; the fourth is in
tcTyClDecls.
894 895 896 897 898 899 900

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
901
  TcMType.defaultTyVar.  Here's another example (#14555):
902 903 904
     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.
905
  #14563 is another example.
906

907
* Duplicate type variables. Consider #11203
908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931
    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
932 933 934

Note [Tricky scoping in generaliseTcTyCon]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
935
Consider #16342
936 937 938 939 940 941 942 943 944 945 946 947 948 949 950
  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.

951
Conclusion: the classTyVars of a class must have the same Name as
952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975
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
976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008
apply this same substitution to the kind of each.

Note [Inferring visible dependent quantification]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider

  data T k :: k -> Type where
    MkT1 :: T Type Int
    MkT2 :: T (Type -> Type) Maybe

This looks like it should work. However, it is polymorphically recursive,
as the uses of T in the constructor types specialize the k in the kind
of T. This trips up our dear users (#17131, #17541), and so we add
a "landmark" context (which cannot be suppressed) whenever we
spot inferred visible dependent quantification (VDQ).

It's hard to know when we've actually been tripped up by polymorphic recursion
specifically, so we just include a note to users whenever we infer VDQ. The
testsuite did not show up a single spurious inclusion of this message.

The context is added in addVDQNote, which looks for a visible TyConBinder
that also appears in the TyCon's kind. (I first looked at the kind for
a visible, dependent quantifier, but Note [No polymorphic recursion] in
TcHsType defeats that approach.) addVDQNote is used in kcTyClDecl,
which is used only when inferring the kind of a tycon (never with a CUSK or
SAK).

Once upon a time, I (Richard E) thought that the tycon-kind could
not be a forall-type. But this is wrong: data T :: forall k. k -> Type
(with -XNoCUSKs) could end up here. And this is all OK.


-}
1009

1010
--------------
1011 1012 1013
tcExtendKindEnvWithTyCons :: [TcTyCon] -> TcM a -> TcM a
tcExtendKindEnvWithTyCons tcs
  = tcExtendKindEnvList [ (tyConName tc, ATcTyCon tc) | tc <- tcs ]
1014 1015

--------------
1016
mkPromotionErrorEnv :: [LTyClDecl GhcRn] -> TcTypeEnv
1017 1018 1019
-- Maps each tycon/datacon to a suitable promotion error
--    tc :-> APromotionErr TyConPE
--    dc :-> APromotionErr RecDataConPE
1020
--    See Note [Recursion and promoting data constructors]
1021 1022 1023 1024 1025

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

1026
mk_prom_err_env :: TyClDecl GhcRn -> TcTypeEnv
1027 1028 1029 1030
mk_prom_err_env (ClassDecl { tcdLName = L _ nm, tcdATs = ats })
  = unitNameEnv nm (APromotionErr ClassPE)
    `plusNameEnv`
    mkNameEnv [ (name, APromotionErr TyConPE)
1031
              | (L _ (FamilyDecl { fdLName = L _ name })) <- ats ]
1032

1033
mk_prom_err_env (DataDecl { tcdLName = L _ name
1034 1035 1036 1037
                          , tcdDataDefn = HsDataDefn { dd_cons = cons } })
  = unitNameEnv name (APromotionErr TyConPE)
    `plusNameEnv`
    mkNameEnv [ (con, APromotionErr RecDataConPE)
1038 1039
              | L _ con' <- cons
              , L _ con  <- getConNames con' ]
1040 1041 1042 1043 1044 1045

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

--------------
1046
inferInitialKinds :: [LTyClDecl GhcRn] -> TcM [TcTyCon]
1047 1048
-- Returns a TcTyCon for each TyCon bound by the decls,
-- each with its initial kind
1049

1050 1051 1052 1053
inferInitialKinds decls
  = do { traceTc "inferInitialKinds {" $ ppr (map (tcdName . unLoc) decls)
       ; tcs <- concatMapM infer_initial_kind decls
       ; traceTc "inferInitialKinds done }" empty
1054
       ; return tcs }
1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072
  where
    infer_initial_kind = addLocM (getInitialKind InitialKindInfer)

-- Check type/class declarations against their standalone kind signatures or
-- CUSKs, producing a generalized TcTyCon for each.
checkInitialKinds :: [(LTyClDecl GhcRn, SAKS_or_CUSK)] -> TcM [TcTyCon]
checkInitialKinds decls
  = do { traceTc "checkInitialKinds {" $ ppr (mapFst (tcdName . unLoc) decls)
       ; tcs <- concatMapM check_initial_kind decls
       ; traceTc "checkInitialKinds done }" empty
       ; return tcs }
  where
    check_initial_kind (ldecl, msig) =
      addLocM (getInitialKind (InitialKindCheck msig)) ldecl

-- | Get the initial kind of a TyClDecl, either generalized or non-generalized,
-- depending on the 'InitialKindStrategy'.
getInitialKind :: InitialKindStrategy -> TyClDecl GhcRn -> TcM [TcTyCon]
1073

dreixel's avatar
dreixel committed
1074
-- Allocate a fresh kind variable for each TyCon and Class
1075
-- For each tycon, return a TcTyCon with kind k
1076
-- where k is the kind of tc, derived from the LHS
1077 1078
--         of the definition (and probably including
--         kind unification variables)
dreixel's avatar
dreixel committed
1079
--      Example: data T a b = ...
1080
--      return (T, kv1 -> kv2 -> kv3)
dreixel's avatar
dreixel committed
1081
--
1082 1083 1084 1085
-- 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
--
1086 1087
-- No family instances are passed to checkInitialKinds/inferInitialKinds
getInitialKind strategy
1088
    (ClassDecl { tcdLName = L _ name
1089 1090
               , tcdTyVars = ktvs
               , tcdATs = ats })
1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105
  = do { cls <- kcDeclHeader strategy name ClassFlavour ktvs $
                return (TheKind constraintKind)
       ; let parent_tv_prs = tcTyConScopedTyVars cls
            -- See Note [Don't process associated types in getInitialKind]
       ; inner_tcs <-
           tcExtendNameTyVarEnv parent_tv_prs $
           mapM (addLocM (getAssocFamInitialKind cls)) ats
       ; return (cls : inner_tcs) }
  where
    getAssocFamInitialKind cls =
      case strategy of
        InitialKindInfer -> get_fam_decl_initial_kind (Just cls)
        InitialKindCheck _ -> check_initial_kind_assoc_fam cls

getInitialKind strategy
1106
    (DataDecl { tcdLName = L _ name
1107 1108 1109 1110
              , tcdTyVars = ktvs
              , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
                                         , dd_ND = new_or_data } })
  = do  { let flav = newOrDataToFlavour new_or_data
1111 1112 1113 1114 1115
              ctxt = DataKindCtxt name
        ; tc <- kcDeclHeader strategy name flav ktvs $
                case m_sig of
                  Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig
                  Nothing -> dataDeclDefaultResultKind new_or_data
1116 1117
        ; return [tc] }

1118 1119
getInitialKind InitialKindInfer (FamDecl { tcdFam = decl })
  = do { tc <- get_fam_decl_initial_kind Nothing decl
1120
       ; return [tc] }
1121

1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138
getInitialKind (InitialKindCheck msig) (FamDecl { tcdFam =
  FamilyDecl { fdLName     = unLoc -> name
             , fdTyVars    = ktvs
             , fdResultSig = unLoc -> resultSig
             , fdInfo      = info } } )
  = do { let flav = getFamFlav Nothing info
             ctxt = TyFamResKindCtxt name
       ; tc <- kcDeclHeader (InitialKindCheck msig) name flav ktvs $
               case famResultKindSignature resultSig of
                 Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig
                 Nothing ->
                   case msig of
                     CUSK -> return (TheKind liftedTypeKind)
                     SAKS _ -> return AnyKind
       ; return [tc] }

getInitialKind strategy
1139
    (SynDecl { tcdLName = L _ name
1140 1141 1142 1143 1144 1145 1146 1147
             , tcdTyVars = ktvs
             , tcdRhs = rhs })
  = do { let ctxt = TySynKindCtxt name
       ; tc <- kcDeclHeader strategy name TypeSynonymFlavour ktvs $
               case hsTyKindSig rhs of
                 Just rhs_sig -> TheKind <$> tcLHsKindSig ctxt rhs_sig
                 Nothing -> return AnyKind
       ; return [tc] }
1148

1149
getInitialKind _ (DataDecl _ _ _ _ (XHsDataDefn nec)) = noExtCon nec
1150
getInitialKind _ (FamDecl {tcdFam = XFamilyDecl nec}) = noExtCon nec
1151
getInitialKind _ (XTyClDecl nec) = noExtCon nec
1152

1153 1154
get_fam_decl_initial_kind
  :: Maybe TcTyCon -- ^ Just cls <=> this is an associated family of class cls
1155 1156
  -> FamilyDecl GhcRn
  -> TcM TcTyCon
1157
get_fam_decl_initial_kind mb_parent_tycon
1158
    FamilyDecl { fdLName     = L _ name
1159
               , fdTyVars    = ktvs
1160
               , fdResultSig = L _ resultSig
1161 1162 1163
               , fdInfo      = info }
  = kcDeclHeader InitialKindInfer name flav ktvs $
    case resultSig of
1164 1165
      KindSig _ ki                          -> TheKind <$> tcLHsKindSig ctxt ki
      TyVarSig _ (L _ (KindedTyVar _ _ ki)) -> TheKind <$> tcLHsKindSig ctxt ki
1166 1167 1168 1169 1170
      _ -- open type families have * return kind by default
        | tcFlavourIsOpen flav              -> return (TheKind liftedTypeKind)
               -- closed type families have their return kind inferred
               -- by default
        | otherwise                         -> return AnyKind
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1171
  where
1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287
    flav = getFamFlav mb_parent_tycon info
    ctxt = TyFamResKindCtxt name
get_fam_decl_initial_kind _ (XFamilyDecl nec) = noExtCon nec

-- See Note [Standalone kind signatures for associated types]
check_initial_kind_assoc_fam
  :: TcTyCon -- parent class
  -> FamilyDecl GhcRn
  -> TcM TcTyCon
check_initial_kind_assoc_fam cls
  FamilyDecl
    { fdLName     = unLoc -> name
    , fdTyVars    = ktvs
    , fdResultSig = unLoc -> resultSig
    , fdInfo      = info }
  = kcDeclHeader (InitialKindCheck CUSK) name flav ktvs $
    case famResultKindSignature resultSig of
      Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig
      Nothing -> return (TheKind liftedTypeKind)
  where
    ctxt = TyFamResKindCtxt name
    flav = getFamFlav (Just cls) info
check_initial_kind_assoc_fam _ (XFamilyDecl nec) = noExtCon nec

{- Note [Standalone kind signatures for associated types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

If associated types had standalone kind signatures, would they wear them

---------------------------+------------------------------
  like this? (OUT)         |   or like this? (IN)
---------------------------+------------------------------
  type T :: Type -> Type   |   class C a where
  class C a where          |     type T :: Type -> Type
    type T a               |     type T a

The (IN) variant is syntactically ambiguous:

  class C a where
    type T :: a   -- standalone kind signature?
    type T :: a   -- declaration header?

The (OUT) variant does not suffer from this issue, but it might not be the
direction in which we want to take Haskell: we seek to unify type families and
functions, and, by extension, associated types with class methods. And yet we
give class methods their signatures inside the class, not outside. Neither do
we have the counterpart of InstanceSigs for StandaloneKindSignatures.

For now, we dodge the question by using CUSKs for associated types instead of
standalone kind signatures. This is a simple addition to the rule we used to
have before standalone kind signatures:

  old rule:  associated type has a CUSK iff its parent class has a CUSK
  new rule:  associated type has a CUSK iff its parent class has a CUSK or a standalone kind signature

-}

-- See Note [Data declaration default result kind]
dataDeclDefaultResultKind :: NewOrData -> TcM ContextKind
dataDeclDefaultResultKind new_or_data = do
  -- See Note [Implementation of UnliftedNewtypes]
  unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
  return $ case new_or_data of
    NewType | unlifted_newtypes -> OpenKind
    _ -> TheKind liftedTypeKind

{- Note [Data declaration default result kind]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

When the user has not written an inline result kind annotation on a data
declaration, we assume it to be 'Type'. That is, the following declarations
D1 and D2 are considered equivalent:

  data D1         where ...
  data D2 :: Type where ...

The consequence of this assumption is that we reject D3 even though we
accept D4:

  data D3 where
    MkD3 :: ... -> D3 param

  data D4 :: Type -> Type where
    MkD4 :: ... -> D4 param

However, there's a twist: when -XUnliftedNewtypes are enabled, we must relax
the assumed result kind to (TYPE r) for newtypes:

  newtype D5 where
    MkD5 :: Int# -> D5

dataDeclDefaultResultKind takes care to produce the appropriate result kind.
-}

---------------------------------
getFamFlav
  :: Maybe TcTyCon    -- ^ Just cls <=> this is an associated family of class cls
  -> FamilyInfo pass
  -> TyConFlavour
getFamFlav mb_parent_tycon info =
  case info of
    DataFamily         -> DataFamilyFlavour mb_parent_tycon
    OpenTypeFamily     -> OpenTypeFamilyFlavour mb_parent_tycon
    ClosedTypeFamily _ -> ASSERT( isNothing mb_parent_tycon ) -- See Note [Closed type family mb_parent_tycon]
                          ClosedTypeFamilyFlavour

{- Note [Closed type family mb_parent_tycon]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
There's no way to write a closed type family inside a class declaration:

  class C a where
    type family F a where  -- error: parse error on input ‘where’

In fact, it is not clear what the meaning of such a declaration would be.
Therefore, 'mb_parent_tycon' of any closed type family has to be Nothing.
-}
1288

1289
------------------------------------------------------------------------
1290
kcLTyClDecl :: LTyClDecl GhcRn -> TcM ()
1291
  -- See Note [Kind checking for type and class decls]
1292
  -- Called only for declarations without a signature (no CUSKs or SAKs here)
1293
kcLTyClDecl (L loc decl)
1294
  = setSrcSpan loc $
1295 1296 1297 1298 1299
    do { tycon <- kcLookupTcTyCon tc_name
       ; traceTc "kcTyClDecl {" (ppr tc_name)
       ; addVDQNote tycon $   -- See Note [Inferring visible dependent quantification]
         addErrCtxt (tcMkDeclCtxt decl) $
         kcTyClDecl decl tycon
1300 1301
       ; traceTc "kcTyClDecl done }" (ppr tc_name) }
  where
1302
    tc_name = tcdName decl
1303

1304
kcTyClDecl :: TyClDecl GhcRn -> TcTyCon -> TcM ()
dreixel's avatar
dreixel committed
1305
-- This function is used solely for its side effect on kind variables
1306
-- NB kind signatures on the type variables and
Gabor Greif's avatar
Gabor Greif committed
1307
--    result kind signature have already been dealt with
1308
--    by inferInitialKind, so we can ignore them here.
dreixel's avatar
dreixel committed
1309

1310
kcTyClDecl (DataDecl { tcdLName    = (L _ name)
1311
                     , tcdDataDefn = defn }) tyCon
1312 1313
  | HsDataDefn { dd_cons = cons@((L _ (ConDeclGADT {})) : _)
               , dd_ctxt = (L _ [])
1314
               , dd_ND = new_or_data } <- defn
1315 1316 1317
  = -- See Note [Implementation of UnliftedNewtypes] STEP 2
    kcConDecls new_or_data (tyConResKind tyCon) cons

1318
    -- hs_tvs and dd_kindSig already dealt with in inferInitialKind
1319
    -- This must be a GADT-style decl,
1320 1321 1322 1323
    --        (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
1324

1325 1326 1327
  | HsDataDefn { dd_ctxt = ctxt
               , dd_cons = cons
               , dd_ND = new_or_data } <- defn
1328
  = bindTyClTyVars name $ \ _ _ ->
1329
    do { _ <- tcHsContext ctxt
1330
       ; kcConDecls new_or_data (tyConResKind tyCon) cons
1331
       }
1332

1333
kcTyClDecl (SynDecl { tcdLName = L _ name, tcdRhs = rhs }) _tycon
1334 1335
  = bindTyClTyVars name $ \ _ res_kind ->
    discardResult $ tcCheckLHsType rhs res_kind
1336
        -- NB: check against the result kind that we allocated
1337
        -- in inferInitialKinds.
1338

1339
kcTyClDecl (ClassDecl { tcdLName = L _ name
1340
                      , tcdCtxt = ctxt, tcdSigs = sigs }) _tycon
1341
  = bindTyClTyVars name $ \ _ _ ->
1342
    do  { _ <- tcHsContext ctxt
1343
        ; mapM_ (wrapLocM_ kc_sig) sigs }
dreixel's avatar
dreixel committed
1344
  where
1345
    kc_sig (ClassOpSig _ _ nms op_ty) = kcClassSigType skol_info nms op_ty
1346
    kc_sig _                          = return ()
1347

1348 1349
    skol_info = TyConSkol ClassFlavour name

1350
kcTyClDecl (FamDecl _ (FamilyDecl { fdInfo   = fd_info })) fam_tc
1351 1352 1353
-- closed type families look at their equations, but other families don't
-- do anything here
  = case fd_info of
1354
      ClosedTypeFamily (Just eqns) -> mapM_ (kcTyFamInstEqn fam_tc) eqns
1355
      _ -> return ()
1356 1357 1358
kcTyClDecl (FamDecl _ (XFamilyDecl nec))        _ = noExtCon nec
kcTyClDecl (DataDecl _ _ _ _ (XHsDataDefn nec)) _ = noExtCon nec
kcTyClDecl (XTyClDecl nec)                      _ = noExtCon nec
dreixel's avatar
dreixel committed
1359 1360

-------------------
1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 1381 1382 1383 1384 1385 1386 1387 1388 1389 1390 1391 1392 1393 1394 1395

-- | Unify the kind of the first type provided with the newtype's kind, if
-- -XUnliftedNewtypes is enabled and the NewOrData indicates Newtype. If there
-- is more than one type provided, do nothing: the newtype is in error, and this
-- will be caught in validity checking (which will give a better error than we can
-- here.)
unifyNewtypeKind :: DynFlags
                 -> NewOrData
                 -> [LHsType GhcRn]   -- user-written argument types, should be just 1
                 -> [TcType]          -- type-checked argument types, should be just 1
                 -> TcKind            -- expected kind of newtype
                 -> TcM [TcType]      -- casted argument types (should be just 1)
                                      --  result = orig_arg |> kind_co
                                      -- where kind_co :: orig_arg_ki ~N expected_ki
unifyNewtypeKind dflags NewType [hs_ty] [tc_ty] ki
  | xopt LangExt.UnliftedNewtypes dflags
  = do { traceTc "unifyNewtypeKind" (ppr hs_ty $$ ppr tc_ty $$ ppr ki)
       ; co <- unifyKind (Just (unLoc hs_ty)) (typeKind tc_ty) ki
       ; return [tc_ty `mkCastTy` co] }
  -- See comments above: just do nothing here
unifyNewtypeKind _ _ _ arg_tys _ = return arg_tys

-- Type check the types of the arguments to a data constructor.
-- This includes doing kind unification if the type is a newtype.
-- See Note [Implementation of UnliftedNewtypes] for why we need
-- the first two arguments.
kcConArgTys :: NewOrData -> Kind -> [LHsType GhcRn] -> TcM ()
kcConArgTys new_or_data res_kind arg_tys = do
  { arg_tc_tys <- mapM (tcHsOpenType . getBangType) arg_tys
    -- See Note [Implementation of UnliftedNewtypes], STEP 2
  ; dflags <- getDynFlags
  ; discardResult $
      unifyNewtypeKind dflags new_or_data arg_tys arg_tc_tys res_kind
  }

1396 1397 1398 1399 1400 1401 1402 1403 1404 1405
kcConDecls :: NewOrData
           -> Kind             -- The result kind signature
           -> [LConDecl GhcRn] -- The data constructors
           -> TcM ()
kcConDecls new_or_data res_kind cons
  = mapM_ (wrapLocM_ (kcConDecl new_or_data final_res_kind)) cons
  where
    (_, final_res_kind) = splitPiTys res_kind
        -- See Note [kcConDecls result kind]

1406 1407 1408 1409 1410
-- Kind check a data constructor. In additional to the data constructor,
-- we also need to know about whether or not its corresponding type was
-- declared with data or newtype, and we need to know the result kind of
-- this type. See Note [Implementation of UnliftedNewtypes] for why
-- we need the first two arguments.
1411 1412 1413 1414 1415 1416
kcConDecl :: NewOrData
          -> Kind  -- Result kind of the type constructor
                   -- Usually Type but can be TYPE UnliftedRep
                   -- or even TYPE r, in the case of unlifted newtype
          -> ConDecl GhcRn
          -> TcM ()
1417 1418 1419
kcConDecl new_or_data res_kind (ConDeclH98
  { con_name = name, con_ex_tvs = ex_tvs
  , con_mb_cxt = ex_ctxt, con_args = args })
Alan Zimmerman's avatar
Alan Zimmerman committed
1420
  = addErrCtxt (dataConCtxtName [name]) $
1421
    discardResult                   $
1422
    bindExplicitTKBndrs_Tv ex_tvs $
1423
    do { _ <- tcHsMbContext ex_ctxt
1424
       ; kcConArgTys new_or_data res_kind (hsConDeclArgTys args)
1425 1426
         -- We don't need to check the telescope here,
         -- because that's done in tcConDecl
1427
       }
1428

1429 1430 1431
kcConDecl new_or_data res_kind (ConDeclGADT
    { con_names = names, con_qvars = qtvs, con_mb_cxt = cxt
    , con_args = args, con_res_ty = res_ty })
1432
  | HsQTvs { hsq_ext = implicit_tkv_nms
Simon Peyton Jones's avatar