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