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