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