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