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