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