TcTyClsDecls.hs 129 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 #-}
Ian Lynagh's avatar
Ian Lynagh committed
10

11
module TcTyClsDecls (
12
        tcTyAndClassDecls, tcAddImplicits,
13

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

22
#include "HsVersions.h"
23

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

Ian Lynagh's avatar
Ian Lynagh committed
71
import Control.Monad
72
import Data.List
73

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

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

99 100 101 102 103 104 105 106 107
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
108
-}
109

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

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

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

154 155 156 157 158 159
           -- 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)

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

164 165 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) } } }

tcTyClDecls :: [LTyClDecl Name] -> RoleAnnotEnv -> TcM [TyCon]
tcTyClDecls tyclds role_annots
dreixel's avatar
dreixel committed
188 189 190
  = 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]
191 192
         tc_tycons <- kcTyClGroup tyclds
       ; traceTc "tcTyAndCl generalized kinds" (vcat (map ppr_tc_tycon tc_tycons))
dreixel's avatar
dreixel committed
193

194 195
            -- Step 2: type-check all groups together, returning
            -- the final TyCons and Classes
196 197 198 199
            --
            -- 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.
200
       ; fixM $ \ ~rec_tyclss -> do
Simon Peyton Jones's avatar
Simon Peyton Jones committed
201
           { is_boot   <- tcIsHsBootOrSig
Edward Z. Yang's avatar
Edward Z. Yang committed
202
           ; let roles = inferRoles is_boot role_annots rec_tyclss
dreixel's avatar
dreixel committed
203 204 205

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

                 -- Also extend the local type envt with bindings giving
                 -- the (polymorphic) kind of each knot-tied TyCon or Class
212
                 -- See Note [Type checking recursive type and class declarations]
213
             tcExtendKindEnv2 (map mkTcTyConPair tc_tycons)              $
dreixel's avatar
dreixel committed
214 215

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

223
zipRecTyClss :: [TcTyCon]
224
             -> [TyCon]           -- Knot-tied
225
             -> [(Name,TyThing)]
226 227
-- 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
228
-- The TyThings in the result list must have a visible ATyCon,
229 230
-- because typechecking types (in, say, tcTyClDecl) looks at
-- this outer constructor
231 232
zipRecTyClss tc_tycons rec_tycons
  = [ (name, ATyCon (get name)) | tc_tycon <- tc_tycons, let name = getName tc_tycon ]
233
  where
234 235
    rec_tc_env :: NameEnv TyCon
    rec_tc_env = foldr add_tc emptyNameEnv rec_tycons
236

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

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

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

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

261
   2. Kind check the declarations
262

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

266 267
  class C a where
     op :: D b => a -> b -> b
268

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

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.

276 277 278 279 280 281
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
282

283 284 285 286 287
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.
288

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

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


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

Austin Seipp's avatar
Austin Seipp committed
304
-}
305

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

-- 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.
--
326
kcTyClGroup :: [LTyClDecl Name] -> TcM [TcTyCon]
327

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

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

343
        ; lcl_env <- solveEqualities $
344
          do {
345 346
               -- Step 1: Bind kind variables for all decls
               initial_kinds <- getInitialKinds decls
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
347 348
             ; traceTc "kcTyClGroup: initial kinds" $
               vcat (map pp_initial_kind initial_kinds)
349
             ; tcExtendKindEnv2 initial_kinds $ do {
350

351 352
             -- Step 2: Set extended envt, kind-check the decls
             ; mapM_ kcLTyClDecl decls
353

354
             ; getLclEnv } }
dreixel's avatar
dreixel committed
355

356 357
             -- Step 4: generalisation
             -- Kind checking done for this group
dreixel's avatar
dreixel committed
358
             -- 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
           ; kvs <- kindGeneralize (mkTyConKind kc_binders kc_res_kind)
375
           ; let all_binders = mkNamedTyConBinders Inferred kvs ++ kc_binders
376

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

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

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

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

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

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

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

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
411 412 413 414 415 416 417
    pp_initial_kind (name, ATcTyCon tc)
      = ppr name <+> dcolon <+> ppr (tyConKind tc)
    pp_initial_kind pair
      = ppr pair

    pp_res tc = ppr (tyConName tc) <+> dcolon <+> ppr (tyConKind tc)

418
mkTcTyConPair :: TcTyCon -> (Name, TcTyThing)
419
-- Makes a binding to put in the local envt, binding
420 421 422
-- a name to a TcTyCon
mkTcTyConPair tc
  = (getName tc, ATcTyCon tc)
423

424 425 426 427 428 429 430 431 432 433 434 435
mk_thing_env :: [LTyClDecl Name] -> [(Name, TcTyThing)]
mk_thing_env [] = []
mk_thing_env (decl : decls)
  | L _ (ClassDecl { tcdLName = L _ nm, tcdATs = ats }) <- decl
  = (nm, APromotionErr ClassPE) :
    (map (, APromotionErr TyConPE) $ map (unLoc . fdLName . unLoc) ats) ++
    (mk_thing_env decls)

  | otherwise
  = (tcdName (unLoc decl), APromotionErr TyConPE) :
    (mk_thing_env decls)

436
getInitialKinds :: [LTyClDecl Name] -> TcM [(Name, TcTyThing)]
437
getInitialKinds decls
438
  = tcExtendKindEnv2 (mk_thing_env decls) $
439 440
    do { pairss <- mapM (addLocM getInitialKind) decls
       ; return (concat pairss) }
441

442 443
getInitialKind :: TyClDecl Name
               -> TcM [(Name, TcTyThing)]    -- Mixture of ATcTyCon and APromotionErr
dreixel's avatar
dreixel committed
444
-- Allocate a fresh kind variable for each TyCon and Class
445
-- For each tycon, return   (name, ATcTyCon (TcCyCon with kind k))
dreixel's avatar
dreixel committed
446 447 448 449
--                 where k is the kind of tc, derived from the LHS
--                       of the definition (and probably including
--                       kind unification variables)
--      Example: data T a b = ...
450
--      return (T, kv1 -> kv2 -> kv3)
dreixel's avatar
dreixel committed
451
--
452 453 454 455 456
-- 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
--
-- ALSO for each datacon, return (dc, APromotionErr RecDataConPE)
457
--    See Note [ARecDataCon: Recursion and promoting data constructors]
458
--
459
-- No family instances are passed to getInitialKinds
dreixel's avatar
dreixel committed
460

461
getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
462 463
  = do { (tycon, inner_prs) <-
           kcHsTyVarBndrs name True cusk False True ktvs $
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
464
           do { inner_prs <- getFamDeclInitialKinds (Just cusk) ats
465
              ; return (constraintKind, inner_prs) }
466
       ; return (mkTcTyConPair tycon : inner_prs) }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
467 468
  where
    cusk = hsDeclHasCusk decl
469

470
getInitialKind decl@(DataDecl { tcdLName = L _ name
471 472
                              , tcdTyVars = ktvs
                              , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
473
                                                         , dd_cons = cons } })
474 475
  = do  { (tycon, _) <-
           kcHsTyVarBndrs name True (hsDeclHasCusk decl) False True ktvs $
476 477 478
           do { res_k <- case m_sig of
                           Just ksig -> tcLHsKind ksig
                           Nothing   -> return liftedTypeKind
479
              ; return (res_k, ()) }
480
        ; let inner_prs = [ (unLoc con, APromotionErr RecDataConPE)
481
                          | L _ con' <- cons, con <- getConNames con' ]
482
        ; return (mkTcTyConPair tycon : inner_prs) }
483

Jan Stolarek's avatar
Jan Stolarek committed
484
getInitialKind (FamDecl { tcdFam = decl })
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
485
  = getFamDeclInitialKind Nothing decl
486

487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502
getInitialKind decl@(SynDecl { tcdLName = L _ name
                             , tcdTyVars = ktvs
                             , tcdRhs = rhs })
  = do  { (tycon, _) <- kcHsTyVarBndrs name False (hsDeclHasCusk decl)
                            False {- not open -} True ktvs $
            do  { res_k <- case kind_annotation rhs of
                            Nothing -> newMetaKindVar
                            Just ksig -> tcLHsKind ksig
                ; return (res_k, ()) }
        ; return [ mkTcTyConPair tycon ] }
  where
    -- Keep this synchronized with 'hsDeclHasCusk'.
    kind_annotation (L _ ty) = case ty of
        HsParTy lty     -> kind_annotation lty
        HsKindSig _ k   -> Just k
        _               -> Nothing
503 504

---------------------------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
505 506 507
getFamDeclInitialKinds :: Maybe Bool  -- if assoc., CUSKness of assoc. class
                       -> [LFamilyDecl Name] -> TcM [(Name, TcTyThing)]
getFamDeclInitialKinds mb_cusk decls
508 509
  = tcExtendKindEnv2 [ (n, APromotionErr TyConPE)
                     | L _ (FamilyDecl { fdLName = L _ n }) <- decls] $
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
510
    concatMapM (addLocM (getFamDeclInitialKind mb_cusk)) decls
511

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
512 513
getFamDeclInitialKind :: Maybe Bool  -- if assoc., CUSKness of assoc. class
                      -> FamilyDecl Name
514
                      -> TcM [(Name, TcTyThing)]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
515 516 517 518
getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName     = L _ name
                                               , fdTyVars    = ktvs
                                               , fdResultSig = L _ resultSig
                                               , fdInfo      = info })
519 520
  = do { (tycon, _) <-
           kcHsTyVarBndrs name unsat cusk open True ktvs $
Jan Stolarek's avatar
Jan Stolarek committed
521 522 523 524
           do { res_k <- case resultSig of
                      KindSig ki                        -> tcLHsKind ki
                      TyVarSig (L _ (KindedTyVar _ ki)) -> tcLHsKind ki
                      _ -- open type families have * return kind by default
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
525
                        | open                     -> return liftedTypeKind
Jan Stolarek's avatar
Jan Stolarek committed
526 527 528
                        -- closed type families have their return kind inferred
                        -- by default
                        | otherwise                -> newMetaKindVar
529
              ; return (res_k, ()) }
530
       ; return [ mkTcTyConPair tycon ] }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
531
  where
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
532 533 534 535 536
    cusk  = famDeclHasCusk mb_cusk decl
    (open, unsat) = case info of
      DataFamily         -> (True,  True)
      OpenTypeFamily     -> (True,  False)
      ClosedTypeFamily _ -> (False, False)
537

538
------------------------------------------------------------------------
539
kcLTyClDecl :: LTyClDecl Name -> TcM ()
540
  -- See Note [Kind checking for type and class decls]
541 542 543
kcLTyClDecl (L loc decl)
  = setSrcSpan loc $ tcAddDeclCtxt decl $ kcTyClDecl decl

dreixel's avatar
dreixel committed
544 545
kcTyClDecl :: TyClDecl Name -> TcM ()
-- This function is used solely for its side effect on kind variables
546
-- NB kind signatures on the type variables and
Gabor Greif's avatar
Gabor Greif committed
547
--    result kind signature have already been dealt with
548
--    by getInitialKind, so we can ignore them here.
dreixel's avatar
dreixel committed
549

550
kcTyClDecl (DataDecl { tcdLName = L _ name, tcdDataDefn = defn })
551
  | HsDataDefn { dd_cons = cons, dd_kindSig = Just _ } <- defn
552
  = mapM_ (wrapLocM kcConDecl) cons
553 554 555 556 557 558
    -- 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
559

560
  | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
561
  = kcTyClTyVars name $
562
    do  { _ <- tcHsContext ctxt
563
        ; mapM_ (wrapLocM kcConDecl) cons }
564

565 566 567 568 569 570
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) }
571

572 573 574
kcTyClDecl (ClassDecl { tcdLName = L _ name
                      , tcdCtxt = ctxt, tcdSigs = sigs })
  = kcTyClTyVars name $
575
    do  { _ <- tcHsContext ctxt
576
        ; mapM_ (wrapLocM kc_sig)     sigs }
dreixel's avatar
dreixel committed
577
  where
Alan Zimmerman's avatar
Alan Zimmerman committed
578
    kc_sig (ClassOpSig _ nms op_ty) = kcHsSigType nms op_ty
579
    kc_sig _                        = return ()
580

581
kcTyClDecl (FamDecl (FamilyDecl { fdLName  = L _ fam_tc_name
582 583 584 585 586
                                , 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) ->
587 588
        do { fam_tc <- kcLookupTcTyCon fam_tc_name
           ; mapM_ (kcTyFamInstEqn (famTyConShape fam_tc)) eqns }
589
      _ -> return ()
dreixel's avatar
dreixel committed
590 591

-------------------
592
kcConDecl :: ConDecl Name -> TcM ()
Alan Zimmerman's avatar
Alan Zimmerman committed
593 594 595
kcConDecl (ConDeclH98 { con_name = name, con_qvars = ex_tvs
                      , con_cxt = ex_ctxt, con_details = details })
  = addErrCtxt (dataConCtxtName [name]) $
596 597
         -- 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
598
         -- into scope.
599
    do { _ <- kcHsTyVarBndrs (unLoc name) False False False False
600
                             ((fromMaybe emptyLHsQTvs ex_tvs)) $
Alan Zimmerman's avatar
Alan Zimmerman committed
601
              do { _ <- tcHsContext (fromMaybe (noLoc []) ex_ctxt)
602 603
                 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details)
                 ; return (panic "kcConDecl", ()) }
604 605
              -- We don't need to check the telescope here, because that's
              -- done in tcConDecl
606
       ; return () }
607

Alan Zimmerman's avatar
Alan Zimmerman committed
608 609 610 611 612 613 614
kcConDecl (ConDeclGADT { con_names = names
                       , con_type = ty })
  = addErrCtxt (dataConCtxtName names) $
      do { _ <- tcGadtSigType (ppr names) (unLoc $ head names) ty
         ; return () }


Austin Seipp's avatar
Austin Seipp committed
615
{-
616 617
Note [Recursion and promoting data constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
618 619 620 621 622 623 624 625
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:
626 627
  T -> ATcTyCon <some initial kind>
  K -> APromotionErr
628

629
APromotionErr is only used for DataCons, and only used during type checking
630 631
in tcTyClGroup.

632

Austin Seipp's avatar
Austin Seipp committed
633 634
************************************************************************
*                                                                      *
635
\subsection{Type checking}
Austin Seipp's avatar
Austin Seipp committed
636 637
*                                                                      *
************************************************************************
638

dreixel's avatar
dreixel committed
639 640 641 642
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,
643
we discarded the kind-checked types (eg RHSs of data type decls);
dreixel's avatar
dreixel committed
644 645 646 647 648 649 650
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
651
    to be given kind arguments.
dreixel's avatar
dreixel committed
652 653 654 655 656 657 658

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

dreixel's avatar
dreixel committed
660 661 662 663 664 665 666
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

667 668
  *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
669 670 671 672 673 674 675 676 677 678

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
679
This fancy footwork (with two bindings for T) is only necessary for the
dreixel's avatar
dreixel committed
680 681
TyCons or Classes of this recursive group.  Earlier, finished groups,
live in the global env only.
682

683 684 685 686 687 688 689 690 691 692 693
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
694
declarations]): in the *local* environment, with ATcTyCon. But we still
695 696 697 698 699 700 701 702 703 704 705
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.

706 707 708 709 710 711
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
712
-}
dreixel's avatar
dreixel committed
713

Edward Z. Yang's avatar
Edward Z. Yang committed
714 715
tcTyClDecl :: RolesInfo -> LTyClDecl Name -> TcM TyCon
tcTyClDecl roles_info (L loc decl)
716
  | Just thing <- wiredInNameTyThing_maybe (tcdName decl)
717 718 719
  = case thing of -- See Note [Declarations for wired-in things]
      ATyCon tc -> return tc
      _ -> pprPanic "tcTyClDecl" (ppr thing)
720 721

  | otherwise
722
  = setSrcSpan loc $ tcAddDeclCtxt decl $
723
    do { traceTc "tcTyAndCl-x" (ppr decl)
Edward Z. Yang's avatar
Edward Z. Yang committed
724
       ; tcTyClDecl1 Nothing roles_info decl }
725

726
  -- "type family" declarations
Edward Z. Yang's avatar
Edward Z. Yang committed
727 728
tcTyClDecl1 :: Maybe Class -> RolesInfo -> TyClDecl Name -> TcM TyCon
tcTyClDecl1 parent _roles_info (FamDecl { tcdFam = fd })
729
  = tcFamDecl1 parent fd
730

731
  -- "type" synonym declaration
Edward Z. Yang's avatar
Edward Z. Yang committed
732
tcTyClDecl1 _parent roles_info
733
            (SynDecl { tcdLName = L _ tc_name, tcdRhs = rhs })
734
  = ASSERT( isNothing _parent )
735
    tcTyClTyVars tc_name $ \ binders res_kind ->
Edward Z. Yang's avatar
Edward Z. Yang committed
736
    tcTySynRhs roles_info tc_name binders res_kind rhs
737

738
  -- "data/newtype" declaration
Edward Z. Yang's avatar
Edward Z. Yang committed
739
tcTyClDecl1 _parent roles_info
740
            (DataDecl { tcdLName = L _ tc_name, tcdDataDefn = defn })
741
  = ASSERT( isNothing _parent )
742
    tcTyClTyVars tc_name $ \ tycon_binders res_kind ->
Edward Z. Yang's avatar
Edward Z. Yang committed
743
    tcDataDefn roles_info tc_name tycon_binders res_kind defn
744

Edward Z. Yang's avatar
Edward Z. Yang committed
745
tcTyClDecl1 _parent roles_info
746
            (ClassDecl { tcdLName = L _ class_name
747
            , tcdCtxt = ctxt, tcdMeths = meths
748
            , tcdFDs = fundeps, tcdSigs = sigs
749
            , tcdATs = ats, tcdATDefs = at_defs })
750
  = ASSERT( isNothing _parent )
751
    do { clas <- fixM $ \ clas ->
Gabor Greif's avatar
Gabor Greif committed
752
            -- We need the knot because 'clas' is passed into tcClassATs
753
            tcTyClTyVars class_name $ \ binders res_kind ->
754
            do { MASSERT( isConstraintKind res_kind )
755
               ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr binders)
756 757
               ; let tycon_name = class_name        -- We use the same name
                     roles = roles_info tycon_name  -- for TyCon and Class
dreixel's avatar
dreixel committed
758

759
               ; ctxt' <- solveEqualities $ tcHsContext ctxt
760
               ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'
761 762
                       -- Squeeze out any kind unification variables
               ; fds'  <- mapM (addLocM tc_fundep) fundeps
763
               ; sig_stuff <- tcClassSigs class_name sigs meths
764
               ; at_stuff <- tcClassATs class_name clas ats at_defs
765
               ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
766
               ; clas <- buildClass
767
                            class_name binders roles ctxt'
768
                            fds' at_stuff
Edward Z. Yang's avatar
Edward Z. Yang committed
769
                            sig_stuff mindef
770
               ; traceTc "tcClassDecl" (ppr fundeps $$ ppr binders $$
771
                                        ppr fds')
772 773 774
               ; return clas }

         ; return (classTyCon clas) }
775
  where
776 777
    tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM (tcLookupTyVar . unLoc) tvs1 ;
                                ; tvs2' <- mapM (tcLookupTyVar . unLoc) tvs2 ;
778
                                ; return (tvs1', tvs2') }
Jan Stolarek's avatar
Jan Stolarek committed
779

780
tcFamDecl1 :: Maybe Class -> FamilyDecl Name -> TcM TyCon
781
tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_name)
782 783
                              , fdTyVars = tvs, fdResultSig = L _ sig
                              , fdInjectivityAnn = inj })
784
  | DataFamily <- fam_info
785
  = tcTyClTyVars tc_name $ \ binders res_kind -> do
786 787
  { traceTc "data family:" (ppr tc_name)
  ; checkFamFlag tc_name
788
  ; (extra_binders, real_res_kind) <- tcDataKindSig res_kind
789
  ; tc_rep_name <- newTyConRepName tc_name
790 791
  ; let tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders)
                              real_res_kind
792 793 794 795 796 797
                              (resultVariableName sig)
                              (DataFamilyTyCon tc_rep_name)
                              parent NotInjective
  ; return tycon }

  | OpenTypeFamily <- fam_info
798
  = tcTyClTyVars tc_name $ \ binders res_kind -> do
799
  { traceTc "open type family:" (ppr tc_name)
800
  ; checkFamFlag tc_name
801 802
  ; inj' <- tcInjectivity binders inj
  ; let tycon = mkFamilyTyCon tc_name binders res_kind