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