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