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, newBoxyTyVarTys, 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, BoxyType, 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, 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 :: Kind -> TcM BoxyTyVar
 307 newBoxyTyVar kind = newMetaTyVar BoxTv kind
 308
 309 newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
 310 newBoxyTyVars kinds = mapM newBoxyTyVar kinds
 311
 312 newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
 313 newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
 314
 315 readFilledBox :: BoxyTyVar -> TcM TcType
 316 -- Read the contents of the box, which should be filled in by now
 317 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
 318                        do { cts <- readMetaTyVar box_tv
 319                           ; case cts of
 320                                 Flexi       -> pprPanic "readFilledBox" (ppr box_tv)
 321                                 Indirect ty -> return ty }
 322
 323 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
 324 -- Instantiate with a BOXY type variable
 325 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
 326
 327 tcInstBoxy :: TcType -> TcM ([BoxyTyVar], BoxyThetaType, BoxySigmaType)
 328 -- tcInstType instantiates the outer-level for-alls of a TcType with
 329 -- fresh BOXY type variables, splits off the dictionary part,
 330 -- and returns the pieces.
 331 tcInstBoxy ty = tcInstType (mapM tcInstBoxyTyVar) ty
 332 \end{code}
 333
 334
 335 %************************************************************************
 336 %*                                                                      *
 337 \subsection{Putting and getting  mutable type variables}
 338 %*                                                                      *
 339 %************************************************************************
 340
 341 But it's more fun to short out indirections on the way: If this
 342 version returns a TyVar, then that TyVar is unbound.  If it returns
 343 any other type, then there might be bound TyVars embedded inside it.
 344
 345 We return Nothing iff the original box was unbound.
 346
 347 \begin{code}
 348 data LookupTyVarResult  -- The result of a lookupTcTyVar call
 349   = DoneTv TcTyVarDetails       -- SkolemTv or virgin MetaTv
 350   | IndirectTv TcType
 351
 352 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
 353 lookupTcTyVar tyvar
 354   = case details of
 355       SkolemTv _   -> return (DoneTv details)
 356       MetaTv _ ref -> do { meta_details <- readMutVar ref
 357                          ; case meta_details of
 358                             Indirect ty -> return (IndirectTv ty)
 359                             Flexi       -> return (DoneTv details) }
 360   where
 361     details =  tcTyVarDetails tyvar
 362
 363 {-
 364 -- gaw 2004 We aren't shorting anything out anymore, at least for now
 365 getTcTyVar tyvar
 366   | not (isTcTyVar tyvar)
 367   = pprTrace "getTcTyVar" (ppr tyvar) $
 368     returnM (Just (mkTyVarTy tyvar))
 369
 370   | otherwise
 371   = ASSERT2( isTcTyVar tyvar, ppr tyvar )
 372     readMetaTyVar tyvar                         `thenM` \ maybe_ty ->
 373     case maybe_ty of
 374         Just ty -> short_out ty                         `thenM` \ ty' ->
 375                    writeMetaTyVar tyvar (Just ty')      `thenM_`
 376                    returnM (Just ty')
 377
 378         Nothing    -> returnM Nothing
 379
 380 short_out :: TcType -> TcM TcType
 381 short_out ty@(TyVarTy tyvar)
 382   | not (isTcTyVar tyvar)
 383   = returnM ty
 384
 385   | otherwise
 386   = readMetaTyVar tyvar `thenM` \ maybe_ty ->
 387     case maybe_ty of
 388         Just ty' -> short_out ty'                       `thenM` \ ty' ->
 389                     writeMetaTyVar tyvar (Just ty')     `thenM_`
 390                     returnM ty'
 391
 392         other    -> returnM ty
 393
 394 short_out other_ty = returnM other_ty
 395 -}
 396 \end{code}
 397
 398
 399 %************************************************************************
 400 %*                                                                      *
 401 \subsection{Zonking -- the exernal interfaces}
 402 %*                                                                      *
 403 %************************************************************************
 404
 405 -----------------  Type variables
 406
 407 \begin{code}
 408 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
 409 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
 410
 411 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
 412 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars     `thenM` \ tys ->
 413                            returnM (tyVarsOfTypes tys)
 414
 415 zonkTcTyVar :: TcTyVar -> TcM TcType
 416 zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
 417                     zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
 418 \end{code}
 419
 420 -----------------  Types
 421
 422 \begin{code}
 423 zonkTcType :: TcType -> TcM TcType
 424 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
 425
 426 zonkTcTypes :: [TcType] -> TcM [TcType]
 427 zonkTcTypes tys = mappM zonkTcType tys
 428
 429 zonkTcClassConstraints cts = mappM zonk cts
 430     where zonk (clas, tys)
 431             = zonkTcTypes tys   `thenM` \ new_tys ->
 432               returnM (clas, new_tys)
 433
 434 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
 435 zonkTcThetaType theta = mappM zonkTcPredType theta
 436
 437 zonkTcPredType :: TcPredType -> TcM TcPredType
 438 zonkTcPredType (ClassP c ts)
 439   = zonkTcTypes ts      `thenM` \ new_ts ->
 440     returnM (ClassP c new_ts)
 441 zonkTcPredType (IParam n t)
 442   = zonkTcType t        `thenM` \ new_t ->
 443     returnM (IParam n new_t)
 444 \end{code}
 445
 446 -------------------  These ...ToType, ...ToKind versions
 447                      are used at the end of type checking
 448
 449 \begin{code}
 450 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
 451 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
 452 -- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
 453 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
 454 -- The meta tyvar is updated to point to the new regular TyVar.  Now any
 455 -- bound occurences of the original type variable will get zonked to
 456 -- the immutable version.
 457 --
 458 -- We leave skolem TyVars alone; they are immutable.
 459 zonkQuantifiedTyVar tv
 460   | isSkolemTyVar tv = return tv
 461         -- It might be a skolem type variable,
 462         -- for example from a user type signature
 463
 464   | otherwise   -- It's a meta-type-variable
 465   = do  { details <- readMetaTyVar tv
 466
 467         -- Create the new, frozen, regular type variable
 468         ; let final_kind = defaultKind (tyVarKind tv)
 469               final_tv   = mkTyVar (tyVarName tv) final_kind
 470
 471         -- Bind the meta tyvar to the new tyvar
 472         ; case details of
 473             Indirect ty -> WARN( True, ppr tv $$ ppr ty )
 474                            return ()
 475                 -- [Sept 04] I don't think this should happen
 476                 -- See note [Silly Type Synonym]
 477
 478             Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
 479
 480         -- Return the new tyvar
 481         ; return final_tv }
 482 \end{code}
 483
 484 [Silly Type Synonyms]
 485
 486 Consider this:
 487         type C u a = u  -- Note 'a' unused
 488
 489         foo :: (forall a. C u a -> C u a) -> u
 490         foo x = ...
 491
 492         bar :: Num u => u
 493         bar = foo (\t -> t + t)
 494
 495 * From the (\t -> t+t) we get type  {Num d} =>  d -> d
 496   where d is fresh.
 497
 498 * Now unify with type of foo's arg, and we get:
 499         {Num (C d a)} =>  C d a -> C d a
 500   where a is fresh.
 501
 502 * Now abstract over the 'a', but float out the Num (C d a) constraint
 503   because it does not 'really' mention a.  (see exactTyVarsOfType)
 504   The arg to foo becomes
 505         /\a -> \t -> t+t
 506
 507 * So we get a dict binding for Num (C d a), which is zonked to give
 508         a = ()
 509   [Note Sept 04: now that we are zonking quantified type variables
 510   on construction, the 'a' will be frozen as a regular tyvar on
 511   quantification, so the floated dict will still have type (C d a).
 512   Which renders this whole note moot; happily!]
 513
 514 * Then the /\a abstraction has a zonked 'a' in it.
 515
 516 All very silly.   I think its harmless to ignore the problem.  We'll end up with
 517 a /\a in the final result but all the occurrences of a will be zonked to ()
 518
 519
 520 %************************************************************************
 521 %*                                                                      *
 522 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
 523 %*                                                                      *
 524 %*              For internal use only!                                  *
 525 %*                                                                      *
 526 %************************************************************************
 527
 528 \begin{code}
 529 -- For unbound, mutable tyvars, zonkType uses the function given to it
 530 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 531 --      type variable and zonks the kind too
 532
 533 zonkType :: (TcTyVar -> TcM Type)       -- What to do with unbound mutable type variables
 534                                         -- see zonkTcType, and zonkTcTypeToType
 535          -> TcType
 536          -> TcM Type
 537 zonkType unbound_var_fn ty
 538   = go ty
 539   where
 540     go (NoteTy _ ty2)    = go ty2       -- Discard free-tyvar annotations
 541
 542     go (TyConApp tc tys) = mappM go tys `thenM` \ tys' ->
 543                            returnM (TyConApp tc tys')
 544
 545     go (PredTy p)        = go_pred p            `thenM` \ p' ->
 546                            returnM (PredTy p')
 547
 548     go (FunTy arg res)   = go arg               `thenM` \ arg' ->
 549                            go res               `thenM` \ res' ->
 550                            returnM (FunTy arg' res')
 551
 552     go (AppTy fun arg)   = go fun               `thenM` \ fun' ->
 553                            go arg               `thenM` \ arg' ->
 554                            returnM (mkAppTy fun' arg')
 555                 -- NB the mkAppTy; we might have instantiated a
 556                 -- type variable to a type constructor, so we need
 557                 -- to pull the TyConApp to the top.
 558
 559         -- The two interesting cases!
 560     go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
 561                        | otherwise       = return (TyVarTy tyvar)
 562                 -- Ordinary (non Tc) tyvars occur inside quantified types
 563
 564     go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
 565                              go ty              `thenM` \ ty' ->
 566                              returnM (ForAllTy tyvar ty')
 567
 568     go_pred (ClassP c tys) = mappM go tys       `thenM` \ tys' ->
 569                              returnM (ClassP c tys')
 570     go_pred (IParam n ty)  = go ty              `thenM` \ ty' ->
 571                              returnM (IParam n ty')
 572
 573 zonk_tc_tyvar :: (TcTyVar -> TcM Type)          -- What to do for an unbound mutable variable
 574               -> TcTyVar -> TcM TcType
 575 zonk_tc_tyvar unbound_var_fn tyvar
 576   | not (isMetaTyVar tyvar)     -- Skolems
 577   = returnM (TyVarTy tyvar)
 578
 579   | otherwise                   -- Mutables
 580   = do  { cts <- readMetaTyVar tyvar
 581         ; case cts of
 582             Flexi       -> unbound_var_fn tyvar    -- Unbound meta type variable
 583             Indirect ty -> zonkType unbound_var_fn ty  }
 584 \end{code}
 585
 586
 587
 588 %************************************************************************
 589 %*                                                                      *
 590                         Zonking kinds
 591 %*                                                                      *
 592 %************************************************************************
 593
 594 \begin{code}
 595 readKindVar  :: KindVar -> TcM (Maybe TcKind)
 596 writeKindVar :: KindVar -> TcKind -> TcM ()
 597 readKindVar  kv = readMutVar (kindVarRef kv)
 598 writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
 599
 600 -------------
 601 zonkTcKind :: TcKind -> TcM TcKind
 602 zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
 603                                 ; k2' <- zonkTcKind k2
 604                                 ; returnM (FunKind k1' k2') }
 605 zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv
 606                                ; case mb_kind of
 607                                     Nothing -> returnM k
 608                                     Just k  -> zonkTcKind k }
 609 zonkTcKind other_kind = returnM other_kind
 610
 611 -------------
 612 zonkTcKindToKind :: TcKind -> TcM Kind
 613 zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
 614                                       ; k2' <- zonkTcKindToKind k2
 615                                       ; returnM (FunKind k1' k2') }
 616
 617 zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv
 618                                    ; case mb_kind of
 619                                        Nothing -> return liftedTypeKind
 620                                        Just k  -> zonkTcKindToKind k }
 621
 622 zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind  -- An "Open" kind defaults to *
 623 zonkTcKindToKind other_kind   = returnM other_kind
 624 \end{code}
 625
 626 %************************************************************************
 627 %*                                                                      *
 628 \subsection{Checking a user type}
 629 %*                                                                      *
 630 %************************************************************************
 631
 632 When dealing with a user-written type, we first translate it from an HsType
 633 to a Type, performing kind checking, and then check various things that should
 634 be true about it.  We don't want to perform these checks at the same time
 635 as the initial translation because (a) they are unnecessary for interface-file
 636 types and (b) when checking a mutually recursive group of type and class decls,
 637 we can't "look" at the tycons/classes yet.  Also, the checks are are rather
 638 diverse, and used to really mess up the other code.
 639
 640 One thing we check for is 'rank'.
 641
 642         Rank 0:         monotypes (no foralls)
 643         Rank 1:         foralls at the front only, Rank 0 inside
 644         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
 645
 646         basic ::= tyvar | T basic ... basic
 647
 648         r2  ::= forall tvs. cxt => r2a
 649         r2a ::= r1 -> r2a | basic
 650         r1  ::= forall tvs. cxt => r0
 651         r0  ::= r0 -> r0 | basic
 652
 653 Another thing is to check that type synonyms are saturated.
 654 This might not necessarily show up in kind checking.
 655         type A i = i
 656         data T k = MkT (k Int)
 657         f :: T A        -- BAD!
 658
 659
 660 \begin{code}
 661 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 662 -- Checks that the type is valid for the given context
 663 checkValidType ctxt ty
 664   = traceTc (text "checkValidType" <+> ppr ty)  `thenM_`
 665     doptM Opt_GlasgowExts       `thenM` \ gla_exts ->
 666     let
 667         rank | gla_exts = Arbitrary
 668              | otherwise
 669              = case ctxt of     -- Haskell 98
 670                  GenPatCtxt     -> Rank 0
 671                  LamPatSigCtxt  -> Rank 0
 672                  BindPatSigCtxt -> Rank 0
 673                  DefaultDeclCtxt-> Rank 0
 674                  ResSigCtxt     -> Rank 0
 675                  TySynCtxt _    -> Rank 0
 676                  ExprSigCtxt    -> Rank 1
 677                  FunSigCtxt _   -> Rank 1
 678                  ConArgCtxt _   -> Rank 1       -- We are given the type of the entire
 679                                                 -- constructor, hence rank 1
 680                  ForSigCtxt _   -> Rank 1
 681                  RuleSigCtxt _  -> Rank 1
 682                  SpecInstCtxt   -> Rank 1
 683
 684         actual_kind = typeKind ty
 685
 686         kind_ok = case ctxt of
 687                         TySynCtxt _  -> True    -- Any kind will do
 688                         ResSigCtxt   -> isOpenTypeKind   actual_kind
 689                         ExprSigCtxt  -> isOpenTypeKind   actual_kind
 690                         GenPatCtxt   -> isLiftedTypeKind actual_kind
 691                         ForSigCtxt _ -> isLiftedTypeKind actual_kind
 692                         other        -> isArgTypeKind    actual_kind
 693
 694         ubx_tup | not gla_exts = UT_NotOk
 695                 | otherwise    = case ctxt of
 696                                    TySynCtxt _ -> UT_Ok
 697                                    ExprSigCtxt -> UT_Ok
 698                                    other       -> UT_NotOk
 699                 -- Unboxed tuples ok in function results,
 700                 -- but for type synonyms we allow them even at
 701                 -- top level
 702     in
 703         -- Check that the thing has kind Type, and is lifted if necessary
 704     checkTc kind_ok (kindErr actual_kind)       `thenM_`
 705
 706         -- Check the internal validity of the type itself
 707     check_poly_type rank ubx_tup ty             `thenM_`
 708
 709     traceTc (text "checkValidType done" <+> ppr ty)
 710 \end{code}
 711
 712
 713 \begin{code}
 714 data Rank = Rank Int | Arbitrary
 715
 716 decRank :: Rank -> Rank
 717 decRank Arbitrary = Arbitrary
 718 decRank (Rank n)  = Rank (n-1)
 719
 720 ----------------------------------------
 721 data UbxTupFlag = UT_Ok | UT_NotOk
 722         -- The "Ok" version means "ok if -fglasgow-exts is on"
 723
 724 ----------------------------------------
 725 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 726 check_poly_type (Rank 0) ubx_tup ty
 727   = check_tau_type (Rank 0) ubx_tup ty
 728
 729 check_poly_type rank ubx_tup ty
 730   = let
 731         (tvs, theta, tau) = tcSplitSigmaTy ty
 732     in
 733     check_valid_theta SigmaCtxt theta           `thenM_`
 734     check_tau_type (decRank rank) ubx_tup tau   `thenM_`
 735     checkFreeness tvs theta                     `thenM_`
 736     checkAmbiguity tvs theta (tyVarsOfType tau)
 737
 738 ----------------------------------------
 739 check_arg_type :: Type -> TcM ()
 740 -- The sort of type that can instantiate a type variable,
 741 -- or be the argument of a type constructor.
 742 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
 743 -- Other unboxed types are very occasionally allowed as type
 744 -- arguments depending on the kind of the type constructor
 745 --
 746 -- For example, we want to reject things like:
 747 --
 748 --      instance Ord a => Ord (forall s. T s a)
 749 -- and
 750 --      g :: T s (forall b.b)
 751 --
 752 -- NB: unboxed tuples can have polymorphic or unboxed args.
 753 --     This happens in the workers for functions returning
 754 --     product types with polymorphic components.
 755 --     But not in user code.
 756 -- Anyway, they are dealt with by a special case in check_tau_type
 757
 758 check_arg_type ty
 759   = check_poly_type Arbitrary UT_NotOk ty       `thenM_`
 760     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 761
 762 ----------------------------------------
 763 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 764 -- Rank is allowed rank for function args
 765 -- No foralls otherwise
 766
 767 check_tau_type rank ubx_tup ty@(ForAllTy _ _)       = failWithTc (forAllTyErr ty)
 768 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
 769         -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
 770
 771 -- Naked PredTys don't usually show up, but they can as a result of
 772 --      {-# SPECIALISE instance Ord Char #-}
 773 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
 774 -- are handled, but the quick thing is just to permit PredTys here.
 775 check_tau_type rank ubx_tup (PredTy sty) = getDOpts             `thenM` \ dflags ->
 776                                            check_source_ty dflags TypeCtxt sty
 777
 778 check_tau_type rank ubx_tup (TyVarTy _)       = returnM ()
 779 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
 780   = check_poly_type rank UT_NotOk arg_ty        `thenM_`
 781     check_poly_type rank UT_Ok    res_ty
 782
 783 check_tau_type rank ubx_tup (AppTy ty1 ty2)
 784   = check_arg_type ty1 `thenM_` check_arg_type ty2
 785
 786 check_tau_type rank ubx_tup (NoteTy other_note ty)
 787   = check_tau_type rank ubx_tup ty
 788
 789 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
 790   | isSynTyCon tc
 791   = do  {       -- It's OK to have an *over-applied* type synonym
 792                 --      data Tree a b = ...
 793                 --      type Foo a = Tree [a]
 794                 --      f :: Foo a b -> ...
 795         ; case tcView ty of
 796              Just ty' -> check_tau_type rank ubx_tup ty'        -- Check expansion
 797              Nothing  -> failWithTc arity_msg
 798
 799         ; gla_exts <- doptM Opt_GlasgowExts
 800         ; if gla_exts then
 801         -- If -fglasgow-exts then don't check the type arguments
 802         -- This allows us to instantiate a synonym defn with a
 803         -- for-all type, or with a partially-applied type synonym.
 804         --      e.g.   type T a b = a
 805         --             type S m   = m ()
 806         --             f :: S (T Int)
 807         -- Here, T is partially applied, so it's illegal in H98.
 808         -- But if you expand S first, then T we get just
 809         --             f :: Int
 810         -- which is fine.
 811                 returnM ()
 812           else
 813                 -- For H98, do check the type args
 814                 mappM_ check_arg_type tys
 815         }
 816
 817   | isUnboxedTupleTyCon tc
 818   = doptM Opt_GlasgowExts                       `thenM` \ gla_exts ->
 819     checkTc (ubx_tup_ok gla_exts) ubx_tup_msg   `thenM_`
 820     mappM_ (check_tau_type (Rank 0) UT_Ok) tys
 821                 -- Args are allowed to be unlifted, or
 822                 -- more unboxed tuples, so can't use check_arg_ty
 823
 824   | otherwise
 825   = mappM_ check_arg_type tys
 826
 827   where
 828     ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
 829
 830     n_args    = length tys
 831     tc_arity  = tyConArity tc
 832
 833     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
 834     ubx_tup_msg = ubxArgTyErr ty
 835
 836 ----------------------------------------
 837 forAllTyErr     ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
 838 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
 839 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
 840 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 841 \end{code}
 842
 843
 844
 845 %************************************************************************
 846 %*                                                                      *
 847 \subsection{Checking a theta or source type}
 848 %*                                                                      *
 849 %************************************************************************
 850
 851 \begin{code}
 852 -- Enumerate the contexts in which a "source type", <S>, can occur
 853 --      Eq a
 854 -- or   ?x::Int
 855 -- or   r <: {x::Int}
 856 -- or   (N a) where N is a newtype
 857
 858 data SourceTyCtxt
 859   = ClassSCCtxt Name    -- Superclasses of clas
 860                         --      class <S> => C a where ...
 861   | SigmaCtxt           -- Theta part of a normal for-all type
 862                         --      f :: <S> => a -> a
 863   | DataTyCtxt Name     -- Theta part of a data decl
 864                         --      data <S> => T a = MkT a
 865   | TypeCtxt            -- Source type in an ordinary type
 866                         --      f :: N a -> N a
 867   | InstThetaCtxt       -- Context of an instance decl
 868                         --      instance <S> => C [a] where ...
 869
 870 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
 871 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
 872 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
 873 pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context 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                      InstThetaCtxt -> parens undecidableMsg
 910                      other         -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 911
 912 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
 913         -- Implicit parameters only allows in type
 914         -- signatures; not in instance decls, superclasses etc
 915         -- The reason for not allowing implicit params in instances is a bit subtle
 916         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
 917         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
 918         -- discharge all the potential usas of the ?x in e.   For example, a
 919         -- constraint Foo [Int] might come out of e,and applying the
 920         -- instance decl would show up two uses of ?x.
 921
 922 -- Catch-all
 923 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 924
 925 -------------------------
 926 check_class_pred_tys dflags ctxt tys
 927   = case ctxt of
 928         TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
 929         InstThetaCtxt -> undecidable_ok || distinct_tyvars tys
 930         other         -> gla_exts       || all tyvar_head tys
 931   where
 932     undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
 933     gla_exts       = dopt Opt_GlasgowExts dflags
 934
 935 -------------------------
 936 distinct_tyvars tys     -- Check that the types are all distinct type variables
 937   = all tcIsTyVarTy tys && null (findDupsEq tcEqType tys)
 938
 939 -------------------------
 940 tyvar_head ty                   -- Haskell 98 allows predicates of form
 941   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
 942   | otherwise                   -- where a is a type variable
 943   = case tcSplitAppTy_maybe ty of
 944         Just (ty, _) -> tyvar_head ty
 945         Nothing      -> False
 946 \end{code}
 947
 948 Check for ambiguity
 949 ~~~~~~~~~~~~~~~~~~~
 950           forall V. P => tau
 951 is ambiguous if P contains generic variables
 952 (i.e. one of the Vs) that are not mentioned in tau
 953
 954 However, we need to take account of functional dependencies
 955 when we speak of 'mentioned in tau'.  Example:
 956         class C a b | a -> b where ...
 957 Then the type
 958         forall x y. (C x y) => x
 959 is not ambiguous because x is mentioned and x determines y
 960
 961 NB; the ambiguity check is only used for *user* types, not for types
 962 coming from inteface files.  The latter can legitimately have
 963 ambiguous types. Example
 964
 965    class S a where s :: a -> (Int,Int)
 966    instance S Char where s _ = (1,1)
 967    f:: S a => [a] -> Int -> (Int,Int)
 968    f (_::[a]) x = (a*x,b)
 969         where (a,b) = s (undefined::a)
 970
 971 Here the worker for f gets the type
 972         fw :: forall a. S a => Int -> (# Int, Int #)
 973
 974 If the list of tv_names is empty, we have a monotype, and then we
 975 don't need to check for ambiguity either, because the test can't fail
 976 (see is_ambig).
 977
 978 \begin{code}
 979 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
 980 checkAmbiguity forall_tyvars theta tau_tyvars
 981   = mappM_ complain (filter is_ambig theta)
 982   where
 983     complain pred     = addErrTc (ambigErr pred)
 984     extended_tau_vars = grow theta tau_tyvars
 985
 986         -- Only a *class* predicate can give rise to ambiguity
 987         -- An *implicit parameter* cannot.  For example:
 988         --      foo :: (?x :: [a]) => Int
 989         --      foo = length ?x
 990         -- is fine.  The call site will suppply a particular 'x'
 991     is_ambig pred     = isClassPred  pred &&
 992                         any ambig_var (varSetElems (tyVarsOfPred pred))
 993
 994     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
 995                         not (ct_var `elemVarSet` extended_tau_vars)
 996
 997 ambigErr pred
 998   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
 999          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1000                  ptext SLIT("must be reachable from the type after the '=>'"))]
1001 \end{code}
1002
1003 In addition, GHC insists that at least one type variable
1004 in each constraint is in V.  So we disallow a type like
1005         forall a. Eq b => b -> b
1006 even in a scope where b is in scope.
1007
1008 \begin{code}
1009 checkFreeness forall_tyvars theta
1010   = mappM_ complain (filter is_free theta)
1011   where
1012     is_free pred     =  not (isIPPred pred)
1013                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1014     bound_var ct_var = ct_var `elem` forall_tyvars
1015     complain pred    = addErrTc (freeErr pred)
1016
1017 freeErr pred
1018   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1019                    ptext SLIT("are already in scope"),
1020          nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1021     ]
1022 \end{code}
1023
1024 \begin{code}
1025 checkThetaCtxt ctxt theta
1026   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1027           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1028
1029 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1030 predTyVarErr pred  = sep [ptext SLIT("Non-type variables, or repeated type variables,"),
1031                           nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1032 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1033
1034 arityErr kind name n m
1035   = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1036            n_arguments <> comma, text "but has been given", int m]
1037     where
1038         n_arguments | n == 0 = ptext SLIT("no arguments")
1039                     | n == 1 = ptext SLIT("1 argument")
1040                     | True   = hsep [int n, ptext SLIT("arguments")]
1041 \end{code}
1042
1043
1044 %************************************************************************
1045 %*                                                                      *
1046 \subsection{Checking for a decent instance head type}
1047 %*                                                                      *
1048 %************************************************************************
1049
1050 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1051 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1052
1053 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1054 flag is on, or (2)~the instance is imported (they must have been
1055 compiled elsewhere). In these cases, we let them go through anyway.
1056
1057 We can also have instances for functions: @instance Foo (a -> b) ...@.
1058
1059 \begin{code}
1060 checkValidInstHead :: Type -> TcM (Class, [TcType])
1061
1062 checkValidInstHead ty   -- Should be a source type
1063   = case tcSplitPredTy_maybe ty of {
1064         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1065         Just pred ->
1066
1067     case getClassPredTys_maybe pred of {
1068         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1069         Just (clas,tys) ->
1070
1071     getDOpts                                    `thenM` \ dflags ->
1072     mappM_ check_arg_type tys                   `thenM_`
1073     check_inst_head dflags clas tys             `thenM_`
1074     returnM (clas, tys)
1075     }}
1076
1077 check_inst_head dflags clas tys
1078         -- If GlasgowExts then check at least one isn't a type variable
1079   | dopt Opt_GlasgowExts dflags
1080   = check_tyvars dflags clas tys
1081
1082         -- WITH HASKELL 98, MUST HAVE C (T a b c)
1083   | isSingleton tys,
1084     tcValidInstHeadTy first_ty
1085   = returnM ()
1086
1087   | otherwise
1088   = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1089
1090   where
1091     (first_ty : _) = tys
1092
1093     head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1094                              text "where T is not a synonym, and a,b,c are distinct type variables")
1095
1096 check_tyvars dflags clas tys
1097         -- Check that at least one isn't a type variable
1098         -- unless -fallow-undecideable-instances
1099   | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1100   | not (all tcIsTyVarTy tys)                 = returnM ()
1101   | otherwise                                 = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1102   where
1103     msg =  parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1104                    $$ undecidableMsg)
1105
1106 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1107 \end{code}
1108
1109 \begin{code}
1110 instTypeErr pp_ty msg
1111   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1112          nest 4 msg]
1113 \end{code}