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