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