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