compiler/typecheck/TcMType.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   4 %
   5
   6 Monadic type operations
   7
   8 This module contains monadic operations over types that contain
   9 mutable type variables
  10
  11 \begin{code}
  12 module TcMType (
  13   TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
  14
  15   --------------------------------
  16   -- Creating new mutable type variables
  17   newFlexiTyVar,
  18   newFlexiTyVarTy,              -- Kind -> TcM TcType
  19   newFlexiTyVarTys,             -- Int -> Kind -> TcM [TcType]
  20   newKindVar, newKindVars,
  21   mkTcTyVarName,
  22
  23   newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
  24   isFilledMetaTyVar, isFlexiMetaTyVar,
  25
  26   --------------------------------
  27   -- Creating new evidence variables
  28   newEvVar, newCoVar, newEvVars,
  29   newIP, newDict, newSilentGiven, isSilentEvVar,
  30
  31   newWantedEvVar, newWantedEvVars,
  32   newTcEvBinds, addTcEvBind,
  33
  34   --------------------------------
  35   -- Instantiation
  36   tcInstTyVar, tcInstTyVars, tcInstSigTyVars,
  37   tcInstType, instMetaTyVar,
  38   tcInstSkolTyVars, tcInstSuperSkolTyVars, tcInstSkolTyVar, tcInstSkolType,
  39   tcSkolDFunType, tcSuperSkolTyVars,
  40
  41   --------------------------------
  42   -- Checking type validity
  43   Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
  44   SourceTyCtxt(..), checkValidTheta,
  45   checkValidInstHead, checkValidInstance,
  46   checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
  47   arityErr,
  48   growPredTyVars, growThetaTyVars, validDerivPred,
  49
  50   --------------------------------
  51   -- Zonking
  52   zonkType, mkZonkTcTyVar, zonkTcPredType,
  53   zonkTcTypeCarefully, skolemiseUnboundMetaTyVar,
  54   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
  55   zonkQuantifiedTyVar, zonkQuantifiedTyVars,
  56   zonkTcType, zonkTcTypes, zonkTcThetaType,
  57   zonkTcKindToKind, zonkTcKind,
  58   zonkImplication, zonkEvVar, zonkWantedEvVar, zonkFlavoredEvVar,
  59   zonkWC, zonkWantedEvVars,
  60   zonkTcTypeAndSubst,
  61   tcGetGlobalTyVars,
  62
  63
  64   readKindVar, writeKindVar
  65   ) where
  66
  67 #include "HsVersions.h"
  68
  69 -- friends:
  70 import TypeRep
  71 import TcType
  72 import Type
  73 import Class
  74 import TyCon
  75 import Var
  76
  77 -- others:
  78 import HsSyn            -- HsType
  79 import TcRnMonad        -- TcType, amongst others
  80 import Id
  81 import FunDeps
  82 import Name
  83 import VarSet
  84 import ErrUtils
  85 import DynFlags
  86 import Util
  87 import Maybes
  88 import ListSetOps
  89 import BasicTypes
  90 import SrcLoc
  91 import Outputable
  92 import FastString
  93 import Unique( Unique )
  94 import Bag
  95
  96 import Control.Monad
  97 import Data.List        ( (\\) )
  98 \end{code}
  99
 100
 101 %************************************************************************
 102 %*                                                                      *
 103         Kind variables
 104 %*                                                                      *
 105 %************************************************************************
 106
 107 \begin{code}
 108 newKindVar :: TcM TcKind
 109 newKindVar = do { uniq <- newUnique
 110                 ; ref <- newMutVar Flexi
 111                 ; return (mkTyVarTy (mkKindVar uniq ref)) }
 112
 113 newKindVars :: Int -> TcM [TcKind]
 114 newKindVars n = mapM (\ _ -> newKindVar) (nOfThem n ())
 115 \end{code}
 116
 117
 118 %************************************************************************
 119 %*                                                                      *
 120      Evidence variables; range over constraints we can abstract over
 121 %*                                                                      *
 122 %************************************************************************
 123
 124 \begin{code}
 125 newEvVars :: TcThetaType -> TcM [EvVar]
 126 newEvVars theta = mapM newEvVar theta
 127
 128 newWantedEvVar :: TcPredType -> TcM EvVar
 129 newWantedEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
 130 newWantedEvVar (ClassP cls tys) = newDict cls tys
 131 newWantedEvVar (IParam ip ty)   = newIP ip ty
 132
 133 newWantedEvVars :: TcThetaType -> TcM [EvVar]
 134 newWantedEvVars theta = mapM newWantedEvVar theta
 135
 136 --------------
 137 newEvVar :: TcPredType -> TcM EvVar
 138 -- Creates new *rigid* variables for predicates
 139 newEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
 140 newEvVar (ClassP cls tys) = newDict  cls tys
 141 newEvVar (IParam ip ty)   = newIP    ip ty
 142
 143 newCoVar :: TcType -> TcType -> TcM CoVar
 144 newCoVar ty1 ty2
 145   = do { name <- newName (mkVarOccFS (fsLit "co"))
 146        ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
 147
 148 newIP :: IPName Name -> TcType -> TcM IpId
 149 newIP ip ty
 150   = do  { name <- newName (getOccName (ipNameName ip))
 151         ; return (mkLocalId name (mkPredTy (IParam ip ty))) }
 152
 153 newDict :: Class -> [TcType] -> TcM DictId
 154 newDict cls tys
 155   = do { name <- newName (mkDictOcc (getOccName cls))
 156        ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
 157
 158 newName :: OccName -> TcM Name
 159 newName occ
 160   = do { uniq <- newUnique
 161        ; loc  <- getSrcSpanM
 162        ; return (mkInternalName uniq occ loc) }
 163
 164 -----------------
 165 newSilentGiven :: PredType -> TcM EvVar
 166 -- Make a dictionary for a "silent" given dictionary
 167 -- Behaves just like any EvVar except that it responds True to isSilentDict
 168 -- This is used only to suppress confusing error reports
 169 newSilentGiven (ClassP cls tys)
 170   = do { uniq <- newUnique
 171        ; let name = mkSystemName uniq (mkDictOcc (getOccName cls))
 172        ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
 173 newSilentGiven (EqPred ty1 ty2)
 174   = do { uniq <- newUnique
 175        ; let name = mkSystemName uniq (mkTyVarOccFS (fsLit "co"))
 176        ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
 177 newSilentGiven pred@(IParam {})
 178   = pprPanic "newSilentDict" (ppr pred) -- Implicit parameters rejected earlier
 179
 180 isSilentEvVar :: EvVar -> Bool
 181 isSilentEvVar v = isSystemName (Var.varName v)
 182   -- Notice that all *other* evidence variables get Internal Names
 183 \end{code}
 184
 185
 186 %************************************************************************
 187 %*                                                                      *
 188         SkolemTvs (immutable)
 189 %*                                                                      *
 190 %************************************************************************
 191
 192 \begin{code}
 193 tcInstType :: ([TyVar] -> TcM [TcTyVar])                -- How to instantiate the type variables
 194            -> TcType                                    -- Type to instantiate
 195            -> TcM ([TcTyVar], TcThetaType, TcType)      -- Result
 196                 -- (type vars (excl coercion vars), preds (incl equalities), rho)
 197 tcInstType inst_tyvars ty
 198   = case tcSplitForAllTys ty of
 199         ([],     rho) -> let    -- There may be overloading despite no type variables;
 200                                 --      (?x :: Int) => Int -> Int
 201                            (theta, tau) = tcSplitPhiTy rho
 202                          in
 203                          return ([], theta, tau)
 204
 205         (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
 206
 207                             ; let  tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
 208                                 -- Either the tyvars are freshly made, by inst_tyvars,
 209                                 -- or any nested foralls have different binders.
 210                                 -- Either way, zipTopTvSubst is ok
 211
 212                             ; let  (theta, tau) = tcSplitPhiTy (substTy tenv rho)
 213                             ; return (tyvars', theta, tau) }
 214
 215 tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
 216 -- Instantiate a type signature with skolem constants, but
 217 -- do *not* give them fresh names, because we want the name to
 218 -- be in the type environment: it is lexically scoped.
 219 tcSkolDFunType ty = tcInstType (\tvs -> return (tcSuperSkolTyVars tvs)) ty
 220
 221 tcSuperSkolTyVars :: [TyVar] -> [TcTyVar]
 222 -- Make skolem constants, but do *not* give them new names, as above
 223 -- Moreover, make them "super skolems"; see comments with superSkolemTv
 224 tcSuperSkolTyVars tyvars
 225   = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) superSkolemTv
 226     | tv <- tyvars ]
 227
 228 tcInstSkolTyVar :: Bool -> TyVar -> TcM TcTyVar
 229 -- Instantiate the tyvar, using
 230 --      * the occ-name and kind of the supplied tyvar,
 231 --      * the unique from the monad,
 232 --      * the location either from the tyvar (skol_info = SigSkol)
 233 --                     or from the monad (otherwise)
 234 tcInstSkolTyVar overlappable tyvar
 235   = do  { uniq <- newUnique
 236         ; loc <-  getSrcSpanM
 237         ; let new_name = mkInternalName uniq occ loc
 238         ; return (mkTcTyVar new_name kind (SkolemTv overlappable)) }
 239   where
 240     old_name = tyVarName tyvar
 241     occ      = nameOccName old_name
 242     kind     = tyVarKind tyvar
 243
 244 tcInstSkolTyVars :: [TyVar] -> TcM [TcTyVar]
 245 tcInstSkolTyVars tyvars = mapM (tcInstSkolTyVar False) tyvars
 246
 247 tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar]
 248 tcInstSuperSkolTyVars tyvars = mapM (tcInstSkolTyVar True) tyvars
 249
 250 tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
 251 -- Instantiate a type with fresh skolem constants
 252 -- Binding location comes from the monad
 253 tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
 254
 255 tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
 256 -- Make meta SigTv type variables for patten-bound scoped type varaibles
 257 -- We use SigTvs for them, so that they can't unify with arbitrary types
 258 tcInstSigTyVars = mapM (\tv -> instMetaTyVar (SigTv (tyVarName tv)) tv)
 259                 -- ToDo: the "function binding site is bogus
 260 \end{code}
 261
 262
 263 %************************************************************************
 264 %*                                                                      *
 265         MetaTvs (meta type variables; mutable)
 266 %*                                                                      *
 267 %************************************************************************
 268
 269 \begin{code}
 270 newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
 271 -- Make a new meta tyvar out of thin air
 272 newMetaTyVar meta_info kind
 273   = do  { uniq <- newMetaUnique
 274         ; ref <- newMutVar Flexi
 275         ; let name = mkTcTyVarName uniq s
 276               s = case meta_info of
 277                         TauTv   -> fsLit "t"
 278                         TcsTv   -> fsLit "u"
 279                         SigTv _ -> fsLit "a"
 280         ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
 281
 282 mkTcTyVarName :: Unique -> FastString -> Name
 283 -- Make sure that fresh TcTyVar names finish with a digit
 284 -- leaving the un-cluttered names free for user names
 285 mkTcTyVarName uniq str = mkSysTvName uniq str
 286
 287 instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar
 288 -- Make a new meta tyvar whose Name and Kind
 289 -- come from an existing TyVar
 290 instMetaTyVar meta_info tyvar
 291   = do  { uniq <- newMetaUnique
 292         ; ref <- newMutVar Flexi
 293         ; let name = mkSystemName uniq (getOccName tyvar)
 294               kind = tyVarKind tyvar
 295         ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
 296
 297 readMetaTyVar :: TyVar -> TcM MetaDetails
 298 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
 299                       readMutVar (metaTvRef tyvar)
 300
 301 isFilledMetaTyVar :: TyVar -> TcM Bool
 302 -- True of a filled-in (Indirect) meta type variable
 303 isFilledMetaTyVar tv
 304   | not (isTcTyVar tv) = return False
 305   | MetaTv _ ref <- tcTyVarDetails tv
 306   = do  { details <- readMutVar ref
 307         ; return (isIndirect details) }
 308   | otherwise = return False
 309
 310 isFlexiMetaTyVar :: TyVar -> TcM Bool
 311 -- True of a un-filled-in (Flexi) meta type variable
 312 isFlexiMetaTyVar tv
 313   | not (isTcTyVar tv) = return False
 314   | MetaTv _ ref <- tcTyVarDetails tv
 315   = do  { details <- readMutVar ref
 316         ; return (isFlexi details) }
 317   | otherwise = return False
 318
 319 --------------------
 320 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
 321 -- Write into a currently-empty MetaTyVar
 322
 323 writeMetaTyVar tyvar ty
 324   | not debugIsOn
 325   = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
 326
 327 -- Everything from here on only happens if DEBUG is on
 328   | not (isTcTyVar tyvar)
 329   = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
 330     return ()
 331
 332   | MetaTv _ ref <- tcTyVarDetails tyvar
 333   = writeMetaTyVarRef tyvar ref ty
 334
 335   | otherwise
 336   = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
 337     return ()
 338
 339 --------------------
 340 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
 341 -- Here the tyvar is for error checking only;
 342 -- the ref cell must be for the same tyvar
 343 writeMetaTyVarRef tyvar ref ty
 344   | not debugIsOn
 345   = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
 346        ; writeMutVar ref (Indirect ty) }
 347
 348 -- Everything from here on only happens if DEBUG is on
 349   | not (isPredTy tv_kind)   -- Don't check kinds for updates to coercion variables
 350   , not (ty_kind `isSubKind` tv_kind)
 351   = WARN( True, hang (text "Ill-kinded update to meta tyvar")
 352                    2 (ppr tyvar $$ ppr tv_kind $$ ppr ty $$ ppr ty_kind) )
 353     return ()
 354
 355   | otherwise
 356   = do { meta_details <- readMutVar ref;
 357        ; ASSERT2( isFlexi meta_details,
 358                   hang (text "Double update of meta tyvar")
 359                    2 (ppr tyvar $$ ppr meta_details) )
 360
 361          traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
 362        ; writeMutVar ref (Indirect ty) }
 363   where
 364     tv_kind = tyVarKind tyvar
 365     ty_kind = typeKind ty
 366 \end{code}
 367
 368
 369 %************************************************************************
 370 %*                                                                      *
 371         MetaTvs: TauTvs
 372 %*                                                                      *
 373 %************************************************************************
 374
 375 \begin{code}
 376 newFlexiTyVar :: Kind -> TcM TcTyVar
 377 newFlexiTyVar kind = newMetaTyVar TauTv kind
 378
 379 newFlexiTyVarTy  :: Kind -> TcM TcType
 380 newFlexiTyVarTy kind = do
 381     tc_tyvar <- newFlexiTyVar kind
 382     return (TyVarTy tc_tyvar)
 383
 384 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
 385 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
 386
 387 tcInstTyVar :: TyVar -> TcM TcTyVar
 388 -- Instantiate with a META type variable
 389 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
 390
 391 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
 392 -- Instantiate with META type variables
 393 tcInstTyVars tyvars
 394   = do  { tc_tvs <- mapM tcInstTyVar tyvars
 395         ; let tys = mkTyVarTys tc_tvs
 396         ; return (tc_tvs, tys, zipTopTvSubst tyvars tys) }
 397                 -- Since the tyvars are freshly made,
 398                 -- they cannot possibly be captured by
 399                 -- any existing for-alls.  Hence zipTopTvSubst
 400 \end{code}
 401
 402
 403 %************************************************************************
 404 %*                                                                      *
 405         MetaTvs: SigTvs
 406 %*                                                                      *
 407 %************************************************************************
 408
 409 \begin{code}
 410 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
 411 zonkSigTyVar sig_tv
 412   | isSkolemTyVar sig_tv
 413   = return sig_tv       -- Happens in the call in TcBinds.checkDistinctTyVars
 414   | otherwise
 415   = ASSERT( isSigTyVar sig_tv )
 416     do { ty <- zonkTcTyVar sig_tv
 417        ; return (tcGetTyVar "zonkSigTyVar" ty) }
 418         -- 'ty' is bound to be a type variable, because SigTvs
 419         -- can only be unified with type variables
 420 \end{code}
 421
 422
 423
 424 %************************************************************************
 425 %*                                                                      *
 426 \subsection{Zonking -- the exernal interfaces}
 427 %*                                                                      *
 428 %************************************************************************
 429
 430 @tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
 431 To improve subsequent calls to the same function it writes the zonked set back into
 432 the environment.
 433
 434 \begin{code}
 435 tcGetGlobalTyVars :: TcM TcTyVarSet
 436 tcGetGlobalTyVars
 437   = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
 438        ; gbl_tvs  <- readMutVar gtv_var
 439        ; gbl_tvs' <- zonkTcTyVarsAndFV gbl_tvs
 440        ; writeMutVar gtv_var gbl_tvs'
 441        ; return gbl_tvs' }
 442 \end{code}
 443
 444 -----------------  Type variables
 445
 446 \begin{code}
 447 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
 448 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
 449
 450 zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet
 451 zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars)
 452
 453 -----------------  Types
 454 zonkTcTypeCarefully :: TcType -> TcM TcType
 455 -- Do not zonk type variables free in the environment
 456 zonkTcTypeCarefully ty
 457   = do { env_tvs <- tcGetGlobalTyVars
 458        ; zonkType (zonk_tv env_tvs) ty }
 459   where
 460     zonk_tv env_tvs tv
 461       | tv `elemVarSet` env_tvs
 462       = return (TyVarTy tv)
 463       | otherwise
 464       = ASSERT( isTcTyVar tv )
 465         case tcTyVarDetails tv of
 466           SkolemTv {}   -> return (TyVarTy tv)
 467           RuntimeUnk {} -> return (TyVarTy tv)
 468           FlatSkol ty   -> zonkType (zonk_tv env_tvs) ty
 469           MetaTv _ ref  -> do { cts <- readMutVar ref
 470                               ; case cts of
 471                                    Flexi       -> return (TyVarTy tv)
 472                                    Indirect ty -> zonkType (zonk_tv env_tvs) ty }
 473
 474 zonkTcType :: TcType -> TcM TcType
 475 -- Simply look through all Flexis
 476 zonkTcType ty = zonkType zonkTcTyVar ty
 477
 478 zonkTcTyVar :: TcTyVar -> TcM TcType
 479 -- Simply look through all Flexis
 480 zonkTcTyVar tv
 481   = ASSERT2( isTcTyVar tv, ppr tv )
 482     case tcTyVarDetails tv of
 483       SkolemTv {}   -> return (TyVarTy tv)
 484       RuntimeUnk {} -> return (TyVarTy tv)
 485       FlatSkol ty   -> zonkTcType ty
 486       MetaTv _ ref  -> do { cts <- readMutVar ref
 487                           ; case cts of
 488                                Flexi       -> return (TyVarTy tv)
 489                                Indirect ty -> zonkTcType ty }
 490
 491 zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
 492 -- Zonk, and simultaneously apply a non-necessarily-idempotent substitution
 493 zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
 494   where
 495     zonk_tv tv
 496       = case tcTyVarDetails tv of
 497           SkolemTv {}   -> return (TyVarTy tv)
 498           RuntimeUnk {} -> return (TyVarTy tv)
 499           FlatSkol ty   -> zonkType zonk_tv ty
 500           MetaTv _ ref  -> do { cts <- readMutVar ref
 501                               ; case cts of
 502                                    Flexi       -> zonk_flexi tv
 503                                    Indirect ty -> zonkType zonk_tv ty }
 504     zonk_flexi tv
 505       = case lookupTyVar subst tv of
 506           Just ty -> zonkType zonk_tv ty
 507           Nothing -> return (TyVarTy tv)
 508
 509 zonkTcTypes :: [TcType] -> TcM [TcType]
 510 zonkTcTypes tys = mapM zonkTcType tys
 511
 512 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
 513 zonkTcThetaType theta = mapM zonkTcPredType theta
 514
 515 zonkTcPredType :: TcPredType -> TcM TcPredType
 516 zonkTcPredType (ClassP c ts)  = ClassP c <$> zonkTcTypes ts
 517 zonkTcPredType (IParam n t)   = IParam n <$> zonkTcType t
 518 zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2
 519 \end{code}
 520
 521 -------------------  These ...ToType, ...ToKind versions
 522                      are used at the end of type checking
 523
 524 \begin{code}
 525 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
 526 zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
 527
 528 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
 529 -- The quantified type variables often include meta type variables
 530 -- we want to freeze them into ordinary type variables, and
 531 -- default their kind (e.g. from OpenTypeKind to TypeKind)
 532 --                      -- see notes with Kind.defaultKind
 533 -- The meta tyvar is updated to point to the new skolem TyVar.  Now any
 534 -- bound occurences of the original type variable will get zonked to
 535 -- the immutable version.
 536 --
 537 -- We leave skolem TyVars alone; they are immutable.
 538 zonkQuantifiedTyVar tv
 539   = ASSERT2( isTcTyVar tv, ppr tv )
 540     case tcTyVarDetails tv of
 541       SkolemTv {} -> WARN( True, ppr tv )  -- Dec10: Can this really happen?
 542                      do { kind <- zonkTcType (tyVarKind tv)
 543                         ; return $ setTyVarKind tv kind }
 544         -- It might be a skolem type variable,
 545         -- for example from a user type signature
 546
 547       MetaTv _ _ref ->
 548 #ifdef DEBUG
 549                         -- [Sept 04] Check for non-empty.
 550                         -- See note [Silly Type Synonym]
 551                       (readMutVar _ref >>= \cts ->
 552                        case cts of
 553                              Flexi -> return ()
 554                              Indirect ty -> WARN( True, ppr tv $$ ppr ty )
 555                                             return ()) >>
 556 #endif
 557                       skolemiseUnboundMetaTyVar tv vanillaSkolemTv
 558       _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
 559
 560 skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
 561 -- We have a Meta tyvar with a ref-cell inside it
 562 -- Skolemise it, including giving it a new Name, so that
 563 --   we are totally out of Meta-tyvar-land
 564 -- We create a skolem TyVar, not a regular TyVar
 565 --   See Note [Zonking to Skolem]
 566 skolemiseUnboundMetaTyVar tv details
 567   = ASSERT2( isMetaTyVar tv, ppr tv )
 568     do  { span <- getSrcSpanM    -- Get the location from "here"
 569                                  -- ie where we are generalising
 570         ; uniq <- newUnique      -- Remove it from TcMetaTyVar unique land
 571         ; let final_kind = defaultKind (tyVarKind tv)
 572               final_name = mkInternalName uniq (getOccName tv) span
 573               final_tv   = mkTcTyVar final_name final_kind details
 574         ; writeMetaTyVar tv (mkTyVarTy final_tv)
 575         ; return final_tv }
 576 \end{code}
 577
 578 \begin{code}
 579 zonkImplication :: Implication -> TcM Implication
 580 zonkImplication implic@(Implic { ic_given = given
 581                                , ic_wanted = wanted
 582                                , ic_loc = loc })
 583   = do {    -- No need to zonk the skolems
 584        ; given'  <- mapM zonkEvVar given
 585        ; loc'    <- zonkGivenLoc loc
 586        ; wanted' <- zonkWC wanted
 587        ; return (implic { ic_given = given'
 588                         , ic_wanted = wanted'
 589                         , ic_loc = loc' }) }
 590
 591 zonkEvVar :: EvVar -> TcM EvVar
 592 zonkEvVar var = do { ty' <- zonkTcType (varType var)
 593                    ; return (setVarType var ty') }
 594
 595 zonkFlavoredEvVar :: FlavoredEvVar -> TcM FlavoredEvVar
 596 zonkFlavoredEvVar (EvVarX ev fl)
 597   = do { ev' <- zonkEvVar ev
 598        ; fl' <- zonkFlavor fl
 599        ; return (EvVarX ev' fl') }
 600
 601 zonkWC :: WantedConstraints -> TcM WantedConstraints
 602 zonkWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
 603   = do { flat'   <- zonkWantedEvVars flat
 604        ; implic' <- mapBagM zonkImplication implic
 605        ; insol'  <- mapBagM zonkFlavoredEvVar insol
 606        ; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) }
 607
 608 zonkWantedEvVars :: Bag WantedEvVar -> TcM (Bag WantedEvVar)
 609 zonkWantedEvVars = mapBagM zonkWantedEvVar
 610
 611 zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
 612 zonkWantedEvVar (EvVarX v l) = do { v' <- zonkEvVar v; return (EvVarX v' l) }
 613
 614 zonkFlavor :: CtFlavor -> TcM CtFlavor
 615 zonkFlavor (Given loc) = do { loc' <- zonkGivenLoc loc; return (Given loc') }
 616 zonkFlavor fl          = return fl
 617
 618 zonkGivenLoc :: GivenLoc -> TcM GivenLoc
 619 -- GivenLocs may have unification variables inside them!
 620 zonkGivenLoc (CtLoc skol_info span ctxt)
 621   = do { skol_info' <- zonkSkolemInfo skol_info
 622        ; return (CtLoc skol_info' span ctxt) }
 623
 624 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
 625 zonkSkolemInfo (SigSkol cx ty)  = do { ty' <- zonkTcType ty
 626                                      ; return (SigSkol cx ty') }
 627 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
 628                                      ; return (InferSkol ntys') }
 629   where
 630     do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
 631 zonkSkolemInfo skol_info = return skol_info
 632 \end{code}
 633
 634 Note [Silly Type Synonyms]
 635 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 636 Consider this:
 637         type C u a = u  -- Note 'a' unused
 638
 639         foo :: (forall a. C u a -> C u a) -> u
 640         foo x = ...
 641
 642         bar :: Num u => u
 643         bar = foo (\t -> t + t)
 644
 645 * From the (\t -> t+t) we get type  {Num d} =>  d -> d
 646   where d is fresh.
 647
 648 * Now unify with type of foo's arg, and we get:
 649         {Num (C d a)} =>  C d a -> C d a
 650   where a is fresh.
 651
 652 * Now abstract over the 'a', but float out the Num (C d a) constraint
 653   because it does not 'really' mention a.  (see exactTyVarsOfType)
 654   The arg to foo becomes
 655         \/\a -> \t -> t+t
 656
 657 * So we get a dict binding for Num (C d a), which is zonked to give
 658         a = ()
 659   [Note Sept 04: now that we are zonking quantified type variables
 660   on construction, the 'a' will be frozen as a regular tyvar on
 661   quantification, so the floated dict will still have type (C d a).
 662   Which renders this whole note moot; happily!]
 663
 664 * Then the \/\a abstraction has a zonked 'a' in it.
 665
 666 All very silly.   I think its harmless to ignore the problem.  We'll end up with
 667 a \/\a in the final result but all the occurrences of a will be zonked to ()
 668
 669 Note [Zonking to Skolem]
 670 ~~~~~~~~~~~~~~~~~~~~~~~~
 671 We used to zonk quantified type variables to regular TyVars.  However, this
 672 leads to problems.  Consider this program from the regression test suite:
 673
 674   eval :: Int -> String -> String -> String
 675   eval 0 root actual = evalRHS 0 root actual
 676
 677   evalRHS :: Int -> a
 678   evalRHS 0 root actual = eval 0 root actual
 679
 680 It leads to the deferral of an equality (wrapped in an implication constraint)
 681
 682   forall a. (String -> String -> String) ~ a
 683
 684 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
 685 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
 686 This has the *side effect* of also zonking the `a' in the deferred equality
 687 (which at this point is being handed around wrapped in an implication
 688 constraint).
 689
 690 Finally, the equality (with the zonked `a') will be handed back to the
 691 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
 692 If we zonk `a' with a regular type variable, we will have this regular type
 693 variable now floating around in the simplifier, which in many places assumes to
 694 only see proper TcTyVars.
 695
 696 We can avoid this problem by zonking with a skolem.  The skolem is rigid
 697 (which we require for a quantified variable), but is still a TcTyVar that the
 698 simplifier knows how to deal with.
 699
 700
 701 %************************************************************************
 702 %*                                                                      *
 703 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
 704 %*                                                                      *
 705 %*              For internal use only!                                  *
 706 %*                                                                      *
 707 %************************************************************************
 708
 709 \begin{code}
 710 -- For unbound, mutable tyvars, zonkType uses the function given to it
 711 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 712 --      type variable and zonks the kind too
 713
 714 zonkType :: (TcTyVar -> TcM Type)  -- What to do with TcTyVars
 715          -> TcType -> TcM Type
 716 zonkType zonk_tc_tyvar ty
 717   = go ty
 718   where
 719     go (TyConApp tc tys) = do tys' <- mapM go tys
 720                               return (TyConApp tc tys')
 721
 722     go (PredTy p)        = do p' <- go_pred p
 723                               return (PredTy p')
 724
 725     go (FunTy arg res)   = do arg' <- go arg
 726                               res' <- go res
 727                               return (FunTy arg' res')
 728
 729     go (AppTy fun arg)   = do fun' <- go fun
 730                               arg' <- go arg
 731                               return (mkAppTy fun' arg')
 732                 -- NB the mkAppTy; we might have instantiated a
 733                 -- type variable to a type constructor, so we need
 734                 -- to pull the TyConApp to the top.
 735
 736         -- The two interesting cases!
 737     go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
 738                        | otherwise       = return (TyVarTy tyvar)
 739                 -- Ordinary (non Tc) tyvars occur inside quantified types
 740
 741     go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
 742                              ty' <- go ty
 743                              tyvar' <- return tyvar
 744                              return (ForAllTy tyvar' ty')
 745
 746     go_pred (ClassP c tys)   = do tys' <- mapM go tys
 747                                   return (ClassP c tys')
 748     go_pred (IParam n ty)    = do ty' <- go ty
 749                                   return (IParam n ty')
 750     go_pred (EqPred ty1 ty2) = do ty1' <- go ty1
 751                                   ty2' <- go ty2
 752                                   return (EqPred ty1' ty2')
 753
 754 mkZonkTcTyVar :: (TcTyVar -> TcM Type)  -- What to do for an *mutable Flexi* var
 755               -> TcTyVar -> TcM TcType
 756 mkZonkTcTyVar unbound_var_fn tyvar
 757   = ASSERT( isTcTyVar tyvar )
 758     case tcTyVarDetails tyvar of
 759       SkolemTv {}    -> return (TyVarTy tyvar)
 760       RuntimeUnk {}  -> return (TyVarTy tyvar)
 761       FlatSkol ty    -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
 762       MetaTv _ ref   -> do { cts <- readMutVar ref
 763                            ; case cts of
 764                                Flexi       -> unbound_var_fn tyvar
 765                                Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
 766 \end{code}
 767
 768
 769
 770 %************************************************************************
 771 %*                                                                      *
 772                         Zonking kinds
 773 %*                                                                      *
 774 %************************************************************************
 775
 776 \begin{code}
 777 readKindVar  :: KindVar -> TcM (MetaDetails)
 778 writeKindVar :: KindVar -> TcKind -> TcM ()
 779 readKindVar  kv = readMutVar (kindVarRef kv)
 780 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
 781
 782 -------------
 783 zonkTcKind :: TcKind -> TcM TcKind
 784 zonkTcKind k = zonkTcType k
 785
 786 -------------
 787 zonkTcKindToKind :: TcKind -> TcM Kind
 788 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
 789 -- Haskell specifies that * is to be used, so we follow that.
 790 zonkTcKindToKind k
 791   = zonkType (mkZonkTcTyVar (\ _ -> return liftedTypeKind)) k
 792 \end{code}
 793
 794 %************************************************************************
 795 %*                                                                      *
 796 \subsection{Checking a user type}
 797 %*                                                                      *
 798 %************************************************************************
 799
 800 When dealing with a user-written type, we first translate it from an HsType
 801 to a Type, performing kind checking, and then check various things that should
 802 be true about it.  We don't want to perform these checks at the same time
 803 as the initial translation because (a) they are unnecessary for interface-file
 804 types and (b) when checking a mutually recursive group of type and class decls,
 805 we can't "look" at the tycons/classes yet.  Also, the checks are are rather
 806 diverse, and used to really mess up the other code.
 807
 808 One thing we check for is 'rank'.
 809
 810         Rank 0:         monotypes (no foralls)
 811         Rank 1:         foralls at the front only, Rank 0 inside
 812         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
 813
 814         basic ::= tyvar | T basic ... basic
 815
 816         r2  ::= forall tvs. cxt => r2a
 817         r2a ::= r1 -> r2a | basic
 818         r1  ::= forall tvs. cxt => r0
 819         r0  ::= r0 -> r0 | basic
 820
 821 Another thing is to check that type synonyms are saturated.
 822 This might not necessarily show up in kind checking.
 823         type A i = i
 824         data T k = MkT (k Int)
 825         f :: T A        -- BAD!
 826
 827
 828 \begin{code}
 829 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 830 -- Checks that the type is valid for the given context
 831 checkValidType ctxt ty = do
 832     traceTc "checkValidType" (ppr ty)
 833     unboxed  <- xoptM Opt_UnboxedTuples
 834     rank2    <- xoptM Opt_Rank2Types
 835     rankn    <- xoptM Opt_RankNTypes
 836     polycomp <- xoptM Opt_PolymorphicComponents
 837     let
 838         gen_rank n | rankn     = ArbitraryRank
 839                    | rank2     = Rank 2
 840                    | otherwise = Rank n
 841         rank
 842           = case ctxt of
 843                  DefaultDeclCtxt-> MustBeMonoType
 844                  ResSigCtxt     -> MustBeMonoType
 845                  LamPatSigCtxt  -> gen_rank 0
 846                  BindPatSigCtxt -> gen_rank 0
 847                  TySynCtxt _    -> gen_rank 0
 848                  GenPatCtxt     -> gen_rank 1
 849                         -- This one is a bit of a hack
 850                         -- See the forall-wrapping in TcClassDcl.mkGenericInstance
 851
 852                  ExprSigCtxt    -> gen_rank 1
 853                  FunSigCtxt _   -> gen_rank 1
 854                  ConArgCtxt _   | polycomp -> gen_rank 2
 855                                 -- We are given the type of the entire
 856                                 -- constructor, hence rank 1
 857                                 | otherwise -> gen_rank 1
 858
 859                  ForSigCtxt _   -> gen_rank 1
 860                  SpecInstCtxt   -> gen_rank 1
 861                  ThBrackCtxt    -> gen_rank 1
 862                  GenSigCtxt     -> panic "checkValidType"
 863                                      -- Can't happen; GenSigCtxt not used for *user* sigs
 864
 865         actual_kind = typeKind ty
 866
 867         kind_ok = case ctxt of
 868                         TySynCtxt _  -> True -- Any kind will do
 869                         ThBrackCtxt  -> True -- Any kind will do
 870                         ResSigCtxt   -> isSubOpenTypeKind actual_kind
 871                         ExprSigCtxt  -> isSubOpenTypeKind actual_kind
 872                         GenPatCtxt   -> isLiftedTypeKind actual_kind
 873                         ForSigCtxt _ -> isLiftedTypeKind actual_kind
 874                         _            -> isSubArgTypeKind actual_kind
 875
 876         ubx_tup = case ctxt of
 877                       TySynCtxt _ | unboxed -> UT_Ok
 878                       ExprSigCtxt | unboxed -> UT_Ok
 879                       ThBrackCtxt | unboxed -> UT_Ok
 880                       _                     -> UT_NotOk
 881
 882         -- Check the internal validity of the type itself
 883     check_type rank ubx_tup ty
 884
 885         -- Check that the thing has kind Type, and is lifted if necessary
 886         -- Do this second, becuase we can't usefully take the kind of an
 887         -- ill-formed type such as (a~Int)
 888     checkTc kind_ok (kindErr actual_kind)
 889
 890     traceTc "checkValidType done" (ppr ty)
 891
 892 checkValidMonoType :: Type -> TcM ()
 893 checkValidMonoType ty = check_mono_type MustBeMonoType ty
 894 \end{code}
 895
 896
 897 \begin{code}
 898 data Rank = ArbitraryRank         -- Any rank ok
 899           | MustBeMonoType        -- Monotype regardless of flags
 900           | TyConArgMonoType      -- Monotype but could be poly if -XImpredicativeTypes
 901           | SynArgMonoType        -- Monotype but could be poly if -XLiberalTypeSynonyms
 902           | Rank Int              -- Rank n, but could be more with -XRankNTypes
 903
 904 decRank :: Rank -> Rank           -- Function arguments
 905 decRank (Rank 0)   = Rank 0
 906 decRank (Rank n)   = Rank (n-1)
 907 decRank other_rank = other_rank
 908
 909 nonZeroRank :: Rank -> Bool
 910 nonZeroRank ArbitraryRank = True
 911 nonZeroRank (Rank n)      = n>0
 912 nonZeroRank _             = False
 913
 914 ----------------------------------------
 915 data UbxTupFlag = UT_Ok | UT_NotOk
 916         -- The "Ok" version means "ok if UnboxedTuples is on"
 917
 918 ----------------------------------------
 919 check_mono_type :: Rank -> Type -> TcM ()       -- No foralls anywhere
 920                                                 -- No unlifted types of any kind
 921 check_mono_type rank ty
 922    = do { check_type rank UT_NotOk ty
 923         ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
 924
 925 check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 926 -- The args say what the *type context* requires, independent
 927 -- of *flag* settings.  You test the flag settings at usage sites.
 928 --
 929 -- Rank is allowed rank for function args
 930 -- Rank 0 means no for-alls anywhere
 931
 932 check_type rank ubx_tup ty
 933   | not (null tvs && null theta)
 934   = do  { checkTc (nonZeroRank rank) (forAllTyErr rank ty)
 935                 -- Reject e.g. (Maybe (?x::Int => Int)),
 936                 -- with a decent error message
 937         ; check_valid_theta SigmaCtxt theta
 938         ; check_type rank ubx_tup tau   -- Allow foralls to right of arrow
 939         ; checkAmbiguity tvs theta (tyVarsOfType tau) }
 940   where
 941     (tvs, theta, tau) = tcSplitSigmaTy ty
 942
 943 -- Naked PredTys should, I think, have been rejected before now
 944 check_type _ _ ty@(PredTy {})
 945   = failWithTc (text "Predicate" <+> ppr ty <+> text "used as a type")
 946
 947 check_type _ _ (TyVarTy _) = return ()
 948
 949 check_type rank _ (FunTy arg_ty res_ty)
 950   = do  { check_type (decRank rank) UT_NotOk arg_ty
 951         ; check_type rank           UT_Ok    res_ty }
 952
 953 check_type rank _ (AppTy ty1 ty2)
 954   = do  { check_arg_type rank ty1
 955         ; check_arg_type rank ty2 }
 956
 957 check_type rank ubx_tup ty@(TyConApp tc tys)
 958   | isSynTyCon tc
 959   = do  {       -- Check that the synonym has enough args
 960                 -- This applies equally to open and closed synonyms
 961                 -- It's OK to have an *over-applied* type synonym
 962                 --      data Tree a b = ...
 963                 --      type Foo a = Tree [a]
 964                 --      f :: Foo a b -> ...
 965           checkTc (tyConArity tc <= length tys) arity_msg
 966
 967         -- See Note [Liberal type synonyms]
 968         ; liberal <- xoptM Opt_LiberalTypeSynonyms
 969         ; if not liberal || isSynFamilyTyCon tc then
 970                 -- For H98 and synonym families, do check the type args
 971                 mapM_ (check_mono_type SynArgMonoType) tys
 972
 973           else  -- In the liberal case (only for closed syns), expand then check
 974           case tcView ty of
 975              Just ty' -> check_type rank ubx_tup ty'
 976              Nothing  -> pprPanic "check_tau_type" (ppr ty)
 977     }
 978
 979   | isUnboxedTupleTyCon tc
 980   = do  { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
 981         ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
 982
 983         ; impred <- xoptM Opt_ImpredicativeTypes
 984         ; let rank' = if impred then ArbitraryRank else TyConArgMonoType
 985                 -- c.f. check_arg_type
 986                 -- However, args are allowed to be unlifted, or
 987                 -- more unboxed tuples, so can't use check_arg_ty
 988         ; mapM_ (check_type rank' UT_Ok) tys }
 989
 990   | otherwise
 991   = mapM_ (check_arg_type rank) tys
 992
 993   where
 994     ubx_tup_ok ub_tuples_allowed = case ubx_tup of
 995                                    UT_Ok -> ub_tuples_allowed
 996                                    _     -> False
 997
 998     n_args    = length tys
 999     tc_arity  = tyConArity tc
1000
1001     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
1002     ubx_tup_msg = ubxArgTyErr ty
1003
1004 check_type _ _ ty = pprPanic "check_type" (ppr ty)
1005
1006 ----------------------------------------
1007 check_arg_type :: Rank -> Type -> TcM ()
1008 -- The sort of type that can instantiate a type variable,
1009 -- or be the argument of a type constructor.
1010 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
1011 -- Other unboxed types are very occasionally allowed as type
1012 -- arguments depending on the kind of the type constructor
1013 --
1014 -- For example, we want to reject things like:
1015 --
1016 --      instance Ord a => Ord (forall s. T s a)
1017 -- and
1018 --      g :: T s (forall b.b)
1019 --
1020 -- NB: unboxed tuples can have polymorphic or unboxed args.
1021 --     This happens in the workers for functions returning
1022 --     product types with polymorphic components.
1023 --     But not in user code.
1024 -- Anyway, they are dealt with by a special case in check_tau_type
1025
1026 check_arg_type rank ty
1027   = do  { impred <- xoptM Opt_ImpredicativeTypes
1028         ; let rank' = case rank of          -- Predictive => must be monotype
1029                         MustBeMonoType     -> MustBeMonoType  -- Monotype, regardless
1030                         _other | impred    -> ArbitraryRank
1031                                | otherwise -> TyConArgMonoType
1032                         -- Make sure that MustBeMonoType is propagated,
1033                         -- so that we don't suggest -XImpredicativeTypes in
1034                         --    (Ord (forall a.a)) => a -> a
1035                         -- and so that if it Must be a monotype, we check that it is!
1036
1037         ; check_type rank' UT_NotOk ty
1038         ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1039
1040 ----------------------------------------
1041 forAllTyErr :: Rank -> Type -> SDoc
1042 forAllTyErr rank ty
1043    = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
1044           , suggestion ]
1045   where
1046     suggestion = case rank of
1047                    Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types")
1048                    TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes")
1049                    SynArgMonoType -> ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms")
1050                    _ -> empty      -- Polytype is always illegal
1051
1052 unliftedArgErr, ubxArgTyErr :: Type -> SDoc
1053 unliftedArgErr  ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
1054 ubxArgTyErr     ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
1055
1056 kindErr :: Kind -> SDoc
1057 kindErr kind       = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
1058 \end{code}
1059
1060 Note [Liberal type synonyms]
1061 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1062 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
1063 doing validity checking.  This allows us to instantiate a synonym defn
1064 with a for-all type, or with a partially-applied type synonym.
1065         e.g.   type T a b = a
1066                type S m   = m ()
1067                f :: S (T Int)
1068 Here, T is partially applied, so it's illegal in H98.  But if you
1069 expand S first, then T we get just
1070                f :: Int
1071 which is fine.
1072
1073 IMPORTANT: suppose T is a type synonym.  Then we must do validity
1074 checking on an appliation (T ty1 ty2)
1075
1076         *either* before expansion (i.e. check ty1, ty2)
1077         *or* after expansion (i.e. expand T ty1 ty2, and then check)
1078         BUT NOT BOTH
1079
1080 If we do both, we get exponential behaviour!!
1081
1082   data TIACons1 i r c = c i ::: r c
1083   type TIACons2 t x = TIACons1 t (TIACons1 t x)
1084   type TIACons3 t x = TIACons2 t (TIACons1 t x)
1085   type TIACons4 t x = TIACons2 t (TIACons2 t x)
1086   type TIACons7 t x = TIACons4 t (TIACons3 t x)
1087
1088
1089 %************************************************************************
1090 %*                                                                      *
1091 \subsection{Checking a theta or source type}
1092 %*                                                                      *
1093 %************************************************************************
1094
1095 \begin{code}
1096 -- Enumerate the contexts in which a "source type", <S>, can occur
1097 --      Eq a
1098 -- or   ?x::Int
1099 -- or   r <: {x::Int}
1100 -- or   (N a) where N is a newtype
1101
1102 data SourceTyCtxt
1103   = ClassSCCtxt Name    -- Superclasses of clas
1104                         --      class <S> => C a where ...
1105   | SigmaCtxt           -- Theta part of a normal for-all type
1106                         --      f :: <S> => a -> a
1107   | DataTyCtxt Name     -- Theta part of a data decl
1108                         --      data <S> => T a = MkT a
1109   | TypeCtxt            -- Source type in an ordinary type
1110                         --      f :: N a -> N a
1111   | InstThetaCtxt       -- Context of an instance decl
1112                         --      instance <S> => C [a] where ...
1113
1114 pprSourceTyCtxt :: SourceTyCtxt -> SDoc
1115 pprSourceTyCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
1116 pprSourceTyCtxt SigmaCtxt       = ptext (sLit "the context of a polymorphic type")
1117 pprSourceTyCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
1118 pprSourceTyCtxt InstThetaCtxt   = ptext (sLit "the context of an instance declaration")
1119 pprSourceTyCtxt TypeCtxt        = ptext (sLit "the context of a type")
1120 \end{code}
1121
1122 \begin{code}
1123 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
1124 checkValidTheta ctxt theta
1125   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
1126
1127 -------------------------
1128 check_valid_theta :: SourceTyCtxt -> [PredType] -> TcM ()
1129 check_valid_theta _ []
1130   = return ()
1131 check_valid_theta ctxt theta = do
1132     dflags <- getDOpts
1133     warnTc (notNull dups) (dupPredWarn dups)
1134     mapM_ (check_pred_ty dflags ctxt) theta
1135   where
1136     (_,dups) = removeDups cmpPred theta
1137
1138 -------------------------
1139 check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
1140 check_pred_ty dflags ctxt pred@(ClassP cls tys)
1141   = do {        -- Class predicates are valid in all contexts
1142        ; checkTc (arity == n_tys) arity_err
1143
1144                 -- Check the form of the argument types
1145        ; mapM_ checkValidMonoType tys
1146        ; checkTc (check_class_pred_tys dflags ctxt tys)
1147                  (predTyVarErr pred $$ how_to_allow)
1148        }
1149   where
1150     class_name = className cls
1151     arity      = classArity cls
1152     n_tys      = length tys
1153     arity_err  = arityErr "Class" class_name arity n_tys
1154     how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
1155
1156
1157 check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
1158   = do {        -- Equational constraints are valid in all contexts if type
1159                 -- families are permitted
1160        ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
1161        ; checkTc (case ctxt of ClassSCCtxt {} -> False; _ -> True)
1162                  (eqSuperClassErr pred)
1163
1164                 -- Check the form of the argument types
1165        ; checkValidMonoType ty1
1166        ; checkValidMonoType ty2
1167        }
1168
1169 check_pred_ty _ SigmaCtxt (IParam _ ty) = checkValidMonoType ty
1170         -- Implicit parameters only allowed in type
1171         -- signatures; not in instance decls, superclasses etc
1172         -- The reason for not allowing implicit params in instances is a bit
1173         -- subtle.
1174         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
1175         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
1176         -- discharge all the potential usas of the ?x in e.   For example, a
1177         -- constraint Foo [Int] might come out of e,and applying the
1178         -- instance decl would show up two uses of ?x.
1179
1180 -- Catch-all
1181 check_pred_ty _ _ sty = failWithTc (badPredTyErr sty)
1182
1183 -------------------------
1184 check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
1185 check_class_pred_tys dflags ctxt tys
1186   = case ctxt of
1187         TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
1188         InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
1189                                 -- Further checks on head and theta in
1190                                 -- checkInstTermination
1191         _             -> flexible_contexts || all tyvar_head tys
1192   where
1193     flexible_contexts = xopt Opt_FlexibleContexts dflags
1194     undecidable_ok = xopt Opt_UndecidableInstances dflags
1195
1196 -------------------------
1197 tyvar_head :: Type -> Bool
1198 tyvar_head ty                   -- Haskell 98 allows predicates of form
1199   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
1200   | otherwise                   -- where a is a type variable
1201   = case tcSplitAppTy_maybe ty of
1202         Just (ty, _) -> tyvar_head ty
1203         Nothing      -> False
1204 \end{code}
1205
1206 Check for ambiguity
1207 ~~~~~~~~~~~~~~~~~~~
1208           forall V. P => tau
1209 is ambiguous if P contains generic variables
1210 (i.e. one of the Vs) that are not mentioned in tau
1211
1212 However, we need to take account of functional dependencies
1213 when we speak of 'mentioned in tau'.  Example:
1214         class C a b | a -> b where ...
1215 Then the type
1216         forall x y. (C x y) => x
1217 is not ambiguous because x is mentioned and x determines y
1218
1219 NB; the ambiguity check is only used for *user* types, not for types
1220 coming from inteface files.  The latter can legitimately have
1221 ambiguous types. Example
1222
1223    class S a where s :: a -> (Int,Int)
1224    instance S Char where s _ = (1,1)
1225    f:: S a => [a] -> Int -> (Int,Int)
1226    f (_::[a]) x = (a*x,b)
1227         where (a,b) = s (undefined::a)
1228
1229 Here the worker for f gets the type
1230         fw :: forall a. S a => Int -> (# Int, Int #)
1231
1232 If the list of tv_names is empty, we have a monotype, and then we
1233 don't need to check for ambiguity either, because the test can't fail
1234 (see is_ambig).
1235
1236 In addition, GHC insists that at least one type variable
1237 in each constraint is in V.  So we disallow a type like
1238         forall a. Eq b => b -> b
1239 even in a scope where b is in scope.
1240
1241 \begin{code}
1242 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1243 checkAmbiguity forall_tyvars theta tau_tyvars
1244   = mapM_ complain (filter is_ambig theta)
1245   where
1246     complain pred     = addErrTc (ambigErr pred)
1247     extended_tau_vars = growThetaTyVars theta tau_tyvars
1248
1249         -- See Note [Implicit parameters and ambiguity] in TcSimplify
1250     is_ambig pred     = isClassPred  pred &&
1251                         any ambig_var (varSetElems (tyVarsOfPred pred))
1252
1253     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
1254                         not (ct_var `elemVarSet` extended_tau_vars)
1255
1256 ambigErr :: PredType -> SDoc
1257 ambigErr pred
1258   = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPredTy pred),
1259          nest 2 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
1260                  ptext (sLit "must be reachable from the type after the '=>'"))]
1261 \end{code}
1262
1263 Note [Growing the tau-tvs using constraints]
1264 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1265 (growInstsTyVars insts tvs) is the result of extending the set
1266     of tyvars tvs using all conceivable links from pred
1267
1268 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
1269 Then grow precs tvs = {a,b,c}
1270
1271 \begin{code}
1272 growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
1273 -- See Note [Growing the tau-tvs using constraints]
1274 growThetaTyVars theta tvs
1275   | null theta = tvs
1276   | otherwise  = fixVarSet mk_next tvs
1277   where
1278     mk_next tvs = foldr grow_one tvs theta
1279     grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
1280
1281 growPredTyVars :: TcPredType
1282                -> TyVarSet      -- The set to extend
1283                -> TyVarSet      -- TyVars of the predicate if it intersects
1284                                 -- the set, or is implicit parameter
1285 growPredTyVars pred tvs
1286   | IParam {} <- pred               = pred_tvs  -- See Note [Implicit parameters and ambiguity]
1287   | pred_tvs `intersectsVarSet` tvs = pred_tvs
1288   | otherwise                       = emptyVarSet
1289   where
1290     pred_tvs = tyVarsOfPred pred
1291 \end{code}
1292
1293 Note [Implicit parameters and ambiguity]
1294 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1295 Only a *class* predicate can give rise to ambiguity
1296 An *implicit parameter* cannot.  For example:
1297         foo :: (?x :: [a]) => Int
1298         foo = length ?x
1299 is fine.  The call site will suppply a particular 'x'
1300
1301 Furthermore, the type variables fixed by an implicit parameter
1302 propagate to the others.  E.g.
1303         foo :: (Show a, ?x::[a]) => Int
1304         foo = show (?x++?x)
1305 The type of foo looks ambiguous.  But it isn't, because at a call site
1306 we might have
1307         let ?x = 5::Int in foo
1308 and all is well.  In effect, implicit parameters are, well, parameters,
1309 so we can take their type variables into account as part of the
1310 "tau-tvs" stuff.  This is done in the function 'FunDeps.grow'.
1311
1312
1313 \begin{code}
1314 checkThetaCtxt :: SourceTyCtxt -> ThetaType -> SDoc
1315 checkThetaCtxt ctxt theta
1316   = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
1317           ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
1318
1319 eqSuperClassErr :: PredType -> SDoc
1320 eqSuperClassErr pred
1321   = hang (ptext (sLit "Alas, GHC 7.0 still cannot handle equality superclasses:"))
1322        2 (ppr pred)
1323
1324 badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
1325 badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPredTy pred
1326 eqPredTyErr  pred = ptext (sLit "Illegal equational constraint") <+> pprPredTy pred
1327                     $$
1328                     parens (ptext (sLit "Use -XTypeFamilies to permit this"))
1329 predTyVarErr pred  = sep [ptext (sLit "Non type-variable argument"),
1330                           nest 2 (ptext (sLit "in the constraint:") <+> pprPredTy pred)]
1331 dupPredWarn :: [[PredType]] -> SDoc
1332 dupPredWarn dups   = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPredTy (map head dups)
1333
1334 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
1335 arityErr kind name n m
1336   = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
1337            n_arguments <> comma, text "but has been given",
1338            if m==0 then text "none" else int m]
1339     where
1340         n_arguments | n == 0 = ptext (sLit "no arguments")
1341                     | n == 1 = ptext (sLit "1 argument")
1342                     | True   = hsep [int n, ptext (sLit "arguments")]
1343 \end{code}
1344
1345 %************************************************************************
1346 %*                                                                      *
1347 \subsection{Checking for a decent instance head type}
1348 %*                                                                      *
1349 %************************************************************************
1350
1351 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1352 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1353
1354 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1355 flag is on, or (2)~the instance is imported (they must have been
1356 compiled elsewhere). In these cases, we let them go through anyway.
1357
1358 We can also have instances for functions: @instance Foo (a -> b) ...@.
1359
1360 \begin{code}
1361 checkValidInstHead :: Class -> [Type] -> TcM ()
1362 checkValidInstHead clas tys
1363   = do { dflags <- getDOpts
1364
1365            -- If GlasgowExts then check at least one isn't a type variable
1366        ; checkTc (xopt Opt_TypeSynonymInstances dflags ||
1367                   all tcInstHeadTyNotSynonym tys)
1368                  (instTypeErr pp_pred head_type_synonym_msg)
1369        ; checkTc (xopt Opt_FlexibleInstances dflags ||
1370                   all tcInstHeadTyAppAllTyVars tys)
1371                  (instTypeErr pp_pred head_type_args_tyvars_msg)
1372        ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
1373                   isSingleton tys)
1374                  (instTypeErr pp_pred head_one_type_msg)
1375          -- May not contain type family applications
1376        ; mapM_ checkTyFamFreeness tys
1377
1378        ; mapM_ checkValidMonoType tys
1379         -- For now, I only allow tau-types (not polytypes) in
1380         -- the head of an instance decl.
1381         --      E.g.  instance C (forall a. a->a) is rejected
1382         -- One could imagine generalising that, but I'm not sure
1383         -- what all the consequences might be
1384        }
1385
1386   where
1387     pp_pred = pprClassPred clas tys
1388     head_type_synonym_msg = parens (
1389                 text "All instance types must be of the form (T t1 ... tn)" $$
1390                 text "where T is not a synonym." $$
1391                 text "Use -XTypeSynonymInstances if you want to disable this.")
1392
1393     head_type_args_tyvars_msg = parens (vcat [
1394                 text "All instance types must be of the form (T a1 ... an)",
1395                 text "where a1 ... an are *distinct type variables*,",
1396                 text "and each type variable appears at most once in the instance head.",
1397                 text "Use -XFlexibleInstances if you want to disable this."])
1398
1399     head_one_type_msg = parens (
1400                 text "Only one type can be given in an instance head." $$
1401                 text "Use -XMultiParamTypeClasses if you want to allow more.")
1402
1403 instTypeErr :: SDoc -> SDoc -> SDoc
1404 instTypeErr pp_ty msg
1405   = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty,
1406          nest 2 msg]
1407 \end{code}
1408
1409
1410 %************************************************************************
1411 %*                                                                      *
1412 \subsection{Checking instance for termination}
1413 %*                                                                      *
1414 %************************************************************************
1415
1416 \begin{code}
1417 checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType
1418                    -> Class -> [TcType] -> TcM ()
1419 checkValidInstance hs_type tyvars theta clas inst_tys
1420   = setSrcSpan (getLoc hs_type) $
1421     do  { setSrcSpan head_loc (checkValidInstHead clas inst_tys)
1422         ; checkValidTheta InstThetaCtxt theta
1423         ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1424
1425         -- Check that instance inference will terminate (if we care)
1426         -- For Haskell 98 this will already have been done by checkValidTheta,
1427         -- but as we may be using other extensions we need to check.
1428         ; undecidable_ok <- xoptM Opt_UndecidableInstances
1429         ; unless undecidable_ok $
1430           mapM_ addErrTc (checkInstTermination inst_tys theta)
1431
1432         -- The Coverage Condition
1433         ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1434                   (instTypeErr (pprClassPred clas inst_tys) msg)
1435         }
1436   where
1437     msg  = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
1438                          undecidableMsg])
1439
1440         -- The location of the "head" of the instance
1441     head_loc = case hs_type of
1442                  L _ (HsForAllTy _ _ _ (L loc _)) -> loc
1443                  L loc _                          -> loc
1444 \end{code}
1445
1446 Termination test: the so-called "Paterson conditions" (see Section 5 of
1447 "Understanding functionsl dependencies via Constraint Handling Rules,
1448 JFP Jan 2007).
1449
1450 We check that each assertion in the context satisfies:
1451  (1) no variable has more occurrences in the assertion than in the head, and
1452  (2) the assertion has fewer constructors and variables (taken together
1453      and counting repetitions) than the head.
1454 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1455 (which have already been checked) guarantee termination.
1456
1457 The underlying idea is that
1458
1459     for any ground substitution, each assertion in the
1460     context has fewer type constructors than the head.
1461
1462
1463 \begin{code}
1464 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1465 checkInstTermination tys theta
1466   = mapCatMaybes check theta
1467   where
1468    fvs  = fvTypes tys
1469    size = sizeTypes tys
1470    check pred
1471       | not (null (fvPred pred \\ fvs))
1472       = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1473       | sizePred pred >= size
1474       = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1475       | otherwise
1476       = Nothing
1477
1478 predUndecErr :: PredType -> SDoc -> SDoc
1479 predUndecErr pred msg = sep [msg,
1480                         nest 2 (ptext (sLit "in the constraint:") <+> pprPredTy pred)]
1481
1482 nomoreMsg, smallerMsg, undecidableMsg :: SDoc
1483 nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
1484 smallerMsg = ptext (sLit "Constraint is no smaller than the instance head")
1485 undecidableMsg = ptext (sLit "Use -XUndecidableInstances to permit this")
1486 \end{code}
1487
1488 validDeivPred checks for OK 'deriving' context.  See Note [Exotic
1489 derived instance contexts] in TcSimplify.  However the predicate is
1490 here because it uses sizeTypes, fvTypes.
1491
1492 \begin{code}
1493 validDerivPred :: PredType -> Bool
1494 validDerivPred (ClassP _ tys) = hasNoDups fvs && sizeTypes tys == length fvs
1495                               where fvs = fvTypes tys
1496 validDerivPred _              = False
1497 \end{code}
1498
1499
1500 %************************************************************************
1501 %*                                                                      *
1502         Checking type instance well-formedness and termination
1503 %*                                                                      *
1504 %************************************************************************
1505
1506 \begin{code}
1507 -- Check that a "type instance" is well-formed (which includes decidability
1508 -- unless -XUndecidableInstances is given).
1509 --
1510 checkValidTypeInst :: [Type] -> Type -> TcM ()
1511 checkValidTypeInst typats rhs
1512   = do { -- left-hand side contains no type family applications
1513          -- (vanilla synonyms are fine, though)
1514        ; mapM_ checkTyFamFreeness typats
1515
1516          -- the right-hand side is a tau type
1517        ; checkValidMonoType rhs
1518
1519          -- we have a decidable instance unless otherwise permitted
1520        ; undecidable_ok <- xoptM Opt_UndecidableInstances
1521        ; unless undecidable_ok $
1522            mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
1523        }
1524
1525 -- Make sure that each type family instance is
1526 --   (1) strictly smaller than the lhs,
1527 --   (2) mentions no type variable more often than the lhs, and
1528 --   (3) does not contain any further type family instances.
1529 --
1530 checkFamInst :: [Type]                  -- lhs
1531              -> [(TyCon, [Type])]       -- type family instances
1532              -> [Message]
1533 checkFamInst lhsTys famInsts
1534   = mapCatMaybes check famInsts
1535   where
1536    size = sizeTypes lhsTys
1537    fvs  = fvTypes lhsTys
1538    check (tc, tys)
1539       | not (all isTyFamFree tys)
1540       = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1541       | not (null (fvTypes tys \\ fvs))
1542       = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1543       | size <= sizeTypes tys
1544       = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1545       | otherwise
1546       = Nothing
1547       where
1548         famInst = TyConApp tc tys
1549
1550 -- Ensure that no type family instances occur in a type.
1551 --
1552 checkTyFamFreeness :: Type -> TcM ()
1553 checkTyFamFreeness ty
1554   = checkTc (isTyFamFree ty) $
1555       tyFamInstIllegalErr ty
1556
1557 -- Check that a type does not contain any type family applications.
1558 --
1559 isTyFamFree :: Type -> Bool
1560 isTyFamFree = null . tyFamInsts
1561
1562 -- Error messages
1563
1564 tyFamInstIllegalErr :: Type -> SDoc
1565 tyFamInstIllegalErr ty
1566   = hang (ptext (sLit "Illegal type synonym family application in instance") <>
1567          colon) 2 $
1568       ppr ty
1569
1570 famInstUndecErr :: Type -> SDoc -> SDoc
1571 famInstUndecErr ty msg
1572   = sep [msg,
1573          nest 2 (ptext (sLit "in the type family application:") <+>
1574                  pprType ty)]
1575
1576 nestedMsg, nomoreVarMsg, smallerAppMsg :: SDoc
1577 nestedMsg     = ptext (sLit "Nested type family application")
1578 nomoreVarMsg  = ptext (sLit "Variable occurs more often than in instance head")
1579 smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
1580 \end{code}
1581
1582
1583 %************************************************************************
1584 %*                                                                      *
1585 \subsection{Auxiliary functions}
1586 %*                                                                      *
1587 %************************************************************************
1588
1589 \begin{code}
1590 -- Free variables of a type, retaining repetitions, and expanding synonyms
1591 fvType :: Type -> [TyVar]
1592 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1593 fvType (TyVarTy tv)        = [tv]
1594 fvType (TyConApp _ tys)    = fvTypes tys
1595 fvType (PredTy pred)       = fvPred pred
1596 fvType (FunTy arg res)     = fvType arg ++ fvType res
1597 fvType (AppTy fun arg)     = fvType fun ++ fvType arg
1598 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1599
1600 fvTypes :: [Type] -> [TyVar]
1601 fvTypes tys                = concat (map fvType tys)
1602
1603 fvPred :: PredType -> [TyVar]
1604 fvPred (ClassP _ tys')     = fvTypes tys'
1605 fvPred (IParam _ ty)       = fvType ty
1606 fvPred (EqPred ty1 ty2)    = fvType ty1 ++ fvType ty2
1607
1608 -- Size of a type: the number of variables and constructors
1609 sizeType :: Type -> Int
1610 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1611 sizeType (TyVarTy _)       = 1
1612 sizeType (TyConApp _ tys)  = sizeTypes tys + 1
1613 sizeType (PredTy pred)     = sizePred pred
1614 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
1615 sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
1616 sizeType (ForAllTy _ ty)   = sizeType ty
1617
1618 sizeTypes :: [Type] -> Int
1619 sizeTypes xs               = sum (map sizeType xs)
1620
1621 -- Size of a predicate
1622 --
1623 -- We are considering whether *class* constraints terminate
1624 -- Once we get into an implicit parameter or equality we
1625 -- can't get back to a class constraint, so it's safe
1626 -- to say "size 0".  See Trac #4200.
1627 sizePred :: PredType -> Int
1628 sizePred (ClassP _ tys')   = sizeTypes tys'
1629 sizePred (IParam {})       = 0
1630 sizePred (EqPred {})       = 0
1631 \end{code}