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