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, tcHsPred,
   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, tcSigPolyId, tcSigMonoId
  17                   ) where
  18
  19 #include "HsVersions.h"
  20
  21 import HsSyn            ( HsType(..), HsTyVarBndr(..), HsTyOp(..),
  22                           Sig(..), HsPred(..), pprParendHsType, HsTupCon(..), hsTyVarNames )
  23 import RnHsSyn          ( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig, extractHsTyVars )
  24 import TcHsSyn          ( TcId )
  25
  26 import TcRnMonad
  27 import TcEnv            ( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
  28                           TyThing(..), TcTyThing(..), tcExtendKindEnv,
  29                           getInLocalScope
  30                         )
  31 import TcMType          ( newMutTyVar, newKindVar, zonkKindEnv, tcInstType,
  32                           checkValidType, UserTypeCtxt(..), pprUserTypeCtxt
  33                         )
  34 import TcUnify          ( unifyKind, unifyOpenTypeKind )
  35 import TcType           ( Type, Kind, SourceType(..), ThetaType, TyVarDetails(..),
  36                           TcTyVar, TcKind, TcThetaType, TcTauType,
  37                           mkTyVarTy, mkTyVarTys, mkFunTy,
  38                           zipFunTys, mkForAllTys, mkFunTys, tcEqType, isPredTy,
  39                           mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys,
  40                           liftedTypeKind, unliftedTypeKind, mkArrowKind,
  41                           mkArrowKinds, tcSplitFunTy_maybe, tcSplitForAllTys
  42                         )
  43 import Inst             ( Inst, InstOrigin(..), newMethodWith, instToId )
  44
  45 import Id               ( mkLocalId, idName, idType )
  46 import Var              ( TyVar, mkTyVar, tyVarKind )
  47 import ErrUtils         ( Message )
  48 import TyCon            ( TyCon, tyConKind )
  49 import Class            ( classTyCon )
  50 import Name             ( Name )
  51 import NameSet
  52 import Subst            ( deShadowTy )
  53 import TysWiredIn       ( mkListTy, mkPArrTy, mkTupleTy, genUnitTyCon )
  54 import BasicTypes       ( Boxity(..) )
  55 import SrcLoc           ( SrcLoc )
  56 import Util             ( lengthIs )
  57 import Outputable
  58 import List             ( nubBy )
  59 \end{code}
  60
  61
  62 %************************************************************************
  63 %*                                                                      *
  64 \subsection{Checking types}
  65 %*                                                                      *
  66 %************************************************************************
  67
  68 Generally speaking we now type-check types in three phases
  69
  70         1.  Kind check the HsType [kcHsType]
  71         2.  Convert from HsType to Type, and hoist the foralls [tcHsType]
  72         3.  Check the validity of the resulting type [checkValidType]
  73
  74 Often these steps are done one after the othe (tcHsSigType).
  75 But in mutually recursive groups of type and class decls we do
  76         1 kind-check the whole group
  77         2 build TyCons/Classes in a knot-tied wa
  78         3 check the validity of types in the now-unknotted TyCons/Classes
  79
  80 \begin{code}
  81 tcHsSigType :: UserTypeCtxt -> RenamedHsType -> TcM Type
  82   -- Do kind checking, and hoist for-alls to the top
  83 tcHsSigType ctxt ty = addErrCtxt (checkTypeCtxt ctxt ty) (
  84                         kcTypeType ty           `thenM_`
  85                         tcHsType ty
  86                       )                         `thenM` \ ty' ->
  87                       checkValidType ctxt ty'   `thenM_`
  88                       returnM ty'
  89
  90 checkTypeCtxt ctxt ty
  91   = vcat [ptext SLIT("In the type:") <+> ppr ty,
  92           ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
  93
  94 tcHsType    :: RenamedHsType -> TcM Type
  95   -- Don't do kind checking, nor validity checking,
  96   --    but do hoist for-alls to the top
  97   -- This is used in type and class decls, where kinding is
  98   -- done in advance, and validity checking is done later
  99   -- [Validity checking done later because of knot-tying issues.]
 100 tcHsType ty = tc_type ty  `thenM` \ ty' ->
 101               returnM (hoistForAllTys ty')
 102
 103 tcHsTheta :: RenamedContext -> TcM ThetaType
 104 -- Used when we are expecting a ClassContext (i.e. no implicit params)
 105 -- Does not do validity checking, like tcHsType
 106 tcHsTheta hs_theta = mappM tc_pred hs_theta
 107
 108 -- In interface files the type is already kinded,
 109 -- and we definitely don't want to hoist for-alls.
 110 -- Otherwise we'll change
 111 --      dmfail :: forall m:(*->*) Monad m => forall a:* => String -> m a
 112 -- into
 113 --      dmfail :: forall m:(*->*) a:* Monad m => String -> m a
 114 -- which definitely isn't right!
 115 tcIfaceType ty = tc_type ty
 116 \end{code}
 117
 118
 119 %************************************************************************
 120 %*                                                                      *
 121 \subsection{Kind checking}
 122 %*                                                                      *
 123 %************************************************************************
 124
 125 Kind checking
 126 ~~~~~~~~~~~~~
 127 When we come across the binding site for some type variables, we
 128 proceed in two stages
 129
 130 1. Figure out what kind each tyvar has
 131
 132 2. Create suitably-kinded tyvars,
 133    extend the envt,
 134    and typecheck the body
 135
 136 To do step 1, we proceed thus:
 137
 138 1a. Bind each type variable to a kind variable
 139 1b. Apply the kind checker
 140 1c. Zonk the resulting kinds
 141
 142 The kind checker is passed to tcHsTyVars as an argument.
 143
 144 For example, when we find
 145         (forall a m. m a -> m a)
 146 we bind a,m to kind varibles and kind-check (m a -> m a).  This
 147 makes a get kind *, and m get kind *->*.  Now we typecheck (m a -> m a)
 148 in an environment that binds a and m suitably.
 149
 150 The kind checker passed to tcHsTyVars needs to look at enough to
 151 establish the kind of the tyvar:
 152   * For a group of type and class decls, it's just the group, not
 153         the rest of the program
 154   * For a tyvar bound in a pattern type signature, its the types
 155         mentioned in the other type signatures in that bunch of patterns
 156   * For a tyvar bound in a RULE, it's the type signatures on other
 157         universally quantified variables in the rule
 158
 159 Note that this may occasionally give surprising results.  For example:
 160
 161         data T a b = MkT (a b)
 162
 163 Here we deduce                  a::*->*, b::*.
 164 But equally valid would be
 165                                 a::(*->*)-> *, b::*->*
 166
 167 \begin{code}
 168 -- tcHsTyVars is used for type variables in type signatures
 169 --      e.g. forall a. a->a
 170 -- They are immutable, because they scope only over the signature
 171 -- They may or may not be explicitly-kinded
 172 tcHsTyVars :: [HsTyVarBndr Name]
 173            -> TcM a                             -- The kind checker
 174            -> ([TyVar] -> TcM b)
 175            -> TcM b
 176
 177 tcHsTyVars [] kind_check thing_inside = thing_inside []
 178         -- A useful short cut for a common case!
 179
 180 tcHsTyVars tv_names kind_check thing_inside
 181   = kcHsTyVars tv_names                                 `thenM` \ tv_names_w_kinds ->
 182     tcExtendKindEnv tv_names_w_kinds kind_check         `thenM_`
 183     zonkKindEnv tv_names_w_kinds                        `thenM` \ tvs_w_kinds ->
 184     let
 185         tyvars = mkImmutTyVars tvs_w_kinds
 186     in
 187     tcExtendTyVarEnv tyvars (thing_inside tyvars)
 188
 189
 190
 191 tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
 192 -- tcAddScopedTyVars is used for scoped type variables
 193 -- added by pattern type signatures
 194 --      e.g.  \ (x::a) (y::a) -> x+y
 195 -- They never have explicit kinds (because this is source-code only)
 196 -- They are mutable (because they can get bound to a more specific type)
 197
 198 -- Find the not-already-in-scope signature type variables,
 199 -- kind-check them, and bring them into scope
 200 --
 201 -- We no longer specify that these type variables must be univerally
 202 -- quantified (lots of email on the subject).  If you want to put that
 203 -- back in, you need to
 204 --      a) Do a checkSigTyVars after thing_inside
 205 --      b) More insidiously, don't pass in expected_ty, else
 206 --         we unify with it too early and checkSigTyVars barfs
 207 --         Instead you have to pass in a fresh ty var, and unify
 208 --         it with expected_ty afterwards
 209 tcAddScopedTyVars [] thing_inside
 210   = thing_inside        -- Quick get-out for the empty case
 211
 212 tcAddScopedTyVars sig_tys thing_inside
 213   = getInLocalScope                     `thenM` \ in_scope ->
 214     let
 215         all_sig_tvs     = foldr (unionNameSets . extractHsTyVars) emptyNameSet sig_tys
 216         sig_tvs         = filter (not . in_scope) (nameSetToList all_sig_tvs)
 217     in
 218     mappM newNamedKindVar sig_tvs                       `thenM` \ kind_env ->
 219     tcExtendKindEnv kind_env (kcHsSigTypes sig_tys)     `thenM_`
 220     zonkKindEnv kind_env                                `thenM` \ tvs_w_kinds ->
 221     sequenceM [ newMutTyVar name kind PatSigTv
 222               | (name, kind) <- tvs_w_kinds]            `thenM` \ tyvars ->
 223     tcExtendTyVarEnv tyvars thing_inside
 224 \end{code}
 225
 226
 227 \begin{code}
 228 kcHsTyVar  :: HsTyVarBndr name   -> TcM (name, TcKind)
 229 kcHsTyVars :: [HsTyVarBndr name] -> TcM [(name, TcKind)]
 230
 231 kcHsTyVar (UserTyVar name)       = newNamedKindVar name
 232 kcHsTyVar (IfaceTyVar name kind) = returnM (name, kind)
 233
 234 kcHsTyVars tvs = mappM kcHsTyVar tvs
 235
 236 newNamedKindVar name = newKindVar       `thenM` \ kind ->
 237                        returnM (name, kind)
 238
 239 ---------------------------
 240 kcLiftedType :: RenamedHsType -> TcM ()
 241         -- The type ty must be a *lifted* *type*
 242 kcLiftedType ty
 243   = kcHsType ty                         `thenM` \ kind ->
 244     addErrCtxt (typeKindCtxt ty)        $
 245     unifyKind liftedTypeKind kind
 246
 247 ---------------------------
 248 kcTypeType :: RenamedHsType -> TcM ()
 249         -- The type ty must be a *type*, but it can be lifted or unlifted.
 250 kcTypeType ty
 251   = kcHsType ty                         `thenM` \ kind ->
 252     addErrCtxt (typeKindCtxt ty)        $
 253     unifyOpenTypeKind kind
 254
 255 ---------------------------
 256 kcHsSigType, kcHsLiftedSigType :: RenamedHsType -> TcM ()
 257         -- Used for type signatures
 258 kcHsSigType       = kcTypeType
 259 kcHsSigTypes tys  = mappM_ kcHsSigType tys
 260 kcHsLiftedSigType = kcLiftedType
 261
 262 ---------------------------
 263 kcHsType :: RenamedHsType -> TcM TcKind
 264 kcHsType (HsTyVar name)       = kcTyVar name
 265
 266 kcHsType (HsKindSig ty k)
 267   = kcHsType ty                 `thenM` \ k' ->
 268     unifyKind k k'              `thenM_`
 269     returnM k
 270
 271 kcHsType (HsListTy ty)
 272   = kcLiftedType ty             `thenM` \ tau_ty ->
 273     returnM liftedTypeKind
 274
 275 kcHsType (HsPArrTy ty)
 276   = kcLiftedType ty             `thenM` \ tau_ty ->
 277     returnM liftedTypeKind
 278
 279 kcHsType (HsTupleTy (HsTupCon boxity _) tys)
 280   = mappM kcTypeType tys        `thenM_`
 281     returnM (case boxity of
 282                   Boxed   -> liftedTypeKind
 283                   Unboxed -> unliftedTypeKind)
 284
 285 kcHsType (HsFunTy ty1 ty2)
 286   = kcTypeType ty1      `thenM_`
 287     kcTypeType ty2      `thenM_`
 288     returnM liftedTypeKind
 289
 290 kcHsType (HsOpTy ty1 HsArrow ty2)
 291   = kcTypeType ty1      `thenM_`
 292     kcTypeType ty2      `thenM_`
 293     returnM liftedTypeKind
 294
 295 kcHsType ty@(HsOpTy ty1 (HsTyOp op) ty2)
 296   = kcTyVar op                          `thenM` \ op_kind ->
 297     kcHsType ty1                        `thenM` \ ty1_kind ->
 298     kcHsType ty2                        `thenM` \ ty2_kind ->
 299     addErrCtxt (appKindCtxt (ppr ty))   $
 300     kcAppKind op_kind  ty1_kind         `thenM` \ op_kind' ->
 301     kcAppKind op_kind' ty2_kind
 302
 303 kcHsType (HsParTy ty)           -- Skip parentheses markers
 304   = kcHsType ty
 305
 306 kcHsType (HsNumTy _)            -- The unit type for generics
 307   = returnM liftedTypeKind
 308
 309 kcHsType (HsPredTy pred)
 310   = kcHsPred pred               `thenM_`
 311     returnM liftedTypeKind
 312
 313 kcHsType ty@(HsAppTy ty1 ty2)
 314   = kcHsType ty1                        `thenM` \ tc_kind ->
 315     kcHsType ty2                        `thenM` \ arg_kind ->
 316     addErrCtxt (appKindCtxt (ppr ty))   $
 317     kcAppKind tc_kind arg_kind
 318
 319 kcHsType (HsForAllTy (Just tv_names) context ty)
 320   = kcHsTyVars tv_names         `thenM` \ kind_env ->
 321     tcExtendKindEnv kind_env    $
 322     kcHsContext context         `thenM_`
 323     kcLiftedType ty             `thenM_`
 324         -- The body of a forall must be of kind *
 325         -- In principle, I suppose, we could allow unlifted types,
 326         -- but it seems simpler to stick to lifted types for now.
 327     returnM liftedTypeKind
 328
 329 ---------------------------
 330 kcAppKind fun_kind arg_kind
 331   = case tcSplitFunTy_maybe fun_kind of
 332         Just (arg_kind', res_kind)
 333                 -> unifyKind arg_kind arg_kind' `thenM_`
 334                    returnM res_kind
 335
 336         Nothing -> newKindVar                                           `thenM` \ res_kind ->
 337                    unifyKind fun_kind (mkArrowKind arg_kind res_kind)   `thenM_`
 338                    returnM res_kind
 339
 340
 341 ---------------------------
 342 kc_pred :: RenamedHsPred -> TcM TcKind  -- Does *not* check for a saturated
 343                                         -- application (reason: used from TcDeriv)
 344 kc_pred pred@(HsIParam name ty)
 345   = kcHsType ty
 346
 347 kc_pred pred@(HsClassP cls tys)
 348   = kcClass cls                         `thenM` \ kind ->
 349     mappM kcHsType tys                  `thenM` \ arg_kinds ->
 350     newKindVar                          `thenM` \ kv ->
 351     unifyKind kind (mkArrowKinds arg_kinds kv)  `thenM_`
 352     returnM kv
 353
 354 ---------------------------
 355 kcHsContext ctxt = mappM_ kcHsPred ctxt
 356
 357 kcHsPred pred           -- Checks that the result is of kind liftedType
 358   = addErrCtxt (appKindCtxt (ppr pred)) $
 359     kc_pred pred                                `thenM` \ kind ->
 360     unifyKind liftedTypeKind kind               `thenM_`
 361     returnM ()
 362
 363
 364  ---------------------------
 365 kcTyVar name    -- Could be a tyvar or a tycon
 366   = tcLookup name       `thenM` \ thing ->
 367     case thing of
 368         AThing kind         -> returnM kind
 369         ATyVar tv           -> returnM (tyVarKind tv)
 370         AGlobal (ATyCon tc) -> returnM (tyConKind tc)
 371         other               -> failWithTc (wrongThingErr "type" thing name)
 372
 373 kcClass cls     -- Must be a class
 374   = tcLookup cls                                `thenM` \ thing ->
 375     case thing of
 376         AThing kind           -> returnM kind
 377         AGlobal (AClass cls)  -> returnM (tyConKind (classTyCon cls))
 378         other                 -> failWithTc (wrongThingErr "class" thing cls)
 379 \end{code}
 380
 381 %************************************************************************
 382 %*                                                                      *
 383 \subsection{tc_type}
 384 %*                                                                      *
 385 %************************************************************************
 386
 387 tc_type, the main work horse
 388 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 389
 390         -------------------
 391         *** BIG WARNING ***
 392         -------------------
 393
 394 tc_type is used to typecheck the types in the RHS of data
 395 constructors.  In the case of recursive data types, that means that
 396 the type constructors themselves are (partly) black holes.  e.g.
 397
 398         data T a = MkT a [T a]
 399
 400 While typechecking the [T a] on the RHS, T itself is not yet fully
 401 defined.  That in turn places restrictions on what you can check in
 402 tcHsType; if you poke on too much you get a black hole.  I keep
 403 forgetting this, hence this warning!
 404
 405 So tc_type does no validity-checking.  Instead that's all done
 406 by TcMType.checkValidType
 407
 408         --------------------------
 409         *** END OF BIG WARNING ***
 410         --------------------------
 411
 412
 413 \begin{code}
 414 tc_type :: RenamedHsType -> TcM Type
 415
 416 tc_type ty@(HsTyVar name)
 417   = tc_app ty []
 418
 419 tc_type (HsKindSig ty k)
 420   = tc_type ty  -- Kind checking done already
 421
 422 tc_type (HsListTy ty)
 423   = tc_type ty  `thenM` \ tau_ty ->
 424     returnM (mkListTy tau_ty)
 425
 426 tc_type (HsPArrTy ty)
 427   = tc_type ty  `thenM` \ tau_ty ->
 428     returnM (mkPArrTy tau_ty)
 429
 430 tc_type (HsTupleTy (HsTupCon boxity arity) tys)
 431   = ASSERT( tys `lengthIs` arity )
 432     tc_types tys        `thenM` \ tau_tys ->
 433     returnM (mkTupleTy boxity arity tau_tys)
 434
 435 tc_type (HsFunTy ty1 ty2)
 436   = tc_type ty1                 `thenM` \ tau_ty1 ->
 437     tc_type ty2                 `thenM` \ tau_ty2 ->
 438     returnM (mkFunTy tau_ty1 tau_ty2)
 439
 440 tc_type (HsOpTy ty1 HsArrow ty2)
 441   = tc_type ty1 `thenM` \ tau_ty1 ->
 442     tc_type ty2 `thenM` \ tau_ty2 ->
 443     returnM (mkFunTy tau_ty1 tau_ty2)
 444
 445 tc_type (HsOpTy ty1 (HsTyOp op) ty2)
 446   = tc_type ty1 `thenM` \ tau_ty1 ->
 447     tc_type ty2 `thenM` \ tau_ty2 ->
 448     tc_fun_type op [tau_ty1,tau_ty2]
 449
 450 tc_type (HsParTy ty)            -- Remove the parentheses markers
 451   = tc_type ty
 452
 453 tc_type (HsNumTy n)
 454   = ASSERT(n== 1)
 455     returnM (mkTyConApp genUnitTyCon [])
 456
 457 tc_type (HsAppTy ty1 ty2) = tc_app ty1 [ty2]
 458
 459 tc_type (HsPredTy pred)
 460   = tc_pred pred        `thenM` \ pred' ->
 461     returnM (mkPredTy pred')
 462
 463 tc_type full_ty@(HsForAllTy (Just tv_names) ctxt ty)
 464   = let
 465         kind_check = kcHsContext ctxt `thenM_` kcHsType ty
 466     in
 467     tcHsTyVars tv_names kind_check      $ \ tyvars ->
 468     mappM tc_pred ctxt                  `thenM` \ theta ->
 469     tc_type ty                          `thenM` \ tau ->
 470     returnM (mkSigmaTy tyvars theta tau)
 471
 472 tc_types arg_tys = mappM tc_type arg_tys
 473 \end{code}
 474
 475 Help functions for type applications
 476 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 477
 478 \begin{code}
 479 tc_app :: RenamedHsType -> [RenamedHsType] -> TcM Type
 480 tc_app (HsAppTy ty1 ty2) tys
 481   = tc_app ty1 (ty2:tys)
 482
 483 tc_app ty tys
 484   = addErrCtxt (appKindCtxt pp_app)     $
 485     tc_types tys                        `thenM` \ arg_tys ->
 486     case ty of
 487         HsTyVar fun -> tc_fun_type fun arg_tys
 488         other       -> tc_type ty               `thenM` \ fun_ty ->
 489                        returnM (mkAppTys fun_ty arg_tys)
 490   where
 491     pp_app = ppr ty <+> sep (map pprParendHsType tys)
 492
 493 -- (tc_fun_type ty arg_tys) returns (mkAppTys ty arg_tys)
 494 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
 495 --      hence the rather strange functionality.
 496
 497 tc_fun_type name arg_tys
 498   = tcLookup name                       `thenM` \ thing ->
 499     case thing of
 500         ATyVar tv -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
 501
 502         AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
 503
 504         other -> failWithTc (wrongThingErr "type constructor" thing name)
 505 \end{code}
 506
 507
 508 Contexts
 509 ~~~~~~~~
 510 \begin{code}
 511 tcHsPred pred = kc_pred pred `thenM_`  tc_pred pred
 512         -- Is happy with a partial application, e.g. (ST s)
 513         -- Used from TcDeriv
 514
 515 tc_pred assn@(HsClassP class_name tys)
 516   = addErrCtxt (appKindCtxt (ppr assn)) $
 517     tc_types tys                        `thenM` \ arg_tys ->
 518     tcLookupGlobal class_name                   `thenM` \ thing ->
 519     case thing of
 520         AClass clas -> returnM (ClassP clas arg_tys)
 521         other       -> failWithTc (wrongThingErr "class" (AGlobal thing) class_name)
 522
 523 tc_pred assn@(HsIParam name ty)
 524   = addErrCtxt (appKindCtxt (ppr assn)) $
 525     tc_type ty                                  `thenM` \ arg_ty ->
 526     returnM (IParam name arg_ty)
 527 \end{code}
 528
 529
 530
 531 %************************************************************************
 532 %*                                                                      *
 533 \subsection{Type variables, with knot tying!}
 534 %*                                                                      *
 535 %************************************************************************
 536
 537 \begin{code}
 538 mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
 539 mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
 540
 541 mkTyClTyVars :: Kind                    -- Kind of the tycon or class
 542              -> [HsTyVarBndr Name]
 543              -> [TyVar]
 544 mkTyClTyVars kind tyvar_names
 545   = mkImmutTyVars tyvars_w_kinds
 546   where
 547     (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
 548 \end{code}
 549
 550
 551 %************************************************************************
 552 %*                                                                      *
 553 \subsection{Signatures}
 554 %*                                                                      *
 555 %************************************************************************
 556
 557 @tcSigs@ checks the signatures for validity, and returns a list of
 558 {\em freshly-instantiated} signatures.  That is, the types are already
 559 split up, and have fresh type variables installed.  All non-type-signature
 560 "RenamedSigs" are ignored.
 561
 562 The @TcSigInfo@ contains @TcTypes@ because they are unified with
 563 the variable's type, and after that checked to see whether they've
 564 been instantiated.
 565
 566 \begin{code}
 567 data TcSigInfo
 568   = TySigInfo
 569         TcId                    -- *Polymorphic* binder for this value...
 570                                 -- Has name = N
 571
 572         [TcTyVar]               -- tyvars
 573         TcThetaType             -- theta
 574         TcTauType               -- tau
 575
 576         TcId                    -- *Monomorphic* binder for this value
 577                                 -- Does *not* have name = N
 578                                 -- Has type tau
 579
 580         [Inst]                  -- Empty if theta is null, or
 581                                 -- (method mono_id) otherwise
 582
 583         SrcLoc                  -- Of the signature
 584
 585 instance Outputable TcSigInfo where
 586     ppr (TySigInfo id tyvars theta tau _ inst loc) =
 587         ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
 588
 589 tcSigPolyId :: TcSigInfo -> TcId
 590 tcSigPolyId (TySigInfo id _ _ _ _ _ _) = id
 591
 592 tcSigMonoId :: TcSigInfo -> TcId
 593 tcSigMonoId (TySigInfo _ _ _ _ id _ _) = id
 594
 595 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
 596         -- Search for a particular signature
 597 maybeSig [] name = Nothing
 598 maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name
 599   | name == idName sig_id = Just sig
 600   | otherwise             = maybeSig sigs name
 601 \end{code}
 602
 603
 604 \begin{code}
 605 tcTySig :: RenamedSig -> TcM TcSigInfo
 606
 607 tcTySig (Sig v ty src_loc)
 608  = addSrcLoc src_loc                            $
 609    tcHsSigType (FunSigCtxt v) ty                `thenM` \ sigma_tc_ty ->
 610    mkTcSig (mkLocalId v sigma_tc_ty) src_loc    `thenM` \ sig ->
 611    returnM sig
 612
 613 mkTcSig :: TcId -> SrcLoc -> TcM TcSigInfo
 614 mkTcSig poly_id src_loc
 615   =     -- Instantiate this type
 616         -- It's important to do this even though in the error-free case
 617         -- we could just split the sigma_tc_ty (since the tyvars don't
 618         -- unified with anything).  But in the case of an error, when
 619         -- the tyvars *do* get unified with something, we want to carry on
 620         -- typechecking the rest of the program with the function bound
 621         -- to a pristine type, namely sigma_tc_ty
 622    tcInstType SigTv (idType poly_id)            `thenM` \ (tyvars', theta', tau') ->
 623
 624    getInstLoc SignatureOrigin                   `thenM` \ inst_loc ->
 625    newMethodWith inst_loc poly_id
 626                  (mkTyVarTys tyvars')
 627                  theta' tau'                    `thenM` \ inst ->
 628         -- We make a Method even if it's not overloaded; no harm
 629         -- But do not extend the LIE!  We're just making an Id.
 630
 631    returnM (TySigInfo poly_id tyvars' theta' tau'
 632                           (instToId inst) [inst] src_loc)
 633 \end{code}
 634
 635
 636 %************************************************************************
 637 %*                                                                      *
 638 \subsection{Errors and contexts}
 639 %*                                                                      *
 640 %************************************************************************
 641
 642
 643 \begin{code}
 644 hoistForAllTys :: Type -> Type
 645 -- Used for user-written type signatures only
 646 -- Move all the foralls and constraints to the top
 647 -- e.g.  T -> forall a. a        ==>   forall a. T -> a
 648 --       T -> (?x::Int) -> Int   ==>   (?x::Int) -> T -> Int
 649 --
 650 -- Also: eliminate duplicate constraints.  These can show up
 651 -- when hoisting constraints, notably implicit parameters.
 652 --
 653 -- We want to 'look through' type synonyms when doing this
 654 -- so it's better done on the Type than the HsType
 655
 656 hoistForAllTys ty
 657   = let
 658         no_shadow_ty = deShadowTy ty
 659         -- Running over ty with an empty substitution gives it the
 660         -- no-shadowing property.  This is important.  For example:
 661         --      type Foo r = forall a. a -> r
 662         --      foo :: Foo (Foo ())
 663         -- Here the hoisting should give
 664         --      foo :: forall a a1. a -> a1 -> ()
 665         --
 666         -- What about type vars that are lexically in scope in the envt?
 667         -- We simply rely on them having a different unique to any
 668         -- binder in 'ty'.  Otherwise we'd have to slurp the in-scope-tyvars
 669         -- out of the envt, which is boring and (I think) not necessary.
 670     in
 671     case hoist no_shadow_ty of
 672         (tvs, theta, body) -> mkForAllTys tvs (mkFunTys (nubBy tcEqType theta) body)
 673                 -- The 'nubBy' eliminates duplicate constraints,
 674                 -- notably implicit parameters
 675   where
 676     hoist ty
 677         | (tvs1, body_ty) <- tcSplitForAllTys ty,
 678           not (null tvs1)
 679         = case hoist body_ty of
 680                 (tvs2,theta,tau) -> (tvs1 ++ tvs2, theta, tau)
 681
 682         | Just (arg, res) <- tcSplitFunTy_maybe ty
 683         = let
 684               arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively
 685           in                            -- to the argument type
 686           if (isPredTy arg') then
 687             case hoist res of
 688                 (tvs,theta,tau) -> (tvs, arg':theta, tau)
 689           else
 690              case hoist res of
 691                 (tvs,theta,tau) -> (tvs, theta, mkFunTy arg' tau)
 692
 693         | otherwise = ([], [], ty)
 694 \end{code}
 695
 696
 697 %************************************************************************
 698 %*                                                                      *
 699 \subsection{Errors and contexts}
 700 %*                                                                      *
 701 %************************************************************************
 702
 703 \begin{code}
 704 typeKindCtxt :: RenamedHsType -> Message
 705 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
 706                        nest 2 (quotes (ppr ty)),
 707                        ptext SLIT("is a type")]
 708
 709 appKindCtxt :: SDoc -> Message
 710 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
 711
 712 wrongThingErr expected thing name
 713   = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
 714   where
 715     pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
 716     pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
 717     pp_thing (AGlobal (AnId   _)) = ptext SLIT("Identifier")
 718     pp_thing (ATyVar _)           = ptext SLIT("Type variable")
 719     pp_thing (ATcId _ _)          = ptext SLIT("Local identifier")
 720     pp_thing (AThing _)           = ptext SLIT("Utterly bogus")
 721 \end{code}