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, tcHsTcType, tcHsTypeKind, tcContext,
   8                     tcTyVarScope,
   9                     TcSigInfo(..), tcTySig, mkTcSig, noSigs, maybeSig,
  10                     checkSigTyVars, sigCtxt, existentialPatCtxt
  11                   ) where
  12
  13 #include "HsVersions.h"
  14
  15 import HsSyn            ( HsType(..), HsTyVar(..), Sig(..), pprContext )
  16 import RnHsSyn          ( RenamedHsType, RenamedContext, RenamedSig )
  17 import TcHsSyn          ( TcIdBndr, TcIdOcc(..) )
  18
  19 import TcMonad
  20 import TcEnv            ( tcLookupTyVar, tcLookupClass, tcLookupTyCon, tcExtendTyVarEnv,
  21                           tcGetGlobalTyVars, tidyTypes, tidyTyVar
  22                         )
  23 import TcType           ( TcType, TcKind, TcTyVar, TcThetaType, TcTauType,
  24                           typeToTcType, tcInstTcType, kindToTcKind,
  25                           newKindVar,
  26                           zonkTcKindToKind, zonkTcTyVars, zonkTcType
  27                         )
  28 import Inst             ( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr )
  29 import TcUnify          ( unifyKind, unifyKinds )
  30 import Type             ( Type, ThetaType,
  31                           mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy,
  32                           mkSigmaTy, mkDictTy, mkTyConApp, mkAppTys, splitRhoTy,
  33                           boxedTypeKind, unboxedTypeKind, openTypeKind,
  34                           mkArrowKind, getTyVar_maybe, getTyVar
  35                         )
  36 import Id               ( mkUserId, idName, idType, idFreeTyVars )
  37 import Var              ( TyVar, mkTyVar )
  38 import VarEnv
  39 import VarSet
  40 import Bag              ( bagToList )
  41 import PrelInfo         ( cCallishClassKeys )
  42 import TyCon            ( TyCon )
  43 import Name             ( Name, OccName, isTvOcc, getOccName )
  44 import TysWiredIn       ( mkListTy, mkTupleTy, mkUnboxedTupleTy )
  45 import SrcLoc           ( SrcLoc )
  46 import Unique           ( Unique, Uniquable(..) )
  47 import Util             ( zipWithEqual, zipLazy, mapAccumL )
  48 import Outputable
  49 \end{code}
  50
  51
  52 %************************************************************************
  53 %*                                                                      *
  54 \subsection{Checking types}
  55 %*                                                                      *
  56 %************************************************************************
  57
  58 tcHsType and tcHsTypeKind
  59 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  60
  61 tcHsType checks that the type really is of kind Type!
  62
  63 \begin{code}
  64 tcHsType :: RenamedHsType -> TcM s Type
  65 tcHsType ty
  66   = tcAddErrCtxt (typeCtxt ty)          $
  67     tc_hs_type ty
  68
  69 -- Version for when we need a TcType returned
  70 tcHsTcType :: RenamedHsType -> TcM s (TcType s)
  71 tcHsTcType ty
  72   = tcHsType ty         `thenTc` \ ty' ->
  73     returnTc (typeToTcType ty')
  74
  75 tc_hs_type ty
  76   = tc_hs_type_kind ty                  `thenTc` \ (kind,ty) ->
  77         -- Check that it really is a type
  78     unifyKind openTypeKind kind         `thenTc_`
  79     returnTc ty
  80 \end{code}
  81
  82 tcHsTypeKind does the real work.  It returns a kind and a type.
  83
  84 \begin{code}
  85 tcHsTypeKind :: RenamedHsType -> TcM s (TcKind s, Type)
  86
  87 tcHsTypeKind ty
  88   = tcAddErrCtxt (typeCtxt ty)          $
  89     tc_hs_type_kind ty
  90
  91
  92         -- This equation isn't needed (the next one would handle it fine)
  93         -- but it's rather a common case, so we handle it directly
  94 tc_hs_type_kind (MonoTyVar name)
  95   | isTvOcc (getOccName name)
  96   = tcLookupTyVar name                  `thenNF_Tc` \ (kind,tyvar) ->
  97     returnTc (kind, mkTyVarTy tyvar)
  98
  99 tc_hs_type_kind ty@(MonoTyVar name)
 100   = tcFunType ty []
 101
 102 tc_hs_type_kind (MonoListTy ty)
 103   = tc_hs_type ty       `thenTc` \ tau_ty ->
 104     returnTc (boxedTypeKind, mkListTy tau_ty)
 105
 106 tc_hs_type_kind (MonoTupleTy tys True{-boxed-})
 107   = mapTc tc_hs_type  tys       `thenTc` \ tau_tys ->
 108     returnTc (boxedTypeKind, mkTupleTy (length tys) tau_tys)
 109
 110 tc_hs_type_kind (MonoTupleTy tys False{-unboxed-})
 111   = mapTc tc_hs_type  tys       `thenTc` \ tau_tys ->
 112     returnTc (unboxedTypeKind, mkUnboxedTupleTy (length tys) tau_tys)
 113
 114 tc_hs_type_kind (MonoFunTy ty1 ty2)
 115   = tc_hs_type ty1      `thenTc` \ tau_ty1 ->
 116     tc_hs_type ty2      `thenTc` \ tau_ty2 ->
 117     returnTc (boxedTypeKind, mkFunTy tau_ty1 tau_ty2)
 118
 119 tc_hs_type_kind (MonoTyApp ty1 ty2)
 120   = tcTyApp ty1 [ty2]
 121
 122 tc_hs_type_kind (HsForAllTy tv_names context ty)
 123   = tcTyVarScope tv_names                       $ \ tyvars ->
 124         tcContext context                       `thenTc` \ theta ->
 125         tc_hs_type ty                           `thenTc` \ tau ->
 126                 -- For-all's are of kind type!
 127         returnTc (boxedTypeKind, mkSigmaTy tyvars theta tau)
 128
 129 -- for unfoldings, and instance decls, only:
 130 tc_hs_type_kind (MonoDictTy class_name tys)
 131   = tcClassAssertion (class_name, tys)  `thenTc` \ (clas, arg_tys) ->
 132     returnTc (boxedTypeKind, mkDictTy clas arg_tys)
 133 \end{code}
 134
 135 Help functions for type applications
 136 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 137 \begin{code}
 138 tcTyApp (MonoTyApp ty1 ty2) tys
 139   = tcTyApp ty1 (ty2:tys)
 140
 141 tcTyApp ty tys
 142   | null tys
 143   = tcFunType ty []
 144
 145   | otherwise
 146   = mapAndUnzipTc tc_hs_type_kind tys   `thenTc` \ (arg_kinds, arg_tys) ->
 147     tcFunType ty arg_tys                `thenTc` \ (fun_kind, result_ty) ->
 148
 149         -- Check argument compatibility
 150     newKindVar                          `thenNF_Tc` \ result_kind ->
 151     unifyKind fun_kind (foldr mkArrowKind result_kind arg_kinds)
 152                                         `thenTc_`
 153     returnTc (result_kind, result_ty)
 154
 155 -- (tcFunType ty arg_tys) returns (kind-of ty, mkAppTys ty arg_tys)
 156 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
 157 --      hence the rather strange functionality.
 158
 159 tcFunType (MonoTyVar name) arg_tys
 160   | isTvOcc (getOccName name)   -- Must be a type variable
 161   = tcLookupTyVar name                  `thenNF_Tc` \ (kind,tyvar) ->
 162     returnTc (kind, mkAppTys (mkTyVarTy tyvar) arg_tys)
 163
 164   | otherwise                   -- Must be a type constructor
 165   = tcLookupTyCon name                  `thenTc` \ (tycon_kind,maybe_arity, tycon) ->
 166     case maybe_arity of
 167         Nothing    ->   -- Data type or newtype
 168                       returnTc (tycon_kind, mkTyConApp tycon arg_tys)
 169
 170         Just arity ->   -- Type synonym
 171                       checkTc (arity <= n_args) err_msg `thenTc_`
 172                       returnTc (tycon_kind, result_ty)
 173                    where
 174                         -- It's OK to have an *over-applied* type synonym
 175                         --      data Tree a b = ...
 176                         --      type Foo a = Tree [a]
 177                         --      f :: Foo a b -> ...
 178                       result_ty = mkAppTys (mkSynTy tycon (take arity arg_tys))
 179                                            (drop arity arg_tys)
 180                       err_msg = arityErr "Type synonym constructor" name arity n_args
 181                       n_args  = length arg_tys
 182
 183 tcFunType ty arg_tys
 184   = tc_hs_type_kind ty          `thenTc` \ (fun_kind, fun_ty) ->
 185     returnTc (fun_kind, mkAppTys fun_ty arg_tys)
 186 \end{code}
 187
 188
 189 Contexts
 190 ~~~~~~~~
 191 \begin{code}
 192
 193 tcContext :: RenamedContext -> TcM s ThetaType
 194 tcContext context
 195   = tcAddErrCtxt (thetaCtxt context) $
 196
 197         --Someone discovered that @CCallable@ and @CReturnable@
 198         -- could be used in contexts such as:
 199         --      foo :: CCallable a => a -> PrimIO Int
 200         -- Doing this utterly wrecks the whole point of introducing these
 201         -- classes so we specifically check that this isn't being done.
 202         --
 203         -- We *don't* do this check in tcClassAssertion, because that's
 204         -- called when checking a HsDictTy, and we don't want to reject
 205         --      instance CCallable Int
 206         -- etc. Ugh!
 207     mapTc check_naughty context `thenTc_`
 208
 209     mapTc tcClassAssertion context
 210
 211  where
 212    check_naughty (class_name, _)
 213      = checkTc (not (getUnique class_name `elem` cCallishClassKeys))
 214                (naughtyCCallContextErr class_name)
 215
 216 tcClassAssertion (class_name, tys)
 217   = tcLookupClass class_name            `thenTc` \ (class_kinds, clas) ->
 218     mapAndUnzipTc tc_hs_type_kind tys   `thenTc` \ (ty_kinds, tc_tys) ->
 219
 220         -- Check with kind mis-match
 221     let
 222         arity = length class_kinds
 223         n_tys = length ty_kinds
 224         err   = arityErr "Class" class_name arity n_tys
 225     in
 226     checkTc (arity == n_tys) err        `thenTc_`
 227     unifyKinds class_kinds ty_kinds     `thenTc_`
 228
 229     returnTc (clas, tc_tys)
 230 \end{code}
 231
 232
 233 %************************************************************************
 234 %*                                                                      *
 235 \subsection{Type variables, with knot tying!}
 236 %*                                                                      *
 237 %************************************************************************
 238
 239 \begin{code}
 240 tcTyVarScope
 241         :: [HsTyVar Name]               -- Names of some type variables
 242         -> ([TyVar] -> TcM s a)         -- Thing to type check in their scope
 243         -> TcM s a                      -- Result
 244
 245 tcTyVarScope tyvar_names thing_inside
 246   = mapAndUnzipNF_Tc tcHsTyVar tyvar_names      `thenNF_Tc` \ (names, kinds) ->
 247
 248     fixTc (\ ~(rec_tyvars, _) ->
 249                 -- Ok to look at names, kinds, but not tyvars!
 250
 251         tcExtendTyVarEnv names (kinds `zipLazy` rec_tyvars)
 252                          (thing_inside rec_tyvars)              `thenTc` \ result ->
 253
 254                 -- Get the tyvar's Kinds from their TcKinds
 255         mapNF_Tc zonkTcKindToKind kinds                         `thenNF_Tc` \ kinds' ->
 256
 257                 -- Construct the real TyVars
 258         let
 259           tyvars = zipWithEqual "tcTyVarScope" mkTyVar names kinds'
 260         in
 261         returnTc (tyvars, result)
 262     )                                   `thenTc` \ (_,result) ->
 263     returnTc result
 264
 265 tcHsTyVar (UserTyVar name)
 266   = newKindVar          `thenNF_Tc` \ tc_kind ->
 267     returnNF_Tc (name, tc_kind)
 268 tcHsTyVar (IfaceTyVar name kind)
 269   = returnNF_Tc (name, kindToTcKind kind)
 270 \end{code}
 271
 272
 273 %************************************************************************
 274 %*                                                                      *
 275 \subsection{Signatures}
 276 %*                                                                      *
 277 %************************************************************************
 278
 279 @tcSigs@ checks the signatures for validity, and returns a list of
 280 {\em freshly-instantiated} signatures.  That is, the types are already
 281 split up, and have fresh type variables installed.  All non-type-signature
 282 "RenamedSigs" are ignored.
 283
 284 The @TcSigInfo@ contains @TcTypes@ because they are unified with
 285 the variable's type, and after that checked to see whether they've
 286 been instantiated.
 287
 288 \begin{code}
 289 data TcSigInfo s
 290   = TySigInfo
 291         Name                    -- N, the Name in corresponding binding
 292
 293         (TcIdBndr s)            -- *Polymorphic* binder for this value...
 294                                 -- Has name = N
 295
 296         [TcTyVar s]             -- tyvars
 297         (TcThetaType s)         -- theta
 298         (TcTauType s)           -- tau
 299
 300         (TcIdBndr s)            -- *Monomorphic* binder for this value
 301                                 -- Does *not* have name = N
 302                                 -- Has type tau
 303
 304         (Inst s)                -- Empty if theta is null, or
 305                                 -- (method mono_id) otherwise
 306
 307         SrcLoc                  -- Of the signature
 308
 309
 310 maybeSig :: [TcSigInfo s] -> Name -> Maybe (TcSigInfo s)
 311         -- Search for a particular signature
 312 maybeSig [] name = Nothing
 313 maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
 314   | name == sig_name = Just sig
 315   | otherwise        = maybeSig sigs name
 316
 317 -- This little helper is useful to pass to tcPat
 318 noSigs :: Name -> Maybe (TcIdBndr s)
 319 noSigs name = Nothing
 320 \end{code}
 321
 322
 323 \begin{code}
 324 tcTySig :: RenamedSig
 325         -> TcM s (TcSigInfo s)
 326
 327 tcTySig (Sig v ty src_loc)
 328  = tcAddSrcLoc src_loc $
 329    tcHsTcType ty                                `thenTc` \ sigma_tc_ty ->
 330    mkTcSig (mkUserId v sigma_tc_ty) src_loc     `thenNF_Tc` \ sig ->
 331    returnTc sig
 332
 333 mkTcSig :: TcIdBndr s -> SrcLoc -> NF_TcM s (TcSigInfo s)
 334 mkTcSig poly_id src_loc
 335   =     -- Instantiate this type
 336         -- It's important to do this even though in the error-free case
 337         -- we could just split the sigma_tc_ty (since the tyvars don't
 338         -- unified with anything).  But in the case of an error, when
 339         -- the tyvars *do* get unified with something, we want to carry on
 340         -- typechecking the rest of the program with the function bound
 341         -- to a pristine type, namely sigma_tc_ty
 342    tcInstTcType (idType poly_id)                `thenNF_Tc` \ (tyvars, rho) ->
 343    let
 344      (theta, tau) = splitRhoTy rho
 345         -- This splitSigmaTy tries hard to make sure that tau' is a type synonym
 346         -- wherever possible, which can improve interface files.
 347    in
 348    newMethodWithGivenTy SignatureOrigin
 349                 (TcId poly_id)
 350                 (mkTyVarTys tyvars)
 351                 theta tau                       `thenNF_Tc` \ inst ->
 352         -- We make a Method even if it's not overloaded; no harm
 353
 354    returnNF_Tc (TySigInfo name poly_id tyvars theta tau (instToIdBndr inst) inst src_loc)
 355   where
 356     name = idName poly_id
 357 \end{code}
 358
 359
 360
 361 %************************************************************************
 362 %*                                                                      *
 363 \subsection{Checking signature type variables}
 364 %*                                                                      *
 365 %************************************************************************
 366
 367 @checkSigTyVars@ is used after the type in a type signature has been unified with
 368 the actual type found.  It then checks that the type variables of the type signature
 369 are
 370         (a) still all type variables
 371                 eg matching signature [a] against inferred type [(p,q)]
 372                 [then a will be unified to a non-type variable]
 373
 374         (b) still all distinct
 375                 eg matching signature [(a,b)] against inferred type [(p,p)]
 376                 [then a and b will be unified together]
 377
 378         (c) not mentioned in the environment
 379                 eg the signature for f in this:
 380
 381                         g x = ... where
 382                                         f :: a->[a]
 383                                         f y = [x,y]
 384
 385                 Here, f is forced to be monorphic by the free occurence of x.
 386
 387 Before doing this, the substitution is applied to the signature type variable.
 388
 389 We used to have the notion of a "DontBind" type variable, which would
 390 only be bound to itself or nothing.  Then points (a) and (b) were
 391 self-checking.  But it gave rise to bogus consequential error messages.
 392 For example:
 393
 394    f = (*)      -- Monomorphic
 395
 396    g :: Num a => a -> a
 397    g x = f x x
 398
 399 Here, we get a complaint when checking the type signature for g,
 400 that g isn't polymorphic enough; but then we get another one when
 401 dealing with the (Num x) context arising from f's definition;
 402 we try to unify x with Int (to default it), but find that x has already
 403 been unified with the DontBind variable "a" from g's signature.
 404 This is really a problem with side-effecting unification; we'd like to
 405 undo g's effects when its type signature fails, but unification is done
 406 by side effect, so we can't (easily).
 407
 408 So we revert to ordinary type variables for signatures, and try to
 409 give a helpful message in checkSigTyVars.
 410
 411 \begin{code}
 412 checkSigTyVars :: [TcTyVar s]           -- The original signature type variables
 413                -> TcM s [TcTyVar s]     -- Zonked signature type variables
 414
 415 checkSigTyVars [] = returnTc []
 416
 417 checkSigTyVars sig_tyvars
 418   = zonkTcTyVars sig_tyvars             `thenNF_Tc` \ sig_tys ->
 419     tcGetGlobalTyVars                   `thenNF_Tc` \ globals ->
 420     checkTcM (all_ok sig_tys globals)
 421              (complain sig_tys globals) `thenTc_`
 422
 423     returnTc (map (getTyVar "checkSigTyVars") sig_tys)
 424
 425   where
 426     all_ok []       acc = True
 427     all_ok (ty:tys) acc = case getTyVar_maybe ty of
 428                             Nothing                       -> False      -- Point (a)
 429                             Just tv | tv `elemVarSet` acc -> False      -- Point (b) or (c)
 430                                     | otherwise           -> all_ok tys (acc `extendVarSet` tv)
 431
 432
 433     complain sig_tys globals
 434       = failWithTcM (env2, main_msg)
 435       where
 436         (env1, tidy_tys) = tidyTypes emptyTidyEnv sig_tys
 437         (env2, tidy_tvs) = mapAccumL tidyTyVar env1 sig_tyvars
 438
 439         msgs = check (tidy_tvs `zip` tidy_tys) emptyVarEnv
 440
 441         main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
 442                    $$
 443                    nest 4 (vcat msgs)
 444
 445         check [] acc = []
 446         check ((sig_tyvar,ty):prs) acc
 447           = case getTyVar_maybe ty of
 448               Nothing                           -- Error (a)!
 449                 -> unify_msg sig_tyvar (ppr ty) : check prs acc
 450
 451               Just tv
 452                 | tv `elemVarSet` globals       -- Error (c)! Type variable escapes
 453                 -> escape_msg tv : check prs acc
 454
 455                 | otherwise
 456                 -> case lookupVarEnv acc tv of
 457                         Nothing                 -- All OK
 458                                 -> check prs (extendVarEnv acc tv sig_tyvar)    -- All OK
 459                         Just sig_tyvar'         -- Error (b)!
 460                                 -> unify_msg sig_tyvar (ppr sig_tyvar') : check prs acc
 461
 462
 463 escape_msg tv      = mk_msg tv <+> ptext SLIT("escapes; i.e. unifies with something more global")
 464 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> quotes thing
 465 mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
 466 \end{code}
 467
 468 These two context are used with checkSigTyVars
 469
 470 \begin{code}
 471 sigCtxt thing sig_tau tidy_env
 472   = zonkTcType sig_tau  `thenNF_Tc` \ zonked_sig_tau ->
 473     let
 474         (env1, [tidy_tau, tidy_zonked_tau]) = tidyTypes tidy_env [sig_tau, zonked_sig_tau]
 475
 476         msg = vcat [ptext SLIT("When checking the type signature for") <+> thing,
 477                     nest 4 (ptext SLIT("Signature:") <+> ppr tidy_tau),
 478                     nest 4 (ptext SLIT("Inferred: ") <+> ppr tidy_zonked_tau)]
 479     in
 480     returnNF_Tc (env1, msg)
 481
 482 existentialPatCtxt bound_tvs bound_ids tidy_env
 483   = returnNF_Tc (env1,
 484                  sep [ptext SLIT("When checking an existential pattern that binds"),
 485                       nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
 486   where
 487     tv_list  = bagToList bound_tvs
 488     show_ids = filter is_interesting (map snd (bagToList bound_ids))
 489     is_interesting id = any (`elemVarSet` idFreeTyVars id) tv_list
 490
 491     (env1, tidy_tys) = tidyTypes tidy_env (map idType show_ids)
 492     ppr_id id ty     = ppr id <+> ptext SLIT("::") <+> ppr ty
 493         -- Don't zonk the types so we get the separate, un-unified versions
 494 \end{code}
 495
 496
 497 %************************************************************************
 498 %*                                                                      *
 499 \subsection{Errors and contexts}
 500 %*                                                                      *
 501 %************************************************************************
 502
 503 \begin{code}
 504 naughtyCCallContextErr clas_name
 505   = sep [ptext SLIT("Can't use class"), quotes (ppr clas_name), ptext SLIT("in a context")]
 506
 507 typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
 508
 509 thetaCtxt theta = ptext SLIT("In the context") <+> quotes (pprContext theta)
 510 \end{code}