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