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