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 module TcTyClsDecls (
  10         tcTyAndClassDecls, tcFamInstDecl
  11     ) where
  12
  13 #include "HsVersions.h"
  14
  15 import HsSyn
  16 import HsTypes
  17 import BasicTypes
  18 import HscTypes
  19 import BuildTyCl
  20 import TcRnMonad
  21 import TcEnv
  22 import TcTyDecls
  23 import TcClassDcl
  24 import TcHsType
  25 import TcMType
  26 import TcType
  27 import FunDeps
  28 import Type
  29 import Generics
  30 import Class
  31 import TyCon
  32 import DataCon
  33 import Var
  34 import VarSet
  35 import Name
  36 import OccName
  37 import Outputable
  38 import Maybes
  39 import Monad
  40 import Unify
  41 import Util
  42 import SrcLoc
  43 import ListSetOps
  44 import Digraph
  45 import DynFlags
  46
  47 import Data.List        ( partition, elemIndex )
  48 import Control.Monad    ( mplus )
  49 \end{code}
  50
  51
  52 %************************************************************************
  53 %*                                                                      *
  54 \subsection{Type checking for type and class declarations}
  55 %*                                                                      *
  56 %************************************************************************
  57
  58 Dealing with a group
  59 ~~~~~~~~~~~~~~~~~~~~
  60 Consider a mutually-recursive group, binding
  61 a type constructor T and a class C.
  62
  63 Step 1:         getInitialKind
  64         Construct a KindEnv by binding T and C to a kind variable
  65
  66 Step 2:         kcTyClDecl
  67         In that environment, do a kind check
  68
  69 Step 3: Zonk the kinds
  70
  71 Step 4:         buildTyConOrClass
  72         Construct an environment binding T to a TyCon and C to a Class.
  73         a) Their kinds comes from zonking the relevant kind variable
  74         b) Their arity (for synonyms) comes direct from the decl
  75         c) The funcional dependencies come from the decl
  76         d) The rest comes a knot-tied binding of T and C, returned from Step 4
  77         e) The variances of the tycons in the group is calculated from
  78                 the knot-tied stuff
  79
  80 Step 5:         tcTyClDecl1
  81         In this environment, walk over the decls, constructing the TyCons and Classes.
  82         This uses in a strict way items (a)-(c) above, which is why they must
  83         be constructed in Step 4. Feed the results back to Step 4.
  84         For this step, pass the is-recursive flag as the wimp-out flag
  85         to tcTyClDecl1.
  86
  87
  88 Step 6:         Extend environment
  89         We extend the type environment with bindings not only for the TyCons and Classes,
  90         but also for their "implicit Ids" like data constructors and class selectors
  91
  92 Step 7:         checkValidTyCl
  93         For a recursive group only, check all the decls again, just
  94         to check all the side conditions on validity.  We could not
  95         do this before because we were in a mutually recursive knot.
  96
  97 Identification of recursive TyCons
  98 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  99 The knot-tying parameters: @rec_details_list@ is an alist mapping @Name@s to
 100 @TyThing@s.
 101
 102 Identifying a TyCon as recursive serves two purposes
 103
 104 1.  Avoid infinite types.  Non-recursive newtypes are treated as
 105 "transparent", like type synonyms, after the type checker.  If we did
 106 this for all newtypes, we'd get infinite types.  So we figure out for
 107 each newtype whether it is "recursive", and add a coercion if so.  In
 108 effect, we are trying to "cut the loops" by identifying a loop-breaker.
 109
 110 2.  Avoid infinite unboxing.  This is nothing to do with newtypes.
 111 Suppose we have
 112         data T = MkT Int T
 113         f (MkT x t) = f t
 114 Well, this function diverges, but we don't want the strictness analyser
 115 to diverge.  But the strictness analyser will diverge because it looks
 116 deeper and deeper into the structure of T.   (I believe there are
 117 examples where the function does something sane, and the strictness
 118 analyser still diverges, but I can't see one now.)
 119
 120 Now, concerning (1), the FC2 branch currently adds a coercion for ALL
 121 newtypes.  I did this as an experiment, to try to expose cases in which
 122 the coercions got in the way of optimisations.  If it turns out that we
 123 can indeed always use a coercion, then we don't risk recursive types,
 124 and don't need to figure out what the loop breakers are.
 125
 126 For newtype *families* though, we will always have a coercion, so they
 127 are always loop breakers!  So you can easily adjust the current
 128 algorithm by simply treating all newtype families as loop breakers (and
 129 indeed type families).  I think.
 130
 131 \begin{code}
 132 tcTyAndClassDecls :: ModDetails -> [LTyClDecl Name]
 133                    -> TcM TcGblEnv      -- Input env extended by types and classes
 134                                         -- and their implicit Ids,DataCons
 135 tcTyAndClassDecls boot_details allDecls
 136   = do  {       -- Omit instances of indexed types; they are handled together
 137                 -- with the *heads* of class instances
 138         ; let decls = filter (not . isFamInstDecl . unLoc) allDecls
 139
 140                 -- First check for cyclic type synonysm or classes
 141                 -- See notes with checkCycleErrs
 142         ; checkCycleErrs decls
 143         ; mod <- getModule
 144         ; traceTc (text "tcTyAndCl" <+> ppr mod)
 145         ; (syn_tycons, alg_tyclss) <- fixM (\ ~(rec_syn_tycons, rec_alg_tyclss) ->
 146           do    { let { -- Seperate ordinary synonyms from all other type and
 147                         -- class declarations and add all associated type
 148                         -- declarations from type classes.  The latter is
 149                         -- required so that the temporary environment for the
 150                         -- knot includes all associated family declarations.
 151                       ; (syn_decls, alg_decls) = partition (isSynDecl . unLoc)
 152                                                    decls
 153                       ; alg_at_decls           = concatMap addATs alg_decls
 154                       }
 155                         -- Extend the global env with the knot-tied results
 156                         -- for data types and classes
 157                         --
 158                         -- We must populate the environment with the loop-tied
 159                         -- T's right away, because the kind checker may "fault
 160                         -- in" some type  constructors that recursively
 161                         -- mention T
 162                 ; let gbl_things = mkGlobalThings alg_at_decls rec_alg_tyclss
 163                 ; tcExtendRecEnv gbl_things $ do
 164
 165                         -- Kind-check the declarations
 166                 { (kc_syn_decls, kc_alg_decls) <- kcTyClDecls syn_decls alg_decls
 167
 168                 ; let { -- Calculate rec-flag
 169                       ; calc_rec  = calcRecFlags boot_details rec_alg_tyclss
 170                       ; tc_decl   = addLocM (tcTyClDecl calc_rec) }
 171
 172                         -- Type-check the type synonyms, and extend the envt
 173                 ; syn_tycons <- tcSynDecls kc_syn_decls
 174                 ; tcExtendGlobalEnv syn_tycons $ do
 175
 176                         -- Type-check the data types and classes
 177                 { alg_tyclss <- mappM tc_decl kc_alg_decls
 178                 ; return (syn_tycons, concat alg_tyclss)
 179             }}})
 180         -- Finished with knot-tying now
 181         -- Extend the environment with the finished things
 182         ; tcExtendGlobalEnv (syn_tycons ++ alg_tyclss) $ do
 183
 184         -- Perform the validity check
 185         { traceTc (text "ready for validity check")
 186         ; mappM_ (addLocM checkValidTyCl) decls
 187         ; traceTc (text "done")
 188
 189         -- Add the implicit things;
 190         -- we want them in the environment because
 191         -- they may be mentioned in interface files
 192         -- NB: All associated types and their implicit things will be added a
 193         --     second time here.  This doesn't matter as the definitions are
 194         --     the same.
 195         ; let { implicit_things = concatMap implicitTyThings alg_tyclss }
 196         ; traceTc ((text "Adding" <+> ppr alg_tyclss)
 197                    $$ (text "and" <+> ppr implicit_things))
 198         ; tcExtendGlobalEnv implicit_things getGblEnv
 199     }}
 200   where
 201     -- Pull associated types out of class declarations, to tie them into the
 202     -- knot above.
 203     -- NB: We put them in the same place in the list as `tcTyClDecl' will
 204     --     eventually put the matching `TyThing's.  That's crucial; otherwise,
 205     --     the two argument lists of `mkGlobalThings' don't match up.
 206     addATs decl@(L _ (ClassDecl {tcdATs = ats})) = decl : ats
 207     addATs decl                                  = [decl]
 208
 209 mkGlobalThings :: [LTyClDecl Name]      -- The decls
 210                -> [TyThing]             -- Knot-tied, in 1-1 correspondence with the decls
 211                -> [(Name,TyThing)]
 212 -- Driven by the Decls, and treating the TyThings lazily
 213 -- make a TypeEnv for the new things
 214 mkGlobalThings decls things
 215   = map mk_thing (decls `zipLazy` things)
 216   where
 217     mk_thing (L _ (ClassDecl {tcdLName = L _ name}), ~(AClass cl))
 218          = (name, AClass cl)
 219     mk_thing (L _ decl, ~(ATyCon tc))
 220          = (tcdName decl, ATyCon tc)
 221 \end{code}
 222
 223
 224 %************************************************************************
 225 %*                                                                      *
 226 \subsection{Type checking family instances}
 227 %*                                                                      *
 228 %************************************************************************
 229
 230 Family instances are somewhat of a hybrid.  They are processed together with
 231 class instance heads, but can contain data constructors and hence they share a
 232 lot of kinding and type checking code with ordinary algebraic data types (and
 233 GADTs).
 234
 235 \begin{code}
 236 tcFamInstDecl :: LTyClDecl Name -> TcM (Maybe TyThing)   -- Nothing if error
 237 tcFamInstDecl (L loc decl)
 238   =     -- Prime error recovery, set source location
 239     recoverM (returnM Nothing)                  $
 240     setSrcSpan loc                              $
 241     tcAddDeclCtxt decl                          $
 242     do { -- type families require -findexed-types and can't be in an
 243          -- hs-boot file
 244        ; gla_exts <- doptM Opt_IndexedTypes
 245        ; is_boot  <- tcIsHsBoot   -- Are we compiling an hs-boot file?
 246        ; checkTc gla_exts      $ badFamInstDecl (tcdLName decl)
 247        ; checkTc (not is_boot) $ badBootFamInstDeclErr
 248
 249          -- perform kind and type checking
 250        ; tcFamInstDecl1 decl
 251        }
 252
 253 tcFamInstDecl1 :: TyClDecl Name -> TcM (Maybe TyThing)   -- Nothing if error
 254
 255 tcFamInstDecl1 (decl@TySynonym {})
 256   = kcIdxTyPats decl $ \k_tvs k_typats resKind family ->
 257     do { -- check that the family declaration is for a synonym
 258          unless (isSynTyCon family) $
 259            addErr (wrongKindOfFamily family)
 260
 261        ; -- (1) kind check the right hand side of the type equation
 262        ; k_rhs <- kcCheckHsType (tcdSynRhs decl) resKind
 263
 264          -- (2) type check type equation
 265        ; tcTyVarBndrs k_tvs $ \t_tvs -> do {  -- turn kinded into proper tyvars
 266        ; t_typats <- mappM tcHsKindedType k_typats
 267        ; t_rhs    <- tcHsKindedType k_rhs
 268
 269          -- !!!of the form: forall t_tvs. (tcdLName decl) t_typats = t_rhs
 270        ; return Nothing     -- !!!TODO: need TyThing for indexed synonym
 271        }}
 272
 273 tcFamInstDecl1 (decl@TyData {tcdND = new_or_data, tcdLName = L loc tc_name,
 274                              tcdCons = cons})
 275   = kcIdxTyPats decl $ \k_tvs k_typats resKind family ->
 276     do { -- check that the family declaration is for the right kind
 277          unless (new_or_data == NewType  && isNewTyCon  family ||
 278                  new_or_data == DataType && isDataTyCon family) $
 279            addErr (wrongKindOfFamily family)
 280
 281        ; -- (1) kind check the data declaration as usual
 282        ; k_decl <- kcDataDecl decl k_tvs
 283        ; let k_ctxt = tcdCtxt k_decl
 284              k_cons = tcdCons k_decl
 285
 286          -- result kind must be '*' (otherwise, we have too few patterns)
 287        ; checkTc (isLiftedTypeKind resKind) $ tooFewParmsErr tc_name
 288
 289          -- (2) type check indexed data type declaration
 290        ; tcTyVarBndrs k_tvs $ \t_tvs -> do {  -- turn kinded into proper tyvars
 291        ; unbox_strict <- doptM Opt_UnboxStrictFields
 292
 293          -- Check that we don't use GADT syntax for indexed types
 294        ; checkTc h98_syntax (badGadtIdxTyDecl tc_name)
 295
 296          -- Check that a newtype has exactly one constructor
 297        ; checkTc (new_or_data == DataType || isSingleton k_cons) $
 298            newtypeConError tc_name (length k_cons)
 299
 300        ; t_typats     <- mappM tcHsKindedType k_typats
 301        ; stupid_theta <- tcHsKindedContext k_ctxt
 302
 303        ; rep_tc_name <- newFamInstTyConName tc_name (srcSpanStart loc)
 304        ; tycon <- fixM (\ tycon -> do
 305              { data_cons <- mappM (addLocM (tcConDecl unbox_strict tycon t_tvs))
 306                                   k_cons
 307              ; tc_rhs <-
 308                  case new_or_data of
 309                    DataType -> return (mkDataTyConRhs data_cons)
 310                    NewType  -> ASSERT( isSingleton data_cons )
 311                                mkNewTyConRhs tc_name tycon (head data_cons)
 312              ; buildAlgTyCon rep_tc_name t_tvs stupid_theta tc_rhs Recursive
 313                              False h98_syntax (Just (family, t_typats))
 314                  -- We always assume that indexed types are recursive.  Why?
 315                  -- (1) Due to their open nature, we can never be sure that a
 316                  -- further instance might not introduce a new recursive
 317                  -- dependency.  (2) They are always valid loop breakers as
 318                  -- they involve a coercion.
 319              })
 320
 321          -- construct result
 322        ; return $ Just (ATyCon tycon)
 323        }}
 324        where
 325          h98_syntax = case cons of      -- All constructors have same shape
 326                         L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False
 327                         other -> True
 328
 329 -- Kind checking of indexed types
 330 -- -
 331
 332 -- Kind check type patterns and kind annotate the embedded type variables.
 333 --
 334 -- * Here we check that a type instance matches its kind signature, but we do
 335 --   not check whether there is a pattern for each type index; the latter
 336 --   check is only required for type functions.
 337 --
 338 kcIdxTyPats :: TyClDecl Name
 339             -> ([LHsTyVarBndr Name] -> [LHsType Name] -> Kind -> TyCon -> TcM a)
 340                -- ^^kinded tvs         ^^kinded ty pats  ^^res kind
 341             -> TcM a
 342 kcIdxTyPats decl thing_inside
 343   = kcHsTyVars (tcdTyVars decl) $ \tvs ->
 344     do { family <- tcLookupLocatedTyCon (tcdLName decl)
 345        ; let { (kinds, resKind) = splitKindFunTys (tyConKind family)
 346              ; hs_typats        = fromJust $ tcdTyPats decl }
 347
 348          -- we may not have more parameters than the kind indicates
 349        ; checkTc (length kinds >= length hs_typats) $
 350            tooManyParmsErr (tcdLName decl)
 351
 352          -- type functions can have a higher-kinded result
 353        ; let resultKind = mkArrowKinds (drop (length hs_typats) kinds) resKind
 354        ; typats <- TcRnMonad.zipWithM kcCheckHsType hs_typats kinds
 355        ; thing_inside tvs typats resultKind family
 356        }
 357   where
 358 \end{code}
 359
 360
 361 %************************************************************************
 362 %*                                                                      *
 363                 Kind checking
 364 %*                                                                      *
 365 %************************************************************************
 366
 367 We need to kind check all types in the mutually recursive group
 368 before we know the kind of the type variables.  For example:
 369
 370 class C a where
 371    op :: D b => a -> b -> b
 372
 373 class D c where
 374    bop :: (Monad c) => ...
 375
 376 Here, the kind of the locally-polymorphic type variable "b"
 377 depends on *all the uses of class D*.  For example, the use of
 378 Monad c in bop's type signature means that D must have kind Type->Type.
 379
 380 However type synonyms work differently.  They can have kinds which don't
 381 just involve (->) and *:
 382         type R = Int#           -- Kind #
 383         type S a = Array# a     -- Kind * -> #
 384         type T a b = (# a,b #)  -- Kind * -> * -> (# a,b #)
 385 So we must infer their kinds from their right-hand sides *first* and then
 386 use them, whereas for the mutually recursive data types D we bring into
 387 scope kind bindings D -> k, where k is a kind variable, and do inference.
 388
 389 Indexed Types
 390 ~~~~~~~~~~~~~
 391 This treatment of type synonyms only applies to Haskell 98-style synonyms.
 392 General type functions can be recursive, and hence, appear in `alg_decls'.
 393
 394 The kind of a type family is solely determinded by its kind signature;
 395 hence, only kind signatures participate in the construction of the initial
 396 kind environment (as constructed by `getInitialKind').  In fact, we ignore
 397 instances of families altogether in the following.  However, we need to
 398 include the kinds of associated families into the construction of the
 399 initial kind environment.  (This is handled by `allDecls').
 400
 401 \begin{code}
 402 kcTyClDecls syn_decls alg_decls
 403   = do  {       -- First extend the kind env with each data type, class, and
 404                 -- indexed type, mapping them to a type variable
 405           let initialKindDecls = concat [allDecls decl | L _ decl <- alg_decls]
 406         ; alg_kinds <- mappM getInitialKind initialKindDecls
 407         ; tcExtendKindEnv alg_kinds $ do
 408
 409                 -- Now kind-check the type synonyms, in dependency order
 410                 -- We do these differently to data type and classes,
 411                 -- because a type synonym can be an unboxed type
 412                 --      type Foo = Int#
 413                 -- and a kind variable can't unify with UnboxedTypeKind
 414                 -- So we infer their kinds in dependency order
 415         { (kc_syn_decls, syn_kinds) <- kcSynDecls (calcSynCycles syn_decls)
 416         ; tcExtendKindEnv syn_kinds $  do
 417
 418                 -- Now kind-check the data type, class, and kind signatures,
 419                 -- returning kind-annotated decls; we don't kind-check
 420                 -- instances of indexed types yet, but leave this to
 421                 -- `tcInstDecls1'
 422         { kc_alg_decls <- mappM (wrapLocM kcTyClDecl)
 423                             (filter (not . isFamInstDecl . unLoc) alg_decls)
 424
 425         ; return (kc_syn_decls, kc_alg_decls) }}}
 426   where
 427     -- get all declarations relevant for determining the initial kind
 428     -- environment
 429     allDecls (decl@ClassDecl {tcdATs = ats}) = decl : [ at
 430                                                       | L _ at <- ats
 431                                                       , isFamilyDecl at]
 432     allDecls decl | isFamInstDecl decl = []
 433                   | otherwise          = [decl]
 434
 435 ------------------------------------------------------------------------
 436 getInitialKind :: TyClDecl Name -> TcM (Name, TcKind)
 437 -- Only for data type, class, and indexed type declarations
 438 -- Get as much info as possible from the data, class, or indexed type decl,
 439 -- so as to maximise usefulness of error messages
 440 getInitialKind decl
 441   = do  { arg_kinds <- mapM (mk_arg_kind . unLoc) (tyClDeclTyVars decl)
 442         ; res_kind  <- mk_res_kind decl
 443         ; return (tcdName decl, mkArrowKinds arg_kinds res_kind) }
 444   where
 445     mk_arg_kind (UserTyVar _)        = newKindVar
 446     mk_arg_kind (KindedTyVar _ kind) = return kind
 447
 448     mk_res_kind (TyFamily { tcdKind    = Just kind }) = return kind
 449     mk_res_kind (TyData   { tcdKindSig = Just kind }) = return kind
 450         -- On GADT-style declarations we allow a kind signature
 451         --      data T :: *->* where { ... }
 452     mk_res_kind other = return liftedTypeKind
 453
 454
 455 ----------------
 456 kcSynDecls :: [SCC (LTyClDecl Name)]
 457            -> TcM ([LTyClDecl Name],    -- Kind-annotated decls
 458                    [(Name,TcKind)])     -- Kind bindings
 459 kcSynDecls []
 460   = return ([], [])
 461 kcSynDecls (group : groups)
 462   = do  { (decl,  nk)  <- kcSynDecl group
 463         ; (decls, nks) <- tcExtendKindEnv [nk] (kcSynDecls groups)
 464         ; return (decl:decls, nk:nks) }
 465
 466 ----------------
 467 kcSynDecl :: SCC (LTyClDecl Name)
 468            -> TcM (LTyClDecl Name,      -- Kind-annotated decls
 469                    (Name,TcKind))       -- Kind bindings
 470 kcSynDecl (AcyclicSCC ldecl@(L loc decl))
 471   = tcAddDeclCtxt decl  $
 472     kcHsTyVars (tcdTyVars decl) (\ k_tvs ->
 473     do { traceTc (text "kcd1" <+> ppr (unLoc (tcdLName decl)) <+> brackets (ppr (tcdTyVars decl))
 474                         <+> brackets (ppr k_tvs))
 475        ; (k_rhs, rhs_kind) <- kcHsType (tcdSynRhs decl)
 476        ; traceTc (text "kcd2" <+> ppr (unLoc (tcdLName decl)))
 477        ; let tc_kind = foldr (mkArrowKind . kindedTyVarKind) rhs_kind k_tvs
 478        ; return (L loc (decl { tcdTyVars = k_tvs, tcdSynRhs = k_rhs }),
 479                  (unLoc (tcdLName decl), tc_kind)) })
 480
 481 kcSynDecl (CyclicSCC decls)
 482   = do { recSynErr decls; failM }       -- Fail here to avoid error cascade
 483                                         -- of out-of-scope tycons
 484
 485 kindedTyVarKind (L _ (KindedTyVar _ k)) = k
 486
 487 ------------------------------------------------------------------------
 488 kcTyClDecl :: TyClDecl Name -> TcM (TyClDecl Name)
 489         -- Not used for type synonyms (see kcSynDecl)
 490
 491 kcTyClDecl decl@(TyData {})
 492   = ASSERT( not . isFamInstDecl $ decl )   -- must not be a family instance
 493     kcTyClDeclBody decl $
 494       kcDataDecl decl
 495
 496 kcTyClDecl decl@(TyFamily {tcdKind = kind})
 497   = kcTyClDeclBody decl $ \ tvs' ->
 498       return (decl {tcdTyVars = tvs',
 499                     tcdKind = kind `mplus` Just liftedTypeKind})
 500                     -- default result kind is '*'
 501
 502 kcTyClDecl decl@(ClassDecl {tcdCtxt = ctxt, tcdSigs = sigs, tcdATs = ats})
 503   = kcTyClDeclBody decl $ \ tvs' ->
 504     do  { is_boot <- tcIsHsBoot
 505         ; ctxt' <- kcHsContext ctxt
 506         ; ats'  <- mappM (wrapLocM kcTyClDecl) ats
 507         ; sigs' <- mappM (wrapLocM kc_sig    ) sigs
 508         ; return (decl {tcdTyVars = tvs', tcdCtxt = ctxt', tcdSigs = sigs',
 509                         tcdATs = ats'}) }
 510   where
 511     kc_sig (TypeSig nm op_ty) = do { op_ty' <- kcHsLiftedSigType op_ty
 512                                    ; return (TypeSig nm op_ty') }
 513     kc_sig other_sig          = return other_sig
 514
 515 kcTyClDecl decl@(ForeignType {})
 516   = return decl
 517
 518 kcTyClDeclBody :: TyClDecl Name
 519                -> ([LHsTyVarBndr Name] -> TcM a)
 520                -> TcM a
 521 -- getInitialKind has made a suitably-shaped kind for the type or class
 522 -- Unpack it, and attribute those kinds to the type variables
 523 -- Extend the env with bindings for the tyvars, taken from
 524 -- the kind of the tycon/class.  Give it to the thing inside, and
 525 -- check the result kind matches
 526 kcTyClDeclBody decl thing_inside
 527   = tcAddDeclCtxt decl          $
 528     do  { tc_ty_thing <- tcLookupLocated (tcdLName decl)
 529         ; let tc_kind    = case tc_ty_thing of { AThing k -> k }
 530               (kinds, _) = splitKindFunTys tc_kind
 531               hs_tvs     = tcdTyVars decl
 532               kinded_tvs = ASSERT( length kinds >= length hs_tvs )
 533                            [ L loc (KindedTyVar (hsTyVarName tv) k)
 534                            | (L loc tv, k) <- zip hs_tvs kinds]
 535         ; tcExtendKindEnvTvs kinded_tvs (thing_inside kinded_tvs) }
 536
 537 -- Kind check a data declaration, assuming that we already extended the
 538 -- kind environment with the type variables of the left-hand side (these
 539 -- kinded type variables are also passed as the second parameter).
 540 --
 541 kcDataDecl :: TyClDecl Name -> [LHsTyVarBndr Name] -> TcM (TyClDecl Name)
 542 kcDataDecl decl@(TyData {tcdND = new_or_data, tcdCtxt = ctxt, tcdCons = cons})
 543            tvs
 544   = do  { ctxt' <- kcHsContext ctxt
 545         ; cons' <- mappM (wrapLocM kc_con_decl) cons
 546         ; return (decl {tcdTyVars = tvs, tcdCtxt = ctxt', tcdCons = cons'}) }
 547   where
 548     -- doc comments are typechecked to Nothing here
 549     kc_con_decl (ConDecl name expl ex_tvs ex_ctxt details res _) = do
 550       kcHsTyVars ex_tvs $ \ex_tvs' -> do
 551         ex_ctxt' <- kcHsContext ex_ctxt
 552         details' <- kc_con_details details
 553         res'     <- case res of
 554           ResTyH98 -> return ResTyH98
 555           ResTyGADT ty -> do { ty' <- kcHsSigType ty; return (ResTyGADT ty') }
 556         return (ConDecl name expl ex_tvs' ex_ctxt' details' res' Nothing)
 557
 558     kc_con_details (PrefixCon btys)
 559         = do { btys' <- mappM kc_larg_ty btys ; return (PrefixCon btys') }
 560     kc_con_details (InfixCon bty1 bty2)
 561         = do { bty1' <- kc_larg_ty bty1; bty2' <- kc_larg_ty bty2; return (InfixCon bty1' bty2') }
 562     kc_con_details (RecCon fields)
 563         = do { fields' <- mappM kc_field fields; return (RecCon fields') }
 564
 565     kc_field (HsRecField fld bty d) = do { bty' <- kc_larg_ty bty ; return (HsRecField fld bty' d) }
 566
 567     kc_larg_ty bty = case new_or_data of
 568                         DataType -> kcHsSigType bty
 569                         NewType  -> kcHsLiftedSigType bty
 570         -- Can't allow an unlifted type for newtypes, because we're effectively
 571         -- going to remove the constructor while coercing it to a lifted type.
 572         -- And newtypes can't be bang'd
 573 \end{code}
 574
 575
 576 %************************************************************************
 577 %*                                                                      *
 578 \subsection{Type checking}
 579 %*                                                                      *
 580 %************************************************************************
 581
 582 \begin{code}
 583 tcSynDecls :: [LTyClDecl Name] -> TcM [TyThing]
 584 tcSynDecls [] = return []
 585 tcSynDecls (decl : decls)
 586   = do { syn_tc <- addLocM tcSynDecl decl
 587        ; syn_tcs <- tcExtendGlobalEnv [syn_tc] (tcSynDecls decls)
 588        ; return (syn_tc : syn_tcs) }
 589
 590 tcSynDecl
 591   (TySynonym {tcdLName = L _ tc_name, tcdTyVars = tvs, tcdSynRhs = rhs_ty})
 592   = tcTyVarBndrs tvs            $ \ tvs' -> do
 593     { traceTc (text "tcd1" <+> ppr tc_name)
 594     ; rhs_ty' <- tcHsKindedType rhs_ty
 595     ; return (ATyCon (buildSynTyCon tc_name tvs' (SynonymTyCon rhs_ty'))) }
 596
 597 --------------------
 598 tcTyClDecl :: (Name -> RecFlag) -> TyClDecl Name -> TcM [TyThing]
 599
 600 tcTyClDecl calc_isrec decl
 601   = tcAddDeclCtxt decl (tcTyClDecl1 calc_isrec decl)
 602
 603   -- "type family" declarations
 604 tcTyClDecl1 _calc_isrec
 605   (TyFamily {tcdFlavour = TypeFamily,
 606              tcdLName = L _ tc_name, tcdTyVars = tvs, tcdKind = Just kind})
 607                                                       -- NB: kind at latest
 608                                                       --     added during
 609                                                       --     kind checking
 610   = tcTyVarBndrs tvs  $ \ tvs' -> do
 611   { traceTc (text "type family: " <+> ppr tc_name)
 612   ; idx_tys <- doptM Opt_IndexedTypes
 613
 614         -- Check that we don't use families without -findexed-types
 615   ; checkTc idx_tys $ badFamInstDecl tc_name
 616
 617   ; return [ATyCon $ buildSynTyCon tc_name tvs' (OpenSynTyCon kind Nothing)]
 618   }
 619
 620   -- "newtype family" or "data family" declaration
 621 tcTyClDecl1 _calc_isrec
 622   (TyFamily {tcdFlavour = DataFamily new_or_data,
 623              tcdLName = L _ tc_name, tcdTyVars = tvs, tcdKind = mb_kind})
 624   = tcTyVarBndrs tvs  $ \ tvs' -> do
 625   { traceTc (text "data/newtype family: " <+> ppr tc_name)
 626   ; extra_tvs <- tcDataKindSig mb_kind
 627   ; let final_tvs = tvs' ++ extra_tvs    -- we may not need these
 628
 629   ; idx_tys <- doptM Opt_IndexedTypes
 630
 631         -- Check that we don't use families without -findexed-types
 632   ; checkTc idx_tys $ badFamInstDecl tc_name
 633
 634   ; tycon <- buildAlgTyCon tc_name final_tvs []
 635                (case new_or_data of
 636                   DataType -> mkOpenDataTyConRhs
 637                   NewType  -> mkOpenNewTyConRhs)
 638                Recursive False True Nothing
 639   ; return [ATyCon tycon]
 640   }
 641
 642   -- "newtype", "data", "newtype instance", "data instance"
 643 tcTyClDecl1 calc_isrec
 644   (TyData {tcdND = new_or_data, tcdCtxt = ctxt, tcdTyVars = tvs,
 645            tcdLName = L _ tc_name, tcdKindSig = mb_ksig, tcdCons = cons})
 646   = tcTyVarBndrs tvs    $ \ tvs' -> do
 647   { extra_tvs <- tcDataKindSig mb_ksig
 648   ; let final_tvs = tvs' ++ extra_tvs
 649   ; stupid_theta <- tcHsKindedContext ctxt
 650   ; want_generic <- doptM Opt_Generics
 651   ; unbox_strict <- doptM Opt_UnboxStrictFields
 652   ; gla_exts     <- doptM Opt_GlasgowExts
 653   ; is_boot      <- tcIsHsBoot  -- Are we compiling an hs-boot file?
 654
 655         -- Check that we don't use GADT syntax in H98 world
 656   ; checkTc (gla_exts || h98_syntax) (badGadtDecl tc_name)
 657
 658         -- Check that we don't use kind signatures without Glasgow extensions
 659   ; checkTc (gla_exts || isNothing mb_ksig) (badSigTyDecl tc_name)
 660
 661         -- Check that the stupid theta is empty for a GADT-style declaration
 662   ; checkTc (null stupid_theta || h98_syntax) (badStupidTheta tc_name)
 663
 664         -- Check that there's at least one condecl,
 665         -- or else we're reading an hs-boot file, or -fglasgow-exts
 666   ; checkTc (not (null cons) || gla_exts || is_boot)
 667             (emptyConDeclsErr tc_name)
 668
 669         -- Check that a newtype has exactly one constructor
 670   ; checkTc (new_or_data == DataType || isSingleton cons)
 671             (newtypeConError tc_name (length cons))
 672
 673   ; tycon <- fixM (\ tycon -> do
 674         { data_cons <- mappM (addLocM (tcConDecl unbox_strict tycon final_tvs))
 675                              cons
 676         ; tc_rhs <-
 677             if null cons && is_boot     -- In a hs-boot file, empty cons means
 678             then return AbstractTyCon   -- "don't know"; hence Abstract
 679             else case new_or_data of
 680                    DataType -> return (mkDataTyConRhs data_cons)
 681                    NewType  ->
 682                        ASSERT( isSingleton data_cons )
 683                        mkNewTyConRhs tc_name tycon (head data_cons)
 684         ; buildAlgTyCon tc_name final_tvs stupid_theta tc_rhs is_rec
 685             (want_generic && canDoGenerics data_cons) h98_syntax Nothing
 686         })
 687   ; return [ATyCon tycon]
 688   }
 689   where
 690     is_rec   = calc_isrec tc_name
 691     h98_syntax = case cons of   -- All constructors have same shape
 692                         L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False
 693                         other -> True
 694
 695 tcTyClDecl1 calc_isrec
 696   (ClassDecl {tcdLName = L _ class_name, tcdTyVars = tvs,
 697               tcdCtxt = ctxt, tcdMeths = meths,
 698               tcdFDs = fundeps, tcdSigs = sigs, tcdATs = ats} )
 699   = tcTyVarBndrs tvs            $ \ tvs' -> do
 700   { ctxt' <- tcHsKindedContext ctxt
 701   ; fds' <- mappM (addLocM tc_fundep) fundeps
 702   ; atss <- mappM (addLocM (tcTyClDecl1 (const Recursive))) ats
 703   ; let ats' = zipWith setTyThingPoss atss (map (tcdTyVars . unLoc) ats)
 704   ; sig_stuff <- tcClassSigs class_name sigs meths
 705   ; clas <- fixM (\ clas ->
 706                 let     -- This little knot is just so we can get
 707                         -- hold of the name of the class TyCon, which we
 708                         -- need to look up its recursiveness
 709                     tycon_name = tyConName (classTyCon clas)
 710                     tc_isrec = calc_isrec tycon_name
 711                 in
 712                 buildClass class_name tvs' ctxt' fds' ats'
 713                            sig_stuff tc_isrec)
 714   ; return (AClass clas : ats')
 715       -- NB: Order is important due to the call to `mkGlobalThings' when
 716       --     tying the the type and class declaration type checking knot.
 717   }
 718   where
 719     tc_fundep (tvs1, tvs2) = do { tvs1' <- mappM tcLookupTyVar tvs1 ;
 720                                 ; tvs2' <- mappM tcLookupTyVar tvs2 ;
 721                                 ; return (tvs1', tvs2') }
 722
 723     -- For each AT argument compute the position of the corresponding class
 724     -- parameter in the class head.  This will later serve as a permutation
 725     -- vector when checking the validity of instance declarations.
 726     setTyThingPoss [ATyCon tycon] atTyVars =
 727       let classTyVars = hsLTyVarNames tvs
 728           poss        =   catMaybes
 729                         . map (`elemIndex` classTyVars)
 730                         . hsLTyVarNames
 731                         $ atTyVars
 732                      -- There will be no Nothing, as we already passed renaming
 733       in
 734       ATyCon (setTyConArgPoss tycon poss)
 735     setTyThingPoss _              _ = panic "TcTyClsDecls.setTyThingPoss"
 736
 737 tcTyClDecl1 calc_isrec
 738   (ForeignType {tcdLName = L _ tc_name, tcdExtName = tc_ext_name})
 739   = returnM [ATyCon (mkForeignTyCon tc_name tc_ext_name liftedTypeKind 0)]
 740
 741 -----------------------------------
 742 tcConDecl :: Bool               -- True <=> -funbox-strict_fields
 743           -> TyCon -> [TyVar]
 744           -> ConDecl Name
 745           -> TcM DataCon
 746
 747 tcConDecl unbox_strict tycon tc_tvs     -- Data types
 748           (ConDecl name _ tvs ctxt details res_ty _)
 749   = tcTyVarBndrs tvs            $ \ tvs' -> do
 750     { ctxt' <- tcHsKindedContext ctxt
 751     ; (univ_tvs, ex_tvs, eq_preds, data_tc) <- tcResultType tycon tc_tvs tvs' res_ty
 752     ; let
 753         -- Tiresome: tidy the tyvar binders, since tc_tvs and tvs' may have the same OccNames
 754         tc_datacon is_infix field_lbls btys
 755           = do { let bangs = map getBangStrictness btys
 756                ; arg_tys <- mappM tcHsBangType btys
 757                ; buildDataCon (unLoc name) is_infix
 758                     (argStrictness unbox_strict bangs arg_tys)
 759                     (map unLoc field_lbls)
 760                     univ_tvs ex_tvs eq_preds ctxt' arg_tys
 761                     data_tc }
 762                 -- NB:  we put data_tc, the type constructor gotten from the
 763                 --      constructor type signature into the data constructor;
 764                 --      that way checkValidDataCon can complain if it's wrong.
 765
 766     ; case details of
 767         PrefixCon btys     -> tc_datacon False [] btys
 768         InfixCon bty1 bty2 -> tc_datacon True  [] [bty1,bty2]
 769         RecCon fields      -> tc_datacon False field_names btys
 770                            where
 771                               (field_names, btys) = unzip [ (n, t) | HsRecField n t _ <- fields ]
 772
 773     }
 774
 775 tcResultType :: TyCon
 776              -> [TyVar]         -- data T a b c = ...
 777              -> [TyVar]         -- where MkT :: forall a b c. ...
 778              -> ResType Name
 779              -> TcM ([TyVar],           -- Universal
 780                      [TyVar],           -- Existential (distinct OccNames from univs)
 781                      [(TyVar,Type)],    -- Equality predicates
 782                      TyCon)             -- TyCon given in the ResTy
 783         -- We don't check that the TyCon given in the ResTy is
 784         -- the same as the parent tycon, becuase we are in the middle
 785         -- of a recursive knot; so it's postponed until checkValidDataCon
 786
 787 tcResultType decl_tycon tc_tvs dc_tvs ResTyH98
 788   = return (tc_tvs, dc_tvs, [], decl_tycon)
 789         -- In H98 syntax the dc_tvs are the existential ones
 790         --      data T a b c = forall d e. MkT ...
 791         -- The {a,b,c} are tc_tvs, and {d,e} are dc_tvs
 792
 793 tcResultType _ tc_tvs dc_tvs (ResTyGADT res_ty)
 794         -- E.g.  data T a b c where
 795         --         MkT :: forall x y z. T (x,y) z z
 796         -- Then we generate
 797         --      ([a,z,c], [x,y], [a:=:(x,y), c:=:z], T)
 798
 799   = do  { (dc_tycon, res_tys) <- tcLHsConResTy res_ty
 800
 801         ; let univ_tvs = choose_univs [] tidy_tc_tvs res_tys
 802                 -- Each univ_tv is either a dc_tv or a tc_tv
 803               ex_tvs = dc_tvs `minusList` univ_tvs
 804               eq_spec = [ (tv, ty) | (tv,ty) <- univ_tvs `zip` res_tys,
 805                                       tv `elem` tc_tvs]
 806         ; return (univ_tvs, ex_tvs, eq_spec, dc_tycon) }
 807   where
 808         -- choose_univs uses the res_ty itself if it's a type variable
 809         -- and hasn't already been used; otherwise it uses one of the tc_tvs
 810     choose_univs used tc_tvs []
 811         = ASSERT( null tc_tvs ) []
 812     choose_univs used (tc_tv:tc_tvs) (res_ty:res_tys)
 813         | Just tv <- tcGetTyVar_maybe res_ty, not (tv `elem` used)
 814         = tv    : choose_univs (tv:used) tc_tvs res_tys
 815         | otherwise
 816         = tc_tv : choose_univs used tc_tvs res_tys
 817
 818         -- NB: tc_tvs and dc_tvs are distinct, but
 819         -- we want them to be *visibly* distinct, both for
 820         -- interface files and general confusion.  So rename
 821         -- the tc_tvs, since they are not used yet (no
 822         -- consequential renaming needed)
 823     init_occ_env     = initTidyOccEnv (map getOccName dc_tvs)
 824     (_, tidy_tc_tvs) = mapAccumL tidy_one init_occ_env tc_tvs
 825     tidy_one env tv  = (env', setTyVarName tv (tidyNameOcc name occ'))
 826               where
 827                  name = tyVarName tv
 828                  (env', occ') = tidyOccName env (getOccName name)
 829
 830               -------------------
 831 argStrictness :: Bool           -- True <=> -funbox-strict_fields
 832               -> [HsBang]
 833               -> [TcType] -> [StrictnessMark]
 834 argStrictness unbox_strict bangs arg_tys
 835  = ASSERT( length bangs == length arg_tys )
 836    zipWith (chooseBoxingStrategy unbox_strict) arg_tys bangs
 837
 838 -- We attempt to unbox/unpack a strict field when either:
 839 --   (i)  The field is marked '!!', or
 840 --   (ii) The field is marked '!', and the -funbox-strict-fields flag is on.
 841 --
 842 -- We have turned off unboxing of newtypes because coercions make unboxing
 843 -- and reboxing more complicated
 844 chooseBoxingStrategy :: Bool -> TcType -> HsBang -> StrictnessMark
 845 chooseBoxingStrategy unbox_strict_fields arg_ty bang
 846   = case bang of
 847         HsNoBang                                    -> NotMarkedStrict
 848         HsStrict | unbox_strict_fields
 849                    && can_unbox arg_ty              -> MarkedUnboxed
 850         HsUnbox  | can_unbox arg_ty                 -> MarkedUnboxed
 851         other                                       -> MarkedStrict
 852   where
 853     -- we can unbox if the type is a chain of newtypes with a product tycon
 854     -- at the end
 855     can_unbox arg_ty = case splitTyConApp_maybe arg_ty of
 856                    Nothing                      -> False
 857                    Just (arg_tycon, tycon_args) ->
 858                        not (isRecursiveTyCon arg_tycon) &&      -- Note [Recusive unboxing]
 859                        isProductTyCon arg_tycon &&
 860                        (if isNewTyCon arg_tycon then
 861                             can_unbox (newTyConInstRhs arg_tycon tycon_args)
 862                         else True)
 863 \end{code}
 864
 865 Note [Recursive unboxing]
 866 ~~~~~~~~~~~~~~~~~~~~~~~~~
 867 Be careful not to try to unbox this!
 868         data T = MkT !T Int
 869 But it's the *argument* type that matters. This is fine:
 870         data S = MkS S !Int
 871 because Int is non-recursive.
 872
 873 %************************************************************************
 874 %*                                                                      *
 875 \subsection{Dependency analysis}
 876 %*                                                                      *
 877 %************************************************************************
 878
 879 Validity checking is done once the mutually-recursive knot has been
 880 tied, so we can look at things freely.
 881
 882 \begin{code}
 883 checkCycleErrs :: [LTyClDecl Name] -> TcM ()
 884 checkCycleErrs tyclss
 885   | null cls_cycles
 886   = return ()
 887   | otherwise
 888   = do  { mappM_ recClsErr cls_cycles
 889         ; failM }       -- Give up now, because later checkValidTyCl
 890                         -- will loop if the synonym is recursive
 891   where
 892     cls_cycles = calcClassCycles tyclss
 893
 894 checkValidTyCl :: TyClDecl Name -> TcM ()
 895 -- We do the validity check over declarations, rather than TyThings
 896 -- only so that we can add a nice context with tcAddDeclCtxt
 897 checkValidTyCl decl
 898   = tcAddDeclCtxt decl $
 899     do  { thing <- tcLookupLocatedGlobal (tcdLName decl)
 900         ; traceTc (text "Validity of" <+> ppr thing)
 901         ; case thing of
 902             ATyCon tc -> checkValidTyCon tc
 903             AClass cl -> checkValidClass cl
 904         ; traceTc (text "Done validity of" <+> ppr thing)
 905         }
 906
 907 -------------------------
 908 -- For data types declared with record syntax, we require
 909 -- that each constructor that has a field 'f'
 910 --      (a) has the same result type
 911 --      (b) has the same type for 'f'
 912 -- module alpha conversion of the quantified type variables
 913 -- of the constructor.
 914
 915 checkValidTyCon :: TyCon -> TcM ()
 916 checkValidTyCon tc
 917   | isSynTyCon tc
 918   = case synTyConRhs tc of
 919       OpenSynTyCon _ _ -> return ()
 920       SynonymTyCon ty  -> checkValidType syn_ctxt ty
 921   | otherwise
 922   =     -- Check the context on the data decl
 923     checkValidTheta (DataTyCtxt name) (tyConStupidTheta tc)     `thenM_`
 924
 925         -- Check arg types of data constructors
 926     mappM_ (checkValidDataCon tc) data_cons                     `thenM_`
 927
 928         -- Check that fields with the same name share a type
 929     mappM_ check_fields groups
 930
 931   where
 932     syn_ctxt  = TySynCtxt name
 933     name      = tyConName tc
 934     data_cons = tyConDataCons tc
 935
 936     groups = equivClasses cmp_fld (concatMap get_fields data_cons)
 937     cmp_fld (f1,_) (f2,_) = f1 `compare` f2
 938     get_fields con = dataConFieldLabels con `zip` repeat con
 939         -- dataConFieldLabels may return the empty list, which is fine
 940
 941     -- See Note [GADT record selectors] in MkId.lhs
 942     -- We must check (a) that the named field has the same
 943     --                   type in each constructor
 944     --               (b) that those constructors have the same result type
 945     --
 946     -- However, the constructors may have differently named type variable
 947     -- and (worse) we don't know how the correspond to each other.  E.g.
 948     --     C1 :: forall a b. { f :: a, g :: b } -> T a b
 949     --     C2 :: forall d c. { f :: c, g :: c } -> T c d
 950     --
 951     -- So what we do is to ust Unify.tcMatchTys to compare the first candidate's
 952     -- result type against other candidates' types BOTH WAYS ROUND.
 953     -- If they magically agrees, take the substitution and
 954     -- apply them to the latter ones, and see if they match perfectly.
 955     check_fields fields@((label, con1) : other_fields)
 956         -- These fields all have the same name, but are from
 957         -- different constructors in the data type
 958         = recoverM (return ()) $ mapM_ checkOne other_fields
 959                 -- Check that all the fields in the group have the same type
 960                 -- NB: this check assumes that all the constructors of a given
 961                 -- data type use the same type variables
 962         where
 963         (tvs1, _, _, res1) = dataConSig con1
 964         ts1 = mkVarSet tvs1
 965         fty1 = dataConFieldType con1 label
 966
 967         checkOne (_, con2)    -- Do it bothways to ensure they are structurally identical
 968             = do { checkFieldCompat label con1 con2 ts1 res1 res2 fty1 fty2
 969                  ; checkFieldCompat label con2 con1 ts2 res2 res1 fty2 fty1 }
 970             where
 971                 (tvs2, _, _, res2) = dataConSig con2
 972                 ts2 = mkVarSet tvs2
 973                 fty2 = dataConFieldType con2 label
 974
 975 checkFieldCompat fld con1 con2 tvs1 res1 res2 fty1 fty2
 976   = do  { checkTc (isJust mb_subst1) (resultTypeMisMatch fld con1 con2)
 977         ; checkTc (isJust mb_subst2) (fieldTypeMisMatch fld con1 con2) }
 978   where
 979     mb_subst1 = tcMatchTy tvs1 res1 res2
 980     mb_subst2 = tcMatchTyX tvs1 (expectJust "checkFieldCompat" mb_subst1) fty1 fty2
 981
 982 -------------------------------
 983 checkValidDataCon :: TyCon -> DataCon -> TcM ()
 984 checkValidDataCon tc con
 985   = setSrcSpan (srcLocSpan (getSrcLoc con))     $
 986     addErrCtxt (dataConCtxt con)                $
 987     do  { checkTc (dataConTyCon con == tc) (badDataConTyCon con)
 988         ; checkValidType ctxt (dataConUserType con)
 989         ; ifM (isNewTyCon tc) (checkNewDataCon con)
 990     }
 991   where
 992     ctxt = ConArgCtxt (dataConName con)
 993
 994 -------------------------------
 995 checkNewDataCon :: DataCon -> TcM ()
 996 -- Checks for the data constructor of a newtype
 997 checkNewDataCon con
 998   = do  { checkTc (isSingleton arg_tys) (newtypeFieldErr con (length arg_tys))
 999                 -- One argument
1000         ; checkTc (null eq_spec) (newtypePredError con)
1001                 -- Return type is (T a b c)
1002         ; checkTc (null ex_tvs && null theta) (newtypeExError con)
1003                 -- No existentials
1004     }
1005   where
1006     (_univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig con
1007
1008 -------------------------------
1009 checkValidClass :: Class -> TcM ()
1010 checkValidClass cls
1011   = do  {       -- CHECK ARITY 1 FOR HASKELL 1.4
1012           gla_exts <- doptM Opt_GlasgowExts
1013
1014         -- Check that the class is unary, unless GlaExs
1015         ; checkTc (notNull tyvars) (nullaryClassErr cls)
1016         ; checkTc (gla_exts || unary) (classArityErr cls)
1017
1018         -- Check the super-classes
1019         ; checkValidTheta (ClassSCCtxt (className cls)) theta
1020
1021         -- Check the class operations
1022         ; mappM_ (check_op gla_exts) op_stuff
1023
1024         -- Check that if the class has generic methods, then the
1025         -- class has only one parameter.  We can't do generic
1026         -- multi-parameter type classes!
1027         ; checkTc (unary || no_generics) (genericMultiParamErr cls)
1028         }
1029   where
1030     (tyvars, theta, _, op_stuff) = classBigSig cls
1031     unary       = isSingleton tyvars
1032     no_generics = null [() | (_, GenDefMeth) <- op_stuff]
1033
1034     check_op gla_exts (sel_id, dm)
1035       = addErrCtxt (classOpCtxt sel_id tau) $ do
1036         { checkValidTheta SigmaCtxt (tail theta)
1037                 -- The 'tail' removes the initial (C a) from the
1038                 -- class itself, leaving just the method type
1039
1040         ; checkValidType (FunSigCtxt op_name) tau
1041
1042                 -- Check that the type mentions at least one of
1043                 -- the class type variables...or at least one reachable
1044                 -- from one of the class variables.  Example: tc223
1045                 --   class Error e => Game b mv e | b -> mv e where
1046                 --      newBoard :: MonadState b m => m ()
1047                 -- Here, MonadState has a fundep m->b, so newBoard is fine
1048         ; let grown_tyvars = grow theta (mkVarSet tyvars)
1049         ; checkTc (tyVarsOfType tau `intersectsVarSet` grown_tyvars)
1050                   (noClassTyVarErr cls sel_id)
1051
1052                 -- Check that for a generic method, the type of
1053                 -- the method is sufficiently simple
1054         ; checkTc (dm /= GenDefMeth || validGenericMethodType tau)
1055                   (badGenericMethodType op_name op_ty)
1056         }
1057         where
1058           op_name = idName sel_id
1059           op_ty   = idType sel_id
1060           (_,theta1,tau1) = tcSplitSigmaTy op_ty
1061           (_,theta2,tau2)  = tcSplitSigmaTy tau1
1062           (theta,tau) | gla_exts  = (theta1 ++ theta2, tau2)
1063                       | otherwise = (theta1,           mkPhiTy (tail theta1) tau1)
1064                 -- Ugh!  The function might have a type like
1065                 --      op :: forall a. C a => forall b. (Eq b, Eq a) => tau2
1066                 -- With -fglasgow-exts, we want to allow this, even though the inner
1067                 -- forall has an (Eq a) constraint.  Whereas in general, each constraint
1068                 -- in the context of a for-all must mention at least one quantified
1069                 -- type variable.  What a mess!
1070
1071
1072 ---------------------------------------------------------------------
1073 resultTypeMisMatch field_name con1 con2
1074   = vcat [sep [ptext SLIT("Constructors") <+> ppr con1 <+> ptext SLIT("and") <+> ppr con2,
1075                 ptext SLIT("have a common field") <+> quotes (ppr field_name) <> comma],
1076           nest 2 $ ptext SLIT("but have different result types")]
1077 fieldTypeMisMatch field_name con1 con2
1078   = sep [ptext SLIT("Constructors") <+> ppr con1 <+> ptext SLIT("and") <+> ppr con2,
1079          ptext SLIT("give different types for field"), quotes (ppr field_name)]
1080
1081 dataConCtxt con = ptext SLIT("In the definition of data constructor") <+> quotes (ppr con)
1082
1083 classOpCtxt sel_id tau = sep [ptext SLIT("When checking the class method:"),
1084                               nest 2 (ppr sel_id <+> dcolon <+> ppr tau)]
1085
1086 nullaryClassErr cls
1087   = ptext SLIT("No parameters for class")  <+> quotes (ppr cls)
1088
1089 classArityErr cls
1090   = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls),
1091           parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))]
1092
1093 noClassTyVarErr clas op
1094   = sep [ptext SLIT("The class method") <+> quotes (ppr op),
1095          ptext SLIT("mentions none of the type variables of the class") <+>
1096                 ppr clas <+> hsep (map ppr (classTyVars clas))]
1097
1098 genericMultiParamErr clas
1099   = ptext SLIT("The multi-parameter class") <+> quotes (ppr clas) <+>
1100     ptext SLIT("cannot have generic methods")
1101
1102 badGenericMethodType op op_ty
1103   = hang (ptext SLIT("Generic method type is too complex"))
1104        4 (vcat [ppr op <+> dcolon <+> ppr op_ty,
1105                 ptext SLIT("You can only use type variables, arrows, lists, and tuples")])
1106
1107 recSynErr syn_decls
1108   = setSrcSpan (getLoc (head sorted_decls)) $
1109     addErr (sep [ptext SLIT("Cycle in type synonym declarations:"),
1110                  nest 2 (vcat (map ppr_decl sorted_decls))])
1111   where
1112     sorted_decls = sortLocated syn_decls
1113     ppr_decl (L loc decl) = ppr loc <> colon <+> ppr decl
1114
1115 recClsErr cls_decls
1116   = setSrcSpan (getLoc (head sorted_decls)) $
1117     addErr (sep [ptext SLIT("Cycle in class declarations (via superclasses):"),
1118                  nest 2 (vcat (map ppr_decl sorted_decls))])
1119   where
1120     sorted_decls = sortLocated cls_decls
1121     ppr_decl (L loc decl) = ppr loc <> colon <+> ppr (decl { tcdSigs = [] })
1122
1123 sortLocated :: [Located a] -> [Located a]
1124 sortLocated things = sortLe le things
1125   where
1126     le (L l1 _) (L l2 _) = l1 <= l2
1127
1128 badDataConTyCon data_con
1129   = hang (ptext SLIT("Data constructor") <+> quotes (ppr data_con) <+>
1130                 ptext SLIT("returns type") <+> quotes (ppr (dataConTyCon data_con)))
1131        2 (ptext SLIT("instead of its parent type"))
1132
1133 badGadtDecl tc_name
1134   = vcat [ ptext SLIT("Illegal generalised algebraic data declaration for") <+> quotes (ppr tc_name)
1135          , nest 2 (parens $ ptext SLIT("Use -fglasgow-exts to allow GADTs")) ]
1136
1137 badStupidTheta tc_name
1138   = ptext SLIT("A data type declared in GADT style cannot have a context:") <+> quotes (ppr tc_name)
1139
1140 newtypeConError tycon n
1141   = sep [ptext SLIT("A newtype must have exactly one constructor,"),
1142          nest 2 $ ptext SLIT("but") <+> quotes (ppr tycon) <+> ptext SLIT("has") <+> speakN n ]
1143
1144 newtypeExError con
1145   = sep [ptext SLIT("A newtype constructor cannot have an existential context,"),
1146          nest 2 $ ptext SLIT("but") <+> quotes (ppr con) <+> ptext SLIT("does")]
1147
1148 newtypePredError con
1149   = sep [ptext SLIT("A newtype constructor must have a return type of form T a1 ... an"),
1150          nest 2 $ ptext SLIT("but") <+> quotes (ppr con) <+> ptext SLIT("does not")]
1151
1152 newtypeFieldErr con_name n_flds
1153   = sep [ptext SLIT("The constructor of a newtype must have exactly one field"),
1154          nest 2 $ ptext SLIT("but") <+> quotes (ppr con_name) <+> ptext SLIT("has") <+> speakN n_flds]
1155
1156 badSigTyDecl tc_name
1157   = vcat [ ptext SLIT("Illegal kind signature") <+>
1158            quotes (ppr tc_name)
1159          , nest 2 (parens $ ptext SLIT("Use -fglasgow-exts to allow kind signatures")) ]
1160
1161 badFamInstDecl tc_name
1162   = vcat [ ptext SLIT("Illegal family instance for") <+>
1163            quotes (ppr tc_name)
1164          , nest 2 (parens $ ptext SLIT("Use -findexed-types to allow indexed type families")) ]
1165
1166 badGadtIdxTyDecl tc_name
1167   = vcat [ ptext SLIT("Illegal generalised algebraic data declaration for") <+>
1168            quotes (ppr tc_name)
1169          , nest 2 (parens $ ptext SLIT("Family instances can not yet use GADT declarations")) ]
1170
1171 tooManyParmsErr tc_name
1172   = ptext SLIT("Family instance has too many parameters:") <+>
1173     quotes (ppr tc_name)
1174
1175 tooFewParmsErr tc_name
1176   = ptext SLIT("Family instance has too few parameters:") <+>
1177     quotes (ppr tc_name)
1178
1179 badBootFamInstDeclErr =
1180   ptext SLIT("Illegal family instance in hs-boot file")
1181
1182 wrongKindOfFamily family =
1183   ptext SLIT("Wrong category of family instance; declaration was for a") <+>
1184   kindOfFamily
1185   where
1186     kindOfFamily | isSynTyCon  family = ptext SLIT("type synonym")
1187                  | isDataTyCon family = ptext SLIT("data type")
1188                  | isNewTyCon  family = ptext SLIT("newtype")
1189
1190 emptyConDeclsErr tycon
1191   = sep [quotes (ppr tycon) <+> ptext SLIT("has no constructors"),
1192          nest 2 $ ptext SLIT("(-fglasgow-exts permits this)")]
1193 \end{code}