ghc/compiler/typecheck/TcMonoType.lhs

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