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