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