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