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, tcHsPred,
   9         UserTypeCtxt(..),
  10
  11                 -- Kind checking
  12         kcHsTyVars, kcHsSigType, kcHsLiftedSigType,
  13         kcCheckHsType, kcHsContext,
  14
  15                 -- Typechecking kinded types
  16         tcHsKindedContext, tcHsKindedType, tcTyVarBndrs, dsHsType,
  17
  18         tcAddScopedTyVars,
  19
  20         TcSigInfo(..), tcTySig, mkTcSig, maybeSig, tcSigPolyId, tcSigMonoId
  21    ) where
  22
  23 #include "HsVersions.h"
  24
  25 import HsSyn            ( HsType(..), HsTyVarBndr(..), HsContext, Sig(..), HsPred(..) )
  26 import RnHsSyn          ( RenamedHsType, RenamedContext, RenamedSig, extractHsTyVars )
  27 import TcHsSyn          ( TcId )
  28
  29 import TcRnMonad
  30 import TcEnv            ( tcExtendTyVarEnv, tcExtendTyVarKindEnv,
  31                           tcLookup, tcLookupClass, tcLookupTyCon,
  32                           TyThing(..), TcTyThing(..),
  33                           getInLocalScope
  34                         )
  35 import TcMType          ( newKindVar, newOpenTypeKind, tcInstType, newMutTyVar,
  36                           zonkTcType, zonkTcKindToKind,
  37                           checkValidType, UserTypeCtxt(..), pprHsSigCtxt
  38                         )
  39 import TcUnify          ( unifyKind, unifyFunKind )
  40 import TcType           ( Type, PredType(..), ThetaType, TyVarDetails(..),
  41                           TcTyVar, TcKind, TcThetaType, TcTauType,
  42                           mkTyVarTy, mkTyVarTys, mkFunTy, isTypeKind,
  43                           mkForAllTys, mkFunTys, tcEqType, isPredTy,
  44                           mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys,
  45                           liftedTypeKind, unliftedTypeKind, eqKind,
  46                           tcSplitFunTy_maybe, tcSplitForAllTys, pprKind )
  47 import qualified Type   ( splitFunTys )
  48 import Inst             ( Inst, InstOrigin(..), newMethod, instToId )
  49
  50 import Id               ( mkLocalId, idName, idType )
  51 import Var              ( TyVar, mkTyVar, tyVarKind )
  52 import TyCon            ( TyCon, tyConKind )
  53 import Class            ( classTyCon )
  54 import Name             ( Name )
  55 import NameSet
  56 import PrelNames        ( genUnitTyConName )
  57 import Subst            ( deShadowTy )
  58 import TysWiredIn       ( mkListTy, mkPArrTy, mkTupleTy )
  59 import BasicTypes       ( Boxity(..) )
  60 import SrcLoc           ( SrcLoc )
  61 import Outputable
  62 import List             ( nubBy )
  63 \end{code}
  64
  65
  66         ----------------------------
  67                 General notes
  68         ----------------------------
  69
  70 Generally speaking we now type-check types in three phases
  71
  72   1.  kcHsType: kind check the HsType
  73         *includes* performing any TH type splices;
  74         so it returns a translated, and kind-annotated, type
  75
  76   2.  dsHsType: convert from HsType to Type:
  77         perform zonking
  78         expand type synonyms [mkGenTyApps]
  79         hoist the foralls [tcHsType]
  80
  81   3.  checkValidType: check the validity of the resulting type
  82
  83 Often these steps are done one after the other (tcHsSigType).
  84 But in mutually recursive groups of type and class decls we do
  85         1 kind-check the whole group
  86         2 build TyCons/Classes in a knot-tied way
  87         3 check the validity of types in the now-unknotted TyCons/Classes
  88
  89 For example, when we find
  90         (forall a m. m a -> m a)
  91 we bind a,m to kind varibles and kind-check (m a -> m a).  This makes
  92 a get kind *, and m get kind *->*.  Now we typecheck (m a -> m a) in
  93 an environment that binds a and m suitably.
  94
  95 The kind checker passed to tcHsTyVars needs to look at enough to
  96 establish the kind of the tyvar:
  97   * For a group of type and class decls, it's just the group, not
  98         the rest of the program
  99   * For a tyvar bound in a pattern type signature, its the types
 100         mentioned in the other type signatures in that bunch of patterns
 101   * For a tyvar bound in a RULE, it's the type signatures on other
 102         universally quantified variables in the rule
 103
 104 Note that this may occasionally give surprising results.  For example:
 105
 106         data T a b = MkT (a b)
 107
 108 Here we deduce                  a::*->*,       b::*
 109 But equally valid would be      a::(*->*)-> *, b::*->*
 110
 111
 112 Validity checking
 113 ~~~~~~~~~~~~~~~~~
 114 Some of the validity check could in principle be done by the kind checker,
 115 but not all:
 116
 117 - During desugaring, we normalise by expanding type synonyms.  Only
 118   after this step can we check things like type-synonym saturation
 119   e.g.  type T k = k Int
 120         type S a = a
 121   Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
 122   and then S is saturated.  This is a GHC extension.
 123
 124 - Similarly, also a GHC extension, we look through synonyms before complaining
 125   about the form of a class or instance declaration
 126
 127 - Ambiguity checks involve functional dependencies, and it's easier to wait
 128   until knots have been resolved before poking into them
 129
 130 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
 131 finished building the loop.  So to keep things simple, we postpone most validity
 132 checking until step (3).
 133
 134 Knot tying
 135 ~~~~~~~~~~
 136 During step (1) we might fault in a TyCon defined in another module, and it might
 137 (via a loop) refer back to a TyCon defined in this module. So when we tie a big
 138 knot around type declarations with ARecThing, so that the fault-in code can get
 139 the TyCon being defined.
 140
 141
 142 %************************************************************************
 143 %*                                                                      *
 144 \subsection{Checking types}
 145 %*                                                                      *
 146 %************************************************************************
 147
 148 \begin{code}
 149 tcHsSigType :: UserTypeCtxt -> RenamedHsType -> TcM Type
 150   -- Do kind checking, and hoist for-alls to the top
 151 tcHsSigType ctxt hs_ty
 152   = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
 153     do  { kinded_ty <- kcTypeType hs_ty
 154         ; ty <- tcHsKindedType kinded_ty
 155         ; checkValidType ctxt ty
 156         ; returnM ty }
 157
 158 -- tcHsPred is happy with a partial application, e.g. (ST s)
 159 -- Used from TcDeriv
 160 tcHsPred pred
 161   = do { (kinded_pred,_) <- kc_pred pred        -- kc_pred rather than kcHsPred
 162                                                 -- to avoid the partial application check
 163        ; dsHsPred kinded_pred }
 164 \end{code}
 165
 166         These functions are used during knot-tying in
 167         type and class declarations, when we have to
 168         separate kind-checking, desugaring, and validity checking
 169
 170 \begin{code}
 171 kcHsSigType, kcHsLiftedSigType :: HsType Name -> TcM (HsType Name)
 172         -- Used for type signatures
 173 kcHsSigType ty       = kcTypeType ty
 174 kcHsLiftedSigType ty = kcLiftedType ty
 175
 176 tcHsKindedType :: RenamedHsType -> TcM Type
 177   -- Don't do kind checking, nor validity checking,
 178   --    but do hoist for-alls to the top
 179   -- This is used in type and class decls, where kinding is
 180   -- done in advance, and validity checking is done later
 181   -- [Validity checking done later because of knot-tying issues.]
 182 tcHsKindedType hs_ty
 183   = do  { ty <- dsHsType hs_ty
 184         ; return (hoistForAllTys ty) }
 185
 186 tcHsKindedContext :: RenamedContext -> TcM ThetaType
 187 -- Used when we are expecting a ClassContext (i.e. no implicit params)
 188 -- Does not do validity checking, like tcHsKindedType
 189 tcHsKindedContext hs_theta = mappM dsHsPred hs_theta
 190 \end{code}
 191
 192
 193 %************************************************************************
 194 %*                                                                      *
 195                 The main kind checker: kcHsType
 196 %*                                                                      *
 197 %************************************************************************
 198
 199         First a couple of simple wrappers for kcHsType
 200
 201 \begin{code}
 202 ---------------------------
 203 kcLiftedType :: HsType Name -> TcM (HsType Name)
 204 -- The type ty must be a *lifted* *type*
 205 kcLiftedType ty = kcCheckHsType ty liftedTypeKind
 206
 207 ---------------------------
 208 kcTypeType :: HsType Name -> TcM (HsType Name)
 209 -- The type ty must be a *type*, but it can be lifted or unlifted
 210 -- Be sure to use checkExpectedKind, rather than simply unifying
 211 -- with (Type bx), because it gives better error messages
 212 kcTypeType ty
 213   = kcHsType ty                 `thenM` \ (ty', kind) ->
 214     if isTypeKind kind then
 215         return ty'
 216     else
 217     newOpenTypeKind                             `thenM` \ type_kind ->
 218     traceTc (text "kcTypeType" $$ nest 2 (ppr ty $$ ppr ty' $$ ppr kind $$ ppr type_kind)) `thenM_`
 219     checkExpectedKind (ppr ty) kind type_kind   `thenM_`
 220     returnM ty'
 221
 222 ---------------------------
 223 kcCheckHsType :: HsType Name -> TcKind -> TcM (HsType Name)
 224 -- Check that the type has the specified kind
 225 kcCheckHsType ty exp_kind
 226   = kcHsType ty                                         `thenM` \ (ty', act_kind) ->
 227     checkExpectedKind (ppr ty) act_kind exp_kind        `thenM_`
 228     returnM ty'
 229 \end{code}
 230
 231         Here comes the main function
 232
 233 \begin{code}
 234 kcHsType :: HsType Name -> TcM (HsType Name, TcKind)
 235 -- kcHsType *returns* the kind of the type, rather than taking an expected
 236 -- kind as argument as tcExpr does.
 237 -- Reasons:
 238 --      (a) the kind of (->) is
 239 --              forall bx1 bx2. Type bx1 -> Type bx2 -> Type Boxed
 240 --          so we'd need to generate huge numbers of bx variables.
 241 --      (b) kinds are so simple that the error messages are fine
 242 --
 243 -- The translated type has explicitly-kinded type-variable binders
 244
 245 kcHsType (HsParTy ty)
 246  = kcHsType ty          `thenM` \ (ty', kind) ->
 247    returnM (HsParTy ty', kind)
 248
 249 kcHsType (HsTyVar name)
 250   = kcTyVar name        `thenM` \ kind ->
 251     returnM (HsTyVar name, kind)
 252
 253 kcHsType (HsListTy ty)
 254   = kcLiftedType ty                     `thenM` \ ty' ->
 255     returnM (HsListTy ty', liftedTypeKind)
 256
 257 kcHsType (HsPArrTy ty)
 258   = kcLiftedType ty                     `thenM` \ ty' ->
 259     returnM (HsPArrTy ty', liftedTypeKind)
 260
 261 kcHsType (HsNumTy n)
 262    = returnM (HsNumTy n, liftedTypeKind)
 263
 264 kcHsType (HsKindSig ty k)
 265   = kcCheckHsType ty k  `thenM` \ ty' ->
 266     returnM (HsKindSig ty' k, k)
 267
 268 kcHsType (HsTupleTy Boxed tys)
 269   = mappM kcLiftedType tys      `thenM` \ tys' ->
 270     returnM (HsTupleTy Boxed tys', liftedTypeKind)
 271
 272 kcHsType (HsTupleTy Unboxed tys)
 273   = mappM kcTypeType tys        `thenM` \ tys' ->
 274     returnM (HsTupleTy Unboxed tys', unliftedTypeKind)
 275
 276 kcHsType (HsFunTy ty1 ty2)
 277   = kcTypeType ty1      `thenM` \ ty1' ->
 278     kcTypeType ty2      `thenM` \ ty2' ->
 279     returnM (HsFunTy ty1' ty2', liftedTypeKind)
 280
 281 kcHsType ty@(HsOpTy ty1 op ty2)
 282   = kcTyVar op                          `thenM` \ op_kind ->
 283     kcApps op_kind (ppr op) [ty1,ty2]   `thenM` \ ([ty1',ty2'], res_kind) ->
 284     returnM (HsOpTy ty1' op ty2', res_kind)
 285
 286 kcHsType ty@(HsAppTy ty1 ty2)
 287   = kcHsType fun_ty                       `thenM` \ (fun_ty', fun_kind) ->
 288     kcApps fun_kind (ppr fun_ty) arg_tys  `thenM` \ (arg_tys', res_kind) ->
 289     returnM (foldl HsAppTy fun_ty' arg_tys', res_kind)
 290   where
 291     (fun_ty, arg_tys) = split ty1 [ty2]
 292     split (HsAppTy f a) as = split f (a:as)
 293     split f             as = (f,as)
 294
 295 kcHsType (HsPredTy pred)
 296   = kcHsPred pred               `thenM` \ pred' ->
 297     returnM (HsPredTy pred', liftedTypeKind)
 298
 299 kcHsType (HsForAllTy exp tv_names context ty)
 300   = kcHsTyVars tv_names         $ \ tv_names' ->
 301     kcHsContext context         `thenM` \ ctxt' ->
 302     kcLiftedType ty             `thenM` \ ty' ->
 303         -- The body of a forall must be a type, but in principle
 304         -- there's no reason to prohibit *unlifted* types.
 305         -- In fact, GHC can itself construct a function with an
 306         -- unboxed tuple inside a for-all (via CPR analyis; see
 307         -- typecheck/should_compile/tc170)
 308         --
 309         -- Still, that's only for internal interfaces, which aren't
 310         -- kind-checked, and it's a bit inconvenient to use kcTypeType
 311         -- here (because it doesn't return the result kind), so I'm
 312         -- leaving it as lifted types for now.
 313     returnM (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind)
 314
 315 ---------------------------
 316 kcApps :: TcKind                -- Function kind
 317        -> SDoc                  -- Function
 318        -> [HsType Name]         -- Arg types
 319        -> TcM ([HsType Name], TcKind)   -- Kind-checked args
 320 kcApps fun_kind ppr_fun args
 321   = split_fk fun_kind (length args)     `thenM` \ (arg_kinds, res_kind) ->
 322     mappM kc_arg (args `zip` arg_kinds) `thenM` \ args' ->
 323     returnM (args', res_kind)
 324   where
 325     split_fk fk 0 = returnM ([], fk)
 326     split_fk fk n = unifyFunKind fk     `thenM` \ mb_fk ->
 327                     case mb_fk of
 328                         Nothing       -> failWithTc too_many_args
 329                         Just (ak,fk') -> split_fk fk' (n-1)     `thenM` \ (aks, rk) ->
 330                                          returnM (ak:aks, rk)
 331
 332     kc_arg (arg, arg_kind) = kcCheckHsType arg arg_kind
 333
 334     too_many_args = ptext SLIT("Kind error:") <+> quotes ppr_fun <+>
 335                     ptext SLIT("is applied to too many type arguments")
 336
 337 ---------------------------
 338 kcHsContext :: HsContext Name -> TcM (HsContext Name)
 339 kcHsContext ctxt = mappM kcHsPred ctxt
 340
 341 kcHsPred pred           -- Checks that the result is of kind liftedType
 342   = kc_pred pred                        `thenM` \ (pred', kind) ->
 343     checkExpectedKind (ppr pred) kind liftedTypeKind    `thenM_`
 344     returnM pred'
 345
 346 ---------------------------
 347 kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)
 348         -- Does *not* check for a saturated
 349         -- application (reason: used from TcDeriv)
 350 kc_pred pred@(HsIParam name ty)
 351   = kcHsType ty         `thenM` \ (ty', kind) ->
 352     returnM (HsIParam name ty', kind)
 353
 354 kc_pred pred@(HsClassP cls tys)
 355   = kcClass cls                 `thenM` \ kind ->
 356     kcApps kind (ppr cls) tys   `thenM` \ (tys', res_kind) ->
 357     returnM (HsClassP cls tys', res_kind)
 358
 359 ---------------------------
 360 kcTyVar :: Name -> TcM TcKind
 361 kcTyVar name    -- Could be a tyvar or a tycon
 362   = tcLookup name       `thenM` \ thing ->
 363     case thing of
 364         ATyVar tv               -> returnM (tyVarKind tv)
 365         ARecTyCon kind          -> returnM kind
 366         AGlobal (ATyCon tc)     -> returnM (tyConKind tc)
 367         other                   -> failWithTc (wrongThingErr "type" thing name)
 368
 369 kcClass :: Name -> TcM TcKind
 370 kcClass cls     -- Must be a class
 371   = tcLookup cls                                `thenM` \ thing ->
 372     case thing of
 373         ARecClass kind          -> returnM kind
 374         AGlobal (AClass cls)    -> returnM (tyConKind (classTyCon cls))
 375         other                   -> failWithTc (wrongThingErr "class" thing cls)
 376 \end{code}
 377
 378         Helper functions
 379
 380
 381 \begin{code}
 382 ---------------------------
 383 -- We would like to get a decent error message from
 384 --   (a) Under-applied type constructors
 385 --              f :: (Maybe, Maybe)
 386 --   (b) Over-applied type constructors
 387 --              f :: Int x -> Int x
 388 --
 389
 390
 391 checkExpectedKind :: SDoc -> TcKind -> TcKind -> TcM TcKind
 392 -- A fancy wrapper for 'unifyKind', which tries to give
 393 -- decent error messages.
 394 -- Returns the same kind that it is passed, exp_kind
 395 checkExpectedKind pp_ty act_kind exp_kind
 396   | act_kind `eqKind` exp_kind -- Short cut for a very common case
 397   = returnM exp_kind
 398   | otherwise
 399   = tryTc (unifyKind exp_kind act_kind) `thenM` \ (errs, mb_r) ->
 400     case mb_r of {
 401         Just _  -> returnM exp_kind ;   -- Unification succeeded
 402         Nothing ->
 403
 404         -- So there's definitely an error
 405         -- Now to find out what sort
 406     zonkTcType exp_kind         `thenM` \ exp_kind ->
 407     zonkTcType act_kind         `thenM` \ act_kind ->
 408
 409     let (exp_as, _) = Type.splitFunTys exp_kind
 410         (act_as, _) = Type.splitFunTys act_kind
 411                 -- Use the Type versions for kinds
 412         n_exp_as = length exp_as
 413         n_act_as = length act_as
 414
 415         err | n_exp_as < n_act_as       -- E.g. [Maybe]
 416             = quotes pp_ty <+> ptext SLIT("is not applied to enough type arguments")
 417
 418                 -- Now n_exp_as >= n_act_as. In the next two cases,
 419                 -- n_exp_as == 0, and hence so is n_act_as
 420             | exp_kind `eqKind` liftedTypeKind && act_kind `eqKind` unliftedTypeKind
 421             = ptext SLIT("Expecting a lifted type, but") <+> quotes pp_ty
 422                 <+> ptext SLIT("is unlifted")
 423
 424             | exp_kind `eqKind` unliftedTypeKind && act_kind `eqKind` liftedTypeKind
 425             = ptext SLIT("Expecting an unlifted type, but") <+> quotes pp_ty
 426                 <+> ptext SLIT("is lifted")
 427
 428             | otherwise                 -- E.g. Monad [Int]
 429             = sep [ ptext SLIT("Expecting kind") <+> quotes (pprKind exp_kind) <> comma,
 430                     ptext SLIT("but") <+> quotes pp_ty <+>
 431                         ptext SLIT("has kind") <+> quotes (pprKind act_kind)]
 432    in
 433    failWithTc (ptext SLIT("Kind error:") <+> err)
 434    }
 435 \end{code}
 436
 437 %************************************************************************
 438 %*                                                                      *
 439                 Desugaring
 440 %*                                                                      *
 441 %************************************************************************
 442
 443 The type desugarer
 444
 445         * Transforms from HsType to Type
 446         * Zonks any kinds
 447
 448 It cannot fail, and does no validity checking
 449
 450 \begin{code}
 451 dsHsType :: HsType Name         -- All HsTyVarBndrs are kind-annotated
 452          -> TcM Type
 453
 454 dsHsType ty@(HsTyVar name)
 455   = ds_app ty []
 456
 457 dsHsType (HsParTy ty)           -- Remove the parentheses markers
 458   = dsHsType ty
 459
 460 dsHsType (HsKindSig ty k)
 461   = dsHsType ty -- Kind checking done already
 462
 463 dsHsType (HsListTy ty)
 464   = dsHsType ty                         `thenM` \ tau_ty ->
 465     returnM (mkListTy tau_ty)
 466
 467 dsHsType (HsPArrTy ty)
 468   = dsHsType ty                         `thenM` \ tau_ty ->
 469     returnM (mkPArrTy tau_ty)
 470
 471 dsHsType (HsTupleTy boxity tys)
 472   = dsHsTypes tys                       `thenM` \ tau_tys ->
 473     returnM (mkTupleTy boxity (length tys) tau_tys)
 474
 475 dsHsType (HsFunTy ty1 ty2)
 476   = dsHsType ty1                        `thenM` \ tau_ty1 ->
 477     dsHsType ty2                        `thenM` \ tau_ty2 ->
 478     returnM (mkFunTy tau_ty1 tau_ty2)
 479
 480 dsHsType (HsOpTy ty1 op ty2)
 481   = dsHsType ty1 `thenM` \ tau_ty1 ->
 482     dsHsType ty2 `thenM` \ tau_ty2 ->
 483     ds_var_app op [tau_ty1,tau_ty2]
 484
 485 dsHsType (HsNumTy n)
 486   = ASSERT(n==1)
 487     tcLookupTyCon genUnitTyConName      `thenM` \ tc ->
 488     returnM (mkTyConApp tc [])
 489
 490 dsHsType ty@(HsAppTy ty1 ty2)
 491   = ds_app ty1 [ty2]
 492
 493 dsHsType (HsPredTy pred)
 494   = dsHsPred pred       `thenM` \ pred' ->
 495     returnM (mkPredTy pred')
 496
 497 dsHsType full_ty@(HsForAllTy exp tv_names ctxt ty)
 498   = tcTyVarBndrs tv_names               $ \ tyvars ->
 499     mappM dsHsPred ctxt                 `thenM` \ theta ->
 500     dsHsType ty                         `thenM` \ tau ->
 501     returnM (mkSigmaTy tyvars theta tau)
 502
 503 dsHsTypes arg_tys = mappM dsHsType arg_tys
 504 \end{code}
 505
 506 Help functions for type applications
 507 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 508
 509 \begin{code}
 510 ds_app :: HsType Name -> [HsType Name] -> TcM Type
 511 ds_app (HsAppTy ty1 ty2) tys
 512   = ds_app ty1 (ty2:tys)
 513
 514 ds_app ty tys
 515   = dsHsTypes tys                       `thenM` \ arg_tys ->
 516     case ty of
 517         HsTyVar fun -> ds_var_app fun arg_tys
 518         other       -> dsHsType ty              `thenM` \ fun_ty ->
 519                        returnM (mkAppTys fun_ty arg_tys)
 520
 521 ds_var_app :: Name -> [Type] -> TcM Type
 522 ds_var_app name arg_tys
 523  = tcLookup name                        `thenM` \ thing ->
 524     case thing of
 525         ATyVar tv            -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
 526         AGlobal (ATyCon tc)  -> returnM (mkGenTyConApp tc arg_tys)
 527         ARecTyCon _          -> tcLookupTyCon name      `thenM` \ tc ->
 528                                 returnM (mkGenTyConApp tc arg_tys)
 529         other -> pprPanic "ds_app_type" (ppr name <+> ppr arg_tys)
 530 \end{code}
 531
 532
 533 Contexts
 534 ~~~~~~~~
 535 \begin{code}
 536 dsHsPred :: HsPred Name -> TcM PredType
 537 dsHsPred pred@(HsClassP class_name tys)
 538   = dsHsTypes tys                       `thenM` \ arg_tys ->
 539     tcLookupClass class_name            `thenM` \ clas ->
 540     returnM (ClassP clas arg_tys)
 541
 542 dsHsPred (HsIParam name ty)
 543   = dsHsType ty                                 `thenM` \ arg_ty ->
 544     returnM (IParam name arg_ty)
 545 \end{code}
 546
 547
 548 %************************************************************************
 549 %*                                                                      *
 550                 Type-variable binders
 551 %*                                                                      *
 552 %************************************************************************
 553
 554
 555 \begin{code}
 556 kcHsTyVars :: [HsTyVarBndr Name]
 557            -> ([HsTyVarBndr Name] -> TcM r)     -- These binders are kind-annotated
 558                                                 -- They scope over the thing inside
 559            -> TcM r
 560 kcHsTyVars tvs thing_inside
 561   = mappM kcHsTyVar tvs         `thenM` \ bndrs ->
 562     tcExtendTyVarKindEnv bndrs  $
 563     thing_inside bndrs
 564
 565 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
 566         -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it
 567 kcHsTyVar (UserTyVar name)        = newKindVar  `thenM` \ kind ->
 568                                     returnM (KindedTyVar name kind)
 569 kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind)
 570
 571 ------------------
 572 tcTyVarBndrs :: [HsTyVarBndr Name]      -- Kind-annotated binders, which need kind-zonking
 573              -> ([TyVar] -> TcM r)
 574              -> TcM r
 575 -- Used when type-checking types/classes/type-decls
 576 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
 577 tcTyVarBndrs bndrs thing_inside
 578   = mapM zonk bndrs     `thenM` \ tyvars ->
 579     tcExtendTyVarEnv tyvars (thing_inside tyvars)
 580   where
 581     zonk (KindedTyVar name kind) = zonkTcKindToKind kind        `thenM` \ kind' ->
 582                                    returnM (mkTyVar name kind')
 583     zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
 584                             returnM (mkTyVar name liftedTypeKind)
 585 \end{code}
 586
 587
 588 %************************************************************************
 589 %*                                                                      *
 590                 Scoped type variables
 591 %*                                                                      *
 592 %************************************************************************
 593
 594
 595 tcAddScopedTyVars is used for scoped type variables added by pattern
 596 type signatures
 597         e.g.  \ ((x::a), (y::a)) -> x+y
 598 They never have explicit kinds (because this is source-code only)
 599 They are mutable (because they can get bound to a more specific type).
 600
 601 Usually we kind-infer and expand type splices, and then
 602 tupecheck/desugar the type.  That doesn't work well for scoped type
 603 variables, because they scope left-right in patterns.  (e.g. in the
 604 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
 605
 606 The current not-very-good plan is to
 607   * find all the types in the patterns
 608   * find their free tyvars
 609   * do kind inference
 610   * bring the kinded type vars into scope
 611   * BUT throw away the kind-checked type
 612         (we'll kind-check it again when we type-check the pattern)
 613
 614 This is bad because throwing away the kind checked type throws away
 615 its splices.  But too bad for now.  [July 03]
 616
 617 Historical note:
 618     We no longer specify that these type variables must be univerally
 619     quantified (lots of email on the subject).  If you want to put that
 620     back in, you need to
 621         a) Do a checkSigTyVars after thing_inside
 622         b) More insidiously, don't pass in expected_ty, else
 623            we unify with it too early and checkSigTyVars barfs
 624            Instead you have to pass in a fresh ty var, and unify
 625            it with expected_ty afterwards
 626
 627 \begin{code}
 628 tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
 629 tcAddScopedTyVars [] thing_inside
 630   = thing_inside        -- Quick get-out for the empty case
 631
 632 tcAddScopedTyVars sig_tys thing_inside
 633   = getInLocalScope                     `thenM` \ in_scope ->
 634     let
 635         sig_tvs = [ UserTyVar n | ty <- sig_tys,
 636                                   n <- nameSetToList (extractHsTyVars ty),
 637                                   not (in_scope n) ]
 638         -- The tyvars we want are the free type variables of
 639         -- the type that are not already in scope
 640     in
 641         -- Behave like kcHsType on a ForAll type
 642         -- i.e. make kinded tyvars with mutable kinds,
 643         --      and kind-check the enclosed types
 644     kcHsTyVars sig_tvs (\ kinded_tvs -> do
 645                             { mappM kcTypeType sig_tys
 646                             ; return kinded_tvs })      `thenM` \ kinded_tvs ->
 647
 648         -- Zonk the mutable kinds and bring the tyvars into scope
 649         -- Rather like tcTyVarBndrs, except that it brings *mutable*
 650         -- tyvars into scope, not immutable ones
 651         --
 652         -- Furthermore, the tyvars are PatSigTvs, which means that we get better
 653         -- error messages when type variables escape:
 654         --      Inferred type is less polymorphic than expected
 655         --      Quantified type variable `t' escapes
 656         --      It is mentioned in the environment:
 657         --      t is bound by the pattern type signature at tcfail103.hs:6
 658     mapM zonk kinded_tvs        `thenM` \ tyvars ->
 659     tcExtendTyVarEnv tyvars thing_inside
 660
 661   where
 662     zonk (KindedTyVar name kind) = zonkTcKindToKind kind        `thenM` \ kind' ->
 663                                    newMutTyVar name kind' PatSigTv
 664     zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
 665                             returnM (mkTyVar name liftedTypeKind)
 666 \end{code}
 667
 668
 669 %************************************************************************
 670 %*                                                                      *
 671 \subsection{Signatures}
 672 %*                                                                      *
 673 %************************************************************************
 674
 675 @tcSigs@ checks the signatures for validity, and returns a list of
 676 {\em freshly-instantiated} signatures.  That is, the types are already
 677 split up, and have fresh type variables installed.  All non-type-signature
 678 "RenamedSigs" are ignored.
 679
 680 The @TcSigInfo@ contains @TcTypes@ because they are unified with
 681 the variable's type, and after that checked to see whether they've
 682 been instantiated.
 683
 684 \begin{code}
 685 data TcSigInfo
 686   = TySigInfo
 687         TcId                    -- *Polymorphic* binder for this value...
 688                                 -- Has name = N
 689
 690         [TcTyVar]               -- tyvars
 691         TcThetaType             -- theta
 692         TcTauType               -- tau
 693
 694         TcId                    -- *Monomorphic* binder for this value
 695                                 -- Does *not* have name = N
 696                                 -- Has type tau
 697
 698         [Inst]                  -- Empty if theta is null, or
 699                                 -- (method mono_id) otherwise
 700
 701         SrcLoc                  -- Of the signature
 702
 703 instance Outputable TcSigInfo where
 704     ppr (TySigInfo id tyvars theta tau _ inst loc) =
 705         ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
 706
 707 tcSigPolyId :: TcSigInfo -> TcId
 708 tcSigPolyId (TySigInfo id _ _ _ _ _ _) = id
 709
 710 tcSigMonoId :: TcSigInfo -> TcId
 711 tcSigMonoId (TySigInfo _ _ _ _ id _ _) = id
 712
 713 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
 714         -- Search for a particular signature
 715 maybeSig [] name = Nothing
 716 maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name
 717   | name == idName sig_id = Just sig
 718   | otherwise             = maybeSig sigs name
 719 \end{code}
 720
 721
 722 \begin{code}
 723 tcTySig :: RenamedSig -> TcM TcSigInfo
 724
 725 tcTySig (Sig v ty src_loc)
 726  = addSrcLoc src_loc                    $
 727    tcHsSigType (FunSigCtxt v) ty        `thenM` \ sigma_tc_ty ->
 728    mkTcSig (mkLocalId v sigma_tc_ty)    `thenM` \ sig ->
 729    returnM sig
 730
 731 mkTcSig :: TcId -> TcM TcSigInfo
 732 mkTcSig poly_id
 733   =     -- Instantiate this type
 734         -- It's important to do this even though in the error-free case
 735         -- we could just split the sigma_tc_ty (since the tyvars don't
 736         -- unified with anything).  But in the case of an error, when
 737         -- the tyvars *do* get unified with something, we want to carry on
 738         -- typechecking the rest of the program with the function bound
 739         -- to a pristine type, namely sigma_tc_ty
 740    tcInstType SigTv (idType poly_id)            `thenM` \ (tyvars', theta', tau') ->
 741
 742    getInstLoc SignatureOrigin                   `thenM` \ inst_loc ->
 743    newMethod inst_loc poly_id
 744              (mkTyVarTys tyvars')
 745              theta' tau'                        `thenM` \ inst ->
 746         -- We make a Method even if it's not overloaded; no harm
 747         -- But do not extend the LIE!  We're just making an Id.
 748
 749    getSrcLocM                                   `thenM` \ src_loc ->
 750    returnM (TySigInfo poly_id tyvars' theta' tau'
 751                           (instToId inst) [inst] src_loc)
 752 \end{code}
 753
 754
 755 %************************************************************************
 756 %*                                                                      *
 757 \subsection{Errors and contexts}
 758 %*                                                                      *
 759 %************************************************************************
 760
 761
 762 \begin{code}
 763 hoistForAllTys :: Type -> Type
 764 -- Used for user-written type signatures only
 765 -- Move all the foralls and constraints to the top
 766 -- e.g.  T -> forall a. a        ==>   forall a. T -> a
 767 --       T -> (?x::Int) -> Int   ==>   (?x::Int) -> T -> Int
 768 --
 769 -- Also: eliminate duplicate constraints.  These can show up
 770 -- when hoisting constraints, notably implicit parameters.
 771 --
 772 -- We want to 'look through' type synonyms when doing this
 773 -- so it's better done on the Type than the HsType
 774
 775 hoistForAllTys ty
 776   = let
 777         no_shadow_ty = deShadowTy ty
 778         -- Running over ty with an empty substitution gives it the
 779         -- no-shadowing property.  This is important.  For example:
 780         --      type Foo r = forall a. a -> r
 781         --      foo :: Foo (Foo ())
 782         -- Here the hoisting should give
 783         --      foo :: forall a a1. a -> a1 -> ()
 784         --
 785         -- What about type vars that are lexically in scope in the envt?
 786         -- We simply rely on them having a different unique to any
 787         -- binder in 'ty'.  Otherwise we'd have to slurp the in-scope-tyvars
 788         -- out of the envt, which is boring and (I think) not necessary.
 789     in
 790     case hoist no_shadow_ty of
 791         (tvs, theta, body) -> mkForAllTys tvs (mkFunTys (nubBy tcEqType theta) body)
 792                 -- The 'nubBy' eliminates duplicate constraints,
 793                 -- notably implicit parameters
 794   where
 795     hoist ty
 796         | (tvs1, body_ty) <- tcSplitForAllTys ty,
 797           not (null tvs1)
 798         = case hoist body_ty of
 799                 (tvs2,theta,tau) -> (tvs1 ++ tvs2, theta, tau)
 800
 801         | Just (arg, res) <- tcSplitFunTy_maybe ty
 802         = let
 803               arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively
 804           in                            -- to the argument type
 805           if (isPredTy arg') then
 806             case hoist res of
 807                 (tvs,theta,tau) -> (tvs, arg':theta, tau)
 808           else
 809              case hoist res of
 810                 (tvs,theta,tau) -> (tvs, theta, mkFunTy arg' tau)
 811
 812         | otherwise = ([], [], ty)
 813 \end{code}
 814
 815
 816 %************************************************************************
 817 %*                                                                      *
 818 \subsection{Errors and contexts}
 819 %*                                                                      *
 820 %************************************************************************
 821
 822 \begin{code}
 823 wrongThingErr expected thing name
 824   = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
 825   where
 826     pp_thing (AGlobal (ATyCon _))   = ptext SLIT("Type constructor")
 827     pp_thing (AGlobal (AClass _))   = ptext SLIT("Class")
 828     pp_thing (AGlobal (AnId   _))   = ptext SLIT("Identifier")
 829     pp_thing (AGlobal (ADataCon _)) = ptext SLIT("Data constructor")
 830     pp_thing (ATyVar _)             = ptext SLIT("Type variable")
 831     pp_thing (ATcId _ _ _)          = ptext SLIT("Local identifier")
 832     pp_thing (ARecTyCon _)          = ptext SLIT("Rec tycon")
 833     pp_thing (ARecClass _)          = ptext SLIT("Rec class")
 834 \end{code}