compiler/typecheck/TcMType.lhs

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