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