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