TcTyClsDecls.hs 112 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 RnTypes( collectAnonWildCards )
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 IdInfo
50
import Var
51
import VarEnv
52
import VarSet
53
import Module
54
import Name
55
import NameSet
56
import NameEnv
Adam Gundry's avatar
Adam Gundry committed
57
import RnEnv
sof's avatar
sof committed
58
import Outputable
59 60 61 62 63 64 65
import Maybes
import Unify
import Util
import SrcLoc
import ListSetOps
import Digraph
import DynFlags
66
import FastString
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
#if __GLASGOW_HASKELL__ < 709
Alan Zimmerman's avatar
Alan Zimmerman committed
74
import Data.Monoid ( mempty )
75
#endif
76

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

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

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

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
129
tcTyClGroup :: TyClGroup Name -> TcM TcGblEnv
dreixel's avatar
dreixel committed
130
-- Typecheck one strongly-connected component of type and class decls
Simon Peyton Jones's avatar
Simon Peyton Jones committed
131
tcTyClGroup tyclds
dreixel's avatar
dreixel committed
132 133 134
  = 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]
135
         names_w_poly_kinds <- kcTyClGroup tyclds
dreixel's avatar
dreixel committed
136 137
       ; traceTc "tcTyAndCl generalized kinds" (ppr names_w_poly_kinds)

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

                 -- 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
150
                 -- (see Note [Recusion and promoting data constructors])
151 152
                 -- we will have failed already in kcTyClGroup, so no worries here
           ; tcExtendRecEnv (zipRecTyClss names_w_poly_kinds rec_tyclss) $
dreixel's avatar
dreixel committed
153 154 155

                 -- Also extend the local type envt with bindings giving
                 -- the (polymorphic) kind of each knot-tied TyCon or Class
156 157
                 -- See Note [Type checking recursive type and class declarations]
             tcExtendKindEnv names_w_poly_kinds              $
dreixel's avatar
dreixel committed
158 159

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

162
           -- Step 3: Perform the validity check
dreixel's avatar
dreixel committed
163 164 165
           -- 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
166 167 168
       ; traceTc "Starting validity check" (ppr tyclss)
       ; tyclss <- mapM checkValidTyCl tyclss
       ; traceTc "Done validity check" (ppr tyclss)
169 170
       ; mapM_ (recoverM (return ()) . checkValidRoleAnnots role_annots) tyclss
           -- See Note [Check role annotations in a second pass]
dreixel's avatar
dreixel committed
171 172 173 174

           -- Step 4: Add the implicit things;
           -- we want them in the environment because
           -- they may be mentioned in interface files
175 176
       ; tcExtendTyConEnv tyclss $
         tcAddImplicits tyclss }
dreixel's avatar
dreixel committed
177

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

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

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

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

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

   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

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

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

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

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.

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

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

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


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

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

268
kcTyClGroup :: TyClGroup Name -> TcM [(Name,Kind)]
dreixel's avatar
dreixel committed
269
-- Kind check this group, kind generalize, and return the resulting local env
270
-- This bindds the TyCons and Classes of the group, but not the DataCons
dreixel's avatar
dreixel committed
271
-- See Note [Kind checking for type and class decls]
272
kcTyClGroup (TyClGroup { group_tyclds = decls })
273 274
  = do  { mod <- getModule
        ; traceTc "kcTyClGroup" (ptext (sLit "module") <+> ppr mod $$ vcat (map ppr decls))
dreixel's avatar
dreixel committed
275

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

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

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

295 296 297 298 299 300 301
             -- Step 3: Set extended envt, kind-check the non-synonyms
             ; setLclEnv lcl_env $
               tcExtendRecEnv (tcTyConPairs initial_kinds) $
              -- See Note [Kind checking recursive type and class declarations]
               mapM_ kcLTyClDecl non_syn_decls

             ; return lcl_env }
dreixel's avatar
dreixel committed
302

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

        ; traceTc "kcTyClGroup result" (ppr res)
309
        ; return res }
310

311
  where
312 313 314 315 316
    tcTyConPairs :: [(Name,TcTyThing)] -> [(Name,TyThing)]
    tcTyConPairs initial_kinds = [ (name, ATyCon tc)
                                 | (name, AThing kind) <- initial_kinds
                                 , let tc = mkTcTyCon name kind ]

317
    generalise :: TcTypeEnv -> Name -> TcM (Name, Kind)
318
    -- For polymorphic things this is a no-op
319
    generalise kind_env name
320
      = do { let kc_kind = case lookupNameEnv kind_env name of
321 322
                               Just (AThing k) -> k
                               _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env)
323 324 325 326
           ; kvs <- kindGeneralize kc_kind
           ; kc_kind' <- zonkTcTypeToType emptyZonkEnv kc_kind

                      -- Make sure kc_kind' has the final, zonked kind variables
327
           ; traceTc "Generalise kind" (vcat [ ppr name, ppr kc_kind, ppr kvs, ppr kc_kind' ])
328
           ; return (name, mkInvForAllTys kvs kc_kind') }
dreixel's avatar
dreixel committed
329

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

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

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

346 347
    generaliseFamDecl :: TcTypeEnv
                      -> FamilyDecl Name -> TcM (Name, Kind)
348 349
    generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name })
      = generalise kind_env name
350

351 352 353 354 355 356 357 358 359 360 361 362
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)

363
getInitialKinds :: [LTyClDecl Name] -> TcM [(Name, TcTyThing)]
364
getInitialKinds decls
365
  = tcExtendKindEnv2 (mk_thing_env decls) $
366 367
    do { pairss <- mapM (addLocM getInitialKind) decls
       ; return (concat pairss) }
368

369
getInitialKind :: TyClDecl Name -> TcM [(Name, TcTyThing)]
dreixel's avatar
dreixel committed
370 371 372 373 374 375
-- Allocate a fresh kind variable for each TyCon and Class
-- For each tycon, return   (tc, AThing k)
--                 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 = ...
376
--      return (T, kv1 -> kv2 -> kv3)
dreixel's avatar
dreixel committed
377
--
378 379 380 381 382 383
-- 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)
-- Note [ARecDataCon: Recursion and promoting data constructors]
384
--
385
-- No family instances are passed to getInitialKinds
dreixel's avatar
dreixel committed
386

387
getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
388
  = do { (cl_kind, inner_prs) <-
389
           kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $ \_ _ ->
390 391
           do { inner_prs <- getFamDeclInitialKinds ats
              ; return (constraintKind, inner_prs) }
392
       ; cl_kind <- zonkTcType cl_kind
393
       ; let main_pr = (name, AThing cl_kind)
394
       ; return (main_pr : inner_prs) }
395

396
getInitialKind decl@(DataDecl { tcdLName = L _ name
397 398 399 400 401 402
                              , tcdTyVars = ktvs
                              , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
                                                         , dd_cons = cons' } })
  = let cons = cons' -- AZ list monad coming
    in
     do { (decl_kind, _) <-
403
           kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $ \_ _ ->
404 405 406
           do { res_k <- case m_sig of
                           Just ksig -> tcLHsKind ksig
                           Nothing   -> return liftedTypeKind
407
              ; return (res_k, ()) }
408 409 410 411 412
        ; decl_kind <- zonkTcType decl_kind
        ; let main_pr = (name, AThing decl_kind)
              inner_prs = [ (unLoc con, APromotionErr RecDataConPE)
                          | L _ con' <- cons, con <- getConNames con' ]
        ; return (main_pr : inner_prs) }
413

Jan Stolarek's avatar
Jan Stolarek committed
414
getInitialKind (FamDecl { tcdFam = decl })
415
  = getFamDeclInitialKind decl
416

Jan Stolarek's avatar
Jan Stolarek committed
417
getInitialKind decl@(SynDecl {})
418 419 420
  = pprPanic "getInitialKind" (ppr decl)

---------------------------------
421 422
getFamDeclInitialKinds :: [LFamilyDecl Name] -> TcM [(Name, TcTyThing)]
getFamDeclInitialKinds decls
423 424
  = tcExtendKindEnv2 [ (n, APromotionErr TyConPE)
                     | L _ (FamilyDecl { fdLName = L _ n }) <- decls] $
425
    concatMapM (addLocM getFamDeclInitialKind) decls
426

427
getFamDeclInitialKind :: FamilyDecl Name
428
                      -> TcM [(Name, TcTyThing)]
Jan Stolarek's avatar
Jan Stolarek committed
429 430 431
getFamDeclInitialKind decl@(FamilyDecl { fdLName     = L _ name
                                       , fdTyVars    = ktvs
                                       , fdResultSig = L _ resultSig })
432
  = do { (fam_kind, _) <-
433
           kcHsTyVarBndrs (famDeclHasCusk decl) ktvs $ \_ _ ->
Jan Stolarek's avatar
Jan Stolarek committed
434 435 436 437 438 439 440 441
           do { res_k <- case resultSig of
                      KindSig ki                        -> tcLHsKind ki
                      TyVarSig (L _ (KindedTyVar _ ki)) -> tcLHsKind ki
                      _ -- open type families have * return kind by default
                        | famDeclHasCusk decl      -> return liftedTypeKind
                        -- closed type families have their return kind inferred
                        -- by default
                        | otherwise                -> newMetaKindVar
442
              ; return (res_k, ()) }
443
       ; fam_kind <- zonkTcType fam_kind
444
       ; return [ (name, AThing fam_kind) ] }
445

446
----------------
447
kcSynDecls :: [SCC (LTyClDecl Name)]
448 449
           -> TcM TcLclEnv -- Kind bindings
kcSynDecls [] = getLclEnv
450
kcSynDecls (group : groups)
451 452 453
  = do  { (n,k) <- kcSynDecl1 group
        ; lcl_env <- tcExtendKindEnv [(n,k)] (kcSynDecls groups)
        ; return lcl_env }
dreixel's avatar
dreixel committed
454 455

kcSynDecl1 :: SCC (LTyClDecl Name)
456
           -> TcM (Name,TcKind) -- Kind bindings
dreixel's avatar
dreixel committed
457 458
kcSynDecl1 (AcyclicSCC (L _ decl)) = kcSynDecl decl
kcSynDecl1 (CyclicSCC decls)       = do { recSynErr decls; failM }
459 460
                                     -- Fail here to avoid error cascade
                                     -- of out-of-scope tycons
dreixel's avatar
dreixel committed
461

462
kcSynDecl :: TyClDecl Name -> TcM (Name, TcKind)
463
kcSynDecl decl@(SynDecl { tcdTyVars = hs_tvs, tcdLName = L _ name
464
                        , tcdRhs = rhs })
465
  -- Returns a possibly-unzonked kind
dreixel's avatar
dreixel committed
466
  = tcAddDeclCtxt decl $
467
    do { (syn_kind, _) <-
468
           kcHsTyVarBndrs (hsDeclHasCusk decl) hs_tvs $ \_ _ ->
469 470 471 472
           do { traceTc "kcd1" (ppr name <+> brackets (ppr hs_tvs))
              ; (_, rhs_kind) <- tcLHsType rhs
              ; traceTc "kcd2" (ppr name)
              ; return (rhs_kind, ()) }
473
       ; return (name, syn_kind) }
474
kcSynDecl decl = pprPanic "kcSynDecl" (ppr decl)
475

476
------------------------------------------------------------------------
477
kcLTyClDecl :: LTyClDecl Name -> TcM ()
478
  -- See Note [Kind checking for type and class decls]
479 480 481
kcLTyClDecl (L loc decl)
  = setSrcSpan loc $ tcAddDeclCtxt decl $ kcTyClDecl decl

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

488 489
kcTyClDecl (DataDecl { tcdLName = L _ name, tcdTyVars = hs_tvs, tcdDataDefn = defn })
  | HsDataDefn { dd_cons = cons, dd_kindSig = Just _ } <- defn
490
  = mapM_ (wrapLocM kcConDecl) cons
491 492 493 494 495 496
    -- 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
497

498 499
  | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
  = kcTyClTyVars name hs_tvs $
500
    do  { _ <- tcHsContext ctxt
501
        ; mapM_ (wrapLocM kcConDecl) cons }
502

503
kcTyClDecl decl@(SynDecl {}) = pprPanic "kcTyClDecl" (ppr decl)
504 505

kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs
506 507
                       , tcdCtxt = ctxt, tcdSigs = sigs })
  = kcTyClTyVars name hs_tvs $
508
    do  { _ <- tcHsContext ctxt
509
        ; mapM_ (wrapLocM kc_sig)     sigs }
dreixel's avatar
dreixel committed
510
  where
Alan Zimmerman's avatar
Alan Zimmerman committed
511
    kc_sig (ClassOpSig _ nms op_ty) = kcHsSigType nms op_ty
512
    kc_sig _                        = return ()
513

514 515
kcTyClDecl (FamDecl (FamilyDecl { fdLName  = L _ fam_tc_name
                                , fdTyVars = hs_tvs
516 517 518 519 520 521 522 523 524 525 526
                                , 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) ->
        do { tc_kind <- kcLookupKind fam_tc_name
           ; let fam_tc_shape = ( fam_tc_name
                                , length $ hsQTvExplicit hs_tvs
                                , tc_kind )
           ; mapM_ (kcTyFamInstEqn fam_tc_shape) eqns }
      _ -> return ()
dreixel's avatar
dreixel committed
527 528

-------------------
529
kcConDecl :: ConDecl Name -> TcM ()
Alan Zimmerman's avatar
Alan Zimmerman committed
530 531 532
kcConDecl (ConDeclH98 { con_name = name, con_qvars = ex_tvs
                      , con_cxt = ex_ctxt, con_details = details })
  = addErrCtxt (dataConCtxtName [name]) $
533 534
         -- 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
535
         -- into scope.
Alan Zimmerman's avatar
Alan Zimmerman committed
536
    do { _ <- kcHsTyVarBndrs False ((fromMaybe (HsQTvs mempty []) ex_tvs)) $
537
              \ _ _ ->
Alan Zimmerman's avatar
Alan Zimmerman committed
538
              do { _ <- tcHsContext (fromMaybe (noLoc []) ex_ctxt)
539 540
                 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details)
                 ; return (panic "kcConDecl", ()) }
541 542
              -- We don't need to check the telescope here, because that's
              -- done in tcConDecl
543
       ; return () }
544

Alan Zimmerman's avatar
Alan Zimmerman committed
545 546 547 548 549 550 551
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
552
{-
553 554
Note [Recursion and promoting data constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
555 556 557 558 559 560 561 562 563 564 565 566 567 568
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:
  T -> AThing <some initial kind>
  K -> ARecDataCon

ANothing is only used for DataCons, and only used during type checking
in tcTyClGroup.

569

Austin Seipp's avatar
Austin Seipp committed
570 571
************************************************************************
*                                                                      *
572
\subsection{Type checking}
Austin Seipp's avatar
Austin Seipp committed
573 574
*                                                                      *
************************************************************************
575

dreixel's avatar
dreixel committed
576 577 578 579
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,
580
we discarded the kind-checked types (eg RHSs of data type decls);
dreixel's avatar
dreixel committed
581 582 583 584 585 586 587
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
588
    to be given kind arguments.
dreixel's avatar
dreixel committed
589 590 591 592 593 594 595

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

dreixel's avatar
dreixel committed
597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615
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

  *Global* env with T -> ATyCon (the (not yet built) TyCon for T)
  *Local*  env with T -> AThing (polymorphic kind of T)

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

620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642
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
declarations]): in the *local* environment, with AThing. But we still
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.

643 644 645 646 647 648
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
649
-}
dreixel's avatar
dreixel committed
650

651
tcTyClDecl :: RecTyInfo -> LTyClDecl Name -> TcM TyCon
652
tcTyClDecl rec_info (L loc decl)
653
  | Just thing <- wiredInNameTyThing_maybe (tcdName decl)
654 655 656
  = case thing of -- See Note [Declarations for wired-in things]
      ATyCon tc -> return tc
      _ -> pprPanic "tcTyClDecl" (ppr thing)
657 658

  | otherwise
659
  = setSrcSpan loc $ tcAddDeclCtxt decl $
660
    do { traceTc "tcTyAndCl-x" (ppr decl)
661
       ; tcTyClDecl1 Nothing rec_info decl }
662

663
  -- "type family" declarations
664
tcTyClDecl1 :: Maybe Class -> RecTyInfo -> TyClDecl Name -> TcM TyCon
665
tcTyClDecl1 parent _rec_info (FamDecl { tcdFam = fd })
666
  = tcFamDecl1 parent fd
667

668
  -- "type" synonym declaration
669
tcTyClDecl1 _parent rec_info
670
            (SynDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdRhs = rhs })
671
  = ASSERT( isNothing _parent )
672 673
    tcTyClTyVars tc_name tvs $ \ kvs' tvs' full_kind res_kind ->
    tcTySynRhs rec_info tc_name (kvs' ++ tvs') full_kind res_kind rhs
674

675
  -- "data/newtype" declaration
676
tcTyClDecl1 _parent rec_info
677
            (DataDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdDataDefn = defn })
678
  = ASSERT( isNothing _parent )
679 680
    tcTyClTyVars tc_name tvs $ \ kvs' tvs' tycon_kind res_kind ->
    tcDataDefn rec_info tc_name (kvs' ++ tvs') tycon_kind res_kind defn
681

682
tcTyClDecl1 _parent rec_info
dreixel's avatar
dreixel committed
683
            (ClassDecl { tcdLName = L _ class_name, tcdTyVars = tvs
684
            , tcdCtxt = ctxt, tcdMeths = meths
685
            , tcdFDs = fundeps, tcdSigs = sigs
686
            , tcdATs = ats, tcdATDefs = at_defs })
687
  = ASSERT( isNothing _parent )
688
    do { clas <- fixM $ \ clas ->
689 690
            tcTyClTyVars class_name tvs $ \ kvs' tvs' full_kind res_kind ->
            do { MASSERT( isConstraintKind res_kind )
691 692 693
                 -- 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
694 695
               ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr kvs' $$
                                          ppr tvs' $$ ppr full_kind)
696 697 698
               ; 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
699

700
               ; ctxt' <- solveEqualities $ tcHsContext ctxt
701
               ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'
702 703
                       -- Squeeze out any kind unification variables
               ; fds'  <- mapM (addLocM tc_fundep) fundeps
704
               ; sig_stuff <- tcClassSigs class_name sigs meths
705
               ; at_stuff <- tcClassATs class_name clas ats at_defs
706
               ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
707
               ; clas <- buildClass
708 709
                            class_name (kvs' ++ tvs') roles ctxt' full_kind
                            fds' at_stuff
710
                            sig_stuff mindef tc_isrec
711 712
               ; traceTc "tcClassDecl" (ppr fundeps $$ ppr (kvs' ++ tvs') $$
                                        ppr fds')
713 714 715
               ; return clas }

         ; return (classTyCon clas) }
716
  where
717 718
    tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM (tcLookupTyVar . unLoc) tvs1 ;
                                ; tvs2' <- mapM (tcLookupTyVar . unLoc) tvs2 ;
719
                                ; return (tvs1', tvs2') }
Jan Stolarek's avatar
Jan Stolarek committed
720

721
tcFamDecl1 :: Maybe Class -> FamilyDecl Name -> TcM TyCon
722 723 724 725
tcFamDecl1 parent (FamilyDecl { fdInfo = OpenTypeFamily, fdLName = L _ tc_name
                              , fdTyVars = tvs, fdResultSig = L _ sig
                              , fdInjectivityAnn = inj })
  = tcTyClTyVars tc_name tvs $ \ kvs' tvs' full_kind _res_kind -> do
726
  { traceTc "open type family:" (ppr tc_name)
727
  ; checkFamFlag tc_name
728 729 730 731 732
  ; let all_tvs = kvs' ++ tvs'
  ; inj' <- tcInjectivity all_tvs inj
  ; let tycon = mkFamilyTyCon tc_name full_kind all_tvs
                               (resultVariableName sig) OpenSynFamilyTyCon
                               parent inj'
733
  ; return tycon }
734 735

tcFamDecl1 parent
736
            (FamilyDecl { fdInfo = ClosedTypeFamily mb_eqns
Jan Stolarek's avatar
Jan Stolarek committed
737 738
                        , fdLName = L _ tc_name, fdTyVars = tvs
                        , fdResultSig = L _ sig, fdInjectivityAnn = inj })
739 740
-- Closed type families are a little tricky, because they contain the definition
-- of both the type family and the equations for a CoAxiom.
Jan Stolarek's avatar
Jan Stolarek committed
741 742 743
  = do { traceTc "Closed type family:" (ppr tc_name)
         -- the variables in the header scope only over the injectivity
         -- declaration but this is not involved here
744 745 746 747 748
       ; (tvs', inj', kind) <- tcTyClTyVars tc_name tvs
                               $ \ kvs' tvs' full_kind _res_kind ->
                               do { let all_tvs = kvs' ++ tvs'
                                  ; inj' <- tcInjectivity all_tvs inj
                                  ; return (all_tvs, inj', full_kind) }
749 750 751

       ; checkFamFlag tc_name -- make sure we have -XTypeFamilies

752 753 754
         -- 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
755 756 757 758 759
           Nothing   ->
               return $ mkFamilyTyCon tc_name kind tvs'
                                      (resultVariableName sig)
                                      AbstractClosedSynFamilyTyCon parent
                                      inj'
760 761
           Just eqns -> do {

762
         -- Process the equations, creating CoAxBranches
763
       ; let fam_tc_shape = (tc_name, length $ hsQTvExplicit tvs, kind)
Jan Stolarek's avatar
Jan Stolarek committed
764

765
       ; branches <- mapM (tcTyFamInstEqn fam_tc_shape Nothing) eqns
Jan Stolarek's avatar
Jan Stolarek committed
766 767 768 769 770
         -- 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
771

Jan Stolarek's avatar
Jan Stolarek committed
772
         -- Create a CoAxiom, with the correct src location. It is Vitally
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
773 774 775 776 777 778
         -- 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
779
       ; loc <- getSrcSpanM
780
       ; co_ax_name <- newFamInstAxiomName loc tc_name []
781

782
       ; let mb_co_ax
Jan Stolarek's avatar
Jan Stolarek committed
783 784 785
              | null eqns = Nothing   -- mkBranchedCoAxiom fails on empty list
              | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches)

786 787
             fam_tc = mkFamilyTyCon tc_name kind tvs' (resultVariableName sig)
                      (ClosedSynFamilyTyCon mb_co_ax) parent inj'
Jan Stolarek's avatar
Jan Stolarek committed
788

789
       ; return fam_tc } }
790 791

-- We check for instance validity later, when doing validity checking for
Jan Stolarek's avatar
Jan Stolarek committed
792
-- the tycon. Exception: checking equations overlap done by dropDominatedAxioms
793