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