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, 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 SLIT("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 SLIT("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 SLIT("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 SLIT("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
 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 an arbitrary type
 404         -- We know it's unbound even though we don't carry an environment,
 405         -- because at the binding site for a type variable we bind the
 406         -- mutable tyvar to a fresh immutable one.  So the mutable store
 407         -- plays the role of an environment.  If we come across a mutable
 408         -- type variable that isn't so bound, it must be completely free.
 409     zonk_unbound_tyvar tv = putTcTyVar tv (mkArbitraryType tv)
 410
 411
 412 -- When the type checker finds a type variable with no binding,
 413 -- which means it can be instantiated with an arbitrary type, it
 414 -- usually instantiates it to Void.  Eg.
 415 --
 416 --      length []
 417 -- ===>
 418 --      length Void (Nil Void)
 419 --
 420 -- But in really obscure programs, the type variable might have
 421 -- a kind other than *, so we need to invent a suitably-kinded type.
 422 --
 423 -- This commit uses
 424 --      Void for kind *
 425 --      List for kind *->*
 426 --      Tuple for kind *->...*->*
 427 --
 428 -- which deals with most cases.  (Previously, it only dealt with
 429 -- kind *.)
 430 --
 431 -- In the other cases, it just makes up a TyCon with a suitable
 432 -- kind.  If this gets into an interface file, anyone reading that
 433 -- file won't understand it.  This is fixable (by making the client
 434 -- of the interface file make up a TyCon too) but it is tiresome and
 435 -- never happens, so I am leaving it
 436
 437 mkArbitraryType :: TcTyVar -> Type
 438 -- Make up an arbitrary type whose kind is the same as the tyvar.
 439 -- We'll use this to instantiate the (unbound) tyvar.
 440 mkArbitraryType tv
 441   | isAnyTypeKind kind = voidTy         -- The vastly common case
 442   | otherwise          = TyConApp tycon []
 443   where
 444     kind       = tyVarKind tv
 445     (args,res) = Type.splitFunTys kind  -- Kinds are simple; use Type.splitFunTys
 446
 447     tycon | kind `eqKind` tyConKind listTyCon   -- *->*
 448           = listTyCon                           -- No tuples this size
 449
 450           | all isTypeKind args && isTypeKind res
 451           = tupleTyCon Boxed (length args)      -- *-> ... ->*->*
 452
 453           | otherwise
 454           = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
 455             mkPrimTyCon tc_name kind 0 [] VoidRep
 456                 -- Same name as the tyvar, apart from making it start with a colon (sigh)
 457                 -- I dread to think what will happen if this gets out into an
 458                 -- interface file.  Catastrophe likely.  Major sigh.
 459
 460     tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
 461
 462 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
 463 -- of a type variable, at the *end* of type checking.  It changes
 464 -- the *mutable* type variable into an *immutable* one.
 465 --
 466 -- It does this by making an immutable version of tv and binds tv to it.
 467 -- Now any bound occurences of the original type variable will get
 468 -- zonked to the immutable version.
 469
 470 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
 471 zonkTcTyVarToTyVar tv
 472   = let
 473                 -- Make an immutable version, defaulting
 474                 -- the kind to lifted if necessary
 475         immut_tv    = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
 476         immut_tv_ty = mkTyVarTy immut_tv
 477
 478         zap tv = putTcTyVar tv immut_tv_ty
 479                 -- Bind the mutable version to the immutable one
 480     in
 481         -- If the type variable is mutable, then bind it to immut_tv_ty
 482         -- so that all other occurrences of the tyvar will get zapped too
 483     zonkTyVar zap tv            `thenNF_Tc` \ ty2 ->
 484
 485     WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
 486
 487     returnNF_Tc immut_tv
 488 \end{code}
 489
 490
 491 %************************************************************************
 492 %*                                                                      *
 493 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
 494 %*                                                                      *
 495 %*              For internal use only!                                  *
 496 %*                                                                      *
 497 %************************************************************************
 498
 499 \begin{code}
 500 -- zonkType is used for Kinds as well
 501
 502 -- For unbound, mutable tyvars, zonkType uses the function given to it
 503 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 504 --      type variable and zonks the kind too
 505
 506 zonkType :: (TcTyVar -> NF_TcM Type)    -- What to do with unbound mutable type variables
 507                                         -- see zonkTcType, and zonkTcTypeToType
 508          -> TcType
 509          -> NF_TcM Type
 510 zonkType unbound_var_fn ty
 511   = go ty
 512   where
 513     go (TyConApp tycon tys)       = mapNF_Tc go tys     `thenNF_Tc` \ tys' ->
 514                                     returnNF_Tc (TyConApp tycon tys')
 515
 516     go (NoteTy (SynNote ty1) ty2) = go ty1              `thenNF_Tc` \ ty1' ->
 517                                     go ty2              `thenNF_Tc` \ ty2' ->
 518                                     returnNF_Tc (NoteTy (SynNote ty1') ty2')
 519
 520     go (NoteTy (FTVNote _) ty2)   = go ty2      -- Discard free-tyvar annotations
 521
 522     go (SourceTy p)               = go_pred p           `thenNF_Tc` \ p' ->
 523                                     returnNF_Tc (SourceTy p')
 524
 525     go (FunTy arg res)            = go arg              `thenNF_Tc` \ arg' ->
 526                                     go res              `thenNF_Tc` \ res' ->
 527                                     returnNF_Tc (FunTy arg' res')
 528
 529     go (AppTy fun arg)            = go fun              `thenNF_Tc` \ fun' ->
 530                                     go arg              `thenNF_Tc` \ arg' ->
 531                                     returnNF_Tc (mkAppTy fun' arg')
 532
 533         -- The two interesting cases!
 534     go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn tyvar
 535
 536     go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar   `thenNF_Tc` \ tyvar' ->
 537                              go ty                      `thenNF_Tc` \ ty' ->
 538                              returnNF_Tc (ForAllTy tyvar' ty')
 539
 540     go_pred (ClassP c tys) = mapNF_Tc go tys    `thenNF_Tc` \ tys' ->
 541                              returnNF_Tc (ClassP c tys')
 542     go_pred (NType tc tys) = mapNF_Tc go tys    `thenNF_Tc` \ tys' ->
 543                              returnNF_Tc (NType tc tys')
 544     go_pred (IParam n ty)  = go ty              `thenNF_Tc` \ ty' ->
 545                              returnNF_Tc (IParam n ty')
 546
 547 zonkTyVar :: (TcTyVar -> NF_TcM Type)           -- What to do for an unbound mutable variable
 548           -> TcTyVar -> NF_TcM TcType
 549 zonkTyVar unbound_var_fn tyvar
 550   | not (isMutTyVar tyvar)      -- Not a mutable tyvar.  This can happen when
 551                                 -- zonking a forall type, when the bound type variable
 552                                 -- needn't be mutable
 553   = ASSERT( isTyVar tyvar )             -- Should not be any immutable kind vars
 554     returnNF_Tc (TyVarTy tyvar)
 555
 556   | otherwise
 557   =  getTcTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
 558      case maybe_ty of
 559           Nothing       -> unbound_var_fn tyvar                 -- Mutable and unbound
 560           Just other_ty -> zonkType unbound_var_fn other_ty     -- Bound
 561 \end{code}
 562
 563
 564
 565 %************************************************************************
 566 %*                                                                      *
 567 \subsection{Checking a user type}
 568 %*                                                                      *
 569 %************************************************************************
 570
 571 When dealing with a user-written type, we first translate it from an HsType
 572 to a Type, performing kind checking, and then check various things that should
 573 be true about it.  We don't want to perform these checks at the same time
 574 as the initial translation because (a) they are unnecessary for interface-file
 575 types and (b) when checking a mutually recursive group of type and class decls,
 576 we can't "look" at the tycons/classes yet.  Also, the checks are are rather
 577 diverse, and used to really mess up the other code.
 578
 579 One thing we check for is 'rank'.
 580
 581         Rank 0:         monotypes (no foralls)
 582         Rank 1:         foralls at the front only, Rank 0 inside
 583         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
 584
 585         basic ::= tyvar | T basic ... basic
 586
 587         r2  ::= forall tvs. cxt => r2a
 588         r2a ::= r1 -> r2a | basic
 589         r1  ::= forall tvs. cxt => r0
 590         r0  ::= r0 -> r0 | basic
 591
 592 Another thing is to check that type synonyms are saturated.
 593 This might not necessarily show up in kind checking.
 594         type A i = i
 595         data T k = MkT (k Int)
 596         f :: T A        -- BAD!
 597
 598
 599 \begin{code}
 600 data UserTypeCtxt
 601   = FunSigCtxt Name     -- Function type signature
 602   | ExprSigCtxt         -- Expression type signature
 603   | ConArgCtxt Name     -- Data constructor argument
 604   | TySynCtxt Name      -- RHS of a type synonym decl
 605   | GenPatCtxt          -- Pattern in generic decl
 606                         --      f{| a+b |} (Inl x) = ...
 607   | PatSigCtxt          -- Type sig in pattern
 608                         --      f (x::t) = ...
 609   | ResSigCtxt          -- Result type sig
 610                         --      f x :: t = ....
 611   | ForSigCtxt Name     -- Foreign inport or export signature
 612   | RuleSigCtxt Name    -- Signature on a forall'd variable in a RULE
 613
 614 -- Notes re TySynCtxt
 615 -- We allow type synonyms that aren't types; e.g.  type List = []
 616 --
 617 -- If the RHS mentions tyvars that aren't in scope, we'll
 618 -- quantify over them:
 619 --      e.g.    type T = a->a
 620 -- will become  type T = forall a. a->a
 621 --
 622 -- With gla-exts that's right, but for H98 we should complain.
 623
 624
 625 pprUserTypeCtxt (FunSigCtxt n)  = ptext SLIT("the type signature for") <+> quotes (ppr n)
 626 pprUserTypeCtxt ExprSigCtxt     = ptext SLIT("an expression type signature")
 627 pprUserTypeCtxt (ConArgCtxt c)  = ptext SLIT("the type of constructor") <+> quotes (ppr c)
 628 pprUserTypeCtxt (TySynCtxt c)   = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
 629 pprUserTypeCtxt GenPatCtxt      = ptext SLIT("the type pattern of a generic definition")
 630 pprUserTypeCtxt PatSigCtxt      = ptext SLIT("a pattern type signature")
 631 pprUserTypeCtxt ResSigCtxt      = ptext SLIT("a result type signature")
 632 pprUserTypeCtxt (ForSigCtxt n)  = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
 633 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
 634 \end{code}
 635
 636 \begin{code}
 637 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 638 -- Checks that the type is valid for the given context
 639 checkValidType ctxt ty
 640   = doptsTc Opt_GlasgowExts     `thenNF_Tc` \ gla_exts ->
 641     let
 642         rank | gla_exts = Arbitrary
 643              | otherwise
 644              = case ctxt of     -- Haskell 98
 645                  GenPatCtxt     -> Rank 0
 646                  PatSigCtxt     -> Rank 0
 647                  ResSigCtxt     -> Rank 0
 648                  TySynCtxt _    -> Rank 0
 649                  ExprSigCtxt    -> Rank 1
 650                  FunSigCtxt _   -> Rank 1
 651                  ConArgCtxt _   -> Rank 1       -- We are given the type of the entire
 652                                                 -- constructor, hence rank 1
 653                  ForSigCtxt _   -> Rank 1
 654                  RuleSigCtxt _  -> Rank 1
 655
 656         actual_kind = typeKind ty
 657
 658         actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
 659
 660         kind_ok = case ctxt of
 661                         TySynCtxt _  -> True    -- Any kind will do
 662                         GenPatCtxt   -> actual_kind_is_lifted
 663                         ForSigCtxt _ -> actual_kind_is_lifted
 664                         other        -> isTypeKind actual_kind
 665
 666         ubx_tup | not gla_exts = UT_NotOk
 667                 | otherwise    = case ctxt of
 668                                    TySynCtxt _ -> UT_Ok
 669                                    other       -> UT_NotOk
 670                 -- Unboxed tuples ok in function results,
 671                 -- but for type synonyms we allow them even at
 672                 -- top level
 673     in
 674     tcAddErrCtxt (checkTypeCtxt ctxt ty)        $
 675
 676         -- Check that the thing has kind Type, and is lifted if necessary
 677     checkTc kind_ok (kindErr actual_kind)       `thenTc_`
 678
 679         -- Check the internal validity of the type itself
 680     check_poly_type rank ubx_tup ty
 681
 682
 683 checkTypeCtxt ctxt ty
 684   = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
 685           ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
 686
 687         -- Hack alert.  If there are no tyvars, (ppr sigma_ty) will print
 688         -- something strange like {Eq k} -> k -> k, because there is no
 689         -- ForAll at the top of the type.  Since this is going to the user
 690         -- we want it to look like a proper Haskell type even then; hence the hack
 691         --
 692         -- This shows up in the complaint about
 693         --      case C a where
 694         --        op :: Eq a => a -> a
 695 ppr_ty ty | null forall_tvs && not (null theta) = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
 696           | otherwise                        = ppr ty
 697           where
 698             (forall_tvs, theta, tau) = tcSplitSigmaTy ty
 699 \end{code}
 700
 701
 702 \begin{code}
 703 data Rank = Rank Int | Arbitrary
 704
 705 decRank :: Rank -> Rank
 706 decRank Arbitrary = Arbitrary
 707 decRank (Rank n)  = Rank (n-1)
 708
 709 ----------------------------------------
 710 data UbxTupFlag = UT_Ok | UT_NotOk
 711         -- The "Ok" version means "ok if -fglasgow-exts is on"
 712
 713 ----------------------------------------
 714 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 715 check_poly_type (Rank 0) ubx_tup ty
 716   = check_tau_type (Rank 0) ubx_tup ty
 717
 718 check_poly_type rank ubx_tup ty
 719   = let
 720         (tvs, theta, tau) = tcSplitSigmaTy ty
 721     in
 722     check_valid_theta SigmaCtxt theta           `thenTc_`
 723     check_tau_type (decRank rank) ubx_tup tau   `thenTc_`
 724     checkFreeness tvs theta                     `thenTc_`
 725     checkAmbiguity tvs theta (tyVarsOfType tau)
 726
 727 ----------------------------------------
 728 check_arg_type :: Type -> TcM ()
 729 -- The sort of type that can instantiate a type variable,
 730 -- or be the argument of a type constructor.
 731 -- Not an unboxed tuple, not a forall.
 732 -- Other unboxed types are very occasionally allowed as type
 733 -- arguments depending on the kind of the type constructor
 734 --
 735 -- For example, we want to reject things like:
 736 --
 737 --      instance Ord a => Ord (forall s. T s a)
 738 -- and
 739 --      g :: T s (forall b.b)
 740 --
 741 -- NB: unboxed tuples can have polymorphic or unboxed args.
 742 --     This happens in the workers for functions returning
 743 --     product types with polymorphic components.
 744 --     But not in user code.
 745 -- Anyway, they are dealt with by a special case in check_tau_type
 746
 747 check_arg_type ty
 748   = check_tau_type (Rank 0) UT_NotOk ty         `thenTc_`
 749     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 750
 751 ----------------------------------------
 752 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 753 -- Rank is allowed rank for function args
 754 -- No foralls otherwise
 755
 756 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
 757 check_tau_type rank ubx_tup (SourceTy sty)    = getDOptsTc              `thenNF_Tc` \ dflags ->
 758                                                 check_source_ty dflags TypeCtxt sty
 759 check_tau_type rank ubx_tup (TyVarTy _)       = returnTc ()
 760 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
 761   = check_poly_type rank UT_NotOk arg_ty        `thenTc_`
 762     check_tau_type  rank UT_Ok    res_ty
 763
 764 check_tau_type rank ubx_tup (AppTy ty1 ty2)
 765   = check_arg_type ty1 `thenTc_` check_arg_type ty2
 766
 767 check_tau_type rank ubx_tup (NoteTy note ty)
 768   = check_tau_type rank ubx_tup ty
 769         -- Synonym notes are built only when the synonym is
 770         -- saturated (see Type.mkSynTy)
 771         -- Not checking the 'note' part allows us to instantiate a synonym
 772         -- defn with a for-all type, but that seems OK too
 773
 774 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
 775   | isSynTyCon tc
 776   =     -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
 777         -- synonym application, leaving it to checkValidType (i.e. right here
 778         -- to find the error
 779     checkTc syn_arity_ok arity_msg      `thenTc_`
 780     mapTc_ check_arg_type tys
 781
 782   | isUnboxedTupleTyCon tc
 783   = doptsTc Opt_GlasgowExts                     `thenNF_Tc` \ gla_exts ->
 784     checkTc (ubx_tup_ok gla_exts) ubx_tup_msg   `thenTc_`
 785     mapTc_ (check_tau_type (Rank 0) UT_Ok) tys
 786                         -- Args are allowed to be unlifted, or
 787                         -- more unboxed tuples, so can't use check_arg_ty
 788
 789   | otherwise
 790   = mapTc_ check_arg_type tys
 791
 792   where
 793     ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
 794
 795     syn_arity_ok = tc_arity <= n_args
 796                 -- It's OK to have an *over-applied* type synonym
 797                 --      data Tree a b = ...
 798                 --      type Foo a = Tree [a]
 799                 --      f :: Foo a b -> ...
 800     n_args    = length tys
 801     tc_arity  = tyConArity tc
 802
 803     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
 804     ubx_tup_msg = ubxArgTyErr ty
 805
 806 ----------------------------------------
 807 forAllTyErr     ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
 808 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
 809 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
 810 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 811 \end{code}
 812
 813 Check for ambiguity
 814 ~~~~~~~~~~~~~~~~~~~
 815           forall V. P => tau
 816 is ambiguous if P contains generic variables
 817 (i.e. one of the Vs) that are not mentioned in tau
 818
 819 However, we need to take account of functional dependencies
 820 when we speak of 'mentioned in tau'.  Example:
 821         class C a b | a -> b where ...
 822 Then the type
 823         forall x y. (C x y) => x
 824 is not ambiguous because x is mentioned and x determines y
 825
 826 NB; the ambiguity check is only used for *user* types, not for types
 827 coming from inteface files.  The latter can legitimately have
 828 ambiguous types. Example
 829
 830    class S a where s :: a -> (Int,Int)
 831    instance S Char where s _ = (1,1)
 832    f:: S a => [a] -> Int -> (Int,Int)
 833    f (_::[a]) x = (a*x,b)
 834         where (a,b) = s (undefined::a)
 835
 836 Here the worker for f gets the type
 837         fw :: forall a. S a => Int -> (# Int, Int #)
 838
 839 If the list of tv_names is empty, we have a monotype, and then we
 840 don't need to check for ambiguity either, because the test can't fail
 841 (see is_ambig).
 842
 843 \begin{code}
 844 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
 845 checkAmbiguity forall_tyvars theta tau_tyvars
 846   = mapTc_ complain (filter is_ambig theta)
 847   where
 848     complain pred     = addErrTc (ambigErr pred)
 849     extended_tau_vars = grow theta tau_tyvars
 850     is_ambig pred     = any ambig_var (varSetElems (tyVarsOfPred pred))
 851
 852     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
 853                         not (ct_var `elemVarSet` extended_tau_vars)
 854
 855     is_free ct_var    = not (ct_var `elem` forall_tyvars)
 856
 857 ambigErr pred
 858   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
 859          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
 860                  ptext SLIT("must be reachable from the type after the '=>'"))]
 861 \end{code}
 862
 863 In addition, GHC insists that at least one type variable
 864 in each constraint is in V.  So we disallow a type like
 865         forall a. Eq b => b -> b
 866 even in a scope where b is in scope.
 867
 868 \begin{code}
 869 checkFreeness forall_tyvars theta
 870   = mapTc_ complain (filter is_free theta)
 871   where
 872     is_free pred     =  not (isIPPred pred)
 873                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
 874     bound_var ct_var = ct_var `elem` forall_tyvars
 875     complain pred    = addErrTc (freeErr pred)
 876
 877 freeErr pred
 878   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
 879                    ptext SLIT("are already in scope"),
 880          nest 4 (ptext SLIT("At least one must be universally quantified here"))
 881     ]
 882 \end{code}
 883
 884
 885 %************************************************************************
 886 %*                                                                      *
 887 \subsection{Checking a theta or source type}
 888 %*                                                                      *
 889 %************************************************************************
 890
 891 \begin{code}
 892 data SourceTyCtxt
 893   = ClassSCCtxt Name    -- Superclasses of clas
 894   | SigmaCtxt           -- Context of a normal for-all type
 895   | DataTyCtxt Name     -- Context of a data decl
 896   | TypeCtxt            -- Source type in an ordinary type
 897   | InstThetaCtxt       -- Context of an instance decl
 898   | InstHeadCtxt        -- Head of an instance decl
 899
 900 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
 901 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
 902 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
 903 pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
 904 pprSourceTyCtxt InstHeadCtxt    = ptext SLIT("the head of an instance declaration")
 905 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
 906 \end{code}
 907
 908 \begin{code}
 909 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
 910 checkValidTheta ctxt theta
 911   = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
 912
 913 -------------------------
 914 check_valid_theta ctxt []
 915   = returnTc ()
 916 check_valid_theta ctxt theta
 917   = getDOptsTc                                  `thenNF_Tc` \ dflags ->
 918     warnTc (not (null dups)) (dupPredWarn dups) `thenNF_Tc_`
 919     mapTc_ (check_source_ty dflags ctxt) theta
 920   where
 921     (_,dups) = removeDups tcCmpPred theta
 922
 923 -------------------------
 924 check_source_ty dflags ctxt pred@(ClassP cls tys)
 925   =     -- Class predicates are valid in all contexts
 926     mapTc_ check_arg_type tys           `thenTc_`
 927     checkTc (arity == n_tys) arity_err          `thenTc_`
 928     checkTc (all tyvar_head tys || arby_preds_ok)
 929             (predTyVarErr pred $$ how_to_allow)
 930
 931   where
 932     class_name = className cls
 933     arity      = classArity cls
 934     n_tys      = length tys
 935     arity_err  = arityErr "Class" class_name arity n_tys
 936
 937     arby_preds_ok = case ctxt of
 938                         InstHeadCtxt  -> True   -- We check for instance-head formation
 939                                                 -- in checkValidInstHead
 940                         InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
 941                         other         -> dopt Opt_GlasgowExts               dflags
 942
 943     how_to_allow = case ctxt of
 944                      InstHeadCtxt  -> empty     -- Should not happen
 945                      InstThetaCtxt -> parens undecidableMsg
 946                      other         -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 947
 948 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
 949         -- Implicit parameters only allows in type
 950         -- signatures; not in instance decls, superclasses etc
 951         -- The reason for not allowing implicit params in instances is a bit subtle
 952         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
 953         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
 954         -- discharge all the potential usas of the ?x in e.   For example, a
 955         -- constraint Foo [Int] might come out of e,and applying the
 956         -- instance decl would show up two uses of ?x.
 957
 958 check_source_ty dflags TypeCtxt  (NType tc tys)   = mapTc_ check_arg_type tys
 959
 960 -- Catch-all
 961 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 962
 963 -------------------------
 964 tyvar_head ty                   -- Haskell 98 allows predicates of form
 965   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
 966   | otherwise                   -- where a is a type variable
 967   = case tcSplitAppTy_maybe ty of
 968         Just (ty, _) -> tyvar_head ty
 969         Nothing      -> False
 970 \end{code}
 971
 972 \begin{code}
 973 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
 974 predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
 975 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
 976
 977 checkThetaCtxt ctxt theta
 978   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
 979           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 980 \end{code}
 981
 982
 983 %************************************************************************
 984 %*                                                                      *
 985 \subsection{Checking for a decent instance head type}
 986 %*                                                                      *
 987 %************************************************************************
 988
 989 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
 990 it must normally look like: @instance Foo (Tycon a b c ...) ...@
 991
 992 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
 993 flag is on, or (2)~the instance is imported (they must have been
 994 compiled elsewhere). In these cases, we let them go through anyway.
 995
 996 We can also have instances for functions: @instance Foo (a -> b) ...@.
 997
 998 \begin{code}
 999 checkValidInstHead :: Type -> TcM (Class, [TcType])
1000
1001 checkValidInstHead ty   -- Should be a source type
1002   = case tcSplitPredTy_maybe ty of {
1003         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1004         Just pred ->
1005
1006     case getClassPredTys_maybe pred of {
1007         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1008         Just (clas,tys) ->
1009
1010     getDOptsTc                                  `thenNF_Tc` \ dflags ->
1011     mapTc_ check_arg_type tys                   `thenTc_`
1012     check_inst_head dflags clas tys             `thenTc_`
1013     returnTc (clas, tys)
1014     }}
1015
1016 check_inst_head dflags clas tys
1017   |     -- CCALL CHECK
1018         -- A user declaration of a CCallable/CReturnable instance
1019         -- must be for a "boxed primitive" type.
1020         (clas `hasKey` cCallableClassKey
1021             && not (ccallable_type first_ty))
1022   ||    (clas `hasKey` cReturnableClassKey
1023             && not (creturnable_type first_ty))
1024   = failWithTc (nonBoxedPrimCCallErr clas first_ty)
1025
1026         -- If GlasgowExts then check at least one isn't a type variable
1027   | dopt Opt_GlasgowExts dflags
1028   = check_tyvars dflags clas tys
1029
1030         -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1031   | isSingleton tys,
1032     Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1033     not (isSynTyCon tycon),             -- ...but not a synonym
1034     all tcIsTyVarTy arg_tys,            -- Applied to type variables
1035     equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1036           -- This last condition checks that all the type variables are distinct
1037   = returnTc ()
1038
1039   | otherwise
1040   = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1041
1042   where
1043     (first_ty : _)       = tys
1044
1045     ccallable_type   ty = isFFIArgumentTy dflags PlayRisky ty
1046     creturnable_type ty = isFFIImportResultTy dflags ty
1047
1048     head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1049                              text "where T is not a synonym, and a,b,c are distinct type variables")
1050
1051 check_tyvars dflags clas tys
1052         -- Check that at least one isn't a type variable
1053         -- unless -fallow-undecideable-instances
1054   | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
1055   | not (all tcIsTyVarTy tys)                 = returnTc ()
1056   | otherwise                                 = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1057   where
1058     msg =  parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1059                    $$ undecidableMsg)
1060
1061 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1062 \end{code}
1063
1064 \begin{code}
1065 instTypeErr pp_ty msg
1066   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1067          nest 4 msg]
1068
1069 nonBoxedPrimCCallErr clas inst_ty
1070   = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
1071          4 (pprClassPred clas [inst_ty])
1072 \end{code}