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