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 )
  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) $
 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 && not (null 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 note ty)
 734   = check_tau_type rank ubx_tup ty
 735         -- Synonym notes are built only when the synonym is
 736         -- saturated (see Type.mkSynTy)
 737         -- Not checking the 'note' part allows us to instantiate a synonym
 738         -- defn with a for-all type, or with a partially-applied type synonym,
 739         -- but that seems OK too
 740
 741 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
 742   | isSynTyCon tc
 743   =     -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
 744         -- synonym application, leaving it to checkValidType (i.e. right here
 745         -- to find the error
 746     checkTc syn_arity_ok arity_msg      `thenTc_`
 747     mapTc_ check_arg_type tys
 748
 749   | isUnboxedTupleTyCon tc
 750   = doptsTc Opt_GlasgowExts                     `thenNF_Tc` \ gla_exts ->
 751     checkTc (ubx_tup_ok gla_exts) ubx_tup_msg   `thenTc_`
 752     mapTc_ (check_tau_type (Rank 0) UT_Ok) tys
 753                         -- Args are allowed to be unlifted, or
 754                         -- more unboxed tuples, so can't use check_arg_ty
 755
 756   | otherwise
 757   = mapTc_ check_arg_type tys
 758
 759   where
 760     ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
 761
 762     syn_arity_ok = tc_arity <= n_args
 763                 -- It's OK to have an *over-applied* type synonym
 764                 --      data Tree a b = ...
 765                 --      type Foo a = Tree [a]
 766                 --      f :: Foo a b -> ...
 767     n_args    = length tys
 768     tc_arity  = tyConArity tc
 769
 770     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
 771     ubx_tup_msg = ubxArgTyErr ty
 772
 773 ----------------------------------------
 774 forAllTyErr     ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
 775 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
 776 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
 777 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 778 \end{code}
 779
 780 Check for ambiguity
 781 ~~~~~~~~~~~~~~~~~~~
 782           forall V. P => tau
 783 is ambiguous if P contains generic variables
 784 (i.e. one of the Vs) that are not mentioned in tau
 785
 786 However, we need to take account of functional dependencies
 787 when we speak of 'mentioned in tau'.  Example:
 788         class C a b | a -> b where ...
 789 Then the type
 790         forall x y. (C x y) => x
 791 is not ambiguous because x is mentioned and x determines y
 792
 793 NB; the ambiguity check is only used for *user* types, not for types
 794 coming from inteface files.  The latter can legitimately have
 795 ambiguous types. Example
 796
 797    class S a where s :: a -> (Int,Int)
 798    instance S Char where s _ = (1,1)
 799    f:: S a => [a] -> Int -> (Int,Int)
 800    f (_::[a]) x = (a*x,b)
 801         where (a,b) = s (undefined::a)
 802
 803 Here the worker for f gets the type
 804         fw :: forall a. S a => Int -> (# Int, Int #)
 805
 806 If the list of tv_names is empty, we have a monotype, and then we
 807 don't need to check for ambiguity either, because the test can't fail
 808 (see is_ambig).
 809
 810 \begin{code}
 811 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
 812 checkAmbiguity forall_tyvars theta tau_tyvars
 813   = mapTc_ complain (filter is_ambig theta)
 814   where
 815     complain pred     = addErrTc (ambigErr pred)
 816     extended_tau_vars = grow theta tau_tyvars
 817     is_ambig pred     = any ambig_var (varSetElems (tyVarsOfPred pred))
 818
 819     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
 820                         not (ct_var `elemVarSet` extended_tau_vars)
 821
 822     is_free ct_var    = not (ct_var `elem` forall_tyvars)
 823
 824 ambigErr pred
 825   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
 826          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
 827                  ptext SLIT("must be reachable from the type after the '=>'"))]
 828 \end{code}
 829
 830 In addition, GHC insists that at least one type variable
 831 in each constraint is in V.  So we disallow a type like
 832         forall a. Eq b => b -> b
 833 even in a scope where b is in scope.
 834
 835 \begin{code}
 836 checkFreeness forall_tyvars theta
 837   = mapTc_ complain (filter is_free theta)
 838   where
 839     is_free pred     =  not (isIPPred pred)
 840                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
 841     bound_var ct_var = ct_var `elem` forall_tyvars
 842     complain pred    = addErrTc (freeErr pred)
 843
 844 freeErr pred
 845   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
 846                    ptext SLIT("are already in scope"),
 847          nest 4 (ptext SLIT("At least one must be universally quantified here"))
 848     ]
 849 \end{code}
 850
 851
 852 %************************************************************************
 853 %*                                                                      *
 854 \subsection{Checking a theta or source type}
 855 %*                                                                      *
 856 %************************************************************************
 857
 858 \begin{code}
 859 data SourceTyCtxt
 860   = ClassSCCtxt Name    -- Superclasses of clas
 861   | SigmaCtxt           -- Context of a normal for-all type
 862   | DataTyCtxt Name     -- Context of a data decl
 863   | TypeCtxt            -- Source type in an ordinary type
 864   | InstThetaCtxt       -- Context of an instance decl
 865   | InstHeadCtxt        -- Head of an instance decl
 866
 867 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
 868 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
 869 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
 870 pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
 871 pprSourceTyCtxt InstHeadCtxt    = ptext SLIT("the head of an instance declaration")
 872 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
 873 \end{code}
 874
 875 \begin{code}
 876 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
 877 checkValidTheta ctxt theta
 878   = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
 879
 880 -------------------------
 881 check_valid_theta ctxt []
 882   = returnTc ()
 883 check_valid_theta ctxt theta
 884   = getDOptsTc                                  `thenNF_Tc` \ dflags ->
 885     warnTc (not (null dups)) (dupPredWarn dups) `thenNF_Tc_`
 886     mapTc_ (check_source_ty dflags ctxt) theta
 887   where
 888     (_,dups) = removeDups tcCmpPred theta
 889
 890 -------------------------
 891 check_source_ty dflags ctxt pred@(ClassP cls tys)
 892   =     -- Class predicates are valid in all contexts
 893     mapTc_ check_arg_type tys           `thenTc_`
 894     checkTc (arity == n_tys) arity_err          `thenTc_`
 895     checkTc (all tyvar_head tys || arby_preds_ok)
 896             (predTyVarErr pred $$ how_to_allow)
 897
 898   where
 899     class_name = className cls
 900     arity      = classArity cls
 901     n_tys      = length tys
 902     arity_err  = arityErr "Class" class_name arity n_tys
 903
 904     arby_preds_ok = case ctxt of
 905                         InstHeadCtxt  -> True   -- We check for instance-head formation
 906                                                 -- in checkValidInstHead
 907                         InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
 908                         other         -> dopt Opt_GlasgowExts               dflags
 909
 910     how_to_allow = case ctxt of
 911                      InstHeadCtxt  -> empty     -- Should not happen
 912                      InstThetaCtxt -> parens undecidableMsg
 913                      other         -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 914
 915 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
 916         -- Implicit parameters only allows in type
 917         -- signatures; not in instance decls, superclasses etc
 918         -- The reason for not allowing implicit params in instances is a bit subtle
 919         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
 920         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
 921         -- discharge all the potential usas of the ?x in e.   For example, a
 922         -- constraint Foo [Int] might come out of e,and applying the
 923         -- instance decl would show up two uses of ?x.
 924
 925 check_source_ty dflags TypeCtxt  (NType tc tys)   = mapTc_ check_arg_type tys
 926
 927 -- Catch-all
 928 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 929
 930 -------------------------
 931 tyvar_head ty                   -- Haskell 98 allows predicates of form
 932   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
 933   | otherwise                   -- where a is a type variable
 934   = case tcSplitAppTy_maybe ty of
 935         Just (ty, _) -> tyvar_head ty
 936         Nothing      -> False
 937 \end{code}
 938
 939 \begin{code}
 940 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
 941 predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
 942 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
 943
 944 checkThetaCtxt ctxt theta
 945   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
 946           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 947 \end{code}
 948
 949
 950 %************************************************************************
 951 %*                                                                      *
 952 \subsection{Validity check for TyCons}
 953 %*                                                                      *
 954 %************************************************************************
 955
 956 checkValidTyCon is called once the mutually-recursive knot has been
 957 tied, so we can look at things freely.
 958
 959 \begin{code}
 960 checkValidTyCon :: TyCon -> TcM ()
 961 checkValidTyCon tc
 962   | isSynTyCon tc = checkValidType (TySynCtxt name) syn_rhs
 963   | otherwise
 964   =     -- Check the context on the data decl
 965     checkValidTheta (DataTyCtxt name) (tyConTheta tc)   `thenTc_`
 966
 967         -- Check arg types of data constructors
 968     mapTc_ checkValidDataCon data_cons                  `thenTc_`
 969
 970         -- Check that fields with the same name share a type
 971     mapTc_ check_fields groups
 972
 973   where
 974     name         = tyConName tc
 975     (_, syn_rhs) = getSynTyConDefn tc
 976     data_cons    = tyConDataCons tc
 977
 978     fields = [field | con <- data_cons, field <- dataConFieldLabels con]
 979     groups = equivClasses cmp_name fields
 980     cmp_name field1 field2 = fieldLabelName field1 `compare` fieldLabelName field2
 981
 982     check_fields fields@(first_field_label : other_fields)
 983         -- These fields all have the same name, but are from
 984         -- different constructors in the data type
 985         =       -- Check that all the fields in the group have the same type
 986                 -- NB: this check assumes that all the constructors of a given
 987                 -- data type use the same type variables
 988           checkTc (all (tcEqType field_ty) other_tys) (fieldTypeMisMatch field_name)
 989         where
 990             field_ty   = fieldLabelType first_field_label
 991             field_name = fieldLabelName first_field_label
 992             other_tys  = map fieldLabelType other_fields
 993
 994 checkValidDataCon :: DataCon -> TcM ()
 995 checkValidDataCon con
 996   = checkValidType ctxt (idType (dataConWrapId con))    `thenTc_`
 997                 -- This checks the argument types and
 998                 -- ambiguity of the existential context (if any)
 999     tcAddErrCtxt (existentialCtxt con)
1000                  (checkFreeness ex_tvs ex_theta)
1001   where
1002     ctxt = ConArgCtxt (dataConName con)
1003     (_, _, ex_tvs, ex_theta, _, _) = dataConSig con
1004
1005
1006 fieldTypeMisMatch field_name
1007   = sep [ptext SLIT("Different constructors give different types for field"), quotes (ppr field_name)]
1008
1009 existentialCtxt con = ptext SLIT("When checking the existential context of constructor")
1010                       <+> ppr con
1011 \end{code}
1012
1013
1014 checkValidClass is called once the mutually-recursive knot has been
1015 tied, so we can look at things freely.
1016
1017 \begin{code}
1018 checkValidClass :: Class -> TcM ()
1019 checkValidClass cls
1020   =     -- CHECK ARITY 1 FOR HASKELL 1.4
1021     doptsTc Opt_GlasgowExts                             `thenTc` \ gla_exts ->
1022
1023         -- Check that the class is unary, unless GlaExs
1024     checkTc (not (null tyvars))         (nullaryClassErr cls)   `thenTc_`
1025     checkTc (gla_exts || unary) (classArityErr cls)     `thenTc_`
1026
1027         -- Check the super-classes
1028     checkValidTheta (ClassSCCtxt (className cls)) theta `thenTc_`
1029
1030         -- Check the class operations
1031     mapTc_ check_op op_stuff            `thenTc_`
1032
1033         -- Check that if the class has generic methods, then the
1034         -- class has only one parameter.  We can't do generic
1035         -- multi-parameter type classes!
1036     checkTc (unary || no_generics) (genericMultiParamErr cls)
1037
1038   where
1039     (tyvars, theta, _, op_stuff) = classBigSig cls
1040     unary       = isSingleton tyvars
1041     no_generics = null [() | (_, GenDefMeth) <- op_stuff]
1042
1043     check_op (sel_id, dm)
1044         = checkValidTheta SigmaCtxt (tail theta)        `thenTc_`
1045                 -- The 'tail' removes the initial (C a) from the
1046                 -- class itself, leaving just the method type
1047
1048           checkValidType (FunSigCtxt op_name) tau       `thenTc_`
1049
1050                 -- Check that for a generic method, the type of
1051                 -- the method is sufficiently simple
1052           checkTc (dm /= GenDefMeth || validGenericMethodType op_ty)
1053                   (badGenericMethodType op_name op_ty)
1054         where
1055           op_name = idName sel_id
1056           op_ty   = idType sel_id
1057           (_,theta,tau) = tcSplitSigmaTy op_ty
1058
1059 nullaryClassErr cls
1060   = ptext SLIT("No parameters for class")  <+> quotes (ppr cls)
1061
1062 classArityErr cls
1063   = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls),
1064           parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))]
1065
1066 genericMultiParamErr clas
1067   = ptext SLIT("The multi-parameter class") <+> quotes (ppr clas) <+>
1068     ptext SLIT("cannot have generic methods")
1069
1070 badGenericMethodType op op_ty
1071   = hang (ptext SLIT("Generic method type is too complex"))
1072        4 (vcat [ppr op <+> dcolon <+> ppr op_ty,
1073                 ptext SLIT("You can only use type variables, arrows, and tuples")])
1074 \end{code}
1075
1076
1077 %************************************************************************
1078 %*                                                                      *
1079 \subsection{Checking for a decent instance head type}
1080 %*                                                                      *
1081 %************************************************************************
1082
1083 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1084 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1085
1086 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1087 flag is on, or (2)~the instance is imported (they must have been
1088 compiled elsewhere). In these cases, we let them go through anyway.
1089
1090 We can also have instances for functions: @instance Foo (a -> b) ...@.
1091
1092 \begin{code}
1093 checkValidInstHead :: Type -> TcM (Class, [TcType])
1094
1095 checkValidInstHead ty   -- Should be a source type
1096   = case tcSplitPredTy_maybe ty of {
1097         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1098         Just pred ->
1099
1100     case getClassPredTys_maybe pred of {
1101         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1102         Just (clas,tys) ->
1103
1104     getDOptsTc                                  `thenNF_Tc` \ dflags ->
1105     mapTc_ check_arg_type tys                   `thenTc_`
1106     check_inst_head dflags clas tys             `thenTc_`
1107     returnTc (clas, tys)
1108     }}
1109
1110 check_inst_head dflags clas tys
1111   |     -- CCALL CHECK
1112         -- A user declaration of a CCallable/CReturnable instance
1113         -- must be for a "boxed primitive" type.
1114         (clas `hasKey` cCallableClassKey
1115             && not (ccallable_type first_ty))
1116   ||    (clas `hasKey` cReturnableClassKey
1117             && not (creturnable_type first_ty))
1118   = failWithTc (nonBoxedPrimCCallErr clas first_ty)
1119
1120         -- If GlasgowExts then check at least one isn't a type variable
1121   | dopt Opt_GlasgowExts dflags
1122   = check_tyvars dflags clas tys
1123
1124         -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1125   | isSingleton tys,
1126     Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1127     not (isSynTyCon tycon),             -- ...but not a synonym
1128     all tcIsTyVarTy arg_tys,            -- Applied to type variables
1129     equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1130           -- This last condition checks that all the type variables are distinct
1131   = returnTc ()
1132
1133   | otherwise
1134   = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1135
1136   where
1137     (first_ty : _)       = tys
1138
1139     ccallable_type   ty = isFFIArgumentTy dflags PlayRisky ty
1140     creturnable_type ty = isFFIImportResultTy dflags ty
1141
1142     head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1143                              text "where T is not a synonym, and a,b,c are distinct type variables")
1144
1145 check_tyvars dflags clas tys
1146         -- Check that at least one isn't a type variable
1147         -- unless -fallow-undecideable-instances
1148   | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
1149   | not (all tcIsTyVarTy tys)                 = returnTc ()
1150   | otherwise                                 = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1151   where
1152     msg =  parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1153                    $$ undecidableMsg)
1154
1155 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1156 \end{code}
1157
1158 \begin{code}
1159 instTypeErr pp_ty msg
1160   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1161          nest 4 msg]
1162
1163 nonBoxedPrimCCallErr clas inst_ty
1164   = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
1165          4 (pprClassPred clas [inst_ty])
1166 \end{code}