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 )
  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 -> [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
 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  (KVar _ ref)     = readMutVar ref
 593 writeKindVar (KVar _ ref) val = writeMutVar ref (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   | ExprSigCtxt         -- Expression type signature
 659   | ConArgCtxt Name     -- Data constructor argument
 660   | TySynCtxt Name      -- RHS of a type synonym decl
 661   | GenPatCtxt          -- Pattern in generic decl
 662                         --      f{| a+b |} (Inl x) = ...
 663   | PatSigCtxt          -- Type sig in pattern
 664                         --      f (x::t) = ...
 665   | ResSigCtxt          -- Result type sig
 666                         --      f x :: t = ....
 667   | ForSigCtxt Name     -- Foreign inport or export signature
 668   | RuleSigCtxt Name    -- Signature on a forall'd variable in a RULE
 669   | DefaultDeclCtxt     -- Types in a default declaration
 670
 671 -- Notes re TySynCtxt
 672 -- We allow type synonyms that aren't types; e.g.  type List = []
 673 --
 674 -- If the RHS mentions tyvars that aren't in scope, we'll
 675 -- quantify over them:
 676 --      e.g.    type T = a->a
 677 -- will become  type T = forall a. a->a
 678 --
 679 -- With gla-exts that's right, but for H98 we should complain.
 680
 681
 682 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
 683 pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt (unLoc hs_ty) ctxt
 684
 685 pprUserTypeCtxt ty (FunSigCtxt n)  = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
 686 pprUserTypeCtxt ty ExprSigCtxt     = sep [ptext SLIT("In an expression type signature:"), nest 2 (ppr ty)]
 687 pprUserTypeCtxt ty (ConArgCtxt c)  = sep [ptext SLIT("In the type of the constructor"), pp_sig c ty]
 688 pprUserTypeCtxt ty (TySynCtxt c)   = sep [ptext SLIT("In the RHS of the type synonym") <+> quotes (ppr c) <> comma,
 689                                           nest 2 (ptext SLIT(", namely") <+> ppr ty)]
 690 pprUserTypeCtxt ty GenPatCtxt      = sep [ptext SLIT("In the type pattern of a generic definition:"), nest 2 (ppr ty)]
 691 pprUserTypeCtxt ty PatSigCtxt      = sep [ptext SLIT("In a pattern type signature:"), nest 2 (ppr ty)]
 692 pprUserTypeCtxt ty ResSigCtxt      = sep [ptext SLIT("In a result type signature:"), nest 2 (ppr ty)]
 693 pprUserTypeCtxt ty (ForSigCtxt n)  = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty]
 694 pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
 695 pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)]
 696
 697 pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
 698 \end{code}
 699
 700 \begin{code}
 701 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 702 -- Checks that the type is valid for the given context
 703 checkValidType ctxt ty
 704   = traceTc (text "checkValidType" <+> ppr ty)  `thenM_`
 705     doptM Opt_GlasgowExts       `thenM` \ gla_exts ->
 706     let
 707         rank | gla_exts = Arbitrary
 708              | otherwise
 709              = case ctxt of     -- Haskell 98
 710                  GenPatCtxt     -> Rank 0
 711                  PatSigCtxt     -> Rank 0
 712                  DefaultDeclCtxt-> Rank 0
 713                  ResSigCtxt     -> Rank 0
 714                  TySynCtxt _    -> Rank 0
 715                  ExprSigCtxt    -> Rank 1
 716                  FunSigCtxt _   -> Rank 1
 717                  ConArgCtxt _   -> Rank 1       -- We are given the type of the entire
 718                                                 -- constructor, hence rank 1
 719                  ForSigCtxt _   -> Rank 1
 720                  RuleSigCtxt _  -> Rank 1
 721
 722         actual_kind = typeKind ty
 723
 724         kind_ok = case ctxt of
 725                         TySynCtxt _  -> True    -- Any kind will do
 726                         ResSigCtxt   -> isOpenTypeKind   actual_kind
 727                         ExprSigCtxt  -> isOpenTypeKind   actual_kind
 728                         GenPatCtxt   -> isLiftedTypeKind actual_kind
 729                         ForSigCtxt _ -> isLiftedTypeKind actual_kind
 730                         other        -> isArgTypeKind       actual_kind
 731
 732         ubx_tup | not gla_exts = UT_NotOk
 733                 | otherwise    = case ctxt of
 734                                    TySynCtxt _ -> UT_Ok
 735                                    ExprSigCtxt -> UT_Ok
 736                                    other       -> UT_NotOk
 737                 -- Unboxed tuples ok in function results,
 738                 -- but for type synonyms we allow them even at
 739                 -- top level
 740     in
 741         -- Check that the thing has kind Type, and is lifted if necessary
 742     checkTc kind_ok (kindErr actual_kind)       `thenM_`
 743
 744         -- Check the internal validity of the type itself
 745     check_poly_type rank ubx_tup ty             `thenM_`
 746
 747     traceTc (text "checkValidType done" <+> ppr ty)
 748 \end{code}
 749
 750
 751 \begin{code}
 752 data Rank = Rank Int | Arbitrary
 753
 754 decRank :: Rank -> Rank
 755 decRank Arbitrary = Arbitrary
 756 decRank (Rank n)  = Rank (n-1)
 757
 758 ----------------------------------------
 759 data UbxTupFlag = UT_Ok | UT_NotOk
 760         -- The "Ok" version means "ok if -fglasgow-exts is on"
 761
 762 ----------------------------------------
 763 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 764 check_poly_type (Rank 0) ubx_tup ty
 765   = check_tau_type (Rank 0) ubx_tup ty
 766
 767 check_poly_type rank ubx_tup ty
 768   = let
 769         (tvs, theta, tau) = tcSplitSigmaTy ty
 770     in
 771     check_valid_theta SigmaCtxt theta           `thenM_`
 772     check_tau_type (decRank rank) ubx_tup tau   `thenM_`
 773     checkFreeness tvs theta                     `thenM_`
 774     checkAmbiguity tvs theta (tyVarsOfType tau)
 775
 776 ----------------------------------------
 777 check_arg_type :: Type -> TcM ()
 778 -- The sort of type that can instantiate a type variable,
 779 -- or be the argument of a type constructor.
 780 -- Not an unboxed tuple, not a forall.
 781 -- Other unboxed types are very occasionally allowed as type
 782 -- arguments depending on the kind of the type constructor
 783 --
 784 -- For example, we want to reject things like:
 785 --
 786 --      instance Ord a => Ord (forall s. T s a)
 787 -- and
 788 --      g :: T s (forall b.b)
 789 --
 790 -- NB: unboxed tuples can have polymorphic or unboxed args.
 791 --     This happens in the workers for functions returning
 792 --     product types with polymorphic components.
 793 --     But not in user code.
 794 -- Anyway, they are dealt with by a special case in check_tau_type
 795
 796 check_arg_type ty
 797   = check_tau_type (Rank 0) UT_NotOk ty         `thenM_`
 798     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 799
 800 ----------------------------------------
 801 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 802 -- Rank is allowed rank for function args
 803 -- No foralls otherwise
 804
 805 check_tau_type rank ubx_tup ty@(ForAllTy _ _)       = failWithTc (forAllTyErr ty)
 806 check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
 807         -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
 808
 809 -- Naked PredTys don't usually show up, but they can as a result of
 810 --      {-# SPECIALISE instance Ord Char #-}
 811 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
 812 -- are handled, but the quick thing is just to permit PredTys here.
 813 check_tau_type rank ubx_tup (PredTy sty) = getDOpts             `thenM` \ dflags ->
 814                                            check_source_ty dflags TypeCtxt sty
 815
 816 check_tau_type rank ubx_tup (TyVarTy _)       = returnM ()
 817 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
 818   = check_poly_type rank UT_NotOk arg_ty        `thenM_`
 819     check_tau_type  rank UT_Ok    res_ty
 820
 821 check_tau_type rank ubx_tup (AppTy ty1 ty2)
 822   = check_arg_type ty1 `thenM_` check_arg_type ty2
 823
 824 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
 825         -- Synonym notes are built only when the synonym is
 826         -- saturated (see Type.mkSynTy)
 827   = doptM Opt_GlasgowExts                       `thenM` \ gla_exts ->
 828     (if gla_exts then
 829         -- If -fglasgow-exts then don't check the 'note' part.
 830         -- This  allows us to instantiate a synonym defn with a
 831         -- for-all type, or with a partially-applied type synonym.
 832         --      e.g.   type T a b = a
 833         --             type S m   = m ()
 834         --             f :: S (T Int)
 835         -- Here, T is partially applied, so it's illegal in H98.
 836         -- But if you expand S first, then T we get just
 837         --             f :: Int
 838         -- which is fine.
 839         returnM ()
 840     else
 841         -- For H98, do check the un-expanded part
 842         check_tau_type rank ubx_tup syn
 843     )                                           `thenM_`
 844
 845     check_tau_type rank ubx_tup ty
 846
 847 check_tau_type rank ubx_tup (NoteTy other_note ty)
 848   = check_tau_type rank ubx_tup ty
 849
 850 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
 851   | isSynTyCon tc
 852   =     -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
 853         -- synonym application, leaving it to checkValidType (i.e. right here)
 854         -- to find the error
 855     checkTc syn_arity_ok arity_msg      `thenM_`
 856     mappM_ check_arg_type tys
 857
 858   | isUnboxedTupleTyCon tc
 859   = doptM Opt_GlasgowExts                       `thenM` \ gla_exts ->
 860     checkTc (ubx_tup_ok gla_exts) ubx_tup_msg   `thenM_`
 861     mappM_ (check_tau_type (Rank 0) UT_Ok) tys
 862                 -- Args are allowed to be unlifted, or
 863                 -- more unboxed tuples, so can't use check_arg_ty
 864
 865   | otherwise
 866   = mappM_ check_arg_type tys
 867
 868   where
 869     ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
 870
 871     syn_arity_ok = tc_arity <= n_args
 872                 -- It's OK to have an *over-applied* type synonym
 873                 --      data Tree a b = ...
 874                 --      type Foo a = Tree [a]
 875                 --      f :: Foo a b -> ...
 876     n_args    = length tys
 877     tc_arity  = tyConArity tc
 878
 879     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
 880     ubx_tup_msg = ubxArgTyErr ty
 881
 882 ----------------------------------------
 883 forAllTyErr     ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
 884 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
 885 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
 886 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 887 \end{code}
 888
 889
 890
 891 %************************************************************************
 892 %*                                                                      *
 893 \subsection{Checking a theta or source type}
 894 %*                                                                      *
 895 %************************************************************************
 896
 897 \begin{code}
 898 -- Enumerate the contexts in which a "source type", <S>, can occur
 899 --      Eq a
 900 -- or   ?x::Int
 901 -- or   r <: {x::Int}
 902 -- or   (N a) where N is a newtype
 903
 904 data SourceTyCtxt
 905   = ClassSCCtxt Name    -- Superclasses of clas
 906                         --      class <S> => C a where ...
 907   | SigmaCtxt           -- Theta part of a normal for-all type
 908                         --      f :: <S> => a -> a
 909   | DataTyCtxt Name     -- Theta part of a data decl
 910                         --      data <S> => T a = MkT a
 911   | TypeCtxt            -- Source type in an ordinary type
 912                         --      f :: N a -> N a
 913   | InstThetaCtxt       -- Context of an instance decl
 914                         --      instance <S> => C [a] where ...
 915   | InstHeadCtxt        -- Head of an instance decl
 916                         --      instance ... => Eq a where ...
 917
 918 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
 919 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
 920 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
 921 pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
 922 pprSourceTyCtxt InstHeadCtxt    = ptext SLIT("the head of an instance declaration")
 923 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
 924 \end{code}
 925
 926 \begin{code}
 927 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
 928 checkValidTheta ctxt theta
 929   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
 930
 931 -------------------------
 932 check_valid_theta ctxt []
 933   = returnM ()
 934 check_valid_theta ctxt theta
 935   = getDOpts                                    `thenM` \ dflags ->
 936     warnTc (notNull dups) (dupPredWarn dups)    `thenM_`
 937         -- Actually, in instance decls and type signatures,
 938         -- duplicate constraints are eliminated by TcHsType.hoistForAllTys,
 939         -- so this error can only fire for the context of a class or
 940         -- data type decl.
 941     mappM_ (check_source_ty dflags ctxt) theta
 942   where
 943     (_,dups) = removeDups tcCmpPred theta
 944
 945 -------------------------
 946 check_source_ty dflags ctxt pred@(ClassP cls tys)
 947   =     -- Class predicates are valid in all contexts
 948     checkTc (arity == n_tys) arity_err          `thenM_`
 949
 950         -- Check the form of the argument types
 951     mappM_ check_arg_type tys                           `thenM_`
 952     checkTc (check_class_pred_tys dflags ctxt tys)
 953             (predTyVarErr pred $$ how_to_allow)
 954
 955   where
 956     class_name = className cls
 957     arity      = classArity cls
 958     n_tys      = length tys
 959     arity_err  = arityErr "Class" class_name arity n_tys
 960
 961     how_to_allow = case ctxt of
 962                      InstHeadCtxt  -> empty     -- Should not happen
 963                      InstThetaCtxt -> parens undecidableMsg
 964                      other         -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 965
 966 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
 967         -- Implicit parameters only allows in type
 968         -- signatures; not in instance decls, superclasses etc
 969         -- The reason for not allowing implicit params in instances is a bit subtle
 970         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
 971         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
 972         -- discharge all the potential usas of the ?x in e.   For example, a
 973         -- constraint Foo [Int] might come out of e,and applying the
 974         -- instance decl would show up two uses of ?x.
 975
 976 -- Catch-all
 977 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 978
 979 -------------------------
 980 check_class_pred_tys dflags ctxt tys
 981   = case ctxt of
 982         InstHeadCtxt  -> True   -- We check for instance-head
 983                                 -- formation in checkValidInstHead
 984         InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys
 985         other         -> gla_exts       || all tyvar_head tys
 986   where
 987     undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
 988     gla_exts       = dopt Opt_GlasgowExts dflags
 989
 990 -------------------------
 991 tyvar_head ty                   -- Haskell 98 allows predicates of form
 992   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
 993   | otherwise                   -- where a is a type variable
 994   = case tcSplitAppTy_maybe ty of
 995         Just (ty, _) -> tyvar_head ty
 996         Nothing      -> False
 997 \end{code}
 998
 999 Check for ambiguity
1000 ~~~~~~~~~~~~~~~~~~~
1001           forall V. P => tau
1002 is ambiguous if P contains generic variables
1003 (i.e. one of the Vs) that are not mentioned in tau
1004
1005 However, we need to take account of functional dependencies
1006 when we speak of 'mentioned in tau'.  Example:
1007         class C a b | a -> b where ...
1008 Then the type
1009         forall x y. (C x y) => x
1010 is not ambiguous because x is mentioned and x determines y
1011
1012 NB; the ambiguity check is only used for *user* types, not for types
1013 coming from inteface files.  The latter can legitimately have
1014 ambiguous types. Example
1015
1016    class S a where s :: a -> (Int,Int)
1017    instance S Char where s _ = (1,1)
1018    f:: S a => [a] -> Int -> (Int,Int)
1019    f (_::[a]) x = (a*x,b)
1020         where (a,b) = s (undefined::a)
1021
1022 Here the worker for f gets the type
1023         fw :: forall a. S a => Int -> (# Int, Int #)
1024
1025 If the list of tv_names is empty, we have a monotype, and then we
1026 don't need to check for ambiguity either, because the test can't fail
1027 (see is_ambig).
1028
1029 \begin{code}
1030 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1031 checkAmbiguity forall_tyvars theta tau_tyvars
1032   = mappM_ complain (filter is_ambig theta)
1033   where
1034     complain pred     = addErrTc (ambigErr pred)
1035     extended_tau_vars = grow theta tau_tyvars
1036
1037         -- Only a *class* predicate can give rise to ambiguity
1038         -- An *implicit parameter* cannot.  For example:
1039         --      foo :: (?x :: [a]) => Int
1040         --      foo = length ?x
1041         -- is fine.  The call site will suppply a particular 'x'
1042     is_ambig pred     = isClassPred  pred &&
1043                         any ambig_var (varSetElems (tyVarsOfPred pred))
1044
1045     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
1046                         not (ct_var `elemVarSet` extended_tau_vars)
1047
1048 ambigErr pred
1049   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1050          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1051                  ptext SLIT("must be reachable from the type after the '=>'"))]
1052 \end{code}
1053
1054 In addition, GHC insists that at least one type variable
1055 in each constraint is in V.  So we disallow a type like
1056         forall a. Eq b => b -> b
1057 even in a scope where b is in scope.
1058
1059 \begin{code}
1060 checkFreeness forall_tyvars theta
1061   = mappM_ complain (filter is_free theta)
1062   where
1063     is_free pred     =  not (isIPPred pred)
1064                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1065     bound_var ct_var = ct_var `elem` forall_tyvars
1066     complain pred    = addErrTc (freeErr pred)
1067
1068 freeErr pred
1069   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1070                    ptext SLIT("are already in scope"),
1071          nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1072     ]
1073 \end{code}
1074
1075 \begin{code}
1076 checkThetaCtxt ctxt theta
1077   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1078           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1079
1080 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1081 predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
1082 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1083
1084 arityErr kind name n m
1085   = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1086            n_arguments <> comma, text "but has been given", int m]
1087     where
1088         n_arguments | n == 0 = ptext SLIT("no arguments")
1089                     | n == 1 = ptext SLIT("1 argument")
1090                     | True   = hsep [int n, ptext SLIT("arguments")]
1091 \end{code}
1092
1093
1094 %************************************************************************
1095 %*                                                                      *
1096 \subsection{Checking for a decent instance head type}
1097 %*                                                                      *
1098 %************************************************************************
1099
1100 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1101 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1102
1103 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1104 flag is on, or (2)~the instance is imported (they must have been
1105 compiled elsewhere). In these cases, we let them go through anyway.
1106
1107 We can also have instances for functions: @instance Foo (a -> b) ...@.
1108
1109 \begin{code}
1110 checkValidInstHead :: Type -> TcM (Class, [TcType])
1111
1112 checkValidInstHead ty   -- Should be a source type
1113   = case tcSplitPredTy_maybe ty of {
1114         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1115         Just pred ->
1116
1117     case getClassPredTys_maybe pred of {
1118         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1119         Just (clas,tys) ->
1120
1121     getDOpts                                    `thenM` \ dflags ->
1122     mappM_ check_arg_type tys                   `thenM_`
1123     check_inst_head dflags clas tys             `thenM_`
1124     returnM (clas, tys)
1125     }}
1126
1127 check_inst_head dflags clas tys
1128         -- If GlasgowExts then check at least one isn't a type variable
1129   | dopt Opt_GlasgowExts dflags
1130   = check_tyvars dflags clas tys
1131
1132         -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1133   | isSingleton tys,
1134     Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1135     not (isSynTyCon tycon),             -- ...but not a synonym
1136     all tcIsTyVarTy arg_tys,            -- Applied to type variables
1137     equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1138           -- This last condition checks that all the type variables are distinct
1139   = returnM ()
1140
1141   | otherwise
1142   = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1143
1144   where
1145     (first_ty : _)       = tys
1146
1147     head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1148                              text "where T is not a synonym, and a,b,c are distinct type variables")
1149
1150 check_tyvars dflags clas tys
1151         -- Check that at least one isn't a type variable
1152         -- unless -fallow-undecideable-instances
1153   | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1154   | not (all tcIsTyVarTy tys)                 = returnM ()
1155   | otherwise                                 = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1156   where
1157     msg =  parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1158                    $$ undecidableMsg)
1159
1160 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1161 \end{code}
1162
1163 \begin{code}
1164 instTypeErr pp_ty msg
1165   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1166          nest 4 msg]
1167 \end{code}