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