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