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 ( tcHsSigType, tcHsType, tcIfaceType, tcHsTheta,
   8                     UserTypeCtxt(..),
   9
  10                         -- Kind checking
  11                     kcHsTyVar, kcHsTyVars, mkTyClTyVars,
  12                     kcHsType, kcHsSigType, kcHsSigTypes,
  13                     kcHsLiftedSigType, kcHsContext,
  14                     tcAddScopedTyVars, tcHsTyVars, mkImmutTyVars,
  15
  16                     TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
  17                     checkSigTyVars, sigCtxt, sigPatCtxt
  18                   ) where
  19
  20 #include "HsVersions.h"
  21
  22 import HsSyn            ( HsType(..), HsTyVarBndr(..),
  23                           Sig(..), HsPred(..), pprParendHsType, HsTupCon(..), hsTyVarNames )
  24 import RnHsSyn          ( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig, extractHsTyVars )
  25 import TcHsSyn          ( TcId )
  26
  27 import TcMonad
  28 import TcEnv            ( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
  29                           tcGetGlobalTyVars, tcLEnvElts, tcInLocalScope,
  30                           TyThing(..), TcTyThing(..), tcExtendKindEnv
  31                         )
  32 import TcMType          ( newKindVar, tcInstSigTyVars,
  33                           zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar,
  34                           unifyKind, unifyOpenTypeKind,
  35                           checkValidType, UserTypeCtxt(..), pprUserTypeCtxt
  36                         )
  37 import TcType           ( Type, Kind, SourceType(..), ThetaType, TyVarDetails(..),
  38                           TcTyVar, TcTyVarSet, TcType, TcKind, TcThetaType, TcTauType,
  39                           mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy,
  40                           tcSplitForAllTys, tcSplitRhoTy,
  41                           hoistForAllTys, allDistinctTyVars, zipFunTys,
  42                           mkSigmaTy, mkPredTy, mkTyConApp, mkAppTys, mkRhoTy,
  43                           liftedTypeKind, unliftedTypeKind, mkArrowKind,
  44                           mkArrowKinds, tcGetTyVar_maybe, tcGetTyVar, tcSplitFunTy_maybe,
  45                           tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
  46                           tyVarsOfType, mkForAllTys
  47                         )
  48 import qualified Type   ( getTyVar_maybe )
  49
  50 import Inst             ( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
  51 import PprType          ( pprType )
  52 import Subst            ( mkTopTyVarSubst, substTy )
  53 import CoreFVs          ( idFreeTyVars )
  54 import Id               ( mkLocalId, idName, idType )
  55 import Var              ( Id, Var, TyVar, mkTyVar, tyVarKind, isMutTyVar, mutTyVarDetails )
  56 import VarEnv
  57 import VarSet
  58 import ErrUtils         ( Message )
  59 import TyCon            ( TyCon, isSynTyCon, tyConArity, tyConKind )
  60 import Class            ( classTyCon )
  61 import Name             ( Name, getSrcLoc )
  62 import NameSet
  63 import TysWiredIn       ( mkListTy, mkTupleTy, genUnitTyCon )
  64 import BasicTypes       ( Boxity(..) )
  65 import SrcLoc           ( SrcLoc )
  66 import Util             ( isSingleton, lengthIs )
  67 import Outputable
  68
  69 \end{code}
  70
  71
  72 %************************************************************************
  73 %*                                                                      *
  74 \subsection{Checking types}
  75 %*                                                                      *
  76 %************************************************************************
  77
  78 Generally speaking we now type-check types in three phases
  79
  80         1.  Kind check the HsType [kcHsType]
  81         2.  Convert from HsType to Type, and hoist the foralls [tcHsType]
  82         3.  Check the validity of the resulting type [checkValidType]
  83
  84 Often these steps are done one after the othe (tcHsSigType).
  85 But in mutually recursive groups of type and class decls we do
  86         1 kind-check the whole group
  87         2 build TyCons/Classes in a knot-tied wa
  88         3 check the validity of types in the now-unknotted TyCons/Classes
  89
  90 \begin{code}
  91 tcHsSigType :: UserTypeCtxt -> RenamedHsType -> TcM Type
  92   -- Do kind checking, and hoist for-alls to the top
  93 tcHsSigType ctxt ty = tcAddErrCtxt (checkTypeCtxt ctxt ty) (
  94                         kcTypeType ty           `thenTc_`
  95                         tcHsType ty
  96                       )                         `thenTc` \ ty' ->
  97                       checkValidType ctxt ty'   `thenTc_`
  98                       returnTc ty'
  99
 100 checkTypeCtxt ctxt ty
 101   = vcat [ptext SLIT("In the type:") <+> ppr ty,
 102           ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
 103
 104 tcHsType    :: RenamedHsType -> TcM Type
 105   -- Don't do kind checking, nor validity checking,
 106   --    but do hoist for-alls to the top
 107   -- This is used in type and class decls, where kinding is
 108   -- done in advance, and validity checking is done later
 109   -- [Validity checking done later because of knot-tying issues.]
 110 tcHsType ty = tc_type ty  `thenTc` \ ty' ->
 111               returnTc (hoistForAllTys ty')
 112
 113 tcHsTheta :: RenamedContext -> TcM ThetaType
 114 -- Used when we are expecting a ClassContext (i.e. no implicit params)
 115 -- Does not do validity checking, like tcHsType
 116 tcHsTheta hs_theta = mapTc tc_pred hs_theta
 117
 118 -- In interface files the type is already kinded,
 119 -- and we definitely don't want to hoist for-alls.
 120 -- Otherwise we'll change
 121 --      dmfail :: forall m:(*->*) Monad m => forall a:* => String -> m a
 122 -- into
 123 --      dmfail :: forall m:(*->*) a:* Monad m => String -> m a
 124 -- which definitely isn't right!
 125 tcIfaceType ty = tc_type ty
 126 \end{code}
 127
 128
 129 %************************************************************************
 130 %*                                                                      *
 131 \subsection{Kind checking}
 132 %*                                                                      *
 133 %************************************************************************
 134
 135 Kind checking
 136 ~~~~~~~~~~~~~
 137 When we come across the binding site for some type variables, we
 138 proceed in two stages
 139
 140 1. Figure out what kind each tyvar has
 141
 142 2. Create suitably-kinded tyvars,
 143    extend the envt,
 144    and typecheck the body
 145
 146 To do step 1, we proceed thus:
 147
 148 1a. Bind each type variable to a kind variable
 149 1b. Apply the kind checker
 150 1c. Zonk the resulting kinds
 151
 152 The kind checker is passed to tcHsTyVars as an argument.
 153
 154 For example, when we find
 155         (forall a m. m a -> m a)
 156 we bind a,m to kind varibles and kind-check (m a -> m a).  This
 157 makes a get kind *, and m get kind *->*.  Now we typecheck (m a -> m a)
 158 in an environment that binds a and m suitably.
 159
 160 The kind checker passed to tcHsTyVars needs to look at enough to
 161 establish the kind of the tyvar:
 162   * For a group of type and class decls, it's just the group, not
 163         the rest of the program
 164   * For a tyvar bound in a pattern type signature, its the types
 165         mentioned in the other type signatures in that bunch of patterns
 166   * For a tyvar bound in a RULE, it's the type signatures on other
 167         universally quantified variables in the rule
 168
 169 Note that this may occasionally give surprising results.  For example:
 170
 171         data T a b = MkT (a b)
 172
 173 Here we deduce                  a::*->*, b::*.
 174 But equally valid would be
 175                                 a::(*->*)-> *, b::*->*
 176
 177 \begin{code}
 178 -- tcHsTyVars is used for type variables in type signatures
 179 --      e.g. forall a. a->a
 180 -- They are immutable, because they scope only over the signature
 181 -- They may or may not be explicitly-kinded
 182 tcHsTyVars :: [HsTyVarBndr Name]
 183            -> TcM a                             -- The kind checker
 184            -> ([TyVar] -> TcM b)
 185            -> TcM b
 186
 187 tcHsTyVars [] kind_check thing_inside = thing_inside []
 188         -- A useful short cut for a common case!
 189
 190 tcHsTyVars tv_names kind_check thing_inside
 191   = kcHsTyVars tv_names                                 `thenNF_Tc` \ tv_names_w_kinds ->
 192     tcExtendKindEnv tv_names_w_kinds kind_check         `thenTc_`
 193     zonkKindEnv tv_names_w_kinds                        `thenNF_Tc` \ tvs_w_kinds ->
 194     let
 195         tyvars = mkImmutTyVars tvs_w_kinds
 196     in
 197     tcExtendTyVarEnv tyvars (thing_inside tyvars)
 198
 199
 200
 201 tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
 202 -- tcAddScopedTyVars is used for scoped type variables
 203 -- added by pattern type signatures
 204 --      e.g.  \ (x::a) (y::a) -> x+y
 205 -- They never have explicit kinds (because this is source-code only)
 206 -- They are mutable (because they can get bound to a more specific type)
 207
 208 -- Find the not-already-in-scope signature type variables,
 209 -- kind-check them, and bring them into scope
 210 --
 211 -- We no longer specify that these type variables must be univerally
 212 -- quantified (lots of email on the subject).  If you want to put that
 213 -- back in, you need to
 214 --      a) Do a checkSigTyVars after thing_inside
 215 --      b) More insidiously, don't pass in expected_ty, else
 216 --         we unify with it too early and checkSigTyVars barfs
 217 --         Instead you have to pass in a fresh ty var, and unify
 218 --         it with expected_ty afterwards
 219 tcAddScopedTyVars [] thing_inside
 220   = thing_inside        -- Quick get-out for the empty case
 221
 222 tcAddScopedTyVars sig_tys thing_inside
 223   = tcGetEnv                                    `thenNF_Tc` \ env ->
 224     let
 225         all_sig_tvs     = foldr (unionNameSets . extractHsTyVars) emptyNameSet sig_tys
 226         sig_tvs         = filter not_in_scope (nameSetToList all_sig_tvs)
 227         not_in_scope tv = not (tcInLocalScope env tv)
 228     in
 229     mapNF_Tc newNamedKindVar sig_tvs                    `thenTc` \ kind_env ->
 230     tcExtendKindEnv kind_env (kcHsSigTypes sig_tys)     `thenTc_`
 231     zonkKindEnv kind_env                                `thenNF_Tc` \ tvs_w_kinds ->
 232     listTc [ tcNewMutTyVar name kind PatSigTv
 233            | (name, kind) <- tvs_w_kinds]               `thenNF_Tc` \ tyvars ->
 234     tcExtendTyVarEnv tyvars thing_inside
 235 \end{code}
 236
 237
 238 \begin{code}
 239 kcHsTyVar  :: HsTyVarBndr name   -> NF_TcM (name, TcKind)
 240 kcHsTyVars :: [HsTyVarBndr name] -> NF_TcM [(name, TcKind)]
 241
 242 kcHsTyVar (UserTyVar name)       = newNamedKindVar name
 243 kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (name, kind)
 244
 245 kcHsTyVars tvs = mapNF_Tc kcHsTyVar tvs
 246
 247 newNamedKindVar name = newKindVar       `thenNF_Tc` \ kind ->
 248                        returnNF_Tc (name, kind)
 249
 250 ---------------------------
 251 kcLiftedType :: RenamedHsType -> TcM ()
 252         -- The type ty must be a *lifted* *type*
 253 kcLiftedType ty
 254   = kcHsType ty                         `thenTc` \ kind ->
 255     tcAddErrCtxt (typeKindCtxt ty)      $
 256     unifyKind liftedTypeKind kind
 257
 258 ---------------------------
 259 kcTypeType :: RenamedHsType -> TcM ()
 260         -- The type ty must be a *type*, but it can be lifted or unlifted.
 261 kcTypeType ty
 262   = kcHsType ty                         `thenTc` \ kind ->
 263     tcAddErrCtxt (typeKindCtxt ty)      $
 264     unifyOpenTypeKind kind
 265
 266 ---------------------------
 267 kcHsSigType, kcHsLiftedSigType :: RenamedHsType -> TcM ()
 268         -- Used for type signatures
 269 kcHsSigType       = kcTypeType
 270 kcHsSigTypes tys  = mapTc_ kcHsSigType tys
 271 kcHsLiftedSigType = kcLiftedType
 272
 273 ---------------------------
 274 kcHsType :: RenamedHsType -> TcM TcKind
 275 kcHsType (HsTyVar name)       = kcTyVar name
 276
 277 kcHsType (HsListTy ty)
 278   = kcLiftedType ty             `thenTc` \ tau_ty ->
 279     returnTc liftedTypeKind
 280
 281 kcHsType (HsTupleTy (HsTupCon _ boxity _) tys)
 282   = mapTc kcTypeType tys        `thenTc_`
 283     returnTc (case boxity of
 284                   Boxed   -> liftedTypeKind
 285                   Unboxed -> unliftedTypeKind)
 286
 287 kcHsType (HsFunTy ty1 ty2)
 288   = kcTypeType ty1      `thenTc_`
 289     kcTypeType ty2      `thenTc_`
 290     returnTc liftedTypeKind
 291
 292 kcHsType (HsNumTy _)            -- The unit type for generics
 293   = returnTc liftedTypeKind
 294
 295 kcHsType ty@(HsOpTy ty1 op ty2)
 296   = kcTyVar op                          `thenTc` \ op_kind ->
 297     kcHsType ty1                        `thenTc` \ ty1_kind ->
 298     kcHsType ty2                        `thenTc` \ ty2_kind ->
 299     tcAddErrCtxt (appKindCtxt (ppr ty)) $
 300     kcAppKind op_kind  ty1_kind         `thenTc` \ op_kind' ->
 301     kcAppKind op_kind' ty2_kind
 302
 303 kcHsType (HsPredTy pred)
 304   = kcHsPred pred               `thenTc_`
 305     returnTc liftedTypeKind
 306
 307 kcHsType ty@(HsAppTy ty1 ty2)
 308   = kcHsType ty1                        `thenTc` \ tc_kind ->
 309     kcHsType ty2                        `thenTc` \ arg_kind ->
 310     tcAddErrCtxt (appKindCtxt (ppr ty)) $
 311     kcAppKind tc_kind arg_kind
 312
 313 kcHsType (HsForAllTy (Just tv_names) context ty)
 314   = kcHsTyVars tv_names         `thenNF_Tc` \ kind_env ->
 315     tcExtendKindEnv kind_env    $
 316     kcHsContext context         `thenTc_`
 317     kcHsType ty                 `thenTc_`
 318     returnTc liftedTypeKind
 319
 320 ---------------------------
 321 kcAppKind fun_kind arg_kind
 322   = case tcSplitFunTy_maybe fun_kind of
 323         Just (arg_kind', res_kind)
 324                 -> unifyKind arg_kind arg_kind' `thenTc_`
 325                    returnTc res_kind
 326
 327         Nothing -> newKindVar                                           `thenNF_Tc` \ res_kind ->
 328                    unifyKind fun_kind (mkArrowKind arg_kind res_kind)   `thenTc_`
 329                    returnTc res_kind
 330
 331
 332 ---------------------------
 333 kcHsContext ctxt = mapTc_ kcHsPred ctxt
 334
 335 kcHsPred :: RenamedHsPred -> TcM ()
 336 kcHsPred pred@(HsIParam name ty)
 337   = tcAddErrCtxt (appKindCtxt (ppr pred))       $
 338     kcLiftedType ty
 339
 340 kcHsPred pred@(HsClassP cls tys)
 341   = tcAddErrCtxt (appKindCtxt (ppr pred))       $
 342     kcClass cls                                 `thenTc` \ kind ->
 343     mapTc kcHsType tys                          `thenTc` \ arg_kinds ->
 344     unifyKind kind (mkArrowKinds arg_kinds liftedTypeKind)
 345
 346  ---------------------------
 347 kcTyVar name    -- Could be a tyvar or a tycon
 348   = tcLookup name       `thenTc` \ thing ->
 349     case thing of
 350         AThing kind         -> returnTc kind
 351         ATyVar tv           -> returnTc (tyVarKind tv)
 352         AGlobal (ATyCon tc) -> returnTc (tyConKind tc)
 353         other               -> failWithTc (wrongThingErr "type" thing name)
 354
 355 kcClass cls     -- Must be a class
 356   = tcLookup cls                                `thenNF_Tc` \ thing ->
 357     case thing of
 358         AThing kind           -> returnTc kind
 359         AGlobal (AClass cls)  -> returnTc (tyConKind (classTyCon cls))
 360         other                 -> failWithTc (wrongThingErr "class" thing cls)
 361 \end{code}
 362
 363 %************************************************************************
 364 %*                                                                      *
 365 \subsection{tc_type}
 366 %*                                                                      *
 367 %************************************************************************
 368
 369 tc_type, the main work horse
 370 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 371
 372         -------------------
 373         *** BIG WARNING ***
 374         -------------------
 375
 376 tc_type is used to typecheck the types in the RHS of data
 377 constructors.  In the case of recursive data types, that means that
 378 the type constructors themselves are (partly) black holes.  e.g.
 379
 380         data T a = MkT a [T a]
 381
 382 While typechecking the [T a] on the RHS, T itself is not yet fully
 383 defined.  That in turn places restrictions on what you can check in
 384 tcHsType; if you poke on too much you get a black hole.  I keep
 385 forgetting this, hence this warning!
 386
 387 So tc_type does no validity-checking.  Instead that's all done
 388 by TcMType.checkValidType
 389
 390         --------------------------
 391         *** END OF BIG WARNING ***
 392         --------------------------
 393
 394
 395 \begin{code}
 396 tc_type :: RenamedHsType -> TcM Type
 397
 398 tc_type ty@(HsTyVar name)
 399   = tc_app ty []
 400
 401 tc_type (HsListTy ty)
 402   = tc_type ty  `thenTc` \ tau_ty ->
 403     returnTc (mkListTy tau_ty)
 404
 405 tc_type (HsTupleTy (HsTupCon _ boxity arity) tys)
 406   = ASSERT( tys `lengthIs` arity )
 407     tc_types tys        `thenTc` \ tau_tys ->
 408     returnTc (mkTupleTy boxity arity tau_tys)
 409
 410 tc_type (HsFunTy ty1 ty2)
 411   = tc_type ty1                 `thenTc` \ tau_ty1 ->
 412     tc_type ty2                 `thenTc` \ tau_ty2 ->
 413     returnTc (mkFunTy tau_ty1 tau_ty2)
 414
 415 tc_type (HsNumTy n)
 416   = ASSERT(n== 1)
 417     returnTc (mkTyConApp genUnitTyCon [])
 418
 419 tc_type (HsOpTy ty1 op ty2)
 420   = tc_type ty1 `thenTc` \ tau_ty1 ->
 421     tc_type ty2 `thenTc` \ tau_ty2 ->
 422     tc_fun_type op [tau_ty1,tau_ty2]
 423
 424 tc_type (HsAppTy ty1 ty2) = tc_app ty1 [ty2]
 425
 426 tc_type (HsPredTy pred)
 427   = tc_pred pred        `thenTc` \ pred' ->
 428     returnTc (mkPredTy pred')
 429
 430 tc_type full_ty@(HsForAllTy (Just tv_names) ctxt ty)
 431   = let
 432         kind_check = kcHsContext ctxt `thenTc_` kcHsType ty
 433     in
 434     tcHsTyVars tv_names kind_check      $ \ tyvars ->
 435     mapTc tc_pred ctxt                  `thenTc` \ theta ->
 436     tc_type ty                          `thenTc` \ tau ->
 437     returnTc (mkSigmaTy tyvars theta tau)
 438
 439 tc_types arg_tys = mapTc tc_type arg_tys
 440 \end{code}
 441
 442 Help functions for type applications
 443 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 444
 445 \begin{code}
 446 tc_app :: RenamedHsType -> [RenamedHsType] -> TcM Type
 447 tc_app (HsAppTy ty1 ty2) tys
 448   = tc_app ty1 (ty2:tys)
 449
 450 tc_app ty tys
 451   = tcAddErrCtxt (appKindCtxt pp_app)   $
 452     tc_types tys                        `thenTc` \ arg_tys ->
 453     case ty of
 454         HsTyVar fun -> tc_fun_type fun arg_tys
 455         other       -> tc_type ty               `thenTc` \ fun_ty ->
 456                        returnNF_Tc (mkAppTys fun_ty arg_tys)
 457   where
 458     pp_app = ppr ty <+> sep (map pprParendHsType tys)
 459
 460 -- (tc_fun_type ty arg_tys) returns (mkAppTys ty arg_tys)
 461 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
 462 --      hence the rather strange functionality.
 463
 464 tc_fun_type name arg_tys
 465   = tcLookup name                       `thenTc` \ thing ->
 466     case thing of
 467         ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)
 468
 469         AGlobal (ATyCon tc)
 470                 | isSynTyCon tc ->  returnTc (mkSynTy tc arg_tys)
 471                 | otherwise     ->  returnTc (mkTyConApp tc arg_tys)
 472
 473         other -> failWithTc (wrongThingErr "type constructor" thing name)
 474 \end{code}
 475
 476
 477 Contexts
 478 ~~~~~~~~
 479 \begin{code}
 480 tc_pred assn@(HsClassP class_name tys)
 481   = tcAddErrCtxt (appKindCtxt (ppr assn))       $
 482     tc_types tys                        `thenTc` \ arg_tys ->
 483     tcLookupGlobal class_name                   `thenTc` \ thing ->
 484     case thing of
 485         AClass clas -> returnTc (ClassP clas arg_tys)
 486         other       -> failWithTc (wrongThingErr "class" (AGlobal thing) class_name)
 487
 488 tc_pred assn@(HsIParam name ty)
 489   = tcAddErrCtxt (appKindCtxt (ppr assn))       $
 490     tc_type ty                                  `thenTc` \ arg_ty ->
 491     returnTc (IParam name arg_ty)
 492 \end{code}
 493
 494
 495
 496 %************************************************************************
 497 %*                                                                      *
 498 \subsection{Type variables, with knot tying!}
 499 %*                                                                      *
 500 %************************************************************************
 501
 502 \begin{code}
 503 mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
 504 mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
 505
 506 mkTyClTyVars :: Kind                    -- Kind of the tycon or class
 507              -> [HsTyVarBndr Name]
 508              -> [TyVar]
 509 mkTyClTyVars kind tyvar_names
 510   = mkImmutTyVars tyvars_w_kinds
 511   where
 512     (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
 513 \end{code}
 514
 515
 516 %************************************************************************
 517 %*                                                                      *
 518 \subsection{Signatures}
 519 %*                                                                      *
 520 %************************************************************************
 521
 522 @tcSigs@ checks the signatures for validity, and returns a list of
 523 {\em freshly-instantiated} signatures.  That is, the types are already
 524 split up, and have fresh type variables installed.  All non-type-signature
 525 "RenamedSigs" are ignored.
 526
 527 The @TcSigInfo@ contains @TcTypes@ because they are unified with
 528 the variable's type, and after that checked to see whether they've
 529 been instantiated.
 530
 531 \begin{code}
 532 data TcSigInfo
 533   = TySigInfo
 534         Name                    -- N, the Name in corresponding binding
 535
 536         TcId                    -- *Polymorphic* binder for this value...
 537                                 -- Has name = N
 538
 539         [TcTyVar]               -- tyvars
 540         TcThetaType             -- theta
 541         TcTauType               -- tau
 542
 543         TcId                    -- *Monomorphic* binder for this value
 544                                 -- Does *not* have name = N
 545                                 -- Has type tau
 546
 547         [Inst]                  -- Empty if theta is null, or
 548                                 -- (method mono_id) otherwise
 549
 550         SrcLoc                  -- Of the signature
 551
 552 instance Outputable TcSigInfo where
 553     ppr (TySigInfo nm id tyvars theta tau _ inst loc) =
 554         ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
 555
 556 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
 557         -- Search for a particular signature
 558 maybeSig [] name = Nothing
 559 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
 560   | name == sig_name = Just sig
 561   | otherwise        = maybeSig sigs name
 562 \end{code}
 563
 564
 565 \begin{code}
 566 tcTySig :: RenamedSig -> TcM TcSigInfo
 567
 568 tcTySig (Sig v ty src_loc)
 569  = tcAddSrcLoc src_loc                          $
 570    tcHsSigType (FunSigCtxt v) ty                `thenTc` \ sigma_tc_ty ->
 571    mkTcSig (mkLocalId v sigma_tc_ty) src_loc    `thenNF_Tc` \ sig ->
 572    returnTc sig
 573
 574 mkTcSig :: TcId -> SrcLoc -> NF_TcM TcSigInfo
 575 mkTcSig poly_id src_loc
 576   =     -- Instantiate this type
 577         -- It's important to do this even though in the error-free case
 578         -- we could just split the sigma_tc_ty (since the tyvars don't
 579         -- unified with anything).  But in the case of an error, when
 580         -- the tyvars *do* get unified with something, we want to carry on
 581         -- typechecking the rest of the program with the function bound
 582         -- to a pristine type, namely sigma_tc_ty
 583    let
 584         (tyvars, rho) = tcSplitForAllTys (idType poly_id)
 585    in
 586    tcInstSigTyVars SigTv tyvars                 `thenNF_Tc` \ tyvars' ->
 587         -- Make *signature* type variables
 588
 589    let
 590      tyvar_tys' = mkTyVarTys tyvars'
 591      rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
 592         -- mkTopTyVarSubst because the tyvars' are fresh
 593
 594      (theta', tau') = tcSplitRhoTy rho'
 595         -- This splitRhoTy tries hard to make sure that tau' is a type synonym
 596         -- wherever possible, which can improve interface files.
 597    in
 598    newMethodWithGivenTy SignatureOrigin
 599                 poly_id
 600                 tyvar_tys'
 601                 theta' tau'                     `thenNF_Tc` \ inst ->
 602         -- We make a Method even if it's not overloaded; no harm
 603
 604    returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToId inst) [inst] src_loc)
 605   where
 606     name = idName poly_id
 607 \end{code}
 608
 609
 610
 611 %************************************************************************
 612 %*                                                                      *
 613 \subsection{Checking signature type variables}
 614 %*                                                                      *
 615 %************************************************************************
 616
 617 @checkSigTyVars@ is used after the type in a type signature has been unified with
 618 the actual type found.  It then checks that the type variables of the type signature
 619 are
 620         (a) Still all type variables
 621                 eg matching signature [a] against inferred type [(p,q)]
 622                 [then a will be unified to a non-type variable]
 623
 624         (b) Still all distinct
 625                 eg matching signature [(a,b)] against inferred type [(p,p)]
 626                 [then a and b will be unified together]
 627
 628         (c) Not mentioned in the environment
 629                 eg the signature for f in this:
 630
 631                         g x = ... where
 632                                         f :: a->[a]
 633                                         f y = [x,y]
 634
 635                 Here, f is forced to be monorphic by the free occurence of x.
 636
 637         (d) Not (unified with another type variable that is) in scope.
 638                 eg f x :: (r->r) = (\y->y) :: forall a. a->r
 639             when checking the expression type signature, we find that
 640             even though there is nothing in scope whose type mentions r,
 641             nevertheless the type signature for the expression isn't right.
 642
 643             Another example is in a class or instance declaration:
 644                 class C a where
 645                    op :: forall b. a -> b
 646                    op x = x
 647             Here, b gets unified with a
 648
 649 Before doing this, the substitution is applied to the signature type variable.
 650
 651 We used to have the notion of a "DontBind" type variable, which would
 652 only be bound to itself or nothing.  Then points (a) and (b) were
 653 self-checking.  But it gave rise to bogus consequential error messages.
 654 For example:
 655
 656    f = (*)      -- Monomorphic
 657
 658    g :: Num a => a -> a
 659    g x = f x x
 660
 661 Here, we get a complaint when checking the type signature for g,
 662 that g isn't polymorphic enough; but then we get another one when
 663 dealing with the (Num x) context arising from f's definition;
 664 we try to unify x with Int (to default it), but find that x has already
 665 been unified with the DontBind variable "a" from g's signature.
 666 This is really a problem with side-effecting unification; we'd like to
 667 undo g's effects when its type signature fails, but unification is done
 668 by side effect, so we can't (easily).
 669
 670 So we revert to ordinary type variables for signatures, and try to
 671 give a helpful message in checkSigTyVars.
 672
 673 \begin{code}
 674 checkSigTyVars :: [TcTyVar]             -- Universally-quantified type variables in the signature
 675                -> TcTyVarSet            -- Tyvars that are free in the type signature
 676                                         --      Not necessarily zonked
 677                                         --      These should *already* be in the free-in-env set,
 678                                         --      and are used here only to improve the error message
 679                -> TcM [TcTyVar]         -- Zonked signature type variables
 680
 681 checkSigTyVars [] free = returnTc []
 682 checkSigTyVars sig_tyvars free_tyvars
 683   = zonkTcTyVars sig_tyvars             `thenNF_Tc` \ sig_tys ->
 684     tcGetGlobalTyVars                   `thenNF_Tc` \ globals ->
 685
 686     checkTcM (allDistinctTyVars sig_tys globals)
 687              (complain sig_tys globals) `thenTc_`
 688
 689     returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
 690
 691   where
 692     complain sig_tys globals
 693       = -- "check" checks each sig tyvar in turn
 694         foldlNF_Tc check
 695                    (env2, emptyVarEnv, [])
 696                    (tidy_tvs `zip` tidy_tys)    `thenNF_Tc` \ (env3, _, msgs) ->
 697
 698         failWithTcM (env3, main_msg $$ vcat msgs)
 699       where
 700         (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tyvars
 701         (env2, tidy_tys) = tidyOpenTypes  env1         sig_tys
 702
 703         main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
 704
 705         check (tidy_env, acc, msgs) (sig_tyvar,ty)
 706                 -- sig_tyvar is from the signature;
 707                 -- ty is what you get if you zonk sig_tyvar and then tidy it
 708                 --
 709                 -- acc maps a zonked type variable back to a signature type variable
 710           = case tcGetTyVar_maybe ty of {
 711               Nothing ->                        -- Error (a)!
 712                         returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
 713
 714               Just tv ->
 715
 716             case lookupVarEnv acc tv of {
 717                 Just sig_tyvar' ->      -- Error (b)!
 718                         returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
 719                     where
 720                         thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
 721
 722               ; Nothing ->
 723
 724             if tv `elemVarSet` globals  -- Error (c) or (d)! Type variable escapes
 725                                         -- The least comprehensible, so put it last
 726                         -- Game plan:
 727                         --    a) get the local TcIds and TyVars from the environment,
 728                         --       and pass them to find_globals (they might have tv free)
 729                         --    b) similarly, find any free_tyvars that mention tv
 730             then   tcGetEnv                                                     `thenNF_Tc` \ ve ->
 731                    find_globals tv tidy_env  (tcLEnvElts ve)                    `thenNF_Tc` \ (tidy_env1, globs) ->
 732                    find_frees   tv tidy_env1 [] (varSetElems free_tyvars)       `thenNF_Tc` \ (tidy_env2, frees) ->
 733                    returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
 734
 735             else        -- All OK
 736             returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
 737             }}
 738
 739 -----------------------
 740 -- find_globals looks at the value environment and finds values
 741 -- whose types mention the offending type variable.  It has to be
 742 -- careful to zonk the Id's type first, so it has to be in the monad.
 743 -- We must be careful to pass it a zonked type variable, too.
 744
 745 find_globals :: Var
 746              -> TidyEnv
 747              -> [TcTyThing]
 748              -> NF_TcM (TidyEnv, [SDoc])
 749
 750 find_globals tv tidy_env things
 751   = go tidy_env [] things
 752   where
 753     go tidy_env acc [] = returnNF_Tc (tidy_env, acc)
 754     go tidy_env acc (thing : things)
 755       = find_thing ignore_it tidy_env thing     `thenNF_Tc` \ (tidy_env1, maybe_doc) ->
 756         case maybe_doc of
 757           Just d  -> go tidy_env1 (d:acc) things
 758           Nothing -> go tidy_env1 acc     things
 759
 760     ignore_it ty = not (tv `elemVarSet` tyVarsOfType ty)
 761
 762 -----------------------
 763 find_thing ignore_it tidy_env (ATcId id)
 764   = zonkTcType  (idType id)     `thenNF_Tc` \ id_ty ->
 765     if ignore_it id_ty then
 766         returnNF_Tc (tidy_env, Nothing)
 767     else let
 768         (tidy_env', tidy_ty) = tidyOpenType tidy_env id_ty
 769         msg = sep [ppr id <+> dcolon <+> ppr tidy_ty,
 770                    nest 2 (parens (ptext SLIT("bound at") <+>
 771                                    ppr (getSrcLoc id)))]
 772     in
 773     returnNF_Tc (tidy_env', Just msg)
 774
 775 find_thing ignore_it tidy_env (ATyVar tv)
 776   = zonkTcTyVar tv              `thenNF_Tc` \ tv_ty ->
 777     if ignore_it tv_ty then
 778         returnNF_Tc (tidy_env, Nothing)
 779     else let
 780         (tidy_env1, tv1)     = tidyOpenTyVar tidy_env  tv
 781         (tidy_env2, tidy_ty) = tidyOpenType  tidy_env1 tv_ty
 782         msg = sep [ptext SLIT("Type variable") <+> quotes (ppr tv1) <+> eq_stuff, nest 2 bound_at]
 783
 784         eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty
 785                  | otherwise                                        = equals <+> ppr tv_ty
 786                 -- It's ok to use Type.getTyVar_maybe because ty is zonked by now
 787
 788         bound_at | isMutTyVar tv = mut_info     -- The expected case
 789                  | otherwise     = empty
 790
 791         mut_info = sep [ptext SLIT("is bound by the") <+> ppr (mutTyVarDetails tv),
 792                         ptext SLIT("at") <+> ppr (getSrcLoc tv)]
 793     in
 794     returnNF_Tc (tidy_env2, Just msg)
 795
 796 -----------------------
 797 find_frees tv tidy_env acc []
 798   = returnNF_Tc (tidy_env, acc)
 799 find_frees tv tidy_env acc (ftv:ftvs)
 800   = zonkTcTyVar ftv     `thenNF_Tc` \ ty ->
 801     if tv `elemVarSet` tyVarsOfType ty then
 802         let
 803             (tidy_env', ftv') = tidyOpenTyVar tidy_env ftv
 804         in
 805         find_frees tv tidy_env' (ftv':acc) ftvs
 806     else
 807         find_frees tv tidy_env  acc        ftvs
 808
 809
 810 escape_msg sig_tv tv globs frees
 811   = mk_msg sig_tv <+> ptext SLIT("escapes") $$
 812     if not (null globs) then
 813         vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"),
 814               nest 2 (vcat globs)]
 815      else if not (null frees) then
 816         vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
 817               nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
 818         ]
 819      else
 820         empty   -- Sigh.  It's really hard to give a good error message
 821                 -- all the time.   One bad case is an existential pattern match
 822   where
 823     is_are | isSingleton frees = ptext SLIT("is")
 824            | otherwise         = ptext SLIT("are")
 825     pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
 826           | otherwise    = ptext SLIT("It")
 827
 828     vcat_first :: Int -> [SDoc] -> SDoc
 829     vcat_first n []     = empty
 830     vcat_first 0 (x:xs) = text "...others omitted..."
 831     vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
 832
 833
 834 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
 835 mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
 836 \end{code}
 837
 838 These two context are used with checkSigTyVars
 839
 840 \begin{code}
 841 sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
 842         -> TidyEnv -> NF_TcM (TidyEnv, Message)
 843 sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
 844   = zonkTcType sig_tau          `thenNF_Tc` \ actual_tau ->
 845     let
 846         (env1, tidy_sig_tyvars)  = tidyOpenTyVars tidy_env sig_tyvars
 847         (env2, tidy_sig_rho)     = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
 848         (env3, tidy_actual_tau)  = tidyOpenType env2 actual_tau
 849         msg = vcat [ptext SLIT("Signature type:    ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
 850                     ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
 851                     when
 852                    ]
 853     in
 854     returnNF_Tc (env3, msg)
 855
 856 sigPatCtxt bound_tvs bound_ids tidy_env
 857   = returnNF_Tc (env1,
 858                  sep [ptext SLIT("When checking a pattern that binds"),
 859                       nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
 860   where
 861     show_ids = filter is_interesting bound_ids
 862     is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
 863
 864     (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
 865     ppr_id id ty     = ppr id <+> dcolon <+> ppr ty
 866         -- Don't zonk the types so we get the separate, un-unified versions
 867 \end{code}
 868
 869
 870 %************************************************************************
 871 %*                                                                      *
 872 \subsection{Errors and contexts}
 873 %*                                                                      *
 874 %************************************************************************
 875
 876 \begin{code}
 877 typeKindCtxt :: RenamedHsType -> Message
 878 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
 879                        nest 2 (quotes (ppr ty)),
 880                        ptext SLIT("is a type")]
 881
 882 appKindCtxt :: SDoc -> Message
 883 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
 884
 885 wrongThingErr expected thing name
 886   = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
 887   where
 888     pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
 889     pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
 890     pp_thing (AGlobal (AnId   _)) = ptext SLIT("Identifier")
 891     pp_thing (ATyVar _)           = ptext SLIT("Type variable")
 892     pp_thing (ATcId _)            = ptext SLIT("Local identifier")
 893     pp_thing (AThing _)           = ptext SLIT("Utterly bogus")
 894 \end{code}