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, tyVarsOfType,
  41                           mkArrowKinds, getTyVar_maybe, getTyVar,
  42                           tidyOpenType, tidyOpenTypes, tidyTyVar, tidyTyVars,
  43                           tyVarsOfType, tyVarsOfTypes, mkForAllTys
  44                         )
  45 import PprType          ( pprConstraint, pprType )
  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         check ct@(Class c tys) | ambiguous = failWithTc (ambigErr (c,tys) tau)
 218           where ct_vars             = tyVarsOfTypes tys
 219                 forall_tyvars       = map varName in_scope_vars
 220                 tau_vars            = tyVarsOfType tau
 221                 fds                 = instFunDepsOfTheta theta
 222                 tvFundep            = tyVarFunDep fds
 223                 extended_tau_vars   = oclose tvFundep tau_vars
 224                 ambig ct_var        = (varName ct_var `elem` forall_tyvars) &&
 225                                       not (ct_var `elemUFM` extended_tau_vars)
 226                 ambiguous           = foldUFM ((||) . ambig) False ct_vars
 227         check _ = returnTc ()
 228     in
 229     mapTc check theta                   `thenTc_`
 230     returnTc (body_kind, mkSigmaTy tyvars theta tau)
 231 \end{code}
 232
 233 Help functions for type applications
 234 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 235
 236 \begin{code}
 237 tc_app (HsAppTy ty1 ty2) tys
 238   = tc_app ty1 (ty2:tys)
 239
 240 tc_app ty tys
 241   | null tys
 242   = tc_fun_type ty []
 243
 244   | otherwise
 245   = tcAddErrCtxt (appKindCtxt pp_app)   $
 246     mapAndUnzipTc tc_type_kind tys      `thenTc` \ (arg_kinds, arg_tys) ->
 247     tc_fun_type ty arg_tys              `thenTc` \ (fun_kind, result_ty) ->
 248
 249         -- Check argument compatibility
 250     newKindVar                                  `thenNF_Tc` \ result_kind ->
 251     unifyKind fun_kind (mkArrowKinds arg_kinds result_kind)
 252                                         `thenTc_`
 253     returnTc (result_kind, result_ty)
 254   where
 255     pp_app = ppr ty <+> sep (map pprParendHsType tys)
 256
 257 -- (tc_fun_type ty arg_tys) returns (kind-of ty, mkAppTys ty arg_tys)
 258 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
 259 --      hence the rather strange functionality.
 260
 261 tc_fun_type (HsTyVar name) arg_tys
 262   = tcLookupTy name                     `thenTc` \ (tycon_kind, thing) ->
 263     case thing of
 264         ATyVar tv     -> returnTc (tycon_kind, mkAppTys (mkTyVarTy tv) arg_tys)
 265         AClass clas _ -> failWithTc (classAsTyConErr name)
 266
 267         ADataTyCon tc ->  -- Data or newtype
 268                           returnTc (tycon_kind, mkTyConApp tc arg_tys)
 269
 270         ASynTyCon tc arity ->   -- Type synonym
 271                                   checkTc (arity <= n_args) err_msg     `thenTc_`
 272                                   returnTc (tycon_kind, result_ty)
 273                            where
 274                                 -- It's OK to have an *over-applied* type synonym
 275                                 --      data Tree a b = ...
 276                                 --      type Foo a = Tree [a]
 277                                 --      f :: Foo a b -> ...
 278                               result_ty = mkAppTys (mkSynTy tc (take arity arg_tys))
 279                                                    (drop arity arg_tys)
 280                               err_msg = arityErr "type synonym" name arity n_args
 281                               n_args  = length arg_tys
 282
 283 tc_fun_type ty arg_tys
 284   = tc_type_kind ty             `thenTc` \ (fun_kind, fun_ty) ->
 285     returnTc (fun_kind, mkAppTys fun_ty arg_tys)
 286 \end{code}
 287
 288
 289 Contexts
 290 ~~~~~~~~
 291 \begin{code}
 292
 293 tcContext :: RenamedContext -> TcM s ThetaType
 294 tcContext context = mapTc (tcClassAssertion False) context
 295
 296 tcClassAssertion ccall_ok assn@(HsPClass class_name tys)
 297   = tcAddErrCtxt (appKindCtxt (ppr assn))       $
 298     mapAndUnzipTc tc_type_kind tys              `thenTc` \ (arg_kinds, arg_tys) ->
 299     tcLookupTy class_name                       `thenTc` \ (kind, thing) ->
 300     case thing of
 301         AClass clas arity ->
 302                         -- Check with kind mis-match
 303                 checkTc (arity == n_tys) err                            `thenTc_`
 304                 unifyKind kind (mkArrowKinds arg_kinds boxedTypeKind)   `thenTc_`
 305                 returnTc (Class clas arg_tys)
 306             where
 307                 n_tys = length tys
 308                 err   = arityErr "Class" class_name arity n_tys
 309         other -> failWithTc (tyVarAsClassErr class_name)
 310
 311 tcClassAssertion ccall_ok assn@(HsPIParam name ty)
 312   = tcAddErrCtxt (appKindCtxt (ppr assn))       $
 313     tc_type_kind ty     `thenTc` \ (arg_kind, arg_ty) ->
 314     returnTc (IParam name arg_ty)
 315 \end{code}
 316
 317
 318 %************************************************************************
 319 %*                                                                      *
 320 \subsection{Type variables, with knot tying!}
 321 %*                                                                      *
 322 %************************************************************************
 323
 324 \begin{code}
 325 tcExtendTopTyVarScope :: TcKind -> [HsTyVarBndr Name]
 326                       -> ([TcTyVar] -> TcKind -> TcM s a)
 327                       -> TcM s a
 328 tcExtendTopTyVarScope kind tyvar_names thing_inside
 329   = let
 330         (tyvars_w_kinds, result_kind) = zipFunTys tyvar_names kind
 331         tyvars                        = map mk_tv tyvars_w_kinds
 332     in
 333     tcExtendTyVarEnv tyvars (thing_inside tyvars result_kind)
 334   where
 335     mk_tv (UserTyVar name,    kind) = mkTyVar name kind
 336     mk_tv (IfaceTyVar name _, kind) = mkTyVar name kind
 337         -- NB: immutable tyvars, but perhaps with mutable kinds
 338
 339 tcExtendTyVarScope :: [HsTyVarBndr Name]
 340                    -> ([TcTyVar] -> TcM s a) -> TcM s a
 341 tcExtendTyVarScope tv_names thing_inside
 342   = mapNF_Tc tcHsTyVar tv_names         `thenNF_Tc` \ tyvars ->
 343     tcExtendTyVarEnv tyvars             $
 344     thing_inside tyvars
 345
 346 tcHsTyVar :: HsTyVarBndr Name -> NF_TcM s TcTyVar
 347 tcHsTyVar (UserTyVar name)       = newKindVar           `thenNF_Tc` \ kind ->
 348                                    tcNewMutTyVar name kind
 349         -- NB: mutable kind => mutable tyvar, so that zonking can bind
 350         -- the tyvar to its immutable form
 351
 352 tcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (mkTyVar name (kindToTcKind kind))
 353
 354 kcHsTyVar :: HsTyVarBndr name -> NF_TcM s TcKind
 355 kcHsTyVar (UserTyVar name)       = newKindVar
 356 kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (kindToTcKind kind)
 357 \end{code}
 358
 359
 360 %************************************************************************
 361 %*                                                                      *
 362 \subsection{Signatures}
 363 %*                                                                      *
 364 %************************************************************************
 365
 366 @tcSigs@ checks the signatures for validity, and returns a list of
 367 {\em freshly-instantiated} signatures.  That is, the types are already
 368 split up, and have fresh type variables installed.  All non-type-signature
 369 "RenamedSigs" are ignored.
 370
 371 The @TcSigInfo@ contains @TcTypes@ because they are unified with
 372 the variable's type, and after that checked to see whether they've
 373 been instantiated.
 374
 375 \begin{code}
 376 data TcSigInfo
 377   = TySigInfo
 378         Name                    -- N, the Name in corresponding binding
 379
 380         TcId                    -- *Polymorphic* binder for this value...
 381                                 -- Has name = N
 382
 383         [TcTyVar]               -- tyvars
 384         TcThetaType             -- theta
 385         TcTauType               -- tau
 386
 387         TcId                    -- *Monomorphic* binder for this value
 388                                 -- Does *not* have name = N
 389                                 -- Has type tau
 390
 391         [Inst]                  -- Empty if theta is null, or
 392                                 -- (method mono_id) otherwise
 393
 394         SrcLoc                  -- Of the signature
 395
 396 instance Outputable TcSigInfo where
 397     ppr (TySigInfo nm id tyvars theta tau _ inst loc) =
 398         ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
 399
 400 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
 401         -- Search for a particular signature
 402 maybeSig [] name = Nothing
 403 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
 404   | name == sig_name = Just sig
 405   | otherwise        = maybeSig sigs name
 406 \end{code}
 407
 408
 409 \begin{code}
 410 tcTySig :: RenamedSig -> TcM s TcSigInfo
 411
 412 tcTySig (Sig v ty src_loc)
 413  = tcAddSrcLoc src_loc $
 414    tcHsSigType ty                               `thenTc` \ sigma_tc_ty ->
 415    mkTcSig (mkVanillaId v sigma_tc_ty) src_loc  `thenNF_Tc` \ sig ->
 416    returnTc sig
 417
 418 mkTcSig :: TcId -> SrcLoc -> NF_TcM s TcSigInfo
 419 mkTcSig poly_id src_loc
 420   =     -- Instantiate this type
 421         -- It's important to do this even though in the error-free case
 422         -- we could just split the sigma_tc_ty (since the tyvars don't
 423         -- unified with anything).  But in the case of an error, when
 424         -- the tyvars *do* get unified with something, we want to carry on
 425         -- typechecking the rest of the program with the function bound
 426         -- to a pristine type, namely sigma_tc_ty
 427    let
 428         (tyvars, rho) = splitForAllTys (idType poly_id)
 429    in
 430    mapNF_Tc tcInstSigVar tyvars         `thenNF_Tc` \ tyvars' ->
 431         -- Make *signature* type variables
 432
 433    let
 434      tyvar_tys' = mkTyVarTys tyvars'
 435      rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
 436         -- mkTopTyVarSubst because the tyvars' are fresh
 437      (theta', tau') = splitRhoTy rho'
 438         -- This splitRhoTy tries hard to make sure that tau' is a type synonym
 439         -- wherever possible, which can improve interface files.
 440    in
 441    newMethodWithGivenTy SignatureOrigin
 442                 poly_id
 443                 tyvar_tys'
 444                 theta' tau'                     `thenNF_Tc` \ inst ->
 445         -- We make a Method even if it's not overloaded; no harm
 446    instFunDeps SignatureOrigin theta'           `thenNF_Tc` \ fds ->
 447
 448    returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) (inst : fds) src_loc)
 449   where
 450     name = idName poly_id
 451 \end{code}
 452
 453
 454
 455 %************************************************************************
 456 %*                                                                      *
 457 \subsection{Checking signature type variables}
 458 %*                                                                      *
 459 %************************************************************************
 460
 461 @checkSigTyVars@ is used after the type in a type signature has been unified with
 462 the actual type found.  It then checks that the type variables of the type signature
 463 are
 464         (a) Still all type variables
 465                 eg matching signature [a] against inferred type [(p,q)]
 466                 [then a will be unified to a non-type variable]
 467
 468         (b) Still all distinct
 469                 eg matching signature [(a,b)] against inferred type [(p,p)]
 470                 [then a and b will be unified together]
 471
 472         (c) Not mentioned in the environment
 473                 eg the signature for f in this:
 474
 475                         g x = ... where
 476                                         f :: a->[a]
 477                                         f y = [x,y]
 478
 479                 Here, f is forced to be monorphic by the free occurence of x.
 480
 481         (d) Not (unified with another type variable that is) in scope.
 482                 eg f x :: (r->r) = (\y->y) :: forall a. a->r
 483             when checking the expression type signature, we find that
 484             even though there is nothing in scope whose type mentions r,
 485             nevertheless the type signature for the expression isn't right.
 486
 487             Another example is in a class or instance declaration:
 488                 class C a where
 489                    op :: forall b. a -> b
 490                    op x = x
 491             Here, b gets unified with a
 492
 493 Before doing this, the substitution is applied to the signature type variable.
 494
 495 We used to have the notion of a "DontBind" type variable, which would
 496 only be bound to itself or nothing.  Then points (a) and (b) were
 497 self-checking.  But it gave rise to bogus consequential error messages.
 498 For example:
 499
 500    f = (*)      -- Monomorphic
 501
 502    g :: Num a => a -> a
 503    g x = f x x
 504
 505 Here, we get a complaint when checking the type signature for g,
 506 that g isn't polymorphic enough; but then we get another one when
 507 dealing with the (Num x) context arising from f's definition;
 508 we try to unify x with Int (to default it), but find that x has already
 509 been unified with the DontBind variable "a" from g's signature.
 510 This is really a problem with side-effecting unification; we'd like to
 511 undo g's effects when its type signature fails, but unification is done
 512 by side effect, so we can't (easily).
 513
 514 So we revert to ordinary type variables for signatures, and try to
 515 give a helpful message in checkSigTyVars.
 516
 517 \begin{code}
 518 checkSigTyVars :: [TcTyVar]             -- Universally-quantified type variables in the signature
 519                -> TcTyVarSet            -- Tyvars that are free in the type signature
 520                                         -- These should *already* be in the global-var set, and are
 521                                         -- used here only to improve the error message
 522                -> TcM s [TcTyVar]       -- Zonked signature type variables
 523
 524 checkSigTyVars [] free = returnTc []
 525
 526 checkSigTyVars sig_tyvars free_tyvars
 527   = zonkTcTyVars sig_tyvars             `thenNF_Tc` \ sig_tys ->
 528     tcGetGlobalTyVars                   `thenNF_Tc` \ globals ->
 529
 530     checkTcM (all_ok sig_tys globals)
 531              (complain sig_tys globals) `thenTc_`
 532
 533     returnTc (map (getTyVar "checkSigTyVars") sig_tys)
 534
 535   where
 536     all_ok []       acc = True
 537     all_ok (ty:tys) acc = case getTyVar_maybe ty of
 538                             Nothing                       -> False      -- Point (a)
 539                             Just tv | tv `elemVarSet` acc -> False      -- Point (b) or (c)
 540                                     | otherwise           -> all_ok tys (acc `extendVarSet` tv)
 541
 542
 543     complain sig_tys globals
 544       = -- For the in-scope ones, zonk them and construct a map
 545         -- from the zonked tyvar to the in-scope one
 546         -- If any of the in-scope tyvars zonk to a type, then ignore them;
 547         -- that'll be caught later when we back up to their type sig
 548         tcGetInScopeTyVars                      `thenNF_Tc` \ in_scope_tvs ->
 549         zonkTcTyVars in_scope_tvs               `thenNF_Tc` \ in_scope_tys ->
 550         let
 551             in_scope_assoc = [ (zonked_tv, in_scope_tv)
 552                              | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
 553                                Just zonked_tv <- [getTyVar_maybe z_ty]
 554                              ]
 555             in_scope_env = mkVarEnv in_scope_assoc
 556         in
 557
 558         -- "check" checks each sig tyvar in turn
 559         foldlNF_Tc check
 560                    (env2, in_scope_env, [])
 561                    (tidy_tvs `zip` tidy_tys)    `thenNF_Tc` \ (env3, _, msgs) ->
 562
 563         failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
 564       where
 565         (env1, tidy_tvs) = mapAccumL tidyTyVar emptyTidyEnv sig_tyvars
 566         (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
 567
 568         main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
 569
 570         check (env, acc, msgs) (sig_tyvar,ty)
 571                 -- sig_tyvar is from the signature;
 572                 -- ty is what you get if you zonk sig_tyvar and then tidy it
 573                 --
 574                 -- acc maps a zonked type variable back to a signature type variable
 575           = case getTyVar_maybe ty of {
 576               Nothing ->                        -- Error (a)!
 577                         returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr ty) : msgs) ;
 578
 579               Just tv ->
 580
 581             case lookupVarEnv acc tv of {
 582                 Just sig_tyvar' ->      -- Error (b) or (d)!
 583                         returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr sig_tyvar') : msgs) ;
 584
 585                 Nothing ->
 586
 587             if tv `elemVarSet` globals  -- Error (c)! Type variable escapes
 588                                         -- The least comprehensible, so put it last
 589             then   tcGetValueEnv                                        `thenNF_Tc` \ ve ->
 590                    find_globals tv env  [] (valueEnvIds ve)             `thenNF_Tc` \ (env1, globs) ->
 591                    find_frees   tv env1 [] (varSetElems free_tyvars)    `thenNF_Tc` \ (env2, frees) ->
 592                    returnNF_Tc (env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
 593
 594             else        -- All OK
 595             returnNF_Tc (env, extendVarEnv acc tv sig_tyvar, msgs)
 596             }}
 597
 598 -- find_globals looks at the value environment and finds values
 599 -- whose types mention the offending type variable.  It has to be
 600 -- careful to zonk the Id's type first, so it has to be in the monad.
 601 -- We must be careful to pass it a zonked type variable, too.
 602 find_globals tv tidy_env acc []
 603   = returnNF_Tc (tidy_env, acc)
 604
 605 find_globals tv tidy_env acc (id:ids)
 606   | not (isLocallyDefined id) ||
 607     isEmptyVarSet (idFreeTyVars id)
 608   = find_globals tv tidy_env acc ids
 609
 610   | otherwise
 611   = zonkTcType (idType id)      `thenNF_Tc` \ id_ty ->
 612     if tv `elemVarSet` tyVarsOfType id_ty then
 613         let
 614            (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
 615            acc'                = (idName id, id_ty') : acc
 616         in
 617         find_globals tv tidy_env' acc' ids
 618     else
 619         find_globals tv tidy_env  acc  ids
 620
 621 find_frees tv tidy_env acc []
 622   = returnNF_Tc (tidy_env, acc)
 623 find_frees tv tidy_env acc (ftv:ftvs)
 624   = zonkTcTyVar ftv     `thenNF_Tc` \ ty ->
 625     if tv `elemVarSet` tyVarsOfType ty then
 626         let
 627             (tidy_env', ftv') = tidyTyVar tidy_env ftv
 628         in
 629         find_frees tv tidy_env' (ftv':acc) ftvs
 630     else
 631         find_frees tv tidy_env  acc        ftvs
 632
 633
 634 escape_msg sig_tv tv globs frees
 635   = mk_msg sig_tv <+> ptext SLIT("escapes") $$
 636     if not (null globs) then
 637         vcat [pp_it <+> ptext SLIT("is mentioned in the environment"),
 638               ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
 639               nest 2 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
 640         ]
 641      else if not (null frees) then
 642         vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
 643               nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
 644         ]
 645      else
 646         empty   -- Sigh.  It's really hard to give a good error message
 647                 -- all the time.   One bad case is an existential pattern match
 648   where
 649     is_are | isSingleton frees = ptext SLIT("is")
 650            | otherwise         = ptext SLIT("are")
 651     pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
 652           | otherwise    = ptext SLIT("It")
 653
 654     vcat_first :: Int -> [SDoc] -> SDoc
 655     vcat_first n []     = empty
 656     vcat_first 0 (x:xs) = text "...others omitted..."
 657     vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
 658
 659 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> quotes thing
 660 mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
 661 \end{code}
 662
 663 These two context are used with checkSigTyVars
 664
 665 \begin{code}
 666 sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
 667         -> TidyEnv -> NF_TcM s (TidyEnv, Message)
 668 sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
 669   = zonkTcType sig_tau          `thenNF_Tc` \ actual_tau ->
 670     let
 671         (env1, tidy_sig_tyvars)  = tidyTyVars tidy_env sig_tyvars
 672         (env2, tidy_sig_rho)     = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
 673         (env3, tidy_actual_tau)  = tidyOpenType env1 actual_tau
 674         msg = vcat [ptext SLIT("Signature type:    ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
 675                     ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
 676                     when
 677                    ]
 678     in
 679     returnNF_Tc (env3, msg)
 680
 681 sigPatCtxt bound_tvs bound_ids tidy_env
 682   = returnNF_Tc (env1,
 683                  sep [ptext SLIT("When checking a pattern that binds"),
 684                       nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
 685   where
 686     show_ids = filter is_interesting bound_ids
 687     is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
 688
 689     (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
 690     ppr_id id ty     = ppr id <+> dcolon <+> ppr ty
 691         -- Don't zonk the types so we get the separate, un-unified versions
 692 \end{code}
 693
 694
 695 %************************************************************************
 696 %*                                                                      *
 697 \subsection{Errors and contexts}
 698 %*                                                                      *
 699 %************************************************************************
 700
 701 \begin{code}
 702 typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
 703
 704 typeKindCtxt :: RenamedHsType -> Message
 705 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
 706                        nest 2 (quotes (ppr ty)),
 707                        ptext SLIT("is a type")]
 708
 709 appKindCtxt :: SDoc -> Message
 710 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
 711
 712 classAsTyConErr name
 713   = ptext SLIT("Class used as a type constructor:") <+> ppr name
 714
 715 tyConAsClassErr name
 716   = ptext SLIT("Type constructor used as a class:") <+> ppr name
 717
 718 tyVarAsClassErr name
 719   = ptext SLIT("Type variable used as a class:") <+> ppr name
 720
 721 ambigErr (c, ts) ty
 722   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprConstraint c ts),
 723          nest 4 (ptext SLIT("for the type:") <+> ppr ty),
 724          nest 4 (ptext SLIT("Each forall'd type variable mentioned by the constraint must appear after the =>"))]
 725 \end{code}