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