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