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