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