compiler/typecheck/TcMType.lhs

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