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