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