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