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