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                                    ExprSigCtxt -> 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}