ghc/compiler/typecheck/TcMonoType.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
   5
   6 \begin{code}
   7 module TcMonoType ( tcHsType, tcHsTypeKind, tcHsTopType, tcHsTopBoxedType, tcHsTopTypeKind,
   8                     tcContext, tcHsTyVar, kcHsTyVar,
   9                     tcExtendTyVarScope, tcExtendTopTyVarScope,
  10                     TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
  11                     checkSigTyVars, sigCtxt, sigPatCtxt
  12                   ) where
  13
  14 #include "HsVersions.h"
  15
  16 import HsSyn            ( HsType(..), HsTyVar(..), MonoUsageAnn(..),
  17                           Sig(..), HsPred(..), pprHsPred, pprParendHsType )
  18 import RnHsSyn          ( RenamedHsType, RenamedContext, RenamedSig )
  19 import TcHsSyn          ( TcId )
  20
  21 import TcMonad
  22 import TcEnv            ( tcExtendTyVarEnv, tcLookupTy, tcGetValueEnv, tcGetInScopeTyVars,
  23                           tcExtendUVarEnv, tcLookupUVar,
  24                           tcGetGlobalTyVars, valueEnvIds, TcTyThing(..)
  25                         )
  26 import TcType           ( TcType, TcKind, TcTyVar, TcThetaType, TcTauType,
  27                           typeToTcType, kindToTcKind,
  28                           newKindVar, tcInstSigVar,
  29                           zonkTcKindToKind, zonkTcTypeToType, zonkTcTyVars, zonkTcType
  30                         )
  31 import Inst             ( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr )
  32 import TcUnify          ( unifyKind, unifyKinds, unifyTypeKind )
  33 import Type             ( Type, PredType(..), ThetaType, UsageAnn(..),
  34                           mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy, mkUsgTy,
  35                           mkUsForAllTy, zipFunTys,
  36                           mkSigmaTy, mkDictTy, mkTyConApp, mkAppTys, splitForAllTys, splitRhoTy,
  37                           boxedTypeKind, unboxedTypeKind, tyVarsOfType,
  38                           mkArrowKinds, getTyVar_maybe, getTyVar,
  39                           tidyOpenType, tidyOpenTypes, tidyTyVar,
  40                           tyVarsOfType, tyVarsOfTypes
  41                         )
  42 import PprType          ( pprConstraint )
  43 import Subst            ( mkTopTyVarSubst, substTy )
  44 import Id               ( mkVanillaId, idName, idType, idFreeTyVars )
  45 import Var              ( TyVar, mkTyVar, mkNamedUVar, varName )
  46 import VarEnv
  47 import VarSet
  48 import Bag              ( bagToList )
  49 import ErrUtils         ( Message )
  50 import PrelInfo         ( cCallishClassKeys )
  51 import TyCon            ( TyCon )
  52 import Name             ( Name, OccName, isLocallyDefined )
  53 import TysWiredIn       ( mkListTy, mkTupleTy, mkUnboxedTupleTy )
  54 import UniqFM           ( elemUFM, foldUFM )
  55 import SrcLoc           ( SrcLoc )
  56 import Unique           ( Unique, Uniquable(..) )
  57 import Util             ( zipWithEqual, zipLazy, mapAccumL )
  58 import Outputable
  59 \end{code}
  60
  61
  62 %************************************************************************
  63 %*                                                                      *
  64 \subsection{Checking types}
  65 %*                                                                      *
  66 %************************************************************************
  67
  68 tcHsType and tcHsTypeKind
  69 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  70
  71 tcHsType checks that the type really is of kind Type!
  72
  73 \begin{code}
  74 tcHsType :: RenamedHsType -> TcM s TcType
  75 tcHsType ty
  76   = -- tcAddErrCtxt (typeCtxt ty)               $
  77     tc_type ty
  78
  79 tcHsTypeKind    :: RenamedHsType -> TcM s (TcKind, TcType)
  80 tcHsTypeKind ty
  81   = -- tcAddErrCtxt (typeCtxt ty)               $
  82     tc_type_kind ty
  83
  84 -- Type-check a type, *and* then lazily zonk it.  The important
  85 -- point is that this zonks all the uncommitted *kind* variables
  86 -- in kinds of any any nested for-all tyvars.
  87 -- There won't be any mutable *type* variables at all.
  88 --
  89 -- NOTE the forkNF_Tc.  This makes the zonking lazy, which is
  90 -- absolutely necessary.  During the type-checking of a recursive
  91 -- group of tycons/classes (TcTyClsDecls.tcGroup) we use an
  92 -- environment in which we aren't allowed to look at the actual
  93 -- tycons/classes returned from a lookup. Because tc_app does
  94 -- look at the tycon to build the type, we can't look at the type
  95 -- either, until we get out of the loop.   The fork delays the
  96 -- zonking till we've completed the loop.  Sigh.
  97
  98 tcHsTopType :: RenamedHsType -> TcM s Type
  99 tcHsTopType ty
 100   = -- tcAddErrCtxt (typeCtxt ty)               $
 101     tc_type ty                          `thenTc` \ ty' ->
 102     forkNF_Tc (zonkTcTypeToType ty')
 103
 104 tcHsTopTypeKind :: RenamedHsType -> TcM s (TcKind, Type)
 105 tcHsTopTypeKind ty
 106   = -- tcAddErrCtxt (typeCtxt ty)               $
 107     tc_type_kind ty                             `thenTc` \ (kind, ty') ->
 108     forkNF_Tc (zonkTcTypeToType ty')            `thenTc` \ zonked_ty ->
 109     returnNF_Tc (kind, zonked_ty)
 110
 111 tcHsTopBoxedType :: RenamedHsType -> TcM s Type
 112 tcHsTopBoxedType ty
 113   = -- tcAddErrCtxt (typeCtxt ty)               $
 114     tc_boxed_type ty                    `thenTc` \ ty' ->
 115     forkNF_Tc (zonkTcTypeToType ty')
 116 \end{code}
 117
 118
 119 The main work horse
 120 ~~~~~~~~~~~~~~~~~~~
 121
 122 \begin{code}
 123 tc_boxed_type :: RenamedHsType -> TcM s Type
 124 tc_boxed_type ty
 125   = tc_type_kind ty                                     `thenTc` \ (actual_kind, tc_ty) ->
 126     tcAddErrCtxt (typeKindCtxt ty)
 127                  (unifyKind boxedTypeKind actual_kind)  `thenTc_`
 128     returnTc tc_ty
 129
 130 tc_type :: RenamedHsType -> TcM s Type
 131 tc_type ty
 132         -- The type ty must be a *type*, but it can be boxed
 133         -- or unboxed.  So we check that is is of form (Type bv)
 134         -- using unifyTypeKind
 135   = tc_type_kind ty                             `thenTc` \ (actual_kind, tc_ty) ->
 136     tcAddErrCtxt (typeKindCtxt ty)
 137                  (unifyTypeKind actual_kind)    `thenTc_`
 138     returnTc tc_ty
 139
 140 tc_type_kind :: RenamedHsType -> TcM s (TcKind, Type)
 141 tc_type_kind ty@(MonoTyVar name)
 142   = tc_app ty []
 143
 144 tc_type_kind (MonoListTy ty)
 145   = tc_boxed_type ty            `thenTc` \ tau_ty ->
 146     returnTc (boxedTypeKind, mkListTy tau_ty)
 147
 148 tc_type_kind (MonoTupleTy tys True {-boxed-})
 149   = mapTc tc_boxed_type tys     `thenTc` \ tau_tys ->
 150     returnTc (boxedTypeKind, mkTupleTy (length tys) tau_tys)
 151
 152 tc_type_kind (MonoTupleTy tys False {-unboxed-})
 153   = mapTc tc_type tys                   `thenTc` \ tau_tys ->
 154     returnTc (unboxedTypeKind, mkUnboxedTupleTy (length tys) tau_tys)
 155
 156 tc_type_kind (MonoFunTy ty1 ty2)
 157   = tc_type ty1 `thenTc` \ tau_ty1 ->
 158     tc_type ty2 `thenTc` \ tau_ty2 ->
 159     returnTc (boxedTypeKind, mkFunTy tau_ty1 tau_ty2)
 160
 161 tc_type_kind (MonoTyApp ty1 ty2)
 162   = tc_app ty1 [ty2]
 163
 164 tc_type_kind (MonoDictTy class_name tys)
 165   = tcClassAssertion (HsPClass class_name tys)  `thenTc` \ (Class clas arg_tys) ->
 166     returnTc (boxedTypeKind, mkDictTy clas arg_tys)
 167
 168 tc_type_kind (MonoUsgTy usg ty)
 169   = newUsg usg                          `thenTc` \ usg' ->
 170     tc_type_kind ty                     `thenTc` \ (kind, tc_ty) ->
 171     returnTc (kind, mkUsgTy usg' tc_ty)
 172   where
 173     newUsg usg = case usg of
 174                    MonoUsOnce        -> returnTc UsOnce
 175                    MonoUsMany        -> returnTc UsMany
 176                    MonoUsVar uv_name -> tcLookupUVar uv_name `thenTc` \ uv ->
 177                                         returnTc (UsVar uv)
 178
 179 tc_type_kind (MonoUsgForAllTy uv_name ty)
 180   = let
 181         uv = mkNamedUVar uv_name
 182     in
 183     tcExtendUVarEnv uv_name uv $
 184       tc_type_kind ty                     `thenTc` \ (kind, tc_ty) ->
 185       returnTc (kind, mkUsForAllTy uv tc_ty)
 186
 187 tc_type_kind (HsForAllTy (Just tv_names) context ty)
 188   = tcExtendTyVarScope tv_names         $ \ tyvars ->
 189     tcContext context                   `thenTc` \ theta ->
 190     tc_type_kind ty                     `thenTc` \ (kind, tau) ->
 191     tcGetInScopeTyVars                  `thenTc` \ in_scope_vars ->
 192     let
 193         body_kind | null theta = kind
 194                   | otherwise  = boxedTypeKind
 195                 -- Context behaves like a function type
 196                 -- This matters.  Return-unboxed-tuple analysis can
 197                 -- give overloaded functions like
 198                 --      f :: forall a. Num a => (# a->a, a->a #)
 199                 -- And we want these to get through the type checker
 200         check ct@(Class c tys) | ambiguous = failWithTc (ambigErr (c,tys) tau)
 201                                | otherwise = returnTc ()
 202           where ct_vars = tyVarsOfTypes tys
 203                 forall_tyvars = map varName in_scope_vars
 204                 tau_vars = tyVarsOfType tau
 205                 ambig ct_var = (varName ct_var `elem` forall_tyvars) &&
 206                                not (ct_var `elemUFM` tau_vars)
 207                 ambiguous = foldUFM ((||) . ambig) False ct_vars
 208     in
 209     mapTc check theta                   `thenTc_`
 210     returnTc (body_kind, mkSigmaTy tyvars theta tau)
 211 \end{code}
 212
 213 Help functions for type applications
 214 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 215
 216 \begin{code}
 217 tc_app (MonoTyApp ty1 ty2) tys
 218   = tc_app ty1 (ty2:tys)
 219
 220 tc_app ty tys
 221   | null tys
 222   = tc_fun_type ty []
 223
 224   | otherwise
 225   = tcAddErrCtxt (appKindCtxt pp_app)   $
 226     mapAndUnzipTc tc_type_kind tys      `thenTc` \ (arg_kinds, arg_tys) ->
 227     tc_fun_type ty arg_tys              `thenTc` \ (fun_kind, result_ty) ->
 228
 229         -- Check argument compatibility
 230     newKindVar                                  `thenNF_Tc` \ result_kind ->
 231     unifyKind fun_kind (mkArrowKinds arg_kinds result_kind)
 232                                         `thenTc_`
 233     returnTc (result_kind, result_ty)
 234   where
 235     pp_app = ppr ty <+> sep (map pprParendHsType tys)
 236
 237 -- (tc_fun_type ty arg_tys) returns (kind-of ty, mkAppTys ty arg_tys)
 238 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
 239 --      hence the rather strange functionality.
 240
 241 tc_fun_type (MonoTyVar name) arg_tys
 242   = tcLookupTy name                     `thenTc` \ (tycon_kind, maybe_arity, thing) ->
 243     case thing of
 244         ATyVar tv   -> returnTc (tycon_kind, mkAppTys (mkTyVarTy tv) arg_tys)
 245         AClass clas -> failWithTc (classAsTyConErr name)
 246         ATyCon tc   -> case maybe_arity of
 247                          Nothing ->     -- Data or newtype
 248                                         returnTc (tycon_kind, mkTyConApp tc arg_tys)
 249
 250                          Just arity ->  -- Type synonym
 251                                   checkTc (arity <= n_args) err_msg     `thenTc_`
 252                                   returnTc (tycon_kind, result_ty)
 253                            where
 254                                 -- It's OK to have an *over-applied* type synonym
 255                                 --      data Tree a b = ...
 256                                 --      type Foo a = Tree [a]
 257                                 --      f :: Foo a b -> ...
 258                               result_ty = mkAppTys (mkSynTy tc (take arity arg_tys))
 259                                                    (drop arity arg_tys)
 260                               err_msg = arityErr "type synonym" name arity n_args
 261                               n_args  = length arg_tys
 262
 263 tc_fun_type ty arg_tys
 264   = tc_type_kind ty             `thenTc` \ (fun_kind, fun_ty) ->
 265     returnTc (fun_kind, mkAppTys fun_ty arg_tys)
 266 \end{code}
 267
 268
 269 Contexts
 270 ~~~~~~~~
 271 \begin{code}
 272
 273 tcContext :: RenamedContext -> TcM s ThetaType
 274 tcContext context
 275   =     --Someone discovered that @CCallable@ and @CReturnable@
 276         -- could be used in contexts such as:
 277         --      foo :: CCallable a => a -> PrimIO Int
 278         -- Doing this utterly wrecks the whole point of introducing these
 279         -- classes so we specifically check that this isn't being done.
 280         --
 281         -- We *don't* do this check in tcClassAssertion, because that's
 282         -- called when checking a HsDictTy, and we don't want to reject
 283         --      instance CCallable Int
 284         -- etc. Ugh!
 285     mapTc check_naughty context `thenTc_`
 286
 287     mapTc tcClassAssertion context
 288
 289  where
 290    check_naughty (HsPClass class_name _)
 291      = checkTc (not (getUnique class_name `elem` cCallishClassKeys))
 292                (naughtyCCallContextErr class_name)
 293    check_naughty (HsPIParam _ _) = returnTc ()
 294
 295 tcClassAssertion assn@(HsPClass class_name tys)
 296   = tcAddErrCtxt (appKindCtxt (pprHsPred assn)) $
 297     mapAndUnzipTc tc_type_kind tys      `thenTc` \ (arg_kinds, arg_tys) ->
 298     tcLookupTy class_name               `thenTc` \ (kind, ~(Just arity), thing) ->
 299     case thing of
 300         ATyVar  _   -> failWithTc (tyVarAsClassErr class_name)
 301         ATyCon  _   -> failWithTc (tyConAsClassErr class_name)
 302         AClass clas ->
 303                         -- Check with kind mis-match
 304                 checkTc (arity == n_tys) err                            `thenTc_`
 305                 unifyKind kind (mkArrowKinds arg_kinds boxedTypeKind)   `thenTc_`
 306                 returnTc (Class clas arg_tys)
 307             where
 308                 n_tys = length tys
 309                 err   = arityErr "Class" class_name arity n_tys
 310 tcClassAssertion assn@(HsPIParam name ty)
 311   = tcAddErrCtxt (appKindCtxt (pprHsPred assn)) $
 312     tc_type_kind ty     `thenTc` \ (arg_kind, arg_ty) ->
 313     returnTc (IParam name arg_ty)
 314 \end{code}
 315
 316
 317 %************************************************************************
 318 %*                                                                      *
 319 \subsection{Type variables, with knot tying!}
 320 %*                                                                      *
 321 %************************************************************************
 322
 323 \begin{code}
 324 tcExtendTopTyVarScope :: TcKind -> [HsTyVar Name]
 325                       -> ([TcTyVar] -> TcKind -> TcM s a)
 326                       -> TcM s a
 327 tcExtendTopTyVarScope kind tyvar_names thing_inside
 328   = let
 329         (tyvars_w_kinds, result_kind) = zipFunTys tyvar_names kind
 330         tyvars                        = map mk_tv tyvars_w_kinds
 331     in
 332     tcExtendTyVarEnv tyvars (thing_inside tyvars result_kind)
 333   where
 334     mk_tv (UserTyVar name,    kind) = mkTyVar name kind
 335     mk_tv (IfaceTyVar name _, kind) = mkTyVar name kind
 336         -- NB: immutable tyvars, but perhaps with mutable kinds
 337
 338 tcExtendTyVarScope :: [HsTyVar Name]
 339                    -> ([TcTyVar] -> TcM s a) -> TcM s a
 340 tcExtendTyVarScope tv_names thing_inside
 341   = mapNF_Tc tcHsTyVar tv_names         `thenNF_Tc` \ tyvars ->
 342     tcExtendTyVarEnv tyvars             $
 343     thing_inside tyvars
 344
 345 tcHsTyVar :: HsTyVar Name -> NF_TcM s TcTyVar
 346 tcHsTyVar (UserTyVar name)       = newKindVar           `thenNF_Tc` \ kind ->
 347                                    tcNewMutTyVar name kind
 348         -- NB: mutable kind => mutable tyvar, so that zonking can bind
 349         -- the tyvar to its immutable form
 350
 351 tcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (mkTyVar name (kindToTcKind kind))
 352
 353 kcHsTyVar :: HsTyVar name -> NF_TcM s TcKind
 354 kcHsTyVar (UserTyVar name)       = newKindVar
 355 kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (kindToTcKind kind)
 356 \end{code}
 357
 358
 359 %************************************************************************
 360 %*                                                                      *
 361 \subsection{Signatures}
 362 %*                                                                      *
 363 %************************************************************************
 364
 365 @tcSigs@ checks the signatures for validity, and returns a list of
 366 {\em freshly-instantiated} signatures.  That is, the types are already
 367 split up, and have fresh type variables installed.  All non-type-signature
 368 "RenamedSigs" are ignored.
 369
 370 The @TcSigInfo@ contains @TcTypes@ because they are unified with
 371 the variable's type, and after that checked to see whether they've
 372 been instantiated.
 373
 374 \begin{code}
 375 data TcSigInfo
 376   = TySigInfo
 377         Name                    -- N, the Name in corresponding binding
 378
 379         TcId                    -- *Polymorphic* binder for this value...
 380                                 -- Has name = N
 381
 382         [TcTyVar]               -- tyvars
 383         TcThetaType             -- theta
 384         TcTauType               -- tau
 385
 386         TcId                    -- *Monomorphic* binder for this value
 387                                 -- Does *not* have name = N
 388                                 -- Has type tau
 389
 390         Inst                    -- Empty if theta is null, or
 391                                 -- (method mono_id) otherwise
 392
 393         SrcLoc                  -- Of the signature
 394
 395
 396 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
 397         -- Search for a particular signature
 398 maybeSig [] name = Nothing
 399 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
 400   | name == sig_name = Just sig
 401   | otherwise        = maybeSig sigs name
 402 \end{code}
 403
 404
 405 \begin{code}
 406 tcTySig :: RenamedSig -> TcM s TcSigInfo
 407
 408 tcTySig (Sig v ty src_loc)
 409  = tcAddSrcLoc src_loc $
 410    tcHsType ty                                  `thenTc` \ sigma_tc_ty ->
 411    mkTcSig (mkVanillaId v sigma_tc_ty) src_loc  `thenNF_Tc` \ sig ->
 412    returnTc sig
 413
 414 mkTcSig :: TcId -> SrcLoc -> NF_TcM s TcSigInfo
 415 mkTcSig poly_id src_loc
 416   =     -- Instantiate this type
 417         -- It's important to do this even though in the error-free case
 418         -- we could just split the sigma_tc_ty (since the tyvars don't
 419         -- unified with anything).  But in the case of an error, when
 420         -- the tyvars *do* get unified with something, we want to carry on
 421         -- typechecking the rest of the program with the function bound
 422         -- to a pristine type, namely sigma_tc_ty
 423    let
 424         (tyvars, rho) = splitForAllTys (idType poly_id)
 425    in
 426    mapNF_Tc tcInstSigVar tyvars         `thenNF_Tc` \ tyvars' ->
 427         -- Make *signature* type variables
 428
 429    let
 430      tyvar_tys' = mkTyVarTys tyvars'
 431      rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
 432         -- mkTopTyVarSubst because the tyvars' are fresh
 433      (theta', tau') = splitRhoTy rho'
 434         -- This splitRhoTy tries hard to make sure that tau' is a type synonym
 435         -- wherever possible, which can improve interface files.
 436    in
 437    newMethodWithGivenTy SignatureOrigin
 438                 poly_id
 439                 tyvar_tys'
 440                 theta' tau'                     `thenNF_Tc` \ inst ->
 441         -- We make a Method even if it's not overloaded; no harm
 442
 443    returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) inst src_loc)
 444   where
 445     name = idName poly_id
 446 \end{code}
 447
 448
 449
 450 %************************************************************************
 451 %*                                                                      *
 452 \subsection{Checking signature type variables}
 453 %*                                                                      *
 454 %************************************************************************
 455
 456 @checkSigTyVars@ is used after the type in a type signature has been unified with
 457 the actual type found.  It then checks that the type variables of the type signature
 458 are
 459         (a) Still all type variables
 460                 eg matching signature [a] against inferred type [(p,q)]
 461                 [then a will be unified to a non-type variable]
 462
 463         (b) Still all distinct
 464                 eg matching signature [(a,b)] against inferred type [(p,p)]
 465                 [then a and b will be unified together]
 466
 467         (c) Not mentioned in the environment
 468                 eg the signature for f in this:
 469
 470                         g x = ... where
 471                                         f :: a->[a]
 472                                         f y = [x,y]
 473
 474                 Here, f is forced to be monorphic by the free occurence of x.
 475
 476         (d) Not (unified with another type variable that is) in scope.
 477                 eg f x :: (r->r) = (\y->y) :: forall a. a->r
 478             when checking the expression type signature, we find that
 479             even though there is nothing in scope whose type mentions r,
 480             nevertheless the type signature for the expression isn't right.
 481
 482             Another example is in a class or instance declaration:
 483                 class C a where
 484                    op :: forall b. a -> b
 485                    op x = x
 486             Here, b gets unified with a
 487
 488 Before doing this, the substitution is applied to the signature type variable.
 489
 490 We used to have the notion of a "DontBind" type variable, which would
 491 only be bound to itself or nothing.  Then points (a) and (b) were
 492 self-checking.  But it gave rise to bogus consequential error messages.
 493 For example:
 494
 495    f = (*)      -- Monomorphic
 496
 497    g :: Num a => a -> a
 498    g x = f x x
 499
 500 Here, we get a complaint when checking the type signature for g,
 501 that g isn't polymorphic enough; but then we get another one when
 502 dealing with the (Num x) context arising from f's definition;
 503 we try to unify x with Int (to default it), but find that x has already
 504 been unified with the DontBind variable "a" from g's signature.
 505 This is really a problem with side-effecting unification; we'd like to
 506 undo g's effects when its type signature fails, but unification is done
 507 by side effect, so we can't (easily).
 508
 509 So we revert to ordinary type variables for signatures, and try to
 510 give a helpful message in checkSigTyVars.
 511
 512 \begin{code}
 513 checkSigTyVars :: [TcTyVar]             -- The original signature type variables
 514                -> TcM s [TcTyVar]       -- Zonked signature type variables
 515
 516 checkSigTyVars [] = returnTc []
 517
 518 checkSigTyVars sig_tyvars
 519   = zonkTcTyVars sig_tyvars             `thenNF_Tc` \ sig_tys ->
 520     tcGetGlobalTyVars                   `thenNF_Tc` \ globals ->
 521
 522     checkTcM (all_ok sig_tys globals)
 523              (complain sig_tys globals) `thenTc_`
 524
 525     returnTc (map (getTyVar "checkSigTyVars") sig_tys)
 526
 527   where
 528     all_ok []       acc = True
 529     all_ok (ty:tys) acc = case getTyVar_maybe ty of
 530                             Nothing                       -> False      -- Point (a)
 531                             Just tv | tv `elemVarSet` acc -> False      -- Point (b) or (c)
 532                                     | otherwise           -> all_ok tys (acc `extendVarSet` tv)
 533
 534
 535     complain sig_tys globals
 536       = -- For the in-scope ones, zonk them and construct a map
 537         -- from the zonked tyvar to the in-scope one
 538         -- If any of the in-scope tyvars zonk to a type, then ignore them;
 539         -- that'll be caught later when we back up to their type sig
 540         tcGetInScopeTyVars                      `thenNF_Tc` \ in_scope_tvs ->
 541         zonkTcTyVars in_scope_tvs               `thenNF_Tc` \ in_scope_tys ->
 542         let
 543             in_scope_assoc = [ (zonked_tv, in_scope_tv)
 544                              | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
 545                                Just zonked_tv <- [getTyVar_maybe z_ty]
 546                              ]
 547             in_scope_env = mkVarEnv in_scope_assoc
 548         in
 549
 550         -- "check" checks each sig tyvar in turn
 551         foldlNF_Tc check
 552                    (env2, in_scope_env, [])
 553                    (tidy_tvs `zip` tidy_tys)    `thenNF_Tc` \ (env3, _, msgs) ->
 554
 555         failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
 556       where
 557         (env1, tidy_tvs) = mapAccumL tidyTyVar emptyTidyEnv sig_tyvars
 558         (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
 559
 560         main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
 561
 562         check (env, acc, msgs) (sig_tyvar,ty)
 563                 -- sig_tyvar is from the signature;
 564                 -- ty is what you get if you zonk sig_tyvar and then tidy it
 565                 --
 566                 -- acc maps a zonked type variable back to a signature type variable
 567           = case getTyVar_maybe ty of {
 568               Nothing ->                        -- Error (a)!
 569                         returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr ty) : msgs) ;
 570
 571               Just tv ->
 572
 573             case lookupVarEnv acc tv of {
 574                 Just sig_tyvar' ->      -- Error (b) or (d)!
 575                         returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr sig_tyvar') : msgs) ;
 576
 577                 Nothing ->
 578
 579             if tv `elemVarSet` globals  -- Error (c)! Type variable escapes
 580                                         -- The least comprehensible, so put it last
 581             then   tcGetValueEnv                        `thenNF_Tc` \ ve ->
 582                    find_globals tv env (valueEnvIds ve) `thenNF_Tc` \ (env1, globs) ->
 583                    returnNF_Tc (env1, acc, escape_msg sig_tyvar tv globs : msgs)
 584
 585             else        -- All OK
 586             returnNF_Tc (env, extendVarEnv acc tv sig_tyvar, msgs)
 587             }}
 588
 589 -- find_globals looks at the value environment and finds values
 590 -- whose types mention the offending type variable.  It has to be
 591 -- careful to zonk the Id's type first, so it has to be in the monad.
 592 -- We must be careful to pass it a zonked type variable, too.
 593 find_globals tv tidy_env ids
 594   | null ids
 595   = returnNF_Tc (tidy_env, [])
 596
 597 find_globals tv tidy_env (id:ids)
 598   | not (isLocallyDefined id) ||
 599     isEmptyVarSet (idFreeTyVars id)
 600   = find_globals tv tidy_env ids
 601
 602   | otherwise
 603   = zonkTcType (idType id)      `thenNF_Tc` \ id_ty ->
 604     if tv `elemVarSet` tyVarsOfType id_ty then
 605         let
 606            (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
 607         in
 608         find_globals tv tidy_env' ids   `thenNF_Tc` \ (tidy_env'', globs) ->
 609         returnNF_Tc (tidy_env'', (idName id, id_ty') : globs)
 610     else
 611         find_globals tv tidy_env ids
 612
 613 escape_msg sig_tv tv globs
 614   = vcat [mk_msg sig_tv <+> ptext SLIT("escapes"),
 615           pp_escape,
 616           ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
 617           nest 4 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
 618     ]
 619   where
 620     pp_escape | sig_tv /= tv = ptext SLIT("It unifies with") <+>
 621                                quotes (ppr tv) <> comma <+>
 622                                ptext SLIT("which is mentioned in the environment")
 623               | otherwise    = ptext SLIT("It is mentioned in the environment")
 624
 625     vcat_first :: Int -> [SDoc] -> SDoc
 626     vcat_first n []     = empty
 627     vcat_first 0 (x:xs) = text "...others omitted..."
 628     vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
 629
 630 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> quotes thing
 631 mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
 632 \end{code}
 633
 634 These two context are used with checkSigTyVars
 635
 636 \begin{code}
 637 sigCtxt :: (Type -> Message) -> Type
 638         -> TidyEnv -> NF_TcM s (TidyEnv, Message)
 639 sigCtxt mk_msg sig_ty tidy_env
 640   = let
 641         (env1, tidy_sig_ty) = tidyOpenType tidy_env sig_ty
 642     in
 643     returnNF_Tc (env1, mk_msg tidy_sig_ty)
 644
 645 sigPatCtxt bound_tvs bound_ids tidy_env
 646   = returnNF_Tc (env1,
 647                  sep [ptext SLIT("When checking a pattern that binds"),
 648                       nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
 649   where
 650     show_ids = filter is_interesting bound_ids
 651     is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
 652
 653     (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
 654     ppr_id id ty     = ppr id <+> dcolon <+> ppr ty
 655         -- Don't zonk the types so we get the separate, un-unified versions
 656 \end{code}
 657
 658
 659 %************************************************************************
 660 %*                                                                      *
 661 \subsection{Errors and contexts}
 662 %*                                                                      *
 663 %************************************************************************
 664
 665 \begin{code}
 666 naughtyCCallContextErr clas_name
 667   = sep [ptext SLIT("Can't use class") <+> quotes (ppr clas_name),
 668          ptext SLIT("in a context")]
 669
 670 typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
 671
 672 typeKindCtxt :: RenamedHsType -> Message
 673 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
 674                        nest 2 (quotes (ppr ty)),
 675                        ptext SLIT("is a type")]
 676
 677 appKindCtxt :: SDoc -> Message
 678 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
 679
 680 classAsTyConErr name
 681   = ptext SLIT("Class used as a type constructor:") <+> ppr name
 682
 683 tyConAsClassErr name
 684   = ptext SLIT("Type constructor used as a class:") <+> ppr name
 685
 686 tyVarAsClassErr name
 687   = ptext SLIT("Type variable used as a class:") <+> ppr name
 688
 689 ambigErr (c, ts) ty
 690   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprConstraint c ts),
 691          nest 4 (ptext SLIT("for the type:") <+> ppr ty),
 692          nest 4 (ptext SLIT("Each forall'd type variable mentioned by the constraint must appear after the =>."))]
 693 \end{code}