ghc/compiler/typecheck/TcMType.lhs

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