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