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