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