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