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