ghc/compiler/typecheck/TcMType.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section{Monadic type operations}
   5
   6 This module contains monadic operations over types that contain mutable type variables
   7
   8 \begin{code}
   9 module TcMType (
  10   TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
  11
  12   --------------------------------
  13   -- Creating new mutable type variables
  14   newTyVar, newHoleTyVarTy,
  15   newTyVarTy,           -- Kind -> NF_TcM TcType
  16   newTyVarTys,          -- Int -> Kind -> NF_TcM [TcType]
  17   newKindVar, newKindVars, newBoxityVar,
  18   putTcTyVar, getTcTyVar,
  19
  20   --------------------------------
  21   -- Instantiation
  22   tcInstTyVar, tcInstTyVars,
  23   tcInstSigTyVars, tcInstType,
  24   tcSplitRhoTyM,
  25
  26   --------------------------------
  27   -- Checking type validity
  28   Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
  29   SourceTyCtxt(..), checkValidTheta,
  30   checkValidInstHead, instTypeErr,
  31
  32   --------------------------------
  33   -- Zonking
  34   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars,
  35   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
  36   zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,
  37
  38   ) where
  39
  40 #include "HsVersions.h"
  41
  42
  43 -- friends:
  44 import TypeRep          ( Type(..), SourceType(..), TyNote(..),  -- Friend; can see representation
  45                           Kind, ThetaType
  46                         )
  47 import TcType           ( TcType, TcThetaType, TcTauType, TcPredType,
  48                           TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
  49                           tcEqType, tcCmpPred,
  50                           tcSplitRhoTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
  51                           tcSplitTyConApp_maybe, tcSplitForAllTys,
  52                           tcGetTyVar, tcIsTyVarTy, tcSplitSigmaTy,
  53                           isUnLiftedType, isIPPred,
  54
  55                           mkAppTy, mkTyVarTy, mkTyVarTys,
  56                           tyVarsOfPred, getClassPredTys_maybe,
  57
  58                           liftedTypeKind, openTypeKind, defaultKind, superKind,
  59                           superBoxity, liftedBoxity, typeKind,
  60                           tyVarsOfType, tyVarsOfTypes,
  61                           eqKind, isTypeKind,
  62
  63                           isFFIArgumentTy, isFFIImportResultTy
  64                         )
  65 import Subst            ( Subst, mkTopTyVarSubst, substTy )
  66 import Class            ( classArity, className )
  67 import TyCon            ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon,
  68                           tyConArity, tyConName )
  69 import PrimRep          ( PrimRep(VoidRep) )
  70 import Var              ( TyVar, tyVarKind, tyVarName, isTyVar, mkTyVar, isMutTyVar )
  71
  72 -- others:
  73 import TcMonad          -- TcType, amongst others
  74 import TysWiredIn       ( voidTy )
  75 import PrelNames        ( cCallableClassKey, cReturnableClassKey, hasKey )
  76 import ForeignCall      ( Safety(..) )
  77 import FunDeps          ( grow )
  78 import PprType          ( pprPred, pprSourceType, pprTheta, pprClassPred )
  79 import Name             ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
  80                           mkLocalName, mkDerivedTyConOcc
  81                         )
  82 import VarSet
  83 import CmdLineOpts      ( dopt, DynFlag(..) )
  84 import Unique           ( Uniquable(..) )
  85 import SrcLoc           ( noSrcLoc )
  86 import Util             ( nOfThem, isSingleton, equalLength )
  87 import ListSetOps       ( removeDups )
  88 import Outputable
  89 \end{code}
  90
  91
  92 %************************************************************************
  93 %*                                                                      *
  94 \subsection{New type variables}
  95 %*                                                                      *
  96 %************************************************************************
  97
  98 \begin{code}
  99 newTyVar :: Kind -> NF_TcM TcTyVar
 100 newTyVar kind
 101   = tcGetUnique         `thenNF_Tc` \ uniq ->
 102     tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind VanillaTv
 103
 104 newTyVarTy  :: Kind -> NF_TcM TcType
 105 newTyVarTy kind
 106   = newTyVar kind       `thenNF_Tc` \ tc_tyvar ->
 107     returnNF_Tc (TyVarTy tc_tyvar)
 108
 109 newHoleTyVarTy :: NF_TcM TcType
 110   = tcGetUnique         `thenNF_Tc` \ uniq ->
 111     tcNewMutTyVar (mkSysLocalName uniq SLIT("h")) openTypeKind HoleTv   `thenNF_Tc` \ tv ->
 112     returnNF_Tc (TyVarTy tv)
 113
 114 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
 115 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
 116
 117 newKindVar :: NF_TcM TcKind
 118 newKindVar
 119   = tcGetUnique                                                         `thenNF_Tc` \ uniq ->
 120     tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind VanillaTv   `thenNF_Tc` \ kv ->
 121     returnNF_Tc (TyVarTy kv)
 122
 123 newKindVars :: Int -> NF_TcM [TcKind]
 124 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
 125
 126 newBoxityVar :: NF_TcM TcKind
 127 newBoxityVar
 128   = tcGetUnique                                                           `thenNF_Tc` \ uniq ->
 129     tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity VanillaTv  `thenNF_Tc` \ kv ->
 130     returnNF_Tc (TyVarTy kv)
 131 \end{code}
 132
 133
 134 %************************************************************************
 135 %*                                                                      *
 136 \subsection{Type instantiation}
 137 %*                                                                      *
 138 %************************************************************************
 139
 140 I don't understand why this is needed
 141 An old comments says "No need for tcSplitForAllTyM because a type
 142         variable can't be instantiated to a for-all type"
 143 But the same is true of rho types!
 144
 145 \begin{code}
 146 tcSplitRhoTyM :: TcType -> NF_TcM (TcThetaType, TcType)
 147 tcSplitRhoTyM t
 148   = go t t []
 149  where
 150         -- A type variable is never instantiated to a dictionary type,
 151         -- so we don't need to do a tcReadVar on the "arg".
 152     go syn_t (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
 153                                         Just pair -> go res res (pair:ts)
 154                                         Nothing   -> returnNF_Tc (reverse ts, syn_t)
 155     go syn_t (NoteTy n t)    ts = go syn_t t ts
 156     go syn_t (TyVarTy tv)    ts = getTcTyVar tv         `thenNF_Tc` \ maybe_ty ->
 157                                   case maybe_ty of
 158                                     Just ty | not (tcIsTyVarTy ty) -> go syn_t ty ts
 159                                     other                          -> returnNF_Tc (reverse ts, syn_t)
 160     go syn_t (UsageTy _ t)   ts = go syn_t t ts
 161     go syn_t t               ts = returnNF_Tc (reverse ts, syn_t)
 162 \end{code}
 163
 164
 165 %************************************************************************
 166 %*                                                                      *
 167 \subsection{Type instantiation}
 168 %*                                                                      *
 169 %************************************************************************
 170
 171 Instantiating a bunch of type variables
 172
 173 \begin{code}
 174 tcInstTyVars :: [TyVar]
 175              -> NF_TcM ([TcTyVar], [TcType], Subst)
 176
 177 tcInstTyVars tyvars
 178   = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
 179     let
 180         tys = mkTyVarTys tc_tyvars
 181     in
 182     returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
 183                 -- Since the tyvars are freshly made,
 184                 -- they cannot possibly be captured by
 185                 -- any existing for-alls.  Hence mkTopTyVarSubst
 186
 187 tcInstTyVar tyvar
 188   = tcGetUnique                 `thenNF_Tc` \ uniq ->
 189     let
 190         name = setNameUnique (tyVarName tyvar) uniq
 191         -- Note that we don't change the print-name
 192         -- This won't confuse the type checker but there's a chance
 193         -- that two different tyvars will print the same way
 194         -- in an error message.  -dppr-debug will show up the difference
 195         -- Better watch out for this.  If worst comes to worst, just
 196         -- use mkSysLocalName.
 197     in
 198     tcNewMutTyVar name (tyVarKind tyvar) VanillaTv
 199
 200 tcInstSigTyVars :: TyVarDetails -> [TyVar] -> NF_TcM [TcTyVar]
 201 tcInstSigTyVars details tyvars  -- Very similar to tcInstTyVar
 202   = tcGetUniques        `thenNF_Tc` \ uniqs ->
 203     listTc [ ASSERT( not (kind `eqKind` openTypeKind) ) -- Shouldn't happen
 204              tcNewMutTyVar name kind details
 205            | (tyvar, uniq) <- tyvars `zip` uniqs,
 206              let name = setNameUnique (tyVarName tyvar) uniq,
 207              let kind = tyVarKind tyvar
 208            ]
 209 \end{code}
 210
 211 @tcInstType@ instantiates the outer-level for-alls of a TcType with
 212 fresh type variables, splits off the dictionary part, and returns the results.
 213
 214 \begin{code}
 215 tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
 216 tcInstType ty
 217   = case tcSplitForAllTys ty of
 218         ([],     rho) ->        -- There may be overloading but no type variables;
 219                                 --      (?x :: Int) => Int -> Int
 220                          let
 221                            (theta, tau) = tcSplitRhoTy rho      -- Used to be tcSplitRhoTyM
 222                          in
 223                          returnNF_Tc ([], theta, tau)
 224
 225         (tyvars, rho) -> tcInstTyVars tyvars                    `thenNF_Tc` \ (tyvars', _, tenv)  ->
 226                          let
 227                            (theta, tau) = tcSplitRhoTy (substTy tenv rho)       -- Used to be tcSplitRhoTyM
 228                          in
 229                          returnNF_Tc (tyvars', theta, tau)
 230 \end{code}
 231
 232
 233
 234 %************************************************************************
 235 %*                                                                      *
 236 \subsection{Putting and getting  mutable type variables}
 237 %*                                                                      *
 238 %************************************************************************
 239
 240 \begin{code}
 241 putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
 242 getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
 243 \end{code}
 244
 245 Putting is easy:
 246
 247 \begin{code}
 248 putTcTyVar tyvar ty
 249   | not (isMutTyVar tyvar)
 250   = pprTrace "putTcTyVar" (ppr tyvar) $
 251     returnNF_Tc ty
 252
 253   | otherwise
 254   = ASSERT( isMutTyVar tyvar )
 255     UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
 256     tcWriteMutTyVar tyvar (Just ty)     `thenNF_Tc_`
 257     returnNF_Tc ty
 258 \end{code}
 259
 260 Getting is more interesting.  The easy thing to do is just to read, thus:
 261
 262 \begin{verbatim}
 263 getTcTyVar tyvar = tcReadMutTyVar tyvar
 264 \end{verbatim}
 265
 266 But it's more fun to short out indirections on the way: If this
 267 version returns a TyVar, then that TyVar is unbound.  If it returns
 268 any other type, then there might be bound TyVars embedded inside it.
 269
 270 We return Nothing iff the original box was unbound.
 271
 272 \begin{code}
 273 getTcTyVar tyvar
 274   | not (isMutTyVar tyvar)
 275   = pprTrace "getTcTyVar" (ppr tyvar) $
 276     returnNF_Tc (Just (mkTyVarTy tyvar))
 277
 278   | otherwise
 279   = ASSERT2( isMutTyVar tyvar, ppr tyvar )
 280     tcReadMutTyVar tyvar                                `thenNF_Tc` \ maybe_ty ->
 281     case maybe_ty of
 282         Just ty -> short_out ty                         `thenNF_Tc` \ ty' ->
 283                    tcWriteMutTyVar tyvar (Just ty')     `thenNF_Tc_`
 284                    returnNF_Tc (Just ty')
 285
 286         Nothing    -> returnNF_Tc Nothing
 287
 288 short_out :: TcType -> NF_TcM TcType
 289 short_out ty@(TyVarTy tyvar)
 290   | not (isMutTyVar tyvar)
 291   = returnNF_Tc ty
 292
 293   | otherwise
 294   = tcReadMutTyVar tyvar        `thenNF_Tc` \ maybe_ty ->
 295     case maybe_ty of
 296         Just ty' -> short_out ty'                       `thenNF_Tc` \ ty' ->
 297                     tcWriteMutTyVar tyvar (Just ty')    `thenNF_Tc_`
 298                     returnNF_Tc ty'
 299
 300         other    -> returnNF_Tc ty
 301
 302 short_out other_ty = returnNF_Tc other_ty
 303 \end{code}
 304
 305
 306 %************************************************************************
 307 %*                                                                      *
 308 \subsection{Zonking -- the exernal interfaces}
 309 %*                                                                      *
 310 %************************************************************************
 311
 312 -----------------  Type variables
 313
 314 \begin{code}
 315 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
 316 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
 317
 318 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
 319 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars  `thenNF_Tc` \ tys ->
 320                            returnNF_Tc (tyVarsOfTypes tys)
 321
 322 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
 323 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
 324
 325 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
 326 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
 327 -- Usually this job is done by checkSigTyVars, but in a couple of places
 328 -- that is overkill, so we use this simpler chap
 329 zonkTcSigTyVars tyvars
 330   = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
 331     returnNF_Tc (map (tcGetTyVar "zonkTcSigTyVars") tys)
 332 \end{code}
 333
 334 -----------------  Types
 335
 336 \begin{code}
 337 zonkTcType :: TcType -> NF_TcM TcType
 338 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
 339
 340 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
 341 zonkTcTypes tys = mapNF_Tc zonkTcType tys
 342
 343 zonkTcClassConstraints cts = mapNF_Tc zonk cts
 344     where zonk (clas, tys)
 345             = zonkTcTypes tys   `thenNF_Tc` \ new_tys ->
 346               returnNF_Tc (clas, new_tys)
 347
 348 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
 349 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
 350
 351 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
 352 zonkTcPredType (ClassP c ts)
 353   = zonkTcTypes ts      `thenNF_Tc` \ new_ts ->
 354     returnNF_Tc (ClassP c new_ts)
 355 zonkTcPredType (IParam n t)
 356   = zonkTcType t        `thenNF_Tc` \ new_t ->
 357     returnNF_Tc (IParam n new_t)
 358 \end{code}
 359
 360 -------------------  These ...ToType, ...ToKind versions
 361                      are used at the end of type checking
 362
 363 \begin{code}
 364 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
 365 zonkKindEnv pairs
 366   = mapNF_Tc zonk_it pairs
 367  where
 368     zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
 369                               returnNF_Tc (name, kind)
 370
 371         -- When zonking a kind, we want to
 372         --      zonk a *kind* variable to (Type *)
 373         --      zonk a *boxity* variable to *
 374     zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind   = putTcTyVar kv liftedTypeKind
 375                              | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
 376                              | otherwise                         = pprPanic "zonkKindEnv" (ppr kv)
 377
 378 zonkTcTypeToType :: TcType -> NF_TcM Type
 379 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
 380   where
 381         -- Zonk a mutable but unbound type variable to
 382         --      Void            if it has kind Lifted
 383         --      :Void           otherwise
 384         -- We know it's unbound even though we don't carry an environment,
 385         -- because at the binding site for a type variable we bind the
 386         -- mutable tyvar to a fresh immutable one.  So the mutable store
 387         -- plays the role of an environment.  If we come across a mutable
 388         -- type variable that isn't so bound, it must be completely free.
 389     zonk_unbound_tyvar tv
 390         | kind `eqKind` liftedTypeKind || kind `eqKind` openTypeKind
 391         = putTcTyVar tv voidTy  -- Just to avoid creating a new tycon in
 392                                 -- this vastly common case
 393         | otherwise
 394         = putTcTyVar tv (TyConApp (mk_void_tycon tv kind) [])
 395         where
 396           kind = tyVarKind tv
 397
 398     mk_void_tycon tv kind       -- Make a new TyCon with the same kind as the
 399                                 -- type variable tv.  Same name too, apart from
 400                                 -- making it start with a colon (sigh)
 401                 -- I dread to think what will happen if this gets out into an
 402                 -- interface file.  Catastrophe likely.  Major sigh.
 403         = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
 404           mkPrimTyCon tc_name kind 0 [] VoidRep
 405         where
 406           tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
 407
 408 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
 409 -- of a type variable, at the *end* of type checking.  It changes
 410 -- the *mutable* type variable into an *immutable* one.
 411 --
 412 -- It does this by making an immutable version of tv and binds tv to it.
 413 -- Now any bound occurences of the original type variable will get
 414 -- zonked to the immutable version.
 415
 416 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
 417 zonkTcTyVarToTyVar tv
 418   = let
 419                 -- Make an immutable version, defaulting
 420                 -- the kind to lifted if necessary
 421         immut_tv    = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
 422         immut_tv_ty = mkTyVarTy immut_tv
 423
 424         zap tv = putTcTyVar tv immut_tv_ty
 425                 -- Bind the mutable version to the immutable one
 426     in
 427         -- If the type variable is mutable, then bind it to immut_tv_ty
 428         -- so that all other occurrences of the tyvar will get zapped too
 429     zonkTyVar zap tv            `thenNF_Tc` \ ty2 ->
 430
 431     WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
 432
 433     returnNF_Tc immut_tv
 434 \end{code}
 435
 436
 437 %************************************************************************
 438 %*                                                                      *
 439 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
 440 %*                                                                      *
 441 %*              For internal use only!                                  *
 442 %*                                                                      *
 443 %************************************************************************
 444
 445 \begin{code}
 446 -- zonkType is used for Kinds as well
 447
 448 -- For unbound, mutable tyvars, zonkType uses the function given to it
 449 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 450 --      type variable and zonks the kind too
 451
 452 zonkType :: (TcTyVar -> NF_TcM Type)    -- What to do with unbound mutable type variables
 453                                         -- see zonkTcType, and zonkTcTypeToType
 454          -> TcType
 455          -> NF_TcM Type
 456 zonkType unbound_var_fn ty
 457   = go ty
 458   where
 459     go (TyConApp tycon tys)       = mapNF_Tc go tys     `thenNF_Tc` \ tys' ->
 460                                     returnNF_Tc (TyConApp tycon tys')
 461
 462     go (NoteTy (SynNote ty1) ty2) = go ty1              `thenNF_Tc` \ ty1' ->
 463                                     go ty2              `thenNF_Tc` \ ty2' ->
 464                                     returnNF_Tc (NoteTy (SynNote ty1') ty2')
 465
 466     go (NoteTy (FTVNote _) ty2)   = go ty2      -- Discard free-tyvar annotations
 467
 468     go (SourceTy p)               = go_pred p           `thenNF_Tc` \ p' ->
 469                                     returnNF_Tc (SourceTy p')
 470
 471     go (FunTy arg res)            = go arg              `thenNF_Tc` \ arg' ->
 472                                     go res              `thenNF_Tc` \ res' ->
 473                                     returnNF_Tc (FunTy arg' res')
 474
 475     go (AppTy fun arg)            = go fun              `thenNF_Tc` \ fun' ->
 476                                     go arg              `thenNF_Tc` \ arg' ->
 477                                     returnNF_Tc (mkAppTy fun' arg')
 478
 479     go (UsageTy u ty)             = go u                `thenNF_Tc` \ u'  ->
 480                                     go ty               `thenNF_Tc` \ ty' ->
 481                                     returnNF_Tc (UsageTy u' ty')
 482
 483         -- The two interesting cases!
 484     go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn tyvar
 485
 486     go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar   `thenNF_Tc` \ tyvar' ->
 487                              go ty                      `thenNF_Tc` \ ty' ->
 488                              returnNF_Tc (ForAllTy tyvar' ty')
 489
 490     go_pred (ClassP c tys) = mapNF_Tc go tys    `thenNF_Tc` \ tys' ->
 491                              returnNF_Tc (ClassP c tys')
 492     go_pred (NType tc tys) = mapNF_Tc go tys    `thenNF_Tc` \ tys' ->
 493                              returnNF_Tc (NType tc tys')
 494     go_pred (IParam n ty)  = go ty              `thenNF_Tc` \ ty' ->
 495                              returnNF_Tc (IParam n ty')
 496
 497 zonkTyVar :: (TcTyVar -> NF_TcM Type)           -- What to do for an unbound mutable variable
 498           -> TcTyVar -> NF_TcM TcType
 499 zonkTyVar unbound_var_fn tyvar
 500   | not (isMutTyVar tyvar)      -- Not a mutable tyvar.  This can happen when
 501                                 -- zonking a forall type, when the bound type variable
 502                                 -- needn't be mutable
 503   = ASSERT( isTyVar tyvar )             -- Should not be any immutable kind vars
 504     returnNF_Tc (TyVarTy tyvar)
 505
 506   | otherwise
 507   =  getTcTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
 508      case maybe_ty of
 509           Nothing       -> unbound_var_fn tyvar                 -- Mutable and unbound
 510           Just other_ty -> zonkType unbound_var_fn other_ty     -- Bound
 511 \end{code}
 512
 513
 514
 515 %************************************************************************
 516 %*                                                                      *
 517 \subsection{Checking a user type}
 518 %*                                                                      *
 519 %************************************************************************
 520
 521 When dealing with a user-written type, we first translate it from an HsType
 522 to a Type, performing kind checking, and then check various things that should
 523 be true about it.  We don't want to perform these checks at the same time
 524 as the initial translation because (a) they are unnecessary for interface-file
 525 types and (b) when checking a mutually recursive group of type and class decls,
 526 we can't "look" at the tycons/classes yet.  Also, the checks are are rather
 527 diverse, and used to really mess up the other code.
 528
 529 One thing we check for is 'rank'.
 530
 531         Rank 0:         monotypes (no foralls)
 532         Rank 1:         foralls at the front only, Rank 0 inside
 533         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
 534
 535         basic ::= tyvar | T basic ... basic
 536
 537         r2  ::= forall tvs. cxt => r2a
 538         r2a ::= r1 -> r2a | basic
 539         r1  ::= forall tvs. cxt => r0
 540         r0  ::= r0 -> r0 | basic
 541
 542 Another thing is to check that type synonyms are saturated.
 543 This might not necessarily show up in kind checking.
 544         type A i = i
 545         data T k = MkT (k Int)
 546         f :: T A        -- BAD!
 547
 548
 549 \begin{code}
 550 data UserTypeCtxt
 551   = FunSigCtxt Name     -- Function type signature
 552   | ExprSigCtxt         -- Expression type signature
 553   | ConArgCtxt Name     -- Data constructor argument
 554   | TySynCtxt Name      -- RHS of a type synonym decl
 555   | GenPatCtxt          -- Pattern in generic decl
 556                         --      f{| a+b |} (Inl x) = ...
 557   | PatSigCtxt          -- Type sig in pattern
 558                         --      f (x::t) = ...
 559   | ResSigCtxt          -- Result type sig
 560                         --      f x :: t = ....
 561   | ForSigCtxt Name     -- Foreign inport or export signature
 562   | RuleSigCtxt Name    -- Signature on a forall'd variable in a RULE
 563
 564 -- Notes re TySynCtxt
 565 -- We allow type synonyms that aren't types; e.g.  type List = []
 566 --
 567 -- If the RHS mentions tyvars that aren't in scope, we'll
 568 -- quantify over them:
 569 --      e.g.    type T = a->a
 570 -- will become  type T = forall a. a->a
 571 --
 572 -- With gla-exts that's right, but for H98 we should complain.
 573
 574
 575 pprUserTypeCtxt (FunSigCtxt n)  = ptext SLIT("the type signature for") <+> quotes (ppr n)
 576 pprUserTypeCtxt ExprSigCtxt     = ptext SLIT("an expression type signature")
 577 pprUserTypeCtxt (ConArgCtxt c)  = ptext SLIT("the type of constructor") <+> quotes (ppr c)
 578 pprUserTypeCtxt (TySynCtxt c)   = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
 579 pprUserTypeCtxt GenPatCtxt      = ptext SLIT("the type pattern of a generic definition")
 580 pprUserTypeCtxt PatSigCtxt      = ptext SLIT("a pattern type signature")
 581 pprUserTypeCtxt ResSigCtxt      = ptext SLIT("a result type signature")
 582 pprUserTypeCtxt (ForSigCtxt n)  = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
 583 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
 584 \end{code}
 585
 586 \begin{code}
 587 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 588 -- Checks that the type is valid for the given context
 589 checkValidType ctxt ty
 590   = doptsTc Opt_GlasgowExts     `thenNF_Tc` \ gla_exts ->
 591     let
 592         rank | gla_exts = Arbitrary
 593              | otherwise
 594              = case ctxt of     -- Haskell 98
 595                  GenPatCtxt     -> Rank 0
 596                  PatSigCtxt     -> Rank 0
 597                  ResSigCtxt     -> Rank 0
 598                  TySynCtxt _    -> Rank 0
 599                  ExprSigCtxt    -> Rank 1
 600                  FunSigCtxt _   -> Rank 1
 601                  ConArgCtxt _   -> Rank 1       -- We are given the type of the entire
 602                                                 -- constructor, hence rank 1
 603                  ForSigCtxt _   -> Rank 1
 604                  RuleSigCtxt _  -> Rank 1
 605
 606         actual_kind = typeKind ty
 607
 608         actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
 609
 610         kind_ok = case ctxt of
 611                         TySynCtxt _  -> True    -- Any kind will do
 612                         GenPatCtxt   -> actual_kind_is_lifted
 613                         ForSigCtxt _ -> actual_kind_is_lifted
 614                         other        -> isTypeKind actual_kind
 615     in
 616     tcAddErrCtxt (checkTypeCtxt ctxt ty)        $
 617
 618         -- Check that the thing has kind Type, and is lifted if necessary
 619     checkTc kind_ok (kindErr actual_kind)       `thenTc_`
 620
 621         -- Check the internal validity of the type itself
 622     check_poly_type rank ty
 623
 624
 625 checkTypeCtxt ctxt ty
 626   = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
 627           ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
 628
 629         -- Hack alert.  If there are no tyvars, (ppr sigma_ty) will print
 630         -- something strange like {Eq k} -> k -> k, because there is no
 631         -- ForAll at the top of the type.  Since this is going to the user
 632         -- we want it to look like a proper Haskell type even then; hence the hack
 633         --
 634         -- This shows up in the complaint about
 635         --      case C a where
 636         --        op :: Eq a => a -> a
 637 ppr_ty ty | null forall_tvs && not (null theta) = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
 638           | otherwise                        = ppr ty
 639           where
 640             (forall_tvs, theta, tau) = tcSplitSigmaTy ty
 641 \end{code}
 642
 643
 644 \begin{code}
 645 data Rank = Rank Int | Arbitrary
 646
 647 decRank :: Rank -> Rank
 648 decRank Arbitrary = Arbitrary
 649 decRank (Rank n)  = Rank (n-1)
 650
 651 check_poly_type :: Rank -> Type -> TcM ()
 652 check_poly_type (Rank 0) ty
 653   = check_tau_type (Rank 0) False ty
 654
 655 check_poly_type rank ty
 656   = let
 657         (tvs, theta, tau) = tcSplitSigmaTy ty
 658     in
 659     check_valid_theta SigmaCtxt theta           `thenTc_`
 660     check_tau_type (decRank rank) False tau     `thenTc_`
 661     checkAmbiguity tvs theta tau
 662
 663 ----------------------------------------
 664 check_arg_type :: Type -> TcM ()
 665 -- The sort of type that can instantiate a type variable,
 666 -- or be the argument of a type constructor.
 667 -- Not an unboxed tuple, not a forall.
 668 -- Other unboxed types are very occasionally allowed as type
 669 -- arguments depending on the kind of the type constructor
 670 --
 671 -- For example, we want to reject things like:
 672 --
 673 --      instance Ord a => Ord (forall s. T s a)
 674 -- and
 675 --      g :: T s (forall b.b)
 676 --
 677 -- NB: unboxed tuples can have polymorphic or unboxed args.
 678 --     This happens in the workers for functions returning
 679 --     product types with polymorphic components.
 680 --     But not in user code
 681 --
 682 -- Question: what about nested unboxed tuples?
 683 --           Currently rejected.
 684 check_arg_type ty
 685   = check_tau_type (Rank 0) False ty    `thenTc_`
 686     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 687
 688 ----------------------------------------
 689 check_tau_type :: Rank -> Bool -> Type -> TcM ()
 690 -- Rank is allowed rank for function args
 691 -- No foralls otherwise
 692 -- Bool is True iff unboxed tuple are allowed here
 693
 694 check_tau_type rank ubx_tup_ok ty@(UsageTy _ _)  = failWithTc (usageTyErr ty)
 695 check_tau_type rank ubx_tup_ok ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
 696 check_tau_type rank ubx_tup_ok (SourceTy sty)    = getDOptsTc           `thenNF_Tc` \ dflags ->
 697                                                    check_source_ty dflags TypeCtxt sty
 698 check_tau_type rank ubx_tup_ok (TyVarTy _)       = returnTc ()
 699 check_tau_type rank ubx_tup_ok ty@(FunTy arg_ty res_ty)
 700   = check_poly_type rank      arg_ty    `thenTc_`
 701     check_tau_type  rank True res_ty
 702
 703 check_tau_type rank ubx_tup_ok (AppTy ty1 ty2)
 704   = check_arg_type ty1 `thenTc_` check_arg_type ty2
 705
 706 check_tau_type rank ubx_tup_ok (NoteTy note ty)
 707   = check_note note `thenTc_` check_tau_type rank ubx_tup_ok ty
 708
 709 check_tau_type rank ubx_tup_ok ty@(TyConApp tc tys)
 710   | isSynTyCon tc
 711   = checkTc syn_arity_ok arity_msg      `thenTc_`
 712     mapTc_ check_arg_type tys
 713
 714   | isUnboxedTupleTyCon tc
 715   = checkTc ubx_tup_ok ubx_tup_msg      `thenTc_`
 716     mapTc_ (check_tau_type (Rank 0) True) tys   -- Args are allowed to be unlifted, or
 717                                                 -- more unboxed tuples, so can't use check_arg_ty
 718
 719   | otherwise
 720   = mapTc_ check_arg_type tys
 721
 722   where
 723     syn_arity_ok = tc_arity <= n_args
 724                 -- It's OK to have an *over-applied* type synonym
 725                 --      data Tree a b = ...
 726                 --      type Foo a = Tree [a]
 727                 --      f :: Foo a b -> ...
 728     n_args    = length tys
 729     tc_arity  = tyConArity tc
 730
 731     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
 732     ubx_tup_msg = ubxArgTyErr ty
 733
 734 ----------------------------------------
 735 check_note (FTVNote _)  = returnTc ()
 736 check_note (SynNote ty) = check_tau_type (Rank 0) False ty
 737 \end{code}
 738
 739 Check for ambiguity
 740 ~~~~~~~~~~~~~~~~~~~
 741           forall V. P => tau
 742 is ambiguous if P contains generic variables
 743 (i.e. one of the Vs) that are not mentioned in tau
 744
 745 However, we need to take account of functional dependencies
 746 when we speak of 'mentioned in tau'.  Example:
 747         class C a b | a -> b where ...
 748 Then the type
 749         forall x y. (C x y) => x
 750 is not ambiguous because x is mentioned and x determines y
 751
 752 NOTE: In addition, GHC insists that at least one type variable
 753 in each constraint is in V.  So we disallow a type like
 754         forall a. Eq b => b -> b
 755 even in a scope where b is in scope.
 756 This is the is_free test below.
 757
 758 NB; the ambiguity check is only used for *user* types, not for types
 759 coming from inteface files.  The latter can legitimately have
 760 ambiguous types. Example
 761
 762    class S a where s :: a -> (Int,Int)
 763    instance S Char where s _ = (1,1)
 764    f:: S a => [a] -> Int -> (Int,Int)
 765    f (_::[a]) x = (a*x,b)
 766         where (a,b) = s (undefined::a)
 767
 768 Here the worker for f gets the type
 769         fw :: forall a. S a => Int -> (# Int, Int #)
 770
 771 If the list of tv_names is empty, we have a monotype, and then we
 772 don't need to check for ambiguity either, because the test can't fail
 773 (see is_ambig).
 774
 775 \begin{code}
 776 checkAmbiguity :: [TyVar] -> ThetaType -> Type -> TcM ()
 777 checkAmbiguity forall_tyvars theta tau
 778   = mapTc_ check_pred theta     `thenTc_`
 779     returnTc ()
 780   where
 781     tau_vars          = tyVarsOfType tau
 782     extended_tau_vars = grow theta tau_vars
 783
 784     is_ambig ct_var   = (ct_var `elem` forall_tyvars) &&
 785                         not (ct_var `elemVarSet` extended_tau_vars)
 786     is_free ct_var    = not (ct_var `elem` forall_tyvars)
 787
 788     check_pred pred = checkTc (not any_ambig)                 (ambigErr pred) `thenTc_`
 789                       checkTc (isIPPred pred || not all_free) (freeErr  pred)
 790              where
 791                 ct_vars   = varSetElems (tyVarsOfPred pred)
 792                 all_free  = all is_free ct_vars
 793                 any_ambig = any is_ambig ct_vars
 794 \end{code}
 795
 796 \begin{code}
 797 ambigErr pred
 798   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
 799          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
 800                  ptext SLIT("must be reachable from the type after the '=>'"))]
 801
 802
 803 freeErr pred
 804   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
 805                    ptext SLIT("are already in scope"),
 806          nest 4 (ptext SLIT("At least one must be universally quantified here"))
 807     ]
 808
 809 forAllTyErr     ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
 810 usageTyErr      ty = ptext SLIT("Illegal usage type:") <+> ppr_ty ty
 811 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
 812 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
 813 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 814 \end{code}
 815
 816 %************************************************************************
 817 %*                                                                      *
 818 \subsection{Checking a theta or source type}
 819 %*                                                                      *
 820 %************************************************************************
 821
 822 \begin{code}
 823 data SourceTyCtxt
 824   = ClassSCCtxt Name    -- Superclasses of clas
 825   | SigmaCtxt           -- Context of a normal for-all type
 826   | DataTyCtxt Name     -- Context of a data decl
 827   | TypeCtxt            -- Source type in an ordinary type
 828   | InstThetaCtxt       -- Context of an instance decl
 829   | InstHeadCtxt        -- Head of an instance decl
 830
 831 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
 832 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
 833 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
 834 pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
 835 pprSourceTyCtxt InstHeadCtxt    = ptext SLIT("the head of an instance declaration")
 836 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
 837 \end{code}
 838
 839 \begin{code}
 840 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
 841 checkValidTheta ctxt theta
 842   = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
 843
 844 -------------------------
 845 check_valid_theta ctxt []
 846   = returnTc ()
 847 check_valid_theta ctxt theta
 848   = getDOptsTc                                  `thenNF_Tc` \ dflags ->
 849     warnTc (not (null dups)) (dupPredWarn dups) `thenNF_Tc_`
 850     mapTc_ (check_source_ty dflags ctxt) theta
 851   where
 852     (_,dups) = removeDups tcCmpPred theta
 853
 854 -------------------------
 855 check_source_ty dflags ctxt pred@(ClassP cls tys)
 856   =     -- Class predicates are valid in all contexts
 857     mapTc_ check_arg_type tys                   `thenTc_`
 858     checkTc (arity == n_tys) arity_err          `thenTc_`
 859     checkTc (all tyvar_head tys || arby_preds_ok) (predTyVarErr pred)
 860
 861   where
 862     class_name = className cls
 863     arity      = classArity cls
 864     n_tys      = length tys
 865     arity_err  = arityErr "Class" class_name arity n_tys
 866
 867     arby_preds_ok = case ctxt of
 868                         InstHeadCtxt  -> True   -- We check for instance-head formation
 869                                                 -- in checkValidInstHead
 870                         InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
 871                         other         -> dopt Opt_GlasgowExts               dflags
 872
 873 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
 874         -- Implicit parameters only allows in type
 875         -- signatures; not in instance decls, superclasses etc
 876         -- The reason for not allowing implicit params in instances is a bit subtle
 877         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
 878         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
 879         -- discharge all the potential usas of the ?x in e.   For example, a
 880         -- constraint Foo [Int] might come out of e,and applying the
 881         -- instance decl would show up two uses of ?x.
 882
 883 check_source_ty dflags TypeCtxt  (NType tc tys)   = mapTc_ check_arg_type tys
 884
 885 -- Catch-all
 886 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 887
 888 -------------------------
 889 tyvar_head ty                   -- Haskell 98 allows predicates of form
 890   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
 891   | otherwise                   -- where a is a type variable
 892   = case tcSplitAppTy_maybe ty of
 893         Just (ty, _) -> tyvar_head ty
 894         Nothing      -> False
 895 \end{code}
 896
 897 \begin{code}
 898 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
 899 predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
 900 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
 901
 902 checkThetaCtxt ctxt theta
 903   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
 904           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 905 \end{code}
 906
 907
 908 %************************************************************************
 909 %*                                                                      *
 910 \subsection{Checking for a decent instance head type}
 911 %*                                                                      *
 912 %************************************************************************
 913
 914 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
 915 it must normally look like: @instance Foo (Tycon a b c ...) ...@
 916
 917 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
 918 flag is on, or (2)~the instance is imported (they must have been
 919 compiled elsewhere). In these cases, we let them go through anyway.
 920
 921 We can also have instances for functions: @instance Foo (a -> b) ...@.
 922
 923 \begin{code}
 924 checkValidInstHead :: Type -> TcM ()
 925
 926 checkValidInstHead ty   -- Should be a source type
 927   = case tcSplitPredTy_maybe ty of {
 928         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
 929         Just pred ->
 930
 931     case getClassPredTys_maybe pred of {
 932         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
 933         Just (clas,tys) ->
 934
 935     getDOptsTc                                  `thenNF_Tc` \ dflags ->
 936     mapTc_ check_arg_type tys                   `thenTc_`
 937     check_inst_head dflags clas tys
 938     }}
 939
 940 check_inst_head dflags clas tys
 941   |     -- CCALL CHECK
 942         -- A user declaration of a CCallable/CReturnable instance
 943         -- must be for a "boxed primitive" type.
 944         (clas `hasKey` cCallableClassKey
 945             && not (ccallable_type first_ty))
 946   ||    (clas `hasKey` cReturnableClassKey
 947             && not (creturnable_type first_ty))
 948   = failWithTc (nonBoxedPrimCCallErr clas first_ty)
 949
 950         -- If GlasgowExts then check at least one isn't a type variable
 951   | dopt Opt_GlasgowExts dflags
 952   = check_tyvars dflags clas tys
 953
 954         -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
 955   | isSingleton tys,
 956     Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
 957     not (isSynTyCon tycon),             -- ...but not a synonym
 958     all tcIsTyVarTy arg_tys,            -- Applied to type variables
 959     equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
 960           -- This last condition checks that all the type variables are distinct
 961   = returnTc ()
 962
 963   | otherwise
 964   = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
 965
 966   where
 967     (first_ty : _)       = tys
 968
 969     ccallable_type   ty = isFFIArgumentTy dflags PlayRisky ty
 970     creturnable_type ty = isFFIImportResultTy dflags ty
 971
 972     head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
 973                              text "where T is not a synonym, and a,b,c are distinct type variables")
 974
 975 check_tyvars dflags clas tys
 976         -- Check that at least one isn't a type variable
 977         -- unless -fallow-undecideable-instances
 978   | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
 979   | not (all tcIsTyVarTy tys)                 = returnTc ()
 980   | otherwise                                 = failWithTc (instTypeErr (pprClassPred clas tys) msg)
 981   where
 982     msg =  parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
 983                 $$ ptext SLIT("Use -fallow-undecidable-instances to lift this restriction"))
 984 \end{code}
 985
 986 \begin{code}
 987 instTypeErr pp_ty msg
 988   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
 989          nest 4 msg]
 990
 991 nonBoxedPrimCCallErr clas inst_ty
 992   = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
 993          4 (pprClassPred clas [inst_ty])
 994 \end{code}
 995
 996