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