ghc/compiler/typecheck/TcHsType.lhs

   1
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
   5
   6 \begin{code}
   7 module TcHsType (
   8         tcHsSigType, tcHsDeriv,
   9         UserTypeCtxt(..),
  10
  11                 -- Kind checking
  12         kcHsTyVars, kcHsSigType, kcHsLiftedSigType,
  13         kcCheckHsType, kcHsContext, kcHsType,
  14
  15                 -- Typechecking kinded types
  16         tcHsKindedContext, tcHsKindedType, tcHsBangType,
  17         tcTyVarBndrs, dsHsType, tcLHsConSig, tcDataKindSig,
  18
  19         tcHsPatSigType, tcAddLetBoundTyVars,
  20
  21         TcSigInfo(..), TcSigFun, lookupSig
  22    ) where
  23
  24 #include "HsVersions.h"
  25
  26 import HsSyn            ( HsType(..), LHsType, HsTyVarBndr(..), LHsTyVarBndr, HsBang,
  27                           LHsContext, HsPred(..), LHsPred, LHsBinds, HsExplicitForAll(..),
  28                           getBangStrictness, collectSigTysFromHsBinds )
  29 import RnHsSyn          ( extractHsTyVars )
  30 import TcRnMonad
  31 import TcEnv            ( tcExtendTyVarEnv, tcExtendKindEnvTvs,
  32                           tcLookup, tcLookupClass, tcLookupTyCon,
  33                           TyThing(..), getInLocalScope, wrongThingErr
  34                         )
  35 import TcMType          ( newKindVar, newMetaTyVar, zonkTcKindToKind,
  36                           checkValidType, UserTypeCtxt(..), pprHsSigCtxt
  37                         )
  38 import TcUnify          ( unifyFunKind, checkExpectedKind )
  39 import TcIface          ( checkWiredInTyCon )
  40 import TcType           ( Type, PredType(..), ThetaType,
  41                           MetaDetails(Flexi), hoistForAllTys,
  42                           TcType, TcTyVar, TcKind, TcThetaType, TcTauType,
  43                           mkFunTy, mkSigmaTy, mkPredTy, mkGenTyConApp,
  44                           mkTyConApp, mkAppTys, typeKind )
  45 import Kind             ( Kind, isLiftedTypeKind, liftedTypeKind, ubxTupleKind,
  46                           openTypeKind, argTypeKind, splitKindFunTys )
  47 import Id               ( idName )
  48 import Var              ( TyVar, mkTyVar )
  49 import TyCon            ( TyCon, tyConKind )
  50 import Class            ( Class, classTyCon )
  51 import Name             ( Name, mkInternalName )
  52 import OccName          ( mkOccName, tvName )
  53 import NameSet
  54 import PrelNames        ( genUnitTyConName )
  55 import TysWiredIn       ( mkListTy, listTyCon, mkPArrTy, parrTyCon, tupleTyCon )
  56 import Bag              ( bagToList )
  57 import BasicTypes       ( Boxity(..) )
  58 import SrcLoc           ( Located(..), unLoc, noLoc, srcSpanStart )
  59 import UniqSupply       ( uniqsFromSupply )
  60 import Outputable
  61 \end{code}
  62
  63
  64         ----------------------------
  65                 General notes
  66         ----------------------------
  67
  68 Generally speaking we now type-check types in three phases
  69
  70   1.  kcHsType: kind check the HsType
  71         *includes* performing any TH type splices;
  72         so it returns a translated, and kind-annotated, type
  73
  74   2.  dsHsType: convert from HsType to Type:
  75         perform zonking
  76         expand type synonyms [mkGenTyApps]
  77         hoist the foralls [tcHsType]
  78
  79   3.  checkValidType: check the validity of the resulting type
  80
  81 Often these steps are done one after the other (tcHsSigType).
  82 But in mutually recursive groups of type and class decls we do
  83         1 kind-check the whole group
  84         2 build TyCons/Classes in a knot-tied way
  85         3 check the validity of types in the now-unknotted TyCons/Classes
  86
  87 For example, when we find
  88         (forall a m. m a -> m a)
  89 we bind a,m to kind varibles and kind-check (m a -> m a).  This makes
  90 a get kind *, and m get kind *->*.  Now we typecheck (m a -> m a) in
  91 an environment that binds a and m suitably.
  92
  93 The kind checker passed to tcHsTyVars needs to look at enough to
  94 establish the kind of the tyvar:
  95   * For a group of type and class decls, it's just the group, not
  96         the rest of the program
  97   * For a tyvar bound in a pattern type signature, its the types
  98         mentioned in the other type signatures in that bunch of patterns
  99   * For a tyvar bound in a RULE, it's the type signatures on other
 100         universally quantified variables in the rule
 101
 102 Note that this may occasionally give surprising results.  For example:
 103
 104         data T a b = MkT (a b)
 105
 106 Here we deduce                  a::*->*,       b::*
 107 But equally valid would be      a::(*->*)-> *, b::*->*
 108
 109
 110 Validity checking
 111 ~~~~~~~~~~~~~~~~~
 112 Some of the validity check could in principle be done by the kind checker,
 113 but not all:
 114
 115 - During desugaring, we normalise by expanding type synonyms.  Only
 116   after this step can we check things like type-synonym saturation
 117   e.g.  type T k = k Int
 118         type S a = a
 119   Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
 120   and then S is saturated.  This is a GHC extension.
 121
 122 - Similarly, also a GHC extension, we look through synonyms before complaining
 123   about the form of a class or instance declaration
 124
 125 - Ambiguity checks involve functional dependencies, and it's easier to wait
 126   until knots have been resolved before poking into them
 127
 128 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
 129 finished building the loop.  So to keep things simple, we postpone most validity
 130 checking until step (3).
 131
 132 Knot tying
 133 ~~~~~~~~~~
 134 During step (1) we might fault in a TyCon defined in another module, and it might
 135 (via a loop) refer back to a TyCon defined in this module. So when we tie a big
 136 knot around type declarations with ARecThing, so that the fault-in code can get
 137 the TyCon being defined.
 138
 139
 140 %************************************************************************
 141 %*                                                                      *
 142 \subsection{Checking types}
 143 %*                                                                      *
 144 %************************************************************************
 145
 146 \begin{code}
 147 tcHsSigType :: UserTypeCtxt -> LHsType Name -> TcM Type
 148   -- Do kind checking, and hoist for-alls to the top
 149   -- NB: it's important that the foralls that come from the top-level
 150   --     HsForAllTy in hs_ty occur *first* in the returned type.
 151   --     See Note [Scoped] with TcSigInfo
 152 tcHsSigType ctxt hs_ty
 153   = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
 154     do  { kinded_ty <- kcTypeType hs_ty
 155         ; ty <- tcHsKindedType kinded_ty
 156         ; checkValidType ctxt ty
 157         ; returnM ty }
 158
 159 -- Used for the deriving(...) items
 160 tcHsDeriv :: LHsType Name -> TcM ([TyVar], Class, [Type])
 161 tcHsDeriv = addLocM (tc_hs_deriv [])
 162
 163 tc_hs_deriv tv_names (HsPredTy (HsClassP cls_name hs_tys))
 164   = kcHsTyVars tv_names                 $ \ tv_names' ->
 165     do  { cls_kind <- kcClass cls_name
 166         ; (tys, res_kind) <- kcApps cls_kind (ppr cls_name) hs_tys
 167         ; tcTyVarBndrs tv_names'        $ \ tyvars ->
 168     do  { arg_tys <- dsHsTypes tys
 169         ; cls <- tcLookupClass cls_name
 170         ; return (tyvars, cls, arg_tys) }}
 171
 172 tc_hs_deriv tv_names1 (HsForAllTy _ tv_names2 (L _ []) (L _ ty))
 173   =     -- Funny newtype deriving form
 174         --      forall a. C [a]
 175         -- where C has arity 2.  Hence can't use regular functions
 176     tc_hs_deriv (tv_names1 ++ tv_names2) ty
 177
 178 tc_hs_deriv _ other
 179   = failWithTc (ptext SLIT("Illegal deriving item") <+> ppr other)
 180 \end{code}
 181
 182         These functions are used during knot-tying in
 183         type and class declarations, when we have to
 184         separate kind-checking, desugaring, and validity checking
 185
 186 \begin{code}
 187 kcHsSigType, kcHsLiftedSigType :: LHsType Name -> TcM (LHsType Name)
 188         -- Used for type signatures
 189 kcHsSigType ty       = kcTypeType ty
 190 kcHsLiftedSigType ty = kcLiftedType ty
 191
 192 tcHsKindedType :: LHsType Name -> TcM Type
 193   -- Don't do kind checking, nor validity checking,
 194   --    but do hoist for-alls to the top
 195   -- This is used in type and class decls, where kinding is
 196   -- done in advance, and validity checking is done later
 197   -- [Validity checking done later because of knot-tying issues.]
 198 tcHsKindedType hs_ty
 199   = do  { ty <- dsHsType hs_ty
 200         ; return (hoistForAllTys ty) }
 201
 202 tcHsBangType :: LHsType Name -> TcM Type
 203 -- Permit a bang, but discard it
 204 tcHsBangType (L span (HsBangTy b ty)) = tcHsKindedType ty
 205 tcHsBangType ty                       = tcHsKindedType ty
 206
 207 tcHsKindedContext :: LHsContext Name -> TcM ThetaType
 208 -- Used when we are expecting a ClassContext (i.e. no implicit params)
 209 -- Does not do validity checking, like tcHsKindedType
 210 tcHsKindedContext hs_theta = addLocM (mappM dsHsLPred) hs_theta
 211 \end{code}
 212
 213
 214 %************************************************************************
 215 %*                                                                      *
 216                 The main kind checker: kcHsType
 217 %*                                                                      *
 218 %************************************************************************
 219
 220         First a couple of simple wrappers for kcHsType
 221
 222 \begin{code}
 223 ---------------------------
 224 kcLiftedType :: LHsType Name -> TcM (LHsType Name)
 225 -- The type ty must be a *lifted* *type*
 226 kcLiftedType ty = kcCheckHsType ty liftedTypeKind
 227
 228 ---------------------------
 229 kcTypeType :: LHsType Name -> TcM (LHsType Name)
 230 -- The type ty must be a *type*, but it can be lifted or
 231 -- unlifted or an unboxed tuple.
 232 kcTypeType ty = kcCheckHsType ty openTypeKind
 233
 234 ---------------------------
 235 kcCheckHsType :: LHsType Name -> TcKind -> TcM (LHsType Name)
 236 -- Check that the type has the specified kind
 237 -- Be sure to use checkExpectedKind, rather than simply unifying
 238 -- with OpenTypeKind, because it gives better error messages
 239 kcCheckHsType (L span ty) exp_kind
 240   = setSrcSpan span                             $
 241     do  { (ty', act_kind) <- add_ctxt ty (kc_hs_type ty)
 242                 -- Add the context round the inner check only
 243                 -- because checkExpectedKind already mentions
 244                 -- 'ty' by name in any error message
 245
 246         ; checkExpectedKind ty act_kind exp_kind
 247         ; return (L span ty') }
 248   where
 249         -- Wrap a context around only if we want to
 250         -- show that contexts.  Omit invisble ones
 251         -- and ones user's won't grok (HsPred p).
 252     add_ctxt (HsPredTy p)                          thing = thing
 253     add_ctxt (HsForAllTy Implicit tvs (L _ []) ty) thing = thing
 254     add_ctxt other_ty thing = addErrCtxt (typeCtxt ty) thing
 255 \end{code}
 256
 257         Here comes the main function
 258
 259 \begin{code}
 260 kcHsType :: LHsType Name -> TcM (LHsType Name, TcKind)
 261 kcHsType ty = wrapLocFstM kc_hs_type ty
 262 -- kcHsType *returns* the kind of the type, rather than taking an expected
 263 -- kind as argument as tcExpr does.
 264 -- Reasons:
 265 --      (a) the kind of (->) is
 266 --              forall bx1 bx2. Type bx1 -> Type bx2 -> Type Boxed
 267 --          so we'd need to generate huge numbers of bx variables.
 268 --      (b) kinds are so simple that the error messages are fine
 269 --
 270 -- The translated type has explicitly-kinded type-variable binders
 271
 272 kc_hs_type (HsParTy ty)
 273  = kcHsType ty          `thenM` \ (ty', kind) ->
 274    returnM (HsParTy ty', kind)
 275
 276 kc_hs_type (HsTyVar name)
 277   = kcTyVar name        `thenM` \ kind ->
 278     returnM (HsTyVar name, kind)
 279
 280 kc_hs_type (HsListTy ty)
 281   = kcLiftedType ty                     `thenM` \ ty' ->
 282     returnM (HsListTy ty', liftedTypeKind)
 283
 284 kc_hs_type (HsPArrTy ty)
 285   = kcLiftedType ty                     `thenM` \ ty' ->
 286     returnM (HsPArrTy ty', liftedTypeKind)
 287
 288 kc_hs_type (HsNumTy n)
 289    = returnM (HsNumTy n, liftedTypeKind)
 290
 291 kc_hs_type (HsKindSig ty k)
 292   = kcCheckHsType ty k  `thenM` \ ty' ->
 293     returnM (HsKindSig ty' k, k)
 294
 295 kc_hs_type (HsTupleTy Boxed tys)
 296   = mappM kcLiftedType tys      `thenM` \ tys' ->
 297     returnM (HsTupleTy Boxed tys', liftedTypeKind)
 298
 299 kc_hs_type (HsTupleTy Unboxed tys)
 300   = mappM kcTypeType tys        `thenM` \ tys' ->
 301     returnM (HsTupleTy Unboxed tys', ubxTupleKind)
 302
 303 kc_hs_type (HsFunTy ty1 ty2)
 304   = kcCheckHsType ty1 argTypeKind       `thenM` \ ty1' ->
 305     kcTypeType ty2                      `thenM` \ ty2' ->
 306     returnM (HsFunTy ty1' ty2', liftedTypeKind)
 307
 308 kc_hs_type ty@(HsOpTy ty1 op ty2)
 309   = addLocM kcTyVar op                  `thenM` \ op_kind ->
 310     kcApps op_kind (ppr op) [ty1,ty2]   `thenM` \ ([ty1',ty2'], res_kind) ->
 311     returnM (HsOpTy ty1' op ty2', res_kind)
 312
 313 kc_hs_type ty@(HsAppTy ty1 ty2)
 314   = kcHsType fun_ty                       `thenM` \ (fun_ty', fun_kind) ->
 315     kcApps fun_kind (ppr fun_ty) arg_tys  `thenM` \ ((arg_ty':arg_tys'), res_kind) ->
 316     returnM (foldl mk_app (HsAppTy fun_ty' arg_ty') arg_tys', res_kind)
 317   where
 318     (fun_ty, arg_tys) = split ty1 [ty2]
 319     split (L _ (HsAppTy f a)) as = split f (a:as)
 320     split f                   as = (f,as)
 321     mk_app fun arg = HsAppTy (noLoc fun) arg    -- Add noLocs for inner nodes of
 322                                                 -- the application; they are never used
 323
 324 kc_hs_type (HsPredTy pred)
 325   = kcHsPred pred               `thenM` \ pred' ->
 326     returnM (HsPredTy pred', liftedTypeKind)
 327
 328 kc_hs_type (HsForAllTy exp tv_names context ty)
 329   = kcHsTyVars tv_names         $ \ tv_names' ->
 330     kcHsContext context         `thenM` \ ctxt' ->
 331     kcLiftedType ty             `thenM` \ ty' ->
 332         -- The body of a forall is usually a type, but in principle
 333         -- there's no reason to prohibit *unlifted* types.
 334         -- In fact, GHC can itself construct a function with an
 335         -- unboxed tuple inside a for-all (via CPR analyis; see
 336         -- typecheck/should_compile/tc170)
 337         --
 338         -- Still, that's only for internal interfaces, which aren't
 339         -- kind-checked, so we only allow liftedTypeKind here
 340     returnM (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind)
 341
 342 kc_hs_type (HsBangTy b ty)
 343   = do { (ty', kind) <- kcHsType ty
 344        ; return (HsBangTy b ty', kind) }
 345
 346 kc_hs_type ty@(HsSpliceTy _)
 347   = failWithTc (ptext SLIT("Unexpected type splice:") <+> ppr ty)
 348
 349
 350 ---------------------------
 351 kcApps :: TcKind                        -- Function kind
 352        -> SDoc                          -- Function
 353        -> [LHsType Name]                -- Arg types
 354        -> TcM ([LHsType Name], TcKind)  -- Kind-checked args
 355 kcApps fun_kind ppr_fun args
 356   = split_fk fun_kind (length args)     `thenM` \ (arg_kinds, res_kind) ->
 357     zipWithM kc_arg args arg_kinds      `thenM` \ args' ->
 358     returnM (args', res_kind)
 359   where
 360     split_fk fk 0 = returnM ([], fk)
 361     split_fk fk n = unifyFunKind fk     `thenM` \ mb_fk ->
 362                     case mb_fk of
 363                         Nothing       -> failWithTc too_many_args
 364                         Just (ak,fk') -> split_fk fk' (n-1)     `thenM` \ (aks, rk) ->
 365                                          returnM (ak:aks, rk)
 366
 367     kc_arg arg arg_kind = kcCheckHsType arg arg_kind
 368
 369     too_many_args = ptext SLIT("Kind error:") <+> quotes ppr_fun <+>
 370                     ptext SLIT("is applied to too many type arguments")
 371
 372 ---------------------------
 373 kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
 374 kcHsContext ctxt = wrapLocM (mappM kcHsLPred) ctxt
 375
 376 kcHsLPred :: LHsPred Name -> TcM (LHsPred Name)
 377 kcHsLPred = wrapLocM kcHsPred
 378
 379 kcHsPred :: HsPred Name -> TcM (HsPred Name)
 380 kcHsPred pred   -- Checks that the result is of kind liftedType
 381   = kc_pred pred                                `thenM` \ (pred', kind) ->
 382     checkExpectedKind pred kind liftedTypeKind  `thenM_`
 383     returnM pred'
 384
 385 ---------------------------
 386 kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)
 387         -- Does *not* check for a saturated
 388         -- application (reason: used from TcDeriv)
 389 kc_pred pred@(HsIParam name ty)
 390   = kcHsType ty         `thenM` \ (ty', kind) ->
 391     returnM (HsIParam name ty', kind)
 392
 393 kc_pred pred@(HsClassP cls tys)
 394   = kcClass cls                 `thenM` \ kind ->
 395     kcApps kind (ppr cls) tys   `thenM` \ (tys', res_kind) ->
 396     returnM (HsClassP cls tys', res_kind)
 397
 398 ---------------------------
 399 kcTyVar :: Name -> TcM TcKind
 400 kcTyVar name    -- Could be a tyvar or a tycon
 401   = traceTc (text "lk1" <+> ppr name)   `thenM_`
 402     tcLookup name       `thenM` \ thing ->
 403     traceTc (text "lk2" <+> ppr name <+> ppr thing)     `thenM_`
 404     case thing of
 405         ATyVar _ ty             -> returnM (typeKind ty)
 406         AThing kind             -> returnM kind
 407         AGlobal (ATyCon tc)     -> returnM (tyConKind tc)
 408         other                   -> wrongThingErr "type" thing name
 409
 410 kcClass :: Name -> TcM TcKind
 411 kcClass cls     -- Must be a class
 412   = tcLookup cls                                `thenM` \ thing ->
 413     case thing of
 414         AThing kind             -> returnM kind
 415         AGlobal (AClass cls)    -> returnM (tyConKind (classTyCon cls))
 416         other                   -> wrongThingErr "class" thing cls
 417 \end{code}
 418
 419
 420 %************************************************************************
 421 %*                                                                      *
 422                 Desugaring
 423 %*                                                                      *
 424 %************************************************************************
 425
 426 The type desugarer
 427
 428         * Transforms from HsType to Type
 429         * Zonks any kinds
 430
 431 It cannot fail, and does no validity checking, except for
 432 structural matters, such as
 433         (a) spurious ! annotations.
 434         (b) a class used as a type
 435
 436 \begin{code}
 437 dsHsType :: LHsType Name -> TcM Type
 438 -- All HsTyVarBndrs in the intput type are kind-annotated
 439 dsHsType ty = ds_type (unLoc ty)
 440
 441 ds_type ty@(HsTyVar name)
 442   = ds_app ty []
 443
 444 ds_type (HsParTy ty)            -- Remove the parentheses markers
 445   = dsHsType ty
 446
 447 ds_type ty@(HsBangTy _ _)       -- No bangs should be here
 448   = failWithTc (ptext SLIT("Unexpected strictness annotation:") <+> ppr ty)
 449
 450 ds_type (HsKindSig ty k)
 451   = dsHsType ty -- Kind checking done already
 452
 453 ds_type (HsListTy ty)
 454   = dsHsType ty                 `thenM` \ tau_ty ->
 455     checkWiredInTyCon listTyCon `thenM_`
 456     returnM (mkListTy tau_ty)
 457
 458 ds_type (HsPArrTy ty)
 459   = dsHsType ty                 `thenM` \ tau_ty ->
 460     checkWiredInTyCon parrTyCon `thenM_`
 461     returnM (mkPArrTy tau_ty)
 462
 463 ds_type (HsTupleTy boxity tys)
 464   = dsHsTypes tys               `thenM` \ tau_tys ->
 465     checkWiredInTyCon tycon     `thenM_`
 466     returnM (mkTyConApp tycon tau_tys)
 467   where
 468     tycon = tupleTyCon boxity (length tys)
 469
 470 ds_type (HsFunTy ty1 ty2)
 471   = dsHsType ty1                        `thenM` \ tau_ty1 ->
 472     dsHsType ty2                        `thenM` \ tau_ty2 ->
 473     returnM (mkFunTy tau_ty1 tau_ty2)
 474
 475 ds_type (HsOpTy ty1 (L span op) ty2)
 476   = dsHsType ty1                `thenM` \ tau_ty1 ->
 477     dsHsType ty2                `thenM` \ tau_ty2 ->
 478     setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
 479
 480 ds_type (HsNumTy n)
 481   = ASSERT(n==1)
 482     tcLookupTyCon genUnitTyConName      `thenM` \ tc ->
 483     returnM (mkTyConApp tc [])
 484
 485 ds_type ty@(HsAppTy _ _)
 486   = ds_app ty []
 487
 488 ds_type (HsPredTy pred)
 489   = dsHsPred pred       `thenM` \ pred' ->
 490     returnM (mkPredTy pred')
 491
 492 ds_type full_ty@(HsForAllTy exp tv_names ctxt ty)
 493   = tcTyVarBndrs tv_names               $ \ tyvars ->
 494     mappM dsHsLPred (unLoc ctxt)        `thenM` \ theta ->
 495     dsHsType ty                         `thenM` \ tau ->
 496     returnM (mkSigmaTy tyvars theta tau)
 497
 498 dsHsTypes arg_tys = mappM dsHsType arg_tys
 499 \end{code}
 500
 501 Help functions for type applications
 502 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 503
 504 \begin{code}
 505 ds_app :: HsType Name -> [LHsType Name] -> TcM Type
 506 ds_app (HsAppTy ty1 ty2) tys
 507   = ds_app (unLoc ty1) (ty2:tys)
 508
 509 ds_app ty tys
 510   = dsHsTypes tys                       `thenM` \ arg_tys ->
 511     case ty of
 512         HsTyVar fun -> ds_var_app fun arg_tys
 513         other       -> ds_type ty               `thenM` \ fun_ty ->
 514                        returnM (mkAppTys fun_ty arg_tys)
 515
 516 ds_var_app :: Name -> [Type] -> TcM Type
 517 ds_var_app name arg_tys
 518  = tcLookup name                        `thenM` \ thing ->
 519     case thing of
 520         ATyVar _ ty         -> returnM (mkAppTys ty arg_tys)
 521         AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
 522         other               -> wrongThingErr "type" thing name
 523 \end{code}
 524
 525
 526 Contexts
 527 ~~~~~~~~
 528
 529 \begin{code}
 530 dsHsLPred :: LHsPred Name -> TcM PredType
 531 dsHsLPred pred = dsHsPred (unLoc pred)
 532
 533 dsHsPred pred@(HsClassP class_name tys)
 534   = dsHsTypes tys                       `thenM` \ arg_tys ->
 535     tcLookupClass class_name            `thenM` \ clas ->
 536     returnM (ClassP clas arg_tys)
 537
 538 dsHsPred (HsIParam name ty)
 539   = dsHsType ty                                 `thenM` \ arg_ty ->
 540     returnM (IParam name arg_ty)
 541 \end{code}
 542
 543 GADT constructor signatures
 544
 545 \begin{code}
 546 tcLHsConSig :: LHsType Name
 547             -> TcM ([TcTyVar], TcThetaType,
 548                     [HsBang], [TcType],
 549                     TyCon, [TcType])
 550 -- Take apart the type signature for a data constructor
 551 -- The difference is that there can be bangs at the top of
 552 -- the argument types, and kind-checking is the right place to check
 553 tcLHsConSig sig@(L span (HsForAllTy exp tv_names ctxt ty))
 554   = setSrcSpan span             $
 555     addErrCtxt (gadtSigCtxt sig) $
 556     tcTyVarBndrs tv_names       $ \ tyvars ->
 557     do  { theta <- mappM dsHsLPred (unLoc ctxt)
 558         ; (bangs, arg_tys, tc, res_tys) <- tc_con_sig_tau ty
 559         ; return (tyvars, theta, bangs, arg_tys, tc, res_tys) }
 560 tcLHsConSig ty
 561   = do  { (bangs, arg_tys, tc, res_tys) <- tc_con_sig_tau ty
 562         ; return ([], [], bangs, arg_tys, tc, res_tys) }
 563
 564 --------
 565 tc_con_sig_tau (L _ (HsFunTy arg ty))
 566   = do  { (bangs, arg_tys, tc, res_tys) <- tc_con_sig_tau ty
 567         ; arg_ty <- tcHsBangType arg
 568         ; return (getBangStrictness arg : bangs,
 569                   arg_ty : arg_tys, tc, res_tys) }
 570
 571 tc_con_sig_tau ty
 572   = do  { (tc, res_tys) <- tc_con_res ty []
 573         ; return ([], [], tc, res_tys) }
 574
 575 --------
 576 tc_con_res (L _ (HsAppTy fun res_ty)) res_tys
 577   = do  { res_ty' <- dsHsType res_ty
 578         ; tc_con_res fun (res_ty' : res_tys) }
 579
 580 tc_con_res ty@(L _ (HsTyVar name)) res_tys
 581   = do  { thing <- tcLookup name
 582         ; case thing of
 583             AGlobal (ATyCon tc) -> return (tc, res_tys)
 584             other -> failWithTc (badGadtDecl ty)
 585         }
 586
 587 tc_con_res ty _ = failWithTc (badGadtDecl ty)
 588
 589 gadtSigCtxt ty
 590   = hang (ptext SLIT("In the signature of a data constructor:"))
 591        2 (ppr ty)
 592 badGadtDecl ty
 593   = hang (ptext SLIT("Malformed constructor signature:"))
 594        2 (ppr ty)
 595
 596 typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
 597 \end{code}
 598
 599 %************************************************************************
 600 %*                                                                      *
 601                 Type-variable binders
 602 %*                                                                      *
 603 %************************************************************************
 604
 605
 606 \begin{code}
 607 kcHsTyVars :: [LHsTyVarBndr Name]
 608            -> ([LHsTyVarBndr Name] -> TcM r)    -- These binders are kind-annotated
 609                                                 -- They scope over the thing inside
 610            -> TcM r
 611 kcHsTyVars tvs thing_inside
 612   = mappM (wrapLocM kcHsTyVar) tvs      `thenM` \ bndrs ->
 613     tcExtendKindEnvTvs bndrs (thing_inside bndrs)
 614
 615 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
 616         -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it
 617 kcHsTyVar (UserTyVar name)        = newKindVar  `thenM` \ kind ->
 618                                     returnM (KindedTyVar name kind)
 619 kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind)
 620
 621 ------------------
 622 tcTyVarBndrs :: [LHsTyVarBndr Name]     -- Kind-annotated binders, which need kind-zonking
 623              -> ([TyVar] -> TcM r)
 624              -> TcM r
 625 -- Used when type-checking types/classes/type-decls
 626 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
 627 tcTyVarBndrs bndrs thing_inside
 628   = mapM (zonk . unLoc) bndrs   `thenM` \ tyvars ->
 629     tcExtendTyVarEnv tyvars (thing_inside tyvars)
 630   where
 631     zonk (KindedTyVar name kind) = zonkTcKindToKind kind        `thenM` \ kind' ->
 632                                    returnM (mkTyVar name kind')
 633     zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $
 634                             returnM (mkTyVar name liftedTypeKind)
 635
 636 -----------------------------------
 637 tcDataKindSig :: Maybe Kind -> TcM [TyVar]
 638 -- GADT decls can have a (perhpas partial) kind signature
 639 --      e.g.  data T :: * -> * -> * where ...
 640 -- This function makes up suitable (kinded) type variables for
 641 -- the argument kinds, and checks that the result kind is indeed *
 642 tcDataKindSig Nothing = return []
 643 tcDataKindSig (Just kind)
 644   = do  { checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
 645         ; span <- getSrcSpanM
 646         ; us   <- newUniqueSupply
 647         ; let loc   = srcSpanStart span
 648               uniqs = uniqsFromSupply us
 649         ; return [ mk_tv loc uniq str kind
 650                  | ((kind, str), uniq) <- arg_kinds `zip` names `zip` uniqs ] }
 651   where
 652     (arg_kinds, res_kind) = splitKindFunTys kind
 653     mk_tv loc uniq str kind = mkTyVar name kind
 654         where
 655            name = mkInternalName uniq occ loc
 656            occ  = mkOccName tvName str
 657
 658     names :: [String]   -- a,b,c...aa,ab,ac etc
 659     names = [ c:cs | cs <- "" : names, c <- ['a'..'z'] ]
 660
 661 badKindSig :: Kind -> SDoc
 662 badKindSig kind
 663  = hang (ptext SLIT("Kind signature on data type declaration has non-* return kind"))
 664         2 (ppr kind)
 665 \end{code}
 666
 667
 668 %************************************************************************
 669 %*                                                                      *
 670                 Scoped type variables
 671 %*                                                                      *
 672 %************************************************************************
 673
 674
 675 tcAddScopedTyVars is used for scoped type variables added by pattern
 676 type signatures
 677         e.g.  \ ((x::a), (y::a)) -> x+y
 678 They never have explicit kinds (because this is source-code only)
 679 They are mutable (because they can get bound to a more specific type).
 680
 681 Usually we kind-infer and expand type splices, and then
 682 tupecheck/desugar the type.  That doesn't work well for scoped type
 683 variables, because they scope left-right in patterns.  (e.g. in the
 684 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
 685
 686 The current not-very-good plan is to
 687   * find all the types in the patterns
 688   * find their free tyvars
 689   * do kind inference
 690   * bring the kinded type vars into scope
 691   * BUT throw away the kind-checked type
 692         (we'll kind-check it again when we type-check the pattern)
 693
 694 This is bad because throwing away the kind checked type throws away
 695 its splices.  But too bad for now.  [July 03]
 696
 697 Historical note:
 698     We no longer specify that these type variables must be univerally
 699     quantified (lots of email on the subject).  If you want to put that
 700     back in, you need to
 701         a) Do a checkSigTyVars after thing_inside
 702         b) More insidiously, don't pass in expected_ty, else
 703            we unify with it too early and checkSigTyVars barfs
 704            Instead you have to pass in a fresh ty var, and unify
 705            it with expected_ty afterwards
 706
 707 \begin{code}
 708 tcPatSigBndrs :: LHsType Name
 709               -> TcM ([TcTyVar],        -- Brought into scope
 710                       LHsType Name)     -- Kinded, but not yet desugared
 711
 712 tcPatSigBndrs hs_ty
 713   = do  { in_scope <- getInLocalScope
 714         ; span <- getSrcSpanM
 715         ; let sig_tvs = [ L span (UserTyVar n)
 716                         | n <- nameSetToList (extractHsTyVars hs_ty),
 717                           not (in_scope n) ]
 718                 -- The tyvars we want are the free type variables of
 719                 -- the type that are not already in scope
 720
 721         -- Behave like kcHsType on a ForAll type
 722         -- i.e. make kinded tyvars with mutable kinds,
 723         --      and kind-check the enclosed types
 724         ; (kinded_tvs, kinded_ty) <- kcHsTyVars sig_tvs $ \ kinded_tvs -> do
 725                                     { kinded_ty <- kcTypeType hs_ty
 726                                     ; return (kinded_tvs, kinded_ty) }
 727
 728         -- Zonk the mutable kinds and bring the tyvars into scope
 729         -- Just like the call to tcTyVarBndrs in ds_type (HsForAllTy case),
 730         -- except that it brings *meta* tyvars into scope, not regular ones
 731         --
 732         --      [Out of date, but perhaps should be resurrected]
 733         -- Furthermore, the tyvars are PatSigTvs, which means that we get better
 734         -- error messages when type variables escape:
 735         --      Inferred type is less polymorphic than expected
 736         --      Quantified type variable `t' escapes
 737         --      It is mentioned in the environment:
 738         --      t is bound by the pattern type signature at tcfail103.hs:6
 739         ; tyvars <- mapM (zonk . unLoc) kinded_tvs
 740         ; return (tyvars, kinded_ty) }
 741   where
 742     zonk (KindedTyVar name kind) = zonkTcKindToKind kind        `thenM` \ kind' ->
 743                                    newMetaTyVar name kind' Flexi
 744         -- Scoped type variables are bound to a *type*, hence Flexi
 745     zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $
 746                             returnM (mkTyVar name liftedTypeKind)
 747
 748 tcHsPatSigType :: UserTypeCtxt
 749                -> LHsType Name          -- The type signature
 750                -> TcM ([TcTyVar],       -- Newly in-scope type variables
 751                         TcType)         -- The signature
 752
 753 tcHsPatSigType ctxt hs_ty
 754   = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
 755     do  { (tyvars, kinded_ty) <- tcPatSigBndrs hs_ty
 756
 757          -- Complete processing of the type, and check its validity
 758         ; tcExtendTyVarEnv tyvars $ do
 759                 { sig_ty <- tcHsKindedType kinded_ty
 760                 ; checkValidType ctxt sig_ty
 761                 ; return (tyvars, sig_ty) }
 762         }
 763
 764 tcAddLetBoundTyVars :: LHsBinds Name -> TcM a -> TcM a
 765 -- Turgid funciton, used for type variables bound by the patterns of a let binding
 766
 767 tcAddLetBoundTyVars binds thing_inside
 768   = go (collectSigTysFromHsBinds (bagToList binds)) thing_inside
 769   where
 770     go [] thing_inside = thing_inside
 771     go (hs_ty:hs_tys) thing_inside
 772         = do { (tyvars, _kinded_ty) <- tcPatSigBndrs hs_ty
 773              ; tcExtendTyVarEnv tyvars (go hs_tys thing_inside) }
 774 \end{code}
 775
 776
 777 %************************************************************************
 778 %*                                                                      *
 779 \subsection{Signatures}
 780 %*                                                                      *
 781 %************************************************************************
 782
 783 @tcSigs@ checks the signatures for validity, and returns a list of
 784 {\em freshly-instantiated} signatures.  That is, the types are already
 785 split up, and have fresh type variables installed.  All non-type-signature
 786 "RenamedSigs" are ignored.
 787
 788 The @TcSigInfo@ contains @TcTypes@ because they are unified with
 789 the variable's type, and after that checked to see whether they've
 790 been instantiated.
 791
 792 \begin{code}
 793 data TcSigInfo
 794   = TcSigInfo {
 795         sig_id     :: TcId,             --  *Polymorphic* binder for this value...
 796
 797         sig_scoped :: [Name],           -- Names for any scoped type variables
 798                                         -- Invariant: correspond 1-1 with an initial
 799                                         -- segment of sig_tvs (see Note [Scoped])
 800
 801         sig_tvs    :: [TcTyVar],        -- Instantiated type variables
 802                                         -- See Note [Instantiate sig]
 803
 804         sig_theta  :: TcThetaType,      -- Instantiated theta
 805         sig_tau    :: TcTauType,        -- Instantiated tau
 806         sig_loc    :: InstLoc           -- The location of the signature
 807     }
 808
 809 --      Note [Scoped]
 810 -- There may be more instantiated type variables than scoped
 811 -- ones.  For example:
 812 --      type T a = forall b. b -> (a,b)
 813 --      f :: forall c. T c
 814 -- Here, the signature for f will have one scoped type variable, c,
 815 -- but two instantiated type variables, c' and b'.
 816 --
 817 -- We assume that the scoped ones are at the *front* of sig_tvs,
 818 -- and remember the names from the original HsForAllTy in sig_scoped
 819
 820 --      Note [Instantiate sig]
 821 -- It's vital to instantiate a type signature with fresh variable.
 822 -- For example:
 823 --      type S = forall a. a->a
 824 --      f,g :: S
 825 --      f = ...
 826 --      g = ...
 827 -- Here, we must use distinct type variables when checking f,g's right hand sides.
 828 -- (Instantiation is only necessary because of type synonyms.  Otherwise,
 829 -- it's all cool; each signature has distinct type variables from the renamer.)
 830
 831 type TcSigFun = Name -> Maybe TcSigInfo
 832
 833 instance Outputable TcSigInfo where
 834     ppr (TcSigInfo { sig_id = id, sig_tvs = tyvars, sig_theta = theta, sig_tau = tau})
 835         = ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
 836
 837 lookupSig :: [TcSigInfo] -> TcSigFun    -- Search for a particular signature
 838 lookupSig [] name = Nothing
 839 lookupSig (sig : sigs) name
 840   | name == idName (sig_id sig) = Just sig
 841   | otherwise                   = lookupSig sigs name
 842 \end{code}
 843