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