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                 -- NB the mkAppTy; we might have instantiated a
 458                 -- type variable to a type constructor, so we need
 459                 -- to pull the TyConApp to the top.
 460
 461         -- The two interesting cases!
 462     go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn tyvar
 463
 464     go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar   `thenNF_Tc` \ tyvar' ->
 465                              go ty                      `thenNF_Tc` \ ty' ->
 466                              returnNF_Tc (ForAllTy tyvar' ty')
 467
 468     go_pred (ClassP c tys) = mapNF_Tc go tys    `thenNF_Tc` \ tys' ->
 469                              returnNF_Tc (ClassP c tys')
 470     go_pred (NType tc tys) = mapNF_Tc go tys    `thenNF_Tc` \ tys' ->
 471                              returnNF_Tc (NType tc tys')
 472     go_pred (IParam n ty)  = go ty              `thenNF_Tc` \ ty' ->
 473                              returnNF_Tc (IParam n ty')
 474
 475 zonkTyVar :: (TcTyVar -> NF_TcM Type)           -- What to do for an unbound mutable variable
 476           -> TcTyVar -> NF_TcM TcType
 477 zonkTyVar unbound_var_fn tyvar
 478   | not (isMutTyVar tyvar)      -- Not a mutable tyvar.  This can happen when
 479                                 -- zonking a forall type, when the bound type variable
 480                                 -- needn't be mutable
 481   = ASSERT( isTyVar tyvar )             -- Should not be any immutable kind vars
 482     returnNF_Tc (TyVarTy tyvar)
 483
 484   | otherwise
 485   =  getTcTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
 486      case maybe_ty of
 487           Nothing       -> unbound_var_fn tyvar                 -- Mutable and unbound
 488           Just other_ty -> zonkType unbound_var_fn other_ty     -- Bound
 489 \end{code}
 490
 491
 492
 493 %************************************************************************
 494 %*                                                                      *
 495 \subsection{Checking a user type}
 496 %*                                                                      *
 497 %************************************************************************
 498
 499 When dealing with a user-written type, we first translate it from an HsType
 500 to a Type, performing kind checking, and then check various things that should
 501 be true about it.  We don't want to perform these checks at the same time
 502 as the initial translation because (a) they are unnecessary for interface-file
 503 types and (b) when checking a mutually recursive group of type and class decls,
 504 we can't "look" at the tycons/classes yet.  Also, the checks are are rather
 505 diverse, and used to really mess up the other code.
 506
 507 One thing we check for is 'rank'.
 508
 509         Rank 0:         monotypes (no foralls)
 510         Rank 1:         foralls at the front only, Rank 0 inside
 511         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
 512
 513         basic ::= tyvar | T basic ... basic
 514
 515         r2  ::= forall tvs. cxt => r2a
 516         r2a ::= r1 -> r2a | basic
 517         r1  ::= forall tvs. cxt => r0
 518         r0  ::= r0 -> r0 | basic
 519
 520 Another thing is to check that type synonyms are saturated.
 521 This might not necessarily show up in kind checking.
 522         type A i = i
 523         data T k = MkT (k Int)
 524         f :: T A        -- BAD!
 525
 526
 527 \begin{code}
 528 data UserTypeCtxt
 529   = FunSigCtxt Name     -- Function type signature
 530   | ExprSigCtxt         -- Expression type signature
 531   | ConArgCtxt Name     -- Data constructor argument
 532   | TySynCtxt Name      -- RHS of a type synonym decl
 533   | GenPatCtxt          -- Pattern in generic decl
 534                         --      f{| a+b |} (Inl x) = ...
 535   | PatSigCtxt          -- Type sig in pattern
 536                         --      f (x::t) = ...
 537   | ResSigCtxt          -- Result type sig
 538                         --      f x :: t = ....
 539   | ForSigCtxt Name     -- Foreign inport or export signature
 540   | RuleSigCtxt Name    -- Signature on a forall'd variable in a RULE
 541
 542 -- Notes re TySynCtxt
 543 -- We allow type synonyms that aren't types; e.g.  type List = []
 544 --
 545 -- If the RHS mentions tyvars that aren't in scope, we'll
 546 -- quantify over them:
 547 --      e.g.    type T = a->a
 548 -- will become  type T = forall a. a->a
 549 --
 550 -- With gla-exts that's right, but for H98 we should complain.
 551
 552
 553 pprUserTypeCtxt (FunSigCtxt n)  = ptext SLIT("the type signature for") <+> quotes (ppr n)
 554 pprUserTypeCtxt ExprSigCtxt     = ptext SLIT("an expression type signature")
 555 pprUserTypeCtxt (ConArgCtxt c)  = ptext SLIT("the type of constructor") <+> quotes (ppr c)
 556 pprUserTypeCtxt (TySynCtxt c)   = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
 557 pprUserTypeCtxt GenPatCtxt      = ptext SLIT("the type pattern of a generic definition")
 558 pprUserTypeCtxt PatSigCtxt      = ptext SLIT("a pattern type signature")
 559 pprUserTypeCtxt ResSigCtxt      = ptext SLIT("a result type signature")
 560 pprUserTypeCtxt (ForSigCtxt n)  = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
 561 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
 562 \end{code}
 563
 564 \begin{code}
 565 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 566 -- Checks that the type is valid for the given context
 567 checkValidType ctxt ty
 568   = doptsTc Opt_GlasgowExts     `thenNF_Tc` \ gla_exts ->
 569     let
 570         rank | gla_exts = Arbitrary
 571              | otherwise
 572              = case ctxt of     -- Haskell 98
 573                  GenPatCtxt     -> Rank 0
 574                  PatSigCtxt     -> Rank 0
 575                  ResSigCtxt     -> Rank 0
 576                  TySynCtxt _    -> Rank 0
 577                  ExprSigCtxt    -> Rank 1
 578                  FunSigCtxt _   -> Rank 1
 579                  ConArgCtxt _   -> Rank 1       -- We are given the type of the entire
 580                                                 -- constructor, hence rank 1
 581                  ForSigCtxt _   -> Rank 1
 582                  RuleSigCtxt _  -> Rank 1
 583
 584         actual_kind = typeKind ty
 585
 586         actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
 587
 588         kind_ok = case ctxt of
 589                         TySynCtxt _  -> True    -- Any kind will do
 590                         GenPatCtxt   -> actual_kind_is_lifted
 591                         ForSigCtxt _ -> actual_kind_is_lifted
 592                         other        -> isTypeKind actual_kind
 593
 594         ubx_tup | not gla_exts = UT_NotOk
 595                 | otherwise    = case ctxt of
 596                                    TySynCtxt _ -> UT_Ok
 597                                    other       -> UT_NotOk
 598                 -- Unboxed tuples ok in function results,
 599                 -- but for type synonyms we allow them even at
 600                 -- top level
 601     in
 602     tcAddErrCtxt (checkTypeCtxt ctxt ty)        $
 603
 604         -- Check that the thing has kind Type, and is lifted if necessary
 605     checkTc kind_ok (kindErr actual_kind)       `thenTc_`
 606
 607         -- Check the internal validity of the type itself
 608     check_poly_type rank ubx_tup ty
 609
 610
 611 checkTypeCtxt ctxt ty
 612   = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
 613           ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
 614
 615         -- Hack alert.  If there are no tyvars, (ppr sigma_ty) will print
 616         -- something strange like {Eq k} -> k -> k, because there is no
 617         -- ForAll at the top of the type.  Since this is going to the user
 618         -- we want it to look like a proper Haskell type even then; hence the hack
 619         --
 620         -- This shows up in the complaint about
 621         --      case C a where
 622         --        op :: Eq a => a -> a
 623 ppr_ty ty | null forall_tvs && not (null theta) = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
 624           | otherwise                        = ppr ty
 625           where
 626             (forall_tvs, theta, tau) = tcSplitSigmaTy ty
 627 \end{code}
 628
 629
 630 \begin{code}
 631 data Rank = Rank Int | Arbitrary
 632
 633 decRank :: Rank -> Rank
 634 decRank Arbitrary = Arbitrary
 635 decRank (Rank n)  = Rank (n-1)
 636
 637 ----------------------------------------
 638 data UbxTupFlag = UT_Ok | UT_NotOk
 639         -- The "Ok" version means "ok if -fglasgow-exts is on"
 640
 641 ----------------------------------------
 642 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 643 check_poly_type (Rank 0) ubx_tup ty
 644   = check_tau_type (Rank 0) ubx_tup ty
 645
 646 check_poly_type rank ubx_tup ty
 647   = let
 648         (tvs, theta, tau) = tcSplitSigmaTy ty
 649     in
 650     check_valid_theta SigmaCtxt theta           `thenTc_`
 651     check_tau_type (decRank rank) ubx_tup tau   `thenTc_`
 652     checkFreeness tvs theta                     `thenTc_`
 653     checkAmbiguity tvs theta (tyVarsOfType tau)
 654
 655 ----------------------------------------
 656 check_arg_type :: Type -> TcM ()
 657 -- The sort of type that can instantiate a type variable,
 658 -- or be the argument of a type constructor.
 659 -- Not an unboxed tuple, not a forall.
 660 -- Other unboxed types are very occasionally allowed as type
 661 -- arguments depending on the kind of the type constructor
 662 --
 663 -- For example, we want to reject things like:
 664 --
 665 --      instance Ord a => Ord (forall s. T s a)
 666 -- and
 667 --      g :: T s (forall b.b)
 668 --
 669 -- NB: unboxed tuples can have polymorphic or unboxed args.
 670 --     This happens in the workers for functions returning
 671 --     product types with polymorphic components.
 672 --     But not in user code.
 673 -- Anyway, they are dealt with by a special case in check_tau_type
 674
 675 check_arg_type ty
 676   = check_tau_type (Rank 0) UT_NotOk ty         `thenTc_`
 677     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 678
 679 ----------------------------------------
 680 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 681 -- Rank is allowed rank for function args
 682 -- No foralls otherwise
 683
 684 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
 685 check_tau_type rank ubx_tup (SourceTy sty)    = getDOptsTc              `thenNF_Tc` \ dflags ->
 686                                                 check_source_ty dflags TypeCtxt sty
 687 check_tau_type rank ubx_tup (TyVarTy _)       = returnTc ()
 688 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
 689   = check_poly_type rank UT_NotOk arg_ty        `thenTc_`
 690     check_tau_type  rank UT_Ok    res_ty
 691
 692 check_tau_type rank ubx_tup (AppTy ty1 ty2)
 693   = check_arg_type ty1 `thenTc_` check_arg_type ty2
 694
 695 check_tau_type rank ubx_tup (NoteTy note ty)
 696   = check_tau_type rank ubx_tup ty
 697         -- Synonym notes are built only when the synonym is
 698         -- saturated (see Type.mkSynTy)
 699         -- Not checking the 'note' part allows us to instantiate a synonym
 700         -- defn with a for-all type, or with a partially-applied type synonym,
 701         -- but that seems OK too
 702
 703 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
 704   | isSynTyCon tc
 705   =     -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
 706         -- synonym application, leaving it to checkValidType (i.e. right here
 707         -- to find the error
 708     checkTc syn_arity_ok arity_msg      `thenTc_`
 709     mapTc_ check_arg_type tys
 710
 711   | isUnboxedTupleTyCon tc
 712   = doptsTc Opt_GlasgowExts                     `thenNF_Tc` \ gla_exts ->
 713     checkTc (ubx_tup_ok gla_exts) ubx_tup_msg   `thenTc_`
 714     mapTc_ (check_tau_type (Rank 0) UT_Ok) tys
 715                         -- Args are allowed to be unlifted, or
 716                         -- more unboxed tuples, so can't use check_arg_ty
 717
 718   | otherwise
 719   = mapTc_ check_arg_type tys
 720
 721   where
 722     ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
 723
 724     syn_arity_ok = tc_arity <= n_args
 725                 -- It's OK to have an *over-applied* type synonym
 726                 --      data Tree a b = ...
 727                 --      type Foo a = Tree [a]
 728                 --      f :: Foo a b -> ...
 729     n_args    = length tys
 730     tc_arity  = tyConArity tc
 731
 732     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
 733     ubx_tup_msg = ubxArgTyErr ty
 734
 735 ----------------------------------------
 736 forAllTyErr     ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
 737 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
 738 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
 739 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 740 \end{code}
 741
 742 Check for ambiguity
 743 ~~~~~~~~~~~~~~~~~~~
 744           forall V. P => tau
 745 is ambiguous if P contains generic variables
 746 (i.e. one of the Vs) that are not mentioned in tau
 747
 748 However, we need to take account of functional dependencies
 749 when we speak of 'mentioned in tau'.  Example:
 750         class C a b | a -> b where ...
 751 Then the type
 752         forall x y. (C x y) => x
 753 is not ambiguous because x is mentioned and x determines y
 754
 755 NB; the ambiguity check is only used for *user* types, not for types
 756 coming from inteface files.  The latter can legitimately have
 757 ambiguous types. Example
 758
 759    class S a where s :: a -> (Int,Int)
 760    instance S Char where s _ = (1,1)
 761    f:: S a => [a] -> Int -> (Int,Int)
 762    f (_::[a]) x = (a*x,b)
 763         where (a,b) = s (undefined::a)
 764
 765 Here the worker for f gets the type
 766         fw :: forall a. S a => Int -> (# Int, Int #)
 767
 768 If the list of tv_names is empty, we have a monotype, and then we
 769 don't need to check for ambiguity either, because the test can't fail
 770 (see is_ambig).
 771
 772 \begin{code}
 773 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
 774 checkAmbiguity forall_tyvars theta tau_tyvars
 775   = mapTc_ complain (filter is_ambig theta)
 776   where
 777     complain pred     = addErrTc (ambigErr pred)
 778     extended_tau_vars = grow theta tau_tyvars
 779     is_ambig pred     = any ambig_var (varSetElems (tyVarsOfPred pred))
 780
 781     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
 782                         not (ct_var `elemVarSet` extended_tau_vars)
 783
 784     is_free ct_var    = not (ct_var `elem` forall_tyvars)
 785
 786 ambigErr pred
 787   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
 788          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
 789                  ptext SLIT("must be reachable from the type after the '=>'"))]
 790 \end{code}
 791
 792 In addition, GHC insists that at least one type variable
 793 in each constraint is in V.  So we disallow a type like
 794         forall a. Eq b => b -> b
 795 even in a scope where b is in scope.
 796
 797 \begin{code}
 798 checkFreeness forall_tyvars theta
 799   = mapTc_ complain (filter is_free theta)
 800   where
 801     is_free pred     =  not (isIPPred pred)
 802                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
 803     bound_var ct_var = ct_var `elem` forall_tyvars
 804     complain pred    = addErrTc (freeErr pred)
 805
 806 freeErr pred
 807   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
 808                    ptext SLIT("are already in scope"),
 809          nest 4 (ptext SLIT("At least one must be universally quantified here"))
 810     ]
 811 \end{code}
 812
 813
 814 %************************************************************************
 815 %*                                                                      *
 816 \subsection{Checking a theta or source type}
 817 %*                                                                      *
 818 %************************************************************************
 819
 820 \begin{code}
 821 data SourceTyCtxt
 822   = ClassSCCtxt Name    -- Superclasses of clas
 823   | SigmaCtxt           -- Context of a normal for-all type
 824   | DataTyCtxt Name     -- Context of a data decl
 825   | TypeCtxt            -- Source type in an ordinary type
 826   | InstThetaCtxt       -- Context of an instance decl
 827   | InstHeadCtxt        -- Head of an instance decl
 828
 829 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
 830 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
 831 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
 832 pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
 833 pprSourceTyCtxt InstHeadCtxt    = ptext SLIT("the head of an instance declaration")
 834 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
 835 \end{code}
 836
 837 \begin{code}
 838 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
 839 checkValidTheta ctxt theta
 840   = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
 841
 842 -------------------------
 843 check_valid_theta ctxt []
 844   = returnTc ()
 845 check_valid_theta ctxt theta
 846   = getDOptsTc                                  `thenNF_Tc` \ dflags ->
 847     warnTc (not (null dups)) (dupPredWarn dups) `thenNF_Tc_`
 848     mapTc_ (check_source_ty dflags ctxt) theta
 849   where
 850     (_,dups) = removeDups tcCmpPred theta
 851
 852 -------------------------
 853 check_source_ty dflags ctxt pred@(ClassP cls tys)
 854   =     -- Class predicates are valid in all contexts
 855     mapTc_ check_arg_type tys           `thenTc_`
 856     checkTc (arity == n_tys) arity_err          `thenTc_`
 857     checkTc (all tyvar_head tys || arby_preds_ok)
 858             (predTyVarErr pred $$ how_to_allow)
 859
 860   where
 861     class_name = className cls
 862     arity      = classArity cls
 863     n_tys      = length tys
 864     arity_err  = arityErr "Class" class_name arity n_tys
 865
 866     arby_preds_ok = case ctxt of
 867                         InstHeadCtxt  -> True   -- We check for instance-head formation
 868                                                 -- in checkValidInstHead
 869                         InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
 870                         other         -> dopt Opt_GlasgowExts               dflags
 871
 872     how_to_allow = case ctxt of
 873                      InstHeadCtxt  -> empty     -- Should not happen
 874                      InstThetaCtxt -> parens undecidableMsg
 875                      other         -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 876
 877 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
 878         -- Implicit parameters only allows in type
 879         -- signatures; not in instance decls, superclasses etc
 880         -- The reason for not allowing implicit params in instances is a bit subtle
 881         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
 882         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
 883         -- discharge all the potential usas of the ?x in e.   For example, a
 884         -- constraint Foo [Int] might come out of e,and applying the
 885         -- instance decl would show up two uses of ?x.
 886
 887 check_source_ty dflags TypeCtxt  (NType tc tys)   = mapTc_ check_arg_type tys
 888
 889 -- Catch-all
 890 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 891
 892 -------------------------
 893 tyvar_head ty                   -- Haskell 98 allows predicates of form
 894   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
 895   | otherwise                   -- where a is a type variable
 896   = case tcSplitAppTy_maybe ty of
 897         Just (ty, _) -> tyvar_head ty
 898         Nothing      -> False
 899 \end{code}
 900
 901 \begin{code}
 902 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
 903 predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
 904 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
 905
 906 checkThetaCtxt ctxt theta
 907   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
 908           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 909 \end{code}
 910
 911
 912 %************************************************************************
 913 %*                                                                      *
 914 \subsection{Checking for a decent instance head type}
 915 %*                                                                      *
 916 %************************************************************************
 917
 918 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
 919 it must normally look like: @instance Foo (Tycon a b c ...) ...@
 920
 921 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
 922 flag is on, or (2)~the instance is imported (they must have been
 923 compiled elsewhere). In these cases, we let them go through anyway.
 924
 925 We can also have instances for functions: @instance Foo (a -> b) ...@.
 926
 927 \begin{code}
 928 checkValidInstHead :: Type -> TcM (Class, [TcType])
 929
 930 checkValidInstHead ty   -- Should be a source type
 931   = case tcSplitPredTy_maybe ty of {
 932         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
 933         Just pred ->
 934
 935     case getClassPredTys_maybe pred of {
 936         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
 937         Just (clas,tys) ->
 938
 939     getDOptsTc                                  `thenNF_Tc` \ dflags ->
 940     mapTc_ check_arg_type tys                   `thenTc_`
 941     check_inst_head dflags clas tys             `thenTc_`
 942     returnTc (clas, tys)
 943     }}
 944
 945 check_inst_head dflags clas tys
 946   |     -- CCALL CHECK
 947         -- A user declaration of a CCallable/CReturnable instance
 948         -- must be for a "boxed primitive" type.
 949         (clas `hasKey` cCallableClassKey
 950             && not (ccallable_type first_ty))
 951   ||    (clas `hasKey` cReturnableClassKey
 952             && not (creturnable_type first_ty))
 953   = failWithTc (nonBoxedPrimCCallErr clas first_ty)
 954
 955         -- If GlasgowExts then check at least one isn't a type variable
 956   | dopt Opt_GlasgowExts dflags
 957   = check_tyvars dflags clas tys
 958
 959         -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
 960   | isSingleton tys,
 961     Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
 962     not (isSynTyCon tycon),             -- ...but not a synonym
 963     all tcIsTyVarTy arg_tys,            -- Applied to type variables
 964     equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
 965           -- This last condition checks that all the type variables are distinct
 966   = returnTc ()
 967
 968   | otherwise
 969   = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
 970
 971   where
 972     (first_ty : _)       = tys
 973
 974     ccallable_type   ty = isFFIArgumentTy dflags PlayRisky ty
 975     creturnable_type ty = isFFIImportResultTy dflags ty
 976
 977     head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
 978                              text "where T is not a synonym, and a,b,c are distinct type variables")
 979
 980 check_tyvars dflags clas tys
 981         -- Check that at least one isn't a type variable
 982         -- unless -fallow-undecideable-instances
 983   | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
 984   | not (all tcIsTyVarTy tys)                 = returnTc ()
 985   | otherwise                                 = failWithTc (instTypeErr (pprClassPred clas tys) msg)
 986   where
 987     msg =  parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
 988                    $$ undecidableMsg)
 989
 990 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
 991 \end{code}
 992
 993 \begin{code}
 994 instTypeErr pp_ty msg
 995   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
 996          nest 4 msg]
 997
 998 nonBoxedPrimCCallErr clas inst_ty
 999   = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
1000          4 (pprClassPred clas [inst_ty])
1001 \end{code}