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