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