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