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   newFlexiTyVar,
  15   newFlexiTyVarTy,              -- Kind -> TcM TcType
  16   newFlexiTyVarTys,             -- Int -> Kind -> TcM [TcType]
  17   newKindVar, newKindVars,
  18   lookupTcTyVar, LookupTyVarResult(..),
  19   newMetaTyVar, readMetaTyVar, writeMetaTyVar,
  20
  21   --------------------------------
  22   -- Boxy type variables
  23   newBoxyTyVar, newBoxyTyVars, readFilledBox,
  24
  25   --------------------------------
  26   -- Instantiation
  27   tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxy, tcInstBoxyTyVar,
  28   tcInstSigTyVars, zonkSigTyVar,
  29   tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
  30   tcSkolSigType, tcSkolSigTyVars,
  31
  32   --------------------------------
  33   -- Checking type validity
  34   Rank, UserTypeCtxt(..), checkValidType,
  35   SourceTyCtxt(..), checkValidTheta, checkFreeness,
  36   checkValidInstHead, instTypeErr, checkAmbiguity,
  37   arityErr,
  38
  39   --------------------------------
  40   -- Zonking
  41   zonkType, zonkTcPredType,
  42   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
  43   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
  44   zonkTcKindToKind, zonkTcKind,
  45
  46   readKindVar, writeKindVar
  47
  48   ) where
  49
  50 #include "HsVersions.h"
  51
  52
  53 -- friends:
  54 import TypeRep          ( Type(..), PredType(..),  -- Friend; can see representation
  55                           ThetaType
  56                         )
  57 import TcType           ( TcType, TcThetaType, TcTauType, TcPredType,
  58                           TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..),
  59                           MetaDetails(..), SkolemInfo(..), BoxInfo(..),
  60                           BoxyTyVar, BoxyThetaType, BoxySigmaType,
  61                           UserTypeCtxt(..),
  62                           isMetaTyVar, isSigTyVar, metaTvRef,
  63                           tcCmpPred, isClassPred, tcEqType, tcGetTyVar,
  64                           tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
  65                           tcValidInstHeadTy, tcSplitForAllTys,
  66                           tcIsTyVarTy, tcSplitSigmaTy,
  67                           isUnLiftedType, isIPPred,
  68                           typeKind, isSkolemTyVar,
  69                           mkAppTy, mkTyVarTy, mkTyVarTys,
  70                           tyVarsOfPred, getClassPredTys_maybe,
  71                           tyVarsOfType, tyVarsOfTypes, tcView,
  72                           pprPred, pprTheta, pprClassPred )
  73 import Kind             ( Kind(..), KindVar, kindVarRef, mkKindVar,
  74                           isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
  75                           liftedTypeKind, openTypeKind, defaultKind
  76                         )
  77 import Type             ( TvSubst, zipTopTvSubst, substTy )
  78 import Class            ( Class, classArity, className )
  79 import TyCon            ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
  80                           tyConArity, tyConName )
  81 import Var              ( TyVar, tyVarKind, tyVarName, isTcTyVar,
  82                           mkTyVar, mkTcTyVar, tcTyVarDetails )
  83
  84         -- Assertions
  85 #ifdef DEBUG
  86 import TcType           ( isFlexi, isBoxyTyVar, isImmutableTyVar )
  87 import Kind             ( isSubKind )
  88 #endif
  89
  90 -- others:
  91 import TcRnMonad          -- TcType, amongst others
  92 import FunDeps          ( grow )
  93 import Name             ( Name, setNameUnique, mkSysTvName )
  94 import VarSet
  95 import DynFlags ( dopt, DynFlag(..) )
  96 import Util             ( nOfThem, isSingleton, notNull )
  97 import ListSetOps       ( removeDups, findDupsEq )
  98 import Outputable
  99 \end{code}
 100
 101
 102 %************************************************************************
 103 %*                                                                      *
 104         Instantiation in general
 105 %*                                                                      *
 106 %************************************************************************
 107
 108 \begin{code}
 109 tcInstType :: ([TyVar] -> TcM [TcTyVar])                -- How to instantiate the type variables
 110            -> TcType                                    -- Type to instantiate
 111            -> TcM ([TcTyVar], TcThetaType, TcType)      -- Result
 112 tcInstType inst_tyvars ty
 113   = case tcSplitForAllTys ty of
 114         ([],     rho) -> let    -- There may be overloading despite no type variables;
 115                                 --      (?x :: Int) => Int -> Int
 116                            (theta, tau) = tcSplitPhiTy rho
 117                          in
 118                          return ([], theta, tau)
 119
 120         (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
 121
 122                             ; let  tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
 123                                 -- Either the tyvars are freshly made, by inst_tyvars,
 124                                 -- or (in the call from tcSkolSigType) any nested foralls
 125                                 -- have different binders.  Either way, zipTopTvSubst is ok
 126
 127                             ; let  (theta, tau) = tcSplitPhiTy (substTy tenv rho)
 128                             ; return (tyvars', theta, tau) }
 129 \end{code}
 130
 131
 132 %************************************************************************
 133 %*                                                                      *
 134         Kind variables
 135 %*                                                                      *
 136 %************************************************************************
 137
 138 \begin{code}
 139 newKindVar :: TcM TcKind
 140 newKindVar = do { uniq <- newUnique
 141                 ; ref <- newMutVar Nothing
 142                 ; return (KindVar (mkKindVar uniq ref)) }
 143
 144 newKindVars :: Int -> TcM [TcKind]
 145 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
 146 \end{code}
 147
 148
 149 %************************************************************************
 150 %*                                                                      *
 151         SkolemTvs (immutable)
 152 %*                                                                      *
 153 %************************************************************************
 154
 155 \begin{code}
 156 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
 157 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
 158
 159 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
 160 -- Instantiate a type signature with skolem constants, but
 161 -- do *not* give them fresh names, because we want the name to
 162 -- be in the type environment -- it is lexically scoped.
 163 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
 164
 165 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
 166 -- Make skolem constants, but do *not* give them new names, as above
 167 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
 168                               | tv <- tyvars ]
 169
 170 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
 171 -- Instantiate a type with fresh skolem constants
 172 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
 173
 174 tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
 175 tcInstSkolTyVar info tyvar
 176   = do  { uniq <- newUnique
 177         ; let name = setNameUnique (tyVarName tyvar) uniq
 178               kind = tyVarKind tyvar
 179         ; return (mkSkolTyVar name kind info) }
 180
 181 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
 182 tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars
 183 \end{code}
 184
 185
 186 %************************************************************************
 187 %*                                                                      *
 188         MetaTvs (meta type variables; mutable)
 189 %*                                                                      *
 190 %************************************************************************
 191
 192 \begin{code}
 193 newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
 194 -- Make a new meta tyvar out of thin air
 195 newMetaTyVar box_info kind
 196   = do  { uniq <- newUnique
 197         ; ref <- newMutVar Flexi ;
 198         ; let name = mkSysTvName uniq fs
 199               fs = case box_info of
 200                         BoxTv   -> FSLIT("bx")
 201                         TauTv   -> FSLIT("t")
 202                         SigTv _ -> FSLIT("a")
 203         ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
 204
 205 instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
 206 -- Make a new meta tyvar whose Name and Kind
 207 -- come from an existing TyVar
 208 instMetaTyVar box_info tyvar
 209   = do  { uniq <- newUnique
 210         ; ref <- newMutVar Flexi ;
 211         ; let name = setNameUnique (tyVarName tyvar) uniq
 212               kind = tyVarKind tyvar
 213         ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
 214
 215 readMetaTyVar :: TyVar -> TcM MetaDetails
 216 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
 217                       readMutVar (metaTvRef tyvar)
 218
 219 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
 220 #ifndef DEBUG
 221 writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
 222 #else
 223 writeMetaTyVar tyvar ty
 224   | not (isMetaTyVar tyvar)
 225   = pprTrace "writeMetaTyVar" (ppr tyvar) $
 226     returnM ()
 227
 228   | otherwise
 229   = ASSERT( isMetaTyVar tyvar )
 230     ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
 231     do  { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
 232         ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
 233   where
 234     k1 = tyVarKind tyvar
 235     k2 = typeKind ty
 236 #endif
 237 \end{code}
 238
 239
 240 %************************************************************************
 241 %*                                                                      *
 242         MetaTvs: TauTvs
 243 %*                                                                      *
 244 %************************************************************************
 245
 246 \begin{code}
 247 newFlexiTyVar :: Kind -> TcM TcTyVar
 248 newFlexiTyVar kind = newMetaTyVar TauTv kind
 249
 250 newFlexiTyVarTy  :: Kind -> TcM TcType
 251 newFlexiTyVarTy kind
 252   = newFlexiTyVar kind  `thenM` \ tc_tyvar ->
 253     returnM (TyVarTy tc_tyvar)
 254
 255 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
 256 newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind)
 257
 258 tcInstTyVar :: TyVar -> TcM TcTyVar
 259 -- Instantiate with a META type variable
 260 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
 261
 262 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
 263 -- Instantiate with META type variables
 264 tcInstTyVars tyvars
 265   = do  { tc_tvs <- mapM tcInstTyVar tyvars
 266         ; let tys = mkTyVarTys tc_tvs
 267         ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
 268                 -- Since the tyvars are freshly made,
 269                 -- they cannot possibly be captured by
 270                 -- any existing for-alls.  Hence zipTopTvSubst
 271 \end{code}
 272
 273
 274 %************************************************************************
 275 %*                                                                      *
 276         MetaTvs: SigTvs
 277 %*                                                                      *
 278 %************************************************************************
 279
 280 \begin{code}
 281 tcInstSigTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
 282 -- Instantiate with meta SigTvs
 283 tcInstSigTyVars skol_info tyvars
 284   = mapM (instMetaTyVar (SigTv skol_info)) tyvars
 285
 286 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
 287 zonkSigTyVar sig_tv
 288   | isSkolemTyVar sig_tv
 289   = return sig_tv       -- Happens in the call in TcBinds.checkDistinctTyVars
 290   | otherwise
 291   = ASSERT( isSigTyVar sig_tv )
 292     do { ty <- zonkTcTyVar sig_tv
 293        ; return (tcGetTyVar "zonkSigTyVar" ty) }
 294         -- 'ty' is bound to be a type variable, because SigTvs
 295         -- can only be unified with type variables
 296 \end{code}
 297
 298
 299 %************************************************************************
 300 %*                                                                      *
 301         MetaTvs: BoxTvs
 302 %*                                                                      *
 303 %************************************************************************
 304
 305 \begin{code}
 306 newBoxyTyVar :: TcM BoxyTyVar           -- Of openTypeKind
 307 newBoxyTyVar = newMetaTyVar BoxTv openTypeKind
 308
 309 newBoxyTyVars :: Int -> TcM [BoxyTyVar]         -- Of openTypeKind
 310 newBoxyTyVars n = sequenceM [newMetaTyVar BoxTv openTypeKind | i <- [1..n]]
 311
 312 readFilledBox :: BoxyTyVar -> TcM TcType
 313 -- Read the contents of the box, which should be filled in by now
 314 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
 315                        do { cts <- readMetaTyVar box_tv
 316                           ; case cts of
 317                                 Flexi       -> pprPanic "readFilledBox" (ppr box_tv)
 318                                 Indirect ty -> return ty }
 319
 320 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
 321 -- Instantiate with a BOXY type variable
 322 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
 323
 324 tcInstBoxy :: TcType -> TcM ([BoxyTyVar], BoxyThetaType, BoxySigmaType)
 325 -- tcInstType instantiates the outer-level for-alls of a TcType with
 326 -- fresh BOXY type variables, splits off the dictionary part,
 327 -- and returns the pieces.
 328 tcInstBoxy ty = tcInstType (mapM tcInstBoxyTyVar) ty
 329 \end{code}
 330
 331
 332 %************************************************************************
 333 %*                                                                      *
 334 \subsection{Putting and getting  mutable type variables}
 335 %*                                                                      *
 336 %************************************************************************
 337
 338 But it's more fun to short out indirections on the way: If this
 339 version returns a TyVar, then that TyVar is unbound.  If it returns
 340 any other type, then there might be bound TyVars embedded inside it.
 341
 342 We return Nothing iff the original box was unbound.
 343
 344 \begin{code}
 345 data LookupTyVarResult  -- The result of a lookupTcTyVar call
 346   = DoneTv TcTyVarDetails       -- SkolemTv or virgin MetaTv
 347   | IndirectTv TcType
 348
 349 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
 350 lookupTcTyVar tyvar
 351   = case details of
 352       SkolemTv _   -> return (DoneTv details)
 353       MetaTv _ ref -> do { meta_details <- readMutVar ref
 354                          ; case meta_details of
 355                             Indirect ty -> return (IndirectTv ty)
 356                             Flexi       -> return (DoneTv details) }
 357   where
 358     details =  tcTyVarDetails tyvar
 359
 360 {-
 361 -- gaw 2004 We aren't shorting anything out anymore, at least for now
 362 getTcTyVar tyvar
 363   | not (isTcTyVar tyvar)
 364   = pprTrace "getTcTyVar" (ppr tyvar) $
 365     returnM (Just (mkTyVarTy tyvar))
 366
 367   | otherwise
 368   = ASSERT2( isTcTyVar tyvar, ppr tyvar )
 369     readMetaTyVar tyvar                         `thenM` \ maybe_ty ->
 370     case maybe_ty of
 371         Just ty -> short_out ty                         `thenM` \ ty' ->
 372                    writeMetaTyVar tyvar (Just ty')      `thenM_`
 373                    returnM (Just ty')
 374
 375         Nothing    -> returnM Nothing
 376
 377 short_out :: TcType -> TcM TcType
 378 short_out ty@(TyVarTy tyvar)
 379   | not (isTcTyVar tyvar)
 380   = returnM ty
 381
 382   | otherwise
 383   = readMetaTyVar tyvar `thenM` \ maybe_ty ->
 384     case maybe_ty of
 385         Just ty' -> short_out ty'                       `thenM` \ ty' ->
 386                     writeMetaTyVar tyvar (Just ty')     `thenM_`
 387                     returnM ty'
 388
 389         other    -> returnM ty
 390
 391 short_out other_ty = returnM other_ty
 392 -}
 393 \end{code}
 394
 395
 396 %************************************************************************
 397 %*                                                                      *
 398 \subsection{Zonking -- the exernal interfaces}
 399 %*                                                                      *
 400 %************************************************************************
 401
 402 -----------------  Type variables
 403
 404 \begin{code}
 405 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
 406 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
 407
 408 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
 409 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars     `thenM` \ tys ->
 410                            returnM (tyVarsOfTypes tys)
 411
 412 zonkTcTyVar :: TcTyVar -> TcM TcType
 413 zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
 414                     zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
 415 \end{code}
 416
 417 -----------------  Types
 418
 419 \begin{code}
 420 zonkTcType :: TcType -> TcM TcType
 421 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
 422
 423 zonkTcTypes :: [TcType] -> TcM [TcType]
 424 zonkTcTypes tys = mappM zonkTcType tys
 425
 426 zonkTcClassConstraints cts = mappM zonk cts
 427     where zonk (clas, tys)
 428             = zonkTcTypes tys   `thenM` \ new_tys ->
 429               returnM (clas, new_tys)
 430
 431 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
 432 zonkTcThetaType theta = mappM zonkTcPredType theta
 433
 434 zonkTcPredType :: TcPredType -> TcM TcPredType
 435 zonkTcPredType (ClassP c ts)
 436   = zonkTcTypes ts      `thenM` \ new_ts ->
 437     returnM (ClassP c new_ts)
 438 zonkTcPredType (IParam n t)
 439   = zonkTcType t        `thenM` \ new_t ->
 440     returnM (IParam n new_t)
 441 \end{code}
 442
 443 -------------------  These ...ToType, ...ToKind versions
 444                      are used at the end of type checking
 445
 446 \begin{code}
 447 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
 448 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
 449 -- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
 450 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
 451 -- The meta tyvar is updated to point to the new regular TyVar.  Now any
 452 -- bound occurences of the original type variable will get zonked to
 453 -- the immutable version.
 454 --
 455 -- We leave skolem TyVars alone; they are immutable.
 456 zonkQuantifiedTyVar tv
 457   | isSkolemTyVar tv = return tv
 458         -- It might be a skolem type variable,
 459         -- for example from a user type signature
 460
 461   | otherwise   -- It's a meta-type-variable
 462   = do  { details <- readMetaTyVar tv
 463
 464         -- Create the new, frozen, regular type variable
 465         ; let final_kind = defaultKind (tyVarKind tv)
 466               final_tv   = mkTyVar (tyVarName tv) final_kind
 467
 468         -- Bind the meta tyvar to the new tyvar
 469         ; case details of
 470             Indirect ty -> WARN( True, ppr tv $$ ppr ty )
 471                            return ()
 472                 -- [Sept 04] I don't think this should happen
 473                 -- See note [Silly Type Synonym]
 474
 475             Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
 476
 477         -- Return the new tyvar
 478         ; return final_tv }
 479 \end{code}
 480
 481 [Silly Type Synonyms]
 482
 483 Consider this:
 484         type C u a = u  -- Note 'a' unused
 485
 486         foo :: (forall a. C u a -> C u a) -> u
 487         foo x = ...
 488
 489         bar :: Num u => u
 490         bar = foo (\t -> t + t)
 491
 492 * From the (\t -> t+t) we get type  {Num d} =>  d -> d
 493   where d is fresh.
 494
 495 * Now unify with type of foo's arg, and we get:
 496         {Num (C d a)} =>  C d a -> C d a
 497   where a is fresh.
 498
 499 * Now abstract over the 'a', but float out the Num (C d a) constraint
 500   because it does not 'really' mention a.  (see exactTyVarsOfType)
 501   The arg to foo becomes
 502         /\a -> \t -> t+t
 503
 504 * So we get a dict binding for Num (C d a), which is zonked to give
 505         a = ()
 506   [Note Sept 04: now that we are zonking quantified type variables
 507   on construction, the 'a' will be frozen as a regular tyvar on
 508   quantification, so the floated dict will still have type (C d a).
 509   Which renders this whole note moot; happily!]
 510
 511 * Then the /\a abstraction has a zonked 'a' in it.
 512
 513 All very silly.   I think its harmless to ignore the problem.  We'll end up with
 514 a /\a in the final result but all the occurrences of a will be zonked to ()
 515
 516
 517 %************************************************************************
 518 %*                                                                      *
 519 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
 520 %*                                                                      *
 521 %*              For internal use only!                                  *
 522 %*                                                                      *
 523 %************************************************************************
 524
 525 \begin{code}
 526 -- For unbound, mutable tyvars, zonkType uses the function given to it
 527 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 528 --      type variable and zonks the kind too
 529
 530 zonkType :: (TcTyVar -> TcM Type)       -- What to do with unbound mutable type variables
 531                                         -- see zonkTcType, and zonkTcTypeToType
 532          -> TcType
 533          -> TcM Type
 534 zonkType unbound_var_fn ty
 535   = go ty
 536   where
 537     go (NoteTy _ ty2)    = go ty2       -- Discard free-tyvar annotations
 538
 539     go (TyConApp tc tys) = mappM go tys `thenM` \ tys' ->
 540                            returnM (TyConApp tc tys')
 541
 542     go (PredTy p)        = go_pred p            `thenM` \ p' ->
 543                            returnM (PredTy p')
 544
 545     go (FunTy arg res)   = go arg               `thenM` \ arg' ->
 546                            go res               `thenM` \ res' ->
 547                            returnM (FunTy arg' res')
 548
 549     go (AppTy fun arg)   = go fun               `thenM` \ fun' ->
 550                            go arg               `thenM` \ arg' ->
 551                            returnM (mkAppTy fun' arg')
 552                 -- NB the mkAppTy; we might have instantiated a
 553                 -- type variable to a type constructor, so we need
 554                 -- to pull the TyConApp to the top.
 555
 556         -- The two interesting cases!
 557     go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
 558                        | otherwise       = return (TyVarTy tyvar)
 559                 -- Ordinary (non Tc) tyvars occur inside quantified types
 560
 561     go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
 562                              go ty              `thenM` \ ty' ->
 563                              returnM (ForAllTy tyvar ty')
 564
 565     go_pred (ClassP c tys) = mappM go tys       `thenM` \ tys' ->
 566                              returnM (ClassP c tys')
 567     go_pred (IParam n ty)  = go ty              `thenM` \ ty' ->
 568                              returnM (IParam n ty')
 569
 570 zonk_tc_tyvar :: (TcTyVar -> TcM Type)          -- What to do for an unbound mutable variable
 571               -> TcTyVar -> TcM TcType
 572 zonk_tc_tyvar unbound_var_fn tyvar
 573   | not (isMetaTyVar tyvar)     -- Skolems
 574   = returnM (TyVarTy tyvar)
 575
 576   | otherwise                   -- Mutables
 577   = do  { cts <- readMetaTyVar tyvar
 578         ; case cts of
 579             Flexi       -> unbound_var_fn tyvar    -- Unbound meta type variable
 580             Indirect ty -> zonkType unbound_var_fn ty  }
 581 \end{code}
 582
 583
 584
 585 %************************************************************************
 586 %*                                                                      *
 587                         Zonking kinds
 588 %*                                                                      *
 589 %************************************************************************
 590
 591 \begin{code}
 592 readKindVar  :: KindVar -> TcM (Maybe TcKind)
 593 writeKindVar :: KindVar -> TcKind -> TcM ()
 594 readKindVar  kv = readMutVar (kindVarRef kv)
 595 writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
 596
 597 -------------
 598 zonkTcKind :: TcKind -> TcM TcKind
 599 zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
 600                                 ; k2' <- zonkTcKind k2
 601                                 ; returnM (FunKind k1' k2') }
 602 zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv
 603                                ; case mb_kind of
 604                                     Nothing -> returnM k
 605                                     Just k  -> zonkTcKind k }
 606 zonkTcKind other_kind = returnM other_kind
 607
 608 -------------
 609 zonkTcKindToKind :: TcKind -> TcM Kind
 610 zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
 611                                       ; k2' <- zonkTcKindToKind k2
 612                                       ; returnM (FunKind k1' k2') }
 613
 614 zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv
 615                                    ; case mb_kind of
 616                                        Nothing -> return liftedTypeKind
 617                                        Just k  -> zonkTcKindToKind k }
 618
 619 zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind  -- An "Open" kind defaults to *
 620 zonkTcKindToKind other_kind   = returnM other_kind
 621 \end{code}
 622
 623 %************************************************************************
 624 %*                                                                      *
 625 \subsection{Checking a user type}
 626 %*                                                                      *
 627 %************************************************************************
 628
 629 When dealing with a user-written type, we first translate it from an HsType
 630 to a Type, performing kind checking, and then check various things that should
 631 be true about it.  We don't want to perform these checks at the same time
 632 as the initial translation because (a) they are unnecessary for interface-file
 633 types and (b) when checking a mutually recursive group of type and class decls,
 634 we can't "look" at the tycons/classes yet.  Also, the checks are are rather
 635 diverse, and used to really mess up the other code.
 636
 637 One thing we check for is 'rank'.
 638
 639         Rank 0:         monotypes (no foralls)
 640         Rank 1:         foralls at the front only, Rank 0 inside
 641         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
 642
 643         basic ::= tyvar | T basic ... basic
 644
 645         r2  ::= forall tvs. cxt => r2a
 646         r2a ::= r1 -> r2a | basic
 647         r1  ::= forall tvs. cxt => r0
 648         r0  ::= r0 -> r0 | basic
 649
 650 Another thing is to check that type synonyms are saturated.
 651 This might not necessarily show up in kind checking.
 652         type A i = i
 653         data T k = MkT (k Int)
 654         f :: T A        -- BAD!
 655
 656
 657 \begin{code}
 658 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 659 -- Checks that the type is valid for the given context
 660 checkValidType ctxt ty
 661   = traceTc (text "checkValidType" <+> ppr ty)  `thenM_`
 662     doptM Opt_GlasgowExts       `thenM` \ gla_exts ->
 663     let
 664         rank | gla_exts = Arbitrary
 665              | otherwise
 666              = case ctxt of     -- Haskell 98
 667                  GenPatCtxt     -> Rank 0
 668                  LamPatSigCtxt  -> Rank 0
 669                  BindPatSigCtxt -> Rank 0
 670                  DefaultDeclCtxt-> Rank 0
 671                  ResSigCtxt     -> Rank 0
 672                  TySynCtxt _    -> Rank 0
 673                  ExprSigCtxt    -> Rank 1
 674                  FunSigCtxt _   -> Rank 1
 675                  ConArgCtxt _   -> Rank 1       -- We are given the type of the entire
 676                                                 -- constructor, hence rank 1
 677                  ForSigCtxt _   -> Rank 1
 678                  RuleSigCtxt _  -> Rank 1
 679                  SpecInstCtxt   -> Rank 1
 680
 681         actual_kind = typeKind ty
 682
 683         kind_ok = case ctxt of
 684                         TySynCtxt _  -> True    -- Any kind will do
 685                         ResSigCtxt   -> isOpenTypeKind   actual_kind
 686                         ExprSigCtxt  -> isOpenTypeKind   actual_kind
 687                         GenPatCtxt   -> isLiftedTypeKind actual_kind
 688                         ForSigCtxt _ -> isLiftedTypeKind actual_kind
 689                         other        -> isArgTypeKind    actual_kind
 690
 691         ubx_tup | not gla_exts = UT_NotOk
 692                 | otherwise    = case ctxt of
 693                                    TySynCtxt _ -> UT_Ok
 694                                    ExprSigCtxt -> UT_Ok
 695                                    other       -> UT_NotOk
 696                 -- Unboxed tuples ok in function results,
 697                 -- but for type synonyms we allow them even at
 698                 -- top level
 699     in
 700         -- Check that the thing has kind Type, and is lifted if necessary
 701     checkTc kind_ok (kindErr actual_kind)       `thenM_`
 702
 703         -- Check the internal validity of the type itself
 704     check_poly_type rank ubx_tup ty             `thenM_`
 705
 706     traceTc (text "checkValidType done" <+> ppr ty)
 707 \end{code}
 708
 709
 710 \begin{code}
 711 data Rank = Rank Int | Arbitrary
 712
 713 decRank :: Rank -> Rank
 714 decRank Arbitrary = Arbitrary
 715 decRank (Rank n)  = Rank (n-1)
 716
 717 ----------------------------------------
 718 data UbxTupFlag = UT_Ok | UT_NotOk
 719         -- The "Ok" version means "ok if -fglasgow-exts is on"
 720
 721 ----------------------------------------
 722 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 723 check_poly_type (Rank 0) ubx_tup ty
 724   = check_tau_type (Rank 0) ubx_tup ty
 725
 726 check_poly_type rank ubx_tup ty
 727   = let
 728         (tvs, theta, tau) = tcSplitSigmaTy ty
 729     in
 730     check_valid_theta SigmaCtxt theta           `thenM_`
 731     check_tau_type (decRank rank) ubx_tup tau   `thenM_`
 732     checkFreeness tvs theta                     `thenM_`
 733     checkAmbiguity tvs theta (tyVarsOfType tau)
 734
 735 ----------------------------------------
 736 check_arg_type :: Type -> TcM ()
 737 -- The sort of type that can instantiate a type variable,
 738 -- or be the argument of a type constructor.
 739 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
 740 -- Other unboxed types are very occasionally allowed as type
 741 -- arguments depending on the kind of the type constructor
 742 --
 743 -- For example, we want to reject things like:
 744 --
 745 --      instance Ord a => Ord (forall s. T s a)
 746 -- and
 747 --      g :: T s (forall b.b)
 748 --
 749 -- NB: unboxed tuples can have polymorphic or unboxed args.
 750 --     This happens in the workers for functions returning
 751 --     product types with polymorphic components.
 752 --     But not in user code.
 753 -- Anyway, they are dealt with by a special case in check_tau_type
 754
 755 check_arg_type ty
 756   = check_poly_type Arbitrary UT_NotOk ty       `thenM_`
 757     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 758
 759 ----------------------------------------
 760 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 761 -- Rank is allowed rank for function args
 762 -- No foralls otherwise
 763
 764 check_tau_type rank ubx_tup ty@(ForAllTy _ _)       = failWithTc (forAllTyErr ty)
 765 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
 766         -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
 767
 768 -- Naked PredTys don't usually show up, but they can as a result of
 769 --      {-# SPECIALISE instance Ord Char #-}
 770 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
 771 -- are handled, but the quick thing is just to permit PredTys here.
 772 check_tau_type rank ubx_tup (PredTy sty) = getDOpts             `thenM` \ dflags ->
 773                                            check_source_ty dflags TypeCtxt sty
 774
 775 check_tau_type rank ubx_tup (TyVarTy _)       = returnM ()
 776 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
 777   = check_poly_type rank UT_NotOk arg_ty        `thenM_`
 778     check_poly_type rank UT_Ok    res_ty
 779
 780 check_tau_type rank ubx_tup (AppTy ty1 ty2)
 781   = check_arg_type ty1 `thenM_` check_arg_type ty2
 782
 783 check_tau_type rank ubx_tup (NoteTy other_note ty)
 784   = check_tau_type rank ubx_tup ty
 785
 786 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
 787   | isSynTyCon tc
 788   = do  {       -- 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         ; case tcView ty of
 793              Just ty' -> check_tau_type rank ubx_tup ty'        -- Check expansion
 794              Nothing  -> failWithTc arity_msg
 795
 796         ; gla_exts <- doptM Opt_GlasgowExts
 797         ; if gla_exts then
 798         -- If -fglasgow-exts then don't check the type arguments
 799         -- This allows us to instantiate a synonym defn with a
 800         -- for-all type, or with a partially-applied type synonym.
 801         --      e.g.   type T a b = a
 802         --             type S m   = m ()
 803         --             f :: S (T Int)
 804         -- Here, T is partially applied, so it's illegal in H98.
 805         -- But if you expand S first, then T we get just
 806         --             f :: Int
 807         -- which is fine.
 808                 returnM ()
 809           else
 810                 -- For H98, do check the type args
 811                 mappM_ check_arg_type tys
 812         }
 813
 814   | isUnboxedTupleTyCon tc
 815   = doptM Opt_GlasgowExts                       `thenM` \ gla_exts ->
 816     checkTc (ubx_tup_ok gla_exts) ubx_tup_msg   `thenM_`
 817     mappM_ (check_tau_type (Rank 0) UT_Ok) tys
 818                 -- Args are allowed to be unlifted, or
 819                 -- more unboxed tuples, so can't use check_arg_ty
 820
 821   | otherwise
 822   = mappM_ check_arg_type tys
 823
 824   where
 825     ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
 826
 827     n_args    = length tys
 828     tc_arity  = tyConArity tc
 829
 830     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
 831     ubx_tup_msg = ubxArgTyErr ty
 832
 833 ----------------------------------------
 834 forAllTyErr     ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
 835 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
 836 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
 837 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 838 \end{code}
 839
 840
 841
 842 %************************************************************************
 843 %*                                                                      *
 844 \subsection{Checking a theta or source type}
 845 %*                                                                      *
 846 %************************************************************************
 847
 848 \begin{code}
 849 -- Enumerate the contexts in which a "source type", <S>, can occur
 850 --      Eq a
 851 -- or   ?x::Int
 852 -- or   r <: {x::Int}
 853 -- or   (N a) where N is a newtype
 854
 855 data SourceTyCtxt
 856   = ClassSCCtxt Name    -- Superclasses of clas
 857                         --      class <S> => C a where ...
 858   | SigmaCtxt           -- Theta part of a normal for-all type
 859                         --      f :: <S> => a -> a
 860   | DataTyCtxt Name     -- Theta part of a data decl
 861                         --      data <S> => T a = MkT a
 862   | TypeCtxt            -- Source type in an ordinary type
 863                         --      f :: N a -> N a
 864   | InstThetaCtxt       -- Context of an instance decl
 865                         --      instance <S> => C [a] where ...
 866   | InstHeadCtxt        -- Head of an instance decl
 867                         --      instance ... => Eq a where ...
 868
 869 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
 870 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
 871 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
 872 pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
 873 pprSourceTyCtxt InstHeadCtxt    = ptext SLIT("the head of an instance declaration")
 874 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
 875 \end{code}
 876
 877 \begin{code}
 878 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
 879 checkValidTheta ctxt theta
 880   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
 881
 882 -------------------------
 883 check_valid_theta ctxt []
 884   = returnM ()
 885 check_valid_theta ctxt theta
 886   = getDOpts                                    `thenM` \ dflags ->
 887     warnTc (notNull dups) (dupPredWarn dups)    `thenM_`
 888     mappM_ (check_source_ty dflags ctxt) theta
 889   where
 890     (_,dups) = removeDups tcCmpPred theta
 891
 892 -------------------------
 893 check_source_ty dflags ctxt pred@(ClassP cls tys)
 894   =     -- Class predicates are valid in all contexts
 895     checkTc (arity == n_tys) arity_err          `thenM_`
 896
 897         -- Check the form of the argument types
 898     mappM_ check_arg_type tys                           `thenM_`
 899     checkTc (check_class_pred_tys dflags ctxt tys)
 900             (predTyVarErr pred $$ how_to_allow)
 901
 902   where
 903     class_name = className cls
 904     arity      = classArity cls
 905     n_tys      = length tys
 906     arity_err  = arityErr "Class" class_name arity n_tys
 907
 908     how_to_allow = case ctxt of
 909                      InstHeadCtxt  -> empty     -- Should not happen
 910                      InstThetaCtxt -> parens undecidableMsg
 911                      other         -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 912
 913 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
 914         -- Implicit parameters only allows in type
 915         -- signatures; not in instance decls, superclasses etc
 916         -- The reason for not allowing implicit params in instances is a bit subtle
 917         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
 918         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
 919         -- discharge all the potential usas of the ?x in e.   For example, a
 920         -- constraint Foo [Int] might come out of e,and applying the
 921         -- instance decl would show up two uses of ?x.
 922
 923 -- Catch-all
 924 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 925
 926 -------------------------
 927 check_class_pred_tys dflags ctxt tys
 928   = case ctxt of
 929         TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
 930         InstHeadCtxt  -> True   -- We check for instance-head
 931                                 -- formation in checkValidInstHead
 932         InstThetaCtxt -> undecidable_ok || distinct_tyvars tys
 933         other         -> gla_exts       || all tyvar_head tys
 934   where
 935     undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
 936     gla_exts       = dopt Opt_GlasgowExts dflags
 937
 938 -------------------------
 939 distinct_tyvars tys     -- Check that the types are all distinct type variables
 940   = all tcIsTyVarTy tys && null (findDupsEq tcEqType tys)
 941
 942 -------------------------
 943 tyvar_head ty                   -- Haskell 98 allows predicates of form
 944   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
 945   | otherwise                   -- where a is a type variable
 946   = case tcSplitAppTy_maybe ty of
 947         Just (ty, _) -> tyvar_head ty
 948         Nothing      -> False
 949 \end{code}
 950
 951 Check for ambiguity
 952 ~~~~~~~~~~~~~~~~~~~
 953           forall V. P => tau
 954 is ambiguous if P contains generic variables
 955 (i.e. one of the Vs) that are not mentioned in tau
 956
 957 However, we need to take account of functional dependencies
 958 when we speak of 'mentioned in tau'.  Example:
 959         class C a b | a -> b where ...
 960 Then the type
 961         forall x y. (C x y) => x
 962 is not ambiguous because x is mentioned and x determines y
 963
 964 NB; the ambiguity check is only used for *user* types, not for types
 965 coming from inteface files.  The latter can legitimately have
 966 ambiguous types. Example
 967
 968    class S a where s :: a -> (Int,Int)
 969    instance S Char where s _ = (1,1)
 970    f:: S a => [a] -> Int -> (Int,Int)
 971    f (_::[a]) x = (a*x,b)
 972         where (a,b) = s (undefined::a)
 973
 974 Here the worker for f gets the type
 975         fw :: forall a. S a => Int -> (# Int, Int #)
 976
 977 If the list of tv_names is empty, we have a monotype, and then we
 978 don't need to check for ambiguity either, because the test can't fail
 979 (see is_ambig).
 980
 981 \begin{code}
 982 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
 983 checkAmbiguity forall_tyvars theta tau_tyvars
 984   = mappM_ complain (filter is_ambig theta)
 985   where
 986     complain pred     = addErrTc (ambigErr pred)
 987     extended_tau_vars = grow theta tau_tyvars
 988
 989         -- Only a *class* predicate can give rise to ambiguity
 990         -- An *implicit parameter* cannot.  For example:
 991         --      foo :: (?x :: [a]) => Int
 992         --      foo = length ?x
 993         -- is fine.  The call site will suppply a particular 'x'
 994     is_ambig pred     = isClassPred  pred &&
 995                         any ambig_var (varSetElems (tyVarsOfPred pred))
 996
 997     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
 998                         not (ct_var `elemVarSet` extended_tau_vars)
 999
1000 ambigErr pred
1001   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1002          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1003                  ptext SLIT("must be reachable from the type after the '=>'"))]
1004 \end{code}
1005
1006 In addition, GHC insists that at least one type variable
1007 in each constraint is in V.  So we disallow a type like
1008         forall a. Eq b => b -> b
1009 even in a scope where b is in scope.
1010
1011 \begin{code}
1012 checkFreeness forall_tyvars theta
1013   = mappM_ complain (filter is_free theta)
1014   where
1015     is_free pred     =  not (isIPPred pred)
1016                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1017     bound_var ct_var = ct_var `elem` forall_tyvars
1018     complain pred    = addErrTc (freeErr pred)
1019
1020 freeErr pred
1021   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1022                    ptext SLIT("are already in scope"),
1023          nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1024     ]
1025 \end{code}
1026
1027 \begin{code}
1028 checkThetaCtxt ctxt theta
1029   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1030           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1031
1032 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1033 predTyVarErr pred  = sep [ptext SLIT("Non-type variables, or repeated type variables,"),
1034                           nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1035 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1036
1037 arityErr kind name n m
1038   = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1039            n_arguments <> comma, text "but has been given", int m]
1040     where
1041         n_arguments | n == 0 = ptext SLIT("no arguments")
1042                     | n == 1 = ptext SLIT("1 argument")
1043                     | True   = hsep [int n, ptext SLIT("arguments")]
1044 \end{code}
1045
1046
1047 %************************************************************************
1048 %*                                                                      *
1049 \subsection{Checking for a decent instance head type}
1050 %*                                                                      *
1051 %************************************************************************
1052
1053 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1054 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1055
1056 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1057 flag is on, or (2)~the instance is imported (they must have been
1058 compiled elsewhere). In these cases, we let them go through anyway.
1059
1060 We can also have instances for functions: @instance Foo (a -> b) ...@.
1061
1062 \begin{code}
1063 checkValidInstHead :: Type -> TcM (Class, [TcType])
1064
1065 checkValidInstHead ty   -- Should be a source type
1066   = case tcSplitPredTy_maybe ty of {
1067         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1068         Just pred ->
1069
1070     case getClassPredTys_maybe pred of {
1071         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1072         Just (clas,tys) ->
1073
1074     getDOpts                                    `thenM` \ dflags ->
1075     mappM_ check_arg_type tys                   `thenM_`
1076     check_inst_head dflags clas tys             `thenM_`
1077     returnM (clas, tys)
1078     }}
1079
1080 check_inst_head dflags clas tys
1081         -- If GlasgowExts then check at least one isn't a type variable
1082   | dopt Opt_GlasgowExts dflags
1083   = check_tyvars dflags clas tys
1084
1085         -- WITH HASKELL 98, MUST HAVE C (T a b c)
1086   | isSingleton tys,
1087     tcValidInstHeadTy first_ty
1088   = returnM ()
1089
1090   | otherwise
1091   = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1092
1093   where
1094     (first_ty : _) = tys
1095
1096     head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1097                              text "where T is not a synonym, and a,b,c are distinct type variables")
1098
1099 check_tyvars dflags clas tys
1100         -- Check that at least one isn't a type variable
1101         -- unless -fallow-undecideable-instances
1102   | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1103   | not (all tcIsTyVarTy tys)                 = returnM ()
1104   | otherwise                                 = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1105   where
1106     msg =  parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1107                    $$ undecidableMsg)
1108
1109 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1110 \end{code}
1111
1112 \begin{code}
1113 instTypeErr pp_ty msg
1114   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1115          nest 4 msg]
1116 \end{code}