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