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