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
  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,
  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 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]             -- The original signature type variables
 536                -> TcM s [TcTyVar]       -- Zonked signature type variables
 537
 538 checkSigTyVars [] = returnTc []
 539
 540 checkSigTyVars sig_tyvars
 541   = zonkTcTyVars sig_tyvars             `thenNF_Tc` \ sig_tys ->
 542     tcGetGlobalTyVars                   `thenNF_Tc` \ globals ->
 543
 544     checkTcM (all_ok sig_tys globals)
 545              (complain sig_tys globals) `thenTc_`
 546
 547     returnTc (map (getTyVar "checkSigTyVars") sig_tys)
 548
 549   where
 550     all_ok []       acc = True
 551     all_ok (ty:tys) acc = case getTyVar_maybe ty of
 552                             Nothing                       -> False      -- Point (a)
 553                             Just tv | tv `elemVarSet` acc -> False      -- Point (b) or (c)
 554                                     | otherwise           -> all_ok tys (acc `extendVarSet` tv)
 555
 556
 557     complain sig_tys globals
 558       = -- For the in-scope ones, zonk them and construct a map
 559         -- from the zonked tyvar to the in-scope one
 560         -- If any of the in-scope tyvars zonk to a type, then ignore them;
 561         -- that'll be caught later when we back up to their type sig
 562         tcGetInScopeTyVars                      `thenNF_Tc` \ in_scope_tvs ->
 563         zonkTcTyVars in_scope_tvs               `thenNF_Tc` \ in_scope_tys ->
 564         let
 565             in_scope_assoc = [ (zonked_tv, in_scope_tv)
 566                              | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
 567                                Just zonked_tv <- [getTyVar_maybe z_ty]
 568                              ]
 569             in_scope_env = mkVarEnv in_scope_assoc
 570         in
 571
 572         -- "check" checks each sig tyvar in turn
 573         foldlNF_Tc check
 574                    (env2, in_scope_env, [])
 575                    (tidy_tvs `zip` tidy_tys)    `thenNF_Tc` \ (env3, _, msgs) ->
 576
 577         failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
 578       where
 579         (env1, tidy_tvs) = mapAccumL tidyTyVar emptyTidyEnv sig_tyvars
 580         (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
 581
 582         main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
 583
 584         check (env, acc, msgs) (sig_tyvar,ty)
 585                 -- sig_tyvar is from the signature;
 586                 -- ty is what you get if you zonk sig_tyvar and then tidy it
 587                 --
 588                 -- acc maps a zonked type variable back to a signature type variable
 589           = case getTyVar_maybe ty of {
 590               Nothing ->                        -- Error (a)!
 591                         returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr ty) : msgs) ;
 592
 593               Just tv ->
 594
 595             case lookupVarEnv acc tv of {
 596                 Just sig_tyvar' ->      -- Error (b) or (d)!
 597                         returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr sig_tyvar') : msgs) ;
 598
 599                 Nothing ->
 600
 601             if tv `elemVarSet` globals  -- Error (c)! Type variable escapes
 602                                         -- The least comprehensible, so put it last
 603             then   tcGetValueEnv                        `thenNF_Tc` \ ve ->
 604                    find_globals tv env (valueEnvIds ve) `thenNF_Tc` \ (env1, globs) ->
 605                    returnNF_Tc (env1, acc, escape_msg sig_tyvar tv globs : msgs)
 606
 607             else        -- All OK
 608             returnNF_Tc (env, extendVarEnv acc tv sig_tyvar, msgs)
 609             }}
 610
 611 -- find_globals looks at the value environment and finds values
 612 -- whose types mention the offending type variable.  It has to be
 613 -- careful to zonk the Id's type first, so it has to be in the monad.
 614 -- We must be careful to pass it a zonked type variable, too.
 615 find_globals tv tidy_env ids
 616   | null ids
 617   = returnNF_Tc (tidy_env, [])
 618
 619 find_globals tv tidy_env (id:ids)
 620   | not (isLocallyDefined id) ||
 621     isEmptyVarSet (idFreeTyVars id)
 622   = find_globals tv tidy_env ids
 623
 624   | otherwise
 625   = zonkTcType (idType id)      `thenNF_Tc` \ id_ty ->
 626     if tv `elemVarSet` tyVarsOfType id_ty then
 627         let
 628            (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
 629         in
 630         find_globals tv tidy_env' ids   `thenNF_Tc` \ (tidy_env'', globs) ->
 631         returnNF_Tc (tidy_env'', (idName id, id_ty') : globs)
 632     else
 633         find_globals tv tidy_env ids
 634
 635 escape_msg sig_tv tv globs
 636   = vcat [mk_msg sig_tv <+> ptext SLIT("escapes"),
 637           pp_escape,
 638           ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
 639           nest 4 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
 640     ]
 641   where
 642     pp_escape | sig_tv /= tv = ptext SLIT("It unifies with") <+>
 643                                quotes (ppr tv) <> comma <+>
 644                                ptext SLIT("which is mentioned in the environment")
 645               | otherwise    = ptext SLIT("It is mentioned in the environment")
 646
 647     vcat_first :: Int -> [SDoc] -> SDoc
 648     vcat_first n []     = empty
 649     vcat_first 0 (x:xs) = text "...others omitted..."
 650     vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
 651
 652 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> quotes thing
 653 mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
 654 \end{code}
 655
 656 These two context are used with checkSigTyVars
 657
 658 \begin{code}
 659 sigCtxt :: (Type -> Message) -> Type
 660         -> TidyEnv -> NF_TcM s (TidyEnv, Message)
 661 sigCtxt mk_msg sig_ty tidy_env
 662   = let
 663         (env1, tidy_sig_ty) = tidyOpenType tidy_env sig_ty
 664     in
 665     returnNF_Tc (env1, mk_msg tidy_sig_ty)
 666
 667 sigPatCtxt bound_tvs bound_ids tidy_env
 668   = returnNF_Tc (env1,
 669                  sep [ptext SLIT("When checking a pattern that binds"),
 670                       nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
 671   where
 672     show_ids = filter is_interesting bound_ids
 673     is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
 674
 675     (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
 676     ppr_id id ty     = ppr id <+> dcolon <+> ppr ty
 677         -- Don't zonk the types so we get the separate, un-unified versions
 678 \end{code}
 679
 680
 681 %************************************************************************
 682 %*                                                                      *
 683 \subsection{Errors and contexts}
 684 %*                                                                      *
 685 %************************************************************************
 686
 687 \begin{code}
 688 naughtyCCallContextErr clas_name
 689   = sep [ptext SLIT("Can't use class") <+> quotes (ppr clas_name),
 690          ptext SLIT("in a context")]
 691
 692 typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
 693
 694 typeKindCtxt :: RenamedHsType -> Message
 695 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
 696                        nest 2 (quotes (ppr ty)),
 697                        ptext SLIT("is a type")]
 698
 699 appKindCtxt :: SDoc -> Message
 700 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
 701
 702 classAsTyConErr name
 703   = ptext SLIT("Class used as a type constructor:") <+> ppr name
 704
 705 tyConAsClassErr name
 706   = ptext SLIT("Type constructor used as a class:") <+> ppr name
 707
 708 tyVarAsClassErr name
 709   = ptext SLIT("Type variable used as a class:") <+> ppr name
 710
 711 ambigErr (c, ts) ty
 712   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprConstraint c ts),
 713          nest 4 (ptext SLIT("for the type:") <+> ppr ty),
 714          nest 4 (ptext SLIT("Each forall'd type variable mentioned by the constraint must appear after the =>."))]
 715 \end{code}