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