compiler/typecheck/TcHsType.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   4 %
   5 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
   6
   7 \begin{code}
   8 module TcHsType (
   9         tcHsSigType, tcHsDeriv,
  10         tcHsInstHead, tcHsQuantifiedType,
  11         UserTypeCtxt(..),
  12
  13                 -- Kind checking
  14         kcHsTyVars, kcHsSigType, kcHsLiftedSigType,
  15         kcLHsType, kcCheckLHsType, kcHsContext,
  16
  17                 -- Typechecking kinded types
  18         tcHsKindedContext, tcHsKindedType, tcHsBangType,
  19         tcTyVarBndrs, dsHsType, tcLHsConResTy,
  20         tcDataKindSig, ExpKind(..), EkCtxt(..),
  21
  22                 -- Pattern type signatures
  23         tcHsPatSigType, tcPatSig
  24    ) where
  25
  26 #include "HsVersions.h"
  27
  28 import HsSyn
  29 import RnHsSyn
  30 import TcRnMonad
  31 import TcEnv
  32 import TcMType
  33 import TcUnify
  34 import TcIface
  35 import TcType
  36 import {- Kind parts of -} Type
  37 import Var
  38 import Coercion
  39 import TyCon
  40 import Class
  41 import Name
  42 import OccName
  43 import NameSet
  44 import PrelNames
  45 import TysWiredIn
  46 import BasicTypes
  47 import SrcLoc
  48 import UniqSupply
  49 import Outputable
  50 import FastString
  51
  52 import Control.Monad
  53 \end{code}
  54
  55
  56         ----------------------------
  57                 General notes
  58         ----------------------------
  59
  60 Generally speaking we now type-check types in three phases
  61
  62   1.  kcHsType: kind check the HsType
  63         *includes* performing any TH type splices;
  64         so it returns a translated, and kind-annotated, type
  65
  66   2.  dsHsType: convert from HsType to Type:
  67         perform zonking
  68         expand type synonyms [mkGenTyApps]
  69         hoist the foralls [tcHsType]
  70
  71   3.  checkValidType: check the validity of the resulting type
  72
  73 Often these steps are done one after the other (tcHsSigType).
  74 But in mutually recursive groups of type and class decls we do
  75         1 kind-check the whole group
  76         2 build TyCons/Classes in a knot-tied way
  77         3 check the validity of types in the now-unknotted TyCons/Classes
  78
  79 For example, when we find
  80         (forall a m. m a -> m a)
  81 we bind a,m to kind varibles and kind-check (m a -> m a).  This makes
  82 a get kind *, and m get kind *->*.  Now we typecheck (m a -> m a) in
  83 an environment that binds a and m suitably.
  84
  85 The kind checker passed to tcHsTyVars needs to look at enough to
  86 establish the kind of the tyvar:
  87   * For a group of type and class decls, it's just the group, not
  88         the rest of the program
  89   * For a tyvar bound in a pattern type signature, its the types
  90         mentioned in the other type signatures in that bunch of patterns
  91   * For a tyvar bound in a RULE, it's the type signatures on other
  92         universally quantified variables in the rule
  93
  94 Note that this may occasionally give surprising results.  For example:
  95
  96         data T a b = MkT (a b)
  97
  98 Here we deduce                  a::*->*,       b::*
  99 But equally valid would be      a::(*->*)-> *, b::*->*
 100
 101
 102 Validity checking
 103 ~~~~~~~~~~~~~~~~~
 104 Some of the validity check could in principle be done by the kind checker,
 105 but not all:
 106
 107 - During desugaring, we normalise by expanding type synonyms.  Only
 108   after this step can we check things like type-synonym saturation
 109   e.g.  type T k = k Int
 110         type S a = a
 111   Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
 112   and then S is saturated.  This is a GHC extension.
 113
 114 - Similarly, also a GHC extension, we look through synonyms before complaining
 115   about the form of a class or instance declaration
 116
 117 - Ambiguity checks involve functional dependencies, and it's easier to wait
 118   until knots have been resolved before poking into them
 119
 120 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
 121 finished building the loop.  So to keep things simple, we postpone most validity
 122 checking until step (3).
 123
 124 Knot tying
 125 ~~~~~~~~~~
 126 During step (1) we might fault in a TyCon defined in another module, and it might
 127 (via a loop) refer back to a TyCon defined in this module. So when we tie a big
 128 knot around type declarations with ARecThing, so that the fault-in code can get
 129 the TyCon being defined.
 130
 131
 132 %************************************************************************
 133 %*                                                                      *
 134 \subsection{Checking types}
 135 %*                                                                      *
 136 %************************************************************************
 137
 138 \begin{code}
 139 tcHsSigType :: UserTypeCtxt -> LHsType Name -> TcM Type
 140   -- Do kind checking, and hoist for-alls to the top
 141   -- NB: it's important that the foralls that come from the top-level
 142   --     HsForAllTy in hs_ty occur *first* in the returned type.
 143   --     See Note [Scoped] with TcSigInfo
 144 tcHsSigType ctxt hs_ty
 145   = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
 146     do  { kinded_ty <- kcTypeType hs_ty
 147         ; ty <- tcHsKindedType kinded_ty
 148         ; checkValidType ctxt ty
 149         ; return ty }
 150
 151 tcHsInstHead :: LHsType Name -> TcM ([TyVar], ThetaType, Type)
 152 -- Typecheck an instance head.  We can't use
 153 -- tcHsSigType, because it's not a valid user type.
 154 tcHsInstHead hs_ty
 155   = do  { kinded_ty <- kcHsSigType hs_ty
 156         ; poly_ty   <- tcHsKindedType kinded_ty
 157         ; return (tcSplitSigmaTy poly_ty) }
 158
 159 tcHsQuantifiedType :: [LHsTyVarBndr Name] -> LHsType Name -> TcM ([TyVar], Type)
 160 -- Behave very like type-checking (HsForAllTy sig_tvs hs_ty),
 161 -- except that we want to keep the tvs separate
 162 tcHsQuantifiedType tv_names hs_ty
 163   = kcHsTyVars tv_names $ \ tv_names' ->
 164     do  { kc_ty <- kcHsSigType hs_ty
 165         ; tcTyVarBndrs tv_names' $ \ tvs ->
 166     do  { ty <- dsHsType kc_ty
 167         ; return (tvs, ty) } }
 168
 169 -- Used for the deriving(...) items
 170 tcHsDeriv :: HsType Name -> TcM ([TyVar], Class, [Type])
 171 tcHsDeriv = tc_hs_deriv []
 172
 173 tc_hs_deriv :: [LHsTyVarBndr Name] -> HsType Name
 174             -> TcM ([TyVar], Class, [Type])
 175 tc_hs_deriv tv_names (HsPredTy (HsClassP cls_name hs_tys))
 176   = kcHsTyVars tv_names                 $ \ tv_names' ->
 177     do  { cls_kind <- kcClass cls_name
 178         ; (tys, _res_kind) <- kcApps cls_name cls_kind hs_tys
 179         ; tcTyVarBndrs tv_names'        $ \ tyvars ->
 180     do  { arg_tys <- dsHsTypes tys
 181         ; cls <- tcLookupClass cls_name
 182         ; return (tyvars, cls, arg_tys) }}
 183
 184 tc_hs_deriv tv_names1 (HsForAllTy _ tv_names2 (L _ []) (L _ ty))
 185   =     -- Funny newtype deriving form
 186         --      forall a. C [a]
 187         -- where C has arity 2.  Hence can't use regular functions
 188     tc_hs_deriv (tv_names1 ++ tv_names2) ty
 189
 190 tc_hs_deriv _ other
 191   = failWithTc (ptext (sLit "Illegal deriving item") <+> ppr other)
 192 \end{code}
 193
 194         These functions are used during knot-tying in
 195         type and class declarations, when we have to
 196         separate kind-checking, desugaring, and validity checking
 197
 198 \begin{code}
 199 kcHsSigType, kcHsLiftedSigType :: LHsType Name -> TcM (LHsType Name)
 200         -- Used for type signatures
 201 kcHsSigType ty       = addKcTypeCtxt ty $ kcTypeType ty
 202 kcHsLiftedSigType ty = addKcTypeCtxt ty $ kcLiftedType ty
 203
 204 tcHsKindedType :: LHsType Name -> TcM Type
 205   -- Don't do kind checking, nor validity checking.
 206   -- This is used in type and class decls, where kinding is
 207   -- done in advance, and validity checking is done later
 208   -- [Validity checking done later because of knot-tying issues.]
 209 tcHsKindedType hs_ty = dsHsType hs_ty
 210
 211 tcHsBangType :: LHsType Name -> TcM Type
 212 -- Permit a bang, but discard it
 213 tcHsBangType (L _ (HsBangTy _ ty)) = tcHsKindedType ty
 214 tcHsBangType ty                    = tcHsKindedType ty
 215
 216 tcHsKindedContext :: LHsContext Name -> TcM ThetaType
 217 -- Used when we are expecting a ClassContext (i.e. no implicit params)
 218 -- Does not do validity checking, like tcHsKindedType
 219 tcHsKindedContext hs_theta = addLocM (mapM dsHsLPred) hs_theta
 220 \end{code}
 221
 222
 223 %************************************************************************
 224 %*                                                                      *
 225                 The main kind checker: kcHsType
 226 %*                                                                      *
 227 %************************************************************************
 228
 229         First a couple of simple wrappers for kcHsType
 230
 231 \begin{code}
 232 ---------------------------
 233 kcLiftedType :: LHsType Name -> TcM (LHsType Name)
 234 -- The type ty must be a *lifted* *type*
 235 kcLiftedType ty = kc_check_lhs_type ty ekLifted
 236
 237 ---------------------------
 238 kcTypeType :: LHsType Name -> TcM (LHsType Name)
 239 -- The type ty must be a *type*, but it can be lifted or
 240 -- unlifted or an unboxed tuple.
 241 kcTypeType ty = kc_check_lhs_type ty ekOpen
 242
 243 ---------------------------
 244 kcCheckLHsType :: LHsType Name -> ExpKind -> TcM (LHsType Name)
 245 kcCheckLHsType ty kind = addKcTypeCtxt ty $ kc_check_lhs_type ty kind
 246
 247
 248 kc_check_lhs_type :: LHsType Name -> ExpKind -> TcM (LHsType Name)
 249 -- Check that the type has the specified kind
 250 -- Be sure to use checkExpectedKind, rather than simply unifying
 251 -- with OpenTypeKind, because it gives better error messages
 252 kc_check_lhs_type (L span ty) exp_kind
 253   = setSrcSpan span $
 254     do { ty' <- kc_check_hs_type ty exp_kind
 255        ; return (L span ty') }
 256
 257 kc_check_lhs_types :: [(LHsType Name, ExpKind)] -> TcM [LHsType Name]
 258 kc_check_lhs_types tys_w_kinds
 259   = mapM kc_arg tys_w_kinds
 260   where
 261     kc_arg (arg, arg_kind) = kc_check_lhs_type arg arg_kind
 262
 263
 264 ---------------------------
 265 kc_check_hs_type :: HsType Name -> ExpKind -> TcM (HsType Name)
 266
 267 -- First some special cases for better error messages
 268 -- when we know the expected kind
 269 kc_check_hs_type (HsParTy ty) exp_kind
 270   = do { ty' <- kc_check_lhs_type ty exp_kind; return (HsParTy ty') }
 271
 272 kc_check_hs_type ty@(HsAppTy ty1 ty2) exp_kind
 273   = do { let (fun_ty, arg_tys) = splitHsAppTys ty1 ty2
 274        ; (fun_ty', fun_kind) <- kc_lhs_type fun_ty
 275        ; arg_tys' <- kcCheckApps fun_ty fun_kind arg_tys ty exp_kind
 276        ; return (mkHsAppTys fun_ty' arg_tys') }
 277
 278 kc_check_hs_type ty@(HsPredTy (HsClassP cls tys)) exp_kind
 279   = do { cls_kind <- kcClass cls
 280        ; tys' <- kcCheckApps cls cls_kind tys ty exp_kind
 281        ; return (HsPredTy (HsClassP cls tys')) }
 282
 283 -- This is the general case: infer the kind and compare
 284 kc_check_hs_type ty exp_kind
 285   = do  { (ty', act_kind) <- kc_hs_type ty
 286                 -- Add the context round the inner check only
 287                 -- because checkExpectedKind already mentions
 288                 -- 'ty' by name in any error message
 289
 290         ; checkExpectedKind (strip ty) act_kind exp_kind
 291         ; return ty' }
 292   where
 293         -- We infer the kind of the type, and then complain if it's
 294         -- not right.  But we don't want to complain about
 295         --      (ty) or !(ty) or forall a. ty
 296         -- when the real difficulty is with the 'ty' part.
 297     strip (HsParTy (L _ ty))          = strip ty
 298     strip (HsBangTy _ (L _ ty))       = strip ty
 299     strip (HsForAllTy _ _ _ (L _ ty)) = strip ty
 300     strip ty                          = ty
 301
 302 \end{code}
 303
 304         Here comes the main function
 305
 306 \begin{code}
 307 kcLHsType :: LHsType Name -> TcM (LHsType Name, TcKind)
 308 -- Called from outside: set the context
 309 kcLHsType ty = addKcTypeCtxt ty (kc_lhs_type ty)
 310
 311 kc_lhs_type :: LHsType Name -> TcM (LHsType Name, TcKind)
 312 kc_lhs_type (L span ty)
 313   = setSrcSpan span $
 314     do { (ty', kind) <- kc_hs_type ty
 315        ; return (L span ty', kind) }
 316
 317 -- kc_hs_type *returns* the kind of the type, rather than taking an expected
 318 -- kind as argument as tcExpr does.
 319 -- Reasons:
 320 --      (a) the kind of (->) is
 321 --              forall bx1 bx2. Type bx1 -> Type bx2 -> Type Boxed
 322 --          so we'd need to generate huge numbers of bx variables.
 323 --      (b) kinds are so simple that the error messages are fine
 324 --
 325 -- The translated type has explicitly-kinded type-variable binders
 326
 327 kc_hs_type :: HsType Name -> TcM (HsType Name, TcKind)
 328 kc_hs_type (HsParTy ty) = do
 329    (ty', kind) <- kc_lhs_type ty
 330    return (HsParTy ty', kind)
 331
 332 kc_hs_type (HsTyVar name) = do
 333     kind <- kcTyVar name
 334     return (HsTyVar name, kind)
 335
 336 kc_hs_type (HsListTy ty) = do
 337     ty' <- kcLiftedType ty
 338     return (HsListTy ty', liftedTypeKind)
 339
 340 kc_hs_type (HsPArrTy ty) = do
 341     ty' <- kcLiftedType ty
 342     return (HsPArrTy ty', liftedTypeKind)
 343
 344 kc_hs_type (HsNumTy n)
 345    = return (HsNumTy n, liftedTypeKind)
 346
 347 kc_hs_type (HsKindSig ty k) = do
 348     ty' <- kc_check_lhs_type ty (EK k EkKindSig)
 349     return (HsKindSig ty' k, k)
 350
 351 kc_hs_type (HsTupleTy Boxed tys) = do
 352     tys' <- mapM kcLiftedType tys
 353     return (HsTupleTy Boxed tys', liftedTypeKind)
 354
 355 kc_hs_type (HsTupleTy Unboxed tys) = do
 356     tys' <- mapM kcTypeType tys
 357     return (HsTupleTy Unboxed tys', ubxTupleKind)
 358
 359 kc_hs_type (HsFunTy ty1 ty2) = do
 360     ty1' <- kc_check_lhs_type ty1 (EK argTypeKind EkUnk)
 361     ty2' <- kcTypeType ty2
 362     return (HsFunTy ty1' ty2', liftedTypeKind)
 363
 364 kc_hs_type (HsOpTy ty1 op ty2) = do
 365     op_kind <- addLocM kcTyVar op
 366     ([ty1',ty2'], res_kind) <- kcApps op op_kind [ty1,ty2]
 367     return (HsOpTy ty1' op ty2', res_kind)
 368
 369 kc_hs_type (HsAppTy ty1 ty2) = do
 370     (fun_ty', fun_kind) <- kc_lhs_type fun_ty
 371     (arg_tys', res_kind) <- kcApps fun_ty fun_kind arg_tys
 372     return (mkHsAppTys fun_ty' arg_tys', res_kind)
 373   where
 374     (fun_ty, arg_tys) = splitHsAppTys ty1 ty2
 375
 376 kc_hs_type (HsPredTy (HsEqualP _ _))
 377   = wrongEqualityErr
 378
 379 kc_hs_type (HsPredTy pred) = do
 380     pred' <- kcHsPred pred
 381     return (HsPredTy pred', liftedTypeKind)
 382
 383 kc_hs_type (HsForAllTy exp tv_names context ty)
 384   = kcHsTyVars tv_names         $ \ tv_names' ->
 385     do  { ctxt' <- kcHsContext context
 386         ; ty'   <- kcLiftedType ty
 387              -- The body of a forall is usually a type, but in principle
 388              -- there's no reason to prohibit *unlifted* types.
 389              -- In fact, GHC can itself construct a function with an
 390              -- unboxed tuple inside a for-all (via CPR analyis; see
 391              -- typecheck/should_compile/tc170)
 392              --
 393              -- Still, that's only for internal interfaces, which aren't
 394              -- kind-checked, so we only allow liftedTypeKind here
 395
 396         ; return (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind) }
 397
 398 kc_hs_type (HsBangTy b ty) = do
 399     (ty', kind) <- kc_lhs_type ty
 400     return (HsBangTy b ty', kind)
 401
 402 kc_hs_type ty@(HsSpliceTy _)
 403   = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty)
 404
 405 -- remove the doc nodes here, no need to worry about the location since
 406 -- its the same for a doc node and it's child type node
 407 kc_hs_type (HsDocTy ty _)
 408   = kc_hs_type (unLoc ty)
 409
 410 ---------------------------
 411 kcApps :: Outputable a
 412        => a
 413        -> TcKind                        -- Function kind
 414        -> [LHsType Name]                -- Arg types
 415        -> TcM ([LHsType Name], TcKind)  -- Kind-checked args
 416 kcApps the_fun fun_kind args
 417   = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
 418        ; args' <- kc_check_lhs_types args_w_kinds
 419        ; return (args', res_kind) }
 420
 421 kcCheckApps :: Outputable a => a -> TcKind -> [LHsType Name]
 422             -> HsType Name     -- The type being checked (for err messages only)
 423             -> ExpKind         -- Expected kind
 424             -> TcM [LHsType Name]
 425 kcCheckApps the_fun fun_kind args ty exp_kind
 426   = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
 427        ; checkExpectedKind ty res_kind exp_kind
 428              -- Check the result kind *before* checking argument kinds
 429              -- This improves error message; Trac #2994
 430        ; kc_check_lhs_types args_w_kinds }
 431
 432 splitHsAppTys :: LHsType Name -> LHsType Name -> (LHsType Name, [LHsType Name])
 433 splitHsAppTys fun_ty arg_ty = split fun_ty [arg_ty]
 434   where
 435     split (L _ (HsAppTy f a)) as = split f (a:as)
 436     split f                   as = (f,as)
 437
 438 mkHsAppTys :: LHsType Name -> [LHsType Name] -> HsType Name
 439 mkHsAppTys fun_ty [] = pprPanic "mkHsAppTys" (ppr fun_ty)
 440 mkHsAppTys fun_ty (arg_ty:arg_tys)
 441   = foldl mk_app (HsAppTy fun_ty arg_ty) arg_tys
 442   where
 443     mk_app fun arg = HsAppTy (noLoc fun) arg    -- Add noLocs for inner nodes of
 444                                                 -- the application; they are
 445                                                 -- never used
 446
 447 ---------------------------
 448 splitFunKind :: SDoc -> Int -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind)
 449 splitFunKind _       _      fk [] = return ([], fk)
 450 splitFunKind the_fun arg_no fk (arg:args)
 451   = do { mb_fk <- unifyFunKind fk
 452        ; case mb_fk of
 453             Nothing       -> failWithTc too_many_args
 454             Just (ak,fk') -> do { (aks, rk) <- splitFunKind the_fun (arg_no+1) fk' args
 455                                 ; return ((arg, EK ak (EkArg the_fun arg_no)):aks, rk) } }
 456   where
 457     too_many_args = quotes the_fun <+>
 458                     ptext (sLit "is applied to too many type arguments")
 459
 460 ---------------------------
 461 kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
 462 kcHsContext ctxt = wrapLocM (mapM kcHsLPred) ctxt
 463
 464 kcHsLPred :: LHsPred Name -> TcM (LHsPred Name)
 465 kcHsLPred = wrapLocM kcHsPred
 466
 467 kcHsPred :: HsPred Name -> TcM (HsPred Name)
 468 kcHsPred pred = do      -- Checks that the result is of kind liftedType
 469     (pred', kind) <- kc_pred pred
 470     checkExpectedKind pred kind ekLifted
 471     return pred'
 472
 473 ---------------------------
 474 kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)
 475         -- Does *not* check for a saturated
 476         -- application (reason: used from TcDeriv)
 477 kc_pred (HsIParam name ty)
 478   = do { (ty', kind) <- kc_lhs_type ty
 479        ; return (HsIParam name ty', kind)
 480        }
 481 kc_pred (HsClassP cls tys)
 482   = do { kind <- kcClass cls
 483        ; (tys', res_kind) <- kcApps cls kind tys
 484        ; return (HsClassP cls tys', res_kind)
 485        }
 486 kc_pred (HsEqualP ty1 ty2)
 487   = do { (ty1', kind1) <- kc_lhs_type ty1
 488 --       ; checkExpectedKind ty1 kind1 liftedTypeKind
 489        ; (ty2', kind2) <- kc_lhs_type ty2
 490 --       ; checkExpectedKind ty2 kind2 liftedTypeKind
 491        ; checkExpectedKind ty2 kind2 (EK kind1 EkEqPred)
 492        ; return (HsEqualP ty1' ty2', liftedTypeKind)
 493        }
 494
 495 ---------------------------
 496 kcTyVar :: Name -> TcM TcKind
 497 kcTyVar name = do       -- Could be a tyvar or a tycon
 498     traceTc (text "lk1" <+> ppr name)
 499     thing <- tcLookup name
 500     traceTc (text "lk2" <+> ppr name <+> ppr thing)
 501     case thing of
 502         ATyVar _ ty             -> return (typeKind ty)
 503         AThing kind             -> return kind
 504         AGlobal (ATyCon tc)     -> return (tyConKind tc)
 505         _                       -> wrongThingErr "type" thing name
 506
 507 kcClass :: Name -> TcM TcKind
 508 kcClass cls = do        -- Must be a class
 509     thing <- tcLookup cls
 510     case thing of
 511         AThing kind             -> return kind
 512         AGlobal (AClass cls)    -> return (tyConKind (classTyCon cls))
 513         _                       -> wrongThingErr "class" thing cls
 514 \end{code}
 515
 516
 517 %************************************************************************
 518 %*                                                                      *
 519                 Desugaring
 520 %*                                                                      *
 521 %************************************************************************
 522
 523 The type desugarer
 524
 525         * Transforms from HsType to Type
 526         * Zonks any kinds
 527
 528 It cannot fail, and does no validity checking, except for
 529 structural matters, such as
 530         (a) spurious ! annotations.
 531         (b) a class used as a type
 532
 533 \begin{code}
 534 dsHsType :: LHsType Name -> TcM Type
 535 -- All HsTyVarBndrs in the intput type are kind-annotated
 536 dsHsType ty = ds_type (unLoc ty)
 537
 538 ds_type :: HsType Name -> TcM Type
 539 ds_type ty@(HsTyVar _)
 540   = ds_app ty []
 541
 542 ds_type (HsParTy ty)            -- Remove the parentheses markers
 543   = dsHsType ty
 544
 545 ds_type ty@(HsBangTy _ _)       -- No bangs should be here
 546   = failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty)
 547
 548 ds_type (HsKindSig ty _)
 549   = dsHsType ty -- Kind checking done already
 550
 551 ds_type (HsListTy ty) = do
 552     tau_ty <- dsHsType ty
 553     checkWiredInTyCon listTyCon
 554     return (mkListTy tau_ty)
 555
 556 ds_type (HsPArrTy ty) = do
 557     tau_ty <- dsHsType ty
 558     checkWiredInTyCon parrTyCon
 559     return (mkPArrTy tau_ty)
 560
 561 ds_type (HsTupleTy boxity tys) = do
 562     tau_tys <- dsHsTypes tys
 563     checkWiredInTyCon tycon
 564     return (mkTyConApp tycon tau_tys)
 565   where
 566     tycon = tupleTyCon boxity (length tys)
 567
 568 ds_type (HsFunTy ty1 ty2) = do
 569     tau_ty1 <- dsHsType ty1
 570     tau_ty2 <- dsHsType ty2
 571     return (mkFunTy tau_ty1 tau_ty2)
 572
 573 ds_type (HsOpTy ty1 (L span op) ty2) = do
 574     tau_ty1 <- dsHsType ty1
 575     tau_ty2 <- dsHsType ty2
 576     setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
 577
 578 ds_type (HsNumTy n)
 579   = ASSERT(n==1) do
 580     tc <- tcLookupTyCon genUnitTyConName
 581     return (mkTyConApp tc [])
 582
 583 ds_type ty@(HsAppTy _ _)
 584   = ds_app ty []
 585
 586 ds_type (HsPredTy pred) = do
 587     pred' <- dsHsPred pred
 588     return (mkPredTy pred')
 589
 590 ds_type (HsForAllTy _ tv_names ctxt ty)
 591   = tcTyVarBndrs tv_names               $ \ tyvars -> do
 592     theta <- mapM dsHsLPred (unLoc ctxt)
 593     tau <- dsHsType ty
 594     return (mkSigmaTy tyvars theta tau)
 595
 596 ds_type (HsSpliceTy {}) = panic "ds_type: HsSpliceTy"
 597
 598 ds_type (HsDocTy ty _)  -- Remove the doc comment
 599   = dsHsType ty
 600
 601 dsHsTypes :: [LHsType Name] -> TcM [Type]
 602 dsHsTypes arg_tys = mapM dsHsType arg_tys
 603 \end{code}
 604
 605 Help functions for type applications
 606 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 607
 608 \begin{code}
 609 ds_app :: HsType Name -> [LHsType Name] -> TcM Type
 610 ds_app (HsAppTy ty1 ty2) tys
 611   = ds_app (unLoc ty1) (ty2:tys)
 612
 613 ds_app ty tys = do
 614     arg_tys <- dsHsTypes tys
 615     case ty of
 616         HsTyVar fun -> ds_var_app fun arg_tys
 617         _           -> do fun_ty <- ds_type ty
 618                           return (mkAppTys fun_ty arg_tys)
 619
 620 ds_var_app :: Name -> [Type] -> TcM Type
 621 ds_var_app name arg_tys = do
 622     thing <- tcLookup name
 623     case thing of
 624         ATyVar _ ty         -> return (mkAppTys ty arg_tys)
 625         AGlobal (ATyCon tc) -> return (mkTyConApp tc arg_tys)
 626         _                   -> wrongThingErr "type" thing name
 627 \end{code}
 628
 629
 630 Contexts
 631 ~~~~~~~~
 632
 633 \begin{code}
 634 dsHsLPred :: LHsPred Name -> TcM PredType
 635 dsHsLPred pred = dsHsPred (unLoc pred)
 636
 637 dsHsPred :: HsPred Name -> TcM PredType
 638 dsHsPred (HsClassP class_name tys)
 639   = do { arg_tys <- dsHsTypes tys
 640        ; clas <- tcLookupClass class_name
 641        ; return (ClassP clas arg_tys)
 642        }
 643 dsHsPred (HsEqualP ty1 ty2)
 644   = do { arg_ty1 <- dsHsType ty1
 645        ; arg_ty2 <- dsHsType ty2
 646        ; return (EqPred arg_ty1 arg_ty2)
 647        }
 648 dsHsPred (HsIParam name ty)
 649   = do { arg_ty <- dsHsType ty
 650        ; return (IParam name arg_ty)
 651        }
 652 \end{code}
 653
 654 GADT constructor signatures
 655
 656 \begin{code}
 657 tcLHsConResTy :: LHsType Name -> TcM (TyCon, [TcType])
 658 tcLHsConResTy (L span res_ty)
 659   = setSrcSpan span $
 660     case get_args res_ty [] of
 661            (HsTyVar tc_name, args)
 662               -> do { args' <- mapM dsHsType args
 663                     ; thing <- tcLookup tc_name
 664                     ; case thing of
 665                         AGlobal (ATyCon tc) -> return (tc, args')
 666                         _ -> failWithTc (badGadtDecl res_ty) }
 667            _ -> failWithTc (badGadtDecl res_ty)
 668   where
 669         -- We can't call dsHsType on res_ty, and then do tcSplitTyConApp_maybe
 670         -- because that causes a black hole, and for good reason.  Building
 671         -- the type means expanding type synonyms, and we can't do that
 672         -- inside the "knot".  So we have to work by steam.
 673     get_args (HsAppTy (L _ fun) arg)   args = get_args fun (arg:args)
 674     get_args (HsParTy (L _ ty))        args = get_args ty  args
 675     get_args (HsOpTy ty1 (L _ tc) ty2) args = (HsTyVar tc, ty1:ty2:args)
 676     get_args ty                        args = (ty, args)
 677
 678 badGadtDecl :: HsType Name -> SDoc
 679 badGadtDecl ty
 680   = hang (ptext (sLit "Malformed constructor result type:"))
 681        2 (ppr ty)
 682
 683 addKcTypeCtxt :: LHsType Name -> TcM a -> TcM a
 684         -- Wrap a context around only if we want to show that contexts.
 685 addKcTypeCtxt (L _ (HsPredTy _)) thing = thing
 686         -- Omit invisble ones and ones user's won't grok (HsPred p).
 687 addKcTypeCtxt (L _ other_ty) thing = addErrCtxt (typeCtxt other_ty) thing
 688
 689 typeCtxt :: HsType Name -> SDoc
 690 typeCtxt ty = ptext (sLit "In the type") <+> quotes (ppr ty)
 691 \end{code}
 692
 693 %************************************************************************
 694 %*                                                                      *
 695                 Type-variable binders
 696 %*                                                                      *
 697 %************************************************************************
 698
 699
 700 \begin{code}
 701 kcHsTyVars :: [LHsTyVarBndr Name]
 702            -> ([LHsTyVarBndr Name] -> TcM r)    -- These binders are kind-annotated
 703                                                 -- They scope over the thing inside
 704            -> TcM r
 705 kcHsTyVars tvs thing_inside  = do
 706     bndrs <- mapM (wrapLocM kcHsTyVar) tvs
 707     tcExtendKindEnvTvs bndrs (thing_inside bndrs)
 708
 709 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
 710         -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it
 711 kcHsTyVar (UserTyVar name)        = KindedTyVar name <$> newKindVar
 712 kcHsTyVar (KindedTyVar name kind) = return (KindedTyVar name kind)
 713
 714 ------------------
 715 tcTyVarBndrs :: [LHsTyVarBndr Name]     -- Kind-annotated binders, which need kind-zonking
 716              -> ([TyVar] -> TcM r)
 717              -> TcM r
 718 -- Used when type-checking types/classes/type-decls
 719 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
 720 tcTyVarBndrs bndrs thing_inside = do
 721     tyvars <- mapM (zonk . unLoc) bndrs
 722     tcExtendTyVarEnv tyvars (thing_inside tyvars)
 723   where
 724     zonk (KindedTyVar name kind) = do { kind' <- zonkTcKindToKind kind
 725                                       ; return (mkTyVar name kind') }
 726     zonk (UserTyVar name) = WARN( True, ptext (sLit "Un-kinded tyvar") <+> ppr name )
 727                             return (mkTyVar name liftedTypeKind)
 728
 729 -----------------------------------
 730 tcDataKindSig :: Maybe Kind -> TcM [TyVar]
 731 -- GADT decls can have a (perhaps partial) kind signature
 732 --      e.g.  data T :: * -> * -> * where ...
 733 -- This function makes up suitable (kinded) type variables for
 734 -- the argument kinds, and checks that the result kind is indeed *.
 735 -- We use it also to make up argument type variables for for data instances.
 736 tcDataKindSig Nothing = return []
 737 tcDataKindSig (Just kind)
 738   = do  { checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
 739         ; span <- getSrcSpanM
 740         ; us   <- newUniqueSupply
 741         ; let uniqs = uniqsFromSupply us
 742         ; return [ mk_tv span uniq str kind
 743                  | ((kind, str), uniq) <- arg_kinds `zip` dnames `zip` uniqs ] }
 744   where
 745     (arg_kinds, res_kind) = splitKindFunTys kind
 746     mk_tv loc uniq str kind = mkTyVar name kind
 747         where
 748            name = mkInternalName uniq occ loc
 749            occ  = mkOccName tvName str
 750
 751     dnames = map ('$' :) names  -- Note [Avoid name clashes for associated data types]
 752
 753     names :: [String]
 754     names = [ c:cs | cs <- "" : names, c <- ['a'..'z'] ]
 755
 756 badKindSig :: Kind -> SDoc
 757 badKindSig kind
 758  = hang (ptext (sLit "Kind signature on data type declaration has non-* return kind"))
 759         2 (ppr kind)
 760 \end{code}
 761
 762 Note [Avoid name clashes for associated data types]
 763 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 764 Consider    class C a b where
 765                data D b :: * -> *
 766 When typechecking the decl for D, we'll invent an extra type variable for D,
 767 to fill out its kind.  We *don't* want this type variable to be 'a', because
 768 in an .hi file we'd get
 769             class C a b where
 770                data D b a
 771 which makes it look as if there are *two* type indices.  But there aren't!
 772 So we use $a instead, which cannot clash with a user-written type variable.
 773 Remember that type variable binders in interface files are just FastStrings,
 774 not proper Names.
 775
 776 (The tidying phase can't help here because we don't tidy TyCons.  Another
 777 alternative would be to record the number of indexing parameters in the
 778 interface file.)
 779
 780
 781 %************************************************************************
 782 %*                                                                      *
 783                 Scoped type variables
 784 %*                                                                      *
 785 %************************************************************************
 786
 787
 788 tcAddScopedTyVars is used for scoped type variables added by pattern
 789 type signatures
 790         e.g.  \ ((x::a), (y::a)) -> x+y
 791 They never have explicit kinds (because this is source-code only)
 792 They are mutable (because they can get bound to a more specific type).
 793
 794 Usually we kind-infer and expand type splices, and then
 795 tupecheck/desugar the type.  That doesn't work well for scoped type
 796 variables, because they scope left-right in patterns.  (e.g. in the
 797 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
 798
 799 The current not-very-good plan is to
 800   * find all the types in the patterns
 801   * find their free tyvars
 802   * do kind inference
 803   * bring the kinded type vars into scope
 804   * BUT throw away the kind-checked type
 805         (we'll kind-check it again when we type-check the pattern)
 806
 807 This is bad because throwing away the kind checked type throws away
 808 its splices.  But too bad for now.  [July 03]
 809
 810 Historical note:
 811     We no longer specify that these type variables must be univerally
 812     quantified (lots of email on the subject).  If you want to put that
 813     back in, you need to
 814         a) Do a checkSigTyVars after thing_inside
 815         b) More insidiously, don't pass in expected_ty, else
 816            we unify with it too early and checkSigTyVars barfs
 817            Instead you have to pass in a fresh ty var, and unify
 818            it with expected_ty afterwards
 819
 820 \begin{code}
 821 tcHsPatSigType :: UserTypeCtxt
 822                -> LHsType Name          -- The type signature
 823                -> TcM ([TyVar],         -- Newly in-scope type variables
 824                         Type)           -- The signature
 825 -- Used for type-checking type signatures in
 826 -- (a) patterns           e.g  f (x::Int) = e
 827 -- (b) result signatures  e.g. g x :: Int = e
 828 -- (c) RULE forall bndrs  e.g. forall (x::Int). f x = x
 829
 830 tcHsPatSigType ctxt hs_ty
 831   = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
 832     do  {       -- Find the type variables that are mentioned in the type
 833                 -- but not already in scope.  These are the ones that
 834                 -- should be bound by the pattern signature
 835           in_scope <- getInLocalScope
 836         ; let span = getLoc hs_ty
 837               sig_tvs = [ L span (UserTyVar n)
 838                         | n <- nameSetToList (extractHsTyVars hs_ty),
 839                           not (in_scope n) ]
 840
 841         ; (tyvars, sig_ty) <- tcHsQuantifiedType sig_tvs hs_ty
 842         ; checkValidType ctxt sig_ty
 843         ; return (tyvars, sig_ty)
 844       }
 845
 846 tcPatSig :: UserTypeCtxt
 847          -> LHsType Name
 848          -> BoxySigmaType
 849          -> TcM (TcType,           -- The type to use for "inside" the signature
 850                  [(Name, TcType)], -- The new bit of type environment, binding
 851                                    -- the scoped type variables
 852                  CoercionI)        -- Coercion due to unification with actual ty
 853 tcPatSig ctxt sig res_ty
 854   = do  { (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig
 855
 856         ; if null sig_tvs then do {
 857                 -- The type signature binds no type variables,
 858                 -- and hence is rigid, so use it to zap the res_ty
 859                   coi <- boxyUnify sig_ty res_ty
 860                 ; return (sig_ty, [], coi)
 861
 862         } else do {
 863                 -- Type signature binds at least one scoped type variable
 864
 865                 -- A pattern binding cannot bind scoped type variables
 866                 -- The renamer fails with a name-out-of-scope error
 867                 -- if a pattern binding tries to bind a type variable,
 868                 -- So we just have an ASSERT here
 869         ; let in_pat_bind = case ctxt of
 870                                 BindPatSigCtxt -> True
 871                                 _              -> False
 872         ; ASSERT( not in_pat_bind || null sig_tvs ) return ()
 873
 874                 -- Check that pat_ty is rigid
 875         ; checkTc (isRigidTy res_ty) (wobblyPatSig sig_tvs)
 876
 877                 -- Now match the pattern signature against res_ty
 878                 -- For convenience, and uniform-looking error messages
 879                 -- we do the matching by allocating meta type variables,
 880                 -- unifying, and reading out the results.
 881                 -- This is a strictly local operation.
 882         ; box_tvs <- mapM tcInstBoxyTyVar sig_tvs
 883         ; coi <- boxyUnify (substTyWith sig_tvs (mkTyVarTys box_tvs) sig_ty)
 884                            res_ty
 885         ; sig_tv_tys <- mapM readFilledBox box_tvs
 886
 887                 -- Check that each is bound to a distinct type variable,
 888                 -- and one that is not already in scope
 889         ; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys
 890         ; binds_in_scope <- getScopedTyVarBinds
 891         ; check binds_in_scope tv_binds
 892
 893                 -- Phew!
 894         ; return (res_ty, tv_binds, coi)
 895         } }
 896   where
 897     check _ [] = return ()
 898     check in_scope ((n,ty):rest) = do { check_one in_scope n ty
 899                                       ; check ((n,ty):in_scope) rest }
 900
 901     check_one in_scope n ty
 902         = do { checkTc (tcIsTyVarTy ty) (scopedNonVar n ty)
 903                 -- Must bind to a type variable
 904
 905              ; checkTc (null dups) (dupInScope n (head dups) ty)
 906                 -- Must not bind to the same type variable
 907                 -- as some other in-scope type variable
 908
 909              ; return () }
 910         where
 911           dups = [n' | (n',ty') <- in_scope, tcEqType ty' ty]
 912 \end{code}
 913
 914
 915 %************************************************************************
 916 %*                                                                      *
 917         Checking kinds
 918 %*                                                                      *
 919 %************************************************************************
 920
 921 We would like to get a decent error message from
 922   (a) Under-applied type constructors
 923              f :: (Maybe, Maybe)
 924   (b) Over-applied type constructors
 925              f :: Int x -> Int x
 926
 927 \begin{code}
 928 -- The ExpKind datatype means "expected kind" and contains
 929 -- some info about just why that kind is expected, to improve
 930 -- the error message on a mis-match
 931 data ExpKind = EK TcKind EkCtxt
 932 data EkCtxt  = EkUnk            -- Unknown context
 933              | EkEqPred         -- Second argument of an equality predicate
 934              | EkKindSig        -- Kind signature
 935              | EkArg SDoc Int   -- Function, arg posn, expected kind
 936
 937
 938 ekLifted, ekOpen :: ExpKind
 939 ekLifted = EK liftedTypeKind EkUnk
 940 ekOpen   = EK openTypeKind   EkUnk
 941
 942 checkExpectedKind :: Outputable a => a -> TcKind -> ExpKind -> TcM ()
 943 -- A fancy wrapper for 'unifyKind', which tries
 944 -- to give decent error messages.
 945 --      (checkExpectedKind ty act_kind exp_kind)
 946 -- checks that the actual kind act_kind is compatible
 947 --      with the expected kind exp_kind
 948 -- The first argument, ty, is used only in the error message generation
 949 checkExpectedKind ty act_kind (EK exp_kind ek_ctxt)
 950   | act_kind `isSubKind` exp_kind -- Short cut for a very common case
 951   = return ()
 952   | otherwise = do
 953     (_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind)
 954     case mb_r of
 955         Just _  -> return ()  -- Unification succeeded
 956         Nothing -> do
 957
 958         -- So there's definitely an error
 959         -- Now to find out what sort
 960            exp_kind <- zonkTcKind exp_kind
 961            act_kind <- zonkTcKind act_kind
 962
 963            env0 <- tcInitTidyEnv
 964            let (exp_as, _) = splitKindFunTys exp_kind
 965                (act_as, _) = splitKindFunTys act_kind
 966                n_exp_as = length exp_as
 967                n_act_as = length act_as
 968
 969                (env1, tidy_exp_kind) = tidyKind env0 exp_kind
 970                (env2, tidy_act_kind) = tidyKind env1 act_kind
 971
 972                err | n_exp_as < n_act_as     -- E.g. [Maybe]
 973                    = quotes (ppr ty) <+> ptext (sLit "is not applied to enough type arguments")
 974
 975                      -- Now n_exp_as >= n_act_as. In the next two cases,
 976                      -- n_exp_as == 0, and hence so is n_act_as
 977                    | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
 978                    = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
 979                        <+> ptext (sLit "is unlifted")
 980
 981                    | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
 982                    = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
 983                        <+> ptext (sLit "is lifted")
 984
 985                    | otherwise               -- E.g. Monad [Int]
 986                    = ptext (sLit "Kind mis-match")
 987
 988                more_info = sep [ expected_herald ek_ctxt <+> ptext (sLit "kind")
 989                                     <+> quotes (pprKind tidy_exp_kind) <> comma,
 990                                  ptext (sLit "but") <+> quotes (ppr ty) <+>
 991                                      ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
 992
 993                expected_herald EkUnk     = ptext (sLit "Expected")
 994                expected_herald EkKindSig = ptext (sLit "An enclosing kind signature specified")
 995                expected_herald EkEqPred  = ptext (sLit "The left argument of the equality predicate had")
 996                expected_herald (EkArg fun arg_no)
 997                  = ptext (sLit "The") <+> speakNth arg_no <+> ptext (sLit "argument of")
 998                    <+> quotes fun <+> ptext (sLit ("should have"))
 999
1000            failWithTcM (env2, err $$ more_info)
1001 \end{code}
1002
1003 %************************************************************************
1004 %*                                                                      *
1005                 Scoped type variables
1006 %*                                                                      *
1007 %************************************************************************
1008
1009 \begin{code}
1010 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
1011 pprHsSigCtxt ctxt hs_ty = vcat [ ptext (sLit "In") <+> pprUserTypeCtxt ctxt <> colon,
1012                                  nest 2 (pp_sig ctxt) ]
1013   where
1014     pp_sig (FunSigCtxt n)  = pp_n_colon n
1015     pp_sig (ConArgCtxt n)  = pp_n_colon n
1016     pp_sig (ForSigCtxt n)  = pp_n_colon n
1017     pp_sig _               = ppr (unLoc hs_ty)
1018
1019     pp_n_colon n = ppr n <+> dcolon <+> ppr (unLoc hs_ty)
1020
1021 wobblyPatSig :: [Var] -> SDoc
1022 wobblyPatSig sig_tvs
1023   = hang (ptext (sLit "A pattern type signature cannot bind scoped type variables")
1024                 <+> pprQuotedList sig_tvs)
1025        2 (ptext (sLit "unless the pattern has a rigid type context"))
1026
1027 scopedNonVar :: Name -> Type -> SDoc
1028 scopedNonVar n ty
1029   = vcat [sep [ptext (sLit "The scoped type variable") <+> quotes (ppr n),
1030                nest 2 (ptext (sLit "is bound to the type") <+> quotes (ppr ty))],
1031           nest 2 (ptext (sLit "You can only bind scoped type variables to type variables"))]
1032
1033 dupInScope :: Name -> Name -> Type -> SDoc
1034 dupInScope n n' _
1035   = hang (ptext (sLit "The scoped type variables") <+> quotes (ppr n) <+> ptext (sLit "and") <+> quotes (ppr n'))
1036        2 (vcat [ptext (sLit "are bound to the same type (variable)"),
1037                 ptext (sLit "Distinct scoped type variables must be distinct")])
1038
1039 wrongEqualityErr :: TcM (HsType Name, TcKind)
1040 wrongEqualityErr
1041   = failWithTc (text "Equality predicate used as a type")
1042 \end{code}
1043