TcTyClsDecls.hs 137 KB
Newer Older
Austin Seipp's avatar
Austin Seipp committed
1 2 3 4
{-
(c) The University of Glasgow 2006
(c) The AQUA Project, Glasgow University, 1996-1998

5 6

TcTyClsDecls: Typecheck type and class declarations
Austin Seipp's avatar
Austin Seipp committed
7
-}
8

9
{-# LANGUAGE CPP, TupleSections, MultiWayIf #-}
10
{-# LANGUAGE TypeFamilies #-}
Ian Lynagh's avatar
Ian Lynagh committed
11

12
module TcTyClsDecls (
13
        tcTyAndClassDecls, tcAddImplicits,
14

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

23
#include "HsVersions.h"
24

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

Ian Lynagh's avatar
Ian Lynagh committed
73
import Control.Monad
74
import Data.List
75

Austin Seipp's avatar
Austin Seipp committed
76 77 78
{-
************************************************************************
*                                                                      *
79
\subsection{Type checking for type and class declarations}
Austin Seipp's avatar
Austin Seipp committed
80 81
*                                                                      *
************************************************************************
82

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

101 102 103 104 105 106 107 108 109
Note [Check role annotations in a second pass]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Role inference potentially depends on the types of all of the datacons declared
in a mutually recursive group. The validity of a role annotation, in turn,
depends on the result of role inference. Because the types of datacons might
be ill-formed (see #7175 and Note [Checking GADT return types]) we must check
*all* the tycons in a group for validity before checking *any* of the roles.
Thus, we take two passes over the resulting tycons, first checking for general
validity and then checking for valid role annotations.
Austin Seipp's avatar
Austin Seipp committed
110
-}
111

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

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

           -- Step 1: Typecheck the type/class declarations
152 153
       ; traceTc "-------- tcTyClGroup ------------" empty
       ; traceTc "Decls for" (ppr (map (tcdName . unLoc) tyclds))
154 155
       ; tyclss <- tcTyClDecls tyclds role_annots

156 157 158 159 160 161
           -- 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)

162 163 164 165
       ; traceTc "Starting family consistency check" (ppr tyclss)
       ; forM_ tyclss checkRecFamInstConsistency
       ; traceTc "Done family consistency" (ppr tyclss)

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

           -- Step 3: Add the implicit things;
           -- we want them in the environment because
           -- they may be mentioned in interface files
       ; tcExtendTyConEnv tyclss $
    do { gbl_env <- tcAddImplicits tyclss
       ; setGblEnv gbl_env $
    do {
            -- Step 4: check instance declarations
       ; (gbl_env, inst_info, datafam_deriv_info) <- tcInstDecls1 instds

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

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

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

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

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

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

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

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

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

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

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

263
   2. Kind check the declarations
264

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

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

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

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.

278 279 280 281 282 283
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
284

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

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

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


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

Austin Seipp's avatar
Austin Seipp committed
306
-}
307

308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327

-- 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.
--
328
kcTyClGroup :: [LTyClDecl GhcRn] -> TcM [TcTyCon]
329

dreixel's avatar
dreixel committed
330
-- Kind check this group, kind generalize, and return the resulting local env
331
-- This binds the TyCons and Classes of the group, but not the DataCons
dreixel's avatar
dreixel committed
332
-- See Note [Kind checking for type and class decls]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
333 334
-- Third return value is Nothing if the tycon be unsaturated; otherwise,
-- the arity
335
kcTyClGroup decls
336
  = do  { mod <- getModule
337
        ; traceTc "kcTyClGroup" (text "module" <+> ppr mod $$ vcat (map ppr decls))
dreixel's avatar
dreixel committed
338

339
          -- Kind checking;
340 341 342
          --    1. Bind kind variables for decls
          --    2. Kind-check decls
          --    3. Generalise the inferred kinds
dreixel's avatar
dreixel committed
343 344
          -- See Note [Kind checking for type and class decls]

345
        ; lcl_env <- solveEqualities $
346 347 348 349 350 351 352 353 354 355 356 357 358
                     do { -- Step 1: Bind kind variables for all decls
                          initial_kinds <- getInitialKinds decls
                        ; traceTc "kcTyClGroup: initial kinds" $
                          ppr initial_kinds

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

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

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
361
        ; traceTc "kcTyClGroup result" (vcat (map pp_res res))
362
        ; return res }
363

364
  where
365
    generalise :: TcTypeEnv -> Name -> TcM TcTyCon
366
    -- For polymorphic things this is a no-op
367
    generalise kind_env name
368 369 370 371 372
      = do { let tc = case lookupNameEnv kind_env name of
                        Just (ATcTyCon tc) -> tc
                        _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env)
                 kc_binders  = tyConBinders tc
                 kc_res_kind = tyConResKind tc
373
                 kc_tyvars   = tyConTyVars tc
374
                 kc_flav     = tyConFlavour tc
375
           ; kvs <- kindGeneralize (mkTyConKind kc_binders kc_res_kind)
376
           ; let all_binders = mkNamedTyConBinders Inferred kvs ++ kc_binders
377

Simon Peyton Jones's avatar
Simon Peyton Jones committed
378
           ; (env, all_binders') <- zonkTyVarBindersX emptyZonkEnv all_binders
379
           ; kc_res_kind'        <- zonkTcTypeToType env kc_res_kind
380 381

                      -- Make sure kc_kind' has the final, zonked kind variables
382
           ; traceTc "Generalise kind" $
383 384
             vcat [ ppr name, ppr kc_binders, ppr kvs, ppr all_binders, ppr kc_res_kind
                  , ppr all_binders', ppr kc_res_kind'
385
                  , ppr kc_tyvars, ppr (tcTyConScopedTyVars tc)]
386

387
           ; return (mkTcTyCon name all_binders' kc_res_kind'
388 389
                               (tcTyConScopedTyVars tc)
                               kc_flav) }
dreixel's avatar
dreixel committed
390

391
    generaliseTCD :: TcTypeEnv
392
                  -> LTyClDecl GhcRn -> TcM [TcTyCon]
393
    generaliseTCD kind_env (L _ decl)
394 395
      | ClassDecl { tcdLName = (L _ name), tcdATs = ats } <- decl
      = do { first <- generalise kind_env name
396 397 398 399 400 401 402 403
           ; rest <- mapM ((generaliseFamDecl kind_env) . unLoc) ats
           ; return (first : rest) }

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

      | otherwise
404
      = do { res <- generalise kind_env (tcdName decl)
405 406
           ; return [res] }

407
    generaliseFamDecl :: TcTypeEnv
408
                      -> FamilyDecl GhcRn -> TcM TcTyCon
409 410
    generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name })
      = generalise kind_env name
411

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

414 415 416 417 418
--------------
mkTcTyConEnv :: TcTyCon -> TcTypeEnv
mkTcTyConEnv tc = unitNameEnv (getName tc) (ATcTyCon tc)

extendEnvWithTcTyCon :: TcTypeEnv -> TcTyCon -> TcTypeEnv
419
-- Makes a binding to put in the local envt, binding
420
-- a name to a TcTyCon
421 422 423 424
extendEnvWithTcTyCon env tc
  = extendNameEnv env (getName tc) (ATcTyCon tc)

--------------
425
mkPromotionErrorEnv :: [LTyClDecl GhcRn] -> TcTypeEnv
426 427 428
-- Maps each tycon/datacon to a suitable promotion error
--    tc :-> APromotionErr TyConPE
--    dc :-> APromotionErr RecDataConPE
429
--    See Note [Recursion and promoting data constructors]
430 431 432 433 434

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

435
mk_prom_err_env :: TyClDecl GhcRn -> TcTypeEnv
436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453
mk_prom_err_env (ClassDecl { tcdLName = L _ nm, tcdATs = ats })
  = unitNameEnv nm (APromotionErr ClassPE)
    `plusNameEnv`
    mkNameEnv [ (name, APromotionErr TyConPE)
              | L _ (FamilyDecl { fdLName = L _ name }) <- ats ]

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

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

--------------
454
getInitialKinds :: [LTyClDecl GhcRn] -> TcM (NameEnv TcTyThing)
455 456 457 458
-- Maps each tycon to its initial kind,
-- and each datacon to a suitable promotion error
--    tc :-> ATcTyCon (tc:initial_kind)
--    dc :-> APromotionErr RecDataConPE
459
--    See Note [Recursion and promoting data constructors]
460

461
getInitialKinds decls
462 463 464 465 466
  = tcExtendKindEnv promotion_err_env $
    do { tc_kinds <- mapM (addLocM getInitialKind) decls
       ; return (foldl plusNameEnv promotion_err_env tc_kinds) }
  where
    promotion_err_env = mkPromotionErrorEnv decls
467

468
getInitialKind :: TyClDecl GhcRn
469
               -> TcM (NameEnv TcTyThing)
dreixel's avatar
dreixel committed
470
-- Allocate a fresh kind variable for each TyCon and Class
471 472 473 474 475
-- For each tycon, return a NameEnv with
--      name :-> ATcTyCon (TcCyCon with kind k))
-- where k is the kind of tc, derived from the LHS
--       of the definition (and probably including
--       kind unification variables)
dreixel's avatar
dreixel committed
476
--      Example: data T a b = ...
477
--      return (T, kv1 -> kv2 -> kv3)
dreixel's avatar
dreixel committed
478
--
479 480 481 482
-- 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
--
483
-- No family instances are passed to getInitialKinds
dreixel's avatar
dreixel committed
484

485
getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
486 487
  = do { let cusk = hsDeclHasCusk decl
       ; (tycon, inner_prs) <-
488
           kcHsTyVarBndrs name ClassFlavour cusk True ktvs $
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
489
           do { inner_prs <- getFamDeclInitialKinds (Just cusk) ats
490
              ; return (constraintKind, inner_prs) }
491
       ; return (extendEnvWithTcTyCon inner_prs tycon) }
492

493
getInitialKind decl@(DataDecl { tcdLName = L _ name
494
                              , tcdTyVars = ktvs
495 496
                              , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
                                                         , dd_ND = new_or_data } })
497
  = do  { (tycon, _) <-
498
           kcHsTyVarBndrs name flav (hsDeclHasCusk decl) True ktvs $
499
           do { res_k <- case m_sig of
500
                           Just ksig -> tcLHsKindSig ksig
501
                           Nothing   -> return liftedTypeKind
502
              ; return (res_k, ()) }
503
        ; return (mkTcTyConEnv tycon) }
504 505 506 507
  where
    flav = case new_or_data of
             NewType  -> NewtypeFlavour
             DataType -> DataTypeFlavour
508

Jan Stolarek's avatar
Jan Stolarek committed
509
getInitialKind (FamDecl { tcdFam = decl })
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
510
  = getFamDeclInitialKind Nothing decl
511

512 513 514
getInitialKind decl@(SynDecl { tcdLName = L _ name
                             , tcdTyVars = ktvs
                             , tcdRhs = rhs })
515 516 517
  = do  { (tycon, _) <- kcHsTyVarBndrs name TypeSynonymFlavour
                            (hsDeclHasCusk decl)
                            True ktvs $
518 519
            do  { res_k <- case kind_annotation rhs of
                            Nothing -> newMetaKindVar
520
                            Just ksig -> tcLHsKindSig ksig
521
                ; return (res_k, ()) }
522
        ; return (mkTcTyConEnv tycon) }
523 524 525 526 527 528
  where
    -- Keep this synchronized with 'hsDeclHasCusk'.
    kind_annotation (L _ ty) = case ty of
        HsParTy lty     -> kind_annotation lty
        HsKindSig _ k   -> Just k
        _               -> Nothing
529 530

---------------------------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
531
getFamDeclInitialKinds :: Maybe Bool  -- if assoc., CUSKness of assoc. class
532
                       -> [LFamilyDecl GhcRn]
533
                       -> TcM TcTypeEnv
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
534
getFamDeclInitialKinds mb_cusk decls
535 536
  = do { tc_kinds <- mapM (addLocM (getFamDeclInitialKind mb_cusk)) decls
       ; return (foldr plusNameEnv emptyNameEnv tc_kinds) }
537

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
538
getFamDeclInitialKind :: Maybe Bool  -- if assoc., CUSKness of assoc. class
539
                      -> FamilyDecl GhcRn
540
                      -> TcM TcTypeEnv
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
541 542 543 544
getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName     = L _ name
                                               , fdTyVars    = ktvs
                                               , fdResultSig = L _ resultSig
                                               , fdInfo      = info })
545
  = do { (tycon, _) <-
546
           kcHsTyVarBndrs name flav cusk True ktvs $
Jan Stolarek's avatar
Jan Stolarek committed
547
           do { res_k <- case resultSig of
548 549
                      KindSig ki                        -> tcLHsKindSig ki
                      TyVarSig (L _ (KindedTyVar _ ki)) -> tcLHsKindSig ki
Jan Stolarek's avatar
Jan Stolarek committed
550
                      _ -- open type families have * return kind by default
551
                        | tcFlavourIsOpen flav     -> return liftedTypeKind
Jan Stolarek's avatar
Jan Stolarek committed
552 553 554
                        -- closed type families have their return kind inferred
                        -- by default
                        | otherwise                -> newMetaKindVar
555
              ; return (res_k, ()) }
556
       ; return (mkTcTyConEnv tycon) }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
557
  where
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
558
    cusk  = famDeclHasCusk mb_cusk decl
559 560 561 562
    flav  = case info of
      DataFamily         -> DataFamilyFlavour
      OpenTypeFamily     -> OpenTypeFamilyFlavour
      ClosedTypeFamily _ -> ClosedTypeFamilyFlavour
563

564
------------------------------------------------------------------------
565
kcLTyClDecl :: LTyClDecl GhcRn -> TcM ()
566
  -- See Note [Kind checking for type and class decls]
567
kcLTyClDecl (L loc decl)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
568 569 570 571 572
  = setSrcSpan loc $
    tcAddDeclCtxt decl $
    do { traceTc "kcTyClDecl {" (ppr (tyClDeclLName decl))
       ; kcTyClDecl decl
       ; traceTc "kcTyClDecl done }" (ppr (tyClDeclLName decl)) }
573

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

580
kcTyClDecl (DataDecl { tcdLName = L _ name, tcdDataDefn = defn })
581
  | HsDataDefn { dd_cons = cons, dd_kindSig = Just _ } <- defn
582
  = mapM_ (wrapLocM kcConDecl) cons
583 584 585 586 587 588
    -- hs_tvs and dd_kindSig already dealt with in getInitialKind
    -- If dd_kindSig is Just, this must be a GADT-style decl,
    --        (see invariants of DataDefn declaration)
    -- so (a) we don't need to bring the hs_tvs into scope, because the
    --        ConDecls bind all their own variables
    --    (b) dd_ctxt is not allowed for GADT-style decls, so we can ignore it
589

590
  | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
591
  = kcTyClTyVars name $
592
    do  { _ <- tcHsContext ctxt
593
        ; mapM_ (wrapLocM kcConDecl) cons }
594

595 596 597 598 599 600
kcTyClDecl (SynDecl { tcdLName = L _ name, tcdRhs = lrhs })
  = kcTyClTyVars name $
    do  { syn_tc <- kcLookupTcTyCon name
        -- NB: check against the result kind that we allocated
        -- in getInitialKinds.
        ; discardResult $ tcCheckLHsType lrhs (tyConResKind syn_tc) }
601

602 603 604
kcTyClDecl (ClassDecl { tcdLName = L _ name
                      , tcdCtxt = ctxt, tcdSigs = sigs })
  = kcTyClTyVars name $
605
    do  { _ <- tcHsContext ctxt
606
        ; mapM_ (wrapLocM kc_sig)     sigs }
dreixel's avatar
dreixel committed
607
  where
Alan Zimmerman's avatar
Alan Zimmerman committed
608
    kc_sig (ClassOpSig _ nms op_ty) = kcHsSigType nms op_ty
609
    kc_sig _                        = return ()
610

611
kcTyClDecl (FamDecl (FamilyDecl { fdLName  = L _ fam_tc_name
612 613 614 615 616
                                , fdInfo   = fd_info }))
-- closed type families look at their equations, but other families don't
-- do anything here
  = case fd_info of
      ClosedTypeFamily (Just eqns) ->
617 618
        do { fam_tc <- kcLookupTcTyCon fam_tc_name
           ; mapM_ (kcTyFamInstEqn (famTyConShape fam_tc)) eqns }
619
      _ -> return ()
dreixel's avatar
dreixel committed
620 621

-------------------
622
kcConDecl :: ConDecl GhcRn -> TcM ()
Alan Zimmerman's avatar
Alan Zimmerman committed
623 624 625
kcConDecl (ConDeclH98 { con_name = name, con_qvars = ex_tvs
                      , con_cxt = ex_ctxt, con_details = details })
  = addErrCtxt (dataConCtxtName [name]) $
626 627
         -- the 'False' says that the existentials don't have a CUSK, as the
         -- concept doesn't really apply here. We just need to bring the variables
628 629 630 631
         -- into scope. (Similarly, the choice of PromotedDataConFlavour isn't
         -- particularly important.)
    do { _ <- kcHsTyVarBndrs (unLoc name) PromotedDataConFlavour
                             False False
632
                             ((fromMaybe emptyLHsQTvs ex_tvs)) $
Alan Zimmerman's avatar
Alan Zimmerman committed
633
              do { _ <- tcHsContext (fromMaybe (noLoc []) ex_ctxt)
634 635
                 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details)
                 ; return (panic "kcConDecl", ()) }
636 637
              -- We don't need to check the telescope here, because that's
              -- done in tcConDecl
638
       ; return () }
639

Alan Zimmerman's avatar
Alan Zimmerman committed
640 641 642 643
kcConDecl (ConDeclGADT { con_names = names
                       , con_type = ty })
  = addErrCtxt (dataConCtxtName names) $
      do { _ <- tcGadtSigType (ppr names) (unLoc $ head names) ty
644 645 646 647 648 649 650
                -- Even though the data constructor's type is closed, we
                -- must still call tcGadtSigType, because that influences
                -- 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
Alan Zimmerman's avatar
Alan Zimmerman committed
651 652
         ; return () }

Austin Seipp's avatar
Austin Seipp committed
653
{-
654 655
Note [Recursion and promoting data constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
656 657 658 659 660 661 662 663
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:
664 665
  T -> ATcTyCon <some initial kind>
  K -> APromotionErr
666

667
APromotionErr is only used for DataCons, and only used during type checking
668 669
in tcTyClGroup.

670

Austin Seipp's avatar
Austin Seipp committed
671 672
************************************************************************
*                                                                      *
673
\subsection{Type checking}
Austin Seipp's avatar
Austin Seipp committed
674 675
*                                                                      *
************************************************************************
676

dreixel's avatar
dreixel committed
677 678 679 680
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,
681
we discarded the kind-checked types (eg RHSs of data type decls);
dreixel's avatar
dreixel committed
682 683 684 685 686 687 688
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
689
    to be given kind arguments.
dreixel's avatar
dreixel committed
690 691 692 693 694 695 696

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

dreixel's avatar
dreixel committed
698 699 700 701 702 703 704
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

705 706
  *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
707 708 709 710 711 712 713 714 715 716

Then:

  * During TcHsType.kcTyVar we look in the *local* env, to get the
    known kind for T.

  * But in TcHsType.ds_type (and ds_var_app in particular) we look in
    the *global* env to get the TyCon. But we must be careful not to
    force the TyCon or we'll get a loop.

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

721 722 723 724 725 726 727 728 729 730 731
See also Note [Kind checking recursive type and class declarations]

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

The initial kind is stored in exactly the same way during kind-checking
as it is during type-checking (Note [Type checking recursive type and class
732
declarations]): in the *local* environment, with ATcTyCon. But we still
733 734 735 736 737 738 739 740 741 742 743
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.

744 745 746 747 748 749
Note [Declarations for wired-in things]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For wired-in things we simply ignore the declaration
and take the wired-in information.  That avoids complications.
e.g. the need to make the data constructor worker name for
     a constraint tuple match the wired-in one
Austin Seipp's avatar
Austin Seipp committed
750
-}
dreixel's avatar
dreixel committed
751

752
tcTyClDecl :: RolesInfo -> LTyClDecl GhcRn -> TcM TyCon
Edward Z. Yang's avatar
Edward Z. Yang committed
753
tcTyClDecl roles_info (L loc decl)
754
  | Just thing <- wiredInNameTyThing_maybe (tcdName decl)
755 756 757
  = case thing of -- See Note [Declarations for wired-in things]
      ATyCon tc -> return tc
      _ -> pprPanic "tcTyClDecl" (ppr thing)
758 759

  | otherwise
760
  = setSrcSpan loc $ tcAddDeclCtxt decl $
761
    do { traceTc "tcTyAndCl-x" (ppr decl)
Edward Z. Yang's avatar
Edward Z. Yang committed
762
       ; tcTyClDecl1 Nothing roles_info decl }
763

764
  -- "type family" declarations
765
tcTyClDecl1 :: Maybe Class -> RolesInfo -> TyClDecl GhcRn -> TcM TyCon
Edward Z. Yang's avatar
Edward Z. Yang committed
766
tcTyClDecl1 parent _roles_info (FamDecl { tcdFam = fd })
767
  = tcFamDecl1 parent fd
768

769
  -- "type" synonym declaration
Edward Z. Yang's avatar
Edward Z. Yang committed
770
tcTyClDecl1 _parent roles_info
771
            (SynDecl { tcdLName = L _ tc_name, tcdRhs = rhs })
772
  = ASSERT( isNothing _parent )
773
    tcTyClTyVars tc_name $ \ binders res_kind ->
Edward Z. Yang's avatar
Edward Z. Yang committed
774
    tcTySynRhs roles_info tc_name binders res_kind rhs
775

776
  -- "data/newtype" declaration
Edward Z. Yang's avatar
Edward Z. Yang committed
777
tcTyClDecl1 _parent roles_info
778
            (DataDecl { tcdLName = L _ tc_name, tcdDataDefn = defn })
779
  = ASSERT( isNothing _parent )
780
    tcTyClTyVars tc_name $ \ tycon_binders res_kind ->
Edward Z. Yang's avatar
Edward Z. Yang committed
781
    tcDataDefn roles_info tc_name tycon_binders res_kind defn
782

Edward Z. Yang's avatar
Edward Z. Yang committed
783
tcTyClDecl1 _parent roles_info
784
            (ClassDecl { tcdLName = L _ class_name
785
            , tcdCtxt = ctxt, tcdMeths = meths
786
            , tcdFDs = fundeps, tcdSigs = sigs
787
            , tcdATs = ats, tcdATDefs = at_defs })
788
  = ASSERT( isNothing _parent )
789
    do { clas <- fixM $ \ clas ->
Gabor Greif's avatar
Gabor Greif committed
790
            -- We need the knot because 'clas' is passed into tcClassATs
791
            tcTyClTyVars class_name $ \ binders res_kind ->
792
            do { MASSERT( isConstraintKind res_kind )
793
               ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr binders)
794 795
               ; let tycon_name = class_name        -- We use the same name
                     roles = roles_info tycon_name  -- for TyCon and Class
dreixel's avatar
dreixel committed
796

797
               ; ctxt' <- solveEqualities $ tcHsContext ctxt
798
               ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'
799 800
                       -- Squeeze out any kind unification variables
               ; fds'  <- mapM (addLocM tc_fundep) fundeps
801
               ; sig_stuff <- tcClassSigs class_name sigs meths
802
               ; at_stuff <- tcClassATs class_name clas ats at_defs
803
               ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
804 805 806 807 808 809 810 811 812
               -- TODO: Allow us to distinguish between abstract class,
               -- and concrete class with no methods (maybe by
               -- specifying a trailing where or not
               ; is_boot <- tcIsHsBootOrSig
               ; let body | is_boot, null ctxt', null at_stuff, null sig_stuff
                          = Nothing
                          | otherwise
                          = Just (ctxt', at_stuff, sig_stuff, mindef)
               ; clas <- buildClass class_name binders roles fds' body
813
               ; traceTc "tcClassDecl" (ppr fundeps $$ ppr binders $$
814
                                        ppr fds')
815 816 817
               ; return clas }

         ; return (classTyCon clas) }
818
  where
819 820
    tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM (tcLookupTyVar . unLoc) tvs1 ;
                                ; tvs2' <- mapM (tcLookupTyVar . unLoc) tvs2 ;
821
                                ; return (tvs1', tvs2') }
Jan Stolarek's avatar
Jan Stolarek committed
822

823
tcFamDecl1 :: Maybe Class -> FamilyDecl GhcRn -> TcM TyCon
824
tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_name)
825 826
                              , fdTyVars = tvs, fdResultSig = L _ sig
                              , fdInjectivityAnn = inj })
827
  | DataFamily <- fam_info
828
  = tcTyClTyVars tc_name $ \ binders res_kind -> do
829 830
  { traceTc "data family:" (ppr tc_name)
  ; checkFamFlag tc_name
831
  ; (extra_binders, real_res_kind) <- tcDataKindSig False res_kind
832
  ; tc_rep_name <- newTyConRepName tc_name
833 834
  ; let tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders)
                              real_res_kind
835 836 837 838 839 840
                              (resultVariableName sig)
                              (DataFamilyTyCon tc_rep_name)
                              parent NotInjective
  ; return tycon }

  | OpenTypeFamily <- fam_info
841
  = tcTyClTyVars tc_name $ \ binders res_kind -> do
842
  { traceTc "open type family:" (ppr tc_name)
843
  ; checkFamFlag tc_name
844 845
  ; inj' <- tcInjectivity binders inj
  ; let tycon = mkFamilyTyCon tc_name binders res_kind
846 847
                               (resultVariableName sig) OpenSynFamilyTyCon
                               parent inj'
848
  ; return tycon }
849

850 851 852 853
  | ClosedTypeFamily mb_eqns <- fam_info
  = -- Closed type families are a little tricky, because they contain the definition
    -- of both the type family and the equations for a CoAxiom.
    do { traceTc "Closed type family:" (ppr tc_name)
Jan Stolarek's avatar
Jan Stolarek committed
854 855
         -- the variables in the header scope only over the injectivity
         -- declaration but this is not involved here
856
       ; (inj', binders, res_kind)
857
            <- tcTyClTyVars tc_name
858 859 860
               $ \ binders res_kind ->
               do { inj' <- tcInjectivity binders inj
                  ; return (inj', binders, res_kind) }