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