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