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