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