ghc/compiler/typecheck/TcMType.lhs

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