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