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