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