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   | null tvs && null theta
 735   = check_tau_type rank ubx_tup ty
 736   | otherwise
 737   = do  { check_valid_theta SigmaCtxt theta
 738         ; check_poly_type rank ubx_tup tau      -- Allow foralls to right of arrow
 739         ; checkFreeness tvs theta
 740         ; checkAmbiguity tvs theta (tyVarsOfType tau) }
 741   where
 742     (tvs, theta, tau) = tcSplitSigmaTy ty
 743
 744 ----------------------------------------
 745 check_arg_type :: Type -> TcM ()
 746 -- The sort of type that can instantiate a type variable,
 747 -- or be the argument of a type constructor.
 748 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
 749 -- Other unboxed types are very occasionally allowed as type
 750 -- arguments depending on the kind of the type constructor
 751 --
 752 -- For example, we want to reject things like:
 753 --
 754 --      instance Ord a => Ord (forall s. T s a)
 755 -- and
 756 --      g :: T s (forall b.b)
 757 --
 758 -- NB: unboxed tuples can have polymorphic or unboxed args.
 759 --     This happens in the workers for functions returning
 760 --     product types with polymorphic components.
 761 --     But not in user code.
 762 -- Anyway, they are dealt with by a special case in check_tau_type
 763
 764 check_arg_type ty
 765   = check_poly_type Arbitrary UT_NotOk ty       `thenM_`
 766     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 767
 768 ----------------------------------------
 769 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 770 -- Rank is allowed rank for function args
 771 -- No foralls otherwise
 772
 773 check_tau_type rank ubx_tup ty@(ForAllTy _ _)       = failWithTc (forAllTyErr ty)
 774 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
 775         -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
 776
 777 -- Naked PredTys don't usually show up, but they can as a result of
 778 --      {-# SPECIALISE instance Ord Char #-}
 779 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
 780 -- are handled, but the quick thing is just to permit PredTys here.
 781 check_tau_type rank ubx_tup (PredTy sty) = getDOpts             `thenM` \ dflags ->
 782                                            check_source_ty dflags TypeCtxt sty
 783
 784 check_tau_type rank ubx_tup (TyVarTy _)       = returnM ()
 785 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
 786   = check_poly_type (decRank rank) UT_NotOk arg_ty      `thenM_`
 787     check_poly_type rank           UT_Ok    res_ty
 788
 789 check_tau_type rank ubx_tup (AppTy ty1 ty2)
 790   = check_arg_type ty1 `thenM_` check_arg_type ty2
 791
 792 check_tau_type rank ubx_tup (NoteTy other_note ty)
 793   = check_tau_type rank ubx_tup ty
 794
 795 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
 796   | isSynTyCon tc
 797   = do  {       -- It's OK to have an *over-applied* type synonym
 798                 --      data Tree a b = ...
 799                 --      type Foo a = Tree [a]
 800                 --      f :: Foo a b -> ...
 801         ; case tcView ty of
 802              Just ty' -> check_tau_type rank ubx_tup ty'        -- Check expansion
 803              Nothing  -> failWithTc arity_msg
 804
 805         ; gla_exts <- doptM Opt_GlasgowExts
 806         ; if gla_exts then
 807         -- If -fglasgow-exts then don't check the type arguments
 808         -- This allows us to instantiate a synonym defn with a
 809         -- for-all type, or with a partially-applied type synonym.
 810         --      e.g.   type T a b = a
 811         --             type S m   = m ()
 812         --             f :: S (T Int)
 813         -- Here, T is partially applied, so it's illegal in H98.
 814         -- But if you expand S first, then T we get just
 815         --             f :: Int
 816         -- which is fine.
 817                 returnM ()
 818           else
 819                 -- For H98, do check the type args
 820                 mappM_ check_arg_type tys
 821         }
 822
 823   | isUnboxedTupleTyCon tc
 824   = doptM Opt_GlasgowExts                       `thenM` \ gla_exts ->
 825     checkTc (ubx_tup_ok gla_exts) ubx_tup_msg   `thenM_`
 826     mappM_ (check_tau_type (Rank 0) UT_Ok) tys
 827                 -- Args are allowed to be unlifted, or
 828                 -- more unboxed tuples, so can't use check_arg_ty
 829
 830   | otherwise
 831   = mappM_ check_arg_type tys
 832
 833   where
 834     ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
 835
 836     n_args    = length tys
 837     tc_arity  = tyConArity tc
 838
 839     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
 840     ubx_tup_msg = ubxArgTyErr ty
 841
 842 ----------------------------------------
 843 forAllTyErr     ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
 844 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
 845 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
 846 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 847 \end{code}
 848
 849
 850
 851 %************************************************************************
 852 %*                                                                      *
 853 \subsection{Checking a theta or source type}
 854 %*                                                                      *
 855 %************************************************************************
 856
 857 \begin{code}
 858 -- Enumerate the contexts in which a "source type", <S>, can occur
 859 --      Eq a
 860 -- or   ?x::Int
 861 -- or   r <: {x::Int}
 862 -- or   (N a) where N is a newtype
 863
 864 data SourceTyCtxt
 865   = ClassSCCtxt Name    -- Superclasses of clas
 866                         --      class <S> => C a where ...
 867   | SigmaCtxt           -- Theta part of a normal for-all type
 868                         --      f :: <S> => a -> a
 869   | DataTyCtxt Name     -- Theta part of a data decl
 870                         --      data <S> => T a = MkT a
 871   | TypeCtxt            -- Source type in an ordinary type
 872                         --      f :: N a -> N a
 873   | InstThetaCtxt       -- Context of an instance decl
 874                         --      instance <S> => C [a] where ...
 875
 876 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
 877 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
 878 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
 879 pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
 880 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
 881 \end{code}
 882
 883 \begin{code}
 884 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
 885 checkValidTheta ctxt theta
 886   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
 887
 888 -------------------------
 889 check_valid_theta ctxt []
 890   = returnM ()
 891 check_valid_theta ctxt theta
 892   = getDOpts                                    `thenM` \ dflags ->
 893     warnTc (notNull dups) (dupPredWarn dups)    `thenM_`
 894     mappM_ (check_source_ty dflags ctxt) theta
 895   where
 896     (_,dups) = removeDups tcCmpPred theta
 897
 898 -------------------------
 899 check_source_ty dflags ctxt pred@(ClassP cls tys)
 900   =     -- Class predicates are valid in all contexts
 901     checkTc (arity == n_tys) arity_err          `thenM_`
 902
 903         -- Check the form of the argument types
 904     mappM_ check_arg_type tys                           `thenM_`
 905     checkTc (check_class_pred_tys dflags ctxt tys)
 906             (predTyVarErr pred $$ how_to_allow)
 907
 908   where
 909     class_name = className cls
 910     arity      = classArity cls
 911     n_tys      = length tys
 912     arity_err  = arityErr "Class" class_name arity n_tys
 913     how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 914
 915 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
 916         -- Implicit parameters only allows in type
 917         -- signatures; not in instance decls, superclasses etc
 918         -- The reason for not allowing implicit params in instances is a bit subtle
 919         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
 920         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
 921         -- discharge all the potential usas of the ?x in e.   For example, a
 922         -- constraint Foo [Int] might come out of e,and applying the
 923         -- instance decl would show up two uses of ?x.
 924
 925 -- Catch-all
 926 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 927
 928 -------------------------
 929 check_class_pred_tys dflags ctxt tys
 930   = case ctxt of
 931         TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
 932         InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys
 933                                 -- Further checks on head and theta in
 934                                 -- checkInstTermination
 935         other         -> gla_exts || all tyvar_head tys
 936   where
 937     gla_exts       = dopt Opt_GlasgowExts dflags
 938     undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
 939
 940 -------------------------
 941 tyvar_head ty                   -- Haskell 98 allows predicates of form
 942   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
 943   | otherwise                   -- where a is a type variable
 944   = case tcSplitAppTy_maybe ty of
 945         Just (ty, _) -> tyvar_head ty
 946         Nothing      -> False
 947 \end{code}
 948
 949 Check for ambiguity
 950 ~~~~~~~~~~~~~~~~~~~
 951           forall V. P => tau
 952 is ambiguous if P contains generic variables
 953 (i.e. one of the Vs) that are not mentioned in tau
 954
 955 However, we need to take account of functional dependencies
 956 when we speak of 'mentioned in tau'.  Example:
 957         class C a b | a -> b where ...
 958 Then the type
 959         forall x y. (C x y) => x
 960 is not ambiguous because x is mentioned and x determines y
 961
 962 NB; the ambiguity check is only used for *user* types, not for types
 963 coming from inteface files.  The latter can legitimately have
 964 ambiguous types. Example
 965
 966    class S a where s :: a -> (Int,Int)
 967    instance S Char where s _ = (1,1)
 968    f:: S a => [a] -> Int -> (Int,Int)
 969    f (_::[a]) x = (a*x,b)
 970         where (a,b) = s (undefined::a)
 971
 972 Here the worker for f gets the type
 973         fw :: forall a. S a => Int -> (# Int, Int #)
 974
 975 If the list of tv_names is empty, we have a monotype, and then we
 976 don't need to check for ambiguity either, because the test can't fail
 977 (see is_ambig).
 978
 979 \begin{code}
 980 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
 981 checkAmbiguity forall_tyvars theta tau_tyvars
 982   = mappM_ complain (filter is_ambig theta)
 983   where
 984     complain pred     = addErrTc (ambigErr pred)
 985     extended_tau_vars = grow theta tau_tyvars
 986
 987         -- Only a *class* predicate can give rise to ambiguity
 988         -- An *implicit parameter* cannot.  For example:
 989         --      foo :: (?x :: [a]) => Int
 990         --      foo = length ?x
 991         -- is fine.  The call site will suppply a particular 'x'
 992     is_ambig pred     = isClassPred  pred &&
 993                         any ambig_var (varSetElems (tyVarsOfPred pred))
 994
 995     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
 996                         not (ct_var `elemVarSet` extended_tau_vars)
 997
 998 ambigErr pred
 999   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1000          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1001                  ptext SLIT("must be reachable from the type after the '=>'"))]
1002 \end{code}
1003
1004 In addition, GHC insists that at least one type variable
1005 in each constraint is in V.  So we disallow a type like
1006         forall a. Eq b => b -> b
1007 even in a scope where b is in scope.
1008
1009 \begin{code}
1010 checkFreeness forall_tyvars theta
1011   = mappM_ complain (filter is_free theta)
1012   where
1013     is_free pred     =  not (isIPPred pred)
1014                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1015     bound_var ct_var = ct_var `elem` forall_tyvars
1016     complain pred    = addErrTc (freeErr pred)
1017
1018 freeErr pred
1019   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1020                    ptext SLIT("are already in scope"),
1021          nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1022     ]
1023 \end{code}
1024
1025 \begin{code}
1026 checkThetaCtxt ctxt theta
1027   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1028           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1029
1030 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1031 predTyVarErr pred  = sep [ptext SLIT("Non type-variable argument"),
1032                           nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1033 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1034
1035 arityErr kind name n m
1036   = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1037            n_arguments <> comma, text "but has been given", int m]
1038     where
1039         n_arguments | n == 0 = ptext SLIT("no arguments")
1040                     | n == 1 = ptext SLIT("1 argument")
1041                     | True   = hsep [int n, ptext SLIT("arguments")]
1042 \end{code}
1043
1044
1045 %************************************************************************
1046 %*                                                                      *
1047 \subsection{Checking for a decent instance head type}
1048 %*                                                                      *
1049 %************************************************************************
1050
1051 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1052 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1053
1054 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1055 flag is on, or (2)~the instance is imported (they must have been
1056 compiled elsewhere). In these cases, we let them go through anyway.
1057
1058 We can also have instances for functions: @instance Foo (a -> b) ...@.
1059
1060 \begin{code}
1061 checkValidInstHead :: Type -> TcM (Class, [TcType])
1062
1063 checkValidInstHead ty   -- Should be a source type
1064   = case tcSplitPredTy_maybe ty of {
1065         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1066         Just pred ->
1067
1068     case getClassPredTys_maybe pred of {
1069         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1070         Just (clas,tys) ->
1071
1072     getDOpts                                    `thenM` \ dflags ->
1073     mappM_ check_arg_type tys                   `thenM_`
1074     check_inst_head dflags clas tys             `thenM_`
1075     returnM (clas, tys)
1076     }}
1077
1078 check_inst_head dflags clas tys
1079         -- If GlasgowExts then check at least one isn't a type variable
1080   | dopt Opt_GlasgowExts dflags
1081   = mapM_ check_one tys
1082
1083         -- WITH HASKELL 98, MUST HAVE C (T a b c)
1084   | otherwise
1085   = checkTc (isSingleton tys && tcValidInstHeadTy first_ty)
1086             (instTypeErr (pprClassPred clas tys) head_shape_msg)
1087
1088   where
1089     (first_ty : _) = tys
1090
1091     head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1092                              text "where T is not a synonym, and a,b,c are distinct type variables")
1093
1094         -- For now, I only allow tau-types (not polytypes) in
1095         -- the head of an instance decl.
1096         --      E.g.  instance C (forall a. a->a) is rejected
1097         -- One could imagine generalising that, but I'm not sure
1098         -- what all the consequences might be
1099     check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
1100                       ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1101
1102 instTypeErr pp_ty msg
1103   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1104          nest 4 msg]
1105 \end{code}
1106
1107
1108 %************************************************************************
1109 %*                                                                      *
1110 \subsection{Checking instance for termination}
1111 %*                                                                      *
1112 %************************************************************************
1113
1114
1115 \begin{code}
1116 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1117 checkValidInstance tyvars theta clas inst_tys
1118   = do  { gla_exts <- doptM Opt_GlasgowExts
1119         ; undecidable_ok <- doptM Opt_AllowUndecidableInstances
1120
1121         ; checkValidTheta InstThetaCtxt theta
1122         ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1123
1124         -- Check that instance inference will terminate (if we care)
1125         -- For Haskell 98, checkValidTheta has already done that
1126         ; when (gla_exts && not undecidable_ok) $
1127                checkInstTermination theta inst_tys
1128
1129         -- The Coverage Condition
1130         ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1131                   (instTypeErr (pprClassPred clas inst_tys) msg)
1132         }
1133   where
1134     msg  = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies"))
1135 \end{code}
1136
1137 Termination test: each assertion in the context satisfies
1138  (1) no variable has more occurrences in the assertion than in the head, and
1139  (2) the assertion has fewer constructors and variables (taken together
1140      and counting repetitions) than the head.
1141 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1142 (which have already been checked) guarantee termination.
1143
1144 The underlying idea is that
1145
1146     for any ground substitution, each assertion in the
1147     context has fewer type constructors than the head.
1148
1149
1150 \begin{code}
1151 checkInstTermination :: ThetaType -> [TcType] -> TcM ()
1152 checkInstTermination theta tys
1153   = do  { mappM_ (check_nomore (fvTypes tys))    theta
1154         ; mappM_ (check_smaller (sizeTypes tys)) theta }
1155
1156 check_nomore :: [TyVar] -> PredType -> TcM ()
1157 check_nomore fvs pred
1158   = checkTc (null (fvPred pred \\ fvs))
1159             (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1160
1161 check_smaller :: Int -> PredType -> TcM ()
1162 check_smaller n pred
1163   = checkTc (sizePred pred < n)
1164             (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1165
1166 predUndecErr pred msg = sep [msg,
1167                         nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1168
1169 nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
1170 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
1171 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1172
1173 -- Free variables of a type, retaining repetitions, and expanding synonyms
1174 fvType :: Type -> [TyVar]
1175 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1176 fvType (TyVarTy tv)        = [tv]
1177 fvType (TyConApp _ tys)    = fvTypes tys
1178 fvType (NoteTy _ ty)       = fvType ty
1179 fvType (PredTy pred)       = fvPred pred
1180 fvType (FunTy arg res)     = fvType arg ++ fvType res
1181 fvType (AppTy fun arg)     = fvType fun ++ fvType arg
1182 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1183
1184 fvTypes :: [Type] -> [TyVar]
1185 fvTypes tys                = concat (map fvType tys)
1186
1187 fvPred :: PredType -> [TyVar]
1188 fvPred (ClassP _ tys')     = fvTypes tys'
1189 fvPred (IParam _ ty)       = fvType ty
1190
1191 -- Size of a type: the number of variables and constructors
1192 sizeType :: Type -> Int
1193 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1194 sizeType (TyVarTy _)       = 1
1195 sizeType (TyConApp _ tys)  = sizeTypes tys + 1
1196 sizeType (NoteTy _ ty)     = sizeType ty
1197 sizeType (PredTy pred)     = sizePred pred
1198 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
1199 sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
1200 sizeType (ForAllTy _ ty)   = sizeType ty
1201
1202 sizeTypes :: [Type] -> Int
1203 sizeTypes xs               = sum (map sizeType xs)
1204
1205 sizePred :: PredType -> Int
1206 sizePred (ClassP _ tys')   = sizeTypes tys'
1207 sizePred (IParam _ ty)     = sizeType ty
1208 \end{code}