ghc/compiler/typecheck/TcMType.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section{Monadic type operations}
   5
   6 This module contains monadic operations over types that contain mutable type variables
   7
   8 \begin{code}
   9 module TcMType (
  10   TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
  11
  12   --------------------------------
  13   -- Creating new mutable type variables
  14   newTyVar,
  15   newTyVarTy,           -- Kind -> NF_TcM TcType
  16   newTyVarTys,          -- Int -> Kind -> NF_TcM [TcType]
  17   newKindVar, newKindVars, newBoxityVar,
  18   putTcTyVar, getTcTyVar,
  19
  20   newHoleTyVarTy, readHoleResult, zapToType,
  21
  22   --------------------------------
  23   -- Instantiation
  24   tcInstTyVar, tcInstTyVars, tcInstType,
  25
  26   --------------------------------
  27   -- Checking type validity
  28   Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
  29   SourceTyCtxt(..), checkValidTheta,
  30   checkValidTyCon, checkValidClass,
  31   checkValidInstHead, instTypeErr, checkAmbiguity,
  32
  33   --------------------------------
  34   -- Zonking
  35   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV,
  36   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
  37   zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,
  38
  39   ) where
  40
  41 #include "HsVersions.h"
  42
  43
  44 -- friends:
  45 import TypeRep          ( Type(..), SourceType(..), TyNote(..),  -- Friend; can see representation
  46                           Kind, ThetaType
  47                         )
  48 import TcType           ( TcType, TcThetaType, TcTauType, TcPredType,
  49                           TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
  50                           tcEqType, tcCmpPred,
  51                           tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
  52                           tcSplitTyConApp_maybe, tcSplitForAllTys,
  53                           tcIsTyVarTy, tcSplitSigmaTy,
  54                           isUnLiftedType, isIPPred, isHoleTyVar, isTyVarTy,
  55
  56                           mkAppTy, mkTyVarTy, mkTyVarTys,
  57                           tyVarsOfPred, getClassPredTys_maybe,
  58
  59                           liftedTypeKind, openTypeKind, defaultKind, superKind,
  60                           superBoxity, liftedBoxity, typeKind,
  61                           tyVarsOfType, tyVarsOfTypes,
  62                           eqKind, isTypeKind, isAnyTypeKind,
  63
  64                           isFFIArgumentTy, isFFIImportResultTy
  65                         )
  66 import qualified Type   ( splitFunTys )
  67 import Subst            ( Subst, mkTopTyVarSubst, substTy )
  68 import Class            ( Class, DefMeth(..), classArity, className, classBigSig )
  69 import TyCon            ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon,
  70                           tyConArity, tyConName, tyConKind, tyConTheta,
  71                           getSynTyConDefn, tyConDataCons )
  72 import DataCon          ( DataCon, dataConWrapId, dataConName, dataConSig, dataConFieldLabels )
  73 import FieldLabel       ( fieldLabelName, fieldLabelType )
  74 import PrimRep          ( PrimRep(VoidRep) )
  75 import Var              ( TyVar, idType, idName, tyVarKind, tyVarName, isTyVar, mkTyVar, isMutTyVar )
  76
  77 -- others:
  78 import Generics         ( validGenericMethodType )
  79 import TcMonad          -- TcType, amongst others
  80 import TysWiredIn       ( voidTy, listTyCon, tupleTyCon )
  81 import PrelNames        ( cCallableClassKey, cReturnableClassKey, hasKey )
  82 import ForeignCall      ( Safety(..) )
  83 import FunDeps          ( grow )
  84 import PprType          ( pprPred, pprSourceType, pprTheta, pprClassPred )
  85 import Name             ( Name, NamedThing(..), setNameUnique, mkSystemName,
  86                           mkInternalName, mkDerivedTyConOcc
  87                         )
  88 import VarSet
  89 import BasicTypes       ( Boxity(Boxed) )
  90 import CmdLineOpts      ( dopt, DynFlag(..) )
  91 import Unique           ( Uniquable(..) )
  92 import SrcLoc           ( noSrcLoc )
  93 import Util             ( nOfThem, isSingleton, equalLength, notNull )
  94 import ListSetOps       ( equivClasses, removeDups )
  95 import Outputable
  96 \end{code}
  97
  98
  99 %************************************************************************
 100 %*                                                                      *
 101 \subsection{New type variables}
 102 %*                                                                      *
 103 %************************************************************************
 104
 105 \begin{code}
 106 newTyVar :: Kind -> NF_TcM TcTyVar
 107 newTyVar kind
 108   = tcGetUnique         `thenNF_Tc` \ uniq ->
 109     tcNewMutTyVar (mkSystemName uniq FSLIT("t")) kind VanillaTv
 110
 111 newTyVarTy  :: Kind -> NF_TcM TcType
 112 newTyVarTy kind
 113   = newTyVar kind       `thenNF_Tc` \ tc_tyvar ->
 114     returnNF_Tc (TyVarTy tc_tyvar)
 115
 116 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
 117 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
 118
 119 newKindVar :: NF_TcM TcKind
 120 newKindVar
 121   = tcGetUnique                                                         `thenNF_Tc` \ uniq ->
 122     tcNewMutTyVar (mkSystemName uniq FSLIT("k")) superKind VanillaTv    `thenNF_Tc` \ kv ->
 123     returnNF_Tc (TyVarTy kv)
 124
 125 newKindVars :: Int -> NF_TcM [TcKind]
 126 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
 127
 128 newBoxityVar :: NF_TcM TcKind
 129 newBoxityVar
 130   = tcGetUnique                                                           `thenNF_Tc` \ uniq ->
 131     tcNewMutTyVar (mkSystemName uniq FSLIT("bx")) superBoxity VanillaTv  `thenNF_Tc` \ kv ->
 132     returnNF_Tc (TyVarTy kv)
 133 \end{code}
 134
 135
 136 %************************************************************************
 137 %*                                                                      *
 138 \subsection{'hole' type variables}
 139 %*                                                                      *
 140 %************************************************************************
 141
 142 \begin{code}
 143 newHoleTyVarTy :: NF_TcM TcType
 144   = tcGetUnique         `thenNF_Tc` \ uniq ->
 145     tcNewMutTyVar (mkSystemName uniq FSLIT("h")) openTypeKind HoleTv    `thenNF_Tc` \ tv ->
 146     returnNF_Tc (TyVarTy tv)
 147
 148 readHoleResult :: TcType -> NF_TcM TcType
 149 -- Read the answer out of a hole, constructed by newHoleTyVarTy
 150 readHoleResult (TyVarTy tv)
 151   = ASSERT( isHoleTyVar tv )
 152     getTcTyVar tv               `thenNF_Tc` \ maybe_res ->
 153     case maybe_res of
 154         Just ty -> returnNF_Tc ty
 155         Nothing ->  pprPanic "readHoleResult: empty" (ppr tv)
 156 readHoleResult ty = pprPanic "readHoleResult: not hole" (ppr ty)
 157
 158 zapToType :: TcType -> NF_TcM TcType
 159 zapToType (TyVarTy tv)
 160   | isHoleTyVar tv
 161   = getTcTyVar tv               `thenNF_Tc` \ maybe_res ->
 162     case maybe_res of
 163         Nothing -> newTyVarTy openTypeKind      `thenNF_Tc` \ ty ->
 164                    putTcTyVar tv ty             `thenNF_Tc_`
 165                    returnNF_Tc ty
 166         Just ty  -> returnNF_Tc ty      -- No need to loop; we never
 167                                         -- have chains of holes
 168
 169 zapToType other_ty = returnNF_Tc other_ty
 170 \end{code}
 171
 172 %************************************************************************
 173 %*                                                                      *
 174 \subsection{Type instantiation}
 175 %*                                                                      *
 176 %************************************************************************
 177
 178 Instantiating a bunch of type variables
 179
 180 \begin{code}
 181 tcInstTyVars :: TyVarDetails -> [TyVar]
 182              -> NF_TcM ([TcTyVar], [TcType], Subst)
 183
 184 tcInstTyVars tv_details tyvars
 185   = mapNF_Tc (tcInstTyVar tv_details) tyvars    `thenNF_Tc` \ tc_tyvars ->
 186     let
 187         tys = mkTyVarTys tc_tyvars
 188     in
 189     returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
 190                 -- Since the tyvars are freshly made,
 191                 -- they cannot possibly be captured by
 192                 -- any existing for-alls.  Hence mkTopTyVarSubst
 193
 194 tcInstTyVar tv_details tyvar
 195   = tcGetUnique                 `thenNF_Tc` \ uniq ->
 196     let
 197         name = setNameUnique (tyVarName tyvar) uniq
 198         -- Note that we don't change the print-name
 199         -- This won't confuse the type checker but there's a chance
 200         -- that two different tyvars will print the same way
 201         -- in an error message.  -dppr-debug will show up the difference
 202         -- Better watch out for this.  If worst comes to worst, just
 203         -- use mkSystemName.
 204     in
 205     tcNewMutTyVar name (tyVarKind tyvar) tv_details
 206
 207 tcInstType :: TyVarDetails -> TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
 208 -- tcInstType instantiates the outer-level for-alls of a TcType with
 209 -- fresh (mutable) type variables, splits off the dictionary part,
 210 -- and returns the pieces.
 211 tcInstType tv_details ty
 212   = case tcSplitForAllTys ty of
 213         ([],     rho) ->        -- There may be overloading despite no type variables;
 214                                 --      (?x :: Int) => Int -> Int
 215                          let
 216                            (theta, tau) = tcSplitPhiTy rho
 217                          in
 218                          returnNF_Tc ([], theta, tau)
 219
 220         (tyvars, rho) -> tcInstTyVars tv_details tyvars         `thenNF_Tc` \ (tyvars', _, tenv) ->
 221                          let
 222                            (theta, tau) = tcSplitPhiTy (substTy tenv rho)
 223                          in
 224                          returnNF_Tc (tyvars', theta, tau)
 225 \end{code}
 226
 227
 228 %************************************************************************
 229 %*                                                                      *
 230 \subsection{Putting and getting  mutable type variables}
 231 %*                                                                      *
 232 %************************************************************************
 233
 234 \begin{code}
 235 putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
 236 getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
 237 \end{code}
 238
 239 Putting is easy:
 240
 241 \begin{code}
 242 putTcTyVar tyvar ty
 243   | not (isMutTyVar tyvar)
 244   = pprTrace "putTcTyVar" (ppr tyvar) $
 245     returnNF_Tc ty
 246
 247   | otherwise
 248   = ASSERT( isMutTyVar tyvar )
 249     tcWriteMutTyVar tyvar (Just ty)     `thenNF_Tc_`
 250     returnNF_Tc ty
 251 \end{code}
 252
 253 Getting is more interesting.  The easy thing to do is just to read, thus:
 254
 255 \begin{verbatim}
 256 getTcTyVar tyvar = tcReadMutTyVar tyvar
 257 \end{verbatim}
 258
 259 But it's more fun to short out indirections on the way: If this
 260 version returns a TyVar, then that TyVar is unbound.  If it returns
 261 any other type, then there might be bound TyVars embedded inside it.
 262
 263 We return Nothing iff the original box was unbound.
 264
 265 \begin{code}
 266 getTcTyVar tyvar
 267   | not (isMutTyVar tyvar)
 268   = pprTrace "getTcTyVar" (ppr tyvar) $
 269     returnNF_Tc (Just (mkTyVarTy tyvar))
 270
 271   | otherwise
 272   = ASSERT2( isMutTyVar tyvar, ppr tyvar )
 273     tcReadMutTyVar tyvar                                `thenNF_Tc` \ maybe_ty ->
 274     case maybe_ty of
 275         Just ty -> short_out ty                         `thenNF_Tc` \ ty' ->
 276                    tcWriteMutTyVar tyvar (Just ty')     `thenNF_Tc_`
 277                    returnNF_Tc (Just ty')
 278
 279         Nothing    -> returnNF_Tc Nothing
 280
 281 short_out :: TcType -> NF_TcM TcType
 282 short_out ty@(TyVarTy tyvar)
 283   | not (isMutTyVar tyvar)
 284   = returnNF_Tc ty
 285
 286   | otherwise
 287   = tcReadMutTyVar tyvar        `thenNF_Tc` \ maybe_ty ->
 288     case maybe_ty of
 289         Just ty' -> short_out ty'                       `thenNF_Tc` \ ty' ->
 290                     tcWriteMutTyVar tyvar (Just ty')    `thenNF_Tc_`
 291                     returnNF_Tc ty'
 292
 293         other    -> returnNF_Tc ty
 294
 295 short_out other_ty = returnNF_Tc other_ty
 296 \end{code}
 297
 298
 299 %************************************************************************
 300 %*                                                                      *
 301 \subsection{Zonking -- the exernal interfaces}
 302 %*                                                                      *
 303 %************************************************************************
 304
 305 -----------------  Type variables
 306
 307 \begin{code}
 308 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
 309 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
 310
 311 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
 312 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars  `thenNF_Tc` \ tys ->
 313                            returnNF_Tc (tyVarsOfTypes tys)
 314
 315 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
 316 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
 317 \end{code}
 318
 319 -----------------  Types
 320
 321 \begin{code}
 322 zonkTcType :: TcType -> NF_TcM TcType
 323 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
 324
 325 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
 326 zonkTcTypes tys = mapNF_Tc zonkTcType tys
 327
 328 zonkTcClassConstraints cts = mapNF_Tc zonk cts
 329     where zonk (clas, tys)
 330             = zonkTcTypes tys   `thenNF_Tc` \ new_tys ->
 331               returnNF_Tc (clas, new_tys)
 332
 333 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
 334 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
 335
 336 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
 337 zonkTcPredType (ClassP c ts)
 338   = zonkTcTypes ts      `thenNF_Tc` \ new_ts ->
 339     returnNF_Tc (ClassP c new_ts)
 340 zonkTcPredType (IParam n t)
 341   = zonkTcType t        `thenNF_Tc` \ new_t ->
 342     returnNF_Tc (IParam n new_t)
 343 \end{code}
 344
 345 -------------------  These ...ToType, ...ToKind versions
 346                      are used at the end of type checking
 347
 348 \begin{code}
 349 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
 350 zonkKindEnv pairs
 351   = mapNF_Tc zonk_it pairs
 352  where
 353     zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
 354                               returnNF_Tc (name, kind)
 355
 356         -- When zonking a kind, we want to
 357         --      zonk a *kind* variable to (Type *)
 358         --      zonk a *boxity* variable to *
 359     zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind   = putTcTyVar kv liftedTypeKind
 360                              | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
 361                              | otherwise                         = pprPanic "zonkKindEnv" (ppr kv)
 362
 363 zonkTcTypeToType :: TcType -> NF_TcM Type
 364 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
 365   where
 366         -- Zonk a mutable but unbound type variable to an arbitrary type
 367         -- We know it's unbound even though we don't carry an environment,
 368         -- because at the binding site for a type variable we bind the
 369         -- mutable tyvar to a fresh immutable one.  So the mutable store
 370         -- plays the role of an environment.  If we come across a mutable
 371         -- type variable that isn't so bound, it must be completely free.
 372     zonk_unbound_tyvar tv = putTcTyVar tv (mkArbitraryType tv)
 373
 374
 375 -- When the type checker finds a type variable with no binding,
 376 -- which means it can be instantiated with an arbitrary type, it
 377 -- usually instantiates it to Void.  Eg.
 378 --
 379 --      length []
 380 -- ===>
 381 --      length Void (Nil Void)
 382 --
 383 -- But in really obscure programs, the type variable might have
 384 -- a kind other than *, so we need to invent a suitably-kinded type.
 385 --
 386 -- This commit uses
 387 --      Void for kind *
 388 --      List for kind *->*
 389 --      Tuple for kind *->...*->*
 390 --
 391 -- which deals with most cases.  (Previously, it only dealt with
 392 -- kind *.)
 393 --
 394 -- In the other cases, it just makes up a TyCon with a suitable
 395 -- kind.  If this gets into an interface file, anyone reading that
 396 -- file won't understand it.  This is fixable (by making the client
 397 -- of the interface file make up a TyCon too) but it is tiresome and
 398 -- never happens, so I am leaving it
 399
 400 mkArbitraryType :: TcTyVar -> Type
 401 -- Make up an arbitrary type whose kind is the same as the tyvar.
 402 -- We'll use this to instantiate the (unbound) tyvar.
 403 mkArbitraryType tv
 404   | isAnyTypeKind kind = voidTy         -- The vastly common case
 405   | otherwise          = TyConApp tycon []
 406   where
 407     kind       = tyVarKind tv
 408     (args,res) = Type.splitFunTys kind  -- Kinds are simple; use Type.splitFunTys
 409
 410     tycon | kind `eqKind` tyConKind listTyCon   -- *->*
 411           = listTyCon                           -- No tuples this size
 412
 413           | all isTypeKind args && isTypeKind res
 414           = tupleTyCon Boxed (length args)      -- *-> ... ->*->*
 415
 416           | otherwise
 417           = pprTrace "Urk! Inventing strangely-kinded void TyCon:" (ppr tc_name $$ ppr kind) $
 418             mkPrimTyCon tc_name kind 0 [] VoidRep
 419                 -- Same name as the tyvar, apart from making it start with a colon (sigh)
 420                 -- I dread to think what will happen if this gets out into an
 421                 -- interface file.  Catastrophe likely.  Major sigh.
 422
 423     tc_name = mkInternalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
 424
 425 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
 426 -- of a type variable, at the *end* of type checking.  It changes
 427 -- the *mutable* type variable into an *immutable* one.
 428 --
 429 -- It does this by making an immutable version of tv and binds tv to it.
 430 -- Now any bound occurences of the original type variable will get
 431 -- zonked to the immutable version.
 432
 433 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
 434 zonkTcTyVarToTyVar tv
 435   = let
 436                 -- Make an immutable version, defaulting
 437                 -- the kind to lifted if necessary
 438         immut_tv    = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
 439         immut_tv_ty = mkTyVarTy immut_tv
 440
 441         zap tv = putTcTyVar tv immut_tv_ty
 442                 -- Bind the mutable version to the immutable one
 443     in
 444         -- If the type variable is mutable, then bind it to immut_tv_ty
 445         -- so that all other occurrences of the tyvar will get zapped too
 446     zonkTyVar zap tv            `thenNF_Tc` \ ty2 ->
 447
 448     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 (check_class_pred_tys dflags ctxt tys)
 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     how_to_allow = case ctxt of
 923                      InstHeadCtxt  -> empty     -- Should not happen
 924                      InstThetaCtxt -> parens undecidableMsg
 925                      other         -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 926
 927 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
 928         -- Implicit parameters only allows in type
 929         -- signatures; not in instance decls, superclasses etc
 930         -- The reason for not allowing implicit params in instances is a bit subtle
 931         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
 932         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
 933         -- discharge all the potential usas of the ?x in e.   For example, a
 934         -- constraint Foo [Int] might come out of e,and applying the
 935         -- instance decl would show up two uses of ?x.
 936
 937 check_source_ty dflags TypeCtxt  (NType tc tys)   = mapTc_ check_arg_type tys
 938
 939 -- Catch-all
 940 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 941
 942 -------------------------
 943 check_class_pred_tys dflags ctxt tys
 944   = case ctxt of
 945         InstHeadCtxt  -> True   -- We check for instance-head
 946                                 -- formation in checkValidInstHead
 947         InstThetaCtxt -> undecidable_ok || all isTyVarTy tys
 948         other         -> gla_exts       || all tyvar_head tys
 949   where
 950     undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
 951     gla_exts       = dopt Opt_GlasgowExts dflags
 952
 953 -------------------------
 954 tyvar_head ty                   -- Haskell 98 allows predicates of form
 955   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
 956   | otherwise                   -- where a is a type variable
 957   = case tcSplitAppTy_maybe ty of
 958         Just (ty, _) -> tyvar_head ty
 959         Nothing      -> False
 960 \end{code}
 961
 962 \begin{code}
 963 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
 964 predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
 965 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
 966
 967 checkThetaCtxt ctxt theta
 968   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
 969           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 970 \end{code}
 971
 972
 973 %************************************************************************
 974 %*                                                                      *
 975 \subsection{Validity check for TyCons}
 976 %*                                                                      *
 977 %************************************************************************
 978
 979 checkValidTyCon is called once the mutually-recursive knot has been
 980 tied, so we can look at things freely.
 981
 982 \begin{code}
 983 checkValidTyCon :: TyCon -> TcM ()
 984 checkValidTyCon tc
 985   | isSynTyCon tc = checkValidType (TySynCtxt name) syn_rhs
 986   | otherwise
 987   =     -- Check the context on the data decl
 988     checkValidTheta (DataTyCtxt name) (tyConTheta tc)   `thenTc_`
 989
 990         -- Check arg types of data constructors
 991     mapTc_ checkValidDataCon data_cons                  `thenTc_`
 992
 993         -- Check that fields with the same name share a type
 994     mapTc_ check_fields groups
 995
 996   where
 997     name         = tyConName tc
 998     (_, syn_rhs) = getSynTyConDefn tc
 999     data_cons    = tyConDataCons tc
1000
1001     fields = [field | con <- data_cons, field <- dataConFieldLabels con]
1002     groups = equivClasses cmp_name fields
1003     cmp_name field1 field2 = fieldLabelName field1 `compare` fieldLabelName field2
1004
1005     check_fields fields@(first_field_label : other_fields)
1006         -- These fields all have the same name, but are from
1007         -- different constructors in the data type
1008         =       -- Check that all the fields in the group have the same type
1009                 -- NB: this check assumes that all the constructors of a given
1010                 -- data type use the same type variables
1011           checkTc (all (tcEqType field_ty) other_tys) (fieldTypeMisMatch field_name)
1012         where
1013             field_ty   = fieldLabelType first_field_label
1014             field_name = fieldLabelName first_field_label
1015             other_tys  = map fieldLabelType other_fields
1016
1017 checkValidDataCon :: DataCon -> TcM ()
1018 checkValidDataCon con
1019   = checkValidType ctxt (idType (dataConWrapId con))    `thenTc_`
1020                 -- This checks the argument types and
1021                 -- ambiguity of the existential context (if any)
1022     tcAddErrCtxt (existentialCtxt con)
1023                  (checkFreeness ex_tvs ex_theta)
1024   where
1025     ctxt = ConArgCtxt (dataConName con)
1026     (_, _, ex_tvs, ex_theta, _, _) = dataConSig con
1027
1028
1029 fieldTypeMisMatch field_name
1030   = sep [ptext SLIT("Different constructors give different types for field"), quotes (ppr field_name)]
1031
1032 existentialCtxt con = ptext SLIT("When checking the existential context of constructor")
1033                       <+> quotes (ppr con)
1034 \end{code}
1035
1036
1037 checkValidClass is called once the mutually-recursive knot has been
1038 tied, so we can look at things freely.
1039
1040 \begin{code}
1041 checkValidClass :: Class -> TcM ()
1042 checkValidClass cls
1043   =     -- CHECK ARITY 1 FOR HASKELL 1.4
1044     doptsTc Opt_GlasgowExts                             `thenTc` \ gla_exts ->
1045
1046         -- Check that the class is unary, unless GlaExs
1047     checkTc (notNull tyvars)    (nullaryClassErr cls)   `thenTc_`
1048     checkTc (gla_exts || unary) (classArityErr cls)     `thenTc_`
1049
1050         -- Check the super-classes
1051     checkValidTheta (ClassSCCtxt (className cls)) theta `thenTc_`
1052
1053         -- Check the class operations
1054     mapTc_ check_op op_stuff            `thenTc_`
1055
1056         -- Check that if the class has generic methods, then the
1057         -- class has only one parameter.  We can't do generic
1058         -- multi-parameter type classes!
1059     checkTc (unary || no_generics) (genericMultiParamErr cls)
1060
1061   where
1062     (tyvars, theta, _, op_stuff) = classBigSig cls
1063     unary       = isSingleton tyvars
1064     no_generics = null [() | (_, GenDefMeth) <- op_stuff]
1065
1066     check_op (sel_id, dm)
1067         = checkValidTheta SigmaCtxt (tail theta)        `thenTc_`
1068                 -- The 'tail' removes the initial (C a) from the
1069                 -- class itself, leaving just the method type
1070
1071           checkValidType (FunSigCtxt op_name) tau       `thenTc_`
1072
1073                 -- Check that for a generic method, the type of
1074                 -- the method is sufficiently simple
1075           checkTc (dm /= GenDefMeth || validGenericMethodType op_ty)
1076                   (badGenericMethodType op_name op_ty)
1077         where
1078           op_name = idName sel_id
1079           op_ty   = idType sel_id
1080           (_,theta,tau) = tcSplitSigmaTy op_ty
1081
1082 nullaryClassErr cls
1083   = ptext SLIT("No parameters for class")  <+> quotes (ppr cls)
1084
1085 classArityErr cls
1086   = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls),
1087           parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))]
1088
1089 genericMultiParamErr clas
1090   = ptext SLIT("The multi-parameter class") <+> quotes (ppr clas) <+>
1091     ptext SLIT("cannot have generic methods")
1092
1093 badGenericMethodType op op_ty
1094   = hang (ptext SLIT("Generic method type is too complex"))
1095        4 (vcat [ppr op <+> dcolon <+> ppr op_ty,
1096                 ptext SLIT("You can only use type variables, arrows, and tuples")])
1097 \end{code}
1098
1099
1100 %************************************************************************
1101 %*                                                                      *
1102 \subsection{Checking for a decent instance head type}
1103 %*                                                                      *
1104 %************************************************************************
1105
1106 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1107 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1108
1109 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1110 flag is on, or (2)~the instance is imported (they must have been
1111 compiled elsewhere). In these cases, we let them go through anyway.
1112
1113 We can also have instances for functions: @instance Foo (a -> b) ...@.
1114
1115 \begin{code}
1116 checkValidInstHead :: Type -> TcM (Class, [TcType])
1117
1118 checkValidInstHead ty   -- Should be a source type
1119   = case tcSplitPredTy_maybe ty of {
1120         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1121         Just pred ->
1122
1123     case getClassPredTys_maybe pred of {
1124         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1125         Just (clas,tys) ->
1126
1127     getDOptsTc                                  `thenNF_Tc` \ dflags ->
1128     mapTc_ check_arg_type tys                   `thenTc_`
1129     check_inst_head dflags clas tys             `thenTc_`
1130     returnTc (clas, tys)
1131     }}
1132
1133 check_inst_head dflags clas tys
1134   |     -- CCALL CHECK
1135         -- A user declaration of a CCallable/CReturnable instance
1136         -- must be for a "boxed primitive" type.
1137         (clas `hasKey` cCallableClassKey
1138             && not (ccallable_type first_ty))
1139   ||    (clas `hasKey` cReturnableClassKey
1140             && not (creturnable_type first_ty))
1141   = failWithTc (nonBoxedPrimCCallErr clas first_ty)
1142
1143         -- If GlasgowExts then check at least one isn't a type variable
1144   | dopt Opt_GlasgowExts dflags
1145   = check_tyvars dflags clas tys
1146
1147         -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1148   | isSingleton tys,
1149     Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1150     not (isSynTyCon tycon),             -- ...but not a synonym
1151     all tcIsTyVarTy arg_tys,            -- Applied to type variables
1152     equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1153           -- This last condition checks that all the type variables are distinct
1154   = returnTc ()
1155
1156   | otherwise
1157   = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1158
1159   where
1160     (first_ty : _)       = tys
1161
1162     ccallable_type   ty = isFFIArgumentTy dflags PlayRisky ty
1163     creturnable_type ty = isFFIImportResultTy dflags ty
1164
1165     head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1166                              text "where T is not a synonym, and a,b,c are distinct type variables")
1167
1168 check_tyvars dflags clas tys
1169         -- Check that at least one isn't a type variable
1170         -- unless -fallow-undecideable-instances
1171   | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
1172   | not (all tcIsTyVarTy tys)                 = returnTc ()
1173   | otherwise                                 = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1174   where
1175     msg =  parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1176                    $$ undecidableMsg)
1177
1178 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1179 \end{code}
1180
1181 \begin{code}
1182 instTypeErr pp_ty msg
1183   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1184          nest 4 msg]
1185
1186 nonBoxedPrimCCallErr clas inst_ty
1187   = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
1188          4 (pprClassPred clas [inst_ty])
1189 \end{code}