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