compiler/typecheck/TcMType.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section{Monadic type operations}
   5
   6 This module contains monadic operations over types that contain mutable type variables
   7
   8 \begin{code}
   9 module TcMType (
  10   TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
  11
  12   --------------------------------
  13   -- Creating new mutable type variables
  14   newFlexiTyVar,
  15   newFlexiTyVarTy,              -- Kind -> TcM TcType
  16   newFlexiTyVarTys,             -- Int -> Kind -> TcM [TcType]
  17   newKindVar, newKindVars,
  18   lookupTcTyVar, LookupTyVarResult(..),
  19   newMetaTyVar, readMetaTyVar, writeMetaTyVar,
  20
  21   --------------------------------
  22   -- Boxy type variables
  23   newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox,
  24
  25   --------------------------------
  26   -- Instantiation
  27   tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
  28   tcInstSigTyVars, zonkSigTyVar,
  29   tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
  30   tcSkolSigType, tcSkolSigTyVars,
  31
  32   --------------------------------
  33   -- Checking type validity
  34   Rank, UserTypeCtxt(..), checkValidType,
  35   SourceTyCtxt(..), checkValidTheta, checkFreeness,
  36   checkValidInstHead, checkValidInstance, checkAmbiguity,
  37   checkInstTermination,
  38   arityErr,
  39
  40   --------------------------------
  41   -- Zonking
  42   zonkType, zonkTcPredType,
  43   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
  44   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
  45   zonkTcKindToKind, zonkTcKind,
  46
  47   readKindVar, writeKindVar
  48
  49   ) where
  50
  51 #include "HsVersions.h"
  52
  53
  54 -- friends:
  55 import TypeRep          ( Type(..), PredType(..),  -- Friend; can see representation
  56                           ThetaType
  57                         )
  58 import TcType           ( TcType, TcThetaType, TcTauType, TcPredType,
  59                           TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..),
  60                           MetaDetails(..), SkolemInfo(..), BoxInfo(..),
  61                           BoxyTyVar, BoxyType, UserTypeCtxt(..),
  62                           isMetaTyVar, isSigTyVar, metaTvRef,
  63                           tcCmpPred, isClassPred, tcGetTyVar,
  64                           tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
  65                           tcValidInstHeadTy, tcSplitForAllTys,
  66                           tcIsTyVarTy, tcSplitSigmaTy,
  67                           isUnLiftedType, isIPPred,
  68                           typeKind, isSkolemTyVar,
  69                           mkAppTy, mkTyVarTy, mkTyVarTys,
  70                           tyVarsOfPred, getClassPredTys_maybe,
  71                           tyVarsOfType, tyVarsOfTypes, tcView,
  72                           pprPred, pprTheta, pprClassPred )
  73 import Kind             ( Kind(..), KindVar, kindVarRef, mkKindVar,
  74                           isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
  75                           liftedTypeKind, defaultKind
  76                         )
  77 import Type             ( TvSubst, zipTopTvSubst, substTy )
  78 import Class            ( Class, classArity, className )
  79 import TyCon            ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
  80                           tyConArity, tyConName )
  81 import Var              ( TyVar, tyVarKind, tyVarName, isTcTyVar,
  82                           mkTyVar, mkTcTyVar, tcTyVarDetails )
  83
  84         -- Assertions
  85 #ifdef DEBUG
  86 import TcType           ( isFlexi, isBoxyTyVar, isImmutableTyVar )
  87 import Kind             ( isSubKind )
  88 #endif
  89
  90 -- others:
  91 import TcRnMonad          -- TcType, amongst others
  92 import FunDeps          ( grow, checkInstCoverage )
  93 import Name             ( Name, setNameUnique, mkSysTvName )
  94 import VarSet
  95 import DynFlags         ( dopt, DynFlag(..) )
  96 import Util             ( nOfThem, isSingleton, notNull )
  97 import ListSetOps       ( removeDups )
  98 import Outputable
  99
 100 import Control.Monad    ( when )
 101 import Data.List        ( (\\) )
 102 \end{code}
 103
 104
 105 %************************************************************************
 106 %*                                                                      *
 107         Instantiation in general
 108 %*                                                                      *
 109 %************************************************************************
 110
 111 \begin{code}
 112 tcInstType :: ([TyVar] -> TcM [TcTyVar])                -- How to instantiate the type variables
 113            -> TcType                                    -- Type to instantiate
 114            -> TcM ([TcTyVar], TcThetaType, TcType)      -- Result
 115 tcInstType inst_tyvars ty
 116   = case tcSplitForAllTys ty of
 117         ([],     rho) -> let    -- There may be overloading despite no type variables;
 118                                 --      (?x :: Int) => Int -> Int
 119                            (theta, tau) = tcSplitPhiTy rho
 120                          in
 121                          return ([], theta, tau)
 122
 123         (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
 124
 125                             ; let  tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
 126                                 -- Either the tyvars are freshly made, by inst_tyvars,
 127                                 -- or (in the call from tcSkolSigType) any nested foralls
 128                                 -- have different binders.  Either way, zipTopTvSubst is ok
 129
 130                             ; let  (theta, tau) = tcSplitPhiTy (substTy tenv rho)
 131                             ; return (tyvars', theta, tau) }
 132 \end{code}
 133
 134
 135 %************************************************************************
 136 %*                                                                      *
 137         Kind variables
 138 %*                                                                      *
 139 %************************************************************************
 140
 141 \begin{code}
 142 newKindVar :: TcM TcKind
 143 newKindVar = do { uniq <- newUnique
 144                 ; ref <- newMutVar Nothing
 145                 ; return (KindVar (mkKindVar uniq ref)) }
 146
 147 newKindVars :: Int -> TcM [TcKind]
 148 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
 149 \end{code}
 150
 151
 152 %************************************************************************
 153 %*                                                                      *
 154         SkolemTvs (immutable)
 155 %*                                                                      *
 156 %************************************************************************
 157
 158 \begin{code}
 159 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
 160 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
 161
 162 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
 163 -- Instantiate a type signature with skolem constants, but
 164 -- do *not* give them fresh names, because we want the name to
 165 -- be in the type environment -- it is lexically scoped.
 166 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
 167
 168 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
 169 -- Make skolem constants, but do *not* give them new names, as above
 170 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
 171                               | tv <- tyvars ]
 172
 173 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
 174 -- Instantiate a type with fresh skolem constants
 175 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
 176
 177 tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
 178 tcInstSkolTyVar info tyvar
 179   = do  { uniq <- newUnique
 180         ; let name = setNameUnique (tyVarName tyvar) uniq
 181               kind = tyVarKind tyvar
 182         ; return (mkSkolTyVar name kind info) }
 183
 184 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
 185 tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars
 186 \end{code}
 187
 188
 189 %************************************************************************
 190 %*                                                                      *
 191         MetaTvs (meta type variables; mutable)
 192 %*                                                                      *
 193 %************************************************************************
 194
 195 \begin{code}
 196 newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
 197 -- Make a new meta tyvar out of thin air
 198 newMetaTyVar box_info kind
 199   = do  { uniq <- newUnique
 200         ; ref <- newMutVar Flexi ;
 201         ; let name = mkSysTvName uniq fs
 202               fs = case box_info of
 203                         BoxTv   -> FSLIT("bx")
 204                         TauTv   -> FSLIT("t")
 205                         SigTv _ -> FSLIT("a")
 206         ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
 207
 208 instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
 209 -- Make a new meta tyvar whose Name and Kind
 210 -- come from an existing TyVar
 211 instMetaTyVar box_info tyvar
 212   = do  { uniq <- newUnique
 213         ; ref <- newMutVar Flexi ;
 214         ; let name = setNameUnique (tyVarName tyvar) uniq
 215               kind = tyVarKind tyvar
 216         ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
 217
 218 readMetaTyVar :: TyVar -> TcM MetaDetails
 219 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
 220                       readMutVar (metaTvRef tyvar)
 221
 222 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
 223 #ifndef DEBUG
 224 writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
 225 #else
 226 writeMetaTyVar tyvar ty
 227   | not (isMetaTyVar tyvar)
 228   = pprTrace "writeMetaTyVar" (ppr tyvar) $
 229     returnM ()
 230
 231   | otherwise
 232   = ASSERT( isMetaTyVar tyvar )
 233     ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
 234     do  { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
 235         ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
 236   where
 237     k1 = tyVarKind tyvar
 238     k2 = typeKind ty
 239 #endif
 240 \end{code}
 241
 242
 243 %************************************************************************
 244 %*                                                                      *
 245         MetaTvs: TauTvs
 246 %*                                                                      *
 247 %************************************************************************
 248
 249 \begin{code}
 250 newFlexiTyVar :: Kind -> TcM TcTyVar
 251 newFlexiTyVar kind = newMetaTyVar TauTv kind
 252
 253 newFlexiTyVarTy  :: Kind -> TcM TcType
 254 newFlexiTyVarTy kind
 255   = newFlexiTyVar kind  `thenM` \ tc_tyvar ->
 256     returnM (TyVarTy tc_tyvar)
 257
 258 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
 259 newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind)
 260
 261 tcInstTyVar :: TyVar -> TcM TcTyVar
 262 -- Instantiate with a META type variable
 263 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
 264
 265 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
 266 -- Instantiate with META type variables
 267 tcInstTyVars tyvars
 268   = do  { tc_tvs <- mapM tcInstTyVar tyvars
 269         ; let tys = mkTyVarTys tc_tvs
 270         ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
 271                 -- Since the tyvars are freshly made,
 272                 -- they cannot possibly be captured by
 273                 -- any existing for-alls.  Hence zipTopTvSubst
 274 \end{code}
 275
 276
 277 %************************************************************************
 278 %*                                                                      *
 279         MetaTvs: SigTvs
 280 %*                                                                      *
 281 %************************************************************************
 282
 283 \begin{code}
 284 tcInstSigTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
 285 -- Instantiate with meta SigTvs
 286 tcInstSigTyVars skol_info tyvars
 287   = mapM (instMetaTyVar (SigTv skol_info)) tyvars
 288
 289 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
 290 zonkSigTyVar sig_tv
 291   | isSkolemTyVar sig_tv
 292   = return sig_tv       -- Happens in the call in TcBinds.checkDistinctTyVars
 293   | otherwise
 294   = ASSERT( isSigTyVar sig_tv )
 295     do { ty <- zonkTcTyVar sig_tv
 296        ; return (tcGetTyVar "zonkSigTyVar" ty) }
 297         -- 'ty' is bound to be a type variable, because SigTvs
 298         -- can only be unified with type variables
 299 \end{code}
 300
 301
 302 %************************************************************************
 303 %*                                                                      *
 304         MetaTvs: BoxTvs
 305 %*                                                                      *
 306 %************************************************************************
 307
 308 \begin{code}
 309 newBoxyTyVar :: Kind -> TcM BoxyTyVar
 310 newBoxyTyVar kind = newMetaTyVar BoxTv kind
 311
 312 newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
 313 newBoxyTyVars kinds = mapM newBoxyTyVar kinds
 314
 315 newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
 316 newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
 317
 318 readFilledBox :: BoxyTyVar -> TcM TcType
 319 -- Read the contents of the box, which should be filled in by now
 320 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
 321                        do { cts <- readMetaTyVar box_tv
 322                           ; case cts of
 323                                 Flexi       -> pprPanic "readFilledBox" (ppr box_tv)
 324                                 Indirect ty -> return ty }
 325
 326 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
 327 -- Instantiate with a BOXY type variable
 328 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
 329 \end{code}
 330
 331
 332 %************************************************************************
 333 %*                                                                      *
 334 \subsection{Putting and getting  mutable type variables}
 335 %*                                                                      *
 336 %************************************************************************
 337
 338 But it's more fun to short out indirections on the way: If this
 339 version returns a TyVar, then that TyVar is unbound.  If it returns
 340 any other type, then there might be bound TyVars embedded inside it.
 341
 342 We return Nothing iff the original box was unbound.
 343
 344 \begin{code}
 345 data LookupTyVarResult  -- The result of a lookupTcTyVar call
 346   = DoneTv TcTyVarDetails       -- SkolemTv or virgin MetaTv
 347   | IndirectTv TcType
 348
 349 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
 350 lookupTcTyVar tyvar
 351   = case details of
 352       SkolemTv _   -> return (DoneTv details)
 353       MetaTv _ ref -> do { meta_details <- readMutVar ref
 354                          ; case meta_details of
 355                             Indirect ty -> return (IndirectTv ty)
 356                             Flexi       -> return (DoneTv details) }
 357   where
 358     details =  tcTyVarDetails tyvar
 359
 360 {-
 361 -- gaw 2004 We aren't shorting anything out anymore, at least for now
 362 getTcTyVar tyvar
 363   | not (isTcTyVar tyvar)
 364   = pprTrace "getTcTyVar" (ppr tyvar) $
 365     returnM (Just (mkTyVarTy tyvar))
 366
 367   | otherwise
 368   = ASSERT2( isTcTyVar tyvar, ppr tyvar )
 369     readMetaTyVar tyvar                         `thenM` \ maybe_ty ->
 370     case maybe_ty of
 371         Just ty -> short_out ty                         `thenM` \ ty' ->
 372                    writeMetaTyVar tyvar (Just ty')      `thenM_`
 373                    returnM (Just ty')
 374
 375         Nothing    -> returnM Nothing
 376
 377 short_out :: TcType -> TcM TcType
 378 short_out ty@(TyVarTy tyvar)
 379   | not (isTcTyVar tyvar)
 380   = returnM ty
 381
 382   | otherwise
 383   = readMetaTyVar tyvar `thenM` \ maybe_ty ->
 384     case maybe_ty of
 385         Just ty' -> short_out ty'                       `thenM` \ ty' ->
 386                     writeMetaTyVar tyvar (Just ty')     `thenM_`
 387                     returnM ty'
 388
 389         other    -> returnM ty
 390
 391 short_out other_ty = returnM other_ty
 392 -}
 393 \end{code}
 394
 395
 396 %************************************************************************
 397 %*                                                                      *
 398 \subsection{Zonking -- the exernal interfaces}
 399 %*                                                                      *
 400 %************************************************************************
 401
 402 -----------------  Type variables
 403
 404 \begin{code}
 405 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
 406 zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
 407
 408 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
 409 zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars     `thenM` \ tys ->
 410                            returnM (tyVarsOfTypes tys)
 411
 412 zonkTcTyVar :: TcTyVar -> TcM TcType
 413 zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
 414                     zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
 415 \end{code}
 416
 417 -----------------  Types
 418
 419 \begin{code}
 420 zonkTcType :: TcType -> TcM TcType
 421 zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
 422
 423 zonkTcTypes :: [TcType] -> TcM [TcType]
 424 zonkTcTypes tys = mappM zonkTcType tys
 425
 426 zonkTcClassConstraints cts = mappM zonk cts
 427     where zonk (clas, tys)
 428             = zonkTcTypes tys   `thenM` \ new_tys ->
 429               returnM (clas, new_tys)
 430
 431 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
 432 zonkTcThetaType theta = mappM zonkTcPredType theta
 433
 434 zonkTcPredType :: TcPredType -> TcM TcPredType
 435 zonkTcPredType (ClassP c ts)
 436   = zonkTcTypes ts      `thenM` \ new_ts ->
 437     returnM (ClassP c new_ts)
 438 zonkTcPredType (IParam n t)
 439   = zonkTcType t        `thenM` \ new_t ->
 440     returnM (IParam n new_t)
 441 \end{code}
 442
 443 -------------------  These ...ToType, ...ToKind versions
 444                      are used at the end of type checking
 445
 446 \begin{code}
 447 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
 448 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
 449 -- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
 450 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
 451 -- The meta tyvar is updated to point to the new regular TyVar.  Now any
 452 -- bound occurences of the original type variable will get zonked to
 453 -- the immutable version.
 454 --
 455 -- We leave skolem TyVars alone; they are immutable.
 456 zonkQuantifiedTyVar tv
 457   | isSkolemTyVar tv = return tv
 458         -- It might be a skolem type variable,
 459         -- for example from a user type signature
 460
 461   | otherwise   -- It's a meta-type-variable
 462   = do  { details <- readMetaTyVar tv
 463
 464         -- Create the new, frozen, regular type variable
 465         ; let final_kind = defaultKind (tyVarKind tv)
 466               final_tv   = mkTyVar (tyVarName tv) final_kind
 467
 468         -- Bind the meta tyvar to the new tyvar
 469         ; case details of
 470             Indirect ty -> WARN( True, ppr tv $$ ppr ty )
 471                            return ()
 472                 -- [Sept 04] I don't think this should happen
 473                 -- See note [Silly Type Synonym]
 474
 475             Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
 476
 477         -- Return the new tyvar
 478         ; return final_tv }
 479 \end{code}
 480
 481 [Silly Type Synonyms]
 482
 483 Consider this:
 484         type C u a = u  -- Note 'a' unused
 485
 486         foo :: (forall a. C u a -> C u a) -> u
 487         foo x = ...
 488
 489         bar :: Num u => u
 490         bar = foo (\t -> t + t)
 491
 492 * From the (\t -> t+t) we get type  {Num d} =>  d -> d
 493   where d is fresh.
 494
 495 * Now unify with type of foo's arg, and we get:
 496         {Num (C d a)} =>  C d a -> C d a
 497   where a is fresh.
 498
 499 * Now abstract over the 'a', but float out the Num (C d a) constraint
 500   because it does not 'really' mention a.  (see exactTyVarsOfType)
 501   The arg to foo becomes
 502         /\a -> \t -> t+t
 503
 504 * So we get a dict binding for Num (C d a), which is zonked to give
 505         a = ()
 506   [Note Sept 04: now that we are zonking quantified type variables
 507   on construction, the 'a' will be frozen as a regular tyvar on
 508   quantification, so the floated dict will still have type (C d a).
 509   Which renders this whole note moot; happily!]
 510
 511 * Then the /\a abstraction has a zonked 'a' in it.
 512
 513 All very silly.   I think its harmless to ignore the problem.  We'll end up with
 514 a /\a in the final result but all the occurrences of a will be zonked to ()
 515
 516
 517 %************************************************************************
 518 %*                                                                      *
 519 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
 520 %*                                                                      *
 521 %*              For internal use only!                                  *
 522 %*                                                                      *
 523 %************************************************************************
 524
 525 \begin{code}
 526 -- For unbound, mutable tyvars, zonkType uses the function given to it
 527 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 528 --      type variable and zonks the kind too
 529
 530 zonkType :: (TcTyVar -> TcM Type)       -- What to do with unbound mutable type variables
 531                                         -- see zonkTcType, and zonkTcTypeToType
 532          -> TcType
 533          -> TcM Type
 534 zonkType unbound_var_fn ty
 535   = go ty
 536   where
 537     go (NoteTy _ ty2)    = go ty2       -- Discard free-tyvar annotations
 538
 539     go (TyConApp tc tys) = mappM go tys `thenM` \ tys' ->
 540                            returnM (TyConApp tc tys')
 541
 542     go (PredTy p)        = go_pred p            `thenM` \ p' ->
 543                            returnM (PredTy p')
 544
 545     go (FunTy arg res)   = go arg               `thenM` \ arg' ->
 546                            go res               `thenM` \ res' ->
 547                            returnM (FunTy arg' res')
 548
 549     go (AppTy fun arg)   = go fun               `thenM` \ fun' ->
 550                            go arg               `thenM` \ arg' ->
 551                            returnM (mkAppTy fun' arg')
 552                 -- NB the mkAppTy; we might have instantiated a
 553                 -- type variable to a type constructor, so we need
 554                 -- to pull the TyConApp to the top.
 555
 556         -- The two interesting cases!
 557     go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
 558                        | otherwise       = return (TyVarTy tyvar)
 559                 -- Ordinary (non Tc) tyvars occur inside quantified types
 560
 561     go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
 562                              go ty              `thenM` \ ty' ->
 563                              returnM (ForAllTy tyvar ty')
 564
 565     go_pred (ClassP c tys) = mappM go tys       `thenM` \ tys' ->
 566                              returnM (ClassP c tys')
 567     go_pred (IParam n ty)  = go ty              `thenM` \ ty' ->
 568                              returnM (IParam n ty')
 569
 570 zonk_tc_tyvar :: (TcTyVar -> TcM Type)          -- What to do for an unbound mutable variable
 571               -> TcTyVar -> TcM TcType
 572 zonk_tc_tyvar unbound_var_fn tyvar
 573   | not (isMetaTyVar tyvar)     -- Skolems
 574   = returnM (TyVarTy tyvar)
 575
 576   | otherwise                   -- Mutables
 577   = do  { cts <- readMetaTyVar tyvar
 578         ; case cts of
 579             Flexi       -> unbound_var_fn tyvar    -- Unbound meta type variable
 580             Indirect ty -> zonkType unbound_var_fn ty  }
 581 \end{code}
 582
 583
 584
 585 %************************************************************************
 586 %*                                                                      *
 587                         Zonking kinds
 588 %*                                                                      *
 589 %************************************************************************
 590
 591 \begin{code}
 592 readKindVar  :: KindVar -> TcM (Maybe TcKind)
 593 writeKindVar :: KindVar -> TcKind -> TcM ()
 594 readKindVar  kv = readMutVar (kindVarRef kv)
 595 writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
 596
 597 -------------
 598 zonkTcKind :: TcKind -> TcM TcKind
 599 zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
 600                                 ; k2' <- zonkTcKind k2
 601                                 ; returnM (FunKind k1' k2') }
 602 zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv
 603                                ; case mb_kind of
 604                                     Nothing -> returnM k
 605                                     Just k  -> zonkTcKind k }
 606 zonkTcKind other_kind = returnM other_kind
 607
 608 -------------
 609 zonkTcKindToKind :: TcKind -> TcM Kind
 610 zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
 611                                       ; k2' <- zonkTcKindToKind k2
 612                                       ; returnM (FunKind k1' k2') }
 613
 614 zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv
 615                                    ; case mb_kind of
 616                                        Nothing -> return liftedTypeKind
 617                                        Just k  -> zonkTcKindToKind k }
 618
 619 zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind  -- An "Open" kind defaults to *
 620 zonkTcKindToKind other_kind   = returnM other_kind
 621 \end{code}
 622
 623 %************************************************************************
 624 %*                                                                      *
 625 \subsection{Checking a user type}
 626 %*                                                                      *
 627 %************************************************************************
 628
 629 When dealing with a user-written type, we first translate it from an HsType
 630 to a Type, performing kind checking, and then check various things that should
 631 be true about it.  We don't want to perform these checks at the same time
 632 as the initial translation because (a) they are unnecessary for interface-file
 633 types and (b) when checking a mutually recursive group of type and class decls,
 634 we can't "look" at the tycons/classes yet.  Also, the checks are are rather
 635 diverse, and used to really mess up the other code.
 636
 637 One thing we check for is 'rank'.
 638
 639         Rank 0:         monotypes (no foralls)
 640         Rank 1:         foralls at the front only, Rank 0 inside
 641         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
 642
 643         basic ::= tyvar | T basic ... basic
 644
 645         r2  ::= forall tvs. cxt => r2a
 646         r2a ::= r1 -> r2a | basic
 647         r1  ::= forall tvs. cxt => r0
 648         r0  ::= r0 -> r0 | basic
 649
 650 Another thing is to check that type synonyms are saturated.
 651 This might not necessarily show up in kind checking.
 652         type A i = i
 653         data T k = MkT (k Int)
 654         f :: T A        -- BAD!
 655
 656
 657 \begin{code}
 658 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 659 -- Checks that the type is valid for the given context
 660 checkValidType ctxt ty
 661   = traceTc (text "checkValidType" <+> ppr ty)  `thenM_`
 662     doptM Opt_GlasgowExts       `thenM` \ gla_exts ->
 663     let
 664         rank | gla_exts = Arbitrary
 665              | otherwise
 666              = case ctxt of     -- Haskell 98
 667                  GenPatCtxt     -> Rank 0
 668                  LamPatSigCtxt  -> Rank 0
 669                  BindPatSigCtxt -> Rank 0
 670                  DefaultDeclCtxt-> Rank 0
 671                  ResSigCtxt     -> Rank 0
 672                  TySynCtxt _    -> Rank 0
 673                  ExprSigCtxt    -> Rank 1
 674                  FunSigCtxt _   -> Rank 1
 675                  ConArgCtxt _   -> Rank 1       -- We are given the type of the entire
 676                                                 -- constructor, hence rank 1
 677                  ForSigCtxt _   -> Rank 1
 678                  RuleSigCtxt _  -> Rank 1
 679                  SpecInstCtxt   -> Rank 1
 680
 681         actual_kind = typeKind ty
 682
 683         kind_ok = case ctxt of
 684                         TySynCtxt _  -> True    -- Any kind will do
 685                         ResSigCtxt   -> isOpenTypeKind   actual_kind
 686                         ExprSigCtxt  -> isOpenTypeKind   actual_kind
 687                         GenPatCtxt   -> isLiftedTypeKind actual_kind
 688                         ForSigCtxt _ -> isLiftedTypeKind actual_kind
 689                         other        -> isArgTypeKind    actual_kind
 690
 691         ubx_tup | not gla_exts = UT_NotOk
 692                 | otherwise    = case ctxt of
 693                                    TySynCtxt _ -> UT_Ok
 694                                    ExprSigCtxt -> UT_Ok
 695                                    other       -> UT_NotOk
 696                 -- Unboxed tuples ok in function results,
 697                 -- but for type synonyms we allow them even at
 698                 -- top level
 699     in
 700         -- Check that the thing has kind Type, and is lifted if necessary
 701     checkTc kind_ok (kindErr actual_kind)       `thenM_`
 702
 703         -- Check the internal validity of the type itself
 704     check_poly_type rank ubx_tup ty             `thenM_`
 705
 706     traceTc (text "checkValidType done" <+> ppr ty)
 707 \end{code}
 708
 709
 710 \begin{code}
 711 data Rank = Rank Int | Arbitrary
 712
 713 decRank :: Rank -> Rank
 714 decRank Arbitrary = Arbitrary
 715 decRank (Rank n)  = Rank (n-1)
 716
 717 ----------------------------------------
 718 data UbxTupFlag = UT_Ok | UT_NotOk
 719         -- The "Ok" version means "ok if -fglasgow-exts is on"
 720
 721 ----------------------------------------
 722 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 723 check_poly_type (Rank 0) ubx_tup ty
 724   = check_tau_type (Rank 0) ubx_tup ty
 725
 726 check_poly_type rank ubx_tup ty
 727   | null tvs && null theta
 728   = check_tau_type rank ubx_tup ty
 729   | otherwise
 730   = do  { check_valid_theta SigmaCtxt theta
 731         ; check_poly_type rank ubx_tup tau      -- Allow foralls to right of arrow
 732         ; checkFreeness tvs theta
 733         ; checkAmbiguity tvs theta (tyVarsOfType tau) }
 734   where
 735     (tvs, theta, tau) = tcSplitSigmaTy ty
 736
 737 ----------------------------------------
 738 check_arg_type :: Type -> TcM ()
 739 -- The sort of type that can instantiate a type variable,
 740 -- or be the argument of a type constructor.
 741 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
 742 -- Other unboxed types are very occasionally allowed as type
 743 -- arguments depending on the kind of the type constructor
 744 --
 745 -- For example, we want to reject things like:
 746 --
 747 --      instance Ord a => Ord (forall s. T s a)
 748 -- and
 749 --      g :: T s (forall b.b)
 750 --
 751 -- NB: unboxed tuples can have polymorphic or unboxed args.
 752 --     This happens in the workers for functions returning
 753 --     product types with polymorphic components.
 754 --     But not in user code.
 755 -- Anyway, they are dealt with by a special case in check_tau_type
 756
 757 check_arg_type ty
 758   = check_poly_type Arbitrary UT_NotOk ty       `thenM_`
 759     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 760
 761 ----------------------------------------
 762 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 763 -- Rank is allowed rank for function args
 764 -- No foralls otherwise
 765
 766 check_tau_type rank ubx_tup ty@(ForAllTy _ _)       = failWithTc (forAllTyErr ty)
 767 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
 768         -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
 769
 770 -- Naked PredTys don't usually show up, but they can as a result of
 771 --      {-# SPECIALISE instance Ord Char #-}
 772 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
 773 -- are handled, but the quick thing is just to permit PredTys here.
 774 check_tau_type rank ubx_tup (PredTy sty) = getDOpts             `thenM` \ dflags ->
 775                                            check_source_ty dflags TypeCtxt sty
 776
 777 check_tau_type rank ubx_tup (TyVarTy _)       = returnM ()
 778 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
 779   = check_poly_type (decRank rank) UT_NotOk arg_ty      `thenM_`
 780     check_poly_type rank           UT_Ok    res_ty
 781
 782 check_tau_type rank ubx_tup (AppTy ty1 ty2)
 783   = check_arg_type ty1 `thenM_` check_arg_type ty2
 784
 785 check_tau_type rank ubx_tup (NoteTy other_note ty)
 786   = check_tau_type rank ubx_tup ty
 787
 788 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
 789   | isSynTyCon tc
 790   = do  {       -- It's OK to have an *over-applied* type synonym
 791                 --      data Tree a b = ...
 792                 --      type Foo a = Tree [a]
 793                 --      f :: Foo a b -> ...
 794         ; case tcView ty of
 795              Just ty' -> check_tau_type rank ubx_tup ty'        -- Check expansion
 796              Nothing  -> failWithTc arity_msg
 797
 798         ; gla_exts <- doptM Opt_GlasgowExts
 799         ; if gla_exts then
 800         -- If -fglasgow-exts then don't check the type arguments
 801         -- This allows us to instantiate a synonym defn with a
 802         -- for-all type, or with a partially-applied type synonym.
 803         --      e.g.   type T a b = a
 804         --             type S m   = m ()
 805         --             f :: S (T Int)
 806         -- Here, T is partially applied, so it's illegal in H98.
 807         -- But if you expand S first, then T we get just
 808         --             f :: Int
 809         -- which is fine.
 810                 returnM ()
 811           else
 812                 -- For H98, do check the type args
 813                 mappM_ check_arg_type tys
 814         }
 815
 816   | isUnboxedTupleTyCon tc
 817   = doptM Opt_GlasgowExts                       `thenM` \ gla_exts ->
 818     checkTc (ubx_tup_ok gla_exts) ubx_tup_msg   `thenM_`
 819     mappM_ (check_tau_type (Rank 0) UT_Ok) tys
 820                 -- Args are allowed to be unlifted, or
 821                 -- more unboxed tuples, so can't use check_arg_ty
 822
 823   | otherwise
 824   = mappM_ check_arg_type tys
 825
 826   where
 827     ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
 828
 829     n_args    = length tys
 830     tc_arity  = tyConArity tc
 831
 832     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
 833     ubx_tup_msg = ubxArgTyErr ty
 834
 835 ----------------------------------------
 836 forAllTyErr     ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
 837 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
 838 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
 839 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 840 \end{code}
 841
 842
 843
 844 %************************************************************************
 845 %*                                                                      *
 846 \subsection{Checking a theta or source type}
 847 %*                                                                      *
 848 %************************************************************************
 849
 850 \begin{code}
 851 -- Enumerate the contexts in which a "source type", <S>, can occur
 852 --      Eq a
 853 -- or   ?x::Int
 854 -- or   r <: {x::Int}
 855 -- or   (N a) where N is a newtype
 856
 857 data SourceTyCtxt
 858   = ClassSCCtxt Name    -- Superclasses of clas
 859                         --      class <S> => C a where ...
 860   | SigmaCtxt           -- Theta part of a normal for-all type
 861                         --      f :: <S> => a -> a
 862   | DataTyCtxt Name     -- Theta part of a data decl
 863                         --      data <S> => T a = MkT a
 864   | TypeCtxt            -- Source type in an ordinary type
 865                         --      f :: N a -> N a
 866   | InstThetaCtxt       -- Context of an instance decl
 867                         --      instance <S> => C [a] where ...
 868
 869 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
 870 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
 871 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
 872 pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
 873 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
 874 \end{code}
 875
 876 \begin{code}
 877 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
 878 checkValidTheta ctxt theta
 879   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
 880
 881 -------------------------
 882 check_valid_theta ctxt []
 883   = returnM ()
 884 check_valid_theta ctxt theta
 885   = getDOpts                                    `thenM` \ dflags ->
 886     warnTc (notNull dups) (dupPredWarn dups)    `thenM_`
 887     mappM_ (check_source_ty dflags ctxt) theta
 888   where
 889     (_,dups) = removeDups tcCmpPred theta
 890
 891 -------------------------
 892 check_source_ty dflags ctxt pred@(ClassP cls tys)
 893   =     -- Class predicates are valid in all contexts
 894     checkTc (arity == n_tys) arity_err          `thenM_`
 895
 896         -- Check the form of the argument types
 897     mappM_ check_arg_type tys                           `thenM_`
 898     checkTc (check_class_pred_tys dflags ctxt tys)
 899             (predTyVarErr pred $$ how_to_allow)
 900
 901   where
 902     class_name = className cls
 903     arity      = classArity cls
 904     n_tys      = length tys
 905     arity_err  = arityErr "Class" class_name arity n_tys
 906     how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 907
 908 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
 909         -- Implicit parameters only allows in type
 910         -- signatures; not in instance decls, superclasses etc
 911         -- The reason for not allowing implicit params in instances is a bit subtle
 912         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
 913         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
 914         -- discharge all the potential usas of the ?x in e.   For example, a
 915         -- constraint Foo [Int] might come out of e,and applying the
 916         -- instance decl would show up two uses of ?x.
 917
 918 -- Catch-all
 919 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 920
 921 -------------------------
 922 check_class_pred_tys dflags ctxt tys
 923   = case ctxt of
 924         TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
 925         InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys
 926                                 -- Further checks on head and theta in
 927                                 -- checkInstTermination
 928         other         -> gla_exts || all tyvar_head tys
 929   where
 930     gla_exts       = dopt Opt_GlasgowExts dflags
 931     undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
 932
 933 -------------------------
 934 tyvar_head ty                   -- Haskell 98 allows predicates of form
 935   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
 936   | otherwise                   -- where a is a type variable
 937   = case tcSplitAppTy_maybe ty of
 938         Just (ty, _) -> tyvar_head ty
 939         Nothing      -> False
 940 \end{code}
 941
 942 Check for ambiguity
 943 ~~~~~~~~~~~~~~~~~~~
 944           forall V. P => tau
 945 is ambiguous if P contains generic variables
 946 (i.e. one of the Vs) that are not mentioned in tau
 947
 948 However, we need to take account of functional dependencies
 949 when we speak of 'mentioned in tau'.  Example:
 950         class C a b | a -> b where ...
 951 Then the type
 952         forall x y. (C x y) => x
 953 is not ambiguous because x is mentioned and x determines y
 954
 955 NB; the ambiguity check is only used for *user* types, not for types
 956 coming from inteface files.  The latter can legitimately have
 957 ambiguous types. Example
 958
 959    class S a where s :: a -> (Int,Int)
 960    instance S Char where s _ = (1,1)
 961    f:: S a => [a] -> Int -> (Int,Int)
 962    f (_::[a]) x = (a*x,b)
 963         where (a,b) = s (undefined::a)
 964
 965 Here the worker for f gets the type
 966         fw :: forall a. S a => Int -> (# Int, Int #)
 967
 968 If the list of tv_names is empty, we have a monotype, and then we
 969 don't need to check for ambiguity either, because the test can't fail
 970 (see is_ambig).
 971
 972 \begin{code}
 973 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
 974 checkAmbiguity forall_tyvars theta tau_tyvars
 975   = mappM_ complain (filter is_ambig theta)
 976   where
 977     complain pred     = addErrTc (ambigErr pred)
 978     extended_tau_vars = grow theta tau_tyvars
 979
 980         -- Only a *class* predicate can give rise to ambiguity
 981         -- An *implicit parameter* cannot.  For example:
 982         --      foo :: (?x :: [a]) => Int
 983         --      foo = length ?x
 984         -- is fine.  The call site will suppply a particular 'x'
 985     is_ambig pred     = isClassPred  pred &&
 986                         any ambig_var (varSetElems (tyVarsOfPred pred))
 987
 988     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
 989                         not (ct_var `elemVarSet` extended_tau_vars)
 990
 991 ambigErr pred
 992   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
 993          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
 994                  ptext SLIT("must be reachable from the type after the '=>'"))]
 995 \end{code}
 996
 997 In addition, GHC insists that at least one type variable
 998 in each constraint is in V.  So we disallow a type like
 999         forall a. Eq b => b -> b
1000 even in a scope where b is in scope.
1001
1002 \begin{code}
1003 checkFreeness forall_tyvars theta
1004   = mappM_ complain (filter is_free theta)
1005   where
1006     is_free pred     =  not (isIPPred pred)
1007                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1008     bound_var ct_var = ct_var `elem` forall_tyvars
1009     complain pred    = addErrTc (freeErr pred)
1010
1011 freeErr pred
1012   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1013                    ptext SLIT("are already in scope"),
1014          nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1015     ]
1016 \end{code}
1017
1018 \begin{code}
1019 checkThetaCtxt ctxt theta
1020   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1021           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1022
1023 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1024 predTyVarErr pred  = sep [ptext SLIT("Non type-variable argument"),
1025                           nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1026 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1027
1028 arityErr kind name n m
1029   = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1030            n_arguments <> comma, text "but has been given", int m]
1031     where
1032         n_arguments | n == 0 = ptext SLIT("no arguments")
1033                     | n == 1 = ptext SLIT("1 argument")
1034                     | True   = hsep [int n, ptext SLIT("arguments")]
1035 \end{code}
1036
1037
1038 %************************************************************************
1039 %*                                                                      *
1040 \subsection{Checking for a decent instance head type}
1041 %*                                                                      *
1042 %************************************************************************
1043
1044 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1045 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1046
1047 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1048 flag is on, or (2)~the instance is imported (they must have been
1049 compiled elsewhere). In these cases, we let them go through anyway.
1050
1051 We can also have instances for functions: @instance Foo (a -> b) ...@.
1052
1053 \begin{code}
1054 checkValidInstHead :: Type -> TcM (Class, [TcType])
1055
1056 checkValidInstHead ty   -- Should be a source type
1057   = case tcSplitPredTy_maybe ty of {
1058         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1059         Just pred ->
1060
1061     case getClassPredTys_maybe pred of {
1062         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1063         Just (clas,tys) ->
1064
1065     getDOpts                                    `thenM` \ dflags ->
1066     mappM_ check_arg_type tys                   `thenM_`
1067     check_inst_head dflags clas tys             `thenM_`
1068     returnM (clas, tys)
1069     }}
1070
1071 check_inst_head dflags clas tys
1072         -- If GlasgowExts then check at least one isn't a type variable
1073   | dopt Opt_GlasgowExts dflags
1074   = mapM_ check_one tys
1075
1076         -- WITH HASKELL 98, MUST HAVE C (T a b c)
1077   | otherwise
1078   = checkTc (isSingleton tys && tcValidInstHeadTy first_ty)
1079             (instTypeErr (pprClassPred clas tys) head_shape_msg)
1080
1081   where
1082     (first_ty : _) = tys
1083
1084     head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1085                              text "where T is not a synonym, and a,b,c are distinct type variables")
1086
1087         -- For now, I only allow tau-types (not polytypes) in
1088         -- the head of an instance decl.
1089         --      E.g.  instance C (forall a. a->a) is rejected
1090         -- One could imagine generalising that, but I'm not sure
1091         -- what all the consequences might be
1092     check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
1093                       ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1094
1095 instTypeErr pp_ty msg
1096   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1097          nest 4 msg]
1098 \end{code}
1099
1100
1101 %************************************************************************
1102 %*                                                                      *
1103 \subsection{Checking instance for termination}
1104 %*                                                                      *
1105 %************************************************************************
1106
1107
1108 \begin{code}
1109 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1110 checkValidInstance tyvars theta clas inst_tys
1111   = do  { gla_exts <- doptM Opt_GlasgowExts
1112         ; undecidable_ok <- doptM Opt_AllowUndecidableInstances
1113
1114         ; checkValidTheta InstThetaCtxt theta
1115         ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1116
1117         -- Check that instance inference will terminate (if we care)
1118         -- For Haskell 98, checkValidTheta has already done that
1119         ; when (gla_exts && not undecidable_ok) $
1120                checkInstTermination theta inst_tys
1121
1122         -- The Coverage Condition
1123         ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1124                   (instTypeErr (pprClassPred clas inst_tys) msg)
1125         }
1126   where
1127     msg  = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies"))
1128 \end{code}
1129
1130 Termination test: each assertion in the context satisfies
1131  (1) no variable has more occurrences in the assertion than in the head, and
1132  (2) the assertion has fewer constructors and variables (taken together
1133      and counting repetitions) than the head.
1134 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1135 (which have already been checked) guarantee termination.
1136
1137 The underlying idea is that
1138
1139     for any ground substitution, each assertion in the
1140     context has fewer type constructors than the head.
1141
1142
1143 \begin{code}
1144 checkInstTermination :: ThetaType -> [TcType] -> TcM ()
1145 checkInstTermination theta tys
1146   = do  { mappM_ (check_nomore (fvTypes tys))    theta
1147         ; mappM_ (check_smaller (sizeTypes tys)) theta }
1148
1149 check_nomore :: [TyVar] -> PredType -> TcM ()
1150 check_nomore fvs pred
1151   = checkTc (null (fvPred pred \\ fvs))
1152             (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1153
1154 check_smaller :: Int -> PredType -> TcM ()
1155 check_smaller n pred
1156   = checkTc (sizePred pred < n)
1157             (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1158
1159 predUndecErr pred msg = sep [msg,
1160                         nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1161
1162 nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
1163 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
1164 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1165
1166 -- Free variables of a type, retaining repetitions, and expanding synonyms
1167 fvType :: Type -> [TyVar]
1168 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1169 fvType (TyVarTy tv)        = [tv]
1170 fvType (TyConApp _ tys)    = fvTypes tys
1171 fvType (NoteTy _ ty)       = fvType ty
1172 fvType (PredTy pred)       = fvPred pred
1173 fvType (FunTy arg res)     = fvType arg ++ fvType res
1174 fvType (AppTy fun arg)     = fvType fun ++ fvType arg
1175 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1176
1177 fvTypes :: [Type] -> [TyVar]
1178 fvTypes tys                = concat (map fvType tys)
1179
1180 fvPred :: PredType -> [TyVar]
1181 fvPred (ClassP _ tys')     = fvTypes tys'
1182 fvPred (IParam _ ty)       = fvType ty
1183
1184 -- Size of a type: the number of variables and constructors
1185 sizeType :: Type -> Int
1186 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1187 sizeType (TyVarTy _)       = 1
1188 sizeType (TyConApp _ tys)  = sizeTypes tys + 1
1189 sizeType (NoteTy _ ty)     = sizeType ty
1190 sizeType (PredTy pred)     = sizePred pred
1191 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
1192 sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
1193 sizeType (ForAllTy _ ty)   = sizeType ty
1194
1195 sizeTypes :: [Type] -> Int
1196 sizeTypes xs               = sum (map sizeType xs)
1197
1198 sizePred :: PredType -> Int
1199 sizePred (ClassP _ tys')   = sizeTypes tys'
1200 sizePred (IParam _ ty)     = sizeType ty
1201 \end{code}