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