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
  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 kc_hs_type (HsTyVar name)
 252   = kcTyVar name        `thenM` \ kind ->
 253     returnM (HsTyVar name, kind)
 254
 255 kc_hs_type (HsListTy ty)
 256   = kcLiftedType ty                     `thenM` \ ty' ->
 257     returnM (HsListTy ty', liftedTypeKind)
 258
 259 kc_hs_type (HsPArrTy ty)
 260   = kcLiftedType ty                     `thenM` \ ty' ->
 261     returnM (HsPArrTy ty', liftedTypeKind)
 262
 263 kc_hs_type (HsNumTy n)
 264    = returnM (HsNumTy n, liftedTypeKind)
 265
 266 kc_hs_type (HsKindSig ty k)
 267   = kcCheckHsType ty k  `thenM` \ ty' ->
 268     returnM (HsKindSig ty' k, k)
 269
 270 kc_hs_type (HsTupleTy Boxed tys)
 271   = mappM kcLiftedType tys      `thenM` \ tys' ->
 272     returnM (HsTupleTy Boxed tys', liftedTypeKind)
 273
 274 kc_hs_type (HsTupleTy Unboxed tys)
 275   = mappM kcTypeType tys        `thenM` \ tys' ->
 276     returnM (HsTupleTy Unboxed tys', unliftedTypeKind)
 277
 278 kc_hs_type (HsFunTy ty1 ty2)
 279   = kcTypeType ty1      `thenM` \ ty1' ->
 280     kcTypeType ty2      `thenM` \ ty2' ->
 281     returnM (HsFunTy ty1' ty2', liftedTypeKind)
 282
 283 kc_hs_type ty@(HsOpTy ty1 op ty2)
 284   = addLocM 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 kc_hs_type ty@(HsAppTy ty1 ty2)
 289   = kcHsType fun_ty                       `thenM` \ (fun_ty', fun_kind) ->
 290     kcApps fun_kind (ppr fun_ty) arg_tys  `thenM` \ ((arg_ty':arg_tys'), res_kind) ->
 291     returnM (foldl mk_app (HsAppTy fun_ty' arg_ty') arg_tys', res_kind)
 292   where
 293     (fun_ty, arg_tys) = split ty1 [ty2]
 294     split (L _ (HsAppTy f a)) as = split f (a:as)
 295     split f                   as = (f,as)
 296     mk_app fun arg = HsAppTy (noLoc fun) arg    -- Add noLocs for inner nodes of
 297                                                 -- the application; they are never used
 298
 299 kc_hs_type (HsPredTy pred)
 300   = kcHsPred pred               `thenM` \ pred' ->
 301     returnM (HsPredTy pred', liftedTypeKind)
 302
 303 kc_hs_type (HsForAllTy exp tv_names context ty)
 304   = kcHsTyVars tv_names         $ \ tv_names' ->
 305     kcHsContext context         `thenM` \ ctxt' ->
 306     kcLiftedType ty             `thenM` \ ty' ->
 307         -- The body of a forall must be a type, but in principle
 308         -- there's no reason to prohibit *unlifted* types.
 309         -- In fact, GHC can itself construct a function with an
 310         -- unboxed tuple inside a for-all (via CPR analyis; see
 311         -- typecheck/should_compile/tc170)
 312         --
 313         -- Still, that's only for internal interfaces, which aren't
 314         -- kind-checked, and it's a bit inconvenient to use kcTypeType
 315         -- here (because it doesn't return the result kind), so I'm
 316         -- leaving it as lifted types for now.
 317     returnM (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind)
 318
 319 ---------------------------
 320 kcApps :: TcKind                        -- Function kind
 321        -> SDoc                          -- Function
 322        -> [LHsType Name]                -- Arg types
 323        -> TcM ([LHsType Name], TcKind)  -- Kind-checked args
 324 kcApps fun_kind ppr_fun args
 325   = split_fk fun_kind (length args)     `thenM` \ (arg_kinds, res_kind) ->
 326     mappM kc_arg (args `zip` arg_kinds) `thenM` \ args' ->
 327     returnM (args', res_kind)
 328   where
 329     split_fk fk 0 = returnM ([], fk)
 330     split_fk fk n = unifyFunKind fk     `thenM` \ mb_fk ->
 331                     case mb_fk of
 332                         Nothing       -> failWithTc too_many_args
 333                         Just (ak,fk') -> split_fk fk' (n-1)     `thenM` \ (aks, rk) ->
 334                                          returnM (ak:aks, rk)
 335
 336     kc_arg (arg, arg_kind) = kcCheckHsType arg arg_kind
 337
 338     too_many_args = ptext SLIT("Kind error:") <+> quotes ppr_fun <+>
 339                     ptext SLIT("is applied to too many type arguments")
 340
 341 ---------------------------
 342 kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
 343 kcHsContext ctxt = wrapLocM (mappM kcHsPred) ctxt
 344
 345 kcHsPred pred           -- Checks that the result is of kind liftedType
 346   = wrapLocFstM kc_pred pred                    `thenM` \ (pred', kind) ->
 347     checkExpectedKind pred kind liftedTypeKind  `thenM_`
 348     returnM pred'
 349
 350 ---------------------------
 351 kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)
 352         -- Does *not* check for a saturated
 353         -- application (reason: used from TcDeriv)
 354 kc_pred pred@(HsIParam name ty)
 355   = kcHsType ty         `thenM` \ (ty', kind) ->
 356     returnM (HsIParam name ty', kind)
 357
 358 kc_pred pred@(HsClassP cls tys)
 359   = kcClass cls                 `thenM` \ kind ->
 360     kcApps kind (ppr cls) tys   `thenM` \ (tys', res_kind) ->
 361     returnM (HsClassP cls tys', res_kind)
 362
 363 ---------------------------
 364 kcTyVar :: Name -> TcM TcKind
 365 kcTyVar name    -- Could be a tyvar or a tycon
 366   = tcLookup name       `thenM` \ thing ->
 367     case thing of
 368         ATyVar tv               -> returnM (tyVarKind tv)
 369         ARecTyCon kind          -> returnM kind
 370         AGlobal (ATyCon tc)     -> returnM (tyConKind tc)
 371         other                   -> failWithTc (wrongThingErr "type" thing name)
 372
 373 kcClass :: Name -> TcM TcKind
 374 kcClass cls     -- Must be a class
 375   = tcLookup cls                                `thenM` \ thing ->
 376     case thing of
 377         ARecClass kind          -> returnM kind
 378         AGlobal (AClass cls)    -> returnM (tyConKind (classTyCon cls))
 379         other                   -> failWithTc (wrongThingErr "class" thing cls)
 380 \end{code}
 381
 382         Helper functions
 383
 384
 385 \begin{code}
 386 ---------------------------
 387 -- We would like to get a decent error message from
 388 --   (a) Under-applied type constructors
 389 --              f :: (Maybe, Maybe)
 390 --   (b) Over-applied type constructors
 391 --              f :: Int x -> Int x
 392 --
 393
 394
 395 checkExpectedKind :: Outputable a => Located a -> TcKind -> TcKind -> TcM TcKind
 396 -- A fancy wrapper for 'unifyKind', which tries to give
 397 -- decent error messages.
 398 -- Returns the same kind that it is passed, exp_kind
 399 checkExpectedKind (L span ty) act_kind exp_kind
 400   | act_kind `eqKind` exp_kind -- Short cut for a very common case
 401   = returnM exp_kind
 402   | otherwise
 403   = tryTc (unifyKind exp_kind act_kind) `thenM` \ (errs, mb_r) ->
 404     case mb_r of {
 405         Just _  -> returnM exp_kind ;   -- Unification succeeded
 406         Nothing ->
 407
 408         -- So there's definitely an error
 409         -- Now to find out what sort
 410     addSrcSpan span             $
 411     zonkTcType exp_kind         `thenM` \ exp_kind ->
 412     zonkTcType act_kind         `thenM` \ act_kind ->
 413
 414     let (exp_as, _) = Type.splitFunTys exp_kind
 415         (act_as, _) = Type.splitFunTys act_kind
 416                 -- Use the Type versions for kinds
 417         n_exp_as = length exp_as
 418         n_act_as = length act_as
 419
 420         err | n_exp_as < n_act_as       -- E.g. [Maybe]
 421             = quotes (ppr ty) <+> ptext SLIT("is not applied to enough type arguments")
 422
 423                 -- Now n_exp_as >= n_act_as. In the next two cases,
 424                 -- n_exp_as == 0, and hence so is n_act_as
 425             | exp_kind `eqKind` liftedTypeKind && act_kind `eqKind` unliftedTypeKind
 426             = ptext SLIT("Expecting a lifted type, but") <+> quotes (ppr ty)
 427                 <+> ptext SLIT("is unlifted")
 428
 429             | exp_kind `eqKind` unliftedTypeKind && act_kind `eqKind` liftedTypeKind
 430             = ptext SLIT("Expecting an unlifted type, but") <+> quotes (ppr ty)
 431                 <+> ptext SLIT("is lifted")
 432
 433             | otherwise                 -- E.g. Monad [Int]
 434             = sep [ ptext SLIT("Expecting kind") <+> quotes (pprKind exp_kind) <> comma,
 435                     ptext SLIT("but") <+> quotes (ppr ty) <+>
 436                         ptext SLIT("has kind") <+> quotes (pprKind act_kind)]
 437    in
 438    failWithTc (ptext SLIT("Kind error:") <+> err)
 439    }
 440 \end{code}
 441
 442 %************************************************************************
 443 %*                                                                      *
 444                 Desugaring
 445 %*                                                                      *
 446 %************************************************************************
 447
 448 The type desugarer
 449
 450         * Transforms from HsType to Type
 451         * Zonks any kinds
 452
 453 It cannot fail, and does no validity checking
 454
 455 \begin{code}
 456 dsHsType :: LHsType Name -> TcM Type
 457 -- All HsTyVarBndrs in the intput type are kind-annotated
 458 dsHsType ty = ds_type (unLoc ty)
 459
 460 ds_type ty@(HsTyVar name)
 461   = ds_app ty []
 462
 463 ds_type (HsParTy ty)            -- Remove the parentheses markers
 464   = dsHsType ty
 465
 466 ds_type (HsKindSig ty k)
 467   = dsHsType ty -- Kind checking done already
 468
 469 ds_type (HsListTy ty)
 470   = dsHsType ty                         `thenM` \ tau_ty ->
 471     returnM (mkListTy tau_ty)
 472
 473 ds_type (HsPArrTy ty)
 474   = dsHsType ty                         `thenM` \ tau_ty ->
 475     returnM (mkPArrTy tau_ty)
 476
 477 ds_type (HsTupleTy boxity tys)
 478   = dsHsTypes tys                       `thenM` \ tau_tys ->
 479     returnM (mkTupleTy boxity (length tys) tau_tys)
 480
 481 ds_type (HsFunTy ty1 ty2)
 482   = dsHsType ty1                        `thenM` \ tau_ty1 ->
 483     dsHsType ty2                        `thenM` \ tau_ty2 ->
 484     returnM (mkFunTy tau_ty1 tau_ty2)
 485
 486 ds_type (HsOpTy ty1 (L span op) ty2)
 487   = dsHsType ty1                `thenM` \ tau_ty1 ->
 488     dsHsType ty2                `thenM` \ tau_ty2 ->
 489     addSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
 490
 491 ds_type (HsNumTy n)
 492   = ASSERT(n==1)
 493     tcLookupTyCon genUnitTyConName      `thenM` \ tc ->
 494     returnM (mkTyConApp tc [])
 495
 496 ds_type ty@(HsAppTy _ _)
 497   = ds_app ty []
 498
 499 ds_type (HsPredTy pred)
 500   = dsHsPred pred       `thenM` \ pred' ->
 501     returnM (mkPredTy pred')
 502
 503 ds_type full_ty@(HsForAllTy exp tv_names ctxt ty)
 504   = tcTyVarBndrs tv_names               $ \ tyvars ->
 505     mappM dsHsPred (unLoc ctxt)         `thenM` \ theta ->
 506     dsHsType ty                         `thenM` \ tau ->
 507     returnM (mkSigmaTy tyvars theta tau)
 508
 509 dsHsTypes arg_tys = mappM dsHsType arg_tys
 510 \end{code}
 511
 512 Help functions for type applications
 513 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 514
 515 \begin{code}
 516 ds_app :: HsType Name -> [LHsType Name] -> TcM Type
 517 ds_app (HsAppTy ty1 ty2) tys
 518   = ds_app (unLoc ty1) (ty2:tys)
 519
 520 ds_app ty tys
 521   = dsHsTypes tys                       `thenM` \ arg_tys ->
 522     case ty of
 523         HsTyVar fun -> ds_var_app fun arg_tys
 524         other       -> ds_type ty               `thenM` \ fun_ty ->
 525                        returnM (mkAppTys fun_ty arg_tys)
 526
 527 ds_var_app :: Name -> [Type] -> TcM Type
 528 ds_var_app name arg_tys
 529  = tcLookup name                        `thenM` \ thing ->
 530     case thing of
 531         ATyVar tv            -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
 532         AGlobal (ATyCon tc)  -> returnM (mkGenTyConApp tc arg_tys)
 533         ARecTyCon _          -> tcLookupTyCon name      `thenM` \ tc ->
 534                                 returnM (mkGenTyConApp tc arg_tys)
 535         other -> pprPanic "ds_app_type" (ppr name <+> ppr arg_tys)
 536 \end{code}
 537
 538
 539 Contexts
 540 ~~~~~~~~
 541 \begin{code}
 542 dsHsPred :: LHsPred Name -> TcM PredType
 543 dsHsPred pred = ds_pred (unLoc pred)
 544
 545 ds_pred pred@(HsClassP class_name tys)
 546   = dsHsTypes tys                       `thenM` \ arg_tys ->
 547     tcLookupClass class_name            `thenM` \ clas ->
 548     returnM (ClassP clas arg_tys)
 549
 550 ds_pred (HsIParam name ty)
 551   = dsHsType ty                                 `thenM` \ arg_ty ->
 552     returnM (IParam name arg_ty)
 553 \end{code}
 554
 555
 556 %************************************************************************
 557 %*                                                                      *
 558                 Type-variable binders
 559 %*                                                                      *
 560 %************************************************************************
 561
 562
 563 \begin{code}
 564 kcHsTyVars :: [LHsTyVarBndr Name]
 565            -> ([LHsTyVarBndr Name] -> TcM r)    -- These binders are kind-annotated
 566                                                 -- They scope over the thing inside
 567            -> TcM r
 568 kcHsTyVars tvs thing_inside
 569   = mappM (wrapLocM kcHsTyVar) tvs      `thenM` \ bndrs ->
 570     tcExtendTyVarKindEnv bndrs          $
 571     thing_inside bndrs
 572
 573 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
 574         -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it
 575 kcHsTyVar (UserTyVar name)        = newKindVar  `thenM` \ kind ->
 576                                     returnM (KindedTyVar name kind)
 577 kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind)
 578
 579 ------------------
 580 tcTyVarBndrs :: [LHsTyVarBndr Name]     -- Kind-annotated binders, which need kind-zonking
 581              -> ([TyVar] -> TcM r)
 582              -> TcM r
 583 -- Used when type-checking types/classes/type-decls
 584 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
 585 tcTyVarBndrs bndrs thing_inside
 586   = mapM (zonk . unLoc) bndrs   `thenM` \ tyvars ->
 587     tcExtendTyVarEnv tyvars (thing_inside tyvars)
 588   where
 589     zonk (KindedTyVar name kind) = zonkTcKindToKind kind        `thenM` \ kind' ->
 590                                    returnM (mkTyVar name kind')
 591     zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
 592                             returnM (mkTyVar name liftedTypeKind)
 593 \end{code}
 594
 595
 596 %************************************************************************
 597 %*                                                                      *
 598                 Scoped type variables
 599 %*                                                                      *
 600 %************************************************************************
 601
 602
 603 tcAddScopedTyVars is used for scoped type variables added by pattern
 604 type signatures
 605         e.g.  \ ((x::a), (y::a)) -> x+y
 606 They never have explicit kinds (because this is source-code only)
 607 They are mutable (because they can get bound to a more specific type).
 608
 609 Usually we kind-infer and expand type splices, and then
 610 tupecheck/desugar the type.  That doesn't work well for scoped type
 611 variables, because they scope left-right in patterns.  (e.g. in the
 612 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
 613
 614 The current not-very-good plan is to
 615   * find all the types in the patterns
 616   * find their free tyvars
 617   * do kind inference
 618   * bring the kinded type vars into scope
 619   * BUT throw away the kind-checked type
 620         (we'll kind-check it again when we type-check the pattern)
 621
 622 This is bad because throwing away the kind checked type throws away
 623 its splices.  But too bad for now.  [July 03]
 624
 625 Historical note:
 626     We no longer specify that these type variables must be univerally
 627     quantified (lots of email on the subject).  If you want to put that
 628     back in, you need to
 629         a) Do a checkSigTyVars after thing_inside
 630         b) More insidiously, don't pass in expected_ty, else
 631            we unify with it too early and checkSigTyVars barfs
 632            Instead you have to pass in a fresh ty var, and unify
 633            it with expected_ty afterwards
 634
 635 \begin{code}
 636 tcAddScopedTyVars :: [LHsType Name] -> TcM a -> TcM a
 637 tcAddScopedTyVars [] thing_inside
 638   = thing_inside        -- Quick get-out for the empty case
 639
 640 tcAddScopedTyVars sig_tys thing_inside
 641   = getInLocalScope                     `thenM` \ in_scope ->
 642     getSrcSpanM                         `thenM` \ span ->
 643     let
 644         sig_tvs = [ L span (UserTyVar n)
 645                   | ty <- sig_tys,
 646                     n <- nameSetToList (extractHsTyVars ty),
 647                     not (in_scope n) ]
 648         -- The tyvars we want are the free type variables of
 649         -- the type that are not already in scope
 650     in
 651         -- Behave like kcHsType on a ForAll type
 652         -- i.e. make kinded tyvars with mutable kinds,
 653         --      and kind-check the enclosed types
 654     kcHsTyVars sig_tvs (\ kinded_tvs -> do
 655                             { mappM kcTypeType sig_tys
 656                             ; return kinded_tvs })      `thenM` \ kinded_tvs ->
 657
 658         -- Zonk the mutable kinds and bring the tyvars into scope
 659         -- Rather like tcTyVarBndrs, except that it brings *mutable*
 660         -- tyvars into scope, not immutable ones
 661         --
 662         -- Furthermore, the tyvars are PatSigTvs, which means that we get better
 663         -- error messages when type variables escape:
 664         --      Inferred type is less polymorphic than expected
 665         --      Quantified type variable `t' escapes
 666         --      It is mentioned in the environment:
 667         --      t is bound by the pattern type signature at tcfail103.hs:6
 668     mapM (zonk . unLoc) kinded_tvs      `thenM` \ tyvars ->
 669     tcExtendTyVarEnv tyvars thing_inside
 670
 671   where
 672     zonk (KindedTyVar name kind) = zonkTcKindToKind kind        `thenM` \ kind' ->
 673                                    newMutTyVar name kind' PatSigTv
 674     zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
 675                             returnM (mkTyVar name liftedTypeKind)
 676 \end{code}
 677
 678
 679 %************************************************************************
 680 %*                                                                      *
 681 \subsection{Signatures}
 682 %*                                                                      *
 683 %************************************************************************
 684
 685 @tcSigs@ checks the signatures for validity, and returns a list of
 686 {\em freshly-instantiated} signatures.  That is, the types are already
 687 split up, and have fresh type variables installed.  All non-type-signature
 688 "RenamedSigs" are ignored.
 689
 690 The @TcSigInfo@ contains @TcTypes@ because they are unified with
 691 the variable's type, and after that checked to see whether they've
 692 been instantiated.
 693
 694 \begin{code}
 695 data TcSigInfo
 696   = TySigInfo {
 697         sig_poly_id :: TcId,    -- *Polymorphic* binder for this value...
 698                                 -- Has name = N
 699
 700         sig_tvs   :: [TcTyVar],         -- tyvars
 701         sig_theta :: TcThetaType,       -- theta
 702         sig_tau   :: TcTauType,         -- tau
 703
 704         sig_mono_id :: TcId,    -- *Monomorphic* binder for this value
 705                                 -- Does *not* have name = N
 706                                 -- Has type tau
 707
 708         sig_insts :: [Inst],    -- Empty if theta is null, or
 709                                 -- (method mono_id) otherwise
 710
 711         sig_loc :: SrcSpan      -- The location of the signature
 712     }
 713
 714
 715 instance Outputable TcSigInfo where
 716     ppr (TySigInfo id tyvars theta tau _ inst _) =
 717         ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
 718
 719 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
 720         -- Search for a particular signature
 721 maybeSig [] name = Nothing
 722 maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name
 723   | name == idName sig_id = Just sig
 724   | otherwise             = maybeSig sigs name
 725 \end{code}
 726
 727
 728 \begin{code}
 729 tcTySig :: LSig Name -> TcM TcSigInfo
 730
 731 tcTySig (L span (Sig (L _ v) ty))
 732  = addSrcSpan span                      $
 733    tcHsSigType (FunSigCtxt v) ty        `thenM` \ sigma_tc_ty ->
 734    mkTcSig (mkLocalId v sigma_tc_ty)    `thenM` \ sig ->
 735    returnM sig
 736
 737 mkTcSig :: TcId -> TcM TcSigInfo
 738 mkTcSig poly_id
 739   =     -- Instantiate this type
 740         -- It's important to do this even though in the error-free case
 741         -- we could just split the sigma_tc_ty (since the tyvars don't
 742         -- unified with anything).  But in the case of an error, when
 743         -- the tyvars *do* get unified with something, we want to carry on
 744         -- typechecking the rest of the program with the function bound
 745         -- to a pristine type, namely sigma_tc_ty
 746    tcInstType SigTv (idType poly_id)            `thenM` \ (tyvars', theta', tau') ->
 747
 748    getInstLoc SignatureOrigin                   `thenM` \ inst_loc ->
 749    newMethod inst_loc poly_id
 750              (mkTyVarTys tyvars')
 751              theta' tau'                        `thenM` \ inst ->
 752         -- We make a Method even if it's not overloaded; no harm
 753         -- But do not extend the LIE!  We're just making an Id.
 754
 755    getSrcSpanM                                  `thenM` \ src_loc ->
 756    returnM (TySigInfo { sig_poly_id = poly_id, sig_tvs = tyvars',
 757                         sig_theta = theta', sig_tau = tau',
 758                         sig_mono_id = instToId inst,
 759                         sig_insts = [inst], sig_loc = src_loc })
 760 \end{code}
 761
 762
 763 %************************************************************************
 764 %*                                                                      *
 765 \subsection{Errors and contexts}
 766 %*                                                                      *
 767 %************************************************************************
 768
 769
 770 \begin{code}
 771 hoistForAllTys :: Type -> Type
 772 -- Used for user-written type signatures only
 773 -- Move all the foralls and constraints to the top
 774 -- e.g.  T -> forall a. a        ==>   forall a. T -> a
 775 --       T -> (?x::Int) -> Int   ==>   (?x::Int) -> T -> Int
 776 --
 777 -- Also: eliminate duplicate constraints.  These can show up
 778 -- when hoisting constraints, notably implicit parameters.
 779 --
 780 -- We want to 'look through' type synonyms when doing this
 781 -- so it's better done on the Type than the HsType
 782
 783 hoistForAllTys ty
 784   = let
 785         no_shadow_ty = deShadowTy ty
 786         -- Running over ty with an empty substitution gives it the
 787         -- no-shadowing property.  This is important.  For example:
 788         --      type Foo r = forall a. a -> r
 789         --      foo :: Foo (Foo ())
 790         -- Here the hoisting should give
 791         --      foo :: forall a a1. a -> a1 -> ()
 792         --
 793         -- What about type vars that are lexically in scope in the envt?
 794         -- We simply rely on them having a different unique to any
 795         -- binder in 'ty'.  Otherwise we'd have to slurp the in-scope-tyvars
 796         -- out of the envt, which is boring and (I think) not necessary.
 797     in
 798     case hoist no_shadow_ty of
 799         (tvs, theta, body) -> mkForAllTys tvs (mkFunTys (nubBy tcEqType theta) body)
 800                 -- The 'nubBy' eliminates duplicate constraints,
 801                 -- notably implicit parameters
 802   where
 803     hoist ty
 804         | (tvs1, body_ty) <- tcSplitForAllTys ty,
 805           not (null tvs1)
 806         = case hoist body_ty of
 807                 (tvs2,theta,tau) -> (tvs1 ++ tvs2, theta, tau)
 808
 809         | Just (arg, res) <- tcSplitFunTy_maybe ty
 810         = let
 811               arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively
 812           in                            -- to the argument type
 813           if (isPredTy arg') then
 814             case hoist res of
 815                 (tvs,theta,tau) -> (tvs, arg':theta, tau)
 816           else
 817              case hoist res of
 818                 (tvs,theta,tau) -> (tvs, theta, mkFunTy arg' tau)
 819
 820         | otherwise = ([], [], ty)
 821 \end{code}
 822
 823
 824 %************************************************************************
 825 %*                                                                      *
 826 \subsection{Errors and contexts}
 827 %*                                                                      *
 828 %************************************************************************
 829
 830 \begin{code}
 831 wrongThingErr expected thing name
 832   = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
 833   where
 834     pp_thing (AGlobal (ATyCon _))   = ptext SLIT("Type constructor")
 835     pp_thing (AGlobal (AClass _))   = ptext SLIT("Class")
 836     pp_thing (AGlobal (AnId   _))   = ptext SLIT("Identifier")
 837     pp_thing (AGlobal (ADataCon _)) = ptext SLIT("Data constructor")
 838     pp_thing (ATyVar _)             = ptext SLIT("Type variable")
 839     pp_thing (ATcId _ _ _)          = ptext SLIT("Local identifier")
 840     pp_thing (ARecTyCon _)          = ptext SLIT("Rec tycon")
 841     pp_thing (ARecClass _)          = ptext SLIT("Rec class")
 842 \end{code}