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