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