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