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