TcTyClsDecls.hs 117 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 TcUnify
34 35
import TcHsType
import TcMType
36
import TysWiredIn ( unitTy )
37
import TcType
38
import FamInst
Jan Stolarek's avatar
Jan Stolarek committed
39
import FamInstEnv
40
import Coercion
41
import Type
42
import TyCoRep   -- for checkValidRoles
dreixel's avatar
dreixel committed
43
import Kind
44
import Class
45
import CoAxiom
46 47
import TyCon
import DataCon
48
import Id
49
import Var
50
import VarEnv
51
import VarSet
52
import Module
53
import Name
54
import NameSet
55
import NameEnv
Adam Gundry's avatar
Adam Gundry committed
56
import RnEnv
sof's avatar
sof committed
57
import Outputable
58 59 60 61 62 63 64
import Maybes
import Unify
import Util
import SrcLoc
import ListSetOps
import Digraph
import DynFlags
65
import Unique
66
import BasicTypes
67
import qualified GHC.LanguageExtensions as LangExt
68

Ian Lynagh's avatar
Ian Lynagh committed
69
import Control.Monad
70
import Data.List
71

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

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

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
108
tcTyAndClassDecls :: [TyClGroup Name]   -- Mutually-recursive groups in dependency order
109 110
                  -> TcM TcGblEnv       -- Input env extended by types and classes
                                        -- and their implicit Ids,DataCons
111
-- Fails if there are any errors
Simon Peyton Jones's avatar
Simon Peyton Jones committed
112
tcTyAndClassDecls tyclds_s
113
  = checkNoErrs $       -- The code recovers internally, but if anything gave rise to
dreixel's avatar
dreixel committed
114
                        -- an error we'd better stop now, to avoid a cascade
115
    fold_env tyclds_s   -- Type check each group in dependency order folding the global env
dreixel's avatar
dreixel committed
116 117 118 119
  where
    fold_env :: [TyClGroup Name] -> TcM TcGblEnv
    fold_env [] = getGblEnv
    fold_env (tyclds:tyclds_s)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
120
      = do { tcg_env <- tcTyClGroup tyclds
121
           ; setGblEnv tcg_env $ fold_env tyclds_s }
dreixel's avatar
dreixel committed
122 123
             -- remaining groups are typecheck in the extended global env

Simon Peyton Jones's avatar
Simon Peyton Jones committed
124
tcTyClGroup :: TyClGroup Name -> TcM TcGblEnv
dreixel's avatar
dreixel committed
125
-- Typecheck one strongly-connected component of type and class decls
Simon Peyton Jones's avatar
Simon Peyton Jones committed
126
tcTyClGroup tyclds
dreixel's avatar
dreixel committed
127 128 129
  = 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]
130 131
         tc_tycons <- kcTyClGroup tyclds
       ; traceTc "tcTyAndCl generalized kinds" (vcat (map ppr_tc_tycon tc_tycons))
dreixel's avatar
dreixel committed
132

133 134
            -- Step 2: type-check all groups together, returning
            -- the final TyCons and Classes
135 136
       ; let role_annots = extractRoleAnnots tyclds
             decls = group_tyclds tyclds
Jan Stolarek's avatar
Jan Stolarek committed
137
       ; tyclss <- fixM $ \ ~rec_tyclss -> do
Simon Peyton Jones's avatar
Simon Peyton Jones committed
138 139 140
           { is_boot   <- tcIsHsBootOrSig
           ; self_boot <- tcSelfBootInfo
           ; let rec_flags = calcRecFlags self_boot is_boot
141
                                          role_annots rec_tyclss
dreixel's avatar
dreixel committed
142 143 144

                 -- 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
145
                 -- (see Note [Recusion and promoting data constructors])
146
                 -- we will have failed already in kcTyClGroup, so no worries here
147
           ; tcExtendRecEnv (zipRecTyClss tc_tycons rec_tyclss) $
dreixel's avatar
dreixel committed
148 149 150

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

                 -- Kind and type check declarations for this group
155
             mapM (tcTyClDecl rec_flags) decls }
dreixel's avatar
dreixel committed
156

157
           -- Step 3: Perform the validity check
dreixel's avatar
dreixel committed
158 159 160
           -- We can do this now because we are done with the recursive knot
           -- Do it before Step 4 (adding implicit things) because the latter
           -- expects well-formed TyCons
161 162 163
       ; traceTc "Starting validity check" (ppr tyclss)
       ; tyclss <- mapM checkValidTyCl tyclss
       ; traceTc "Done validity check" (ppr tyclss)
164 165
       ; mapM_ (recoverM (return ()) . checkValidRoleAnnots role_annots) tyclss
           -- See Note [Check role annotations in a second pass]
dreixel's avatar
dreixel committed
166 167 168 169

           -- Step 4: Add the implicit things;
           -- we want them in the environment because
           -- they may be mentioned in interface files
170 171
       ; tcExtendTyConEnv tyclss $
         tcAddImplicits tyclss }
172 173 174 175
  where
    ppr_tc_tycon tc = parens (sep [ ppr (tyConName tc) <> comma
                                  , ppr (tyConBinders tc) <> comma
                                  , ppr (tyConResKind tc) ])
dreixel's avatar
dreixel committed
176

177
zipRecTyClss :: [TcTyCon]
178
             -> [TyCon]           -- Knot-tied
179
             -> [(Name,TyThing)]
180 181
-- 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
182
-- The TyThings in the result list must have a visible ATyCon,
183 184
-- because typechecking types (in, say, tcTyClDecl) looks at
-- this outer constructor
185 186
zipRecTyClss tc_tycons rec_tycons
  = [ (name, ATyCon (get name)) | tc_tycon <- tc_tycons, let name = getName tc_tycon ]
187
  where
188 189
    rec_tc_env :: NameEnv TyCon
    rec_tc_env = foldr add_tc emptyNameEnv rec_tycons
190

191 192 193 194 195 196 197 198 199
    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)
200

Austin Seipp's avatar
Austin Seipp committed
201 202 203
{-
************************************************************************
*                                                                      *
204
                Kind checking
Austin Seipp's avatar
Austin Seipp committed
205 206
*                                                                      *
************************************************************************
207

208 209 210 211
Note [Kind checking for type and class decls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Kind checking is done thus:

212 213 214
   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)
215 216 217 218 219 220

   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

221 222
We need to kind check all types in the mutually recursive group
before we know the kind of the type variables.  For example:
223

224 225
  class C a where
     op :: D b => a -> b -> b
226

227 228
  class D c where
     bop :: (Monad c) => ...
229 230 231 232 233

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.

234 235
However type synonyms work differently.  They can have kinds which don't
just involve (->) and *:
236 237 238
        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
239 240 241 242 243 244 245 246 247 248
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
249

250 251
Open type families
~~~~~~~~~~~~~~~~~~
252 253 254
This treatment of type synonyms only applies to Haskell 98-style synonyms.
General type functions can be recursive, and hence, appear in `alg_decls'.

255
The kind of an open type family is solely determinded by its kind signature;
256
hence, only kind signatures participate in the construction of the initial
257 258 259 260
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').
261 262 263 264


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

Austin Seipp's avatar
Austin Seipp committed
265
-}
266

267
kcTyClGroup :: TyClGroup Name -> TcM [TcTyCon]
dreixel's avatar
dreixel committed
268
-- Kind check this group, kind generalize, and return the resulting local env
269
-- This bindds the TyCons and Classes of the group, but not the DataCons
dreixel's avatar
dreixel committed
270
-- See Note [Kind checking for type and class decls]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
271 272
-- Third return value is Nothing if the tycon be unsaturated; otherwise,
-- the arity
273
kcTyClGroup (TyClGroup { group_tyclds = decls })
274
  = do  { mod <- getModule
275
        ; traceTc "kcTyClGroup" (text "module" <+> ppr mod $$ vcat (map ppr decls))
dreixel's avatar
dreixel committed
276

277 278
          -- Kind checking;
          --    1. Bind kind variables for non-synonyms
dreixel's avatar
dreixel committed
279 280
          --    2. Kind-check synonyms, and bind kinds of those synonyms
          --    3. Kind-check non-synonyms
281
          --    4. Generalise the inferred kinds
dreixel's avatar
dreixel committed
282 283
          -- See Note [Kind checking for type and class decls]

284
        ; lcl_env <- solveEqualities $
285 286 287 288
          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
289 290
             ; traceTc "kcTyClGroup: initial kinds" $
               vcat (map pp_initial_kind initial_kinds)
291

292 293 294
             -- Step 2: Set initial envt, kind-check the synonyms
             ; lcl_env <- tcExtendKindEnv2 initial_kinds $
                          kcSynDecls (calcSynCycles syn_decls)
295

296 297 298 299 300
             -- 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
301

302 303
             -- Step 4: generalisation
             -- Kind checking done for this group
dreixel's avatar
dreixel committed
304
             -- Now we have to kind generalize the flexis
305
        ; res <- concatMapM (generaliseTCD (tcl_env lcl_env)) decls
306

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
307
        ; traceTc "kcTyClGroup result" (vcat (map pp_res res))
308
        ; return res }
309

310
  where
311
    generalise :: TcTypeEnv -> Name -> TcM TcTyCon
312
    -- For polymorphic things this is a no-op
313
    generalise kind_env name
314 315 316 317 318 319 320
      = 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
           ; kvs <- kindGeneralize (mkForAllTys kc_binders kc_res_kind)
           ; (kc_binders', kc_res_kind') <- zonkTcKindToKind kc_binders kc_res_kind
321 322

                      -- Make sure kc_kind' has the final, zonked kind variables
323 324
           ; traceTc "Generalise kind" $
             vcat [ ppr name, ppr kc_binders, ppr kc_res_kind
325
                  , ppr kvs, ppr kc_binders', ppr kc_res_kind' ]
326 327

           ; return (mkTcTyCon name
328
                               (mkNamedBinders Invisible kvs ++ kc_binders')
329 330
                               kc_res_kind'
                               (mightBeUnsaturatedTyCon tc)) }
dreixel's avatar
dreixel committed
331

332
    generaliseTCD :: TcTypeEnv
333
                  -> LTyClDecl Name -> TcM [TcTyCon]
334
    generaliseTCD kind_env (L _ decl)
335 336
      | ClassDecl { tcdLName = (L _ name), tcdATs = ats } <- decl
      = do { first <- generalise kind_env name
337 338 339 340 341 342 343 344
           ; rest <- mapM ((generaliseFamDecl kind_env) . unLoc) ats
           ; return (first : rest) }

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

      | otherwise
345
      = do { res <- generalise kind_env (tcdName decl)
346 347
           ; return [res] }

348
    generaliseFamDecl :: TcTypeEnv
349
                      -> FamilyDecl Name -> TcM TcTyCon
350 351
    generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name })
      = generalise kind_env name
352

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
353 354 355 356 357 358 359
    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)

360
mkTcTyConPair :: TcTyCon -> (Name, TcTyThing)
361
-- Makes a binding to put in the local envt, binding
362 363 364
-- a name to a TcTyCon
mkTcTyConPair tc
  = (getName tc, ATcTyCon tc)
365

366 367 368 369 370 371 372 373 374 375 376 377
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)

378
getInitialKinds :: [LTyClDecl Name] -> TcM [(Name, TcTyThing)]
379
getInitialKinds decls
380
  = tcExtendKindEnv2 (mk_thing_env decls) $
381 382
    do { pairss <- mapM (addLocM getInitialKind) decls
       ; return (concat pairss) }
383

384 385
getInitialKind :: TyClDecl Name
               -> TcM [(Name, TcTyThing)]    -- Mixture of ATcTyCon and APromotionErr
dreixel's avatar
dreixel committed
386
-- Allocate a fresh kind variable for each TyCon and Class
387
-- For each tycon, return   (name, ATcTyCon (TcCyCon with kind k))
dreixel's avatar
dreixel committed
388 389 390 391
--                 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 = ...
392
--      return (T, kv1 -> kv2 -> kv3)
dreixel's avatar
dreixel committed
393
--
394 395 396 397 398
-- 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)
399
--    See Note [ARecDataCon: Recursion and promoting data constructors]
400
--
401
-- No family instances are passed to getInitialKinds
dreixel's avatar
dreixel committed
402

403
getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
404
  = do { (cl_binders, cl_kind, inner_prs) <-
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
405 406
           kcHsTyVarBndrs cusk False True ktvs $
           do { inner_prs <- getFamDeclInitialKinds (Just cusk) ats
407
              ; return (constraintKind, inner_prs) }
408 409 410
       ; cl_binders <- mapM zonkTcTyBinder cl_binders
       ; cl_kind    <- zonkTcType cl_kind
       ; let main_pr = mkTcTyConPair (mkTcTyCon name cl_binders cl_kind True)
411
       ; return (main_pr : inner_prs) }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
412 413
  where
    cusk = hsDeclHasCusk decl
414

415
getInitialKind decl@(DataDecl { tcdLName = L _ name
416 417
                              , tcdTyVars = ktvs
                              , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
418
                                                         , dd_cons = cons } })
419
  = do  { (decl_binders, decl_kind, _) <-
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
420
           kcHsTyVarBndrs (hsDeclHasCusk decl) False True ktvs $
421 422 423
           do { res_k <- case m_sig of
                           Just ksig -> tcLHsKind ksig
                           Nothing   -> return liftedTypeKind
424
              ; return (res_k, ()) }
425 426 427
        ; decl_binders <- mapM zonkTcTyBinder decl_binders
        ; decl_kind    <- zonkTcType decl_kind
        ; let main_pr = mkTcTyConPair (mkTcTyCon name decl_binders decl_kind True)
428 429 430
              inner_prs = [ (unLoc con, APromotionErr RecDataConPE)
                          | L _ con' <- cons, con <- getConNames con' ]
        ; return (main_pr : inner_prs) }
431

Jan Stolarek's avatar
Jan Stolarek committed
432
getInitialKind (FamDecl { tcdFam = decl })
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
433
  = getFamDeclInitialKind Nothing decl
434

Jan Stolarek's avatar
Jan Stolarek committed
435
getInitialKind decl@(SynDecl {})
436 437 438
  = pprPanic "getInitialKind" (ppr decl)

---------------------------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
439 440 441
getFamDeclInitialKinds :: Maybe Bool  -- if assoc., CUSKness of assoc. class
                       -> [LFamilyDecl Name] -> TcM [(Name, TcTyThing)]
getFamDeclInitialKinds mb_cusk decls
442 443
  = tcExtendKindEnv2 [ (n, APromotionErr TyConPE)
                     | L _ (FamilyDecl { fdLName = L _ n }) <- decls] $
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
444
    concatMapM (addLocM (getFamDeclInitialKind mb_cusk)) decls
445

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
446 447
getFamDeclInitialKind :: Maybe Bool  -- if assoc., CUSKness of assoc. class
                      -> FamilyDecl Name
448
                      -> TcM [(Name, TcTyThing)]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
449 450 451 452
getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName     = L _ name
                                               , fdTyVars    = ktvs
                                               , fdResultSig = L _ resultSig
                                               , fdInfo      = info })
453
  = do { (fam_binders, fam_kind, _) <-
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
454
           kcHsTyVarBndrs cusk open True ktvs $
Jan Stolarek's avatar
Jan Stolarek committed
455 456 457 458
           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
459
                        | open                     -> return liftedTypeKind
Jan Stolarek's avatar
Jan Stolarek committed
460 461 462
                        -- closed type families have their return kind inferred
                        -- by default
                        | otherwise                -> newMetaKindVar
463
              ; return (res_k, ()) }
464 465 466
       ; fam_binders <- mapM zonkTcTyBinder fam_binders
       ; fam_kind    <- zonkTcType fam_kind
       ; return [ mkTcTyConPair (mkTcTyCon name fam_binders fam_kind unsat) ] }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
467
  where
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
468 469 470 471 472
    cusk  = famDeclHasCusk mb_cusk decl
    (open, unsat) = case info of
      DataFamily         -> (True,  True)
      OpenTypeFamily     -> (True,  False)
      ClosedTypeFamily _ -> (False, False)
473

474
----------------
475
kcSynDecls :: [SCC (LTyClDecl Name)]
476 477
           -> TcM TcLclEnv -- Kind bindings
kcSynDecls [] = getLclEnv
478
kcSynDecls (group : groups)
479
  = do  { tc <- kcSynDecl1 group
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
480
        ; traceTc "kcSynDecl" (ppr tc <+> dcolon <+> ppr (tyConKind tc))
481
        ; tcExtendKindEnv2 [ mkTcTyConPair tc ] $
482
          kcSynDecls groups }
dreixel's avatar
dreixel committed
483 484

kcSynDecl1 :: SCC (LTyClDecl Name)
485
           -> TcM TcTyCon -- Kind bindings
dreixel's avatar
dreixel committed
486 487
kcSynDecl1 (AcyclicSCC (L _ decl)) = kcSynDecl decl
kcSynDecl1 (CyclicSCC decls)       = do { recSynErr decls; failM }
488 489
                                     -- Fail here to avoid error cascade
                                     -- of out-of-scope tycons
dreixel's avatar
dreixel committed
490

491
kcSynDecl :: TyClDecl Name -> TcM TcTyCon
492
kcSynDecl decl@(SynDecl { tcdTyVars = hs_tvs, tcdLName = L _ name
493
                        , tcdRhs = rhs })
494
  -- Returns a possibly-unzonked kind
dreixel's avatar
dreixel committed
495
  = tcAddDeclCtxt decl $
496
    do { (syn_binders, syn_kind, _) <-
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
497
           kcHsTyVarBndrs (hsDeclHasCusk decl) False True hs_tvs $
498 499 500 501
           do { traceTc "kcd1" (ppr name <+> brackets (ppr hs_tvs))
              ; (_, rhs_kind) <- tcLHsType rhs
              ; traceTc "kcd2" (ppr name)
              ; return (rhs_kind, ()) }
502
       ; return (mkTcTyCon name syn_binders syn_kind False) }
503
kcSynDecl decl = pprPanic "kcSynDecl" (ppr decl)
504

505
------------------------------------------------------------------------
506
kcLTyClDecl :: LTyClDecl Name -> TcM ()
507
  -- See Note [Kind checking for type and class decls]
508 509 510
kcLTyClDecl (L loc decl)
  = setSrcSpan loc $ tcAddDeclCtxt decl $ kcTyClDecl decl

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

517 518
kcTyClDecl (DataDecl { tcdLName = L _ name, tcdTyVars = hs_tvs, tcdDataDefn = defn })
  | HsDataDefn { dd_cons = cons, dd_kindSig = Just _ } <- defn
519
  = mapM_ (wrapLocM kcConDecl) cons
520 521 522 523 524 525
    -- 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
526

527 528
  | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
  = kcTyClTyVars name hs_tvs $
529
    do  { _ <- tcHsContext ctxt
530
        ; mapM_ (wrapLocM kcConDecl) cons }
531

532
kcTyClDecl decl@(SynDecl {}) = pprPanic "kcTyClDecl" (ppr decl)
533 534

kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs
535 536
                       , tcdCtxt = ctxt, tcdSigs = sigs })
  = kcTyClTyVars name hs_tvs $
537
    do  { _ <- tcHsContext ctxt
538
        ; mapM_ (wrapLocM kc_sig)     sigs }
dreixel's avatar
dreixel committed
539
  where
Alan Zimmerman's avatar
Alan Zimmerman committed
540
    kc_sig (ClassOpSig _ nms op_ty) = kcHsSigType nms op_ty
541
    kc_sig _                        = return ()
542

543 544
kcTyClDecl (FamDecl (FamilyDecl { fdLName  = L _ fam_tc_name
                                , fdTyVars = hs_tvs
545 546 547 548 549
                                , 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) ->
550
        do { (tc_binders, tc_res_kind) <- kcLookupKind fam_tc_name
551 552
           ; let fam_tc_shape = ( fam_tc_name
                                , length $ hsQTvExplicit hs_tvs
553 554
                                , tc_binders
                                , tc_res_kind )
555 556
           ; mapM_ (kcTyFamInstEqn fam_tc_shape) eqns }
      _ -> return ()
dreixel's avatar
dreixel committed
557 558

-------------------
559
kcConDecl :: ConDecl Name -> TcM ()
Alan Zimmerman's avatar
Alan Zimmerman committed
560 561 562
kcConDecl (ConDeclH98 { con_name = name, con_qvars = ex_tvs
                      , con_cxt = ex_ctxt, con_details = details })
  = addErrCtxt (dataConCtxtName [name]) $
563 564
         -- 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
565
         -- into scope.
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
566
    do { _ <- kcHsTyVarBndrs False False False ((fromMaybe emptyLHsQTvs ex_tvs)) $
Alan Zimmerman's avatar
Alan Zimmerman committed
567
              do { _ <- tcHsContext (fromMaybe (noLoc []) ex_ctxt)
568 569
                 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details)
                 ; return (panic "kcConDecl", ()) }
570 571
              -- We don't need to check the telescope here, because that's
              -- done in tcConDecl
572
       ; return () }
573

Alan Zimmerman's avatar
Alan Zimmerman committed
574 575 576 577 578 579 580
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
581
{-
582 583
Note [Recursion and promoting data constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
584 585 586 587 588 589 590 591
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:
592 593
  T -> ATcTyCon <some initial kind>
  K -> APromotionErr
594

595
APromotionErr is only used for DataCons, and only used during type checking
596 597
in tcTyClGroup.

598

Austin Seipp's avatar
Austin Seipp committed
599 600
************************************************************************
*                                                                      *
601
\subsection{Type checking}
Austin Seipp's avatar
Austin Seipp committed
602 603
*                                                                      *
************************************************************************
604

dreixel's avatar
dreixel committed
605 606 607 608
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,
609
we discarded the kind-checked types (eg RHSs of data type decls);
dreixel's avatar
dreixel committed
610 611 612 613 614 615 616
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
617
    to be given kind arguments.
dreixel's avatar
dreixel committed
618 619 620 621 622 623 624

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

dreixel's avatar
dreixel committed
626 627 628 629 630 631 632
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

633 634
  *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
635 636 637 638 639 640 641 642 643 644

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

649 650 651 652 653 654 655 656 657 658 659
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
660
declarations]): in the *local* environment, with ATcTyCon. But we still
661 662 663 664 665 666 667 668 669 670 671
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.

672 673 674 675 676 677
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
678
-}
dreixel's avatar
dreixel committed
679

680
tcTyClDecl :: RecTyInfo -> LTyClDecl Name -> TcM TyCon
681
tcTyClDecl rec_info (L loc decl)
682
  | Just thing <- wiredInNameTyThing_maybe (tcdName decl)
683 684 685
  = case thing of -- See Note [Declarations for wired-in things]
      ATyCon tc -> return tc
      _ -> pprPanic "tcTyClDecl" (ppr thing)
686 687

  | otherwise
688
  = setSrcSpan loc $ tcAddDeclCtxt decl $
689
    do { traceTc "tcTyAndCl-x" (ppr decl)
690
       ; tcTyClDecl1 Nothing rec_info decl }
691

692
  -- "type family" declarations
693
tcTyClDecl1 :: Maybe Class -> RecTyInfo -> TyClDecl Name -> TcM TyCon
694
tcTyClDecl1 parent _rec_info (FamDecl { tcdFam = fd })
695
  = tcFamDecl1 parent fd
696

697
  -- "type" synonym declaration
698
tcTyClDecl1 _parent rec_info
699
            (SynDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdRhs = rhs })
700
  = ASSERT( isNothing _parent )
701 702
    tcTyClTyVars tc_name tvs $ \ kvs' tvs' binders res_kind ->
    tcTySynRhs rec_info tc_name (kvs' ++ tvs') binders res_kind rhs
703

704
  -- "data/newtype" declaration
705
tcTyClDecl1 _parent rec_info
706
            (DataDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdDataDefn = defn })
707
  = ASSERT( isNothing _parent )
708 709
    tcTyClTyVars tc_name tvs $ \ kvs' tvs' tycon_binders res_kind ->
    tcDataDefn rec_info tc_name (kvs' ++ tvs') tycon_binders res_kind defn
710

711
tcTyClDecl1 _parent rec_info
dreixel's avatar
dreixel committed
712
            (ClassDecl { tcdLName = L _ class_name, tcdTyVars = tvs
713
            , tcdCtxt = ctxt, tcdMeths = meths
714
            , tcdFDs = fundeps, tcdSigs = sigs
715
            , tcdATs = ats, tcdATDefs = at_defs })
716
  = ASSERT( isNothing _parent )
717
    do { clas <- fixM $ \ clas ->
718
            tcTyClTyVars class_name tvs $ \ kvs' tvs' binders res_kind ->
719
            do { MASSERT( isConstraintKind res_kind )
720 721 722
                 -- This little knot is just so we can get
                 -- hold of the name of the class TyCon, which we
                 -- need to look up its recursiveness
723
               ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr kvs' $$
724
                                          ppr tvs' $$ ppr binders)
725 726 727
               ; let tycon_name = tyConName (classTyCon clas)
                     tc_isrec = rti_is_rec rec_info tycon_name
                     roles = rti_roles rec_info tycon_name
dreixel's avatar
dreixel committed
728

729
               ; ctxt' <- solveEqualities $ tcHsContext ctxt
730
               ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'
731 732
                       -- Squeeze out any kind unification variables
               ; fds'  <- mapM (addLocM tc_fundep) fundeps
733
               ; sig_stuff <- tcClassSigs class_name sigs meths
734
               ; at_stuff <- tcClassATs class_name clas ats at_defs
735
               ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
736
               ; clas <- buildClass
737
                            class_name (kvs' ++ tvs') roles ctxt' binders
738
                            fds' at_stuff
739
                            sig_stuff mindef tc_isrec
740 741
               ; traceTc "tcClassDecl" (ppr fundeps $$ ppr (kvs' ++ tvs') $$
                                        ppr fds')
742 743 744
               ; return clas }

         ; return (classTyCon clas) }
745
  where
746 747
    tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM (tcLookupTyVar . unLoc) tvs1 ;
                                ; tvs2' <- mapM (tcLookupTyVar . unLoc) tvs2 ;
748
                                ; return (tvs1', tvs2') }
Jan Stolarek's avatar
Jan Stolarek committed
749

750
tcFamDecl1 :: Maybe Class -> FamilyDecl Name -> TcM TyCon
751
tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_name)
752 753
                              , fdTyVars = tvs, fdResultSig = L _ sig
                              , fdInjectivityAnn = inj })
754
  | DataFamily <- fam_info
755
  = tcTyClTyVars tc_name tvs $ \ kvs' tvs' binders res_kind -> do
756 757
  { traceTc "data family:" (ppr tc_name)
  ; checkFamFlag tc_name
758
  ; (extra_tvs, extra_binders, real_res_kind) <- tcDataKindSig res_kind
759 760
  ; tc_rep_name <- newTyConRepName tc_name
  ; let final_tvs = (kvs' ++ tvs') `chkAppend` extra_tvs -- we may not need these
761 762
        tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders)
                              real_res_kind final_tvs
763 764 765 766 767 768
                              (resultVariableName sig)
                              (DataFamilyTyCon tc_rep_name)
                              parent NotInjective
  ; return tycon }

  | OpenTypeFamily <- fam_info
769
  = tcTyClTyVars tc_name tvs $ \ kvs' tvs' binders res_kind -> do
770
  { traceTc "open type family:" (ppr tc_name)
771
  ; checkFamFlag tc_name
772 773
  ; let all_tvs = kvs' ++ tvs'
  ; inj' <- tcInjectivity all_tvs inj
774
  ; let tycon = mkFamilyTyCon tc_name binders res_kind all_tvs
775 776
                               (resultVariableName sig) OpenSynFamilyTyCon
                               parent inj'
777
  ; return tycon }
778

779 780 781 782
  | 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
783 784
         -- the variables in the header scope only over the injectivity
         -- declaration but this is not involved here
785 786 787 788 789 790
       ; (tvs', inj', binders, res_kind)
            <- tcTyClTyVars tc_name tvs
               $ \ kvs' tvs' binders res_kind ->
               do { let all_tvs = kvs' ++ tvs'
                  ; inj' <- tcInjectivity all_tvs inj
                  ; return (all_tvs, inj', binders, res_kind) }
791 792 793

       ; checkFamFlag tc_name -- make sure we have -XTypeFamilies

794 795 796
         -- If Nothing, this is an abstract family in a hs-boot file;
         -- but eqns might be empty in the Just case as well
       ; case mb_eqns of
797
           Nothing   ->
798
               return $ mkFamilyTyCon tc_name binders res_kind tvs'
799 800 801
                                      (resultVariableName sig)
                                      AbstractClosedSynFamilyTyCon parent
                                      inj'
802 803
           Just eqns -> do {

804
         -- Process the equations, creating CoAxBranches
805
       ; let fam_tc_shape = (tc_name, length $ hsQTvExplicit tvs, binders, res_kind)
Jan Stolarek's avatar
Jan Stolarek committed
806

807
       ; branches <- mapM (tcTyFamInstEqn fam_tc_shape Nothing) eqns
Jan Stolarek's avatar
Jan Stolarek committed
808 809 810 811 812
         -- Do not attempt to drop equations dominated by earlier
         -- ones here; in the case of mutual recursion with a data
         -- type, we get a knot-tying failure.  Instead we check
         -- for this afterwards, in TcValidity.checkValidCoAxiom
         -- Example: tc265
813

Jan Stolarek's avatar
Jan Stolarek committed
814
         -- Create a CoAxiom, with the correct src location. It is Vitally
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
815 816 817 818 819 820
         -- Important that we do not pass the branches into
         -- newFamInstAxiomName. They have types that have been zonked inside
         -- the knot and we will die if we look at them. This is OK here
         -- because there will only be one axiom, so we don't need to
         -- differentiate names.
         -- See [Zonking inside the knot] in TcHsType
821
       ; co_ax_name <- newFamInstAxiomName tc_lname []
822

823
       ; let mb_co_ax
Jan Stolarek's avatar
Jan Stolarek committed
824 825 826
              | null eqns = Nothing   -- mkBranchedCoAxiom fails on empty list
              | otherwise = Just (