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