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 -- Enumerate the contexts in which a "source type", <S>, can occur
 748 --      Eq a
 749 -- or   ?x::Int
 750 -- or   r <: {x::Int}
 751 -- or   (N a) where N is a newtype
 752
 753 data SourceTyCtxt
 754   = ClassSCCtxt Name    -- Superclasses of clas
 755                         --      class <S> => C a where ...
 756   | SigmaCtxt           -- Theta part of a normal for-all type
 757                         --      f :: <S> => a -> a
 758   | DataTyCtxt Name     -- Theta part of a data decl
 759                         --      data <S> => T a = MkT a
 760   | TypeCtxt            -- Source type in an ordinary type
 761                         --      f :: N a -> N a
 762   | InstThetaCtxt       -- Context of an instance decl
 763                         --      instance <S> => C [a] where ...
 764   | InstHeadCtxt        -- Head of an instance decl
 765                         --      instance ... => Eq a where ...
 766
 767 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
 768 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
 769 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
 770 pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
 771 pprSourceTyCtxt InstHeadCtxt    = ptext SLIT("the head of an instance declaration")
 772 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
 773 \end{code}
 774
 775 \begin{code}
 776 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
 777 checkValidTheta ctxt theta
 778   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
 779
 780 -------------------------
 781 check_valid_theta ctxt []
 782   = returnM ()
 783 check_valid_theta ctxt theta
 784   = getDOpts                                    `thenM` \ dflags ->
 785     warnTc (notNull dups) (dupPredWarn dups)    `thenM_`
 786         -- Actually, in instance decls and type signatures,
 787         -- duplicate constraints are eliminated by TcMonoType.hoistForAllTys,
 788         -- so this error can only fire for the context of a class or
 789         -- data type decl.
 790     mappM_ (check_source_ty dflags ctxt) theta
 791   where
 792     (_,dups) = removeDups tcCmpPred theta
 793
 794 -------------------------
 795 check_source_ty dflags ctxt pred@(ClassP cls tys)
 796   =     -- Class predicates are valid in all contexts
 797     mappM_ check_arg_type tys           `thenM_`
 798     checkTc (arity == n_tys) arity_err          `thenM_`
 799     checkTc (check_class_pred_tys dflags ctxt tys)
 800             (predTyVarErr pred $$ how_to_allow)
 801
 802   where
 803     class_name = className cls
 804     arity      = classArity cls
 805     n_tys      = length tys
 806     arity_err  = arityErr "Class" class_name arity n_tys
 807
 808     how_to_allow = case ctxt of
 809                      InstHeadCtxt  -> empty     -- Should not happen
 810                      InstThetaCtxt -> parens undecidableMsg
 811                      other         -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 812
 813 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
 814         -- Implicit parameters only allows in type
 815         -- signatures; not in instance decls, superclasses etc
 816         -- The reason for not allowing implicit params in instances is a bit subtle
 817         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
 818         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
 819         -- discharge all the potential usas of the ?x in e.   For example, a
 820         -- constraint Foo [Int] might come out of e,and applying the
 821         -- instance decl would show up two uses of ?x.
 822
 823 check_source_ty dflags TypeCtxt  (NType tc tys)   = mappM_ check_arg_type tys
 824
 825 -- Catch-all
 826 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 827
 828 -------------------------
 829 check_class_pred_tys dflags ctxt tys
 830   = case ctxt of
 831         InstHeadCtxt  -> True   -- We check for instance-head
 832                                 -- formation in checkValidInstHead
 833         InstThetaCtxt -> undecidable_ok || all isTyVarTy tys
 834         other         -> gla_exts       || all tyvar_head tys
 835   where
 836     undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
 837     gla_exts       = dopt Opt_GlasgowExts dflags
 838
 839 -------------------------
 840 tyvar_head ty                   -- Haskell 98 allows predicates of form
 841   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
 842   | otherwise                   -- where a is a type variable
 843   = case tcSplitAppTy_maybe ty of
 844         Just (ty, _) -> tyvar_head ty
 845         Nothing      -> False
 846 \end{code}
 847
 848 Check for ambiguity
 849 ~~~~~~~~~~~~~~~~~~~
 850           forall V. P => tau
 851 is ambiguous if P contains generic variables
 852 (i.e. one of the Vs) that are not mentioned in tau
 853
 854 However, we need to take account of functional dependencies
 855 when we speak of 'mentioned in tau'.  Example:
 856         class C a b | a -> b where ...
 857 Then the type
 858         forall x y. (C x y) => x
 859 is not ambiguous because x is mentioned and x determines y
 860
 861 NB; the ambiguity check is only used for *user* types, not for types
 862 coming from inteface files.  The latter can legitimately have
 863 ambiguous types. Example
 864
 865    class S a where s :: a -> (Int,Int)
 866    instance S Char where s _ = (1,1)
 867    f:: S a => [a] -> Int -> (Int,Int)
 868    f (_::[a]) x = (a*x,b)
 869         where (a,b) = s (undefined::a)
 870
 871 Here the worker for f gets the type
 872         fw :: forall a. S a => Int -> (# Int, Int #)
 873
 874 If the list of tv_names is empty, we have a monotype, and then we
 875 don't need to check for ambiguity either, because the test can't fail
 876 (see is_ambig).
 877
 878 \begin{code}
 879 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
 880 checkAmbiguity forall_tyvars theta tau_tyvars
 881   = mappM_ complain (filter is_ambig theta)
 882   where
 883     complain pred     = addErrTc (ambigErr pred)
 884     extended_tau_vars = grow theta tau_tyvars
 885
 886         -- Only a *class* predicate can give rise to ambiguity
 887         -- An *implicit parameter* cannot.  For example:
 888         --      foo :: (?x :: [a]) => Int
 889         --      foo = length ?x
 890         -- is fine.  The call site will suppply a particular 'x'
 891     is_ambig pred     = isClassPred  pred &&
 892                         any ambig_var (varSetElems (tyVarsOfPred pred))
 893
 894     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
 895                         not (ct_var `elemVarSet` extended_tau_vars)
 896
 897 ambigErr pred
 898   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
 899          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
 900                  ptext SLIT("must be reachable from the type after the '=>'"))]
 901 \end{code}
 902
 903 In addition, GHC insists that at least one type variable
 904 in each constraint is in V.  So we disallow a type like
 905         forall a. Eq b => b -> b
 906 even in a scope where b is in scope.
 907
 908 \begin{code}
 909 checkFreeness forall_tyvars theta
 910   = mappM_ complain (filter is_free theta)
 911   where
 912     is_free pred     =  not (isIPPred pred)
 913                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
 914     bound_var ct_var = ct_var `elem` forall_tyvars
 915     complain pred    = addErrTc (freeErr pred)
 916
 917 freeErr pred
 918   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
 919                    ptext SLIT("are already in scope"),
 920          nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
 921     ]
 922 \end{code}
 923
 924 \begin{code}
 925 checkThetaCtxt ctxt theta
 926   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
 927           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 928
 929 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
 930 predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
 931 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
 932
 933 arityErr kind name n m
 934   = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
 935            n_arguments <> comma, text "but has been given", int m]
 936     where
 937         n_arguments | n == 0 = ptext SLIT("no arguments")
 938                     | n == 1 = ptext SLIT("1 argument")
 939                     | True   = hsep [int n, ptext SLIT("arguments")]
 940 \end{code}
 941
 942
 943 %************************************************************************
 944 %*                                                                      *
 945 \subsection{Validity check for TyCons}
 946 %*                                                                      *
 947 %************************************************************************
 948
 949 checkValidTyCon is called once the mutually-recursive knot has been
 950 tied, so we can look at things freely.
 951
 952 \begin{code}
 953 checkValidTyCon :: TyCon -> TcM ()
 954 checkValidTyCon tc
 955   | isSynTyCon tc = checkValidType (TySynCtxt name) syn_rhs
 956   | otherwise
 957   =     -- Check the context on the data decl
 958     checkValidTheta (DataTyCtxt name) (tyConTheta tc)   `thenM_`
 959
 960         -- Check arg types of data constructors
 961     mappM_ checkValidDataCon data_cons                  `thenM_`
 962
 963         -- Check that fields with the same name share a type
 964     mappM_ check_fields groups
 965
 966   where
 967     name         = tyConName tc
 968     (_, syn_rhs) = getSynTyConDefn tc
 969     data_cons    = tyConDataCons tc
 970
 971     fields = [field | con <- data_cons, field <- dataConFieldLabels con]
 972     groups = equivClasses cmp_name fields
 973     cmp_name field1 field2 = fieldLabelName field1 `compare` fieldLabelName field2
 974
 975     check_fields fields@(first_field_label : other_fields)
 976         -- These fields all have the same name, but are from
 977         -- different constructors in the data type
 978         =       -- Check that all the fields in the group have the same type
 979                 -- NB: this check assumes that all the constructors of a given
 980                 -- data type use the same type variables
 981           checkTc (all (tcEqType field_ty) other_tys) (fieldTypeMisMatch field_name)
 982         where
 983             field_ty   = fieldLabelType first_field_label
 984             field_name = fieldLabelName first_field_label
 985             other_tys  = map fieldLabelType other_fields
 986
 987 checkValidDataCon :: DataCon -> TcM ()
 988 checkValidDataCon con
 989   = checkValidType ctxt (idType (dataConWrapId con))    `thenM_`
 990                 -- This checks the argument types and
 991                 -- ambiguity of the existential context (if any)
 992     addErrCtxt (existentialCtxt con)
 993                (checkFreeness ex_tvs ex_theta)
 994   where
 995     ctxt = ConArgCtxt (dataConName con)
 996     (_, _, ex_tvs, ex_theta, _, _) = dataConSig con
 997
 998
 999 fieldTypeMisMatch field_name
1000   = sep [ptext SLIT("Different constructors give different types for field"), quotes (ppr field_name)]
1001
1002 existentialCtxt con = ptext SLIT("When checking the existential context of constructor")
1003                       <+> quotes (ppr con)
1004 \end{code}
1005
1006
1007 checkValidClass is called once the mutually-recursive knot has been
1008 tied, so we can look at things freely.
1009
1010 \begin{code}
1011 checkValidClass :: Class -> TcM ()
1012 checkValidClass cls
1013   =     -- CHECK ARITY 1 FOR HASKELL 1.4
1014     doptM Opt_GlasgowExts                               `thenM` \ gla_exts ->
1015
1016         -- Check that the class is unary, unless GlaExs
1017     checkTc (notNull tyvars)    (nullaryClassErr cls)   `thenM_`
1018     checkTc (gla_exts || unary) (classArityErr cls)     `thenM_`
1019
1020         -- Check the super-classes
1021     checkValidTheta (ClassSCCtxt (className cls)) theta `thenM_`
1022
1023         -- Check the class operations
1024     mappM_ check_op op_stuff            `thenM_`
1025
1026         -- Check that if the class has generic methods, then the
1027         -- class has only one parameter.  We can't do generic
1028         -- multi-parameter type classes!
1029     checkTc (unary || no_generics) (genericMultiParamErr cls)
1030
1031   where
1032     (tyvars, theta, _, op_stuff) = classBigSig cls
1033     unary       = isSingleton tyvars
1034     no_generics = null [() | (_, GenDefMeth) <- op_stuff]
1035
1036     check_op (sel_id, dm)
1037         = checkValidTheta SigmaCtxt (tail theta)        `thenM_`
1038                 -- The 'tail' removes the initial (C a) from the
1039                 -- class itself, leaving just the method type
1040
1041           checkValidType (FunSigCtxt op_name) tau       `thenM_`
1042
1043                 -- Check that for a generic method, the type of
1044                 -- the method is sufficiently simple
1045           checkTc (dm /= GenDefMeth || validGenericMethodType op_ty)
1046                   (badGenericMethodType op_name op_ty)
1047         where
1048           op_name = idName sel_id
1049           op_ty   = idType sel_id
1050           (_,theta,tau) = tcSplitSigmaTy op_ty
1051
1052 nullaryClassErr cls
1053   = ptext SLIT("No parameters for class")  <+> quotes (ppr cls)
1054
1055 classArityErr cls
1056   = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls),
1057           parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))]
1058
1059 genericMultiParamErr clas
1060   = ptext SLIT("The multi-parameter class") <+> quotes (ppr clas) <+>
1061     ptext SLIT("cannot have generic methods")
1062
1063 badGenericMethodType op op_ty
1064   = hang (ptext SLIT("Generic method type is too complex"))
1065        4 (vcat [ppr op <+> dcolon <+> ppr op_ty,
1066                 ptext SLIT("You can only use type variables, arrows, and tuples")])
1067 \end{code}
1068
1069
1070 %************************************************************************
1071 %*                                                                      *
1072 \subsection{Checking for a decent instance head type}
1073 %*                                                                      *
1074 %************************************************************************
1075
1076 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1077 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1078
1079 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1080 flag is on, or (2)~the instance is imported (they must have been
1081 compiled elsewhere). In these cases, we let them go through anyway.
1082
1083 We can also have instances for functions: @instance Foo (a -> b) ...@.
1084
1085 \begin{code}
1086 checkValidInstHead :: Type -> TcM (Class, [TcType])
1087
1088 checkValidInstHead ty   -- Should be a source type
1089   = case tcSplitPredTy_maybe ty of {
1090         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1091         Just pred ->
1092
1093     case getClassPredTys_maybe pred of {
1094         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1095         Just (clas,tys) ->
1096
1097     getDOpts                                    `thenM` \ dflags ->
1098     mappM_ check_arg_type tys                   `thenM_`
1099     check_inst_head dflags clas tys             `thenM_`
1100     returnM (clas, tys)
1101     }}
1102
1103 check_inst_head dflags clas tys
1104   |     -- CCALL CHECK
1105         -- A user declaration of a CCallable/CReturnable instance
1106         -- must be for a "boxed primitive" type.
1107         (clas `hasKey` cCallableClassKey
1108             && not (ccallable_type first_ty))
1109   ||    (clas `hasKey` cReturnableClassKey
1110             && not (creturnable_type first_ty))
1111   = failWithTc (nonBoxedPrimCCallErr clas first_ty)
1112
1113         -- If GlasgowExts then check at least one isn't a type variable
1114   | dopt Opt_GlasgowExts dflags
1115   = check_tyvars dflags clas tys
1116
1117         -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1118   | isSingleton tys,
1119     Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1120     not (isSynTyCon tycon),             -- ...but not a synonym
1121     all tcIsTyVarTy arg_tys,            -- Applied to type variables
1122     equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1123           -- This last condition checks that all the type variables are distinct
1124   = returnM ()
1125
1126   | otherwise
1127   = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1128
1129   where
1130     (first_ty : _)       = tys
1131
1132     ccallable_type   ty = isFFIArgumentTy dflags PlayRisky ty
1133     creturnable_type ty = isFFIImportResultTy dflags ty
1134
1135     head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1136                              text "where T is not a synonym, and a,b,c are distinct type variables")
1137
1138 check_tyvars dflags clas tys
1139         -- Check that at least one isn't a type variable
1140         -- unless -fallow-undecideable-instances
1141   | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1142   | not (all tcIsTyVarTy tys)                 = returnM ()
1143   | otherwise                                 = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1144   where
1145     msg =  parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1146                    $$ undecidableMsg)
1147
1148 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1149 \end{code}
1150
1151 \begin{code}
1152 instTypeErr pp_ty msg
1153   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1154          nest 4 msg]
1155
1156 nonBoxedPrimCCallErr clas inst_ty
1157   = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
1158          4 (pprClassPred clas [inst_ty])
1159 \end{code}