TcTyClsDecls.hs 120 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 67
import Maybes
import Unify
import Util
import SrcLoc
import ListSetOps
import Digraph
import DynFlags
68
import Unique
69
import BasicTypes
70
import qualified GHC.LanguageExtensions as LangExt
71

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

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

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

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

111 112 113 114 115 116 117 118
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
                         )
119
-- Fails if there are any errors
Simon Peyton Jones's avatar
Simon Peyton Jones committed
120
tcTyAndClassDecls tyclds_s
121 122 123 124
  -- 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
125
  where
126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143
    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
144
-- See Note [TyClGroups and dependency analysis] in HsDecls
145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177
tcTyClGroup (TyClGroup { group_tyclds = tyclds
                       , group_roles  = roles
                       , group_instds = instds })
  = do { let role_annots = mkRoleAnnotEnv roles

           -- Step 1: Typecheck the type/class declarations
       ; tyclss <- tcTyClDecls tyclds role_annots

           -- 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
178 179 180
  = 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]
181 182
         tc_tycons <- kcTyClGroup tyclds
       ; traceTc "tcTyAndCl generalized kinds" (vcat (map ppr_tc_tycon tc_tycons))
dreixel's avatar
dreixel committed
183

184 185
            -- Step 2: type-check all groups together, returning
            -- the final TyCons and Classes
186
       ; fixM $ \ ~rec_tyclss -> do
Simon Peyton Jones's avatar
Simon Peyton Jones committed
187
           { is_boot   <- tcIsHsBootOrSig
Edward Z. Yang's avatar
Edward Z. Yang committed
188
           ; let roles = inferRoles is_boot role_annots rec_tyclss
dreixel's avatar
dreixel committed
189 190 191

                 -- 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
192
                 -- (see Note [Recusion and promoting data constructors])
193
                 -- we will have failed already in kcTyClGroup, so no worries here
194
           ; tcExtendRecEnv (zipRecTyClss tc_tycons rec_tyclss) $
dreixel's avatar
dreixel committed
195 196 197

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

                 -- Kind and type check declarations for this group
Edward Z. Yang's avatar
Edward Z. Yang committed
202
               mapM (tcTyClDecl roles) tyclds
203
           } }
204 205 206 207
  where
    ppr_tc_tycon tc = parens (sep [ ppr (tyConName tc) <> comma
                                  , ppr (tyConBinders tc) <> comma
                                  , ppr (tyConResKind tc) ])
dreixel's avatar
dreixel committed
208

209
zipRecTyClss :: [TcTyCon]
210
             -> [TyCon]           -- Knot-tied
211
             -> [(Name,TyThing)]
212 213
-- 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
214
-- The TyThings in the result list must have a visible ATyCon,
215 216
-- because typechecking types (in, say, tcTyClDecl) looks at
-- this outer constructor
217 218
zipRecTyClss tc_tycons rec_tycons
  = [ (name, ATyCon (get name)) | tc_tycon <- tc_tycons, let name = getName tc_tycon ]
219
  where
220 221
    rec_tc_env :: NameEnv TyCon
    rec_tc_env = foldr add_tc emptyNameEnv rec_tycons
222

223 224 225 226 227 228 229 230 231
    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)
232

Austin Seipp's avatar
Austin Seipp committed
233 234 235
{-
************************************************************************
*                                                                      *
236
                Kind checking
Austin Seipp's avatar
Austin Seipp committed
237 238
*                                                                      *
************************************************************************
239

240 241 242 243
Note [Kind checking for type and class decls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Kind checking is done thus:

244 245 246
   1. Make up a kind variable for each parameter of the *data* type, class,
      and closed type family decls, and extend the kind environment (which is
      in the TcLclEnv)
247 248 249 250 251 252

   2. Dependency-analyse the type *synonyms* (which must be non-recursive),
      and kind-check them in dependency order.  Extend the kind envt.

   3. Kind check the data type and class decls

253 254
We need to kind check all types in the mutually recursive group
before we know the kind of the type variables.  For example:
255

256 257
  class C a where
     op :: D b => a -> b -> b
258

259 260
  class D c where
     bop :: (Monad c) => ...
261 262 263 264 265

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.

266 267
However type synonyms work differently.  They can have kinds which don't
just involve (->) and *:
268 269 270
        type R = Int#           -- Kind #
        type S a = Array# a     -- Kind * -> #
        type T a b = (# a,b #)  -- Kind * -> * -> (# a,b #)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
271 272 273 274 275 276 277 278 279 280
and a kind variable can't unify with UnboxedTypeKind.

So we must infer the kinds of type synonyms from their right-hand
sides *first* and then use them, whereas for the mutually recursive
data types D we bring into scope kind bindings D -> k, where k is a
kind variable, and do inference.

NB: synonyms can be mutually recursive with data type declarations though!
   type T = D -> D
   data D = MkD Int T
281

282 283
Open type families
~~~~~~~~~~~~~~~~~~
284 285 286
This treatment of type synonyms only applies to Haskell 98-style synonyms.
General type functions can be recursive, and hence, appear in `alg_decls'.

287
The kind of an open type family is solely determinded by its kind signature;
288
hence, only kind signatures participate in the construction of the initial
289 290 291 292
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').
293 294 295 296


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

Austin Seipp's avatar
Austin Seipp committed
297
-}
298

299
kcTyClGroup :: [LTyClDecl Name] -> TcM [TcTyCon]
dreixel's avatar
dreixel committed
300
-- Kind check this group, kind generalize, and return the resulting local env
301
-- This bindds the TyCons and Classes of the group, but not the DataCons
dreixel's avatar
dreixel committed
302
-- See Note [Kind checking for type and class decls]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
303 304
-- Third return value is Nothing if the tycon be unsaturated; otherwise,
-- the arity
305
kcTyClGroup decls
306
  = do  { mod <- getModule
307
        ; traceTc "kcTyClGroup" (text "module" <+> ppr mod $$ vcat (map ppr decls))
dreixel's avatar
dreixel committed
308

309 310
          -- Kind checking;
          --    1. Bind kind variables for non-synonyms
dreixel's avatar
dreixel committed
311 312
          --    2. Kind-check synonyms, and bind kinds of those synonyms
          --    3. Kind-check non-synonyms
313
          --    4. Generalise the inferred kinds
dreixel's avatar
dreixel committed
314 315
          -- See Note [Kind checking for type and class decls]

316
        ; lcl_env <- solveEqualities $
317 318 319 320
          do {
               -- Step 1: Bind kind variables for non-synonyms
               let (syn_decls, non_syn_decls) = partition (isSynDecl . unLoc) decls
             ; initial_kinds <- getInitialKinds non_syn_decls
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
321 322
             ; traceTc "kcTyClGroup: initial kinds" $
               vcat (map pp_initial_kind initial_kinds)
323

324 325 326
             -- Step 2: Set initial envt, kind-check the synonyms
             ; lcl_env <- tcExtendKindEnv2 initial_kinds $
                          kcSynDecls (calcSynCycles syn_decls)
327

328 329 330 331 332
             -- Step 3: Set extended envt, kind-check the non-synonyms
             ; setLclEnv lcl_env $
               mapM_ kcLTyClDecl non_syn_decls

             ; return lcl_env }
dreixel's avatar
dreixel committed
333

334 335
             -- Step 4: generalisation
             -- Kind checking done for this group
dreixel's avatar
dreixel committed
336
             -- Now we have to kind generalize the flexis
337
        ; res <- concatMapM (generaliseTCD (tcl_env lcl_env)) decls
338

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
339
        ; traceTc "kcTyClGroup result" (vcat (map pp_res res))
340
        ; return res }
341

342
  where
343
    generalise :: TcTypeEnv -> Name -> TcM TcTyCon
344
    -- For polymorphic things this is a no-op
345
    generalise kind_env name
346 347 348 349 350
      = 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
351
                 kc_tyvars   = tyConTyVars tc
352
           ; kvs <- kindGeneralize (mkTyConKind kc_binders kc_res_kind)
353
           ; let all_binders = mkNamedTyConBinders Inferred kvs ++ kc_binders
354

355 356
           ; (env, all_binders') <- zonkTyConBinders emptyZonkEnv all_binders
           ; kc_res_kind'        <- zonkTcTypeToType env kc_res_kind
357 358

                      -- Make sure kc_kind' has the final, zonked kind variables
359
           ; traceTc "Generalise kind" $
360 361
             vcat [ ppr name, ppr kc_binders, ppr kvs, ppr all_binders, ppr kc_res_kind
                  , ppr all_binders', ppr kc_res_kind'
362
                  , ppr kc_tyvars, ppr (tcTyConScopedTyVars tc)]
363

364
           ; return (mkTcTyCon name all_binders' kc_res_kind'
365 366
                               (mightBeUnsaturatedTyCon tc)
                               (tcTyConScopedTyVars tc)) }
dreixel's avatar
dreixel committed
367

368
    generaliseTCD :: TcTypeEnv
369
                  -> LTyClDecl Name -> TcM [TcTyCon]
370
    generaliseTCD kind_env (L _ decl)
371 372
      | ClassDecl { tcdLName = (L _ name), tcdATs = ats } <- decl
      = do { first <- generalise kind_env name
373 374 375 376 377 378 379 380
           ; rest <- mapM ((generaliseFamDecl kind_env) . unLoc) ats
           ; return (first : rest) }

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

      | otherwise
381
      = do { res <- generalise kind_env (tcdName decl)
382 383
           ; return [res] }

384
    generaliseFamDecl :: TcTypeEnv
385
                      -> FamilyDecl Name -> TcM TcTyCon
386 387
    generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name })
      = generalise kind_env name
388

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
389 390 391 392 393 394 395
    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)

396
mkTcTyConPair :: TcTyCon -> (Name, TcTyThing)
397
-- Makes a binding to put in the local envt, binding
398 399 400
-- a name to a TcTyCon
mkTcTyConPair tc
  = (getName tc, ATcTyCon tc)
401

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

414
getInitialKinds :: [LTyClDecl Name] -> TcM [(Name, TcTyThing)]
415
getInitialKinds decls
416
  = tcExtendKindEnv2 (mk_thing_env decls) $
417 418
    do { pairss <- mapM (addLocM getInitialKind) decls
       ; return (concat pairss) }
419

420 421
getInitialKind :: TyClDecl Name
               -> TcM [(Name, TcTyThing)]    -- Mixture of ATcTyCon and APromotionErr
dreixel's avatar
dreixel committed
422
-- Allocate a fresh kind variable for each TyCon and Class
423
-- For each tycon, return   (name, ATcTyCon (TcCyCon with kind k))
dreixel's avatar
dreixel committed
424 425 426 427
--                 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 = ...
428
--      return (T, kv1 -> kv2 -> kv3)
dreixel's avatar
dreixel committed
429
--
430 431 432 433 434
-- 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)
435
--    See Note [ARecDataCon: Recursion and promoting data constructors]
436
--
437
-- No family instances are passed to getInitialKinds
dreixel's avatar
dreixel committed
438

439
getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
440 441
  = do { (tycon, inner_prs) <-
           kcHsTyVarBndrs name True cusk False True ktvs $
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
442
           do { inner_prs <- getFamDeclInitialKinds (Just cusk) ats
443
              ; return (constraintKind, inner_prs) }
444
       ; return (mkTcTyConPair tycon : inner_prs) }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
445 446
  where
    cusk = hsDeclHasCusk decl
447

448
getInitialKind decl@(DataDecl { tcdLName = L _ name
449 450
                              , tcdTyVars = ktvs
                              , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
451
                                                         , dd_cons = cons } })
452 453
  = do  { (tycon, _) <-
           kcHsTyVarBndrs name True (hsDeclHasCusk decl) False True ktvs $
454 455 456
           do { res_k <- case m_sig of
                           Just ksig -> tcLHsKind ksig
                           Nothing   -> return liftedTypeKind
457
              ; return (res_k, ()) }
458
        ; let inner_prs = [ (unLoc con, APromotionErr RecDataConPE)
459
                          | L _ con' <- cons, con <- getConNames con' ]
460
        ; return (mkTcTyConPair tycon : inner_prs) }
461

Jan Stolarek's avatar
Jan Stolarek committed
462
getInitialKind (FamDecl { tcdFam = decl })
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
463
  = getFamDeclInitialKind Nothing decl
464

Jan Stolarek's avatar
Jan Stolarek committed
465
getInitialKind decl@(SynDecl {})
466 467 468
  = pprPanic "getInitialKind" (ppr decl)

---------------------------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
469 470 471
getFamDeclInitialKinds :: Maybe Bool  -- if assoc., CUSKness of assoc. class
                       -> [LFamilyDecl Name] -> TcM [(Name, TcTyThing)]
getFamDeclInitialKinds mb_cusk decls
472 473
  = tcExtendKindEnv2 [ (n, APromotionErr TyConPE)
                     | L _ (FamilyDecl { fdLName = L _ n }) <- decls] $
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
474
    concatMapM (addLocM (getFamDeclInitialKind mb_cusk)) decls
475

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
476 477
getFamDeclInitialKind :: Maybe Bool  -- if assoc., CUSKness of assoc. class
                      -> FamilyDecl Name
478
                      -> TcM [(Name, TcTyThing)]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
479 480 481 482
getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName     = L _ name
                                               , fdTyVars    = ktvs
                                               , fdResultSig = L _ resultSig
                                               , fdInfo      = info })
483 484
  = do { (tycon, _) <-
           kcHsTyVarBndrs name unsat cusk open True ktvs $
Jan Stolarek's avatar
Jan Stolarek committed
485 486 487 488
           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
489
                        | open                     -> return liftedTypeKind
Jan Stolarek's avatar
Jan Stolarek committed
490 491 492
                        -- closed type families have their return kind inferred
                        -- by default
                        | otherwise                -> newMetaKindVar
493
              ; return (res_k, ()) }
494
       ; return [ mkTcTyConPair tycon ] }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
495
  where
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
496 497 498 499 500
    cusk  = famDeclHasCusk mb_cusk decl
    (open, unsat) = case info of
      DataFamily         -> (True,  True)
      OpenTypeFamily     -> (True,  False)
      ClosedTypeFamily _ -> (False, False)
501

502
----------------
503
kcSynDecls :: [SCC (LTyClDecl Name)]
504 505
           -> TcM TcLclEnv -- Kind bindings
kcSynDecls [] = getLclEnv
506
kcSynDecls (group : groups)
507
  = do  { tc <- kcSynDecl1 group
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
508
        ; traceTc "kcSynDecl" (ppr tc <+> dcolon <+> ppr (tyConKind tc))
509
        ; tcExtendKindEnv2 [ mkTcTyConPair tc ] $
510
          kcSynDecls groups }
dreixel's avatar
dreixel committed
511 512

kcSynDecl1 :: SCC (LTyClDecl Name)
513
           -> TcM TcTyCon -- Kind bindings
dreixel's avatar
dreixel committed
514 515
kcSynDecl1 (AcyclicSCC (L _ decl)) = kcSynDecl decl
kcSynDecl1 (CyclicSCC decls)       = do { recSynErr decls; failM }
516 517
                                     -- Fail here to avoid error cascade
                                     -- of out-of-scope tycons
dreixel's avatar
dreixel committed
518

519
kcSynDecl :: TyClDecl Name -> TcM TcTyCon
520
kcSynDecl decl@(SynDecl { tcdTyVars = hs_tvs, tcdLName = L _ name
521
                        , tcdRhs = rhs })
522
  -- Returns a possibly-unzonked kind
dreixel's avatar
dreixel committed
523
  = tcAddDeclCtxt decl $
524 525
    do { (tycon, _) <-
           kcHsTyVarBndrs name False (hsDeclHasCusk decl) False True hs_tvs $
526 527 528 529
           do { traceTc "kcd1" (ppr name <+> brackets (ppr hs_tvs))
              ; (_, rhs_kind) <- tcLHsType rhs
              ; traceTc "kcd2" (ppr name)
              ; return (rhs_kind, ()) }
530
       ; return tycon }
531
kcSynDecl decl = pprPanic "kcSynDecl" (ppr decl)
532

533
------------------------------------------------------------------------
534
kcLTyClDecl :: LTyClDecl Name -> TcM ()
535
  -- See Note [Kind checking for type and class decls]
536 537 538
kcLTyClDecl (L loc decl)
  = setSrcSpan loc $ tcAddDeclCtxt decl $ kcTyClDecl decl

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

545
kcTyClDecl (DataDecl { tcdLName = L _ name, tcdDataDefn = defn })
546
  | HsDataDefn { dd_cons = cons, dd_kindSig = Just _ } <- defn
547
  = mapM_ (wrapLocM kcConDecl) cons
548 549 550 551 552 553
    -- 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
554

555
  | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
556
  = kcTyClTyVars name $
557
    do  { _ <- tcHsContext ctxt
558
        ; mapM_ (wrapLocM kcConDecl) cons }
559

560
kcTyClDecl decl@(SynDecl {}) = pprPanic "kcTyClDecl" (ppr decl)
561

562 563 564
kcTyClDecl (ClassDecl { tcdLName = L _ name
                      , tcdCtxt = ctxt, tcdSigs = sigs })
  = kcTyClTyVars name $
565
    do  { _ <- tcHsContext ctxt
566
        ; mapM_ (wrapLocM kc_sig)     sigs }
dreixel's avatar
dreixel committed
567
  where
Alan Zimmerman's avatar
Alan Zimmerman committed
568
    kc_sig (ClassOpSig _ nms op_ty) = kcHsSigType nms op_ty
569
    kc_sig _                        = return ()
570

571
kcTyClDecl (FamDecl (FamilyDecl { fdLName  = L _ fam_tc_name
572 573 574 575 576
                                , 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) ->
577 578
        do { fam_tc <- kcLookupTcTyCon fam_tc_name
           ; mapM_ (kcTyFamInstEqn (famTyConShape fam_tc)) eqns }
579
      _ -> return ()
dreixel's avatar
dreixel committed
580 581

-------------------
582
kcConDecl :: ConDecl Name -> TcM ()
Alan Zimmerman's avatar
Alan Zimmerman committed
583 584 585
kcConDecl (ConDeclH98 { con_name = name, con_qvars = ex_tvs
                      , con_cxt = ex_ctxt, con_details = details })
  = addErrCtxt (dataConCtxtName [name]) $
586 587
         -- 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
588
         -- into scope.
589
    do { _ <- kcHsTyVarBndrs (unLoc name) False False False False
590
                             ((fromMaybe emptyLHsQTvs ex_tvs)) $
Alan Zimmerman's avatar
Alan Zimmerman committed
591
              do { _ <- tcHsContext (fromMaybe (noLoc []) ex_ctxt)
592 593
                 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details)
                 ; return (panic "kcConDecl", ()) }
594 595
              -- We don't need to check the telescope here, because that's
              -- done in tcConDecl
596
       ; return () }
597

Alan Zimmerman's avatar
Alan Zimmerman committed
598 599 600 601 602 603 604
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
605
{-
606 607
Note [Recursion and promoting data constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
608 609 610 611 612 613 614 615
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:
616 617
  T -> ATcTyCon <some initial kind>
  K -> APromotionErr
618

619
APromotionErr is only used for DataCons, and only used during type checking
620 621
in tcTyClGroup.

622

Austin Seipp's avatar
Austin Seipp committed
623 624
************************************************************************
*                                                                      *
625
\subsection{Type checking}
Austin Seipp's avatar
Austin Seipp committed
626 627
*                                                                      *
************************************************************************
628

dreixel's avatar
dreixel committed
629 630 631 632
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,
633
we discarded the kind-checked types (eg RHSs of data type decls);
dreixel's avatar
dreixel committed
634 635 636 637 638 639 640
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
641
    to be given kind arguments.
dreixel's avatar
dreixel committed
642 643 644 645 646 647 648

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

dreixel's avatar
dreixel committed
650 651 652 653 654 655 656
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

657 658
  *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
659 660 661 662 663 664 665 666 667 668

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

673 674 675 676 677 678 679 680 681 682 683
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
684
declarations]): in the *local* environment, with ATcTyCon. But we still
685 686 687 688 689 690 691 692 693 694 695
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.

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

Edward Z. Yang's avatar
Edward Z. Yang committed
704 705
tcTyClDecl :: RolesInfo -> LTyClDecl Name -> TcM TyCon
tcTyClDecl roles_info (L loc decl)
706
  | Just thing <- wiredInNameTyThing_maybe (tcdName decl)
707 708 709
  = case thing of -- See Note [Declarations for wired-in things]
      ATyCon tc -> return tc
      _ -> pprPanic "tcTyClDecl" (ppr thing)
710 711

  | otherwise
712
  = setSrcSpan loc $ tcAddDeclCtxt decl $
713
    do { traceTc "tcTyAndCl-x" (ppr decl)
Edward Z. Yang's avatar
Edward Z. Yang committed
714
       ; tcTyClDecl1 Nothing roles_info decl }
715

716
  -- "type family" declarations
Edward Z. Yang's avatar
Edward Z. Yang committed
717 718
tcTyClDecl1 :: Maybe Class -> RolesInfo -> TyClDecl Name -> TcM TyCon
tcTyClDecl1 parent _roles_info (FamDecl { tcdFam = fd })
719
  = tcFamDecl1 parent fd
720

721
  -- "type" synonym declaration
Edward Z. Yang's avatar
Edward Z. Yang committed
722
tcTyClDecl1 _parent roles_info
723
            (SynDecl { tcdLName = L _ tc_name, tcdRhs = rhs })
724
  = ASSERT( isNothing _parent )
725
    tcTyClTyVars tc_name $ \ binders res_kind ->
Edward Z. Yang's avatar
Edward Z. Yang committed
726
    tcTySynRhs roles_info tc_name binders res_kind rhs
727

728
  -- "data/newtype" declaration
Edward Z. Yang's avatar
Edward Z. Yang committed
729
tcTyClDecl1 _parent roles_info
730
            (DataDecl { tcdLName = L _ tc_name, tcdDataDefn = defn })
731
  = ASSERT( isNothing _parent )
732
    tcTyClTyVars tc_name $ \ tycon_binders res_kind ->
Edward Z. Yang's avatar
Edward Z. Yang committed
733
    tcDataDefn roles_info tc_name tycon_binders res_kind defn
734

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

749
               ; ctxt' <- solveEqualities $ tcHsContext ctxt
750
               ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'
751 752
                       -- Squeeze out any kind unification variables
               ; fds'  <- mapM (addLocM tc_fundep) fundeps
753
               ; sig_stuff <- tcClassSigs class_name sigs meths
754
               ; at_stuff <- tcClassATs class_name clas ats at_defs
755
               ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
756
               ; clas <- buildClass
757
                            class_name binders roles ctxt'
758
                            fds' at_stuff
Edward Z. Yang's avatar
Edward Z. Yang committed
759
                            sig_stuff mindef
760
               ; traceTc "tcClassDecl" (ppr fundeps $$ ppr binders $$
761
                                        ppr fds')
762 763 764
               ; return clas }

         ; return (classTyCon clas) }
765
  where
766 767
    tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM (tcLookupTyVar . unLoc) tvs1 ;
                                ; tvs2' <- mapM (tcLookupTyVar . unLoc) tvs2 ;
768
                                ; return (tvs1', tvs2') }
Jan Stolarek's avatar
Jan Stolarek committed
769

770
tcFamDecl1 :: Maybe Class -> FamilyDecl Name -> TcM TyCon
771
tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_name)
772 773
                              , fdTyVars = tvs, fdResultSig = L _ sig
                              , fdInjectivityAnn = inj })
774
  | DataFamily <- fam_info
775
  = tcTyClTyVars tc_name $ \ binders res_kind -> do
776 777
  { traceTc "data family:" (ppr tc_name)
  ; checkFamFlag tc_name
778
  ; (extra_binders, real_res_kind) <- tcDataKindSig res_kind
779
  ; tc_rep_name <- newTyConRepName tc_name
780 781
  ; let tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders)
                              real_res_kind
782 783 784 785 786 787
                              (resultVariableName sig)
                              (DataFamilyTyCon tc_rep_name)
                              parent NotInjective
  ; return tycon }

  | OpenTypeFamily <- fam_info
788
  = tcTyClTyVars tc_name $ \ binders res_kind -> do