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 {-# OPTIONS -w #-}
  13 -- The above warning supression flag is a temporary kludge.
  14 -- While working on this module you are encouraged to remove it and fix
  15 -- any warnings in the module. See
  16 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
  17 -- for details
  18
  19 module TcMType (
  20   TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
  21
  22   --------------------------------
  23   -- Creating new mutable type variables
  24   newFlexiTyVar,
  25   newFlexiTyVarTy,              -- Kind -> TcM TcType
  26   newFlexiTyVarTys,             -- Int -> Kind -> TcM [TcType]
  27   newKindVar, newKindVars,
  28   lookupTcTyVar, LookupTyVarResult(..),
  29   newMetaTyVar, readMetaTyVar, writeMetaTyVar,
  30
  31   --------------------------------
  32   -- Boxy type variables
  33   newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox,
  34
  35   --------------------------------
  36   -- Creating new coercion variables
  37   newCoVars, newMetaCoVar,
  38
  39   --------------------------------
  40   -- Instantiation
  41   tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
  42   tcInstSigTyVars, zonkSigTyVar,
  43   tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
  44   tcSkolSigType, tcSkolSigTyVars, occurCheckErr,
  45
  46   --------------------------------
  47   -- Checking type validity
  48   Rank, UserTypeCtxt(..), checkValidType,
  49   SourceTyCtxt(..), checkValidTheta, checkFreeness,
  50   checkValidInstHead, checkValidInstance,
  51   checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
  52   checkUpdateMeta, updateMeta, checkTauTvUpdate, fillBoxWithTau, unifyKindCtxt,
  53   unifyKindMisMatch, validDerivPred, arityErr, notMonoType, notMonoArgs,
  54
  55   --------------------------------
  56   -- Zonking
  57   zonkType, zonkTcPredType,
  58   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV,
  59   zonkQuantifiedTyVar, zonkQuantifiedTyVars,
  60   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
  61   zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
  62
  63   readKindVar, writeKindVar
  64   ) where
  65
  66 #include "HsVersions.h"
  67
  68 -- friends:
  69 import TypeRep
  70 import TcType
  71 import Type
  72 import Coercion
  73 import Class
  74 import TyCon
  75 import Var
  76
  77 -- others:
  78 import TcRnMonad          -- TcType, amongst others
  79 import FunDeps
  80 import Name
  81 import VarSet
  82 import ErrUtils
  83 import DynFlags
  84 import Util
  85 import Maybes
  86 import ListSetOps
  87 import UniqSupply
  88 import SrcLoc
  89 import Outputable
  90
  91 import Control.Monad    ( when, unless )
  92 import Data.List        ( (\\) )
  93 \end{code}
  94
  95
  96 %************************************************************************
  97 %*                                                                      *
  98         Instantiation in general
  99 %*                                                                      *
 100 %************************************************************************
 101
 102 \begin{code}
 103 tcInstType :: ([TyVar] -> TcM [TcTyVar])                -- How to instantiate the type variables
 104            -> TcType                                    -- Type to instantiate
 105            -> TcM ([TcTyVar], TcThetaType, TcType)      -- Result
 106 tcInstType inst_tyvars ty
 107   = case tcSplitForAllTys ty of
 108         ([],     rho) -> let    -- There may be overloading despite no type variables;
 109                                 --      (?x :: Int) => Int -> Int
 110                            (theta, tau) = tcSplitPhiTy rho
 111                          in
 112                          return ([], theta, tau)
 113
 114         (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
 115
 116                             ; let  tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
 117                                 -- Either the tyvars are freshly made, by inst_tyvars,
 118                                 -- or (in the call from tcSkolSigType) any nested foralls
 119                                 -- have different binders.  Either way, zipTopTvSubst is ok
 120
 121                             ; let  (theta, tau) = tcSplitPhiTy (substTy tenv rho)
 122                             ; return (tyvars', theta, tau) }
 123 \end{code}
 124
 125
 126 %************************************************************************
 127 %*                                                                      *
 128         Updating tau types
 129 %*                                                                      *
 130 %************************************************************************
 131
 132 Can't be in TcUnify, as we also need it in TcTyFuns.
 133
 134 \begin{code}
 135 type SwapFlag = Bool
 136         -- False <=> the two args are (actual, expected) respectively
 137         -- True  <=> the two args are (expected, actual) respectively
 138
 139 checkUpdateMeta :: SwapFlag
 140                 -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
 141 -- Update tv1, which is flexi; occurs check is alrady done
 142 -- The 'check' version does a kind check too
 143 -- We do a sub-kind check here: we might unify (a b) with (c d)
 144 --      where b::*->* and d::*; this should fail
 145
 146 checkUpdateMeta swapped tv1 ref1 ty2
 147   = do  { checkKinds swapped tv1 ty2
 148         ; updateMeta tv1 ref1 ty2 }
 149
 150 updateMeta :: TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
 151 updateMeta tv1 ref1 ty2
 152   = ASSERT( isMetaTyVar tv1 )
 153     ASSERT( isBoxyTyVar tv1 || isTauTy ty2 )
 154     do  { ASSERTM2( do { details <- readMetaTyVar tv1; return (isFlexi details) }, ppr tv1 )
 155         ; traceTc (text "updateMeta" <+> ppr tv1 <+> text ":=" <+> ppr ty2)
 156         ; writeMutVar ref1 (Indirect ty2)
 157         }
 158
 159 ----------------
 160 checkKinds swapped tv1 ty2
 161 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
 162 -- ty2 has been zonked at this stage, which ensures that
 163 -- its kind has as much boxity information visible as possible.
 164   | tk2 `isSubKind` tk1 = returnM ()
 165
 166   | otherwise
 167         -- Either the kinds aren't compatible
 168         --      (can happen if we unify (a b) with (c d))
 169         -- or we are unifying a lifted type variable with an
 170         --      unlifted type: e.g.  (id 3#) is illegal
 171   = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
 172     unifyKindMisMatch k1 k2
 173   where
 174     (k1,k2) | swapped   = (tk2,tk1)
 175             | otherwise = (tk1,tk2)
 176     tk1 = tyVarKind tv1
 177     tk2 = typeKind ty2
 178
 179 ----------------
 180 checkTauTvUpdate :: TcTyVar -> TcType -> TcM TcType
 181 --    (checkTauTvUpdate tv ty)
 182 -- We are about to update the TauTv tv with ty.
 183 -- Check (a) that tv doesn't occur in ty (occurs check)
 184 --       (b) that ty is a monotype
 185 -- Furthermore, in the interest of (b), if you find an
 186 -- empty box (BoxTv that is Flexi), fill it in with a TauTv
 187 --
 188 -- Returns the (non-boxy) type to update the type variable with, or fails
 189
 190 checkTauTvUpdate orig_tv orig_ty
 191   = go orig_ty
 192   where
 193     go (TyConApp tc tys)
 194         | isSynTyCon tc  = go_syn tc tys
 195         | otherwise      = do { tys' <- mappM go tys; return (TyConApp tc tys') }
 196     go (NoteTy _ ty2)    = go ty2       -- Discard free-tyvar annotations
 197     go (PredTy p)        = do { p' <- go_pred p; return (PredTy p') }
 198     go (FunTy arg res)   = do { arg' <- go arg; res' <- go res; return (FunTy arg' res') }
 199     go (AppTy fun arg)   = do { fun' <- go fun; arg' <- go arg; return (mkAppTy fun' arg') }
 200                 -- NB the mkAppTy; we might have instantiated a
 201                 -- type variable to a type constructor, so we need
 202                 -- to pull the TyConApp to the top.
 203     go (ForAllTy tv ty) = notMonoType orig_ty           -- (b)
 204
 205     go (TyVarTy tv)
 206         | orig_tv == tv = occurCheck tv                 -- (a)
 207         | isTcTyVar tv  = go_tyvar tv (tcTyVarDetails tv)
 208         | otherwise     = return (TyVarTy tv)
 209                  -- Ordinary (non Tc) tyvars
 210                  -- occur inside quantified types
 211
 212     go_pred (ClassP c tys) = do { tys' <- mapM go tys; return (ClassP c tys') }
 213     go_pred (IParam n ty)  = do { ty' <- go ty;        return (IParam n ty') }
 214     go_pred (EqPred t1 t2) = do { t1' <- go t1; t2' <- go t2; return (EqPred t1' t2') }
 215
 216     go_tyvar tv (SkolemTv _) = return (TyVarTy tv)
 217     go_tyvar tv (MetaTv box ref)
 218         = do { cts <- readMutVar ref
 219              ; case cts of
 220                   Indirect ty -> go ty
 221                   Flexi -> case box of
 222                                 BoxTv -> fillBoxWithTau tv ref
 223                                 other -> return (TyVarTy tv)
 224              }
 225
 226         -- go_syn is called for synonyms only
 227         -- See Note [Type synonyms and the occur check]
 228     go_syn tc tys
 229         | not (isTauTyCon tc)
 230         = notMonoType orig_ty   -- (b) again
 231         | otherwise
 232         = do { (msgs, mb_tys') <- tryTc (mapM go tys)
 233              ; case mb_tys' of
 234                 Just tys' -> return (TyConApp tc tys')
 235                                 -- Retain the synonym (the common case)
 236                 Nothing | isOpenTyCon tc
 237                           -> notMonoArgs (TyConApp tc tys)
 238                                 -- Synonym families must have monotype args
 239                         | otherwise
 240                           -> go (expectJust "checkTauTvUpdate"
 241                                         (tcView (TyConApp tc tys)))
 242                                 -- Try again, expanding the synonym
 243              }
 244
 245     occurCheck tv = occurCheckErr (mkTyVarTy tv) orig_ty
 246
 247 fillBoxWithTau :: BoxyTyVar -> IORef MetaDetails -> TcM TcType
 248 -- (fillBoxWithTau tv ref) fills ref with a freshly allocated
 249 --  tau-type meta-variable, whose print-name is the same as tv
 250 -- Choosing the same name is good: when we instantiate a function
 251 -- we allocate boxy tyvars with the same print-name as the quantified
 252 -- tyvar; and then we often fill the box with a tau-tyvar, and again
 253 -- we want to choose the same name.
 254 fillBoxWithTau tv ref
 255   = do  { tv' <- tcInstTyVar tv         -- Do not gratuitously forget
 256         ; let tau = mkTyVarTy tv'       -- name of the type variable
 257         ; writeMutVar ref (Indirect tau)
 258         ; return tau }
 259 \end{code}
 260
 261 Error mesages in case of kind mismatch.
 262
 263 \begin{code}
 264 unifyKindMisMatch ty1 ty2
 265   = zonkTcKind ty1      `thenM` \ ty1' ->
 266     zonkTcKind ty2      `thenM` \ ty2' ->
 267     let
 268         msg = hang (ptext SLIT("Couldn't match kind"))
 269                    2 (sep [quotes (ppr ty1'),
 270                            ptext SLIT("against"),
 271                            quotes (ppr ty2')])
 272     in
 273     failWithTc msg
 274
 275 unifyKindCtxt swapped tv1 ty2 tidy_env  -- not swapped => tv1 expected, ty2 inferred
 276         -- tv1 and ty2 are zonked already
 277   = returnM msg
 278   where
 279     msg = (env2, ptext SLIT("When matching the kinds of") <+>
 280                  sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual])
 281
 282     (pp_expected, pp_actual) | swapped   = (pp2, pp1)
 283                              | otherwise = (pp1, pp2)
 284     (env1, tv1') = tidyOpenTyVar tidy_env tv1
 285     (env2, ty2') = tidyOpenType  env1 ty2
 286     pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1)
 287     pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)
 288 \end{code}
 289
 290 Error message for failure due to an occurs check.
 291
 292 \begin{code}
 293 occurCheckErr :: TcType -> TcType -> TcM a
 294 occurCheckErr ty containingTy
 295   = do  { env0 <- tcInitTidyEnv
 296         ; ty'           <- zonkTcType ty
 297         ; containingTy' <- zonkTcType containingTy
 298         ; let (env1, tidy_ty1) = tidyOpenType env0 ty'
 299               (env2, tidy_ty2) = tidyOpenType env1 containingTy'
 300               extra = sep [ppr tidy_ty1, char '=', ppr tidy_ty2]
 301         ; failWithTcM (env2, hang msg 2 extra) }
 302   where
 303     msg = ptext SLIT("Occurs check: cannot construct the infinite type:")
 304 \end{code}
 305
 306 %************************************************************************
 307 %*                                                                      *
 308         Kind variables
 309 %*                                                                      *
 310 %************************************************************************
 311
 312 \begin{code}
 313 newCoVars :: [(TcType,TcType)] -> TcM [CoVar]
 314 newCoVars spec
 315   = do  { us <- newUniqueSupply
 316         ; return [ mkCoVar (mkSysTvName uniq FSLIT("co"))
 317                            (mkCoKind ty1 ty2)
 318                  | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
 319
 320 newMetaCoVar :: TcType -> TcType -> TcM TcTyVar
 321 newMetaCoVar ty1 ty2 = newMetaTyVar TauTv (mkCoKind ty1 ty2)
 322
 323 newKindVar :: TcM TcKind
 324 newKindVar = do { uniq <- newUnique
 325                 ; ref <- newMutVar Flexi
 326                 ; return (mkTyVarTy (mkKindVar uniq ref)) }
 327
 328 newKindVars :: Int -> TcM [TcKind]
 329 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
 330 \end{code}
 331
 332
 333 %************************************************************************
 334 %*                                                                      *
 335         SkolemTvs (immutable)
 336 %*                                                                      *
 337 %************************************************************************
 338
 339 \begin{code}
 340 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
 341 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
 342
 343 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
 344 -- Instantiate a type signature with skolem constants, but
 345 -- do *not* give them fresh names, because we want the name to
 346 -- be in the type environment -- it is lexically scoped.
 347 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
 348
 349 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
 350 -- Make skolem constants, but do *not* give them new names, as above
 351 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
 352                               | tv <- tyvars ]
 353
 354 tcInstSkolTyVar :: SkolemInfo -> Maybe SrcSpan -> TyVar -> TcM TcTyVar
 355 -- Instantiate the tyvar, using
 356 --      * the occ-name and kind of the supplied tyvar,
 357 --      * the unique from the monad,
 358 --      * the location either from the tyvar (mb_loc = Nothing)
 359 --        or from mb_loc (Just loc)
 360 tcInstSkolTyVar info mb_loc tyvar
 361   = do  { uniq <- newUnique
 362         ; let old_name = tyVarName tyvar
 363               kind     = tyVarKind tyvar
 364               loc      = mb_loc `orElse` getSrcSpan old_name
 365               new_name = mkInternalName uniq (nameOccName old_name) loc
 366         ; return (mkSkolTyVar new_name kind info) }
 367
 368 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
 369 -- Get the location from the monad
 370 tcInstSkolTyVars info tyvars
 371   = do  { span <- getSrcSpanM
 372         ; mapM (tcInstSkolTyVar info (Just span)) tyvars }
 373
 374 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
 375 -- Instantiate a type with fresh skolem constants
 376 -- Binding location comes from the monad
 377 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
 378 \end{code}
 379
 380
 381 %************************************************************************
 382 %*                                                                      *
 383         MetaTvs (meta type variables; mutable)
 384 %*                                                                      *
 385 %************************************************************************
 386
 387 \begin{code}
 388 newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
 389 -- Make a new meta tyvar out of thin air
 390 newMetaTyVar box_info kind
 391   = do  { uniq <- newUnique
 392         ; ref <- newMutVar Flexi
 393         ; let name = mkSysTvName uniq fs
 394               fs = case box_info of
 395                         BoxTv   -> FSLIT("t")
 396                         TauTv   -> FSLIT("t")
 397                         SigTv _ -> FSLIT("a")
 398                 -- We give BoxTv and TauTv the same string, because
 399                 -- otherwise we get user-visible differences in error
 400                 -- messages, which are confusing.  If you want to see
 401                 -- the box_info of each tyvar, use -dppr-debug
 402         ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
 403
 404 instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
 405 -- Make a new meta tyvar whose Name and Kind
 406 -- come from an existing TyVar
 407 instMetaTyVar box_info tyvar
 408   = do  { uniq <- newUnique
 409         ; ref <- newMutVar Flexi
 410         ; let name = setNameUnique (tyVarName tyvar) uniq
 411               kind = tyVarKind tyvar
 412         ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
 413
 414 readMetaTyVar :: TyVar -> TcM MetaDetails
 415 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
 416                       readMutVar (metaTvRef tyvar)
 417
 418 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
 419 #ifndef DEBUG
 420 writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
 421 #else
 422 writeMetaTyVar tyvar ty
 423   | not (isMetaTyVar tyvar)
 424   = pprTrace "writeMetaTyVar" (ppr tyvar) $
 425     returnM ()
 426
 427   | otherwise
 428   = ASSERT( isMetaTyVar tyvar )
 429     -- TOM: It should also work for coercions
 430     -- ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
 431     do  { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
 432         ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
 433   where
 434     k1 = tyVarKind tyvar
 435     k2 = typeKind ty
 436 #endif
 437 \end{code}
 438
 439
 440 %************************************************************************
 441 %*                                                                      *
 442         MetaTvs: TauTvs
 443 %*                                                                      *
 444 %************************************************************************
 445
 446 \begin{code}
 447 newFlexiTyVar :: Kind -> TcM TcTyVar
 448 newFlexiTyVar kind = newMetaTyVar TauTv kind
 449
 450 newFlexiTyVarTy  :: Kind -> TcM TcType
 451 newFlexiTyVarTy kind
 452   = newFlexiTyVar kind  `thenM` \ tc_tyvar ->
 453     returnM (TyVarTy tc_tyvar)
 454
 455 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
 456 newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind)
 457
 458 tcInstTyVar :: TyVar -> TcM TcTyVar
 459 -- Instantiate with a META type variable
 460 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
 461
 462 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
 463 -- Instantiate with META type variables
 464 tcInstTyVars tyvars
 465   = do  { tc_tvs <- mapM tcInstTyVar tyvars
 466         ; let tys = mkTyVarTys tc_tvs
 467         ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
 468                 -- Since the tyvars are freshly made,
 469                 -- they cannot possibly be captured by
 470                 -- any existing for-alls.  Hence zipTopTvSubst
 471 \end{code}
 472
 473
 474 %************************************************************************
 475 %*                                                                      *
 476         MetaTvs: SigTvs
 477 %*                                                                      *
 478 %************************************************************************
 479
 480 \begin{code}
 481 tcInstSigTyVars :: Bool -> SkolemInfo -> [TyVar] -> TcM [TcTyVar]
 482 -- Instantiate with skolems or meta SigTvs; depending on use_skols
 483 -- Always take location info from the supplied tyvars
 484 tcInstSigTyVars use_skols skol_info tyvars
 485   | use_skols
 486   = mapM (tcInstSkolTyVar skol_info Nothing) tyvars
 487
 488   | otherwise
 489   = mapM (instMetaTyVar (SigTv skol_info)) tyvars
 490
 491 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
 492 zonkSigTyVar sig_tv
 493   | isSkolemTyVar sig_tv
 494   = return sig_tv       -- Happens in the call in TcBinds.checkDistinctTyVars
 495   | otherwise
 496   = ASSERT( isSigTyVar sig_tv )
 497     do { ty <- zonkTcTyVar sig_tv
 498        ; return (tcGetTyVar "zonkSigTyVar" ty) }
 499         -- 'ty' is bound to be a type variable, because SigTvs
 500         -- can only be unified with type variables
 501 \end{code}
 502
 503
 504 %************************************************************************
 505 %*                                                                      *
 506         MetaTvs: BoxTvs
 507 %*                                                                      *
 508 %************************************************************************
 509
 510 \begin{code}
 511 newBoxyTyVar :: Kind -> TcM BoxyTyVar
 512 newBoxyTyVar kind = newMetaTyVar BoxTv kind
 513
 514 newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
 515 newBoxyTyVars kinds = mapM newBoxyTyVar kinds
 516
 517 newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
 518 newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
 519
 520 readFilledBox :: BoxyTyVar -> TcM TcType
 521 -- Read the contents of the box, which should be filled in by now
 522 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
 523                        do { cts <- readMetaTyVar box_tv
 524                           ; case cts of
 525                                 Flexi -> pprPanic "readFilledBox" (ppr box_tv)
 526                                 Indirect ty -> return ty }
 527
 528 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
 529 -- Instantiate with a BOXY type variable
 530 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
 531 \end{code}
 532
 533
 534 %************************************************************************
 535 %*                                                                      *
 536 \subsection{Putting and getting  mutable type variables}
 537 %*                                                                      *
 538 %************************************************************************
 539
 540 But it's more fun to short out indirections on the way: If this
 541 version returns a TyVar, then that TyVar is unbound.  If it returns
 542 any other type, then there might be bound TyVars embedded inside it.
 543
 544 We return Nothing iff the original box was unbound.
 545
 546 \begin{code}
 547 data LookupTyVarResult  -- The result of a lookupTcTyVar call
 548   = DoneTv TcTyVarDetails       -- SkolemTv or virgin MetaTv
 549   | IndirectTv TcType
 550
 551 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
 552 lookupTcTyVar tyvar
 553   = ASSERT2( isTcTyVar tyvar, ppr tyvar )
 554     case details of
 555       SkolemTv _   -> return (DoneTv details)
 556       MetaTv _ ref -> do { meta_details <- readMutVar ref
 557                          ; case meta_details of
 558                             Indirect ty -> return (IndirectTv ty)
 559                             Flexi -> return (DoneTv details) }
 560   where
 561     details =  tcTyVarDetails tyvar
 562
 563 {-
 564 -- gaw 2004 We aren't shorting anything out anymore, at least for now
 565 getTcTyVar tyvar
 566   | not (isTcTyVar tyvar)
 567   = pprTrace "getTcTyVar" (ppr tyvar) $
 568     returnM (Just (mkTyVarTy tyvar))
 569
 570   | otherwise
 571   = ASSERT2( isTcTyVar tyvar, ppr tyvar )
 572     readMetaTyVar tyvar                         `thenM` \ maybe_ty ->
 573     case maybe_ty of
 574         Just ty -> short_out ty                         `thenM` \ ty' ->
 575                    writeMetaTyVar tyvar (Just ty')      `thenM_`
 576                    returnM (Just ty')
 577
 578         Nothing    -> returnM Nothing
 579
 580 short_out :: TcType -> TcM TcType
 581 short_out ty@(TyVarTy tyvar)
 582   | not (isTcTyVar tyvar)
 583   = returnM ty
 584
 585   | otherwise
 586   = readMetaTyVar tyvar `thenM` \ maybe_ty ->
 587     case maybe_ty of
 588         Just ty' -> short_out ty'                       `thenM` \ ty' ->
 589                     writeMetaTyVar tyvar (Just ty')     `thenM_`
 590                     returnM ty'
 591
 592         other    -> returnM ty
 593
 594 short_out other_ty = returnM other_ty
 595 -}
 596 \end{code}
 597
 598
 599 %************************************************************************
 600 %*                                                                      *
 601 \subsection{Zonking -- the exernal interfaces}
 602 %*                                                                      *
 603 %************************************************************************
 604
 605 -----------------  Type variables
 606
 607 \begin{code}
 608 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
 609 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
 610
 611 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
 612 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars     `thenM` \ tys ->
 613                            returnM (tyVarsOfTypes tys)
 614
 615 zonkTcTyVar :: TcTyVar -> TcM TcType
 616 zonkTcTyVar tyvar = ASSERT2( isTcTyVar tyvar, ppr tyvar)
 617                     zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
 618 \end{code}
 619
 620 -----------------  Types
 621
 622 \begin{code}
 623 zonkTcType :: TcType -> TcM TcType
 624 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
 625
 626 zonkTcTypes :: [TcType] -> TcM [TcType]
 627 zonkTcTypes tys = mappM zonkTcType tys
 628
 629 zonkTcClassConstraints cts = mappM zonk cts
 630     where zonk (clas, tys)
 631             = zonkTcTypes tys   `thenM` \ new_tys ->
 632               returnM (clas, new_tys)
 633
 634 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
 635 zonkTcThetaType theta = mappM zonkTcPredType theta
 636
 637 zonkTcPredType :: TcPredType -> TcM TcPredType
 638 zonkTcPredType (ClassP c ts)
 639   = zonkTcTypes ts      `thenM` \ new_ts ->
 640     returnM (ClassP c new_ts)
 641 zonkTcPredType (IParam n t)
 642   = zonkTcType t        `thenM` \ new_t ->
 643     returnM (IParam n new_t)
 644 zonkTcPredType (EqPred t1 t2)
 645   = zonkTcType t1       `thenM` \ new_t1 ->
 646     zonkTcType t2       `thenM` \ new_t2 ->
 647     returnM (EqPred new_t1 new_t2)
 648 \end{code}
 649
 650 -------------------  These ...ToType, ...ToKind versions
 651                      are used at the end of type checking
 652
 653 \begin{code}
 654 zonkTopTyVar :: TcTyVar -> TcM TcTyVar
 655 -- zonkTopTyVar is used, at the top level, on any un-instantiated meta type variables
 656 -- to default the kind of ? and ?? etc to *.  This is important to ensure that
 657 -- instance declarations match.  For example consider
 658 --      instance Show (a->b)
 659 --      foo x = show (\_ -> True)
 660 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
 661 -- and that won't match the typeKind (*) in the instance decl.
 662 --
 663 -- Because we are at top level, no further constraints are going to affect these
 664 -- type variables, so it's time to do it by hand.  However we aren't ready
 665 -- to default them fully to () or whatever, because the type-class defaulting
 666 -- rules have yet to run.
 667
 668 zonkTopTyVar tv
 669   | k `eqKind` default_k = return tv
 670   | otherwise
 671   = do  { tv' <- newFlexiTyVar default_k
 672         ; writeMetaTyVar tv (mkTyVarTy tv')
 673         ; return tv' }
 674   where
 675     k = tyVarKind tv
 676     default_k = defaultKind k
 677
 678 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TyVar]
 679 zonkQuantifiedTyVars = mappM zonkQuantifiedTyVar
 680
 681 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
 682 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
 683 --
 684 -- The quantified type variables often include meta type variables
 685 -- we want to freeze them into ordinary type variables, and
 686 -- default their kind (e.g. from OpenTypeKind to TypeKind)
 687 --                      -- see notes with Kind.defaultKind
 688 -- The meta tyvar is updated to point to the new regular TyVar.  Now any
 689 -- bound occurences of the original type variable will get zonked to
 690 -- the immutable version.
 691 --
 692 -- We leave skolem TyVars alone; they are immutable.
 693 zonkQuantifiedTyVar tv
 694   | ASSERT( isTcTyVar tv )
 695     isSkolemTyVar tv = return tv
 696         -- It might be a skolem type variable,
 697         -- for example from a user type signature
 698
 699   | otherwise   -- It's a meta-type-variable
 700   = do  { details <- readMetaTyVar tv
 701
 702         -- Create the new, frozen, regular type variable
 703         ; let final_kind = defaultKind (tyVarKind tv)
 704               final_tv   = mkTyVar (tyVarName tv) final_kind
 705
 706         -- Bind the meta tyvar to the new tyvar
 707         ; case details of
 708             Indirect ty -> WARN( True, ppr tv $$ ppr ty )
 709                            return ()
 710                 -- [Sept 04] I don't think this should happen
 711                 -- See note [Silly Type Synonym]
 712
 713             Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
 714
 715         -- Return the new tyvar
 716         ; return final_tv }
 717 \end{code}
 718
 719 [Silly Type Synonyms]
 720
 721 Consider this:
 722         type C u a = u  -- Note 'a' unused
 723
 724         foo :: (forall a. C u a -> C u a) -> u
 725         foo x = ...
 726
 727         bar :: Num u => u
 728         bar = foo (\t -> t + t)
 729
 730 * From the (\t -> t+t) we get type  {Num d} =>  d -> d
 731   where d is fresh.
 732
 733 * Now unify with type of foo's arg, and we get:
 734         {Num (C d a)} =>  C d a -> C d a
 735   where a is fresh.
 736
 737 * Now abstract over the 'a', but float out the Num (C d a) constraint
 738   because it does not 'really' mention a.  (see exactTyVarsOfType)
 739   The arg to foo becomes
 740         /\a -> \t -> t+t
 741
 742 * So we get a dict binding for Num (C d a), which is zonked to give
 743         a = ()
 744   [Note Sept 04: now that we are zonking quantified type variables
 745   on construction, the 'a' will be frozen as a regular tyvar on
 746   quantification, so the floated dict will still have type (C d a).
 747   Which renders this whole note moot; happily!]
 748
 749 * Then the /\a abstraction has a zonked 'a' in it.
 750
 751 All very silly.   I think its harmless to ignore the problem.  We'll end up with
 752 a /\a in the final result but all the occurrences of a will be zonked to ()
 753
 754
 755 %************************************************************************
 756 %*                                                                      *
 757 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
 758 %*                                                                      *
 759 %*              For internal use only!                                  *
 760 %*                                                                      *
 761 %************************************************************************
 762
 763 \begin{code}
 764 -- For unbound, mutable tyvars, zonkType uses the function given to it
 765 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 766 --      type variable and zonks the kind too
 767
 768 zonkType :: (TcTyVar -> TcM Type)       -- What to do with unbound mutable type variables
 769                                         -- see zonkTcType, and zonkTcTypeToType
 770          -> TcType
 771          -> TcM Type
 772 zonkType unbound_var_fn ty
 773   = go ty
 774   where
 775     go (NoteTy _ ty2)    = go ty2       -- Discard free-tyvar annotations
 776
 777     go (TyConApp tc tys) = mappM go tys `thenM` \ tys' ->
 778                            returnM (TyConApp tc tys')
 779
 780     go (PredTy p)        = go_pred p            `thenM` \ p' ->
 781                            returnM (PredTy p')
 782
 783     go (FunTy arg res)   = go arg               `thenM` \ arg' ->
 784                            go res               `thenM` \ res' ->
 785                            returnM (FunTy arg' res')
 786
 787     go (AppTy fun arg)   = go fun               `thenM` \ fun' ->
 788                            go arg               `thenM` \ arg' ->
 789                            returnM (mkAppTy fun' arg')
 790                 -- NB the mkAppTy; we might have instantiated a
 791                 -- type variable to a type constructor, so we need
 792                 -- to pull the TyConApp to the top.
 793
 794         -- The two interesting cases!
 795     go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
 796                        | otherwise       = return (TyVarTy tyvar)
 797                 -- Ordinary (non Tc) tyvars occur inside quantified types
 798
 799     go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
 800                              go ty              `thenM` \ ty' ->
 801                              returnM (ForAllTy tyvar ty')
 802
 803     go_pred (ClassP c tys)   = mappM go tys     `thenM` \ tys' ->
 804                                returnM (ClassP c tys')
 805     go_pred (IParam n ty)    = go ty            `thenM` \ ty' ->
 806                                returnM (IParam n ty')
 807     go_pred (EqPred ty1 ty2) = go ty1           `thenM` \ ty1' ->
 808                                go ty2           `thenM` \ ty2' ->
 809                                returnM (EqPred ty1' ty2')
 810
 811 zonk_tc_tyvar :: (TcTyVar -> TcM Type)          -- What to do for an unbound mutable variable
 812               -> TcTyVar -> TcM TcType
 813 zonk_tc_tyvar unbound_var_fn tyvar
 814   | not (isMetaTyVar tyvar)     -- Skolems
 815   = returnM (TyVarTy tyvar)
 816
 817   | otherwise                   -- Mutables
 818   = do  { cts <- readMetaTyVar tyvar
 819         ; case cts of
 820             Flexi       -> unbound_var_fn tyvar    -- Unbound meta type variable
 821             Indirect ty -> zonkType unbound_var_fn ty  }
 822 \end{code}
 823
 824
 825
 826 %************************************************************************
 827 %*                                                                      *
 828                         Zonking kinds
 829 %*                                                                      *
 830 %************************************************************************
 831
 832 \begin{code}
 833 readKindVar  :: KindVar -> TcM (MetaDetails)
 834 writeKindVar :: KindVar -> TcKind -> TcM ()
 835 readKindVar  kv = readMutVar (kindVarRef kv)
 836 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
 837
 838 -------------
 839 zonkTcKind :: TcKind -> TcM TcKind
 840 zonkTcKind k = zonkTcType k
 841
 842 -------------
 843 zonkTcKindToKind :: TcKind -> TcM Kind
 844 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
 845 -- Haskell specifies that * is to be used, so we follow that.
 846 zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k
 847 \end{code}
 848
 849 %************************************************************************
 850 %*                                                                      *
 851 \subsection{Checking a user type}
 852 %*                                                                      *
 853 %************************************************************************
 854
 855 When dealing with a user-written type, we first translate it from an HsType
 856 to a Type, performing kind checking, and then check various things that should
 857 be true about it.  We don't want to perform these checks at the same time
 858 as the initial translation because (a) they are unnecessary for interface-file
 859 types and (b) when checking a mutually recursive group of type and class decls,
 860 we can't "look" at the tycons/classes yet.  Also, the checks are are rather
 861 diverse, and used to really mess up the other code.
 862
 863 One thing we check for is 'rank'.
 864
 865         Rank 0:         monotypes (no foralls)
 866         Rank 1:         foralls at the front only, Rank 0 inside
 867         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
 868
 869         basic ::= tyvar | T basic ... basic
 870
 871         r2  ::= forall tvs. cxt => r2a
 872         r2a ::= r1 -> r2a | basic
 873         r1  ::= forall tvs. cxt => r0
 874         r0  ::= r0 -> r0 | basic
 875
 876 Another thing is to check that type synonyms are saturated.
 877 This might not necessarily show up in kind checking.
 878         type A i = i
 879         data T k = MkT (k Int)
 880         f :: T A        -- BAD!
 881
 882
 883 \begin{code}
 884 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 885 -- Checks that the type is valid for the given context
 886 checkValidType ctxt ty
 887   = traceTc (text "checkValidType" <+> ppr ty)  `thenM_`
 888     doptM Opt_UnboxedTuples `thenM` \ unboxed ->
 889     doptM Opt_Rank2Types        `thenM` \ rank2 ->
 890     doptM Opt_RankNTypes        `thenM` \ rankn ->
 891     doptM Opt_PolymorphicComponents     `thenM` \ polycomp ->
 892     let
 893         rank | rankn = Arbitrary
 894              | rank2 = Rank 2
 895              | otherwise
 896              = case ctxt of     -- Haskell 98
 897                  GenPatCtxt     -> Rank 0
 898                  LamPatSigCtxt  -> Rank 0
 899                  BindPatSigCtxt -> Rank 0
 900                  DefaultDeclCtxt-> Rank 0
 901                  ResSigCtxt     -> Rank 0
 902                  TySynCtxt _    -> Rank 0
 903                  ExprSigCtxt    -> Rank 1
 904                  FunSigCtxt _   -> Rank 1
 905                  ConArgCtxt _   -> if polycomp
 906                            then Rank 2
 907                                 -- We are given the type of the entire
 908                                 -- constructor, hence rank 1
 909                            else Rank 1
 910                  ForSigCtxt _   -> Rank 1
 911                  SpecInstCtxt   -> Rank 1
 912
 913         actual_kind = typeKind ty
 914
 915         kind_ok = case ctxt of
 916                         TySynCtxt _  -> True    -- Any kind will do
 917                         ResSigCtxt   -> isSubOpenTypeKind        actual_kind
 918                         ExprSigCtxt  -> isSubOpenTypeKind        actual_kind
 919                         GenPatCtxt   -> isLiftedTypeKind actual_kind
 920                         ForSigCtxt _ -> isLiftedTypeKind actual_kind
 921                         other        -> isSubArgTypeKind    actual_kind
 922
 923         ubx_tup = case ctxt of
 924                       TySynCtxt _ | unboxed -> UT_Ok
 925                       ExprSigCtxt | unboxed -> UT_Ok
 926                       _                     -> UT_NotOk
 927     in
 928         -- Check that the thing has kind Type, and is lifted if necessary
 929     checkTc kind_ok (kindErr actual_kind)       `thenM_`
 930
 931         -- Check the internal validity of the type itself
 932     check_poly_type rank ubx_tup ty             `thenM_`
 933
 934     traceTc (text "checkValidType done" <+> ppr ty)
 935 \end{code}
 936
 937
 938 \begin{code}
 939 data Rank = Rank Int | Arbitrary
 940
 941 decRank :: Rank -> Rank
 942 decRank Arbitrary = Arbitrary
 943 decRank (Rank n)  = Rank (n-1)
 944
 945 ----------------------------------------
 946 data UbxTupFlag = UT_Ok | UT_NotOk
 947         -- The "Ok" version means "ok if -fglasgow-exts is on"
 948
 949 ----------------------------------------
 950 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 951 check_poly_type (Rank 0) ubx_tup ty
 952   = check_tau_type (Rank 0) ubx_tup ty
 953
 954 check_poly_type rank ubx_tup ty
 955   | null tvs && null theta
 956   = check_tau_type rank ubx_tup ty
 957   | otherwise
 958   = do  { check_valid_theta SigmaCtxt theta
 959         ; check_poly_type rank ubx_tup tau      -- Allow foralls to right of arrow
 960         ; checkFreeness tvs theta
 961         ; checkAmbiguity tvs theta (tyVarsOfType tau) }
 962   where
 963     (tvs, theta, tau) = tcSplitSigmaTy ty
 964
 965 ----------------------------------------
 966 check_arg_type :: Type -> TcM ()
 967 -- The sort of type that can instantiate a type variable,
 968 -- or be the argument of a type constructor.
 969 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
 970 -- Other unboxed types are very occasionally allowed as type
 971 -- arguments depending on the kind of the type constructor
 972 --
 973 -- For example, we want to reject things like:
 974 --
 975 --      instance Ord a => Ord (forall s. T s a)
 976 -- and
 977 --      g :: T s (forall b.b)
 978 --
 979 -- NB: unboxed tuples can have polymorphic or unboxed args.
 980 --     This happens in the workers for functions returning
 981 --     product types with polymorphic components.
 982 --     But not in user code.
 983 -- Anyway, they are dealt with by a special case in check_tau_type
 984
 985 check_arg_type ty
 986   = check_poly_type Arbitrary UT_NotOk ty       `thenM_`
 987     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 988
 989 ----------------------------------------
 990 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 991 -- Rank is allowed rank for function args
 992 -- No foralls otherwise
 993
 994 check_tau_type rank ubx_tup ty@(ForAllTy _ _)       = failWithTc (forAllTyErr ty)
 995 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
 996         -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
 997
 998 -- Naked PredTys don't usually show up, but they can as a result of
 999 --      {-# SPECIALISE instance Ord Char #-}
1000 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
1001 -- are handled, but the quick thing is just to permit PredTys here.
1002 check_tau_type rank ubx_tup (PredTy sty) = getDOpts             `thenM` \ dflags ->
1003                                            check_pred_ty dflags TypeCtxt sty
1004
1005 check_tau_type rank ubx_tup (TyVarTy _)       = returnM ()
1006 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
1007   = check_poly_type (decRank rank) UT_NotOk arg_ty      `thenM_`
1008     check_poly_type rank           UT_Ok    res_ty
1009
1010 check_tau_type rank ubx_tup (AppTy ty1 ty2)
1011   = check_arg_type ty1 `thenM_` check_arg_type ty2
1012
1013 check_tau_type rank ubx_tup (NoteTy other_note ty)
1014   = check_tau_type rank ubx_tup ty
1015
1016 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
1017   | isSynTyCon tc
1018   = do  {       -- It's OK to have an *over-applied* type synonym
1019                 --      data Tree a b = ...
1020                 --      type Foo a = Tree [a]
1021                 --      f :: Foo a b -> ...
1022         ; case tcView ty of
1023              Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
1024              Nothing -> unless (isOpenTyCon tc           -- No expansion if open
1025                                 && tyConArity tc <= length tys) $
1026                           failWithTc arity_msg
1027
1028         ; ok <- doptM Opt_PartiallyAppliedClosedTypeSynonyms
1029         ; if ok && not (isOpenTyCon tc) then
1030         -- Don't check the type arguments of *closed* synonyms.
1031         -- This allows us to instantiate a synonym defn with a
1032         -- for-all type, or with a partially-applied type synonym.
1033         --      e.g.   type T a b = a
1034         --             type S m   = m ()
1035         --             f :: S (T Int)
1036         -- Here, T is partially applied, so it's illegal in H98.
1037         -- But if you expand S first, then T we get just
1038         --             f :: Int
1039         -- which is fine.
1040                 returnM ()
1041           else
1042                 -- For H98, do check the type args
1043                 mappM_ check_arg_type tys
1044         }
1045
1046   | isUnboxedTupleTyCon tc
1047   = doptM Opt_UnboxedTuples `thenM` \ ub_tuples_allowed ->
1048     checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg  `thenM_`
1049     mappM_ (check_tau_type (Rank 0) UT_Ok) tys
1050                 -- Args are allowed to be unlifted, or
1051                 -- more unboxed tuples, so can't use check_arg_ty
1052
1053   | otherwise
1054   = mappM_ check_arg_type tys
1055
1056   where
1057     ubx_tup_ok ub_tuples_allowed = case ubx_tup of { UT_Ok -> ub_tuples_allowed; other -> False }
1058
1059     n_args    = length tys
1060     tc_arity  = tyConArity tc
1061
1062     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
1063     ubx_tup_msg = ubxArgTyErr ty
1064
1065 ----------------------------------------
1066 forAllTyErr     ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
1067 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
1068 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
1069 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
1070 \end{code}
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 (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
1099 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
1100 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
1101 pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
1102 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
1103 \end{code}
1104
1105 \begin{code}
1106 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
1107 checkValidTheta ctxt theta
1108   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
1109
1110 -------------------------
1111 check_valid_theta ctxt []
1112   = returnM ()
1113 check_valid_theta ctxt theta
1114   = getDOpts                                    `thenM` \ dflags ->
1115     warnTc (notNull dups) (dupPredWarn dups)    `thenM_`
1116     mappM_ (check_pred_ty dflags ctxt) theta
1117   where
1118     (_,dups) = removeDups tcCmpPred theta
1119
1120 -------------------------
1121 check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
1122 check_pred_ty dflags ctxt pred@(ClassP cls tys)
1123   = do {        -- Class predicates are valid in all contexts
1124        ; checkTc (arity == n_tys) arity_err
1125
1126                 -- Check the form of the argument types
1127        ; mappM_ check_arg_type tys
1128        ; checkTc (check_class_pred_tys dflags ctxt tys)
1129                  (predTyVarErr pred $$ how_to_allow)
1130        }
1131   where
1132     class_name = className cls
1133     arity      = classArity cls
1134     n_tys      = length tys
1135     arity_err  = arityErr "Class" class_name arity n_tys
1136     how_to_allow = parens (ptext SLIT("Use -XFlexibleContexts to permit this"))
1137
1138 check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
1139   = do {        -- Equational constraints are valid in all contexts if type
1140                 -- families are permitted
1141        ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
1142
1143                 -- Check the form of the argument types
1144        ; check_eq_arg_type ty1
1145        ; check_eq_arg_type ty2
1146        }
1147   where
1148     check_eq_arg_type = check_poly_type (Rank 0) UT_NotOk
1149
1150 check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
1151         -- Implicit parameters only allowed in type
1152         -- signatures; not in instance decls, superclasses etc
1153         -- The reason for not allowing implicit params in instances is a bit
1154         -- subtle.
1155         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
1156         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
1157         -- discharge all the potential usas of the ?x in e.   For example, a
1158         -- constraint Foo [Int] might come out of e,and applying the
1159         -- instance decl would show up two uses of ?x.
1160
1161 -- Catch-all
1162 check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
1163
1164 -------------------------
1165 check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
1166 check_class_pred_tys dflags ctxt tys
1167   = case ctxt of
1168         TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
1169         InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
1170                                 -- Further checks on head and theta in
1171                                 -- checkInstTermination
1172         other         -> flexible_contexts || all tyvar_head tys
1173   where
1174     flexible_contexts = dopt Opt_FlexibleContexts dflags
1175     undecidable_ok = dopt Opt_UndecidableInstances dflags
1176
1177 -------------------------
1178 tyvar_head ty                   -- Haskell 98 allows predicates of form
1179   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
1180   | otherwise                   -- where a is a type variable
1181   = case tcSplitAppTy_maybe ty of
1182         Just (ty, _) -> tyvar_head ty
1183         Nothing      -> False
1184 \end{code}
1185
1186 Check for ambiguity
1187 ~~~~~~~~~~~~~~~~~~~
1188           forall V. P => tau
1189 is ambiguous if P contains generic variables
1190 (i.e. one of the Vs) that are not mentioned in tau
1191
1192 However, we need to take account of functional dependencies
1193 when we speak of 'mentioned in tau'.  Example:
1194         class C a b | a -> b where ...
1195 Then the type
1196         forall x y. (C x y) => x
1197 is not ambiguous because x is mentioned and x determines y
1198
1199 NB; the ambiguity check is only used for *user* types, not for types
1200 coming from inteface files.  The latter can legitimately have
1201 ambiguous types. Example
1202
1203    class S a where s :: a -> (Int,Int)
1204    instance S Char where s _ = (1,1)
1205    f:: S a => [a] -> Int -> (Int,Int)
1206    f (_::[a]) x = (a*x,b)
1207         where (a,b) = s (undefined::a)
1208
1209 Here the worker for f gets the type
1210         fw :: forall a. S a => Int -> (# Int, Int #)
1211
1212 If the list of tv_names is empty, we have a monotype, and then we
1213 don't need to check for ambiguity either, because the test can't fail
1214 (see is_ambig).
1215
1216
1217 \begin{code}
1218 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1219 checkAmbiguity forall_tyvars theta tau_tyvars
1220   = mappM_ complain (filter is_ambig theta)
1221   where
1222     complain pred     = addErrTc (ambigErr pred)
1223     extended_tau_vars = grow theta tau_tyvars
1224
1225         -- See Note [Implicit parameters and ambiguity] in TcSimplify
1226     is_ambig pred     = isClassPred  pred &&
1227                         any ambig_var (varSetElems (tyVarsOfPred pred))
1228
1229     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
1230                         not (ct_var `elemVarSet` extended_tau_vars)
1231
1232 ambigErr pred
1233   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1234          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1235                  ptext SLIT("must be reachable from the type after the '=>'"))]
1236 \end{code}
1237
1238 In addition, GHC insists that at least one type variable
1239 in each constraint is in V.  So we disallow a type like
1240         forall a. Eq b => b -> b
1241 even in a scope where b is in scope.
1242
1243 \begin{code}
1244 checkFreeness forall_tyvars theta
1245   = do  { flexible_contexts <- doptM Opt_FlexibleContexts
1246         ; unless flexible_contexts $ mappM_ complain (filter is_free theta) }
1247   where
1248     is_free pred     =  not (isIPPred pred)
1249                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1250     bound_var ct_var = ct_var `elem` forall_tyvars
1251     complain pred    = addErrTc (freeErr pred)
1252
1253 freeErr pred
1254   = sep [ ptext SLIT("All of the type variables in the constraint") <+>
1255           quotes (pprPred pred)
1256         , ptext SLIT("are already in scope") <+>
1257           ptext SLIT("(at least one must be universally quantified here)")
1258         , nest 4 $
1259             ptext SLIT("(Use -XFlexibleContexts to lift this restriction)")
1260         ]
1261 \end{code}
1262
1263 \begin{code}
1264 checkThetaCtxt ctxt theta
1265   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1266           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1267
1268 badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1269 eqPredTyErr  sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty
1270                    $$
1271                    parens (ptext SLIT("Use -XTypeFamilies to permit this"))
1272 predTyVarErr pred  = sep [ptext SLIT("Non type-variable argument"),
1273                           nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1274 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1275
1276 arityErr kind name n m
1277   = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1278            n_arguments <> comma, text "but has been given", int m]
1279     where
1280         n_arguments | n == 0 = ptext SLIT("no arguments")
1281                     | n == 1 = ptext SLIT("1 argument")
1282                     | True   = hsep [int n, ptext SLIT("arguments")]
1283
1284 -----------------
1285 notMonoType ty
1286   = do  { ty' <- zonkTcType ty
1287         ; env0 <- tcInitTidyEnv
1288         ; let (env1, tidy_ty) = tidyOpenType env0 ty'
1289               msg = ptext SLIT("Cannot match a monotype with") <+> quotes (ppr tidy_ty)
1290         ; failWithTcM (env1, msg) }
1291
1292 notMonoArgs ty
1293   = do  { ty' <- zonkTcType ty
1294         ; env0 <- tcInitTidyEnv
1295         ; let (env1, tidy_ty) = tidyOpenType env0 ty'
1296               msg = ptext SLIT("Arguments of type synonym families must be monotypes") <+> quotes (ppr tidy_ty)
1297         ; failWithTcM (env1, msg) }
1298 \end{code}
1299
1300
1301 %************************************************************************
1302 %*                                                                      *
1303 \subsection{Checking for a decent instance head type}
1304 %*                                                                      *
1305 %************************************************************************
1306
1307 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1308 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1309
1310 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1311 flag is on, or (2)~the instance is imported (they must have been
1312 compiled elsewhere). In these cases, we let them go through anyway.
1313
1314 We can also have instances for functions: @instance Foo (a -> b) ...@.
1315
1316 \begin{code}
1317 checkValidInstHead :: Type -> TcM (Class, [TcType])
1318
1319 checkValidInstHead ty   -- Should be a source type
1320   = case tcSplitPredTy_maybe ty of {
1321         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1322         Just pred ->
1323
1324     case getClassPredTys_maybe pred of {
1325         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1326         Just (clas,tys) ->
1327
1328     getDOpts                                    `thenM` \ dflags ->
1329     mappM_ check_arg_type tys                   `thenM_`
1330     check_inst_head dflags clas tys             `thenM_`
1331     returnM (clas, tys)
1332     }}
1333
1334 check_inst_head dflags clas tys
1335         -- If GlasgowExts then check at least one isn't a type variable
1336   = do checkTc (dopt Opt_TypeSynonymInstances dflags ||
1337                 all tcInstHeadTyNotSynonym tys)
1338                (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
1339        checkTc (dopt Opt_FlexibleInstances dflags ||
1340                 all tcInstHeadTyAppAllTyVars tys)
1341                (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
1342        checkTc (dopt Opt_MultiParamTypeClasses dflags ||
1343                 isSingleton tys)
1344                (instTypeErr (pprClassPred clas tys) head_one_type_msg)
1345        mapM_ check_one tys
1346   where
1347     head_type_synonym_msg = parens (
1348                 text "All instance types must be of the form (T t1 ... tn)" $$
1349                 text "where T is not a synonym." $$
1350                 text "Use -XTypeSynonymInstances if you want to disable this.")
1351
1352     head_type_args_tyvars_msg = parens (
1353                 text "All instance types must be of the form (T a1 ... an)" $$
1354                 text "where a1 ... an are distinct type *variables*" $$
1355                 text "Use -XFlexibleInstances if you want to disable this.")
1356
1357     head_one_type_msg = parens (
1358                 text "Only one type can be given in an instance head." $$
1359                 text "Use -XMultiParamTypeClasses if you want to allow more.")
1360
1361         -- For now, I only allow tau-types (not polytypes) in
1362         -- the head of an instance decl.
1363         --      E.g.  instance C (forall a. a->a) is rejected
1364         -- One could imagine generalising that, but I'm not sure
1365         -- what all the consequences might be
1366     check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
1367                       ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1368
1369 instTypeErr pp_ty msg
1370   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1371          nest 4 msg]
1372 \end{code}
1373
1374
1375 %************************************************************************
1376 %*                                                                      *
1377 \subsection{Checking instance for termination}
1378 %*                                                                      *
1379 %************************************************************************
1380
1381
1382 \begin{code}
1383 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1384 checkValidInstance tyvars theta clas inst_tys
1385   = do  { undecidable_ok <- doptM Opt_UndecidableInstances
1386
1387         ; checkValidTheta InstThetaCtxt theta
1388         ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1389
1390         -- Check that instance inference will terminate (if we care)
1391         -- For Haskell 98 this will already have been done by checkValidTheta,
1392         -- but as we may be using other extensions we need to check.
1393         ; unless undecidable_ok $
1394           mapM_ addErrTc (checkInstTermination inst_tys theta)
1395
1396         -- The Coverage Condition
1397         ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1398                   (instTypeErr (pprClassPred clas inst_tys) msg)
1399         }
1400   where
1401     msg  = parens (vcat [ptext SLIT("the Coverage Condition fails for one of the functional dependencies;"),
1402                          undecidableMsg])
1403 \end{code}
1404
1405 Termination test: the so-called "Paterson conditions" (see Section 5 of
1406 "Understanding functionsl dependencies via Constraint Handling Rules,
1407 JFP Jan 2007).
1408
1409 We check that each assertion in the context satisfies:
1410  (1) no variable has more occurrences in the assertion than in the head, and
1411  (2) the assertion has fewer constructors and variables (taken together
1412      and counting repetitions) than the head.
1413 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1414 (which have already been checked) guarantee termination.
1415
1416 The underlying idea is that
1417
1418     for any ground substitution, each assertion in the
1419     context has fewer type constructors than the head.
1420
1421
1422 \begin{code}
1423 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1424 checkInstTermination tys theta
1425   = mapCatMaybes check theta
1426   where
1427    fvs  = fvTypes tys
1428    size = sizeTypes tys
1429    check pred
1430       | not (null (fvPred pred \\ fvs))
1431       = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1432       | sizePred pred >= size
1433       = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1434       | otherwise
1435       = Nothing
1436
1437 predUndecErr pred msg = sep [msg,
1438                         nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1439
1440 nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
1441 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
1442 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1443 \end{code}
1444
1445
1446 %************************************************************************
1447 %*                                                                      *
1448         Checking the context of a derived instance declaration
1449 %*                                                                      *
1450 %************************************************************************
1451
1452 Note [Exotic derived instance contexts]
1453 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1454 In a 'derived' instance declaration, we *infer* the context.  It's a
1455 bit unclear what rules we should apply for this; the Haskell report is
1456 silent.  Obviously, constraints like (Eq a) are fine, but what about
1457         data T f a = MkT (f a) deriving( Eq )
1458 where we'd get an Eq (f a) constraint.  That's probably fine too.
1459
1460 One could go further: consider
1461         data T a b c = MkT (Foo a b c) deriving( Eq )
1462         instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
1463
1464 Notice that this instance (just) satisfies the Paterson termination
1465 conditions.  Then we *could* derive an instance decl like this:
1466
1467         instance (C Int a, Eq b, Eq c) => Eq (T a b c)
1468
1469 even though there is no instance for (C Int a), because there just
1470 *might* be an instance for, say, (C Int Bool) at a site where we
1471 need the equality instance for T's.
1472
1473 However, this seems pretty exotic, and it's quite tricky to allow
1474 this, and yet give sensible error messages in the (much more common)
1475 case where we really want that instance decl for C.
1476
1477 So for now we simply require that the derived instance context
1478 should have only type-variable constraints.
1479
1480 Here is another example:
1481         data Fix f = In (f (Fix f)) deriving( Eq )
1482 Here, if we are prepared to allow -fallow-undecidable-instances we
1483 could derive the instance
1484         instance Eq (f (Fix f)) => Eq (Fix f)
1485 but this is so delicate that I don't think it should happen inside
1486 'deriving'. If you want this, write it yourself!
1487
1488 NB: if you want to lift this condition, make sure you still meet the
1489 termination conditions!  If not, the deriving mechanism generates
1490 larger and larger constraints.  Example:
1491   data Succ a = S a
1492   data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
1493
1494 Note the lack of a Show instance for Succ.  First we'll generate
1495   instance (Show (Succ a), Show a) => Show (Seq a)
1496 and then
1497   instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
1498 and so on.  Instead we want to complain of no instance for (Show (Succ a)).
1499
1500 The bottom line
1501 ~~~~~~~~~~~~~~~
1502 Allow constraints which consist only of type variables, with no repeats.
1503
1504 \begin{code}
1505 validDerivPred :: PredType -> Bool
1506 validDerivPred (ClassP cls tys) = hasNoDups fvs && sizeTypes tys == length fvs
1507                                 where fvs = fvTypes tys
1508 validDerivPred otehr            = False
1509 \end{code}
1510
1511 %************************************************************************
1512 %*                                                                      *
1513         Checking type instance well-formedness and termination
1514 %*                                                                      *
1515 %************************************************************************
1516
1517 \begin{code}
1518 -- Check that a "type instance" is well-formed (which includes decidability
1519 -- unless -fallow-undecidable-instances is given).
1520 --
1521 checkValidTypeInst :: [Type] -> Type -> TcM ()
1522 checkValidTypeInst typats rhs
1523   = do { -- left-hand side contains no type family applications
1524          -- (vanilla synonyms are fine, though)
1525        ; mappM_ checkTyFamFreeness typats
1526
1527          -- the right-hand side is a tau type
1528        ; checkTc (isTauTy rhs) $
1529            polyTyErr rhs
1530
1531          -- we have a decidable instance unless otherwise permitted
1532        ; undecidable_ok <- doptM Opt_UndecidableInstances
1533        ; unless undecidable_ok $
1534            mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
1535        }
1536
1537 -- Make sure that each type family instance is
1538 --   (1) strictly smaller than the lhs,
1539 --   (2) mentions no type variable more often than the lhs, and
1540 --   (3) does not contain any further type family instances.
1541 --
1542 checkFamInst :: [Type]                  -- lhs
1543              -> [(TyCon, [Type])]       -- type family instances
1544              -> [Message]
1545 checkFamInst lhsTys famInsts
1546   = mapCatMaybes check famInsts
1547   where
1548    size = sizeTypes lhsTys
1549    fvs  = fvTypes lhsTys
1550    check (tc, tys)
1551       | not (all isTyFamFree tys)
1552       = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1553       | not (null (fvTypes tys \\ fvs))
1554       = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1555       | size <= sizeTypes tys
1556       = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1557       | otherwise
1558       = Nothing
1559       where
1560         famInst = TyConApp tc tys
1561
1562 -- Ensure that no type family instances occur in a type.
1563 --
1564 checkTyFamFreeness :: Type -> TcM ()
1565 checkTyFamFreeness ty
1566   = checkTc (isTyFamFree ty) $
1567       tyFamInstInIndexErr ty
1568
1569 -- Check that a type does not contain any type family applications.
1570 --
1571 isTyFamFree :: Type -> Bool
1572 isTyFamFree = null . tyFamInsts
1573
1574 -- Error messages
1575
1576 tyFamInstInIndexErr ty
1577   = hang (ptext SLIT("Illegal type family application in type instance") <>
1578          colon) 4 $
1579       ppr ty
1580
1581 polyTyErr ty
1582   = hang (ptext SLIT("Illegal polymorphic type in type instance") <> colon) 4 $
1583       ppr ty
1584
1585 famInstUndecErr ty msg
1586   = sep [msg,
1587          nest 2 (ptext SLIT("in the type family application:") <+>
1588                  pprType ty)]
1589
1590 nestedMsg     = ptext SLIT("Nested type family application")
1591 nomoreVarMsg  = ptext SLIT("Variable occurs more often than in instance head")
1592 smallerAppMsg = ptext SLIT("Application is no smaller than the instance head")
1593 \end{code}
1594
1595
1596 %************************************************************************
1597 %*                                                                      *
1598 \subsection{Auxiliary functions}
1599 %*                                                                      *
1600 %************************************************************************
1601
1602 \begin{code}
1603 -- Free variables of a type, retaining repetitions, and expanding synonyms
1604 fvType :: Type -> [TyVar]
1605 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1606 fvType (TyVarTy tv)        = [tv]
1607 fvType (TyConApp _ tys)    = fvTypes tys
1608 fvType (NoteTy _ ty)       = fvType ty
1609 fvType (PredTy pred)       = fvPred pred
1610 fvType (FunTy arg res)     = fvType arg ++ fvType res
1611 fvType (AppTy fun arg)     = fvType fun ++ fvType arg
1612 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1613
1614 fvTypes :: [Type] -> [TyVar]
1615 fvTypes tys                = concat (map fvType tys)
1616
1617 fvPred :: PredType -> [TyVar]
1618 fvPred (ClassP _ tys')     = fvTypes tys'
1619 fvPred (IParam _ ty)       = fvType ty
1620 fvPred (EqPred ty1 ty2)    = fvType ty1 ++ fvType ty2
1621
1622 -- Size of a type: the number of variables and constructors
1623 sizeType :: Type -> Int
1624 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1625 sizeType (TyVarTy _)       = 1
1626 sizeType (TyConApp _ tys)  = sizeTypes tys + 1
1627 sizeType (NoteTy _ ty)     = sizeType ty
1628 sizeType (PredTy pred)     = sizePred pred
1629 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
1630 sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
1631 sizeType (ForAllTy _ ty)   = sizeType ty
1632
1633 sizeTypes :: [Type] -> Int
1634 sizeTypes xs               = sum (map sizeType xs)
1635
1636 sizePred :: PredType -> Int
1637 sizePred (ClassP _ tys')   = sizeTypes tys'
1638 sizePred (IParam _ ty)     = sizeType ty
1639 sizePred (EqPred ty1 ty2)  = sizeType ty1 + sizeType ty2
1640 \end{code}