TcTyClsDecls.hs 102 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 #-}
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, tcAddDataFamInstCtxt,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
19
        wrongKindOfFamily, dataConCtxt, badDataConTyCon
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
import TcBinds( tcRecSelBinds )
32 33 34 35 36
import TcTyDecls
import TcClassDcl
import TcHsType
import TcMType
import TcType
37
import TysWiredIn( unitTy )
38
import FamInst
Jan Stolarek's avatar
Jan Stolarek committed
39 40
import FamInstEnv
import Coercion( ltRole )
41
import Type
42
import TypeRep   -- 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 MkCore           ( rEC_SEL_ERROR_ID )
50
import IdInfo
51
import Var
52
import VarEnv
53
import VarSet
54
import Module
55
import Name
56
import NameSet
57
import NameEnv
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           ( mkBuiltinUnique )
68
import BasicTypes
69

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

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

dreixel's avatar
dreixel committed
81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98
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
forall (k::BOX). k -> k. Since it does not depend on anything else, it can be
kind-checked by itself, hence getting the most general kind. We then kind check
X, which works fine because we then know the polymorphic kind of Id, and simply
instantiate k to *.

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

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

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

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

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

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

                 -- Kind and type check declarations for this group
157
             concatMapM (tcTyClDecl rec_flags) decls }
dreixel's avatar
dreixel committed
158

159
           -- Step 3: Perform the validity check
dreixel's avatar
dreixel committed
160 161 162
           -- 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
163
       ; tcExtendGlobalEnv tyclss $ do
dreixel's avatar
dreixel committed
164
       { traceTc "Starting validity check" (ppr tyclss)
165
       ; mapM_ (recoverM (return ()) . checkValidTyCl) tyclss
166
           -- We recover, which allows us to report multiple validity errors
167 168
       ; mapM_ (recoverM (return ()) . checkValidRoleAnnots role_annots) tyclss
           -- See Note [Check role annotations in a second pass]
dreixel's avatar
dreixel committed
169 170 171 172

           -- Step 4: Add the implicit things;
           -- we want them in the environment because
           -- they may be mentioned in interface files
173 174 175 176 177
       ; tcExtendGlobalValEnv (mkDefaultMethodIds tyclss) $
         tcAddImplicits tyclss } }

tcAddImplicits :: [TyThing] -> TcM TcGblEnv
tcAddImplicits tyclss
178
 = tcExtendGlobalEnvImplicit implicit_things $
179 180 181 182
   tcRecSelBinds rec_sel_binds
 where
   implicit_things = concatMap implicitTyThings tyclss
   rec_sel_binds   = mkRecSelBinds tyclss
dreixel's avatar
dreixel committed
183

184
zipRecTyClss :: [(Name, Kind)]
185 186 187 188
             -> [TyThing]           -- Knot-tied
             -> [(Name,TyThing)]
-- Build a name-TyThing mapping for the things bound by decls
-- being careful not to look at the [TyThing]
batterseapower's avatar
batterseapower committed
189
-- The TyThings in the result list must have a visible ATyCon,
190
-- because typechecking types (in, say, tcTyClDecl) looks at this outer constructor
191 192
zipRecTyClss kind_pairs rec_things
  = [ (name, ATyCon (get name)) | (name, _kind) <- kind_pairs ]
193
  where
194 195 196
    rec_type_env :: TypeEnv
    rec_type_env = mkTypeEnv rec_things

dreixel's avatar
dreixel committed
197 198 199
    get name = case lookupTypeEnv rec_type_env name of
                 Just (ATyCon 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').
Austin Seipp's avatar
Austin Seipp committed
261
-}
262

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

271 272
          -- Kind checking;
          --    1. Bind kind variables for non-synonyms
dreixel's avatar
dreixel committed
273 274
          --    2. Kind-check synonyms, and bind kinds of those synonyms
          --    3. Kind-check non-synonyms
275
          --    4. Generalise the inferred kinds
dreixel's avatar
dreixel committed
276 277
          -- See Note [Kind checking for type and class decls]

278
          -- Step 1: Bind kind variables for non-synonyms
dreixel's avatar
dreixel committed
279
        ; let (syn_decls, non_syn_decls) = partition (isSynDecl . unLoc) decls
280
        ; initial_kinds <- getInitialKinds non_syn_decls
281
        ; traceTc "kcTyClGroup: initial kinds" (ppr initial_kinds)
282 283

        -- Step 2: Set initial envt, kind-check the synonyms
284
        ; lcl_env <- tcExtendKindEnv2 initial_kinds $
285
                     kcSynDecls (calcSynCycles syn_decls)
286 287 288 289

        -- Step 3: Set extended envt, kind-check the non-synonyms
        ; setLclEnv lcl_env $
          mapM_ kcLTyClDecl non_syn_decls
dreixel's avatar
dreixel committed
290

291 292
             -- Step 4: generalisation
             -- Kind checking done for this group
dreixel's avatar
dreixel committed
293
             -- Now we have to kind generalize the flexis
294
        ; res <- concatMapM (generaliseTCD (tcl_env lcl_env)) decls
295 296

        ; traceTc "kcTyClGroup result" (ppr res)
297
        ; return res }
298

299
  where
300
    generalise :: TcTypeEnv -> Name -> TcM (Name, Kind)
301
    -- For polymorphic things this is a no-op
302
    generalise kind_env name
303
      = do { let kc_kind = case lookupNameEnv kind_env name of
304 305
                               Just (AThing k) -> k
                               _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env)
306
           ; kvs <- kindGeneralize (tyVarsOfType kc_kind)
307 308 309
           ; kc_kind' <- zonkTcKind kc_kind    -- Make sure kc_kind' has the final,
                                               -- skolemised kind variables
           ; traceTc "Generalise kind" (vcat [ ppr name, ppr kc_kind, ppr kvs, ppr kc_kind' ])
dreixel's avatar
dreixel committed
310 311
           ; return (name, mkForAllTys kvs kc_kind') }

312 313
    generaliseTCD :: TcTypeEnv -> LTyClDecl Name -> TcM [(Name, Kind)]
    generaliseTCD kind_env (L _ decl)
314 315
      | ClassDecl { tcdLName = (L _ name), tcdATs = ats } <- decl
      = do { first <- generalise kind_env name
316 317 318 319 320 321 322 323
           ; rest <- mapM ((generaliseFamDecl kind_env) . unLoc) ats
           ; return (first : rest) }

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

      | otherwise
324
      = do { res <- generalise kind_env (tcdName decl)
325 326 327
           ; return [res] }

    generaliseFamDecl :: TcTypeEnv -> FamilyDecl Name -> TcM (Name, Kind)
328 329
    generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name })
      = generalise kind_env name
330

331 332 333 334 335 336 337 338 339 340 341 342
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)

343
getInitialKinds :: [LTyClDecl Name] -> TcM [(Name, TcTyThing)]
344
getInitialKinds decls
345
  = tcExtendKindEnv2 (mk_thing_env decls) $
346 347
    do { pairss <- mapM (addLocM getInitialKind) decls
       ; return (concat pairss) }
348

349
getInitialKind :: TyClDecl Name -> TcM [(Name, TcTyThing)]
dreixel's avatar
dreixel committed
350 351 352 353 354 355
-- 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 = ...
356
--      return (T, kv1 -> kv2 -> kv3)
dreixel's avatar
dreixel committed
357
--
358 359 360 361 362 363
-- 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]
364
--
365
-- No family instances are passed to getInitialKinds
dreixel's avatar
dreixel committed
366

367
getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
368
  = do { (cl_kind, inner_prs) <-
369
           kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $
370 371 372
           do { inner_prs <- getFamDeclInitialKinds ats
              ; return (constraintKind, inner_prs) }
       ; let main_pr = (name, AThing cl_kind)
373
       ; return (main_pr : inner_prs) }
374

375
getInitialKind decl@(DataDecl { tcdLName = L _ name
376 377 378 379 380 381
                              , tcdTyVars = ktvs
                              , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
                                                         , dd_cons = cons' } })
  = let cons = cons' -- AZ list monad coming
    in
     do { (decl_kind, _) <-
382
           kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $
383 384 385
           do { res_k <- case m_sig of
                           Just ksig -> tcLHsKind ksig
                           Nothing   -> return liftedTypeKind
386
              ; return (res_k, ()) }
387
       ; let main_pr = (name, AThing decl_kind)
388 389
             inner_prs = [ (unLoc con, APromotionErr RecDataConPE)
                         | L _ con' <- cons, con <- con_names con' ]
390
       ; return (main_pr : inner_prs) }
391

Jan Stolarek's avatar
Jan Stolarek committed
392
getInitialKind (FamDecl { tcdFam = decl })
393
  = getFamDeclInitialKind decl
394

Jan Stolarek's avatar
Jan Stolarek committed
395
getInitialKind decl@(SynDecl {})
396 397 398
  = pprPanic "getInitialKind" (ppr decl)

---------------------------------
399 400
getFamDeclInitialKinds :: [LFamilyDecl Name] -> TcM [(Name, TcTyThing)]
getFamDeclInitialKinds decls
401 402
  = tcExtendKindEnv2 [ (n, APromotionErr TyConPE)
                     | L _ (FamilyDecl { fdLName = L _ n }) <- decls] $
403
    concatMapM (addLocM getFamDeclInitialKind) decls
404

405
getFamDeclInitialKind :: FamilyDecl Name
406
                      -> TcM [(Name, TcTyThing)]
Jan Stolarek's avatar
Jan Stolarek committed
407 408 409
getFamDeclInitialKind decl@(FamilyDecl { fdLName     = L _ name
                                       , fdTyVars    = ktvs
                                       , fdResultSig = L _ resultSig })
410
  = do { (fam_kind, _) <-
411
           kcHsTyVarBndrs (famDeclHasCusk decl) ktvs $
Jan Stolarek's avatar
Jan Stolarek committed
412 413 414 415 416 417 418 419
           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
420 421
              ; return (res_k, ()) }
       ; return [ (name, AThing fam_kind) ] }
422

423
----------------
424
kcSynDecls :: [SCC (LTyClDecl Name)]
425 426
           -> TcM TcLclEnv -- Kind bindings
kcSynDecls [] = getLclEnv
427
kcSynDecls (group : groups)
428 429 430
  = do  { (n,k) <- kcSynDecl1 group
        ; lcl_env <- tcExtendKindEnv [(n,k)] (kcSynDecls groups)
        ; return lcl_env }
dreixel's avatar
dreixel committed
431 432

kcSynDecl1 :: SCC (LTyClDecl Name)
433
           -> TcM (Name,TcKind) -- Kind bindings
dreixel's avatar
dreixel committed
434 435
kcSynDecl1 (AcyclicSCC (L _ decl)) = kcSynDecl decl
kcSynDecl1 (CyclicSCC decls)       = do { recSynErr decls; failM }
436 437
                                     -- Fail here to avoid error cascade
                                     -- of out-of-scope tycons
dreixel's avatar
dreixel committed
438

439
kcSynDecl :: TyClDecl Name -> TcM (Name, TcKind)
440
kcSynDecl decl@(SynDecl { tcdTyVars = hs_tvs, tcdLName = L _ name
441
                        , tcdRhs = rhs })
442
  -- Returns a possibly-unzonked kind
dreixel's avatar
dreixel committed
443
  = tcAddDeclCtxt decl $
444
    do { (syn_kind, _) <-
445
           kcHsTyVarBndrs (hsDeclHasCusk decl) hs_tvs $
446 447 448 449
           do { traceTc "kcd1" (ppr name <+> brackets (ppr hs_tvs))
              ; (_, rhs_kind) <- tcLHsType rhs
              ; traceTc "kcd2" (ppr name)
              ; return (rhs_kind, ()) }
450
       ; return (name, syn_kind) }
451
kcSynDecl decl = pprPanic "kcSynDecl" (ppr decl)
452

453
------------------------------------------------------------------------
454
kcLTyClDecl :: LTyClDecl Name -> TcM ()
455
  -- See Note [Kind checking for type and class decls]
456 457 458
kcLTyClDecl (L loc decl)
  = setSrcSpan loc $ tcAddDeclCtxt decl $ kcTyClDecl decl

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

465 466
kcTyClDecl (DataDecl { tcdLName = L _ name, tcdTyVars = hs_tvs, tcdDataDefn = defn })
  | HsDataDefn { dd_cons = cons, dd_kindSig = Just _ } <- defn
467
  = mapM_ (wrapLocM kcConDecl) cons
468 469 470 471 472 473
    -- 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
474

475 476
  | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
  = kcTyClTyVars name hs_tvs $
477
    do  { _ <- tcHsContext ctxt
478
        ; mapM_ (wrapLocM kcConDecl) cons }
479

480
kcTyClDecl decl@(SynDecl {}) = pprPanic "kcTyClDecl" (ppr decl)
481 482

kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs
483 484
                       , tcdCtxt = ctxt, tcdSigs = sigs })
  = kcTyClTyVars name hs_tvs $
485 486
    do  { _ <- tcHsContext ctxt
        ; mapM_ (wrapLocM kc_sig)     sigs }
dreixel's avatar
dreixel committed
487
  where
thomasw's avatar
thomasw committed
488
    kc_sig (TypeSig _ op_ty _)  = discardResult (tcHsLiftedType op_ty)
489
    kc_sig (GenericSig _ op_ty) = discardResult (tcHsLiftedType op_ty)
dreixel's avatar
dreixel committed
490
    kc_sig _                    = return ()
491

492 493
-- closed type families look at their equations, but other families don't
-- do anything here
494 495
kcTyClDecl (FamDecl (FamilyDecl { fdLName  = L _ fam_tc_name
                                , fdTyVars = hs_tvs
496
                                , fdInfo   = ClosedTypeFamily (Just eqns) }))
497 498 499
  = do { tc_kind <- kcLookupKind fam_tc_name
       ; let fam_tc_shape = ( fam_tc_name, length (hsQTvBndrs hs_tvs), tc_kind)
       ; mapM_ (kcTyFamInstEqn fam_tc_shape) eqns }
500
kcTyClDecl (FamDecl {})    = return ()
dreixel's avatar
dreixel committed
501 502

-------------------
503
kcConDecl :: ConDecl Name -> TcM ()
504
kcConDecl (ConDecl { con_names = names, con_qvars = ex_tvs
505 506
                   , con_cxt = ex_ctxt, con_details = details
                   , con_res = res })
507
  = addErrCtxt (dataConCtxtName names) $
508 509 510 511
         -- 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
         -- into scope!
    do { _ <- kcHsTyVarBndrs False ex_tvs $
512 513
              do { _ <- tcHsContext ex_ctxt
                 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details)
514
                 ; _ <- tcConRes res
515
                 ; return (panic "kcConDecl", ()) }
516
       ; return () }
517

Austin Seipp's avatar
Austin Seipp committed
518
{-
519 520
Note [Recursion and promoting data constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
521 522 523 524 525 526 527 528 529 530 531 532 533 534
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.

535

Austin Seipp's avatar
Austin Seipp committed
536 537
************************************************************************
*                                                                      *
538
\subsection{Type checking}
Austin Seipp's avatar
Austin Seipp committed
539 540
*                                                                      *
************************************************************************
541

dreixel's avatar
dreixel committed
542 543 544 545
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,
546
we discarded the kind-checked types (eg RHSs of data type decls);
dreixel's avatar
dreixel committed
547 548 549 550 551 552 553
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
554
    to be given kind arguments.
dreixel's avatar
dreixel committed
555 556 557 558 559 560 561

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

dreixel's avatar
dreixel committed
563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581
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
582
This fancy footwork (with two bindings for T) is only necessary for the
dreixel's avatar
dreixel committed
583 584
TyCons or Classes of this recursive group.  Earlier, finished groups,
live in the global env only.
585 586 587 588 589 590 591

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
592
-}
dreixel's avatar
dreixel committed
593

594 595
tcTyClDecl :: RecTyInfo -> LTyClDecl Name -> TcM [TyThing]
tcTyClDecl rec_info (L loc decl)
596 597 598 599
  | Just thing <- wiredInNameTyThing_maybe (tcdName decl)
  = return [thing]  -- See Note [Declarations for wired-in things]

  | otherwise
600
  = setSrcSpan loc $ tcAddDeclCtxt decl $
601 602
    do { traceTc "tcTyAndCl-x" (ppr decl)
       ; tcTyClDecl1 NoParentTyCon rec_info decl }
603

604
  -- "type family" declarations
605 606
tcTyClDecl1 :: TyConParent -> RecTyInfo -> TyClDecl Name -> TcM [TyThing]
tcTyClDecl1 parent _rec_info (FamDecl { tcdFam = fd })
607
  = tcFamDecl1 parent fd
608

609
  -- "type" synonym declaration
610
tcTyClDecl1 _parent rec_info
611 612
            (SynDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdRhs = rhs })
  = ASSERT( isNoParent _parent )
613
    tcTyClTyVars tc_name tvs $ \ tvs' kind ->
614
    tcTySynRhs rec_info tc_name tvs' kind rhs
615

616
  -- "data/newtype" declaration
617
tcTyClDecl1 _parent rec_info
618
            (DataDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdDataDefn = defn })
619
  = ASSERT( isNoParent _parent )
620
    tcTyClTyVars tc_name tvs $ \ tvs' kind ->
621
    tcDataDefn rec_info tc_name tvs' kind defn
622

623
tcTyClDecl1 _parent rec_info
dreixel's avatar
dreixel committed
624
            (ClassDecl { tcdLName = L _ class_name, tcdTyVars = tvs
625
            , tcdCtxt = ctxt, tcdMeths = meths
626
            , tcdFDs = fundeps, tcdSigs = sigs
627
            , tcdATs = ats, tcdATDefs = at_defs })
628
  = ASSERT( isNoParent _parent )
629
    do { (clas, tvs', gen_dm_env) <- fixM $ \ ~(clas,_,_) ->
630
            tcTyClTyVars class_name tvs $ \ tvs' kind ->
631
            do { MASSERT( isConstraintKind kind )
632 633 634
                 -- 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
Jan Stolarek's avatar
Jan Stolarek committed
635
               ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr tvs' $$ ppr kind)
636 637 638
               ; 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
639

640
               ; ctxt' <- tcHsContext ctxt
641
               ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'
642 643 644 645
                       -- Squeeze out any kind unification variables
               ; fds'  <- mapM (addLocM tc_fundep) fundeps
               ; (sig_stuff, gen_dm_env) <- tcClassSigs class_name sigs meths
               ; at_stuff <- tcClassATs class_name (AssocFamilyTyCon clas) ats at_defs
646
               ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
647
               ; clas <- buildClass
648
                            class_name tvs' roles ctxt' fds' at_stuff
649
                            sig_stuff mindef tc_isrec
650 651 652
               ; traceTc "tcClassDecl" (ppr fundeps $$ ppr tvs' $$ ppr fds')
               ; return (clas, tvs', gen_dm_env) }

653
       ; let { gen_dm_ids = [ AnId (mkExportedLocalId VanillaId gen_dm_name gen_dm_ty)
654
                            | (sel_id, GenDefMeth gen_dm_name) <- classOpItems clas
655 656 657 658 659 660
                            , let gen_dm_tau = expectJust "tcTyClDecl1" $
                                               lookupNameEnv gen_dm_env (idName sel_id)
                            , let gen_dm_ty = mkSigmaTy tvs'
                                                      [mkClassPred clas (mkTyVarTys tvs')]
                                                      gen_dm_tau
                            ]
661 662 663 664 665
             ; class_ats = map ATyCon (classATs clas) }

       ; return (ATyCon (classTyCon clas) : gen_dm_ids ++ class_ats ) }
         -- NB: Order is important due to the call to `mkGlobalThings' when
         --     tying the the type and class declaration type checking knot.
666
  where
Jan Stolarek's avatar
Jan Stolarek committed
667 668
    tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM tcFdTyVar tvs1
                                ; tvs2' <- mapM tcFdTyVar tvs2
669
                                ; return (tvs1', tvs2') }
Jan Stolarek's avatar
Jan Stolarek committed
670 671 672 673 674 675 676 677 678 679 680 681 682

tcFdTyVar :: Located Name -> TcM TcTyVar
-- Look up a type/kind variable in a functional dependency
-- or injectivity annotation.  In the case of kind variables,
-- the environment contains a binding of the kind var to a
-- a SigTv unification variables, which has now fixed.
-- So we must zonk to get the real thing.  Ugh!
tcFdTyVar (L _ name)
  = do { tv <- tcLookupTyVar name
       ; ty <- zonkTyVarOcc emptyZonkEnv tv
       ; case getTyVar_maybe ty of
           Just tv' -> return tv'
           Nothing  -> pprPanic "tcFdTyVar" (ppr name $$ ppr tv $$ ppr ty) }
683

684
tcFamDecl1 :: TyConParent -> FamilyDecl Name -> TcM [TyThing]
Jan Stolarek's avatar
Jan Stolarek committed
685 686 687
tcFamDecl1 parent (FamilyDecl { fdInfo = OpenTypeFamily, fdLName = L _ tc_name
                              , fdTyVars = tvs, fdResultSig = L _ sig
                              , fdInjectivityAnn = inj })
688
  = tcTyClTyVars tc_name tvs $ \ tvs' kind -> do
689
  { traceTc "open type family:" (ppr tc_name)
690
  ; checkFamFlag tc_name
Jan Stolarek's avatar
Jan Stolarek committed
691 692 693
  ; inj' <- tcInjectivity tvs' inj
  ; let tycon = buildFamilyTyCon tc_name tvs' (resultVariableName sig)
                                 OpenSynFamilyTyCon kind parent inj'
694 695 696
  ; return [ATyCon tycon] }

tcFamDecl1 parent
697
            (FamilyDecl { fdInfo = ClosedTypeFamily mb_eqns
Jan Stolarek's avatar
Jan Stolarek committed
698 699
                        , fdLName = L _ tc_name, fdTyVars = tvs
                        , fdResultSig = L _ sig, fdInjectivityAnn = inj })
700 701
-- 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
702 703 704 705 706 707
  = 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
       ; (tvs', inj', kind) <- tcTyClTyVars tc_name tvs $ \ tvs' kind ->
                               do { inj' <- tcInjectivity tvs' inj
                                  ; return (tvs', inj', kind) }
708 709 710

       ; checkFamFlag tc_name -- make sure we have -XTypeFamilies

711 712 713
         -- 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
Jan Stolarek's avatar
Jan Stolarek committed
714 715 716 717
           Nothing   ->
               return [ATyCon $ buildFamilyTyCon tc_name tvs' Nothing
                                     AbstractClosedSynFamilyTyCon kind parent
                                     NotInjective ]
718 719
           Just eqns -> do {

720 721
         -- Process the equations, creating CoAxBranches
       ; tc_kind <- kcLookupKind tc_name
Jan Stolarek's avatar
Jan Stolarek committed
722 723
       ; let fam_tc_shape = (tc_name, length (hsQTvBndrs tvs), tc_kind)

724
       ; branches <- mapM (tcTyFamInstEqn fam_tc_shape) eqns
Jan Stolarek's avatar
Jan Stolarek committed
725 726 727 728 729
         -- 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
730

Jan Stolarek's avatar
Jan Stolarek committed
731
         -- Create a CoAxiom, with the correct src location. It is Vitally
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
732 733 734 735 736 737
         -- 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
738
       ; loc <- getSrcSpanM
739
       ; co_ax_name <- newFamInstAxiomName loc tc_name []
740

741
       ; let mb_co_ax
Jan Stolarek's avatar
Jan Stolarek committed
742 743 744 745 746 747 748
              | null eqns = Nothing   -- mkBranchedCoAxiom fails on empty list
              | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches)

             fam_tc = buildFamilyTyCon tc_name tvs' (resultVariableName sig)
                      (ClosedSynFamilyTyCon mb_co_ax) kind parent inj'

       ; return $ ATyCon fam_tc : maybeToList (fmap ACoAxiom mb_co_ax) } }
749 750

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

tcFamDecl1 parent
           (FamilyDecl {fdInfo = DataFamily, fdLName = L _ tc_name, fdTyVars = tvs})
755 756 757 758 759
  = tcTyClTyVars tc_name tvs $ \ tvs' kind -> do
  { traceTc "data family:" (ppr tc_name)
  ; checkFamFlag tc_name
  ; extra_tvs <- tcDataKindSig kind
  ; let final_tvs = tvs' ++ extra_tvs    -- we may not need these
760 761
        roles     = map (const Nominal) final_tvs
        tycon = buildAlgTyCon tc_name final_tvs roles Nothing []
762
                              DataFamilyTyCon Recursive
763 764 765
                              False   -- Not promotable to the kind level
                              True    -- GADT syntax
                              parent
766 767
  ; return [ATyCon tycon] }

Jan Stolarek's avatar
Jan Stolarek committed
768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804
-- | Maybe return a list of Bools that say whether a type family was declared
-- injective in the corresponding type arguments. Length of the list is equal to
-- the number of arguments (including implicit kind arguments). True on position
-- N means that a function is injective in its Nth argument. False means it is
-- not.
tcInjectivity :: [TyVar] -> Maybe (LInjectivityAnn Name)
              -> TcM Injectivity
tcInjectivity _ Nothing
  = return NotInjective

  -- User provided an injectivity annotation, so for each tyvar argument we
  -- check whether a type family was declared injective in that argument. We
  -- return a list of Bools, where True means that corresponding type variable
  -- was mentioned in lInjNames (type family is injective in that argument) and
  -- False means that it was not mentioned in lInjNames (type family is not
  -- injective in that type variable). We also extend injectivity information to
  -- kind variables, so if a user declares:
  --
  --   type family F (a :: k1) (b :: k2) = (r :: k3) | r -> a
  --
  -- then we mark both `a` and `k1` as injective.
  -- NB: the return kind is considered to be *input* argument to a type family.
  -- Since injectivity allows to infer input arguments from the result in theory
  -- we should always mark the result kind variable (`k3` in this example) as
  -- injective.  The reason is that result type has always an assigned kind and
  -- therefore we can always infer the result kind if we know the result type.
  -- But this does not seem to be useful in any way so we don't do it.  (Another
  -- reason is that the implementation would not be straightforward.)
tcInjectivity tvs (Just (L loc (InjectivityAnn _ lInjNames)))
  = setSrcSpan loc $
    do { inj_tvs <- mapM tcFdTyVar lInjNames
       ; let inj_ktvs = closeOverKinds (mkVarSet inj_tvs)
       ; let inj_bools = map (`elemVarSet` inj_ktvs) tvs
       ; traceTc "tcInjectivity" (vcat [ ppr tvs, ppr lInjNames, ppr inj_tvs
                                       , ppr inj_ktvs, ppr inj_bools ])
       ; return $ Injective inj_bools }

805 806
tcTySynRhs :: RecTyInfo
           -> Name
807 808
           -> [TyVar] -> Kind
           -> LHsType Name -> TcM [TyThing]
809
tcTySynRhs rec_info tc_name tvs kind hs_ty
810 811 812 813
  = do { env <- getLclEnv
       ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
       ; rhs_ty <- tcCheckLHsType hs_ty kind
       ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
814
       ; let roles = rti_roles rec_info tc_name
Jan Stolarek's avatar
Jan Stolarek committed
815
             tycon = buildSynonymTyCon tc_name tvs roles rhs_ty kind
816 817
       ; return [ATyCon tycon] }

818
tcDataDefn :: RecTyInfo -> Name
819 820 821
           -> [TyVar] -> Kind
           -> HsDataDefn Name -> TcM [TyThing]
  -- NB: not used for newtype/data instances (whether associated or not)
822
tcDataDefn rec_info tc_name tvs kind
823 824
         (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
                     , dd_ctxt = ctxt, dd_kindSig = mb_ksig
825 826 827
                     , dd_cons = cons' })
 = let cons = cons' -- AZ List monad coming
   in do { extra_tvs <- tcDataKindSig kind
828
       ; let final_tvs  = tvs ++ extra_tvs
829
             roles      = rti_roles rec_info tc_name
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
830 831
       ; stupid_tc_theta <- tcHsContext ctxt
       ; stupid_theta    <- zonkTcTypeToTypes emptyZonkEnv stupid_tc_theta
832
       ; kind_signatures <- xoptM Opt_KindSignatures
833
       ; is_boot         <- tcIsHsBootOrSig -- Are we compiling an hs-boot file?
834 835

             -- Check that we don't use kind signatures without Glasgow extensions
836 837 838 839
       ; case mb_ksig of
           Nothing   -> return ()
           Just hs_k -> do { checkTc (kind_signatures) (badSigTyDecl tc_name)
                           ; tc_kind <- tcLHsKind hs_k
840
                           ; checkKind kind tc_kind