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