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