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 -- remove the doc nodes here, no need to worry about the location since
 422 -- its the same for a doc node and it's child type node
 423 kc_hs_type (HsDocTy ty _)
 424   = kc_hs_type (unLoc ty)
 425
 426 ---------------------------
 427 kcApps :: Outputable a
 428        => a
 429        -> TcKind                        -- Function kind
 430        -> [LHsType Name]                -- Arg types
 431        -> TcM ([LHsType Name], TcKind)  -- Kind-checked args
 432 kcApps the_fun fun_kind args
 433   = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
 434        ; args' <- kc_check_lhs_types args_w_kinds
 435        ; return (args', res_kind) }
 436
 437 kcCheckApps :: Outputable a => a -> TcKind -> [LHsType Name]
 438             -> HsType Name     -- The type being checked (for err messages only)
 439             -> ExpKind         -- Expected kind
 440             -> TcM [LHsType Name]
 441 kcCheckApps the_fun fun_kind args ty exp_kind
 442   = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
 443        ; checkExpectedKind ty res_kind exp_kind
 444              -- Check the result kind *before* checking argument kinds
 445              -- This improves error message; Trac #2994
 446        ; kc_check_lhs_types args_w_kinds }
 447
 448 splitHsAppTys :: LHsType Name -> LHsType Name -> (LHsType Name, [LHsType Name])
 449 splitHsAppTys fun_ty arg_ty = split fun_ty [arg_ty]
 450   where
 451     split (L _ (HsAppTy f a)) as = split f (a:as)
 452     split f                   as = (f,as)
 453
 454 mkHsAppTys :: LHsType Name -> [LHsType Name] -> HsType Name
 455 mkHsAppTys fun_ty [] = pprPanic "mkHsAppTys" (ppr fun_ty)
 456 mkHsAppTys fun_ty (arg_ty:arg_tys)
 457   = foldl mk_app (HsAppTy fun_ty arg_ty) arg_tys
 458   where
 459     mk_app fun arg = HsAppTy (noLoc fun) arg    -- Add noLocs for inner nodes of
 460                                                 -- the application; they are
 461                                                 -- never used
 462
 463 ---------------------------
 464 splitFunKind :: SDoc -> Int -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind)
 465 splitFunKind _       _      fk [] = return ([], fk)
 466 splitFunKind the_fun arg_no fk (arg:args)
 467   = do { mb_fk <- unifyFunKind fk
 468        ; case mb_fk of
 469             Nothing       -> failWithTc too_many_args
 470             Just (ak,fk') -> do { (aks, rk) <- splitFunKind the_fun (arg_no+1) fk' args
 471                                 ; return ((arg, EK ak (EkArg the_fun arg_no)):aks, rk) } }
 472   where
 473     too_many_args = quotes the_fun <+>
 474                     ptext (sLit "is applied to too many type arguments")
 475
 476 ---------------------------
 477 kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
 478 kcHsContext ctxt = wrapLocM (mapM kcHsLPred) ctxt
 479
 480 kcHsLPred :: LHsPred Name -> TcM (LHsPred Name)
 481 kcHsLPred = wrapLocM kcHsPred
 482
 483 kcHsPred :: HsPred Name -> TcM (HsPred Name)
 484 kcHsPred pred = do      -- Checks that the result is of kind liftedType
 485     (pred', kind) <- kc_pred pred
 486     checkExpectedKind pred kind ekLifted
 487     return pred'
 488
 489 ---------------------------
 490 kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)
 491         -- Does *not* check for a saturated
 492         -- application (reason: used from TcDeriv)
 493 kc_pred (HsIParam name ty)
 494   = do { (ty', kind) <- kc_lhs_type ty
 495        ; return (HsIParam name ty', kind)
 496        }
 497 kc_pred (HsClassP cls tys)
 498   = do { kind <- kcClass cls
 499        ; (tys', res_kind) <- kcApps cls kind tys
 500        ; return (HsClassP cls tys', res_kind)
 501        }
 502 kc_pred (HsEqualP ty1 ty2)
 503   = do { (ty1', kind1) <- kc_lhs_type ty1
 504 --       ; checkExpectedKind ty1 kind1 liftedTypeKind
 505        ; (ty2', kind2) <- kc_lhs_type ty2
 506 --       ; checkExpectedKind ty2 kind2 liftedTypeKind
 507        ; checkExpectedKind ty2 kind2 (EK kind1 EkEqPred)
 508        ; return (HsEqualP ty1' ty2', liftedTypeKind)
 509        }
 510
 511 ---------------------------
 512 kcTyVar :: Name -> TcM TcKind
 513 kcTyVar name = do       -- Could be a tyvar or a tycon
 514     traceTc (text "lk1" <+> ppr name)
 515     thing <- tcLookup name
 516     traceTc (text "lk2" <+> ppr name <+> ppr thing)
 517     case thing of
 518         ATyVar _ ty             -> return (typeKind ty)
 519         AThing kind             -> return kind
 520         AGlobal (ATyCon tc)     -> return (tyConKind tc)
 521         _                       -> wrongThingErr "type" thing name
 522
 523 kcClass :: Name -> TcM TcKind
 524 kcClass cls = do        -- Must be a class
 525     thing <- tcLookup cls
 526     case thing of
 527         AThing kind             -> return kind
 528         AGlobal (AClass cls)    -> return (tyConKind (classTyCon cls))
 529         _                       -> wrongThingErr "class" thing cls
 530 \end{code}
 531
 532
 533 %************************************************************************
 534 %*                                                                      *
 535                 Desugaring
 536 %*                                                                      *
 537 %************************************************************************
 538
 539 The type desugarer
 540
 541         * Transforms from HsType to Type
 542         * Zonks any kinds
 543
 544 It cannot fail, and does no validity checking, except for
 545 structural matters, such as
 546         (a) spurious ! annotations.
 547         (b) a class used as a type
 548
 549 \begin{code}
 550 dsHsType :: LHsType Name -> TcM Type
 551 -- All HsTyVarBndrs in the intput type are kind-annotated
 552 dsHsType ty = ds_type (unLoc ty)
 553
 554 ds_type :: HsType Name -> TcM Type
 555 ds_type ty@(HsTyVar _)
 556   = ds_app ty []
 557
 558 ds_type (HsParTy ty)            -- Remove the parentheses markers
 559   = dsHsType ty
 560
 561 ds_type ty@(HsBangTy {})    -- No bangs should be here
 562   = failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty)
 563
 564 ds_type ty@(HsRecTy {})     -- No bangs should be here
 565   = failWithTc (ptext (sLit "Unexpected record type:") <+> ppr ty)
 566
 567 ds_type (HsKindSig ty _)
 568   = dsHsType ty -- Kind checking done already
 569
 570 ds_type (HsListTy ty) = do
 571     tau_ty <- dsHsType ty
 572     checkWiredInTyCon listTyCon
 573     return (mkListTy tau_ty)
 574
 575 ds_type (HsPArrTy ty) = do
 576     tau_ty <- dsHsType ty
 577     checkWiredInTyCon parrTyCon
 578     return (mkPArrTy tau_ty)
 579
 580 ds_type (HsTupleTy boxity tys) = do
 581     tau_tys <- dsHsTypes tys
 582     checkWiredInTyCon tycon
 583     return (mkTyConApp tycon tau_tys)
 584   where
 585     tycon = tupleTyCon boxity (length tys)
 586
 587 ds_type (HsFunTy ty1 ty2) = do
 588     tau_ty1 <- dsHsType ty1
 589     tau_ty2 <- dsHsType ty2
 590     return (mkFunTy tau_ty1 tau_ty2)
 591
 592 ds_type (HsOpTy ty1 (L span op) ty2) = do
 593     tau_ty1 <- dsHsType ty1
 594     tau_ty2 <- dsHsType ty2
 595     setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
 596
 597 ds_type (HsNumTy n)
 598   = ASSERT(n==1) do
 599     tc <- tcLookupTyCon genUnitTyConName
 600     return (mkTyConApp tc [])
 601
 602 ds_type ty@(HsAppTy _ _)
 603   = ds_app ty []
 604
 605 ds_type (HsPredTy pred) = do
 606     pred' <- dsHsPred pred
 607     return (mkPredTy pred')
 608
 609 ds_type (HsForAllTy _ tv_names ctxt ty)
 610   = tcTyVarBndrs tv_names               $ \ tyvars -> do
 611     theta <- mapM dsHsLPred (unLoc ctxt)
 612     tau <- dsHsType ty
 613     return (mkSigmaTy tyvars theta tau)
 614
 615 ds_type (HsSpliceTy {}) = panic "ds_type: HsSpliceTy"
 616
 617 ds_type (HsDocTy ty _)  -- Remove the doc comment
 618   = dsHsType ty
 619
 620 dsHsTypes :: [LHsType Name] -> TcM [Type]
 621 dsHsTypes arg_tys = mapM dsHsType arg_tys
 622 \end{code}
 623
 624 Help functions for type applications
 625 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 626
 627 \begin{code}
 628 ds_app :: HsType Name -> [LHsType Name] -> TcM Type
 629 ds_app (HsAppTy ty1 ty2) tys
 630   = ds_app (unLoc ty1) (ty2:tys)
 631
 632 ds_app ty tys = do
 633     arg_tys <- dsHsTypes tys
 634     case ty of
 635         HsTyVar fun -> ds_var_app fun arg_tys
 636         _           -> do fun_ty <- ds_type ty
 637                           return (mkAppTys fun_ty arg_tys)
 638
 639 ds_var_app :: Name -> [Type] -> TcM Type
 640 ds_var_app name arg_tys = do
 641     thing <- tcLookup name
 642     case thing of
 643         ATyVar _ ty         -> return (mkAppTys ty arg_tys)
 644         AGlobal (ATyCon tc) -> return (mkTyConApp tc arg_tys)
 645         _                   -> wrongThingErr "type" thing name
 646 \end{code}
 647
 648
 649 Contexts
 650 ~~~~~~~~
 651
 652 \begin{code}
 653 dsHsLPred :: LHsPred Name -> TcM PredType
 654 dsHsLPred pred = dsHsPred (unLoc pred)
 655
 656 dsHsPred :: HsPred Name -> TcM PredType
 657 dsHsPred (HsClassP class_name tys)
 658   = do { arg_tys <- dsHsTypes tys
 659        ; clas <- tcLookupClass class_name
 660        ; return (ClassP clas arg_tys)
 661        }
 662 dsHsPred (HsEqualP ty1 ty2)
 663   = do { arg_ty1 <- dsHsType ty1
 664        ; arg_ty2 <- dsHsType ty2
 665        ; return (EqPred arg_ty1 arg_ty2)
 666        }
 667 dsHsPred (HsIParam name ty)
 668   = do { arg_ty <- dsHsType ty
 669        ; return (IParam name arg_ty)
 670        }
 671 \end{code}
 672
 673 GADT constructor signatures
 674
 675 \begin{code}
 676 tcLHsConResTy :: LHsType Name -> TcM (TyCon, [TcType])
 677 tcLHsConResTy (L span res_ty)
 678   = setSrcSpan span $
 679     case get_args res_ty [] of
 680            (HsTyVar tc_name, args)
 681               -> do { args' <- mapM dsHsType args
 682                     ; thing <- tcLookup tc_name
 683                     ; case thing of
 684                         AGlobal (ATyCon tc) -> return (tc, args')
 685                         _ -> failWithTc (badGadtDecl res_ty) }
 686            _ -> failWithTc (badGadtDecl res_ty)
 687   where
 688         -- We can't call dsHsType on res_ty, and then do tcSplitTyConApp_maybe
 689         -- because that causes a black hole, and for good reason.  Building
 690         -- the type means expanding type synonyms, and we can't do that
 691         -- inside the "knot".  So we have to work by steam.
 692     get_args (HsAppTy (L _ fun) arg)   args = get_args fun (arg:args)
 693     get_args (HsParTy (L _ ty))        args = get_args ty  args
 694     get_args (HsOpTy ty1 (L _ tc) ty2) args = (HsTyVar tc, ty1:ty2:args)
 695     get_args ty                        args = (ty, args)
 696
 697 badGadtDecl :: HsType Name -> SDoc
 698 badGadtDecl ty
 699   = hang (ptext (sLit "Malformed constructor result type:"))
 700        2 (ppr ty)
 701
 702 addKcTypeCtxt :: LHsType Name -> TcM a -> TcM a
 703         -- Wrap a context around only if we want to show that contexts.
 704 addKcTypeCtxt (L _ (HsPredTy _)) thing = thing
 705         -- Omit invisble ones and ones user's won't grok (HsPred p).
 706 addKcTypeCtxt (L _ other_ty) thing = addErrCtxt (typeCtxt other_ty) thing
 707
 708 typeCtxt :: HsType Name -> SDoc
 709 typeCtxt ty = ptext (sLit "In the type") <+> quotes (ppr ty)
 710 \end{code}
 711
 712 %************************************************************************
 713 %*                                                                      *
 714                 Type-variable binders
 715 %*                                                                      *
 716 %************************************************************************
 717
 718
 719 \begin{code}
 720 kcHsTyVars :: [LHsTyVarBndr Name]
 721            -> ([LHsTyVarBndr Name] -> TcM r)    -- These binders are kind-annotated
 722                                                 -- They scope over the thing inside
 723            -> TcM r
 724 kcHsTyVars tvs thing_inside  = do
 725     bndrs <- mapM (wrapLocM kcHsTyVar) tvs
 726     tcExtendKindEnvTvs bndrs (thing_inside bndrs)
 727
 728 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
 729         -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it
 730 kcHsTyVar (UserTyVar name)        = KindedTyVar name <$> newKindVar
 731 kcHsTyVar (KindedTyVar name kind) = return (KindedTyVar name kind)
 732
 733 ------------------
 734 tcTyVarBndrs :: [LHsTyVarBndr Name]     -- Kind-annotated binders, which need kind-zonking
 735              -> ([TyVar] -> TcM r)
 736              -> TcM r
 737 -- Used when type-checking types/classes/type-decls
 738 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
 739 tcTyVarBndrs bndrs thing_inside = do
 740     tyvars <- mapM (zonk . unLoc) bndrs
 741     tcExtendTyVarEnv tyvars (thing_inside tyvars)
 742   where
 743     zonk (KindedTyVar name kind) = do { kind' <- zonkTcKindToKind kind
 744                                       ; return (mkTyVar name kind') }
 745     zonk (UserTyVar name) = WARN( True, ptext (sLit "Un-kinded tyvar") <+> ppr name )
 746                             return (mkTyVar name liftedTypeKind)
 747
 748 -----------------------------------
 749 tcDataKindSig :: Maybe Kind -> TcM [TyVar]
 750 -- GADT decls can have a (perhaps partial) kind signature
 751 --      e.g.  data T :: * -> * -> * where ...
 752 -- This function makes up suitable (kinded) type variables for
 753 -- the argument kinds, and checks that the result kind is indeed *.
 754 -- We use it also to make up argument type variables for for data instances.
 755 tcDataKindSig Nothing = return []
 756 tcDataKindSig (Just kind)
 757   = do  { checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
 758         ; span <- getSrcSpanM
 759         ; us   <- newUniqueSupply
 760         ; let uniqs = uniqsFromSupply us
 761         ; return [ mk_tv span uniq str kind
 762                  | ((kind, str), uniq) <- arg_kinds `zip` dnames `zip` uniqs ] }
 763   where
 764     (arg_kinds, res_kind) = splitKindFunTys kind
 765     mk_tv loc uniq str kind = mkTyVar name kind
 766         where
 767            name = mkInternalName uniq occ loc
 768            occ  = mkOccName tvName str
 769
 770     dnames = map ('$' :) names  -- Note [Avoid name clashes for associated data types]
 771
 772     names :: [String]
 773     names = [ c:cs | cs <- "" : names, c <- ['a'..'z'] ]
 774
 775 badKindSig :: Kind -> SDoc
 776 badKindSig kind
 777  = hang (ptext (sLit "Kind signature on data type declaration has non-* return kind"))
 778         2 (ppr kind)
 779 \end{code}
 780
 781 Note [Avoid name clashes for associated data types]
 782 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 783 Consider    class C a b where
 784                data D b :: * -> *
 785 When typechecking the decl for D, we'll invent an extra type variable for D,
 786 to fill out its kind.  We *don't* want this type variable to be 'a', because
 787 in an .hi file we'd get
 788             class C a b where
 789                data D b a
 790 which makes it look as if there are *two* type indices.  But there aren't!
 791 So we use $a instead, which cannot clash with a user-written type variable.
 792 Remember that type variable binders in interface files are just FastStrings,
 793 not proper Names.
 794
 795 (The tidying phase can't help here because we don't tidy TyCons.  Another
 796 alternative would be to record the number of indexing parameters in the
 797 interface file.)
 798
 799
 800 %************************************************************************
 801 %*                                                                      *
 802                 Scoped type variables
 803 %*                                                                      *
 804 %************************************************************************
 805
 806
 807 tcAddScopedTyVars is used for scoped type variables added by pattern
 808 type signatures
 809         e.g.  \ ((x::a), (y::a)) -> x+y
 810 They never have explicit kinds (because this is source-code only)
 811 They are mutable (because they can get bound to a more specific type).
 812
 813 Usually we kind-infer and expand type splices, and then
 814 tupecheck/desugar the type.  That doesn't work well for scoped type
 815 variables, because they scope left-right in patterns.  (e.g. in the
 816 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
 817
 818 The current not-very-good plan is to
 819   * find all the types in the patterns
 820   * find their free tyvars
 821   * do kind inference
 822   * bring the kinded type vars into scope
 823   * BUT throw away the kind-checked type
 824         (we'll kind-check it again when we type-check the pattern)
 825
 826 This is bad because throwing away the kind checked type throws away
 827 its splices.  But too bad for now.  [July 03]
 828
 829 Historical note:
 830     We no longer specify that these type variables must be univerally
 831     quantified (lots of email on the subject).  If you want to put that
 832     back in, you need to
 833         a) Do a checkSigTyVars after thing_inside
 834         b) More insidiously, don't pass in expected_ty, else
 835            we unify with it too early and checkSigTyVars barfs
 836            Instead you have to pass in a fresh ty var, and unify
 837            it with expected_ty afterwards
 838
 839 \begin{code}
 840 tcHsPatSigType :: UserTypeCtxt
 841                -> LHsType Name          -- The type signature
 842                -> TcM ([TyVar],         -- Newly in-scope type variables
 843                         Type)           -- The signature
 844 -- Used for type-checking type signatures in
 845 -- (a) patterns           e.g  f (x::Int) = e
 846 -- (b) result signatures  e.g. g x :: Int = e
 847 -- (c) RULE forall bndrs  e.g. forall (x::Int). f x = x
 848
 849 tcHsPatSigType ctxt hs_ty
 850   = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
 851     do  {       -- Find the type variables that are mentioned in the type
 852                 -- but not already in scope.  These are the ones that
 853                 -- should be bound by the pattern signature
 854           in_scope <- getInLocalScope
 855         ; let span = getLoc hs_ty
 856               sig_tvs = [ L span (UserTyVar n)
 857                         | n <- nameSetToList (extractHsTyVars hs_ty),
 858                           not (in_scope n) ]
 859
 860         ; (tyvars, sig_ty) <- tcHsQuantifiedType sig_tvs hs_ty
 861         ; checkValidType ctxt sig_ty
 862         ; return (tyvars, sig_ty)
 863       }
 864
 865 tcPatSig :: UserTypeCtxt
 866          -> LHsType Name
 867          -> BoxySigmaType
 868          -> TcM (TcType,           -- The type to use for "inside" the signature
 869                  [(Name, TcType)], -- The new bit of type environment, binding
 870                                    -- the scoped type variables
 871                  CoercionI)        -- Coercion due to unification with actual ty
 872 tcPatSig ctxt sig res_ty
 873   = do  { (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig
 874
 875         ; if null sig_tvs then do {
 876                 -- The type signature binds no type variables,
 877                 -- and hence is rigid, so use it to zap the res_ty
 878                   coi <- boxyUnify sig_ty res_ty
 879                 ; return (sig_ty, [], coi)
 880
 881         } else do {
 882                 -- Type signature binds at least one scoped type variable
 883
 884                 -- A pattern binding cannot bind scoped type variables
 885                 -- The renamer fails with a name-out-of-scope error
 886                 -- if a pattern binding tries to bind a type variable,
 887                 -- So we just have an ASSERT here
 888         ; let in_pat_bind = case ctxt of
 889                                 BindPatSigCtxt -> True
 890                                 _              -> False
 891         ; ASSERT( not in_pat_bind || null sig_tvs ) return ()
 892
 893                 -- Check that pat_ty is rigid
 894         ; checkTc (isRigidTy res_ty) (wobblyPatSig sig_tvs)
 895
 896                 -- Check that all newly-in-scope tyvars are in fact
 897                 -- constrained by the pattern.  This catches tiresome
 898                 -- cases like
 899                 --      type T a = Int
 900                 --      f :: Int -> Int
 901                 --      f (x :: T a) = ...
 902                 -- Here 'a' doesn't get a binding.  Sigh
 903         ; let bad_tvs = filterOut (`elemVarSet` exactTyVarsOfType sig_ty) sig_tvs
 904         ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
 905
 906                 -- Now match the pattern signature against res_ty
 907                 -- For convenience, and uniform-looking error messages
 908                 -- we do the matching by allocating meta type variables,
 909                 -- unifying, and reading out the results.
 910                 -- This is a strictly local operation.
 911         ; box_tvs <- mapM tcInstBoxyTyVar sig_tvs
 912         ; coi <- boxyUnify (substTyWith sig_tvs (mkTyVarTys box_tvs) sig_ty)
 913                            res_ty
 914         ; sig_tv_tys <- mapM readFilledBox box_tvs
 915
 916                 -- Check that each is bound to a distinct type variable,
 917                 -- and one that is not already in scope
 918         ; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys
 919         ; binds_in_scope <- getScopedTyVarBinds
 920         ; check binds_in_scope tv_binds
 921
 922                 -- Phew!
 923         ; return (res_ty, tv_binds, coi)
 924         } }
 925   where
 926     check _ [] = return ()
 927     check in_scope ((n,ty):rest) = do { check_one in_scope n ty
 928                                       ; check ((n,ty):in_scope) rest }
 929
 930     check_one in_scope n ty
 931         = do { checkTc (tcIsTyVarTy ty) (scopedNonVar n ty)
 932                 -- Must bind to a type variable
 933
 934              ; checkTc (null dups) (dupInScope n (head dups) ty)
 935                 -- Must not bind to the same type variable
 936                 -- as some other in-scope type variable
 937
 938              ; return () }
 939         where
 940           dups = [n' | (n',ty') <- in_scope, tcEqType ty' ty]
 941 \end{code}
 942
 943
 944 %************************************************************************
 945 %*                                                                      *
 946         Checking kinds
 947 %*                                                                      *
 948 %************************************************************************
 949
 950 We would like to get a decent error message from
 951   (a) Under-applied type constructors
 952              f :: (Maybe, Maybe)
 953   (b) Over-applied type constructors
 954              f :: Int x -> Int x
 955
 956 \begin{code}
 957 -- The ExpKind datatype means "expected kind" and contains
 958 -- some info about just why that kind is expected, to improve
 959 -- the error message on a mis-match
 960 data ExpKind = EK TcKind EkCtxt
 961 data EkCtxt  = EkUnk            -- Unknown context
 962              | EkEqPred         -- Second argument of an equality predicate
 963              | EkKindSig        -- Kind signature
 964              | EkArg SDoc Int   -- Function, arg posn, expected kind
 965
 966
 967 ekLifted, ekOpen :: ExpKind
 968 ekLifted = EK liftedTypeKind EkUnk
 969 ekOpen   = EK openTypeKind   EkUnk
 970
 971 checkExpectedKind :: Outputable a => a -> TcKind -> ExpKind -> TcM ()
 972 -- A fancy wrapper for 'unifyKind', which tries
 973 -- to give decent error messages.
 974 --      (checkExpectedKind ty act_kind exp_kind)
 975 -- checks that the actual kind act_kind is compatible
 976 --      with the expected kind exp_kind
 977 -- The first argument, ty, is used only in the error message generation
 978 checkExpectedKind ty act_kind (EK exp_kind ek_ctxt)
 979   | act_kind `isSubKind` exp_kind -- Short cut for a very common case
 980   = return ()
 981   | otherwise = do
 982     (_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind)
 983     case mb_r of
 984         Just _  -> return ()  -- Unification succeeded
 985         Nothing -> do
 986
 987         -- So there's definitely an error
 988         -- Now to find out what sort
 989            exp_kind <- zonkTcKind exp_kind
 990            act_kind <- zonkTcKind act_kind
 991
 992            env0 <- tcInitTidyEnv
 993            let (exp_as, _) = splitKindFunTys exp_kind
 994                (act_as, _) = splitKindFunTys act_kind
 995                n_exp_as = length exp_as
 996                n_act_as = length act_as
 997
 998                (env1, tidy_exp_kind) = tidyKind env0 exp_kind
 999                (env2, tidy_act_kind) = tidyKind env1 act_kind
1000
1001                err | n_exp_as < n_act_as     -- E.g. [Maybe]
1002                    = quotes (ppr ty) <+> ptext (sLit "is not applied to enough type arguments")
1003
1004                      -- Now n_exp_as >= n_act_as. In the next two cases,
1005                      -- n_exp_as == 0, and hence so is n_act_as
1006                    | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
1007                    = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
1008                        <+> ptext (sLit "is unlifted")
1009
1010                    | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
1011                    = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
1012                        <+> ptext (sLit "is lifted")
1013
1014                    | otherwise               -- E.g. Monad [Int]
1015                    = ptext (sLit "Kind mis-match")
1016
1017                more_info = sep [ expected_herald ek_ctxt <+> ptext (sLit "kind")
1018                                     <+> quotes (pprKind tidy_exp_kind) <> comma,
1019                                  ptext (sLit "but") <+> quotes (ppr ty) <+>
1020                                      ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
1021
1022                expected_herald EkUnk     = ptext (sLit "Expected")
1023                expected_herald EkKindSig = ptext (sLit "An enclosing kind signature specified")
1024                expected_herald EkEqPred  = ptext (sLit "The left argument of the equality predicate had")
1025                expected_herald (EkArg fun arg_no)
1026                  = ptext (sLit "The") <+> speakNth arg_no <+> ptext (sLit "argument of")
1027                    <+> quotes fun <+> ptext (sLit ("should have"))
1028
1029            failWithTcM (env2, err $$ more_info)
1030 \end{code}
1031
1032 %************************************************************************
1033 %*                                                                      *
1034                 Scoped type variables
1035 %*                                                                      *
1036 %************************************************************************
1037
1038 \begin{code}
1039 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
1040 pprHsSigCtxt ctxt hs_ty = vcat [ ptext (sLit "In") <+> pprUserTypeCtxt ctxt <> colon,
1041                                  nest 2 (pp_sig ctxt) ]
1042   where
1043     pp_sig (FunSigCtxt n)  = pp_n_colon n
1044     pp_sig (ConArgCtxt n)  = pp_n_colon n
1045     pp_sig (ForSigCtxt n)  = pp_n_colon n
1046     pp_sig _               = ppr (unLoc hs_ty)
1047
1048     pp_n_colon n = ppr n <+> dcolon <+> ppr (unLoc hs_ty)
1049
1050 wobblyPatSig :: [Var] -> SDoc
1051 wobblyPatSig sig_tvs
1052   = hang (ptext (sLit "A pattern type signature cannot bind scoped type variables")
1053                 <+> pprQuotedList sig_tvs)
1054        2 (ptext (sLit "unless the pattern has a rigid type context"))
1055
1056 badPatSigTvs :: TcType -> [TyVar] -> SDoc
1057 badPatSigTvs sig_ty bad_tvs
1058   = vcat [ fsep [ptext (sLit "The type variable") <> plural bad_tvs,
1059                  quotes (pprWithCommas ppr bad_tvs),
1060                  ptext (sLit "should be bound by the pattern signature") <+> quotes (ppr sig_ty),
1061                  ptext (sLit "but are actually discarded by a type synonym") ]
1062          , ptext (sLit "To fix this, expand the type synonym")
1063          , ptext (sLit "[Note: I hope to lift this restriction in due course]") ]
1064
1065 scopedNonVar :: Name -> Type -> SDoc
1066 scopedNonVar n ty
1067   = vcat [sep [ptext (sLit "The scoped type variable") <+> quotes (ppr n),
1068                nest 2 (ptext (sLit "is bound to the type") <+> quotes (ppr ty))],
1069           nest 2 (ptext (sLit "You can only bind scoped type variables to type variables"))]
1070
1071 dupInScope :: Name -> Name -> Type -> SDoc
1072 dupInScope n n' _
1073   = hang (ptext (sLit "The scoped type variables") <+> quotes (ppr n) <+> ptext (sLit "and") <+> quotes (ppr n'))
1074        2 (vcat [ptext (sLit "are bound to the same type (variable)"),
1075                 ptext (sLit "Distinct scoped type variables must be distinct")])
1076
1077 wrongEqualityErr :: TcM (HsType Name, TcKind)
1078 wrongEqualityErr
1079   = failWithTc (text "Equality predicate used as a type")
1080 \end{code}
1081