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