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