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