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,
  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     WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
 449
 450     returnNF_Tc immut_tv
 451 \end{code}
 452
 453
 454 %************************************************************************
 455 %*                                                                      *
 456 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
 457 %*                                                                      *
 458 %*              For internal use only!                                  *
 459 %*                                                                      *
 460 %************************************************************************
 461
 462 \begin{code}
 463 -- zonkType is used for Kinds as well
 464
 465 -- For unbound, mutable tyvars, zonkType uses the function given to it
 466 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 467 --      type variable and zonks the kind too
 468
 469 zonkType :: (TcTyVar -> NF_TcM Type)    -- What to do with unbound mutable type variables
 470                                         -- see zonkTcType, and zonkTcTypeToType
 471          -> TcType
 472          -> NF_TcM Type
 473 zonkType unbound_var_fn ty
 474   = go ty
 475   where
 476     go (TyConApp tycon tys)       = mapNF_Tc go tys     `thenNF_Tc` \ tys' ->
 477                                     returnNF_Tc (TyConApp tycon tys')
 478
 479     go (NoteTy (SynNote ty1) ty2) = go ty1              `thenNF_Tc` \ ty1' ->
 480                                     go ty2              `thenNF_Tc` \ ty2' ->
 481                                     returnNF_Tc (NoteTy (SynNote ty1') ty2')
 482
 483     go (NoteTy (FTVNote _) ty2)   = go ty2      -- Discard free-tyvar annotations
 484
 485     go (SourceTy p)               = go_pred p           `thenNF_Tc` \ p' ->
 486                                     returnNF_Tc (SourceTy p')
 487
 488     go (FunTy arg res)            = go arg              `thenNF_Tc` \ arg' ->
 489                                     go res              `thenNF_Tc` \ res' ->
 490                                     returnNF_Tc (FunTy arg' res')
 491
 492     go (AppTy fun arg)            = go fun              `thenNF_Tc` \ fun' ->
 493                                     go arg              `thenNF_Tc` \ arg' ->
 494                                     returnNF_Tc (mkAppTy fun' arg')
 495                 -- NB the mkAppTy; we might have instantiated a
 496                 -- type variable to a type constructor, so we need
 497                 -- to pull the TyConApp to the top.
 498
 499         -- The two interesting cases!
 500     go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn tyvar
 501
 502     go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar   `thenNF_Tc` \ tyvar' ->
 503                              go ty                      `thenNF_Tc` \ ty' ->
 504                              returnNF_Tc (ForAllTy tyvar' ty')
 505
 506     go_pred (ClassP c tys) = mapNF_Tc go tys    `thenNF_Tc` \ tys' ->
 507                              returnNF_Tc (ClassP c tys')
 508     go_pred (NType tc tys) = mapNF_Tc go tys    `thenNF_Tc` \ tys' ->
 509                              returnNF_Tc (NType tc tys')
 510     go_pred (IParam n ty)  = go ty              `thenNF_Tc` \ ty' ->
 511                              returnNF_Tc (IParam n ty')
 512
 513 zonkTyVar :: (TcTyVar -> NF_TcM Type)           -- What to do for an unbound mutable variable
 514           -> TcTyVar -> NF_TcM TcType
 515 zonkTyVar unbound_var_fn tyvar
 516   | not (isMutTyVar tyvar)      -- Not a mutable tyvar.  This can happen when
 517                                 -- zonking a forall type, when the bound type variable
 518                                 -- needn't be mutable
 519   = ASSERT( isTyVar tyvar )             -- Should not be any immutable kind vars
 520     returnNF_Tc (TyVarTy tyvar)
 521
 522   | otherwise
 523   =  getTcTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
 524      case maybe_ty of
 525           Nothing       -> unbound_var_fn tyvar                 -- Mutable and unbound
 526           Just other_ty -> zonkType unbound_var_fn other_ty     -- Bound
 527 \end{code}
 528
 529
 530
 531 %************************************************************************
 532 %*                                                                      *
 533 \subsection{Checking a user type}
 534 %*                                                                      *
 535 %************************************************************************
 536
 537 When dealing with a user-written type, we first translate it from an HsType
 538 to a Type, performing kind checking, and then check various things that should
 539 be true about it.  We don't want to perform these checks at the same time
 540 as the initial translation because (a) they are unnecessary for interface-file
 541 types and (b) when checking a mutually recursive group of type and class decls,
 542 we can't "look" at the tycons/classes yet.  Also, the checks are are rather
 543 diverse, and used to really mess up the other code.
 544
 545 One thing we check for is 'rank'.
 546
 547         Rank 0:         monotypes (no foralls)
 548         Rank 1:         foralls at the front only, Rank 0 inside
 549         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
 550
 551         basic ::= tyvar | T basic ... basic
 552
 553         r2  ::= forall tvs. cxt => r2a
 554         r2a ::= r1 -> r2a | basic
 555         r1  ::= forall tvs. cxt => r0
 556         r0  ::= r0 -> r0 | basic
 557
 558 Another thing is to check that type synonyms are saturated.
 559 This might not necessarily show up in kind checking.
 560         type A i = i
 561         data T k = MkT (k Int)
 562         f :: T A        -- BAD!
 563
 564
 565 \begin{code}
 566 data UserTypeCtxt
 567   = FunSigCtxt Name     -- Function type signature
 568   | ExprSigCtxt         -- Expression type signature
 569   | ConArgCtxt Name     -- Data constructor argument
 570   | TySynCtxt Name      -- RHS of a type synonym decl
 571   | GenPatCtxt          -- Pattern in generic decl
 572                         --      f{| a+b |} (Inl x) = ...
 573   | PatSigCtxt          -- Type sig in pattern
 574                         --      f (x::t) = ...
 575   | ResSigCtxt          -- Result type sig
 576                         --      f x :: t = ....
 577   | ForSigCtxt Name     -- Foreign inport or export signature
 578   | RuleSigCtxt Name    -- Signature on a forall'd variable in a RULE
 579
 580 -- Notes re TySynCtxt
 581 -- We allow type synonyms that aren't types; e.g.  type List = []
 582 --
 583 -- If the RHS mentions tyvars that aren't in scope, we'll
 584 -- quantify over them:
 585 --      e.g.    type T = a->a
 586 -- will become  type T = forall a. a->a
 587 --
 588 -- With gla-exts that's right, but for H98 we should complain.
 589
 590
 591 pprUserTypeCtxt (FunSigCtxt n)  = ptext SLIT("the type signature for") <+> quotes (ppr n)
 592 pprUserTypeCtxt ExprSigCtxt     = ptext SLIT("an expression type signature")
 593 pprUserTypeCtxt (ConArgCtxt c)  = ptext SLIT("the type of constructor") <+> quotes (ppr c)
 594 pprUserTypeCtxt (TySynCtxt c)   = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
 595 pprUserTypeCtxt GenPatCtxt      = ptext SLIT("the type pattern of a generic definition")
 596 pprUserTypeCtxt PatSigCtxt      = ptext SLIT("a pattern type signature")
 597 pprUserTypeCtxt ResSigCtxt      = ptext SLIT("a result type signature")
 598 pprUserTypeCtxt (ForSigCtxt n)  = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
 599 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
 600 \end{code}
 601
 602 \begin{code}
 603 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 604 -- Checks that the type is valid for the given context
 605 checkValidType ctxt ty
 606   = doptsTc Opt_GlasgowExts     `thenNF_Tc` \ gla_exts ->
 607     let
 608         rank | gla_exts = Arbitrary
 609              | otherwise
 610              = case ctxt of     -- Haskell 98
 611                  GenPatCtxt     -> Rank 0
 612                  PatSigCtxt     -> Rank 0
 613                  ResSigCtxt     -> Rank 0
 614                  TySynCtxt _    -> Rank 0
 615                  ExprSigCtxt    -> Rank 1
 616                  FunSigCtxt _   -> Rank 1
 617                  ConArgCtxt _   -> Rank 1       -- We are given the type of the entire
 618                                                 -- constructor, hence rank 1
 619                  ForSigCtxt _   -> Rank 1
 620                  RuleSigCtxt _  -> Rank 1
 621
 622         actual_kind = typeKind ty
 623
 624         actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
 625
 626         kind_ok = case ctxt of
 627                         TySynCtxt _  -> True    -- Any kind will do
 628                         GenPatCtxt   -> actual_kind_is_lifted
 629                         ForSigCtxt _ -> actual_kind_is_lifted
 630                         other        -> isTypeKind actual_kind
 631
 632         ubx_tup | not gla_exts = UT_NotOk
 633                 | otherwise    = case ctxt of
 634                                    TySynCtxt _ -> UT_Ok
 635                                    other       -> UT_NotOk
 636                 -- Unboxed tuples ok in function results,
 637                 -- but for type synonyms we allow them even at
 638                 -- top level
 639     in
 640     tcAddErrCtxt (checkTypeCtxt ctxt ty)        $
 641
 642         -- Check that the thing has kind Type, and is lifted if necessary
 643     checkTc kind_ok (kindErr actual_kind)       `thenTc_`
 644
 645         -- Check the internal validity of the type itself
 646     check_poly_type rank ubx_tup ty
 647
 648
 649 checkTypeCtxt ctxt ty
 650   = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
 651           ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
 652
 653         -- Hack alert.  If there are no tyvars, (ppr sigma_ty) will print
 654         -- something strange like {Eq k} -> k -> k, because there is no
 655         -- ForAll at the top of the type.  Since this is going to the user
 656         -- we want it to look like a proper Haskell type even then; hence the hack
 657         --
 658         -- This shows up in the complaint about
 659         --      case C a where
 660         --        op :: Eq a => a -> a
 661 ppr_ty ty | null forall_tvs && notNull theta = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
 662           | otherwise                        = ppr ty
 663           where
 664             (forall_tvs, theta, tau) = tcSplitSigmaTy ty
 665 \end{code}
 666
 667
 668 \begin{code}
 669 data Rank = Rank Int | Arbitrary
 670
 671 decRank :: Rank -> Rank
 672 decRank Arbitrary = Arbitrary
 673 decRank (Rank n)  = Rank (n-1)
 674
 675 ----------------------------------------
 676 data UbxTupFlag = UT_Ok | UT_NotOk
 677         -- The "Ok" version means "ok if -fglasgow-exts is on"
 678
 679 ----------------------------------------
 680 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 681 check_poly_type (Rank 0) ubx_tup ty
 682   = check_tau_type (Rank 0) ubx_tup ty
 683
 684 check_poly_type rank ubx_tup ty
 685   = let
 686         (tvs, theta, tau) = tcSplitSigmaTy ty
 687     in
 688     check_valid_theta SigmaCtxt theta           `thenTc_`
 689     check_tau_type (decRank rank) ubx_tup tau   `thenTc_`
 690     checkFreeness tvs theta                     `thenTc_`
 691     checkAmbiguity tvs theta (tyVarsOfType tau)
 692
 693 ----------------------------------------
 694 check_arg_type :: Type -> TcM ()
 695 -- The sort of type that can instantiate a type variable,
 696 -- or be the argument of a type constructor.
 697 -- Not an unboxed tuple, not a forall.
 698 -- Other unboxed types are very occasionally allowed as type
 699 -- arguments depending on the kind of the type constructor
 700 --
 701 -- For example, we want to reject things like:
 702 --
 703 --      instance Ord a => Ord (forall s. T s a)
 704 -- and
 705 --      g :: T s (forall b.b)
 706 --
 707 -- NB: unboxed tuples can have polymorphic or unboxed args.
 708 --     This happens in the workers for functions returning
 709 --     product types with polymorphic components.
 710 --     But not in user code.
 711 -- Anyway, they are dealt with by a special case in check_tau_type
 712
 713 check_arg_type ty
 714   = check_tau_type (Rank 0) UT_NotOk ty         `thenTc_`
 715     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 716
 717 ----------------------------------------
 718 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 719 -- Rank is allowed rank for function args
 720 -- No foralls otherwise
 721
 722 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
 723 check_tau_type rank ubx_tup (SourceTy sty)    = getDOptsTc              `thenNF_Tc` \ dflags ->
 724                                                 check_source_ty dflags TypeCtxt sty
 725 check_tau_type rank ubx_tup (TyVarTy _)       = returnTc ()
 726 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
 727   = check_poly_type rank UT_NotOk arg_ty        `thenTc_`
 728     check_tau_type  rank UT_Ok    res_ty
 729
 730 check_tau_type rank ubx_tup (AppTy ty1 ty2)
 731   = check_arg_type ty1 `thenTc_` check_arg_type ty2
 732
 733 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
 734         -- Synonym notes are built only when the synonym is
 735         -- saturated (see Type.mkSynTy)
 736   = doptsTc Opt_GlasgowExts                     `thenNF_Tc` \ gla_exts ->
 737     (if gla_exts then
 738         -- If -fglasgow-exts then don't check the 'note' part.
 739         -- This  allows us to instantiate a synonym defn with a
 740         -- for-all type, or with a partially-applied type synonym.
 741         --      e.g.   type T a b = a
 742         --             type S m   = m ()
 743         --             f :: S (T Int)
 744         -- Here, T is partially applied, so it's illegal in H98.
 745         -- But if you expand S first, then T we get just
 746         --             f :: Int
 747         -- which is fine.
 748         returnTc ()
 749     else
 750         -- For H98, do check the un-expanded part
 751         check_tau_type rank ubx_tup syn
 752     )                                           `thenTc_`
 753
 754     check_tau_type rank ubx_tup ty
 755
 756 check_tau_type rank ubx_tup (NoteTy other_note ty)
 757   = check_tau_type rank ubx_tup ty
 758
 759 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
 760   | isSynTyCon tc
 761   =     -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
 762         -- synonym application, leaving it to checkValidType (i.e. right here)
 763         -- to find the error
 764     checkTc syn_arity_ok arity_msg      `thenTc_`
 765     mapTc_ check_arg_type tys
 766
 767   | isUnboxedTupleTyCon tc
 768   = doptsTc Opt_GlasgowExts                     `thenNF_Tc` \ gla_exts ->
 769     checkTc (ubx_tup_ok gla_exts) ubx_tup_msg   `thenTc_`
 770     mapTc_ (check_tau_type (Rank 0) UT_Ok) tys
 771                         -- Args are allowed to be unlifted, or
 772                         -- more unboxed tuples, so can't use check_arg_ty
 773
 774   | otherwise
 775   = mapTc_ check_arg_type tys
 776
 777   where
 778     ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
 779
 780     syn_arity_ok = tc_arity <= n_args
 781                 -- It's OK to have an *over-applied* type synonym
 782                 --      data Tree a b = ...
 783                 --      type Foo a = Tree [a]
 784                 --      f :: Foo a b -> ...
 785     n_args    = length tys
 786     tc_arity  = tyConArity tc
 787
 788     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
 789     ubx_tup_msg = ubxArgTyErr ty
 790
 791 ----------------------------------------
 792 forAllTyErr     ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
 793 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
 794 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
 795 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 796 \end{code}
 797
 798 Check for ambiguity
 799 ~~~~~~~~~~~~~~~~~~~
 800           forall V. P => tau
 801 is ambiguous if P contains generic variables
 802 (i.e. one of the Vs) that are not mentioned in tau
 803
 804 However, we need to take account of functional dependencies
 805 when we speak of 'mentioned in tau'.  Example:
 806         class C a b | a -> b where ...
 807 Then the type
 808         forall x y. (C x y) => x
 809 is not ambiguous because x is mentioned and x determines y
 810
 811 NB; the ambiguity check is only used for *user* types, not for types
 812 coming from inteface files.  The latter can legitimately have
 813 ambiguous types. Example
 814
 815    class S a where s :: a -> (Int,Int)
 816    instance S Char where s _ = (1,1)
 817    f:: S a => [a] -> Int -> (Int,Int)
 818    f (_::[a]) x = (a*x,b)
 819         where (a,b) = s (undefined::a)
 820
 821 Here the worker for f gets the type
 822         fw :: forall a. S a => Int -> (# Int, Int #)
 823
 824 If the list of tv_names is empty, we have a monotype, and then we
 825 don't need to check for ambiguity either, because the test can't fail
 826 (see is_ambig).
 827
 828 \begin{code}
 829 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
 830 checkAmbiguity forall_tyvars theta tau_tyvars
 831   = mapTc_ complain (filter is_ambig theta)
 832   where
 833     complain pred     = addErrTc (ambigErr pred)
 834     extended_tau_vars = grow theta tau_tyvars
 835     is_ambig pred     = any ambig_var (varSetElems (tyVarsOfPred pred))
 836
 837     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
 838                         not (ct_var `elemVarSet` extended_tau_vars)
 839
 840     is_free ct_var    = not (ct_var `elem` forall_tyvars)
 841
 842 ambigErr pred
 843   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
 844          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
 845                  ptext SLIT("must be reachable from the type after the '=>'"))]
 846 \end{code}
 847
 848 In addition, GHC insists that at least one type variable
 849 in each constraint is in V.  So we disallow a type like
 850         forall a. Eq b => b -> b
 851 even in a scope where b is in scope.
 852
 853 \begin{code}
 854 checkFreeness forall_tyvars theta
 855   = mapTc_ complain (filter is_free theta)
 856   where
 857     is_free pred     =  not (isIPPred pred)
 858                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
 859     bound_var ct_var = ct_var `elem` forall_tyvars
 860     complain pred    = addErrTc (freeErr pred)
 861
 862 freeErr pred
 863   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
 864                    ptext SLIT("are already in scope"),
 865          nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
 866     ]
 867 \end{code}
 868
 869
 870 %************************************************************************
 871 %*                                                                      *
 872 \subsection{Checking a theta or source type}
 873 %*                                                                      *
 874 %************************************************************************
 875
 876 \begin{code}
 877 data SourceTyCtxt
 878   = ClassSCCtxt Name    -- Superclasses of clas
 879   | SigmaCtxt           -- Context of a normal for-all type
 880   | DataTyCtxt Name     -- Context of a data decl
 881   | TypeCtxt            -- Source type in an ordinary type
 882   | InstThetaCtxt       -- Context of an instance decl
 883   | InstHeadCtxt        -- Head of an instance decl
 884
 885 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
 886 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
 887 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
 888 pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
 889 pprSourceTyCtxt InstHeadCtxt    = ptext SLIT("the head of an instance declaration")
 890 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
 891 \end{code}
 892
 893 \begin{code}
 894 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
 895 checkValidTheta ctxt theta
 896   = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
 897
 898 -------------------------
 899 check_valid_theta ctxt []
 900   = returnTc ()
 901 check_valid_theta ctxt theta
 902   = getDOptsTc                                  `thenNF_Tc` \ dflags ->
 903     warnTc (notNull dups) (dupPredWarn dups)    `thenNF_Tc_`
 904     mapTc_ (check_source_ty dflags ctxt) theta
 905   where
 906     (_,dups) = removeDups tcCmpPred theta
 907
 908 -------------------------
 909 check_source_ty dflags ctxt pred@(ClassP cls tys)
 910   =     -- Class predicates are valid in all contexts
 911     mapTc_ check_arg_type tys           `thenTc_`
 912     checkTc (arity == n_tys) arity_err          `thenTc_`
 913     checkTc (all tyvar_head tys || arby_preds_ok)
 914             (predTyVarErr pred $$ how_to_allow)
 915
 916   where
 917     class_name = className cls
 918     arity      = classArity cls
 919     n_tys      = length tys
 920     arity_err  = arityErr "Class" class_name arity n_tys
 921
 922     arby_preds_ok = case ctxt of
 923                         InstHeadCtxt  -> True   -- We check for instance-head formation
 924                                                 -- in checkValidInstHead
 925                         InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
 926                         other         -> dopt Opt_GlasgowExts               dflags
 927
 928     how_to_allow = case ctxt of
 929                      InstHeadCtxt  -> empty     -- Should not happen
 930                      InstThetaCtxt -> parens undecidableMsg
 931                      other         -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 932
 933 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
 934         -- Implicit parameters only allows in type
 935         -- signatures; not in instance decls, superclasses etc
 936         -- The reason for not allowing implicit params in instances is a bit subtle
 937         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
 938         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
 939         -- discharge all the potential usas of the ?x in e.   For example, a
 940         -- constraint Foo [Int] might come out of e,and applying the
 941         -- instance decl would show up two uses of ?x.
 942
 943 check_source_ty dflags TypeCtxt  (NType tc tys)   = mapTc_ check_arg_type tys
 944
 945 -- Catch-all
 946 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 947
 948 -------------------------
 949 tyvar_head ty                   -- Haskell 98 allows predicates of form
 950   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
 951   | otherwise                   -- where a is a type variable
 952   = case tcSplitAppTy_maybe ty of
 953         Just (ty, _) -> tyvar_head ty
 954         Nothing      -> False
 955 \end{code}
 956
 957 \begin{code}
 958 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
 959 predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
 960 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
 961
 962 checkThetaCtxt ctxt theta
 963   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
 964           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 965 \end{code}
 966
 967
 968 %************************************************************************
 969 %*                                                                      *
 970 \subsection{Validity check for TyCons}
 971 %*                                                                      *
 972 %************************************************************************
 973
 974 checkValidTyCon is called once the mutually-recursive knot has been
 975 tied, so we can look at things freely.
 976
 977 \begin{code}
 978 checkValidTyCon :: TyCon -> TcM ()
 979 checkValidTyCon tc
 980   | isSynTyCon tc = checkValidType (TySynCtxt name) syn_rhs
 981   | otherwise
 982   =     -- Check the context on the data decl
 983     checkValidTheta (DataTyCtxt name) (tyConTheta tc)   `thenTc_`
 984
 985         -- Check arg types of data constructors
 986     mapTc_ checkValidDataCon data_cons                  `thenTc_`
 987
 988         -- Check that fields with the same name share a type
 989     mapTc_ check_fields groups
 990
 991   where
 992     name         = tyConName tc
 993     (_, syn_rhs) = getSynTyConDefn tc
 994     data_cons    = tyConDataCons tc
 995
 996     fields = [field | con <- data_cons, field <- dataConFieldLabels con]
 997     groups = equivClasses cmp_name fields
 998     cmp_name field1 field2 = fieldLabelName field1 `compare` fieldLabelName field2
 999
1000     check_fields fields@(first_field_label : other_fields)
1001         -- These fields all have the same name, but are from
1002         -- different constructors in the data type
1003         =       -- Check that all the fields in the group have the same type
1004                 -- NB: this check assumes that all the constructors of a given
1005                 -- data type use the same type variables
1006           checkTc (all (tcEqType field_ty) other_tys) (fieldTypeMisMatch field_name)
1007         where
1008             field_ty   = fieldLabelType first_field_label
1009             field_name = fieldLabelName first_field_label
1010             other_tys  = map fieldLabelType other_fields
1011
1012 checkValidDataCon :: DataCon -> TcM ()
1013 checkValidDataCon con
1014   = checkValidType ctxt (idType (dataConWrapId con))    `thenTc_`
1015                 -- This checks the argument types and
1016                 -- ambiguity of the existential context (if any)
1017     tcAddErrCtxt (existentialCtxt con)
1018                  (checkFreeness ex_tvs ex_theta)
1019   where
1020     ctxt = ConArgCtxt (dataConName con)
1021     (_, _, ex_tvs, ex_theta, _, _) = dataConSig con
1022
1023
1024 fieldTypeMisMatch field_name
1025   = sep [ptext SLIT("Different constructors give different types for field"), quotes (ppr field_name)]
1026
1027 existentialCtxt con = ptext SLIT("When checking the existential context of constructor")
1028                       <+> quotes (ppr con)
1029 \end{code}
1030
1031
1032 checkValidClass is called once the mutually-recursive knot has been
1033 tied, so we can look at things freely.
1034
1035 \begin{code}
1036 checkValidClass :: Class -> TcM ()
1037 checkValidClass cls
1038   =     -- CHECK ARITY 1 FOR HASKELL 1.4
1039     doptsTc Opt_GlasgowExts                             `thenTc` \ gla_exts ->
1040
1041         -- Check that the class is unary, unless GlaExs
1042     checkTc (notNull tyvars)    (nullaryClassErr cls)   `thenTc_`
1043     checkTc (gla_exts || unary) (classArityErr cls)     `thenTc_`
1044
1045         -- Check the super-classes
1046     checkValidTheta (ClassSCCtxt (className cls)) theta `thenTc_`
1047
1048         -- Check the class operations
1049     mapTc_ check_op op_stuff            `thenTc_`
1050
1051         -- Check that if the class has generic methods, then the
1052         -- class has only one parameter.  We can't do generic
1053         -- multi-parameter type classes!
1054     checkTc (unary || no_generics) (genericMultiParamErr cls)
1055
1056   where
1057     (tyvars, theta, _, op_stuff) = classBigSig cls
1058     unary       = isSingleton tyvars
1059     no_generics = null [() | (_, GenDefMeth) <- op_stuff]
1060
1061     check_op (sel_id, dm)
1062         = checkValidTheta SigmaCtxt (tail theta)        `thenTc_`
1063                 -- The 'tail' removes the initial (C a) from the
1064                 -- class itself, leaving just the method type
1065
1066           checkValidType (FunSigCtxt op_name) tau       `thenTc_`
1067
1068                 -- Check that for a generic method, the type of
1069                 -- the method is sufficiently simple
1070           checkTc (dm /= GenDefMeth || validGenericMethodType op_ty)
1071                   (badGenericMethodType op_name op_ty)
1072         where
1073           op_name = idName sel_id
1074           op_ty   = idType sel_id
1075           (_,theta,tau) = tcSplitSigmaTy op_ty
1076
1077 nullaryClassErr cls
1078   = ptext SLIT("No parameters for class")  <+> quotes (ppr cls)
1079
1080 classArityErr cls
1081   = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls),
1082           parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))]
1083
1084 genericMultiParamErr clas
1085   = ptext SLIT("The multi-parameter class") <+> quotes (ppr clas) <+>
1086     ptext SLIT("cannot have generic methods")
1087
1088 badGenericMethodType op op_ty
1089   = hang (ptext SLIT("Generic method type is too complex"))
1090        4 (vcat [ppr op <+> dcolon <+> ppr op_ty,
1091                 ptext SLIT("You can only use type variables, arrows, and tuples")])
1092 \end{code}
1093
1094
1095 %************************************************************************
1096 %*                                                                      *
1097 \subsection{Checking for a decent instance head type}
1098 %*                                                                      *
1099 %************************************************************************
1100
1101 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1102 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1103
1104 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1105 flag is on, or (2)~the instance is imported (they must have been
1106 compiled elsewhere). In these cases, we let them go through anyway.
1107
1108 We can also have instances for functions: @instance Foo (a -> b) ...@.
1109
1110 \begin{code}
1111 checkValidInstHead :: Type -> TcM (Class, [TcType])
1112
1113 checkValidInstHead ty   -- Should be a source type
1114   = case tcSplitPredTy_maybe ty of {
1115         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1116         Just pred ->
1117
1118     case getClassPredTys_maybe pred of {
1119         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1120         Just (clas,tys) ->
1121
1122     getDOptsTc                                  `thenNF_Tc` \ dflags ->
1123     mapTc_ check_arg_type tys                   `thenTc_`
1124     check_inst_head dflags clas tys             `thenTc_`
1125     returnTc (clas, tys)
1126     }}
1127
1128 check_inst_head dflags clas tys
1129   |     -- CCALL CHECK
1130         -- A user declaration of a CCallable/CReturnable instance
1131         -- must be for a "boxed primitive" type.
1132         (clas `hasKey` cCallableClassKey
1133             && not (ccallable_type first_ty))
1134   ||    (clas `hasKey` cReturnableClassKey
1135             && not (creturnable_type first_ty))
1136   = failWithTc (nonBoxedPrimCCallErr clas first_ty)
1137
1138         -- If GlasgowExts then check at least one isn't a type variable
1139   | dopt Opt_GlasgowExts dflags
1140   = check_tyvars dflags clas tys
1141
1142         -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1143   | isSingleton tys,
1144     Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1145     not (isSynTyCon tycon),             -- ...but not a synonym
1146     all tcIsTyVarTy arg_tys,            -- Applied to type variables
1147     equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1148           -- This last condition checks that all the type variables are distinct
1149   = returnTc ()
1150
1151   | otherwise
1152   = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1153
1154   where
1155     (first_ty : _)       = tys
1156
1157     ccallable_type   ty = isFFIArgumentTy dflags PlayRisky ty
1158     creturnable_type ty = isFFIImportResultTy dflags ty
1159
1160     head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1161                              text "where T is not a synonym, and a,b,c are distinct type variables")
1162
1163 check_tyvars dflags clas tys
1164         -- Check that at least one isn't a type variable
1165         -- unless -fallow-undecideable-instances
1166   | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
1167   | not (all tcIsTyVarTy tys)                 = returnTc ()
1168   | otherwise                                 = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1169   where
1170     msg =  parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1171                    $$ undecidableMsg)
1172
1173 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1174 \end{code}
1175
1176 \begin{code}
1177 instTypeErr pp_ty msg
1178   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1179          nest 4 msg]
1180
1181 nonBoxedPrimCCallErr clas inst_ty
1182   = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
1183          4 (pprClassPred clas [inst_ty])
1184 \end{code}