compiler/typecheck/TcTyClsDecls.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 % (c) The AQUA Project, Glasgow University, 1996-1998
   4 %
   5
   6 TcTyClsDecls: Typecheck type and class declarations
   7
   8 \begin{code}
   9 {-# LANGUAGE TupleSections #-}
  10
  11 module TcTyClsDecls (
  12         tcTyAndClassDecls, tcAddImplicits,
  13
  14         -- Functions used by TcInstDcls to check
  15         -- data/type family instance declarations
  16         kcDataDefn, tcConDecls, dataDeclChecks, checkValidTyCon,
  17         tcSynFamInstDecl, tcFamTyPats,
  18         tcAddTyFamInstCtxt, tcAddDataFamInstCtxt,
  19         wrongKindOfFamily,
  20     ) where
  21
  22 #include "HsVersions.h"
  23
  24 import HsSyn
  25 import HscTypes
  26 import BuildTyCl
  27 import TcRnMonad
  28 import TcEnv
  29 import TcValidity
  30 import TcHsSyn
  31 import TcBinds( tcRecSelBinds )
  32 import FunDeps( growThetaTyVars )
  33 import TcTyDecls
  34 import TcClassDcl
  35 import TcHsType
  36 import TcMType
  37 import TcType
  38 import TysWiredIn( unitTy )
  39 import FamInst
  40 import Coercion( mkCoAxBranch )
  41 import Type
  42 import Kind
  43 import Class
  44 import CoAxiom( CoAxBranch(..) )
  45 import TyCon
  46 import DataCon
  47 import Id
  48 import MkCore           ( rEC_SEL_ERROR_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
  57 import Outputable
  58 import Maybes
  59 import Unify
  60 import Util
  61 import SrcLoc
  62 import ListSetOps
  63 import Digraph
  64 import DynFlags
  65 import FastString
  66 import Unique           ( mkBuiltinUnique )
  67 import BasicTypes
  68
  69 import Bag
  70 import Control.Monad
  71 import Data.List
  72 \end{code}
  73
  74
  75 %************************************************************************
  76 %*                                                                      *
  77 \subsection{Type checking for type and class declarations}
  78 %*                                                                      *
  79 %************************************************************************
  80
  81 Note [Grouping of type and class declarations]
  82 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  83 tcTyAndClassDecls is called on a list of `TyClGroup`s. Each group is a strongly
  84 connected component of mutually dependent types and classes. We kind check and
  85 type check each group separately to enhance kind polymorphism. Take the
  86 following example:
  87
  88   type Id a = a
  89   data X = X (Id Int)
  90
  91 If we were to kind check the two declarations together, we would give Id the
  92 kind * -> *, since we apply it to an Int in the definition of X. But we can do
  93 better than that, since Id really is kind polymorphic, and should get kind
  94 forall (k::BOX). k -> k. Since it does not depend on anything else, it can be
  95 kind-checked by itself, hence getting the most general kind. We then kind check
  96 X, which works fine because we then know the polymorphic kind of Id, and simply
  97 instantiate k to *.
  98
  99 \begin{code}
 100
 101 tcTyAndClassDecls :: ModDetails
 102                   -> [TyClGroup Name]   -- Mutually-recursive groups in dependency order
 103                   -> TcM TcGblEnv       -- Input env extended by types and classes
 104                                         -- and their implicit Ids,DataCons
 105 -- Fails if there are any errors
 106 tcTyAndClassDecls boot_details tyclds_s
 107   = checkNoErrs $       -- The code recovers internally, but if anything gave rise to
 108                         -- an error we'd better stop now, to avoid a cascade
 109     fold_env tyclds_s   -- Type check each group in dependency order folding the global env
 110   where
 111     fold_env :: [TyClGroup Name] -> TcM TcGblEnv
 112     fold_env [] = getGblEnv
 113     fold_env (tyclds:tyclds_s)
 114       = do { tcg_env <- tcTyClGroup boot_details tyclds
 115            ; setGblEnv tcg_env $ fold_env tyclds_s }
 116              -- remaining groups are typecheck in the extended global env
 117
 118 tcTyClGroup :: ModDetails -> TyClGroup Name -> TcM TcGblEnv
 119 -- Typecheck one strongly-connected component of type and class decls
 120 tcTyClGroup boot_details tyclds
 121   = do {    -- Step 1: kind-check this group and returns the final
 122             -- (possibly-polymorphic) kind of each TyCon and Class
 123             -- See Note [Kind checking for type and class decls]
 124          names_w_poly_kinds <- kcTyClGroup tyclds
 125        ; traceTc "tcTyAndCl generalized kinds" (ppr names_w_poly_kinds)
 126
 127             -- Step 2: type-check all groups together, returning
 128             -- the final TyCons and Classes
 129        ; tyclss <- fixM $ \ rec_tyclss -> do
 130            { let rec_flags = calcRecFlags boot_details rec_tyclss
 131
 132                  -- Populate environment with knot-tied ATyCon for TyCons
 133                  -- NB: if the decls mention any ill-staged data cons
 134                  -- (see Note [Recusion and promoting data constructors]
 135                  -- we will have failed already in kcTyClGroup, so no worries here
 136            ; tcExtendRecEnv (zipRecTyClss names_w_poly_kinds rec_tyclss) $
 137
 138                  -- Also extend the local type envt with bindings giving
 139                  -- the (polymorphic) kind of each knot-tied TyCon or Class
 140                  -- See Note [Type checking recursive type and class declarations]
 141              tcExtendKindEnv names_w_poly_kinds              $
 142
 143                  -- Kind and type check declarations for this group
 144              concatMapM (tcTyClDecl rec_flags) tyclds }
 145
 146            -- Step 3: Perform the validity chebck
 147            -- We can do this now because we are done with the recursive knot
 148            -- Do it before Step 4 (adding implicit things) because the latter
 149            -- expects well-formed TyCons
 150        ; tcExtendGlobalEnv tyclss $ do
 151        { traceTc "Starting validity check" (ppr tyclss)
 152        ; checkNoErrs $
 153          mapM_ (recoverM (return ()) . addLocM checkValidTyCl) tyclds
 154            -- We recover, which allows us to report multiple validity errors
 155            -- but we then fail if any are wrong.  Lacking the checkNoErrs
 156            -- we get Trac #7175
 157
 158            -- Step 4: Add the implicit things;
 159            -- we want them in the environment because
 160            -- they may be mentioned in interface files
 161        ; tcExtendGlobalValEnv (mkDefaultMethodIds tyclss) $
 162          tcAddImplicits tyclss } }
 163
 164 tcAddImplicits :: [TyThing] -> TcM TcGblEnv
 165 tcAddImplicits tyclss
 166  = tcExtendGlobalEnvImplicit implicit_things $
 167    tcRecSelBinds rec_sel_binds
 168  where
 169    implicit_things = concatMap implicitTyThings tyclss
 170    rec_sel_binds   = mkRecSelBinds tyclss
 171
 172 zipRecTyClss :: [(Name, Kind)]
 173              -> [TyThing]           -- Knot-tied
 174              -> [(Name,TyThing)]
 175 -- Build a name-TyThing mapping for the things bound by decls
 176 -- being careful not to look at the [TyThing]
 177 -- The TyThings in the result list must have a visible ATyCon,
 178 -- because typechecking types (in, say, tcTyClDecl) looks at this outer constructor
 179 zipRecTyClss kind_pairs rec_things
 180   = [ (name, ATyCon (get name)) | (name, _kind) <- kind_pairs ]
 181   where
 182     rec_type_env :: TypeEnv
 183     rec_type_env = mkTypeEnv rec_things
 184
 185     get name = case lookupTypeEnv rec_type_env name of
 186                  Just (ATyCon tc) -> tc
 187                  other            -> pprPanic "zipRecTyClss" (ppr name <+> ppr other)
 188 \end{code}
 189
 190
 191 %************************************************************************
 192 %*                                                                      *
 193                 Kind checking
 194 %*                                                                      *
 195 %************************************************************************
 196
 197 Note [Kind checking for type and class decls]
 198 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 199 Kind checking is done thus:
 200
 201    1. Make up a kind variable for each parameter of the *data* type,
 202       and class, decls, and extend the kind environment (which is in
 203       the TcLclEnv)
 204
 205    2. Dependency-analyse the type *synonyms* (which must be non-recursive),
 206       and kind-check them in dependency order.  Extend the kind envt.
 207
 208    3. Kind check the data type and class decls
 209
 210 Synonyms are treated differently to data type and classes,
 211 because a type synonym can be an unboxed type
 212         type Foo = Int#
 213 and a kind variable can't unify with UnboxedTypeKind
 214 So we infer their kinds in dependency order
 215
 216 We need to kind check all types in the mutually recursive group
 217 before we know the kind of the type variables.  For example:
 218
 219   class C a where
 220      op :: D b => a -> b -> b
 221
 222   class D c where
 223      bop :: (Monad c) => ...
 224
 225 Here, the kind of the locally-polymorphic type variable "b"
 226 depends on *all the uses of class D*.  For example, the use of
 227 Monad c in bop's type signature means that D must have kind Type->Type.
 228
 229 However type synonyms work differently.  They can have kinds which don't
 230 just involve (->) and *:
 231         type R = Int#           -- Kind #
 232         type S a = Array# a     -- Kind * -> #
 233         type T a b = (# a,b #)  -- Kind * -> * -> (# a,b #)
 234 So we must infer their kinds from their right-hand sides *first* and then
 235 use them, whereas for the mutually recursive data types D we bring into
 236 scope kind bindings D -> k, where k is a kind variable, and do inference.
 237
 238 Type families
 239 ~~~~~~~~~~~~~
 240 This treatment of type synonyms only applies to Haskell 98-style synonyms.
 241 General type functions can be recursive, and hence, appear in `alg_decls'.
 242
 243 The kind of a type family is solely determinded by its kind signature;
 244 hence, only kind signatures participate in the construction of the initial
 245 kind environment (as constructed by `getInitialKind').  In fact, we ignore
 246 instances of families altogether in the following.  However, we need to
 247 include the kinds of *associated* families into the construction of the
 248 initial kind environment.  (This is handled by `allDecls').
 249
 250
 251 \begin{code}
 252 kcTyClGroup :: TyClGroup Name -> TcM [(Name,Kind)]
 253 -- Kind check this group, kind generalize, and return the resulting local env
 254 -- This bindds the TyCons and Classes of the group, but not the DataCons
 255 -- See Note [Kind checking for type and class decls]
 256 kcTyClGroup decls
 257   = do  { mod <- getModule
 258         ; traceTc "kcTyClGroup" (ptext (sLit "module") <+> ppr mod $$ vcat (map ppr decls))
 259
 260           -- Kind checking;
 261           --    1. Bind kind variables for non-synonyms
 262           --    2. Kind-check synonyms, and bind kinds of those synonyms
 263           --    3. Kind-check non-synonyms
 264           --    4. Generalise the inferred kinds
 265           -- See Note [Kind checking for type and class decls]
 266
 267           -- Step 1: Bind kind variables for non-synonyms
 268         ; let (syn_decls, non_syn_decls) = partition (isSynDecl . unLoc) decls
 269         ; initial_kinds <- getInitialKinds TopLevel non_syn_decls
 270         ; traceTc "kcTyClGroup: initial kinds" (ppr initial_kinds)
 271
 272         -- Step 2: Set initial envt, kind-check the synonyms
 273         ; lcl_env <- tcExtendTcTyThingEnv initial_kinds $
 274                      kcSynDecls (calcSynCycles syn_decls)
 275
 276         -- Step 3: Set extended envt, kind-check the non-synonyms
 277         ; setLclEnv lcl_env $
 278           mapM_ kcLTyClDecl non_syn_decls
 279
 280              -- Step 4: generalisation
 281              -- Kind checking done for this group
 282              -- Now we have to kind generalize the flexis
 283         ; res <- concatMapM (generaliseTCD (tcl_env lcl_env)) decls
 284
 285         ; traceTc "kcTyClGroup result" (ppr res)
 286         ; return res }
 287
 288   where
 289     generalise :: TcTypeEnv -> Name -> LHsTyVarBndrs Name -> TcM (Name, Kind)
 290     -- For polymorphic things this is a no-op
 291     generalise kind_env name tvs
 292       = do { let kc_kind = case lookupNameEnv kind_env name of
 293                                Just (AThing k) -> k
 294                                _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env)
 295            ; kvs <- kindGeneralize (tyVarsOfType kc_kind) (hsLTyVarNames tvs)
 296            ; kc_kind' <- zonkTcKind kc_kind    -- Make sure kc_kind' has the final,
 297                                                -- skolemised kind variables
 298            ; traceTc "Generalise kind" (vcat [ ppr name, ppr kc_kind, ppr kvs, ppr kc_kind' ])
 299            ; return (name, mkForAllTys kvs kc_kind') }
 300
 301     generaliseTCD :: TcTypeEnv -> LTyClDecl Name -> TcM [(Name, Kind)]
 302     generaliseTCD kind_env (L _ decl)
 303       | ClassDecl { tcdLName = (L _ name), tcdTyVars = tyvars, tcdATs = ats } <- decl
 304       = do { first <- generalise kind_env name tyvars
 305            ; rest <- mapM ((generaliseFamDecl kind_env) . unLoc) ats
 306            ; return (first : rest) }
 307
 308       | FamDecl { tcdFam = fam } <- decl
 309       = do { res <- generaliseFamDecl kind_env fam
 310            ; return [res] }
 311
 312       | ForeignType {} <- decl
 313       = pprPanic "generaliseTCD" (ppr decl)
 314
 315       | otherwise
 316       -- Note: tcdTyVars is safe here because we've eliminated FamDecl and ForeignType
 317       = do { res <- generalise kind_env (tcdName decl) (tcdTyVars decl)
 318            ; return [res] }
 319
 320     generaliseFamDecl :: TcTypeEnv -> FamilyDecl Name -> TcM (Name, Kind)
 321     generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name, fdTyVars = tyvars })
 322       = generalise kind_env name tyvars
 323
 324 mk_thing_env :: [LTyClDecl Name] -> [(Name, TcTyThing)]
 325 mk_thing_env [] = []
 326 mk_thing_env (decl : decls)
 327   | L _ (ClassDecl { tcdLName = L _ nm, tcdATs = ats }) <- decl
 328   = (nm, APromotionErr ClassPE) :
 329     (map (, APromotionErr TyConPE) $ map (unLoc . fdLName . unLoc) ats) ++
 330     (mk_thing_env decls)
 331
 332   | otherwise
 333   = (tcdName (unLoc decl), APromotionErr TyConPE) :
 334     (mk_thing_env decls)
 335
 336 getInitialKinds :: TopLevelFlag -> [LTyClDecl Name] -> TcM [(Name, TcTyThing)]
 337 getInitialKinds top_lvl decls
 338   = tcExtendTcTyThingEnv (mk_thing_env decls) $
 339     concatMapM (addLocM (getInitialKind top_lvl)) decls
 340
 341 getInitialKind :: TopLevelFlag -> TyClDecl Name -> TcM [(Name, TcTyThing)]
 342 -- Allocate a fresh kind variable for each TyCon and Class
 343 -- For each tycon, return   (tc, AThing k)
 344 --                 where k is the kind of tc, derived from the LHS
 345 --                       of the definition (and probably including
 346 --                       kind unification variables)
 347 --      Example: data T a b = ...
 348 --      return (T, kv1 -> kv2 -> kv3)
 349 --
 350 -- This pass deals with (ie incorporates into the kind it produces)
 351 --   * The kind signatures on type-variable binders
 352 --   * The result kinds signature on a TyClDecl
 353 --
 354 -- ALSO for each datacon, return (dc, APromotionErr RecDataConPE)
 355 -- Note [ARecDataCon: Recursion and promoting data constructors]
 356 --
 357 -- No family instances are passed to getInitialKinds
 358
 359 getInitialKind top_lvl (FamDecl { tcdFam = decl }) = getFamDeclInitialKind top_lvl decl
 360 getInitialKind _ (ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
 361   = kcHsTyVarBndrs False ktvs $ \ arg_kinds ->
 362     do { inner_prs <- getFamDeclInitialKinds ats
 363        ; let main_pr = (name, AThing (mkArrowKinds arg_kinds constraintKind))
 364        ; return (main_pr : inner_prs) }
 365
 366 getInitialKind _top_lvl decl@(SynDecl {}) = pprPanic "getInitialKind" (ppr decl)
 367
 368 getInitialKind top_lvl (DataDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdDataDefn = defn })
 369   | HsDataDefn { dd_kindSig = Just ksig, dd_cons = cons } <- defn
 370   = ASSERT( isTopLevel top_lvl )
 371     kcHsTyVarBndrs True ktvs $ \ arg_kinds ->
 372     do { res_k <- tcLHsKind ksig
 373        ; let body_kind = mkArrowKinds arg_kinds res_k
 374              kvs       = varSetElems (tyVarsOfType body_kind)
 375              main_pr   = (name, AThing (mkForAllTys kvs body_kind))
 376              inner_prs = [(unLoc (con_name con), APromotionErr RecDataConPE) | L _ con <- cons ]
 377              -- See Note [Recusion and promoting data constructors]
 378        ; return (main_pr : inner_prs) }
 379
 380   | HsDataDefn { dd_cons = cons } <- defn
 381   = kcHsTyVarBndrs False ktvs $ \ arg_kinds ->
 382     do { let main_pr   = (name, AThing (mkArrowKinds arg_kinds liftedTypeKind))
 383              inner_prs = [ (unLoc (con_name con), APromotionErr RecDataConPE)
 384                          | L _ con <- cons ]
 385              -- See Note [Recusion and promoting data constructors]
 386        ; return (main_pr : inner_prs) }
 387
 388 getInitialKind _ (ForeignType { tcdLName = L _ name })
 389   = return [(name, AThing liftedTypeKind)]
 390
 391 getFamDeclInitialKinds :: [LFamilyDecl Name] -> TcM [(Name, TcTyThing)]
 392 getFamDeclInitialKinds decls
 393   = tcExtendTcTyThingEnv [ (n, APromotionErr TyConPE)
 394                          | L _ (FamilyDecl { fdLName = L _ n }) <- decls] $
 395     concatMapM (addLocM (getFamDeclInitialKind NotTopLevel)) decls
 396
 397 getFamDeclInitialKind :: TopLevelFlag
 398                       -> FamilyDecl Name
 399                       -> TcM [(Name, TcTyThing)]
 400 getFamDeclInitialKind top_lvl (FamilyDecl { fdLName = L _ name
 401                                           , fdTyVars = ktvs
 402                                           , fdKindSig = ksig })
 403   | isTopLevel top_lvl
 404   = kcHsTyVarBndrs True ktvs $ \ arg_kinds ->
 405     do { res_k <- case ksig of
 406                     Just k  -> tcLHsKind k
 407                     Nothing -> return liftedTypeKind
 408        ; let body_kind = mkArrowKinds arg_kinds res_k
 409              kvs       = varSetElems (tyVarsOfType body_kind)
 410        ; return [ (name, AThing (mkForAllTys kvs body_kind)) ] }
 411
 412   | otherwise
 413   = kcHsTyVarBndrs False ktvs $ \ arg_kinds ->
 414     do { res_k <- case ksig of
 415                     Just k  -> tcLHsKind k
 416                     Nothing -> newMetaKindVar
 417        ; return [ (name, AThing (mkArrowKinds arg_kinds res_k)) ] }
 418
 419 ----------------
 420 kcSynDecls :: [SCC (LTyClDecl Name)] -> TcM TcLclEnv    -- Kind bindings
 421 kcSynDecls [] = getLclEnv
 422 kcSynDecls (group : groups)
 423   = do  { nk <- kcSynDecl1 group
 424         ; tcExtendKindEnv [nk] (kcSynDecls groups) }
 425
 426 kcSynDecl1 :: SCC (LTyClDecl Name)
 427            -> TcM (Name,TcKind) -- Kind bindings
 428 kcSynDecl1 (AcyclicSCC (L _ decl)) = kcSynDecl decl
 429 kcSynDecl1 (CyclicSCC decls)       = do { recSynErr decls; failM }
 430                                      -- Fail here to avoid error cascade
 431                                      -- of out-of-scope tycons
 432
 433 kcSynDecl :: TyClDecl Name -> TcM (Name, TcKind)
 434 kcSynDecl decl@(SynDecl { tcdTyVars = hs_tvs, tcdLName = L _ name
 435                        , tcdRhs = rhs })
 436   -- Returns a possibly-unzonked kind
 437   = tcAddDeclCtxt decl $
 438     kcHsTyVarBndrs False hs_tvs $ \ ks ->
 439     do { traceTc "kcd1" (ppr name <+> brackets (ppr hs_tvs)
 440                          <+> brackets (ppr ks))
 441        ; (_, rhs_kind) <- tcLHsType rhs
 442        ; traceTc "kcd2" (ppr name)
 443        ; let tc_kind = mkArrowKinds ks rhs_kind
 444        ; return (name, tc_kind) }
 445 kcSynDecl decl = pprPanic "kcSynDecl" (ppr decl)
 446
 447 ------------------------------------------------------------------------
 448 kcLTyClDecl :: LTyClDecl Name -> TcM ()
 449   -- See Note [Kind checking for type and class decls]
 450 kcLTyClDecl (L loc decl)
 451   = setSrcSpan loc $ tcAddDeclCtxt decl $ kcTyClDecl decl
 452
 453 kcTyClDecl :: TyClDecl Name -> TcM ()
 454 -- This function is used solely for its side effect on kind variables
 455 -- NB kind signatures on the type variables and
 456 --    result kind signature have aready been dealt with
 457 --    by getInitialKind, so we can ignore them here.
 458
 459 kcTyClDecl (DataDecl { tcdLName = L _ name, tcdTyVars = hs_tvs, tcdDataDefn = defn })
 460   | HsDataDefn { dd_cons = cons, dd_kindSig = Just _ } <- defn
 461   = mapM_ (wrapLocM kcConDecl) cons
 462     -- hs_tvs and td_kindSig already dealt with in getInitialKind
 463     -- Ignore the dd_ctxt; heavily deprecated and inconvenient
 464
 465   | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
 466   = kcTyClTyVars name hs_tvs $
 467     do  { _ <- tcHsContext ctxt
 468         ; mapM_ (wrapLocM kcConDecl) cons }
 469
 470 kcTyClDecl decl@(SynDecl {}) = pprPanic "kcTyClDecl" (ppr decl)
 471
 472 kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs
 473                        , tcdCtxt = ctxt, tcdSigs = sigs })
 474   = kcTyClTyVars name hs_tvs $
 475     do  { _ <- tcHsContext ctxt
 476         ; mapM_ (wrapLocM kc_sig)     sigs }
 477   where
 478     kc_sig (TypeSig _ op_ty)    = discardResult (tcHsLiftedType op_ty)
 479     kc_sig (GenericSig _ op_ty) = discardResult (tcHsLiftedType op_ty)
 480     kc_sig _                    = return ()
 481
 482 kcTyClDecl (ForeignType {}) = return ()
 483 kcTyClDecl (FamDecl {})    = return ()
 484
 485 -------------------
 486 kcConDecl :: ConDecl Name -> TcM ()
 487 kcConDecl (ConDecl { con_name = name, con_qvars = ex_tvs
 488                    , con_cxt = ex_ctxt, con_details = details, con_res = res })
 489   = addErrCtxt (dataConCtxt name) $
 490     kcHsTyVarBndrs False ex_tvs $ \ _ ->
 491     do { _ <- tcHsContext ex_ctxt
 492        ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details)
 493        ; _ <- tcConRes res
 494        ; return () }
 495 \end{code}
 496
 497 Note [Recursion and promoting data constructors]
 498 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 499 We don't want to allow promotion in a strongly connected component
 500 when kind checking.
 501
 502 Consider:
 503   data T f = K (f (K Any))
 504
 505 When kind checking the `data T' declaration the local env contains the
 506 mappings:
 507   T -> AThing <some initial kind>
 508   K -> ARecDataCon
 509
 510 ANothing is only used for DataCons, and only used during type checking
 511 in tcTyClGroup.
 512
 513
 514 %************************************************************************
 515 %*                                                                      *
 516 \subsection{Type checking}
 517 %*                                                                      *
 518 %************************************************************************
 519
 520 Note [Type checking recursive type and class declarations]
 521 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 522 At this point we have completed *kind-checking* of a mutually
 523 recursive group of type/class decls (done in kcTyClGroup). However,
 524 we discarded the kind-checked types (eg RHSs of data type decls);
 525 note that kcTyClDecl returns ().  There are two reasons:
 526
 527   * It's convenient, because we don't have to rebuild a
 528     kinded HsDecl (a fairly elaborate type)
 529
 530   * It's necessary, because after kind-generalisation, the
 531     TyCons/Classes may now be kind-polymorphic, and hence need
 532     to be given kind arguments.
 533
 534 Example:
 535        data T f a = MkT (f a) (T f a)
 536 During kind-checking, we give T the kind T :: k1 -> k2 -> *
 537 and figure out constraints on k1, k2 etc. Then we generalise
 538 to get   T :: forall k. (k->*) -> k -> *
 539 So now the (T f a) in the RHS must be elaborated to (T k f a).
 540
 541 However, during tcTyClDecl of T (above) we will be in a recursive
 542 "knot". So we aren't allowed to look at the TyCon T itself; we are only
 543 allowed to put it (lazily) in the returned structures.  But when
 544 kind-checking the RHS of T's decl, we *do* need to know T's kind (so
 545 that we can correctly elaboarate (T k f a).  How can we get T's kind
 546 without looking at T?  Delicate answer: during tcTyClDecl, we extend
 547
 548   *Global* env with T -> ATyCon (the (not yet built) TyCon for T)
 549   *Local*  env with T -> AThing (polymorphic kind of T)
 550
 551 Then:
 552
 553   * During TcHsType.kcTyVar we look in the *local* env, to get the
 554     known kind for T.
 555
 556   * But in TcHsType.ds_type (and ds_var_app in particular) we look in
 557     the *global* env to get the TyCon. But we must be careful not to
 558     force the TyCon or we'll get a loop.
 559
 560 This fancy footwork (with two bindings for T) is only necesary for the
 561 TyCons or Classes of this recursive group.  Earlier, finished groups,
 562 live in the global env only.
 563
 564 \begin{code}
 565 tcTyClDecl :: RecTyInfo -> LTyClDecl Name -> TcM [TyThing]
 566 tcTyClDecl rec_info (L loc decl)
 567   = setSrcSpan loc $ tcAddDeclCtxt decl $
 568     traceTc "tcTyAndCl-x" (ppr decl) >>
 569     tcTyClDecl1 NoParentTyCon rec_info decl
 570
 571   -- "type family" declarations
 572 tcTyClDecl1 :: TyConParent -> RecTyInfo -> TyClDecl Name -> TcM [TyThing]
 573 tcTyClDecl1 parent _rec_info (FamDecl { tcdFam = fd })
 574   = tcFamDecl1 parent fd
 575
 576   -- "type" synonym declaration
 577 tcTyClDecl1 _parent _rec_info
 578             (SynDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdRhs = rhs })
 579   = ASSERT( isNoParent _parent )
 580     tcTyClTyVars tc_name tvs $ \ tvs' kind ->
 581     tcTySynRhs tc_name tvs' kind rhs
 582
 583   -- "data/newtype" declaration
 584 tcTyClDecl1 _parent rec_info
 585             (DataDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdDataDefn = defn })
 586   = ASSERT( isNoParent _parent )
 587     tcTyClTyVars tc_name tvs $ \ tvs' kind ->
 588     tcDataDefn rec_info tc_name tvs' kind defn
 589
 590 tcTyClDecl1 _parent rec_info
 591             (ClassDecl { tcdLName = L _ class_name, tcdTyVars = tvs
 592             , tcdCtxt = ctxt, tcdMeths = meths
 593             , tcdFDs = fundeps, tcdSigs = sigs
 594             , tcdATs = ats, tcdATDefs = at_defs })
 595   = ASSERT( isNoParent _parent )
 596     do { (clas, tvs', gen_dm_env) <- fixM $ \ ~(clas,_,_) ->
 597             tcTyClTyVars class_name tvs $ \ tvs' kind ->
 598             do { MASSERT( isConstraintKind kind )
 599                ; let    -- This little knot is just so we can get
 600                         -- hold of the name of the class TyCon, which we
 601                         -- need to look up its recursiveness
 602                     tycon_name = tyConName (classTyCon clas)
 603                     tc_isrec = rti_is_rec rec_info tycon_name
 604
 605                ; ctxt' <- tcHsContext ctxt
 606                ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'
 607                        -- Squeeze out any kind unification variables
 608                ; fds'  <- mapM (addLocM tc_fundep) fundeps
 609                ; (sig_stuff, gen_dm_env) <- tcClassSigs class_name sigs meths
 610                ; at_stuff <- tcClassATs class_name (AssocFamilyTyCon clas) ats at_defs
 611                ; clas <- buildClass False {- Must include unfoldings for selectors -}
 612                             class_name tvs' ctxt' fds' at_stuff
 613                             sig_stuff tc_isrec
 614                ; traceTc "tcClassDecl" (ppr fundeps $$ ppr tvs' $$ ppr fds')
 615                ; return (clas, tvs', gen_dm_env) }
 616
 617        ; let { gen_dm_ids = [ AnId (mkExportedLocalId gen_dm_name gen_dm_ty)
 618                             | (sel_id, GenDefMeth gen_dm_name) <- classOpItems clas
 619                             , let gen_dm_tau = expectJust "tcTyClDecl1" $
 620                                                lookupNameEnv gen_dm_env (idName sel_id)
 621                             , let gen_dm_ty = mkSigmaTy tvs'
 622                                                       [mkClassPred clas (mkTyVarTys tvs')]
 623                                                       gen_dm_tau
 624                             ]
 625              ; class_ats = map ATyCon (classATs clas) }
 626
 627        ; return (ATyCon (classTyCon clas) : gen_dm_ids ++ class_ats ) }
 628          -- NB: Order is important due to the call to `mkGlobalThings' when
 629          --     tying the the type and class declaration type checking knot.
 630   where
 631     tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM tc_fd_tyvar tvs1 ;
 632                                 ; tvs2' <- mapM tc_fd_tyvar tvs2 ;
 633                                 ; return (tvs1', tvs2') }
 634     tc_fd_tyvar name   -- Scoped kind variables are bound to unification variables
 635                        -- which are now fixed, so we can zonk
 636       = do { tv <- tcLookupTyVar name
 637            ; ty <- zonkTyVarOcc emptyZonkEnv tv
 638                   -- Squeeze out any kind unification variables
 639            ; case getTyVar_maybe ty of
 640                Just tv' -> return tv'
 641                Nothing  -> pprPanic "tc_fd_tyvar" (ppr name $$ ppr tv $$ ppr ty) }
 642
 643 tcTyClDecl1 _ _
 644   (ForeignType {tcdLName = L _ tc_name, tcdExtName = tc_ext_name})
 645   = return [ATyCon (mkForeignTyCon tc_name tc_ext_name liftedTypeKind 0)]
 646 \end{code}
 647
 648 \begin{code}
 649 tcFamDecl1 :: TyConParent -> FamilyDecl Name -> TcM [TyThing]
 650 tcFamDecl1 parent
 651             (FamilyDecl {fdFlavour = TypeFamily, fdLName = L _ tc_name, fdTyVars = tvs})
 652   = tcTyClTyVars tc_name tvs $ \ tvs' kind -> do
 653   { traceTc "type family:" (ppr tc_name)
 654   ; checkFamFlag tc_name
 655   ; let syn_rhs = SynFamilyTyCon { synf_open = True, synf_injective = False }
 656   ; tycon <- buildSynTyCon tc_name tvs' syn_rhs kind parent
 657   ; return [ATyCon tycon] }
 658
 659 tcFamDecl1 parent
 660            (FamilyDecl {fdFlavour = DataFamily, fdLName = L _ tc_name, fdTyVars = tvs})
 661   = tcTyClTyVars tc_name tvs $ \ tvs' kind -> do
 662   { traceTc "data family:" (ppr tc_name)
 663   ; checkFamFlag tc_name
 664   ; extra_tvs <- tcDataKindSig kind
 665   ; let final_tvs = tvs' ++ extra_tvs    -- we may not need these
 666         tycon = buildAlgTyCon tc_name final_tvs Nothing []
 667                               DataFamilyTyCon Recursive
 668                               False   -- Not promotable to the kind level
 669                               True    -- GADT syntax
 670                               parent
 671   ; return [ATyCon tycon] }
 672
 673 tcTySynRhs :: Name
 674            -> [TyVar] -> Kind
 675            -> LHsType Name -> TcM [TyThing]
 676 tcTySynRhs tc_name tvs kind hs_ty
 677   = do { env <- getLclEnv
 678        ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
 679        ; rhs_ty <- tcCheckLHsType hs_ty kind
 680        ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
 681        ; tycon <- buildSynTyCon tc_name tvs (SynonymTyCon rhs_ty)
 682                                 kind NoParentTyCon
 683        ; return [ATyCon tycon] }
 684
 685 tcDataDefn :: RecTyInfo -> Name
 686            -> [TyVar] -> Kind
 687            -> HsDataDefn Name -> TcM [TyThing]
 688   -- NB: not used for newtype/data instances (whether associated or not)
 689 tcDataDefn rec_info tc_name tvs kind
 690          (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
 691                      , dd_ctxt = ctxt, dd_kindSig = mb_ksig
 692                      , dd_cons = cons })
 693   = do { extra_tvs <- tcDataKindSig kind
 694        ; let final_tvs  = tvs ++ extra_tvs
 695        ; stupid_theta <- tcHsContext ctxt
 696        ; kind_signatures <- xoptM Opt_KindSignatures
 697        ; is_boot         <- tcIsHsBoot  -- Are we compiling an hs-boot file?
 698
 699              -- Check that we don't use kind signatures without Glasgow extensions
 700        ; case mb_ksig of
 701            Nothing   -> return ()
 702            Just hs_k -> do { checkTc (kind_signatures) (badSigTyDecl tc_name)
 703                            ; tc_kind <- tcLHsKind hs_k
 704                            ; checkKind kind tc_kind
 705                            ; return () }
 706
 707        ; h98_syntax <- dataDeclChecks tc_name new_or_data stupid_theta cons
 708
 709        ; tycon <- fixM $ \ tycon -> do
 710              { let res_ty = mkTyConApp tycon (mkTyVarTys final_tvs)
 711              ; data_cons <- tcConDecls new_or_data tycon (final_tvs, res_ty) cons
 712              ; tc_rhs <-
 713                  if null cons && is_boot              -- In a hs-boot file, empty cons means
 714                  then return totallyAbstractTyConRhs  -- "don't know"; hence totally Abstract
 715                  else case new_or_data of
 716                    DataType -> return (mkDataTyConRhs data_cons)
 717                    NewType  -> ASSERT( not (null data_cons) )
 718                                     mkNewTyConRhs tc_name tycon (head data_cons)
 719              ; return (buildAlgTyCon tc_name final_tvs cType stupid_theta tc_rhs
 720                                      (rti_is_rec rec_info tc_name)
 721                                      (rti_promotable rec_info)
 722                                      (not h98_syntax) NoParentTyCon) }
 723        ; return [ATyCon tycon] }
 724 \end{code}
 725
 726 %************************************************************************
 727 %*                                                                      *
 728                Typechecking associated types (in class decls)
 729                (including the associated-type defaults)
 730 %*                                                                      *
 731 %************************************************************************
 732
 733 Note [Associated type defaults]
 734 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 735
 736 The following is an example of associated type defaults:
 737              class C a where
 738                data D a
 739
 740                type F a b :: *
 741                type F a Z = [a]        -- Default
 742                type F a (S n) = F a n  -- Default
 743
 744 Note that:
 745   - We can have more than one default definition for a single associated type,
 746     as long as they do not overlap (same rules as for instances)
 747   - We can get default definitions only for type families, not data families
 748
 749 \begin{code}
 750 tcClassATs :: Name             -- The class name (not knot-tied)
 751            -> TyConParent      -- The class parent of this associated type
 752            -> [LFamilyDecl Name] -- Associated types.
 753            -> [LTyFamInstDecl Name] -- Associated type defaults.
 754            -> TcM [ClassATItem]
 755 tcClassATs class_name parent ats at_defs
 756   = do {  -- Complain about associated type defaults for non associated-types
 757          sequence_ [ failWithTc (badATErr class_name n)
 758                    | n <- map (tyFamInstDeclName . unLoc) at_defs
 759                    , not (n `elemNameSet` at_names) ]
 760        ; mapM tc_at ats }
 761   where
 762     at_names = mkNameSet (map (unLoc . fdLName . unLoc) ats)
 763
 764     at_defs_map :: NameEnv [LTyFamInstDecl Name]
 765     -- Maps an AT in 'ats' to a list of all its default defs in 'at_defs'
 766     at_defs_map = foldr (\at_def nenv -> extendNameEnv_C (++) nenv
 767                                           (tyFamInstDeclName (unLoc at_def)) [at_def])
 768                         emptyNameEnv at_defs
 769
 770     tc_at at = do { [ATyCon fam_tc] <- addLocM (tcFamDecl1 parent) at
 771                   ; let at_defs = lookupNameEnv at_defs_map (unLoc $ fdLName $ unLoc at)
 772                                         `orElse` []
 773                   ; atd <- concatMapM (tcDefaultAssocDecl fam_tc) at_defs
 774                   ; return (fam_tc, atd) }
 775
 776 -------------------------
 777 tcDefaultAssocDecl :: TyCon                -- ^ Family TyCon
 778                    -> LTyFamInstDecl Name  -- ^ RHS
 779                    -> TcM [CoAxBranch]     -- ^ Type checked RHS and free TyVars
 780 tcDefaultAssocDecl fam_tc (L loc decl)
 781   = setSrcSpan loc $
 782     tcAddTyFamInstCtxt decl $
 783     do { traceTc "tcDefaultAssocDecl" (ppr decl)
 784        ; tcSynFamInstDecl fam_tc decl }
 785     -- We check for well-formedness and validity later, in checkValidClass
 786
 787 -------------------------
 788 tcSynFamInstDecl :: TyCon -> TyFamInstDecl Name -> TcM [CoAxBranch]
 789 -- Placed here because type family instances appear as
 790 -- default decls in class declarations
 791 tcSynFamInstDecl fam_tc (TyFamInstDecl { tfid_eqns = eqns })
 792   -- we know the first equation matches the fam_tc because of the lookup logic
 793   -- now, just check that all other names match the first
 794   = do { let names = map (tfie_tycon . unLoc) eqns
 795              first = head names
 796        ; tcSynFamInstNames first names
 797        ; checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc)
 798        ; mapM (tcTyFamInstEqn fam_tc) eqns }
 799
 800 -- Checks to make sure that all the names in an instance group are the same
 801 tcSynFamInstNames :: Located Name -> [Located Name] -> TcM ()
 802 tcSynFamInstNames (L _ first) names
 803   = do { let badNames = filter ((/= first) . unLoc) names
 804        ; mapM_ (failLocated (wrongNamesInInstGroup first)) badNames }
 805   where
 806     failLocated :: (Name -> SDoc) -> Located Name -> TcM ()
 807     failLocated msg_fun (L loc name)
 808       = setSrcSpan loc $
 809         failWithTc (msg_fun name)
 810
 811 tcTyFamInstEqn :: TyCon -> LTyFamInstEqn Name -> TcM CoAxBranch
 812 tcTyFamInstEqn fam_tc
 813     (L loc (TyFamInstEqn { tfie_pats = pats, tfie_rhs = hs_ty }))
 814   = setSrcSpan loc $
 815     tcFamTyPats fam_tc pats (discardResult . (tcCheckLHsType hs_ty)) $
 816        \tvs' pats' res_kind ->
 817     do { rhs_ty <- tcCheckLHsType hs_ty res_kind
 818        ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
 819        ; traceTc "tcSynFamInstEqn" (ppr fam_tc <+> (ppr tvs' $$ ppr pats' $$ ppr rhs_ty))
 820        ; return (mkCoAxBranch tvs' pats' rhs_ty loc) }
 821
 822 kcDataDefn :: HsDataDefn Name -> TcKind -> TcM ()
 823 -- Used for 'data instance' only
 824 -- Ordinary 'data' is handled by kcTyClDec
 825 kcDataDefn (HsDataDefn { dd_ctxt = ctxt, dd_cons = cons, dd_kindSig = mb_kind }) res_k
 826   = do  { _ <- tcHsContext ctxt
 827         ; mapM_ (wrapLocM kcConDecl) cons
 828         ; kcResultKind mb_kind res_k }
 829
 830 ------------------
 831 kcResultKind :: Maybe (LHsKind Name) -> Kind -> TcM ()
 832 kcResultKind Nothing res_k
 833   = checkKind res_k liftedTypeKind
 834       --             type family F a
 835       -- defaults to type family F a :: *
 836 kcResultKind (Just k) res_k
 837   = do { k' <- tcLHsKind k
 838        ; checkKind  k' res_k }
 839
 840 -------------------------
 841 -- Kind check type patterns and kind annotate the embedded type variables.
 842 --     type instance F [a] = rhs
 843 --
 844 -- * Here we check that a type instance matches its kind signature, but we do
 845 --   not check whether there is a pattern for each type index; the latter
 846 --   check is only required for type synonym instances.
 847
 848 -----------------
 849 tcFamTyPats :: TyCon
 850             -> HsWithBndrs [LHsType Name] -- Patterns
 851             -> (TcKind -> TcM ())       -- Kind checker for RHS
 852                                         -- result is ignored
 853             -> ([TKVar] -> [TcType] -> Kind -> TcM a)
 854             -> TcM a
 855 -- Check the type patterns of a type or data family instance
 856 --     type instance F <pat1> <pat2> = <type>
 857 -- The 'tyvars' are the free type variables of pats
 858 --
 859 -- NB: The family instance declaration may be an associated one,
 860 -- nested inside an instance decl, thus
 861 --        instance C [a] where
 862 --          type F [a] = ...
 863 -- In that case, the type variable 'a' will *already be in scope*
 864 -- (and, if C is poly-kinded, so will its kind parameter).
 865
 866 tcFamTyPats fam_tc (HsWB { hswb_cts = arg_pats, hswb_kvs = kvars, hswb_tvs = tvars })
 867             kind_checker thing_inside
 868   = do { -- A family instance must have exactly the same number of type
 869          -- parameters as the family declaration.  You can't write
 870          --     type family F a :: * -> *
 871          --     type instance F Int y = y
 872          -- because then the type (F Int) would be like (\y.y)
 873        ; let (fam_kvs, fam_body) = splitForAllTys (tyConKind fam_tc)
 874              fam_arity = tyConArity fam_tc - length fam_kvs
 875        ; checkTc (length arg_pats == fam_arity) $
 876                  wrongNumberOfParmsErr fam_arity
 877
 878          -- Instantiate with meta kind vars
 879        ; fam_arg_kinds <- mapM (const newMetaKindVar) fam_kvs
 880        ; loc <- getSrcSpanM
 881        ; let (arg_kinds, res_kind)
 882                  = splitKindFunTysN fam_arity $
 883                    substKiWith fam_kvs fam_arg_kinds fam_body
 884              hs_tvs = HsQTvs { hsq_kvs = kvars
 885                              , hsq_tvs = userHsTyVarBndrs loc tvars }
 886
 887          -- Kind-check and quantify
 888          -- See Note [Quantifying over family patterns]
 889        ; typats <- tcHsTyVarBndrs hs_tvs $ \ _ ->
 890                    do { kind_checker res_kind
 891                       ; tcHsArgTys (quotes (ppr fam_tc)) arg_pats arg_kinds }
 892        ; let all_args = fam_arg_kinds ++ typats
 893
 894             -- Find free variables (after zonking) and turn
 895             -- them into skolems, so that we don't subsequently
 896             -- replace a meta kind var with AnyK
 897             -- Very like kindGeneralize
 898        ; tkvs <- zonkTyVarsAndFV (tyVarsOfTypes all_args)
 899        ; qtkvs <- zonkQuantifiedTyVars (varSetElems tkvs)
 900
 901             -- Zonk the patterns etc into the Type world
 902        ; (ze, qtkvs') <- zonkTyBndrsX emptyZonkEnv qtkvs
 903        ; all_args'    <- zonkTcTypeToTypes ze all_args
 904        ; res_kind'    <- zonkTcTypeToType  ze res_kind
 905
 906        ; traceTc "tcFamTyPats" (pprTvBndrs qtkvs' $$ ppr all_args' $$ ppr res_kind')
 907        ; tcExtendTyVarEnv qtkvs' $
 908          thing_inside qtkvs' all_args' res_kind' }
 909 \end{code}
 910
 911 Note [Quantifying over family patterns]
 912 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 913 We need to quantify over two different lots of kind variables:
 914
 915 First, the ones that come from the kinds of the tyvar args of
 916 tcTyVarBndrsKindGen, as usual
 917   data family Dist a
 918
 919   -- Proxy :: forall k. k -> *
 920   data instance Dist (Proxy a) = DP
 921   -- Generates  data DistProxy = DP
 922   --            ax8 k (a::k) :: Dist * (Proxy k a) ~ DistProxy k a
 923   -- The 'k' comes from the tcTyVarBndrsKindGen (a::k)
 924
 925 Second, the ones that come from the kind argument of the type family
 926 which we pick up using the (tyVarsOfTypes typats) in the result of
 927 the thing_inside of tcHsTyvarBndrsGen.
 928   -- Any :: forall k. k
 929   data instance Dist Any = DA
 930   -- Generates  data DistAny k = DA
 931   --            ax7 k :: Dist k (Any k) ~ DistAny k
 932   -- The 'k' comes from kindGeneralizeKinds (Any k)
 933
 934 Note [Quantified kind variables of a family pattern]
 935 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 936 Consider   type family KindFam (p :: k1) (q :: k1)
 937            data T :: Maybe k1 -> k2 -> *
 938            type instance KindFam (a :: Maybe k) b = T a b -> Int
 939 The HsBSig for the family patterns will be ([k], [a])
 940
 941 Then in the family instance we want to
 942   * Bring into scope [ "k" -> k:BOX, "a" -> a:k ]
 943   * Kind-check the RHS
 944   * Quantify the type instance over k and k', as well as a,b, thus
 945        type instance [k, k', a:Maybe k, b:k']
 946                      KindFam (Maybe k) k' a b = T k k' a b -> Int
 947
 948 Notice that in the third step we quantify over all the visibly-mentioned
 949 type variables (a,b), but also over the implicitly mentioned kind varaibles
 950 (k, k').  In this case one is bound explicitly but often there will be
 951 none. The role of the kind signature (a :: Maybe k) is to add a constraint
 952 that 'a' must have that kind, and to bring 'k' into scope.
 953
 954
 955 %************************************************************************
 956 %*                                                                      *
 957                Data types
 958 %*                                                                      *
 959 %************************************************************************
 960
 961 \begin{code}
 962 dataDeclChecks :: Name -> NewOrData -> ThetaType -> [LConDecl Name] -> TcM Bool
 963 dataDeclChecks tc_name new_or_data stupid_theta cons
 964   = do {   -- Check that we don't use GADT syntax in H98 world
 965          gadtSyntax_ok <- xoptM Opt_GADTSyntax
 966        ; let h98_syntax = consUseH98Syntax cons
 967        ; checkTc (gadtSyntax_ok || h98_syntax) (badGadtDecl tc_name)
 968
 969            -- Check that the stupid theta is empty for a GADT-style declaration
 970        ; checkTc (null stupid_theta || h98_syntax) (badStupidTheta tc_name)
 971
 972          -- Check that a newtype has exactly one constructor
 973          -- Do this before checking for empty data decls, so that
 974          -- we don't suggest -XEmptyDataDecls for newtypes
 975        ; checkTc (new_or_data == DataType || isSingleton cons)
 976                 (newtypeConError tc_name (length cons))
 977
 978                 -- Check that there's at least one condecl,
 979          -- or else we're reading an hs-boot file, or -XEmptyDataDecls
 980        ; empty_data_decls <- xoptM Opt_EmptyDataDecls
 981        ; is_boot <- tcIsHsBoot  -- Are we compiling an hs-boot file?
 982        ; checkTc (not (null cons) || empty_data_decls || is_boot)
 983                  (emptyConDeclsErr tc_name)
 984        ; return h98_syntax }
 985
 986
 987 -----------------------------------
 988 consUseH98Syntax :: [LConDecl a] -> Bool
 989 consUseH98Syntax (L _ (ConDecl { con_res = ResTyGADT _ }) : _) = False
 990 consUseH98Syntax _                                             = True
 991                  -- All constructors have same shape
 992
 993 -----------------------------------
 994 tcConDecls :: NewOrData -> TyCon -> ([TyVar], Type)
 995            -> [LConDecl Name] -> TcM [DataCon]
 996 tcConDecls new_or_data rep_tycon res_tmpl cons
 997   = mapM (addLocM (tcConDecl new_or_data rep_tycon res_tmpl)) cons
 998
 999 tcConDecl :: NewOrData
1000           -> TyCon              -- Representation tycon
1001           -> ([TyVar], Type)    -- Return type template (with its template tyvars)
1002           -> ConDecl Name
1003           -> TcM DataCon
1004
1005 tcConDecl new_or_data rep_tycon res_tmpl        -- Data types
1006           (ConDecl { con_name = name
1007                    , con_qvars = hs_tvs, con_cxt = hs_ctxt
1008                    , con_details = hs_details, con_res = hs_res_ty })
1009   = addErrCtxt (dataConCtxt name) $
1010     do { traceTc "tcConDecl 1" (ppr name)
1011        ; (tvs, ctxt, arg_tys, res_ty, is_infix, field_lbls, stricts)
1012            <- tcHsTyVarBndrs hs_tvs $ \ tvs ->
1013               do { ctxt    <- tcHsContext hs_ctxt
1014                  ; details <- tcConArgs new_or_data hs_details
1015                  ; res_ty  <- tcConRes hs_res_ty
1016                  ; let (is_infix, field_lbls, btys) = details
1017                        (arg_tys, stricts)           = unzip btys
1018                  ; return (tvs, ctxt, arg_tys, res_ty, is_infix, field_lbls, stricts) }
1019
1020        ; let pretend_res_ty = case res_ty of
1021                                 ResTyH98     -> unitTy
1022                                 ResTyGADT ty -> ty
1023              pretend_con_ty = mkSigmaTy tvs ctxt (mkFunTys arg_tys pretend_res_ty)
1024                 -- This pretend_con_ty stuff is just a convenient way to get the
1025                 -- free kind variables of the type, for kindGeneralize to work on
1026
1027              -- Generalise the kind variables (returning quantifed TcKindVars)
1028              -- and quantify the type variables (substiting their kinds)
1029        ; kvs <- kindGeneralize (tyVarsOfType pretend_con_ty) (map getName tvs)
1030        ; tvs <- zonkQuantifiedTyVars tvs
1031
1032              -- Zonk to Types
1033        ; (ze, qtkvs) <- zonkTyBndrsX emptyZonkEnv (kvs ++ tvs)
1034        ; arg_tys <- zonkTcTypeToTypes ze arg_tys
1035        ; ctxt    <- zonkTcTypeToTypes ze ctxt
1036        ; res_ty  <- case res_ty of
1037                       ResTyH98     -> return ResTyH98
1038                       ResTyGADT ty -> ResTyGADT <$> zonkTcTypeToType ze ty
1039
1040        ; let (univ_tvs, ex_tvs, eq_preds, res_ty')
1041                 = rejigConRes res_tmpl qtkvs res_ty
1042
1043        ; traceTc "tcConDecl 3" (ppr name)
1044        ; fam_envs <- tcGetFamInstEnvs
1045        ; buildDataCon fam_envs (unLoc name) is_infix
1046                       stricts field_lbls
1047                       univ_tvs ex_tvs eq_preds ctxt arg_tys
1048                       res_ty' rep_tycon
1049                 -- NB:  we put data_tc, the type constructor gotten from the
1050                 --      constructor type signature into the data constructor;
1051                 --      that way checkValidDataCon can complain if it's wrong.
1052        }
1053
1054 tcConArgs :: NewOrData -> HsConDeclDetails Name -> TcM (Bool, [Name], [(TcType, HsBang)])
1055 tcConArgs new_or_data (PrefixCon btys)
1056   = do { btys' <- mapM (tcConArg new_or_data) btys
1057        ; return (False, [], btys') }
1058 tcConArgs new_or_data (InfixCon bty1 bty2)
1059   = do { bty1' <- tcConArg new_or_data bty1
1060        ; bty2' <- tcConArg new_or_data bty2
1061        ; return (True, [], [bty1', bty2']) }
1062 tcConArgs new_or_data (RecCon fields)
1063   = do { btys' <- mapM (tcConArg new_or_data) btys
1064        ; return (False, field_names, btys') }
1065   where
1066     field_names = map (unLoc . cd_fld_name) fields
1067     btys        = map cd_fld_type fields
1068
1069 tcConArg :: NewOrData -> LHsType Name -> TcM (TcType, HsBang)
1070 tcConArg new_or_data bty
1071   = do  { traceTc "tcConArg 1" (ppr bty)
1072         ; arg_ty <- tcHsConArgType new_or_data bty
1073         ; traceTc "tcConArg 2" (ppr bty)
1074         ; return (arg_ty, getBangStrictness bty) }
1075
1076 tcConRes :: ResType (LHsType Name) -> TcM (ResType Type)
1077 tcConRes ResTyH98           = return ResTyH98
1078 tcConRes (ResTyGADT res_ty) = do { res_ty' <- tcHsLiftedType res_ty
1079                                  ; return (ResTyGADT res_ty') }
1080
1081 -- Example
1082 --   data instance T (b,c) where
1083 --      TI :: forall e. e -> T (e,e)
1084 --
1085 -- The representation tycon looks like this:
1086 --   data :R7T b c where
1087 --      TI :: forall b1 c1. (b1 ~ c1) => b1 -> :R7T b1 c1
1088 -- In this case orig_res_ty = T (e,e)
1089
1090 rejigConRes :: ([TyVar], Type)  -- Template for result type; e.g.
1091                                 -- data instance T [a] b c = ...
1092                                 --      gives template ([a,b,c], T [a] b c)
1093              -> [TyVar]         -- where MkT :: forall x y z. ...
1094              -> ResType Type
1095              -> ([TyVar],               -- Universal
1096                  [TyVar],               -- Existential (distinct OccNames from univs)
1097                  [(TyVar,Type)],        -- Equality predicates
1098                  Type)          -- Typechecked return type
1099         -- We don't check that the TyCon given in the ResTy is
1100         -- the same as the parent tycon, because we are in the middle
1101         -- of a recursive knot; so it's postponed until checkValidDataCon
1102
1103 rejigConRes (tmpl_tvs, res_ty) dc_tvs ResTyH98
1104   = (tmpl_tvs, dc_tvs, [], res_ty)
1105         -- In H98 syntax the dc_tvs are the existential ones
1106         --      data T a b c = forall d e. MkT ...
1107         -- The {a,b,c} are tc_tvs, and {d,e} are dc_tvs
1108
1109 rejigConRes (tmpl_tvs, res_tmpl) dc_tvs (ResTyGADT res_ty)
1110         -- E.g.  data T [a] b c where
1111         --         MkT :: forall x y z. T [(x,y)] z z
1112         -- Then we generate
1113         --      Univ tyvars     Eq-spec
1114         --          a              a~(x,y)
1115         --          b              b~z
1116         --          z
1117         -- Existentials are the leftover type vars: [x,y]
1118         -- So we return ([a,b,z], [x,y], [a~(x,y),b~z], T [(x,y)] z z)
1119   = (univ_tvs, ex_tvs, eq_spec, res_ty)
1120   where
1121     Just subst = tcMatchTy (mkVarSet tmpl_tvs) res_tmpl res_ty
1122                 -- This 'Just' pattern is sure to match, because if not
1123                 -- checkValidDataCon will complain first. The 'subst'
1124                 -- should not be looked at until after checkValidDataCon
1125                 -- We can't check eagerly because we are in a "knot" in
1126                 -- which 'tycon' is not yet fully defined
1127
1128                 -- /Lazily/ figure out the univ_tvs etc
1129                 -- Each univ_tv is either a dc_tv or a tmpl_tv
1130     (univ_tvs, eq_spec) = foldr choose ([], []) tmpl_tvs
1131     choose tmpl (univs, eqs)
1132       | Just ty <- lookupTyVar subst tmpl
1133       = case tcGetTyVar_maybe ty of
1134           Just tv | not (tv `elem` univs)
1135             -> (tv:univs,   eqs)
1136           _other  -> (new_tmpl:univs, (new_tmpl,ty):eqs)
1137                      where  -- see Note [Substitution in template variables kinds]
1138                        new_tmpl = updateTyVarKind (substTy subst) tmpl
1139       | otherwise = pprPanic "tcResultType" (ppr res_ty)
1140     ex_tvs = dc_tvs `minusList` univ_tvs
1141 \end{code}
1142
1143 Note [Substitution in template variables kinds]
1144 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1145
1146 data List a = Nil | Cons a (List a)
1147 data SList s as where
1148   SNil :: SList s Nil
1149
1150 We call tcResultType with
1151   tmpl_tvs = [(k :: BOX), (s :: k -> *), (as :: List k)]
1152   res_tmpl = SList k s as
1153   res_ty = ResTyGADT (SList k1 (s1 :: k1 -> *) (Nil k1))
1154
1155 We get subst:
1156   k -> k1
1157   s -> s1
1158   as -> Nil k1
1159
1160 Now we want to find out the universal variables and the equivalences
1161 between some of them and types (GADT).
1162
1163 In this example, k and s are mapped to exactly variables which are not
1164 already present in the universal set, so we just add them without any
1165 coercion.
1166
1167 But 'as' is mapped to 'Nil k1', so we add 'as' to the universal set,
1168 and add the equivalence with 'Nil k1' in 'eqs'.
1169
1170 The problem is that with kind polymorphism, as's kind may now contain
1171 kind variables, and we have to apply the template substitution to it,
1172 which is why we create new_tmpl.
1173
1174 The template substitution only maps kind variables to kind variables,
1175 since GADTs are not kind indexed.
1176
1177 %************************************************************************
1178 %*                                                                      *
1179                 Validity checking
1180 %*                                                                      *
1181 %************************************************************************
1182
1183 Validity checking is done once the mutually-recursive knot has been
1184 tied, so we can look at things freely.
1185
1186 \begin{code}
1187 checkClassCycleErrs :: Class -> TcM ()
1188 checkClassCycleErrs cls
1189   = unless (null cls_cycles) $ mapM_ recClsErr cls_cycles
1190   where cls_cycles = calcClassCycles cls
1191
1192 checkValidDecl :: SDoc -- the context for error checking
1193                -> Located Name -> TcM ()
1194 checkValidDecl ctxt lname
1195   = addErrCtxt ctxt $
1196     do  { traceTc "Validity of 1" (ppr lname)
1197         ; env <- getGblEnv
1198         ; traceTc "Validity of 1a" (ppr (tcg_type_env env))
1199         ; thing <- tcLookupLocatedGlobal lname
1200         ; traceTc "Validity of 2" (ppr lname)
1201         ; traceTc "Validity of" (ppr thing)
1202         ; case thing of
1203             ATyCon tc -> do
1204                 traceTc "  of kind" (ppr (tyConKind tc))
1205                 checkValidTyCon tc
1206             AnId _    -> return ()  -- Generic default methods are checked
1207                                     -- with their parent class
1208             _         -> panic "checkValidTyCl"
1209         ; traceTc "Done validity of" (ppr thing)
1210         }
1211
1212 checkValidTyCl :: TyClDecl Name -> TcM ()
1213 checkValidTyCl decl
1214   = do { checkValidDecl (tcMkDeclCtxt decl) (tyClDeclLName decl)
1215        ; case decl of
1216            ClassDecl { tcdATs = ats } ->
1217              mapM_ (checkValidFamDecl . unLoc) ats
1218            _ -> return () }
1219
1220 checkValidFamDecl :: FamilyDecl Name -> TcM ()
1221 checkValidFamDecl (FamilyDecl { fdLName = lname, fdFlavour = flav })
1222   = checkValidDecl (hsep [ptext (sLit "In the"), ppr flav,
1223                           ptext (sLit "declaration for"), quotes (ppr lname)])
1224                    lname
1225
1226 -------------------------
1227 -- For data types declared with record syntax, we require
1228 -- that each constructor that has a field 'f'
1229 --      (a) has the same result type
1230 --      (b) has the same type for 'f'
1231 -- module alpha conversion of the quantified type variables
1232 -- of the constructor.
1233 --
1234 -- Note that we allow existentials to match because the
1235 -- fields can never meet. E.g
1236 --      data T where
1237 --        T1 { f1 :: b, f2 :: a, f3 ::Int } :: T
1238 --        T2 { f1 :: c, f2 :: c, f3 ::Int } :: T
1239 -- Here we do not complain about f1,f2 because they are existential
1240
1241 checkValidTyCon :: TyCon -> TcM ()
1242 checkValidTyCon tc
1243   | Just cl <- tyConClass_maybe tc
1244   = checkValidClass cl
1245
1246   | Just syn_rhs <- synTyConRhs_maybe tc
1247   = case syn_rhs of
1248       SynFamilyTyCon {} -> return ()
1249       SynonymTyCon ty   -> checkValidType syn_ctxt ty
1250
1251   | otherwise
1252   = do { -- Check the context on the data decl
1253        ; traceTc "cvtc1" (ppr tc)
1254        ; checkValidTheta (DataTyCtxt name) (tyConStupidTheta tc)
1255
1256         -- Check arg types of data constructors
1257        ; traceTc "cvtc2" (ppr tc)
1258
1259        ; dflags          <- getDynFlags
1260        ; existential_ok  <- xoptM Opt_ExistentialQuantification
1261        ; gadt_ok         <- xoptM Opt_GADTs
1262        ; let ex_ok = existential_ok || gadt_ok  -- Data cons can have existential context
1263        ; mapM_ (checkValidDataCon dflags ex_ok tc) data_cons
1264
1265         -- Check that fields with the same name share a type
1266        ; mapM_ check_fields groups }
1267
1268   where
1269     syn_ctxt  = TySynCtxt name
1270     name      = tyConName tc
1271     data_cons = tyConDataCons tc
1272
1273     groups = equivClasses cmp_fld (concatMap get_fields data_cons)
1274     cmp_fld (f1,_) (f2,_) = f1 `compare` f2
1275     get_fields con = dataConFieldLabels con `zip` repeat con
1276         -- dataConFieldLabels may return the empty list, which is fine
1277
1278     -- See Note [GADT record selectors] in MkId.lhs
1279     -- We must check (a) that the named field has the same
1280     --                   type in each constructor
1281     --               (b) that those constructors have the same result type
1282     --
1283     -- However, the constructors may have differently named type variable
1284     -- and (worse) we don't know how the correspond to each other.  E.g.
1285     --     C1 :: forall a b. { f :: a, g :: b } -> T a b
1286     --     C2 :: forall d c. { f :: c, g :: c } -> T c d
1287     --
1288     -- So what we do is to ust Unify.tcMatchTys to compare the first candidate's
1289     -- result type against other candidates' types BOTH WAYS ROUND.
1290     -- If they magically agrees, take the substitution and
1291     -- apply them to the latter ones, and see if they match perfectly.
1292     check_fields ((label, con1) : other_fields)
1293         -- These fields all have the same name, but are from
1294         -- different constructors in the data type
1295         = recoverM (return ()) $ mapM_ checkOne other_fields
1296                 -- Check that all the fields in the group have the same type
1297                 -- NB: this check assumes that all the constructors of a given
1298                 -- data type use the same type variables
1299         where
1300         (tvs1, _, _, res1) = dataConSig con1
1301         ts1 = mkVarSet tvs1
1302         fty1 = dataConFieldType con1 label
1303
1304         checkOne (_, con2)    -- Do it bothways to ensure they are structurally identical
1305             = do { checkFieldCompat label con1 con2 ts1 res1 res2 fty1 fty2
1306                  ; checkFieldCompat label con2 con1 ts2 res2 res1 fty2 fty1 }
1307             where
1308                 (tvs2, _, _, res2) = dataConSig con2
1309                 ts2 = mkVarSet tvs2
1310                 fty2 = dataConFieldType con2 label
1311     check_fields [] = panic "checkValidTyCon/check_fields []"
1312
1313 checkFieldCompat :: Name -> DataCon -> DataCon -> TyVarSet
1314                  -> Type -> Type -> Type -> Type -> TcM ()
1315 checkFieldCompat fld con1 con2 tvs1 res1 res2 fty1 fty2
1316   = do  { checkTc (isJust mb_subst1) (resultTypeMisMatch fld con1 con2)
1317         ; checkTc (isJust mb_subst2) (fieldTypeMisMatch fld con1 con2) }
1318   where
1319     mb_subst1 = tcMatchTy tvs1 res1 res2
1320     mb_subst2 = tcMatchTyX tvs1 (expectJust "checkFieldCompat" mb_subst1) fty1 fty2
1321
1322 -------------------------------
1323 checkValidDataCon :: DynFlags -> Bool -> TyCon -> DataCon -> TcM ()
1324 checkValidDataCon dflags existential_ok tc con
1325   = setSrcSpan (srcLocSpan (getSrcLoc con))     $
1326     addErrCtxt (dataConCtxt con)                $
1327     do  { traceTc "Validity of data con" (ppr con)
1328         ; let tc_tvs = tyConTyVars tc
1329               res_ty_tmpl = mkFamilyTyConApp tc (mkTyVarTys tc_tvs)
1330               actual_res_ty = dataConOrigResTy con
1331         ; traceTc "checkValidDataCon" (ppr con $$ ppr tc $$ ppr tc_tvs $$ ppr res_ty_tmpl)
1332         ; checkTc (isJust (tcMatchTy (mkVarSet tc_tvs)
1333                                 res_ty_tmpl
1334                                 actual_res_ty))
1335                   (badDataConTyCon con res_ty_tmpl actual_res_ty)
1336              -- IA0_TODO: we should also check that kind variables
1337              -- are only instantiated with kind variables
1338         ; checkValidMonoType (dataConOrigResTy con)
1339                 -- Disallow MkT :: T (forall a. a->a)
1340                 -- Reason: it's really the argument of an equality constraint
1341         ; checkValidType ctxt (dataConUserType con)
1342         ; when (isNewTyCon tc) (checkNewDataCon con)
1343
1344         ; mapM_ check_bang (zip3 (dataConStrictMarks con) (dataConRepBangs con) [1..])
1345
1346         ; checkTc (existential_ok || isVanillaDataCon con)
1347                   (badExistential con)
1348
1349         ; checkTc (not (any (isKindVar . fst) (dataConEqSpec con)))
1350                   (badGadtKindCon con)
1351
1352         ; traceTc "Done validity of data con" (ppr con <+> ppr (dataConRepType con))
1353     }
1354   where
1355     ctxt = ConArgCtxt (dataConName con)
1356     check_bang (HsUserBang (Just want_unpack) has_bang, rep_bang, n)
1357       | want_unpack, not has_bang
1358       = addWarnTc (bad_bang n (ptext (sLit "UNPACK pragma lacks '!'")))
1359       | want_unpack
1360       , case rep_bang of { HsUnpack {} -> False; _ -> True }
1361       , not (gopt Opt_OmitInterfacePragmas dflags)
1362            -- If not optimising, se don't unpack, so don't complain!
1363            -- See MkId.dataConArgRep, the (HsBang True) case
1364       = addWarnTc (bad_bang n (ptext (sLit "Ignoring unusable UNPACK pragma")))
1365
1366     check_bang _
1367       = return ()
1368
1369     bad_bang n herald
1370       = hang herald 2 (ptext (sLit "on the") <+> speakNth n
1371                        <+> ptext (sLit "argument of") <+> quotes (ppr con))
1372 -------------------------------
1373 checkNewDataCon :: DataCon -> TcM ()
1374 -- Checks for the data constructor of a newtype
1375 checkNewDataCon con
1376   = do  { checkTc (isSingleton arg_tys) (newtypeFieldErr con (length arg_tys))
1377                 -- One argument
1378         ; checkTc (null eq_spec) (newtypePredError con)
1379                 -- Return type is (T a b c)
1380         ; checkTc (null ex_tvs && null theta) (newtypeExError con)
1381                 -- No existentials
1382         ; checkTc (not (any isBanged (dataConStrictMarks con)))
1383                   (newtypeStrictError con)
1384                 -- No strictness
1385     }
1386   where
1387     (_univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig con
1388
1389 -------------------------------
1390 checkValidClass :: Class -> TcM ()
1391 checkValidClass cls
1392   = do  { constrained_class_methods <- xoptM Opt_ConstrainedClassMethods
1393         ; multi_param_type_classes <- xoptM Opt_MultiParamTypeClasses
1394         ; nullary_type_classes <- xoptM Opt_NullaryTypeClasses
1395         ; fundep_classes <- xoptM Opt_FunctionalDependencies
1396
1397         -- Check that the class is unary, unless multiparameter or
1398         -- nullary type classes are enabled
1399         ; checkTc (nullary_type_classes || notNull tyvars) (nullaryClassErr cls)
1400         ; checkTc (multi_param_type_classes || arity <= 1) (classArityErr cls)
1401         ; checkTc (fundep_classes || null fundeps) (classFunDepsErr cls)
1402
1403         -- Check the super-classes
1404         ; checkValidTheta (ClassSCCtxt (className cls)) theta
1405
1406           -- Now check for cyclic superclasses
1407         ; checkClassCycleErrs cls
1408
1409         -- Check the class operations
1410         ; mapM_ (check_op constrained_class_methods) op_stuff
1411
1412         -- Check the associated type defaults are well-formed and instantiated
1413         ; mapM_ check_at_defs at_stuff  }
1414   where
1415     (tyvars, fundeps, theta, _, at_stuff, op_stuff) = classExtraBigSig cls
1416     arity = count isTypeVar tyvars    -- Ignore kind variables
1417
1418     check_op constrained_class_methods (sel_id, dm)
1419       = addErrCtxt (classOpCtxt sel_id tau) $ do
1420         { checkValidTheta ctxt (tail theta)
1421                 -- The 'tail' removes the initial (C a) from the
1422                 -- class itself, leaving just the method type
1423
1424         ; traceTc "class op type" (ppr op_ty <+> ppr tau)
1425         ; checkValidType ctxt tau
1426
1427                 -- Check that the type mentions at least one of
1428                 -- the class type variables...or at least one reachable
1429                 -- from one of the class variables.  Example: tc223
1430                 --   class Error e => Game b mv e | b -> mv e where
1431                 --      newBoard :: MonadState b m => m ()
1432                 -- Here, MonadState has a fundep m->b, so newBoard is fine
1433                 -- The check is disabled for nullary type classes,
1434                 -- since there is no possible ambiguity
1435         ; let grown_tyvars = growThetaTyVars theta (mkVarSet tyvars)
1436         ; checkTc (arity == 0 || tyVarsOfType tau `intersectsVarSet` grown_tyvars)
1437                   (noClassTyVarErr cls sel_id)
1438
1439         ; case dm of
1440             GenDefMeth dm_name -> do { dm_id <- tcLookupId dm_name
1441                                      ; checkValidType (FunSigCtxt op_name) (idType dm_id) }
1442             _                  -> return ()
1443         }
1444         where
1445           ctxt    = FunSigCtxt op_name
1446           op_name = idName sel_id
1447           op_ty   = idType sel_id
1448           (_,theta1,tau1) = tcSplitSigmaTy op_ty
1449           (_,theta2,tau2)  = tcSplitSigmaTy tau1
1450           (theta,tau) | constrained_class_methods = (theta1 ++ theta2, tau2)
1451                       | otherwise = (theta1, mkPhiTy (tail theta1) tau1)
1452                 -- Ugh!  The function might have a type like
1453                 --      op :: forall a. C a => forall b. (Eq b, Eq a) => tau2
1454                 -- With -XConstrainedClassMethods, we want to allow this, even though the inner
1455                 -- forall has an (Eq a) constraint.  Whereas in general, each constraint
1456                 -- in the context of a for-all must mention at least one quantified
1457                 -- type variable.  What a mess!
1458
1459     check_at_defs (fam_tc, defs)
1460       = tcAddDefaultAssocDeclCtxt (tyConName fam_tc) $
1461         mapM_ (checkValidTyFamInst mb_clsinfo fam_tc) defs
1462
1463     mb_clsinfo = Just (cls, mkVarEnv [ (tv, mkTyVarTy tv) | tv <- tyvars ])
1464
1465 checkFamFlag :: Name -> TcM ()
1466 -- Check that we don't use families without -XTypeFamilies
1467 -- The parser won't even parse them, but I suppose a GHC API
1468 -- client might have a go!
1469 checkFamFlag tc_name
1470   = do { idx_tys <- xoptM Opt_TypeFamilies
1471        ; checkTc idx_tys err_msg }
1472   where
1473     err_msg = hang (ptext (sLit "Illegal family declaraion for") <+> quotes (ppr tc_name))
1474                  2 (ptext (sLit "Use -XTypeFamilies to allow indexed type families"))
1475 \end{code}
1476
1477
1478 %************************************************************************
1479 %*                                                                      *
1480                 Building record selectors
1481 %*                                                                      *
1482 %************************************************************************
1483
1484 \begin{code}
1485 mkDefaultMethodIds :: [TyThing] -> [Id]
1486 -- See Note [Default method Ids and Template Haskell]
1487 mkDefaultMethodIds things
1488   = [ mkExportedLocalId dm_name (idType sel_id)
1489     | ATyCon tc <- things
1490     , Just cls <- [tyConClass_maybe tc]
1491     , (sel_id, DefMeth dm_name) <- classOpItems cls ]
1492 \end{code}
1493
1494 Note [Default method Ids and Template Haskell]
1495 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1496 Consider this (Trac #4169):
1497    class Numeric a where
1498      fromIntegerNum :: a
1499      fromIntegerNum = ...
1500
1501    ast :: Q [Dec]
1502    ast = [d| instance Numeric Int |]
1503
1504 When we typecheck 'ast' we have done the first pass over the class decl
1505 (in tcTyClDecls), but we have not yet typechecked the default-method
1506 declarations (because they can mention value declarations).  So we
1507 must bring the default method Ids into scope first (so they can be seen
1508 when typechecking the [d| .. |] quote, and typecheck them later.
1509
1510 \begin{code}
1511 mkRecSelBinds :: [TyThing] -> HsValBinds Name
1512 -- NB We produce *un-typechecked* bindings, rather like 'deriving'
1513 --    This makes life easier, because the later type checking will add
1514 --    all necessary type abstractions and applications
1515 mkRecSelBinds tycons
1516   = ValBindsOut [(NonRecursive, b) | b <- binds] sigs
1517   where
1518     (sigs, binds) = unzip rec_sels
1519     rec_sels = map mkRecSelBind [ (tc,fld)
1520                                 | ATyCon tc <- tycons
1521                                 , fld <- tyConFields tc ]
1522
1523 mkRecSelBind :: (TyCon, FieldLabel) -> (LSig Name, LHsBinds Name)
1524 mkRecSelBind (tycon, sel_name)
1525   = (L loc (IdSig sel_id), unitBag (L loc sel_bind))
1526   where
1527     loc    = getSrcSpan sel_name
1528     sel_id = Var.mkExportedLocalVar rec_details sel_name
1529                                     sel_ty vanillaIdInfo
1530     rec_details = RecSelId { sel_tycon = tycon, sel_naughty = is_naughty }
1531
1532     -- Find a representative constructor, con1
1533     all_cons     = tyConDataCons tycon
1534     cons_w_field = [ con | con <- all_cons
1535                    , sel_name `elem` dataConFieldLabels con ]
1536     con1 = ASSERT( not (null cons_w_field) ) head cons_w_field
1537
1538     -- Selector type; Note [Polymorphic selectors]
1539     field_ty   = dataConFieldType con1 sel_name
1540     data_ty    = dataConOrigResTy con1
1541     data_tvs   = tyVarsOfType data_ty
1542     is_naughty = not (tyVarsOfType field_ty `subVarSet` data_tvs)
1543     (field_tvs, field_theta, field_tau) = tcSplitSigmaTy field_ty
1544     sel_ty | is_naughty = unitTy  -- See Note [Naughty record selectors]
1545            | otherwise  = mkForAllTys (varSetElemsKvsFirst $
1546                                        data_tvs `extendVarSetList` field_tvs) $
1547                           mkPhiTy (dataConStupidTheta con1) $   -- Urgh!
1548                           mkPhiTy field_theta               $   -- Urgh!
1549                           mkFunTy data_ty field_tau
1550
1551     -- Make the binding: sel (C2 { fld = x }) = x
1552     --                   sel (C7 { fld = x }) = x
1553     --    where cons_w_field = [C2,C7]
1554     sel_bind | is_naughty = mkTopFunBind sel_lname [mkSimpleMatch [] unit_rhs]
1555              | otherwise  = mkTopFunBind sel_lname (map mk_match cons_w_field ++ deflt)
1556     mk_match con = mkSimpleMatch [L loc (mk_sel_pat con)]
1557                                  (L loc (HsVar field_var))
1558     mk_sel_pat con = ConPatIn (L loc (getName con)) (RecCon rec_fields)
1559     rec_fields = HsRecFields { rec_flds = [rec_field], rec_dotdot = Nothing }
1560     rec_field  = HsRecField { hsRecFieldId = sel_lname
1561                             , hsRecFieldArg = L loc (VarPat field_var)
1562                             , hsRecPun = False }
1563     sel_lname = L loc sel_name
1564     field_var = mkInternalName (mkBuiltinUnique 1) (getOccName sel_name) loc
1565
1566     -- Add catch-all default case unless the case is exhaustive
1567     -- We do this explicitly so that we get a nice error message that
1568     -- mentions this particular record selector
1569     deflt | all dealt_with all_cons = []
1570           | otherwise = [mkSimpleMatch [L loc (WildPat placeHolderType)]
1571                             (mkHsApp (L loc (HsVar (getName rEC_SEL_ERROR_ID)))
1572                                      (L loc (HsLit msg_lit)))]
1573
1574         -- Do not add a default case unless there are unmatched
1575         -- constructors.  We must take account of GADTs, else we
1576         -- get overlap warning messages from the pattern-match checker
1577         -- NB: we need to pass type args for the *representation* TyCon
1578         --     to dataConCannotMatch, hence the calculation of inst_tys
1579         --     This matters in data families
1580         --              data instance T Int a where
1581         --                 A :: { fld :: Int } -> T Int Bool
1582         --                 B :: { fld :: Int } -> T Int Char
1583     dealt_with con = con `elem` cons_w_field || dataConCannotMatch inst_tys con
1584     inst_tys = substTyVars (mkTopTvSubst (dataConEqSpec con1)) (dataConUnivTyVars con1)
1585
1586     unit_rhs = mkLHsTupleExpr []
1587     msg_lit = HsStringPrim $ unsafeMkByteString $
1588               occNameString (getOccName sel_name)
1589
1590 ---------------
1591 tyConFields :: TyCon -> [FieldLabel]
1592 tyConFields tc
1593   | isAlgTyCon tc = nub (concatMap dataConFieldLabels (tyConDataCons tc))
1594   | otherwise     = []
1595 \end{code}
1596
1597 Note [Polymorphic selectors]
1598 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1599 When a record has a polymorphic field, we pull the foralls out to the front.
1600    data T = MkT { f :: forall a. [a] -> a }
1601 Then f :: forall a. T -> [a] -> a
1602 NOT  f :: T -> forall a. [a] -> a
1603
1604 This is horrid.  It's only needed in deeply obscure cases, which I hate.
1605 The only case I know is test tc163, which is worth looking at.  It's far
1606 from clear that this test should succeed at all!
1607
1608 Note [Naughty record selectors]
1609 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1610 A "naughty" field is one for which we can't define a record
1611 selector, because an existential type variable would escape.  For example:
1612         data T = forall a. MkT { x,y::a }
1613 We obviously can't define
1614         x (MkT v _) = v
1615 Nevertheless we *do* put a RecSelId into the type environment
1616 so that if the user tries to use 'x' as a selector we can bleat
1617 helpfully, rather than saying unhelpfully that 'x' is not in scope.
1618 Hence the sel_naughty flag, to identify record selectors that don't really exist.
1619
1620 In general, a field is "naughty" if its type mentions a type variable that
1621 isn't in the result type of the constructor.  Note that this *allows*
1622 GADT record selectors (Note [GADT record selectors]) whose types may look
1623 like     sel :: T [a] -> a
1624
1625 For naughty selectors we make a dummy binding
1626    sel = ()
1627 for naughty selectors, so that the later type-check will add them to the
1628 environment, and they'll be exported.  The function is never called, because
1629 the tyepchecker spots the sel_naughty field.
1630
1631 Note [GADT record selectors]
1632 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1633 For GADTs, we require that all constructors with a common field 'f' have the same
1634 result type (modulo alpha conversion).  [Checked in TcTyClsDecls.checkValidTyCon]
1635 E.g.
1636         data T where
1637           T1 { f :: Maybe a } :: T [a]
1638           T2 { f :: Maybe a, y :: b  } :: T [a]
1639           T3 :: T Int
1640
1641 and now the selector takes that result type as its argument:
1642    f :: forall a. T [a] -> Maybe a
1643
1644 Details: the "real" types of T1,T2 are:
1645    T1 :: forall r a.   (r~[a]) => a -> T r
1646    T2 :: forall r a b. (r~[a]) => a -> b -> T r
1647
1648 So the selector loooks like this:
1649    f :: forall a. T [a] -> Maybe a
1650    f (a:*) (t:T [a])
1651      = case t of
1652          T1 c   (g:[a]~[c]) (v:Maybe c)       -> v `cast` Maybe (right (sym g))
1653          T2 c d (g:[a]~[c]) (v:Maybe c) (w:d) -> v `cast` Maybe (right (sym g))
1654          T3 -> error "T3 does not have field f"
1655
1656 Note the forall'd tyvars of the selector are just the free tyvars
1657 of the result type; there may be other tyvars in the constructor's
1658 type (e.g. 'b' in T2).
1659
1660 Note the need for casts in the result!
1661
1662 Note [Selector running example]
1663 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1664 It's OK to combine GADTs and type families.  Here's a running example:
1665
1666         data instance T [a] where
1667           T1 { fld :: b } :: T [Maybe b]
1668
1669 The representation type looks like this
1670         data :R7T a where
1671           T1 { fld :: b } :: :R7T (Maybe b)
1672
1673 and there's coercion from the family type to the representation type
1674         :CoR7T a :: T [a] ~ :R7T a
1675
1676 The selector we want for fld looks like this:
1677
1678         fld :: forall b. T [Maybe b] -> b
1679         fld = /\b. \(d::T [Maybe b]).
1680               case d `cast` :CoR7T (Maybe b) of
1681                 T1 (x::b) -> x
1682
1683 The scrutinee of the case has type :R7T (Maybe b), which can be
1684 gotten by appying the eq_spec to the univ_tvs of the data con.
1685
1686 %************************************************************************
1687 %*                                                                      *
1688                 Error messages
1689 %*                                                                      *
1690 %************************************************************************
1691
1692 \begin{code}
1693 tcAddDefaultAssocDeclCtxt :: Name -> TcM a -> TcM a
1694 tcAddDefaultAssocDeclCtxt name thing_inside
1695   = addErrCtxt ctxt thing_inside
1696   where
1697      ctxt = hsep [ptext (sLit "In the type synonym instance default declaration for"),
1698                   quotes (ppr name)]
1699
1700 tcAddTyFamInstCtxt :: TyFamInstDecl Name -> TcM a -> TcM a
1701 tcAddTyFamInstCtxt decl
1702   | [_] <- tfid_eqns decl
1703   = tcAddFamInstCtxt (ptext (sLit "type instance")) (tyFamInstDeclName decl)
1704   | otherwise
1705   = tcAddFamInstCtxt (ptext (sLit "type instance group")) (tyFamInstDeclName decl)
1706
1707 tcAddDataFamInstCtxt :: DataFamInstDecl Name -> TcM a -> TcM a
1708 tcAddDataFamInstCtxt decl
1709   = tcAddFamInstCtxt (pprDataFamInstFlavour decl <+> ptext (sLit "instance"))
1710                      (unLoc (dfid_tycon decl))
1711
1712 tcAddFamInstCtxt :: SDoc -> Name -> TcM a -> TcM a
1713 tcAddFamInstCtxt flavour tycon thing_inside
1714   = addErrCtxt ctxt thing_inside
1715   where
1716      ctxt = hsep [ptext (sLit "In the") <+> flavour
1717                   <+> ptext (sLit "declaration for"),
1718                   quotes (ppr tycon)]
1719
1720 resultTypeMisMatch :: Name -> DataCon -> DataCon -> SDoc
1721 resultTypeMisMatch field_name con1 con2
1722   = vcat [sep [ptext (sLit "Constructors") <+> ppr con1 <+> ptext (sLit "and") <+> ppr con2,
1723                 ptext (sLit "have a common field") <+> quotes (ppr field_name) <> comma],
1724           nest 2 $ ptext (sLit "but have different result types")]
1725
1726 fieldTypeMisMatch :: Name -> DataCon -> DataCon -> SDoc
1727 fieldTypeMisMatch field_name con1 con2
1728   = sep [ptext (sLit "Constructors") <+> ppr con1 <+> ptext (sLit "and") <+> ppr con2,
1729          ptext (sLit "give different types for field"), quotes (ppr field_name)]
1730
1731 dataConCtxt :: Outputable a => a -> SDoc
1732 dataConCtxt con = ptext (sLit "In the definition of data constructor") <+> quotes (ppr con)
1733
1734 classOpCtxt :: Var -> Type -> SDoc
1735 classOpCtxt sel_id tau = sep [ptext (sLit "When checking the class method:"),
1736                               nest 2 (pprPrefixOcc sel_id <+> dcolon <+> ppr tau)]
1737
1738 nullaryClassErr :: Class -> SDoc
1739 nullaryClassErr cls
1740   = vcat [ptext (sLit "No parameters for class") <+> quotes (ppr cls),
1741           parens (ptext (sLit "Use -XNullaryTypeClasses to allow no-parameter classes"))]
1742
1743 classArityErr :: Class -> SDoc
1744 classArityErr cls
1745   = vcat [ptext (sLit "Too many parameters for class") <+> quotes (ppr cls),
1746           parens (ptext (sLit "Use -XMultiParamTypeClasses to allow multi-parameter classes"))]
1747
1748 classFunDepsErr :: Class -> SDoc
1749 classFunDepsErr cls
1750   = vcat [ptext (sLit "Fundeps in class") <+> quotes (ppr cls),
1751           parens (ptext (sLit "Use -XFunctionalDependencies to allow fundeps"))]
1752
1753 noClassTyVarErr :: Class -> Var -> SDoc
1754 noClassTyVarErr clas op
1755   = sep [ptext (sLit "The class method") <+> quotes (ppr op),
1756          ptext (sLit "mentions none of the type variables of the class") <+>
1757                 ppr clas <+> hsep (map ppr (classTyVars clas))]
1758
1759 recSynErr :: [LTyClDecl Name] -> TcRn ()
1760 recSynErr syn_decls
1761   = setSrcSpan (getLoc (head sorted_decls)) $
1762     addErr (sep [ptext (sLit "Cycle in type synonym declarations:"),
1763                  nest 2 (vcat (map ppr_decl sorted_decls))])
1764   where
1765     sorted_decls = sortLocated syn_decls
1766     ppr_decl (L loc decl) = ppr loc <> colon <+> ppr decl
1767
1768 recClsErr :: [TyCon] -> TcRn ()
1769 recClsErr cycles
1770   = addErr (sep [ptext (sLit "Cycle in class declaration (via superclasses):"),
1771                  nest 2 (hsep (intersperse (text "->") (map ppr cycles)))])
1772
1773 badDataConTyCon :: DataCon -> Type -> Type -> SDoc
1774 badDataConTyCon data_con res_ty_tmpl actual_res_ty
1775   = hang (ptext (sLit "Data constructor") <+> quotes (ppr data_con) <+>
1776                 ptext (sLit "returns type") <+> quotes (ppr actual_res_ty))
1777        2 (ptext (sLit "instead of an instance of its parent type") <+> quotes (ppr res_ty_tmpl))
1778
1779 badGadtKindCon :: DataCon -> SDoc
1780 badGadtKindCon data_con
1781   = hang (ptext (sLit "Data constructor") <+> quotes (ppr data_con)
1782           <+> ptext (sLit "cannot be GADT-like in its *kind* arguments"))
1783        2 (ppr data_con <+> dcolon <+> ppr (dataConUserType data_con))
1784
1785 badGadtDecl :: Name -> SDoc
1786 badGadtDecl tc_name
1787   = vcat [ ptext (sLit "Illegal generalised algebraic data declaration for") <+> quotes (ppr tc_name)
1788          , nest 2 (parens $ ptext (sLit "Use -XGADTs to allow GADTs")) ]
1789
1790 badExistential :: DataCon -> SDoc
1791 badExistential con_name
1792   = hang (ptext (sLit "Data constructor") <+> quotes (ppr con_name) <+>
1793                 ptext (sLit "has existential type variables, a context, or a specialised result type"))
1794        2 (parens $ ptext (sLit "Use -XExistentialQuantification or -XGADTs to allow this"))
1795
1796 badStupidTheta :: Name -> SDoc
1797 badStupidTheta tc_name
1798   = ptext (sLit "A data type declared in GADT style cannot have a context:") <+> quotes (ppr tc_name)
1799
1800 newtypeConError :: Name -> Int -> SDoc
1801 newtypeConError tycon n
1802   = sep [ptext (sLit "A newtype must have exactly one constructor,"),
1803          nest 2 $ ptext (sLit "but") <+> quotes (ppr tycon) <+> ptext (sLit "has") <+> speakN n ]
1804
1805 newtypeExError :: DataCon -> SDoc
1806 newtypeExError con
1807   = sep [ptext (sLit "A newtype constructor cannot have an existential context,"),
1808          nest 2 $ ptext (sLit "but") <+> quotes (ppr con) <+> ptext (sLit "does")]
1809
1810 newtypeStrictError :: DataCon -> SDoc
1811 newtypeStrictError con
1812   = sep [ptext (sLit "A newtype constructor cannot have a strictness annotation,"),
1813          nest 2 $ ptext (sLit "but") <+> quotes (ppr con) <+> ptext (sLit "does")]
1814
1815 newtypePredError :: DataCon -> SDoc
1816 newtypePredError con
1817   = sep [ptext (sLit "A newtype constructor must have a return type of form T a1 ... an"),
1818          nest 2 $ ptext (sLit "but") <+> quotes (ppr con) <+> ptext (sLit "does not")]
1819
1820 newtypeFieldErr :: DataCon -> Int -> SDoc
1821 newtypeFieldErr con_name n_flds
1822   = sep [ptext (sLit "The constructor of a newtype must have exactly one field"),
1823          nest 2 $ ptext (sLit "but") <+> quotes (ppr con_name) <+> ptext (sLit "has") <+> speakN n_flds]
1824
1825 badSigTyDecl :: Name -> SDoc
1826 badSigTyDecl tc_name
1827   = vcat [ ptext (sLit "Illegal kind signature") <+>
1828            quotes (ppr tc_name)
1829          , nest 2 (parens $ ptext (sLit "Use -XKindSignatures to allow kind signatures")) ]
1830
1831 emptyConDeclsErr :: Name -> SDoc
1832 emptyConDeclsErr tycon
1833   = sep [quotes (ppr tycon) <+> ptext (sLit "has no constructors"),
1834          nest 2 $ ptext (sLit "(-XEmptyDataDecls permits this)")]
1835
1836 wrongNumberOfParmsErr :: Arity -> SDoc
1837 wrongNumberOfParmsErr exp_arity
1838   = ptext (sLit "Number of parameters must match family declaration; expected")
1839     <+> ppr exp_arity
1840
1841 wrongKindOfFamily :: TyCon -> SDoc
1842 wrongKindOfFamily family
1843   = ptext (sLit "Wrong category of family instance; declaration was for a")
1844     <+> kindOfFamily
1845   where
1846     kindOfFamily | isSynTyCon family = ptext (sLit "type synonym")
1847                  | isAlgTyCon family = ptext (sLit "data type")
1848                  | otherwise = pprPanic "wrongKindOfFamily" (ppr family)
1849
1850 wrongNamesInInstGroup :: Name -> Name -> SDoc
1851 wrongNamesInInstGroup first cur
1852   = ptext (sLit "Mismatched family names in instance group.") $$
1853     ptext (sLit "First name was") <+>
1854     (ppr first) <> (ptext (sLit "; this one is")) <+> (ppr cur)
1855
1856 \end{code}