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                     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
  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   * They are only called when there are no kind vars in the environment
 269         so the kind returned is indeed a Kind not a TcKind
 270
 271 \begin{code}
 272 tcHsSigType :: RenamedHsType -> TcM s TcType
 273 tcHsSigType ty
 274   = kcTypeType ty       `thenTc_`
 275     tcHsType ty         `thenTc` \ ty' ->
 276     returnTc (hoistForAllTys ty')
 277
 278 tcHsBoxedSigType :: RenamedHsType -> TcM s Type
 279 tcHsBoxedSigType ty
 280   = kcBoxedType ty      `thenTc_`
 281     tcHsType ty         `thenTc` \ ty' ->
 282     returnTc (hoistForAllTys ty')
 283 \end{code}
 284
 285
 286 tcHsType, the main work horse
 287 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 288
 289 \begin{code}
 290 tcHsType :: RenamedHsType -> TcM s Type
 291 tcHsType ty@(HsTyVar name)
 292   = tc_app ty []
 293
 294 tcHsType (HsListTy ty)
 295   = tcHsType ty         `thenTc` \ tau_ty ->
 296     returnTc (mkListTy tau_ty)
 297
 298 tcHsType (HsTupleTy (HsTupCon _ boxity) tys)
 299   = mapTc tcHsType tys  `thenTc` \ tau_tys ->
 300     returnTc (mkTupleTy boxity (length tys) tau_tys)
 301
 302 tcHsType (HsFunTy ty1 ty2)
 303   = tcHsType ty1        `thenTc` \ tau_ty1 ->
 304     tcHsType ty2        `thenTc` \ tau_ty2 ->
 305     returnTc (mkFunTy tau_ty1 tau_ty2)
 306
 307 tcHsType (HsAppTy ty1 ty2)
 308   = tc_app ty1 [ty2]
 309
 310 tcHsType (HsPredTy pred)
 311   = tcClassAssertion True pred  `thenTc` \ pred' ->
 312     returnTc (mkPredTy pred')
 313
 314 tcHsType (HsUsgTy usg ty)
 315   = newUsg usg                  `thenTc` \ usg' ->
 316     tcHsType ty                 `thenTc` \ tc_ty ->
 317     returnTc (mkUsgTy usg' tc_ty)
 318   where
 319     newUsg usg = case usg of
 320                    HsUsOnce        -> returnTc UsOnce
 321                    HsUsMany        -> returnTc UsMany
 322                    HsUsVar uv_name -> tcLookupUVar uv_name `thenTc` \ uv ->
 323                                       returnTc (UsVar uv)
 324
 325 tcHsType (HsUsgForAllTy uv_name ty)
 326   = let
 327         uv = mkNamedUVar uv_name
 328     in
 329     tcExtendUVarEnv uv_name uv $
 330     tcHsType ty                     `thenTc` \ tc_ty ->
 331     returnTc (mkUsForAllTy uv tc_ty)
 332
 333 tcHsType full_ty@(HsForAllTy (Just tv_names) ctxt ty)
 334   = kcTyVarScope tv_names
 335                  (kcHsContext ctxt `thenTc_` kcHsType ty)  `thenTc` \ tv_kinds ->
 336     let
 337         forall_tyvars = mkImmutTyVars tv_kinds
 338     in
 339     tcExtendTyVarEnv forall_tyvars      $
 340     tcContext ctxt                      `thenTc` \ theta ->
 341     tcHsType ty                         `thenTc` \ tau ->
 342     let
 343         -- Check for ambiguity
 344         --   forall V. P => tau
 345         -- is ambiguous if P contains generic variables
 346         -- (i.e. one of the Vs) that are not mentioned in tau
 347         --
 348         -- However, we need to take account of functional dependencies
 349         -- when we speak of 'mentioned in tau'.  Example:
 350         --      class C a b | a -> b where ...
 351         -- Then the type
 352         --      forall x y. (C x y) => x
 353         -- is not ambiguous because x is mentioned and x determines y
 354         --
 355         -- NOTE: In addition, GHC insists that at least one type variable
 356         -- in each constraint is in V.  So we disallow a type like
 357         --      forall a. Eq b => b -> b
 358         -- even in a scope where b is in scope.
 359         -- This is the is_free test below.
 360
 361         tau_vars            = tyVarsOfType tau
 362         fds                 = instFunDepsOfTheta theta
 363         tvFundep            = tyVarFunDep fds
 364         extended_tau_vars   = oclose tvFundep tau_vars
 365         is_ambig ct_var     = (ct_var `elem` forall_tyvars) &&
 366                               not (ct_var `elemUFM` extended_tau_vars)
 367         is_free ct_var      = not (ct_var `elem` forall_tyvars)
 368
 369         check_pred pred = checkTc (not any_ambig) (ambigErr pred full_ty) `thenTc_`
 370                           checkTc (not all_free)  (freeErr  pred full_ty)
 371               where
 372                 ct_vars   = varSetElems (tyVarsOfPred pred)
 373                 any_ambig = is_source_polytype && any is_ambig ct_vars
 374                 all_free  = all is_free  ct_vars
 375
 376         -- Check ambiguity only for source-program types, not
 377         -- for types coming from inteface files.  The latter can
 378         -- legitimately have ambiguous types. Example
 379         --    class S a where s :: a -> (Int,Int)
 380         --    instance S Char where s _ = (1,1)
 381         --    f:: S a => [a] -> Int -> (Int,Int)
 382         --    f (_::[a]) x = (a*x,b)
 383         --      where (a,b) = s (undefined::a)
 384         -- Here the worker for f gets the type
 385         --      fw :: forall a. S a => Int -> (# Int, Int #)
 386         --
 387         -- If the list of tv_names is empty, we have a monotype,
 388         -- and then we don't need to check for ambiguity either,
 389         -- because the test can't fail (see is_ambig).
 390         is_source_polytype = case tv_names of
 391                                 (UserTyVar _ : _) -> True
 392                                 other             -> False
 393     in
 394     mapTc check_pred theta              `thenTc_`
 395     returnTc (mkSigmaTy forall_tyvars theta tau)
 396 \end{code}
 397
 398 Help functions for type applications
 399 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 400
 401 \begin{code}
 402 tc_app (HsAppTy ty1 ty2) tys
 403   = tc_app ty1 (ty2:tys)
 404
 405 tc_app ty tys
 406   = tcAddErrCtxt (appKindCtxt pp_app)   $
 407     mapTc tcHsType tys                  `thenTc` \ arg_tys ->
 408     tc_fun_type ty arg_tys
 409   where
 410     pp_app = ppr ty <+> sep (map pprParendHsType tys)
 411
 412 -- (tc_fun_type ty arg_tys) returns (mkAppTys ty arg_tys)
 413 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
 414 --      hence the rather strange functionality.
 415
 416 tc_fun_type (HsTyVar name) arg_tys
 417   = tcLookupTy name                     `thenTc` \ thing ->
 418     case thing of
 419         ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)
 420
 421         ATyCon tc | isSynTyCon tc ->  checkTc arity_ok err_msg  `thenTc_`
 422                                       returnTc (mkAppTys (mkSynTy tc (take arity arg_tys))
 423                                                          (drop arity arg_tys))
 424
 425                   | otherwise     ->  returnTc (mkTyConApp tc arg_tys)
 426                   where
 427
 428                     arity_ok = arity <= n_args
 429                     arity = tyConArity tc
 430                         -- It's OK to have an *over-applied* type synonym
 431                         --      data Tree a b = ...
 432                         --      type Foo a = Tree [a]
 433                         --      f :: Foo a b -> ...
 434                     err_msg = arityErr "Type synonym" name arity n_args
 435                     n_args  = length arg_tys
 436
 437         other -> failWithTc (wrongThingErr "type constructor" thing name)
 438
 439 tc_fun_type ty arg_tys
 440   = tcHsType ty         `thenTc` \ fun_ty ->
 441     returnNF_Tc (mkAppTys fun_ty arg_tys)
 442 \end{code}
 443
 444
 445 Contexts
 446 ~~~~~~~~
 447 \begin{code}
 448 tcClassContext :: RenamedContext -> TcM s ClassContext
 449         -- Used when we are expecting a ClassContext (i.e. no implicit params)
 450 tcClassContext context
 451   = tcContext context   `thenTc` \ theta ->
 452     returnTc (classesOfPreds theta)
 453
 454 tcContext :: RenamedContext -> TcM s ThetaType
 455 tcContext context = mapTc (tcClassAssertion False) context
 456
 457 tcClassAssertion ccall_ok assn@(HsPClass class_name tys)
 458   = tcAddErrCtxt (appKindCtxt (ppr assn))       $
 459     mapTc tcHsType tys                          `thenTc` \ arg_tys ->
 460     tcLookupTy class_name                       `thenTc` \ thing ->
 461     case thing of
 462         AClass clas -> checkTc (arity == n_tys) err                             `thenTc_`
 463                        returnTc (Class clas arg_tys)
 464             where
 465                 arity = classArity clas
 466                 n_tys = length tys
 467                 err   = arityErr "Class" class_name arity n_tys
 468
 469         other -> failWithTc (wrongThingErr "class" thing class_name)
 470
 471 tcClassAssertion ccall_ok assn@(HsPIParam name ty)
 472   = tcAddErrCtxt (appKindCtxt (ppr assn))       $
 473     tcHsType ty                                 `thenTc` \ arg_ty ->
 474     returnTc (IParam name arg_ty)
 475 \end{code}
 476
 477
 478 %************************************************************************
 479 %*                                                                      *
 480 \subsection{Type variables, with knot tying!}
 481 %*                                                                      *
 482 %************************************************************************
 483
 484 \begin{code}
 485 mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
 486 newSigTyVars  :: [(Name,Kind)] -> NF_TcM s [TcTyVar]
 487
 488 mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
 489 newSigTyVars  pairs = listNF_Tc [tcNewSigTyVar name kind | (name,kind) <- pairs]
 490
 491 mkTyClTyVars :: Kind                    -- Kind of the tycon or class
 492              -> [HsTyVarBndr Name]
 493              -> [TyVar]
 494 mkTyClTyVars kind tyvar_names
 495   = mkImmutTyVars tyvars_w_kinds
 496   where
 497     (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
 498 \end{code}
 499
 500
 501 %************************************************************************
 502 %*                                                                      *
 503 \subsection{Signatures}
 504 %*                                                                      *
 505 %************************************************************************
 506
 507 @tcSigs@ checks the signatures for validity, and returns a list of
 508 {\em freshly-instantiated} signatures.  That is, the types are already
 509 split up, and have fresh type variables installed.  All non-type-signature
 510 "RenamedSigs" are ignored.
 511
 512 The @TcSigInfo@ contains @TcTypes@ because they are unified with
 513 the variable's type, and after that checked to see whether they've
 514 been instantiated.
 515
 516 \begin{code}
 517 data TcSigInfo
 518   = TySigInfo
 519         Name                    -- N, the Name in corresponding binding
 520
 521         TcId                    -- *Polymorphic* binder for this value...
 522                                 -- Has name = N
 523
 524         [TcTyVar]               -- tyvars
 525         TcThetaType             -- theta
 526         TcTauType               -- tau
 527
 528         TcId                    -- *Monomorphic* binder for this value
 529                                 -- Does *not* have name = N
 530                                 -- Has type tau
 531
 532         [Inst]                  -- Empty if theta is null, or
 533                                 -- (method mono_id) otherwise
 534
 535         SrcLoc                  -- Of the signature
 536
 537 instance Outputable TcSigInfo where
 538     ppr (TySigInfo nm id tyvars theta tau _ inst loc) =
 539         ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
 540
 541 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
 542         -- Search for a particular signature
 543 maybeSig [] name = Nothing
 544 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
 545   | name == sig_name = Just sig
 546   | otherwise        = maybeSig sigs name
 547 \end{code}
 548
 549
 550 \begin{code}
 551 tcTySig :: RenamedSig -> TcM s TcSigInfo
 552
 553 tcTySig (Sig v ty src_loc)
 554  = tcAddSrcLoc src_loc                          $
 555    tcAddErrCtxt (tcsigCtxt v)                   $
 556    tcHsSigType ty                               `thenTc` \ sigma_tc_ty ->
 557    mkTcSig (mkVanillaId v sigma_tc_ty) src_loc  `thenNF_Tc` \ sig ->
 558    returnTc sig
 559
 560 mkTcSig :: TcId -> SrcLoc -> NF_TcM s TcSigInfo
 561 mkTcSig poly_id src_loc
 562   =     -- Instantiate this type
 563         -- It's important to do this even though in the error-free case
 564         -- we could just split the sigma_tc_ty (since the tyvars don't
 565         -- unified with anything).  But in the case of an error, when
 566         -- the tyvars *do* get unified with something, we want to carry on
 567         -- typechecking the rest of the program with the function bound
 568         -- to a pristine type, namely sigma_tc_ty
 569    let
 570         (tyvars, rho) = splitForAllTys (idType poly_id)
 571    in
 572    mapNF_Tc tcInstSigVar tyvars         `thenNF_Tc` \ tyvars' ->
 573         -- Make *signature* type variables
 574
 575    let
 576      tyvar_tys' = mkTyVarTys tyvars'
 577      rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
 578         -- mkTopTyVarSubst because the tyvars' are fresh
 579      (theta', tau') = splitRhoTy rho'
 580         -- This splitRhoTy tries hard to make sure that tau' is a type synonym
 581         -- wherever possible, which can improve interface files.
 582    in
 583    newMethodWithGivenTy SignatureOrigin
 584                 poly_id
 585                 tyvar_tys'
 586                 theta' tau'                     `thenNF_Tc` \ inst ->
 587         -- We make a Method even if it's not overloaded; no harm
 588    instFunDeps SignatureOrigin theta'           `thenNF_Tc` \ fds ->
 589
 590    returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) (inst : fds) src_loc)
 591   where
 592     name = idName poly_id
 593 \end{code}
 594
 595
 596
 597 %************************************************************************
 598 %*                                                                      *
 599 \subsection{Checking signature type variables}
 600 %*                                                                      *
 601 %************************************************************************
 602
 603 @checkSigTyVars@ is used after the type in a type signature has been unified with
 604 the actual type found.  It then checks that the type variables of the type signature
 605 are
 606         (a) Still all type variables
 607                 eg matching signature [a] against inferred type [(p,q)]
 608                 [then a will be unified to a non-type variable]
 609
 610         (b) Still all distinct
 611                 eg matching signature [(a,b)] against inferred type [(p,p)]
 612                 [then a and b will be unified together]
 613
 614         (c) Not mentioned in the environment
 615                 eg the signature for f in this:
 616
 617                         g x = ... where
 618                                         f :: a->[a]
 619                                         f y = [x,y]
 620
 621                 Here, f is forced to be monorphic by the free occurence of x.
 622
 623         (d) Not (unified with another type variable that is) in scope.
 624                 eg f x :: (r->r) = (\y->y) :: forall a. a->r
 625             when checking the expression type signature, we find that
 626             even though there is nothing in scope whose type mentions r,
 627             nevertheless the type signature for the expression isn't right.
 628
 629             Another example is in a class or instance declaration:
 630                 class C a where
 631                    op :: forall b. a -> b
 632                    op x = x
 633             Here, b gets unified with a
 634
 635 Before doing this, the substitution is applied to the signature type variable.
 636
 637 We used to have the notion of a "DontBind" type variable, which would
 638 only be bound to itself or nothing.  Then points (a) and (b) were
 639 self-checking.  But it gave rise to bogus consequential error messages.
 640 For example:
 641
 642    f = (*)      -- Monomorphic
 643
 644    g :: Num a => a -> a
 645    g x = f x x
 646
 647 Here, we get a complaint when checking the type signature for g,
 648 that g isn't polymorphic enough; but then we get another one when
 649 dealing with the (Num x) context arising from f's definition;
 650 we try to unify x with Int (to default it), but find that x has already
 651 been unified with the DontBind variable "a" from g's signature.
 652 This is really a problem with side-effecting unification; we'd like to
 653 undo g's effects when its type signature fails, but unification is done
 654 by side effect, so we can't (easily).
 655
 656 So we revert to ordinary type variables for signatures, and try to
 657 give a helpful message in checkSigTyVars.
 658
 659 \begin{code}
 660 checkSigTyVars :: [TcTyVar]             -- Universally-quantified type variables in the signature
 661                -> TcTyVarSet            -- Tyvars that are free in the type signature
 662                                         -- These should *already* be in the global-var set, and are
 663                                         -- used here only to improve the error message
 664                -> TcM s [TcTyVar]       -- Zonked signature type variables
 665
 666 checkSigTyVars [] free = returnTc []
 667
 668 checkSigTyVars sig_tyvars free_tyvars
 669   = zonkTcTyVars sig_tyvars             `thenNF_Tc` \ sig_tys ->
 670     tcGetGlobalTyVars                   `thenNF_Tc` \ globals ->
 671
 672     checkTcM (all_ok sig_tys globals)
 673              (complain sig_tys globals) `thenTc_`
 674
 675     returnTc (map (getTyVar "checkSigTyVars") sig_tys)
 676
 677   where
 678     all_ok []       acc = True
 679     all_ok (ty:tys) acc = case getTyVar_maybe ty of
 680                             Nothing                       -> False      -- Point (a)
 681                             Just tv | tv `elemVarSet` acc -> False      -- Point (b) or (c)
 682                                     | otherwise           -> all_ok tys (acc `extendVarSet` tv)
 683
 684
 685     complain sig_tys globals
 686       = -- For the in-scope ones, zonk them and construct a map
 687         -- from the zonked tyvar to the in-scope one
 688         -- If any of the in-scope tyvars zonk to a type, then ignore them;
 689         -- that'll be caught later when we back up to their type sig
 690         tcGetInScopeTyVars                      `thenNF_Tc` \ in_scope_tvs ->
 691         zonkTcTyVars in_scope_tvs               `thenNF_Tc` \ in_scope_tys ->
 692         let
 693             in_scope_assoc = [ (zonked_tv, in_scope_tv)
 694                              | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
 695                                Just zonked_tv <- [getTyVar_maybe z_ty]
 696                              ]
 697             in_scope_env = mkVarEnv in_scope_assoc
 698         in
 699
 700         -- "check" checks each sig tyvar in turn
 701         foldlNF_Tc check
 702                    (env2, in_scope_env, [])
 703                    (tidy_tvs `zip` tidy_tys)    `thenNF_Tc` \ (env3, _, msgs) ->
 704
 705         failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
 706       where
 707         (env1, tidy_tvs) = mapAccumL tidyTyVar emptyTidyEnv sig_tyvars
 708         (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
 709
 710         main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
 711
 712         check (env, acc, msgs) (sig_tyvar,ty)
 713                 -- sig_tyvar is from the signature;
 714                 -- ty is what you get if you zonk sig_tyvar and then tidy it
 715                 --
 716                 -- acc maps a zonked type variable back to a signature type variable
 717           = case getTyVar_maybe ty of {
 718               Nothing ->                        -- Error (a)!
 719                         returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr ty) : msgs) ;
 720
 721               Just tv ->
 722
 723             case lookupVarEnv acc tv of {
 724                 Just sig_tyvar' ->      -- Error (b) or (d)!
 725                         returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr sig_tyvar') : msgs) ;
 726
 727                 Nothing ->
 728
 729             if tv `elemVarSet` globals  -- Error (c)! Type variable escapes
 730                                         -- The least comprehensible, so put it last
 731             then   tcGetValueEnv                                        `thenNF_Tc` \ ve ->
 732                    find_globals tv env  [] (valueEnvIds ve)             `thenNF_Tc` \ (env1, globs) ->
 733                    find_frees   tv env1 [] (varSetElems free_tyvars)    `thenNF_Tc` \ (env2, frees) ->
 734                    returnNF_Tc (env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
 735
 736             else        -- All OK
 737             returnNF_Tc (env, extendVarEnv acc tv sig_tyvar, msgs)
 738             }}
 739
 740 -- find_globals looks at the value environment and finds values
 741 -- whose types mention the offending type variable.  It has to be
 742 -- careful to zonk the Id's type first, so it has to be in the monad.
 743 -- We must be careful to pass it a zonked type variable, too.
 744 find_globals tv tidy_env acc []
 745   = returnNF_Tc (tidy_env, acc)
 746
 747 find_globals tv tidy_env acc (id:ids)
 748   | not (isLocallyDefined id) ||
 749     isEmptyVarSet (idFreeTyVars id)
 750   = find_globals tv tidy_env acc ids
 751
 752   | otherwise
 753   = zonkTcType (idType id)      `thenNF_Tc` \ id_ty ->
 754     if tv `elemVarSet` tyVarsOfType id_ty then
 755         let
 756            (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
 757            acc'                = (idName id, id_ty') : acc
 758         in
 759         find_globals tv tidy_env' acc' ids
 760     else
 761         find_globals tv tidy_env  acc  ids
 762
 763 find_frees tv tidy_env acc []
 764   = returnNF_Tc (tidy_env, acc)
 765 find_frees tv tidy_env acc (ftv:ftvs)
 766   = zonkTcTyVar ftv     `thenNF_Tc` \ ty ->
 767     if tv `elemVarSet` tyVarsOfType ty then
 768         let
 769             (tidy_env', ftv') = tidyTyVar tidy_env ftv
 770         in
 771         find_frees tv tidy_env' (ftv':acc) ftvs
 772     else
 773         find_frees tv tidy_env  acc        ftvs
 774
 775
 776 escape_msg sig_tv tv globs frees
 777   = mk_msg sig_tv <+> ptext SLIT("escapes") $$
 778     if not (null globs) then
 779         vcat [pp_it <+> ptext SLIT("is mentioned in the environment"),
 780               ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
 781               nest 2 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
 782         ]
 783      else if not (null frees) then
 784         vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
 785               nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
 786         ]
 787      else
 788         empty   -- Sigh.  It's really hard to give a good error message
 789                 -- all the time.   One bad case is an existential pattern match
 790   where
 791     is_are | isSingleton frees = ptext SLIT("is")
 792            | otherwise         = ptext SLIT("are")
 793     pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
 794           | otherwise    = ptext SLIT("It")
 795
 796     vcat_first :: Int -> [SDoc] -> SDoc
 797     vcat_first n []     = empty
 798     vcat_first 0 (x:xs) = text "...others omitted..."
 799     vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
 800
 801 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> quotes thing
 802 mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
 803 \end{code}
 804
 805 These two context are used with checkSigTyVars
 806
 807 \begin{code}
 808 sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
 809         -> TidyEnv -> NF_TcM s (TidyEnv, Message)
 810 sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
 811   = zonkTcType sig_tau          `thenNF_Tc` \ actual_tau ->
 812     let
 813         (env1, tidy_sig_tyvars)  = tidyTyVars tidy_env sig_tyvars
 814         (env2, tidy_sig_rho)     = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
 815         (env3, tidy_actual_tau)  = tidyOpenType env2 actual_tau
 816         msg = vcat [ptext SLIT("Signature type:    ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
 817                     ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
 818                     when
 819                    ]
 820     in
 821     returnNF_Tc (env3, msg)
 822
 823 sigPatCtxt bound_tvs bound_ids tidy_env
 824   = returnNF_Tc (env1,
 825                  sep [ptext SLIT("When checking a pattern that binds"),
 826                       nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
 827   where
 828     show_ids = filter is_interesting bound_ids
 829     is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
 830
 831     (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
 832     ppr_id id ty     = ppr id <+> dcolon <+> ppr ty
 833         -- Don't zonk the types so we get the separate, un-unified versions
 834 \end{code}
 835
 836
 837 %************************************************************************
 838 %*                                                                      *
 839 \subsection{Errors and contexts}
 840 %*                                                                      *
 841 %************************************************************************
 842
 843 \begin{code}
 844 tcsigCtxt v   = ptext SLIT("In a type signature for") <+> quotes (ppr v)
 845
 846 typeKindCtxt :: RenamedHsType -> Message
 847 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
 848                        nest 2 (quotes (ppr ty)),
 849                        ptext SLIT("is a type")]
 850
 851 appKindCtxt :: SDoc -> Message
 852 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
 853
 854 wrongThingErr expected actual name
 855   = pp_actual actual <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
 856   where
 857     pp_actual (ATyCon _) = ptext SLIT("Type constructor")
 858     pp_actual (AClass _) = ptext SLIT("Class")
 859     pp_actual (ATyVar _) = ptext SLIT("Type variable")
 860     pp_actual (AThing _) = ptext SLIT("Utterly bogus")
 861
 862 ambigErr pred ty
 863   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
 864          nest 4 (ptext SLIT("for the type:") <+> ppr ty),
 865          nest 4 (ptext SLIT("Each forall'd type variable mentioned by the constraint must appear after the =>"))]
 866
 867 freeErr pred ty
 868   = sep [ptext SLIT("The constraint") <+> quotes (pprPred pred) <+>
 869                    ptext SLIT("does not mention any of the universally quantified type variables"),
 870          nest 4 (ptext SLIT("in the type") <+> quotes (ppr ty))
 871     ]
 872 \end{code}