ghc/compiler/typecheck/TcMonoType.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 TcMonoType ( tcHsSigType, tcHsType, tcIfaceType, tcHsTheta, tcHsPred,
   8                     UserTypeCtxt(..),
   9
  10                         -- Kind checking
  11                     kcHsTyVar, kcHsTyVars, mkTyClTyVars,
  12                     kcHsType, kcHsSigType, kcHsSigTypes,
  13                     kcHsLiftedSigType, kcHsContext,
  14                     tcAddScopedTyVars, tcHsTyVars, mkImmutTyVars,
  15
  16                     TcSigInfo(..), tcTySig, mkTcSig, maybeSig, tcSigPolyId, tcSigMonoId
  17                   ) where
  18
  19 #include "HsVersions.h"
  20
  21 import HsSyn            ( HsType(..), HsTyVarBndr(..), HsTyOp(..),
  22                           Sig(..), HsPred(..), pprParendHsType, HsTupCon(..), hsTyVarNames )
  23 import RnHsSyn          ( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig, extractHsTyVars )
  24 import TcHsSyn          ( TcId )
  25
  26 import TcMonad
  27 import TcEnv            ( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
  28                           tcInLocalScope,
  29                           TyThing(..), TcTyThing(..), tcExtendKindEnv
  30                         )
  31 import TcMType          ( newKindVar, zonkKindEnv, tcInstType,
  32                           checkValidType, UserTypeCtxt(..), pprUserTypeCtxt
  33                         )
  34 import TcUnify          ( unifyKind, unifyOpenTypeKind )
  35 import TcType           ( Type, Kind, SourceType(..), ThetaType, TyVarDetails(..),
  36                           TcTyVar, TcKind, TcThetaType, TcTauType,
  37                           mkTyVarTy, mkTyVarTys, mkFunTy,
  38                           zipFunTys, mkForAllTys, mkFunTys, tcEqType, isPredTy,
  39                           mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys,
  40                           liftedTypeKind, unliftedTypeKind, mkArrowKind,
  41                           mkArrowKinds, tcSplitFunTy_maybe, tcSplitForAllTys
  42                         )
  43 import Inst             ( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
  44
  45 import Id               ( mkLocalId, idName, idType )
  46 import Var              ( TyVar, mkTyVar, tyVarKind )
  47 import ErrUtils         ( Message )
  48 import TyCon            ( TyCon, tyConKind )
  49 import Class            ( classTyCon )
  50 import Name             ( Name )
  51 import NameSet
  52 import Subst            ( deShadowTy )
  53 import TysWiredIn       ( mkListTy, mkPArrTy, mkTupleTy, genUnitTyCon )
  54 import BasicTypes       ( Boxity(..) )
  55 import SrcLoc           ( SrcLoc )
  56 import Util             ( lengthIs )
  57 import Outputable
  58 import List             ( nubBy )
  59 \end{code}
  60
  61
  62 %************************************************************************
  63 %*                                                                      *
  64 \subsection{Checking types}
  65 %*                                                                      *
  66 %************************************************************************
  67
  68 Generally speaking we now type-check types in three phases
  69
  70         1.  Kind check the HsType [kcHsType]
  71         2.  Convert from HsType to Type, and hoist the foralls [tcHsType]
  72         3.  Check the validity of the resulting type [checkValidType]
  73
  74 Often these steps are done one after the othe (tcHsSigType).
  75 But in mutually recursive groups of type and class decls we do
  76         1 kind-check the whole group
  77         2 build TyCons/Classes in a knot-tied wa
  78         3 check the validity of types in the now-unknotted TyCons/Classes
  79
  80 \begin{code}
  81 tcHsSigType :: UserTypeCtxt -> RenamedHsType -> TcM Type
  82   -- Do kind checking, and hoist for-alls to the top
  83 tcHsSigType ctxt ty = tcAddErrCtxt (checkTypeCtxt ctxt ty) (
  84                         kcTypeType ty           `thenTc_`
  85                         tcHsType ty
  86                       )                         `thenTc` \ ty' ->
  87                       checkValidType ctxt ty'   `thenTc_`
  88                       returnTc ty'
  89
  90 checkTypeCtxt ctxt ty
  91   = vcat [ptext SLIT("In the type:") <+> ppr ty,
  92           ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
  93
  94 tcHsType    :: RenamedHsType -> TcM Type
  95   -- Don't do kind checking, nor validity checking,
  96   --    but do hoist for-alls to the top
  97   -- This is used in type and class decls, where kinding is
  98   -- done in advance, and validity checking is done later
  99   -- [Validity checking done later because of knot-tying issues.]
 100 tcHsType ty = tc_type ty  `thenTc` \ ty' ->
 101               returnTc (hoistForAllTys ty')
 102
 103 tcHsTheta :: RenamedContext -> TcM ThetaType
 104 -- Used when we are expecting a ClassContext (i.e. no implicit params)
 105 -- Does not do validity checking, like tcHsType
 106 tcHsTheta hs_theta = mapTc tc_pred hs_theta
 107
 108 -- In interface files the type is already kinded,
 109 -- and we definitely don't want to hoist for-alls.
 110 -- Otherwise we'll change
 111 --      dmfail :: forall m:(*->*) Monad m => forall a:* => String -> m a
 112 -- into
 113 --      dmfail :: forall m:(*->*) a:* Monad m => String -> m a
 114 -- which definitely isn't right!
 115 tcIfaceType ty = tc_type ty
 116 \end{code}
 117
 118
 119 %************************************************************************
 120 %*                                                                      *
 121 \subsection{Kind checking}
 122 %*                                                                      *
 123 %************************************************************************
 124
 125 Kind checking
 126 ~~~~~~~~~~~~~
 127 When we come across the binding site for some type variables, we
 128 proceed in two stages
 129
 130 1. Figure out what kind each tyvar has
 131
 132 2. Create suitably-kinded tyvars,
 133    extend the envt,
 134    and typecheck the body
 135
 136 To do step 1, we proceed thus:
 137
 138 1a. Bind each type variable to a kind variable
 139 1b. Apply the kind checker
 140 1c. Zonk the resulting kinds
 141
 142 The kind checker is passed to tcHsTyVars as an argument.
 143
 144 For example, when we find
 145         (forall a m. m a -> m a)
 146 we bind a,m to kind varibles and kind-check (m a -> m a).  This
 147 makes a get kind *, and m get kind *->*.  Now we typecheck (m a -> m a)
 148 in an environment that binds a and m suitably.
 149
 150 The kind checker passed to tcHsTyVars needs to look at enough to
 151 establish the kind of the tyvar:
 152   * For a group of type and class decls, it's just the group, not
 153         the rest of the program
 154   * For a tyvar bound in a pattern type signature, its the types
 155         mentioned in the other type signatures in that bunch of patterns
 156   * For a tyvar bound in a RULE, it's the type signatures on other
 157         universally quantified variables in the rule
 158
 159 Note that this may occasionally give surprising results.  For example:
 160
 161         data T a b = MkT (a b)
 162
 163 Here we deduce                  a::*->*, b::*.
 164 But equally valid would be
 165                                 a::(*->*)-> *, b::*->*
 166
 167 \begin{code}
 168 -- tcHsTyVars is used for type variables in type signatures
 169 --      e.g. forall a. a->a
 170 -- They are immutable, because they scope only over the signature
 171 -- They may or may not be explicitly-kinded
 172 tcHsTyVars :: [HsTyVarBndr Name]
 173            -> TcM a                             -- The kind checker
 174            -> ([TyVar] -> TcM b)
 175            -> TcM b
 176
 177 tcHsTyVars [] kind_check thing_inside = thing_inside []
 178         -- A useful short cut for a common case!
 179
 180 tcHsTyVars tv_names kind_check thing_inside
 181   = kcHsTyVars tv_names                                 `thenNF_Tc` \ tv_names_w_kinds ->
 182     tcExtendKindEnv tv_names_w_kinds kind_check         `thenTc_`
 183     zonkKindEnv tv_names_w_kinds                        `thenNF_Tc` \ tvs_w_kinds ->
 184     let
 185         tyvars = mkImmutTyVars tvs_w_kinds
 186     in
 187     tcExtendTyVarEnv tyvars (thing_inside tyvars)
 188
 189
 190
 191 tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
 192 -- tcAddScopedTyVars is used for scoped type variables
 193 -- added by pattern type signatures
 194 --      e.g.  \ (x::a) (y::a) -> x+y
 195 -- They never have explicit kinds (because this is source-code only)
 196 -- They are mutable (because they can get bound to a more specific type)
 197
 198 -- Find the not-already-in-scope signature type variables,
 199 -- kind-check them, and bring them into scope
 200 --
 201 -- We no longer specify that these type variables must be univerally
 202 -- quantified (lots of email on the subject).  If you want to put that
 203 -- back in, you need to
 204 --      a) Do a checkSigTyVars after thing_inside
 205 --      b) More insidiously, don't pass in expected_ty, else
 206 --         we unify with it too early and checkSigTyVars barfs
 207 --         Instead you have to pass in a fresh ty var, and unify
 208 --         it with expected_ty afterwards
 209 tcAddScopedTyVars [] thing_inside
 210   = thing_inside        -- Quick get-out for the empty case
 211
 212 tcAddScopedTyVars sig_tys thing_inside
 213   = tcGetEnv                                    `thenNF_Tc` \ env ->
 214     let
 215         all_sig_tvs     = foldr (unionNameSets . extractHsTyVars) emptyNameSet sig_tys
 216         sig_tvs         = filter not_in_scope (nameSetToList all_sig_tvs)
 217         not_in_scope tv = not (tcInLocalScope env tv)
 218     in
 219     mapNF_Tc newNamedKindVar sig_tvs                    `thenTc` \ kind_env ->
 220     tcExtendKindEnv kind_env (kcHsSigTypes sig_tys)     `thenTc_`
 221     zonkKindEnv kind_env                                `thenNF_Tc` \ tvs_w_kinds ->
 222     listTc [ tcNewMutTyVar name kind PatSigTv
 223            | (name, kind) <- tvs_w_kinds]               `thenNF_Tc` \ tyvars ->
 224     tcExtendTyVarEnv tyvars thing_inside
 225 \end{code}
 226
 227
 228 \begin{code}
 229 kcHsTyVar  :: HsTyVarBndr name   -> NF_TcM (name, TcKind)
 230 kcHsTyVars :: [HsTyVarBndr name] -> NF_TcM [(name, TcKind)]
 231
 232 kcHsTyVar (UserTyVar name)       = newNamedKindVar name
 233 kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (name, kind)
 234
 235 kcHsTyVars tvs = mapNF_Tc kcHsTyVar tvs
 236
 237 newNamedKindVar name = newKindVar       `thenNF_Tc` \ kind ->
 238                        returnNF_Tc (name, kind)
 239
 240 ---------------------------
 241 kcLiftedType :: RenamedHsType -> TcM ()
 242         -- The type ty must be a *lifted* *type*
 243 kcLiftedType ty
 244   = kcHsType ty                         `thenTc` \ kind ->
 245     tcAddErrCtxt (typeKindCtxt ty)      $
 246     unifyKind liftedTypeKind kind
 247
 248 ---------------------------
 249 kcTypeType :: RenamedHsType -> TcM ()
 250         -- The type ty must be a *type*, but it can be lifted or unlifted.
 251 kcTypeType ty
 252   = kcHsType ty                         `thenTc` \ kind ->
 253     tcAddErrCtxt (typeKindCtxt ty)      $
 254     unifyOpenTypeKind kind
 255
 256 ---------------------------
 257 kcHsSigType, kcHsLiftedSigType :: RenamedHsType -> TcM ()
 258         -- Used for type signatures
 259 kcHsSigType       = kcTypeType
 260 kcHsSigTypes tys  = mapTc_ kcHsSigType tys
 261 kcHsLiftedSigType = kcLiftedType
 262
 263 ---------------------------
 264 kcHsType :: RenamedHsType -> TcM TcKind
 265 kcHsType (HsTyVar name)       = kcTyVar name
 266
 267 kcHsType (HsKindSig ty k)
 268   = kcHsType ty                 `thenTc` \ k' ->
 269     unifyKind k k'              `thenTc_`
 270     returnTc k
 271
 272 kcHsType (HsListTy ty)
 273   = kcLiftedType ty             `thenTc` \ tau_ty ->
 274     returnTc liftedTypeKind
 275
 276 kcHsType (HsPArrTy ty)
 277   = kcLiftedType ty             `thenTc` \ tau_ty ->
 278     returnTc liftedTypeKind
 279
 280 kcHsType (HsTupleTy (HsTupCon _ boxity _) tys)
 281   = mapTc kcTypeType tys        `thenTc_`
 282     returnTc (case boxity of
 283                   Boxed   -> liftedTypeKind
 284                   Unboxed -> unliftedTypeKind)
 285
 286 kcHsType (HsFunTy ty1 ty2)
 287   = kcTypeType ty1      `thenTc_`
 288     kcTypeType ty2      `thenTc_`
 289     returnTc liftedTypeKind
 290
 291 kcHsType (HsOpTy ty1 HsArrow ty2)
 292   = kcTypeType ty1      `thenTc_`
 293     kcTypeType ty2      `thenTc_`
 294     returnTc liftedTypeKind
 295
 296 kcHsType ty@(HsOpTy ty1 (HsTyOp op) ty2)
 297   = kcTyVar op                          `thenTc` \ op_kind ->
 298     kcHsType ty1                        `thenTc` \ ty1_kind ->
 299     kcHsType ty2                        `thenTc` \ ty2_kind ->
 300     tcAddErrCtxt (appKindCtxt (ppr ty)) $
 301     kcAppKind op_kind  ty1_kind         `thenTc` \ op_kind' ->
 302     kcAppKind op_kind' ty2_kind
 303
 304 kcHsType (HsParTy ty)           -- Skip parentheses markers
 305   = kcHsType ty
 306
 307 kcHsType (HsNumTy _)            -- The unit type for generics
 308   = returnTc liftedTypeKind
 309
 310 kcHsType (HsPredTy pred)
 311   = kcHsPred pred               `thenTc_`
 312     returnTc liftedTypeKind
 313
 314 kcHsType ty@(HsAppTy ty1 ty2)
 315   = kcHsType ty1                        `thenTc` \ tc_kind ->
 316     kcHsType ty2                        `thenTc` \ arg_kind ->
 317     tcAddErrCtxt (appKindCtxt (ppr ty)) $
 318     kcAppKind tc_kind arg_kind
 319
 320 kcHsType (HsForAllTy (Just tv_names) context ty)
 321   = kcHsTyVars tv_names         `thenNF_Tc` \ kind_env ->
 322     tcExtendKindEnv kind_env    $
 323     kcHsContext context         `thenTc_`
 324     kcHsType ty                 `thenTc_`
 325     returnTc liftedTypeKind
 326
 327 ---------------------------
 328 kcAppKind fun_kind arg_kind
 329   = case tcSplitFunTy_maybe fun_kind of
 330         Just (arg_kind', res_kind)
 331                 -> unifyKind arg_kind arg_kind' `thenTc_`
 332                    returnTc res_kind
 333
 334         Nothing -> newKindVar                                           `thenNF_Tc` \ res_kind ->
 335                    unifyKind fun_kind (mkArrowKind arg_kind res_kind)   `thenTc_`
 336                    returnTc res_kind
 337
 338
 339 ---------------------------
 340 kc_pred :: RenamedHsPred -> TcM TcKind  -- Does *not* check for a saturated
 341                                         -- application (reason: used from TcDeriv)
 342 kc_pred pred@(HsIParam name ty)
 343   = kcHsType ty
 344
 345 kc_pred pred@(HsClassP cls tys)
 346   = kcClass cls                         `thenTc` \ kind ->
 347     mapTc kcHsType tys                  `thenTc` \ arg_kinds ->
 348     newKindVar                          `thenNF_Tc` \ kv ->
 349     unifyKind kind (mkArrowKinds arg_kinds kv)  `thenTc_`
 350     returnTc kv
 351
 352 ---------------------------
 353 kcHsContext ctxt = mapTc_ kcHsPred ctxt
 354
 355 kcHsPred pred           -- Checks that the result is of kind liftedType
 356   = tcAddErrCtxt (appKindCtxt (ppr pred))       $
 357     kc_pred pred                                `thenTc` \ kind ->
 358     unifyKind liftedTypeKind kind               `thenTc_`
 359     returnTc ()
 360
 361
 362  ---------------------------
 363 kcTyVar name    -- Could be a tyvar or a tycon
 364   = tcLookup name       `thenTc` \ thing ->
 365     case thing of
 366         AThing kind         -> returnTc kind
 367         ATyVar tv           -> returnTc (tyVarKind tv)
 368         AGlobal (ATyCon tc) -> returnTc (tyConKind tc)
 369         other               -> failWithTc (wrongThingErr "type" thing name)
 370
 371 kcClass cls     -- Must be a class
 372   = tcLookup cls                                `thenNF_Tc` \ thing ->
 373     case thing of
 374         AThing kind           -> returnTc kind
 375         AGlobal (AClass cls)  -> returnTc (tyConKind (classTyCon cls))
 376         other                 -> failWithTc (wrongThingErr "class" thing cls)
 377 \end{code}
 378
 379 %************************************************************************
 380 %*                                                                      *
 381 \subsection{tc_type}
 382 %*                                                                      *
 383 %************************************************************************
 384
 385 tc_type, the main work horse
 386 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 387
 388         -------------------
 389         *** BIG WARNING ***
 390         -------------------
 391
 392 tc_type is used to typecheck the types in the RHS of data
 393 constructors.  In the case of recursive data types, that means that
 394 the type constructors themselves are (partly) black holes.  e.g.
 395
 396         data T a = MkT a [T a]
 397
 398 While typechecking the [T a] on the RHS, T itself is not yet fully
 399 defined.  That in turn places restrictions on what you can check in
 400 tcHsType; if you poke on too much you get a black hole.  I keep
 401 forgetting this, hence this warning!
 402
 403 So tc_type does no validity-checking.  Instead that's all done
 404 by TcMType.checkValidType
 405
 406         --------------------------
 407         *** END OF BIG WARNING ***
 408         --------------------------
 409
 410
 411 \begin{code}
 412 tc_type :: RenamedHsType -> TcM Type
 413
 414 tc_type ty@(HsTyVar name)
 415   = tc_app ty []
 416
 417 tc_type (HsKindSig ty k)
 418   = tc_type ty  -- Kind checking done already
 419
 420 tc_type (HsListTy ty)
 421   = tc_type ty  `thenTc` \ tau_ty ->
 422     returnTc (mkListTy tau_ty)
 423
 424 tc_type (HsPArrTy ty)
 425   = tc_type ty  `thenTc` \ tau_ty ->
 426     returnTc (mkPArrTy tau_ty)
 427
 428 tc_type (HsTupleTy (HsTupCon _ boxity arity) tys)
 429   = ASSERT( tys `lengthIs` arity )
 430     tc_types tys        `thenTc` \ tau_tys ->
 431     returnTc (mkTupleTy boxity arity tau_tys)
 432
 433 tc_type (HsFunTy ty1 ty2)
 434   = tc_type ty1                 `thenTc` \ tau_ty1 ->
 435     tc_type ty2                 `thenTc` \ tau_ty2 ->
 436     returnTc (mkFunTy tau_ty1 tau_ty2)
 437
 438 tc_type (HsOpTy ty1 HsArrow ty2)
 439   = tc_type ty1 `thenTc` \ tau_ty1 ->
 440     tc_type ty2 `thenTc` \ tau_ty2 ->
 441     returnTc (mkFunTy tau_ty1 tau_ty2)
 442
 443 tc_type (HsOpTy ty1 (HsTyOp op) ty2)
 444   = tc_type ty1 `thenTc` \ tau_ty1 ->
 445     tc_type ty2 `thenTc` \ tau_ty2 ->
 446     tc_fun_type op [tau_ty1,tau_ty2]
 447
 448 tc_type (HsParTy ty)            -- Remove the parentheses markers
 449   = tc_type ty
 450
 451 tc_type (HsNumTy n)
 452   = ASSERT(n== 1)
 453     returnTc (mkTyConApp genUnitTyCon [])
 454
 455 tc_type (HsAppTy ty1 ty2) = tc_app ty1 [ty2]
 456
 457 tc_type (HsPredTy pred)
 458   = tc_pred pred        `thenTc` \ pred' ->
 459     returnTc (mkPredTy pred')
 460
 461 tc_type full_ty@(HsForAllTy (Just tv_names) ctxt ty)
 462   = let
 463         kind_check = kcHsContext ctxt `thenTc_` kcHsType ty
 464     in
 465     tcHsTyVars tv_names kind_check      $ \ tyvars ->
 466     mapTc tc_pred ctxt                  `thenTc` \ theta ->
 467     tc_type ty                          `thenTc` \ tau ->
 468     returnTc (mkSigmaTy tyvars theta tau)
 469
 470 tc_types arg_tys = mapTc tc_type arg_tys
 471 \end{code}
 472
 473 Help functions for type applications
 474 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 475
 476 \begin{code}
 477 tc_app :: RenamedHsType -> [RenamedHsType] -> TcM Type
 478 tc_app (HsAppTy ty1 ty2) tys
 479   = tc_app ty1 (ty2:tys)
 480
 481 tc_app ty tys
 482   = tcAddErrCtxt (appKindCtxt pp_app)   $
 483     tc_types tys                        `thenTc` \ arg_tys ->
 484     case ty of
 485         HsTyVar fun -> tc_fun_type fun arg_tys
 486         other       -> tc_type ty               `thenTc` \ fun_ty ->
 487                        returnNF_Tc (mkAppTys fun_ty arg_tys)
 488   where
 489     pp_app = ppr ty <+> sep (map pprParendHsType tys)
 490
 491 -- (tc_fun_type ty arg_tys) returns (mkAppTys ty arg_tys)
 492 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
 493 --      hence the rather strange functionality.
 494
 495 tc_fun_type name arg_tys
 496   = tcLookup name                       `thenTc` \ thing ->
 497     case thing of
 498         ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)
 499
 500         AGlobal (ATyCon tc) -> returnTc (mkGenTyConApp tc arg_tys)
 501
 502         other -> failWithTc (wrongThingErr "type constructor" thing name)
 503 \end{code}
 504
 505
 506 Contexts
 507 ~~~~~~~~
 508 \begin{code}
 509 tcHsPred pred = kc_pred pred `thenTc_`  tc_pred pred
 510         -- Is happy with a partial application, e.g. (ST s)
 511         -- Used from TcDeriv
 512
 513 tc_pred assn@(HsClassP class_name tys)
 514   = tcAddErrCtxt (appKindCtxt (ppr assn))       $
 515     tc_types tys                        `thenTc` \ arg_tys ->
 516     tcLookupGlobal class_name                   `thenTc` \ thing ->
 517     case thing of
 518         AClass clas -> returnTc (ClassP clas arg_tys)
 519         other       -> failWithTc (wrongThingErr "class" (AGlobal thing) class_name)
 520
 521 tc_pred assn@(HsIParam name ty)
 522   = tcAddErrCtxt (appKindCtxt (ppr assn))       $
 523     tc_type ty                                  `thenTc` \ arg_ty ->
 524     returnTc (IParam name arg_ty)
 525 \end{code}
 526
 527
 528
 529 %************************************************************************
 530 %*                                                                      *
 531 \subsection{Type variables, with knot tying!}
 532 %*                                                                      *
 533 %************************************************************************
 534
 535 \begin{code}
 536 mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
 537 mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
 538
 539 mkTyClTyVars :: Kind                    -- Kind of the tycon or class
 540              -> [HsTyVarBndr Name]
 541              -> [TyVar]
 542 mkTyClTyVars kind tyvar_names
 543   = mkImmutTyVars tyvars_w_kinds
 544   where
 545     (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
 546 \end{code}
 547
 548
 549 %************************************************************************
 550 %*                                                                      *
 551 \subsection{Signatures}
 552 %*                                                                      *
 553 %************************************************************************
 554
 555 @tcSigs@ checks the signatures for validity, and returns a list of
 556 {\em freshly-instantiated} signatures.  That is, the types are already
 557 split up, and have fresh type variables installed.  All non-type-signature
 558 "RenamedSigs" are ignored.
 559
 560 The @TcSigInfo@ contains @TcTypes@ because they are unified with
 561 the variable's type, and after that checked to see whether they've
 562 been instantiated.
 563
 564 \begin{code}
 565 data TcSigInfo
 566   = TySigInfo
 567         TcId                    -- *Polymorphic* binder for this value...
 568                                 -- Has name = N
 569
 570         [TcTyVar]               -- tyvars
 571         TcThetaType             -- theta
 572         TcTauType               -- tau
 573
 574         TcId                    -- *Monomorphic* binder for this value
 575                                 -- Does *not* have name = N
 576                                 -- Has type tau
 577
 578         [Inst]                  -- Empty if theta is null, or
 579                                 -- (method mono_id) otherwise
 580
 581         SrcLoc                  -- Of the signature
 582
 583 instance Outputable TcSigInfo where
 584     ppr (TySigInfo id tyvars theta tau _ inst loc) =
 585         ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
 586
 587 tcSigPolyId :: TcSigInfo -> TcId
 588 tcSigPolyId (TySigInfo id _ _ _ _ _ _) = id
 589
 590 tcSigMonoId :: TcSigInfo -> TcId
 591 tcSigMonoId (TySigInfo _ _ _ _ id _ _) = id
 592
 593 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
 594         -- Search for a particular signature
 595 maybeSig [] name = Nothing
 596 maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name
 597   | name == idName sig_id = Just sig
 598   | otherwise             = maybeSig sigs name
 599 \end{code}
 600
 601
 602 \begin{code}
 603 tcTySig :: RenamedSig -> TcM TcSigInfo
 604
 605 tcTySig (Sig v ty src_loc)
 606  = tcAddSrcLoc src_loc                          $
 607    tcHsSigType (FunSigCtxt v) ty                `thenTc` \ sigma_tc_ty ->
 608    mkTcSig (mkLocalId v sigma_tc_ty) src_loc    `thenNF_Tc` \ sig ->
 609    returnTc sig
 610
 611 mkTcSig :: TcId -> SrcLoc -> NF_TcM TcSigInfo
 612 mkTcSig poly_id src_loc
 613   =     -- Instantiate this type
 614         -- It's important to do this even though in the error-free case
 615         -- we could just split the sigma_tc_ty (since the tyvars don't
 616         -- unified with anything).  But in the case of an error, when
 617         -- the tyvars *do* get unified with something, we want to carry on
 618         -- typechecking the rest of the program with the function bound
 619         -- to a pristine type, namely sigma_tc_ty
 620    tcInstType SigTv (idType poly_id)            `thenNF_Tc` \ (tyvars', theta', tau') ->
 621
 622    newMethodWithGivenTy SignatureOrigin
 623                         poly_id
 624                         (mkTyVarTys tyvars')
 625                         theta' tau'             `thenNF_Tc` \ inst ->
 626         -- We make a Method even if it's not overloaded; no harm
 627
 628    returnNF_Tc (TySigInfo poly_id tyvars' theta' tau'
 629                           (instToId inst) [inst] src_loc)
 630 \end{code}
 631
 632
 633 %************************************************************************
 634 %*                                                                      *
 635 \subsection{Errors and contexts}
 636 %*                                                                      *
 637 %************************************************************************
 638
 639
 640 \begin{code}
 641 hoistForAllTys :: Type -> Type
 642 -- Used for user-written type signatures only
 643 -- Move all the foralls and constraints to the top
 644 -- e.g.  T -> forall a. a        ==>   forall a. T -> a
 645 --       T -> (?x::Int) -> Int   ==>   (?x::Int) -> T -> Int
 646 --
 647 -- We want to 'look through' type synonyms when doing this
 648 -- so it's better done on the Type than the HsType
 649
 650 hoistForAllTys ty
 651   = let
 652         no_shadow_ty = deShadowTy ty
 653         -- Running over ty with an empty substitution gives it the
 654         -- no-shadowing property.  This is important.  For example:
 655         --      type Foo r = forall a. a -> r
 656         --      foo :: Foo (Foo ())
 657         -- Here the hoisting should give
 658         --      foo :: forall a a1. a -> a1 -> ()
 659         --
 660         -- What about type vars that are lexically in scope in the envt?
 661         -- We simply rely on them having a different unique to any
 662         -- binder in 'ty'.  Otherwise we'd have to slurp the in-scope-tyvars
 663         -- out of the envt, which is boring and (I think) not necessary.
 664     in
 665     case hoist no_shadow_ty of
 666         (tvs, theta, body) -> mkForAllTys tvs (mkFunTys (nubBy tcEqType theta) body)
 667                 -- The 'nubBy' eliminates duplicate constraints
 668   where
 669     hoist ty
 670         | (tvs1, body_ty) <- tcSplitForAllTys ty,
 671           not (null tvs1)
 672         = case hoist body_ty of
 673                 (tvs2,theta,tau) -> (tvs1 ++ tvs2, theta, tau)
 674
 675         | Just (arg, res) <- tcSplitFunTy_maybe ty
 676         = let
 677               arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively
 678           in                            -- to the argument type
 679           if (isPredTy arg') then
 680             case hoist res of
 681                 (tvs,theta,tau) -> (tvs, arg':theta, tau)
 682           else
 683              case hoist res of
 684                 (tvs,theta,tau) -> (tvs, theta, mkFunTy arg' tau)
 685
 686         | otherwise = ([], [], ty)
 687 \end{code}
 688
 689
 690 %************************************************************************
 691 %*                                                                      *
 692 \subsection{Errors and contexts}
 693 %*                                                                      *
 694 %************************************************************************
 695
 696 \begin{code}
 697 typeKindCtxt :: RenamedHsType -> Message
 698 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
 699                        nest 2 (quotes (ppr ty)),
 700                        ptext SLIT("is a type")]
 701
 702 appKindCtxt :: SDoc -> Message
 703 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
 704
 705 wrongThingErr expected thing name
 706   = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
 707   where
 708     pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
 709     pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
 710     pp_thing (AGlobal (AnId   _)) = ptext SLIT("Identifier")
 711     pp_thing (ATyVar _)           = ptext SLIT("Type variable")
 712     pp_thing (ATcId _)            = ptext SLIT("Local identifier")
 713     pp_thing (AThing _)           = ptext SLIT("Utterly bogus")
 714 \end{code}