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