compiler/typecheck/TcTyClsDecls.lhs

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