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(..),  -- 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, tcEqType, 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, tcView,
  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, findDupsEq )
  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 _ ty2)             = go ty2      -- Discard free-tyvar annotations
 531
 532     go (PredTy p)                 = go_pred p           `thenM` \ p' ->
 533                                     returnM (PredTy p')
 534
 535     go (FunTy arg res)            = go arg              `thenM` \ arg' ->
 536                                     go res              `thenM` \ res' ->
 537                                     returnM (FunTy arg' res')
 538
 539     go (AppTy fun arg)            = go fun              `thenM` \ fun' ->
 540                                     go arg              `thenM` \ arg' ->
 541                                     returnM (mkAppTy fun' arg')
 542                 -- NB the mkAppTy; we might have instantiated a
 543                 -- type variable to a type constructor, so we need
 544                 -- to pull the TyConApp to the top.
 545
 546         -- The two interesting cases!
 547     go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn rflag tyvar
 548
 549     go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
 550                              go ty              `thenM` \ ty' ->
 551                              returnM (ForAllTy tyvar ty')
 552
 553     go_pred (ClassP c tys) = mappM go tys       `thenM` \ tys' ->
 554                              returnM (ClassP c tys')
 555     go_pred (IParam n ty)  = go ty              `thenM` \ ty' ->
 556                              returnM (IParam n ty')
 557
 558 zonkTyVar :: (TcTyVar -> TcM Type)              -- What to do for an unbound mutable variable
 559           -> Bool                               -- Consult the type refinement?
 560           -> TcTyVar -> TcM TcType
 561 zonkTyVar unbound_var_fn rflag tyvar
 562   | not (isTcTyVar tyvar)       -- When zonking (forall a.  ...a...), the occurrences of
 563                                 -- the quantified variable 'a' are TyVars not TcTyVars
 564   = returnM (TyVarTy tyvar)
 565
 566   | otherwise
 567   =  condLookupTcTyVar rflag tyvar  `thenM` \ details ->
 568      case details of
 569           -- If b is true, the variable was refined, and therefore it is okay
 570           -- to continue refining inside.  Otherwise it was wobbly and we should
 571           -- not refine further inside.
 572           IndirectTv b ty   -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
 573           DoneTv (MetaTv _) -> unbound_var_fn tyvar         -- Unbound meta type variable
 574           DoneTv other      -> return (TyVarTy tyvar)       -- Rigid, no zonking necessary
 575 \end{code}
 576
 577
 578
 579 %************************************************************************
 580 %*                                                                      *
 581                         Zonking kinds
 582 %*                                                                      *
 583 %************************************************************************
 584
 585 \begin{code}
 586 readKindVar  :: KindVar -> TcM (Maybe TcKind)
 587 writeKindVar :: KindVar -> TcKind -> TcM ()
 588 readKindVar  kv = readMutVar (kindVarRef kv)
 589 writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
 590
 591 -------------
 592 zonkTcKind :: TcKind -> TcM TcKind
 593 zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
 594                                 ; k2' <- zonkTcKind k2
 595                                 ; returnM (FunKind k1' k2') }
 596 zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv
 597                                ; case mb_kind of
 598                                     Nothing -> returnM k
 599                                     Just k  -> zonkTcKind k }
 600 zonkTcKind other_kind = returnM other_kind
 601
 602 -------------
 603 zonkTcKindToKind :: TcKind -> TcM Kind
 604 zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
 605                                       ; k2' <- zonkTcKindToKind k2
 606                                       ; returnM (FunKind k1' k2') }
 607
 608 zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv
 609                                    ; case mb_kind of
 610                                        Nothing -> return liftedTypeKind
 611                                        Just k  -> zonkTcKindToKind k }
 612
 613 zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind  -- An "Open" kind defaults to *
 614 zonkTcKindToKind other_kind   = returnM other_kind
 615 \end{code}
 616
 617 %************************************************************************
 618 %*                                                                      *
 619 \subsection{Checking a user type}
 620 %*                                                                      *
 621 %************************************************************************
 622
 623 When dealing with a user-written type, we first translate it from an HsType
 624 to a Type, performing kind checking, and then check various things that should
 625 be true about it.  We don't want to perform these checks at the same time
 626 as the initial translation because (a) they are unnecessary for interface-file
 627 types and (b) when checking a mutually recursive group of type and class decls,
 628 we can't "look" at the tycons/classes yet.  Also, the checks are are rather
 629 diverse, and used to really mess up the other code.
 630
 631 One thing we check for is 'rank'.
 632
 633         Rank 0:         monotypes (no foralls)
 634         Rank 1:         foralls at the front only, Rank 0 inside
 635         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
 636
 637         basic ::= tyvar | T basic ... basic
 638
 639         r2  ::= forall tvs. cxt => r2a
 640         r2a ::= r1 -> r2a | basic
 641         r1  ::= forall tvs. cxt => r0
 642         r0  ::= r0 -> r0 | basic
 643
 644 Another thing is to check that type synonyms are saturated.
 645 This might not necessarily show up in kind checking.
 646         type A i = i
 647         data T k = MkT (k Int)
 648         f :: T A        -- BAD!
 649
 650
 651 \begin{code}
 652 data UserTypeCtxt
 653   = FunSigCtxt Name     -- Function type signature
 654                         -- Also used for types in SPECIALISE pragmas
 655   | ExprSigCtxt         -- Expression type signature
 656   | ConArgCtxt Name     -- Data constructor argument
 657   | TySynCtxt Name      -- RHS of a type synonym decl
 658   | GenPatCtxt          -- Pattern in generic decl
 659                         --      f{| a+b |} (Inl x) = ...
 660   | PatSigCtxt          -- Type sig in pattern
 661                         --      f (x::t) = ...
 662   | ResSigCtxt          -- Result type sig
 663                         --      f x :: t = ....
 664   | ForSigCtxt Name     -- Foreign inport or export signature
 665   | RuleSigCtxt Name    -- Signature on a forall'd variable in a RULE
 666   | DefaultDeclCtxt     -- Types in a default declaration
 667   | SpecInstCtxt        -- SPECIALISE instance pragma
 668
 669 -- Notes re TySynCtxt
 670 -- We allow type synonyms that aren't types; e.g.  type List = []
 671 --
 672 -- If the RHS mentions tyvars that aren't in scope, we'll
 673 -- quantify over them:
 674 --      e.g.    type T = a->a
 675 -- will become  type T = forall a. a->a
 676 --
 677 -- With gla-exts that's right, but for H98 we should complain.
 678
 679
 680 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
 681 pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt (unLoc hs_ty) ctxt
 682
 683 pprUserTypeCtxt ty (FunSigCtxt n)  = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
 684 pprUserTypeCtxt ty ExprSigCtxt     = sep [ptext SLIT("In an expression type signature:"), nest 2 (ppr ty)]
 685 pprUserTypeCtxt ty (ConArgCtxt c)  = sep [ptext SLIT("In the type of the constructor"), pp_sig c ty]
 686 pprUserTypeCtxt ty (TySynCtxt c)   = sep [ptext SLIT("In the RHS of the type synonym") <+> quotes (ppr c) <> comma,
 687                                           nest 2 (ptext SLIT(", namely") <+> ppr ty)]
 688 pprUserTypeCtxt ty GenPatCtxt      = sep [ptext SLIT("In the type pattern of a generic definition:"), nest 2 (ppr ty)]
 689 pprUserTypeCtxt ty PatSigCtxt      = sep [ptext SLIT("In a pattern type signature:"), nest 2 (ppr ty)]
 690 pprUserTypeCtxt ty ResSigCtxt      = sep [ptext SLIT("In a result type signature:"), nest 2 (ppr ty)]
 691 pprUserTypeCtxt ty (ForSigCtxt n)  = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty]
 692 pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
 693 pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)]
 694 pprUserTypeCtxt ty SpecInstCtxt    = sep [ptext SLIT("In a SPECIALISE instance pragma:"), nest 2 (ppr ty)]
 695
 696 pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
 697 \end{code}
 698
 699 \begin{code}
 700 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 701 -- Checks that the type is valid for the given context
 702 checkValidType ctxt ty
 703   = traceTc (text "checkValidType" <+> ppr ty)  `thenM_`
 704     doptM Opt_GlasgowExts       `thenM` \ gla_exts ->
 705     let
 706         rank | gla_exts = Arbitrary
 707              | otherwise
 708              = case ctxt of     -- Haskell 98
 709                  GenPatCtxt     -> Rank 0
 710                  PatSigCtxt     -> Rank 0
 711                  DefaultDeclCtxt-> Rank 0
 712                  ResSigCtxt     -> Rank 0
 713                  TySynCtxt _    -> Rank 0
 714                  ExprSigCtxt    -> Rank 1
 715                  FunSigCtxt _   -> Rank 1
 716                  ConArgCtxt _   -> Rank 1       -- We are given the type of the entire
 717                                                 -- constructor, hence rank 1
 718                  ForSigCtxt _   -> Rank 1
 719                  RuleSigCtxt _  -> Rank 1
 720                  SpecInstCtxt   -> 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 other_note ty)
 825   = check_tau_type rank ubx_tup ty
 826
 827 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
 828   | isSynTyCon tc
 829   =     -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
 830         -- synonym application, leaving it to checkValidType (i.e. right here)
 831         -- to find the error
 832     do  {       -- It's OK to have an *over-applied* type synonym
 833                 --      data Tree a b = ...
 834                 --      type Foo a = Tree [a]
 835                 --      f :: Foo a b -> ...
 836         ; case tcView ty of
 837              Just ty' -> check_tau_type rank ubx_tup ty'        -- Check expansion
 838              Nothing  -> failWithTc arity_msg
 839
 840         ; gla_exts <- doptM Opt_GlasgowExts
 841         ; if gla_exts then
 842         -- If -fglasgow-exts then don't check the type arguments
 843         -- This allows us to instantiate a synonym defn with a
 844         -- for-all type, or with a partially-applied type synonym.
 845         --      e.g.   type T a b = a
 846         --             type S m   = m ()
 847         --             f :: S (T Int)
 848         -- Here, T is partially applied, so it's illegal in H98.
 849         -- But if you expand S first, then T we get just
 850         --             f :: Int
 851         -- which is fine.
 852                 returnM ()
 853           else
 854                 -- For H98, do check the type args
 855                 mappM_ check_arg_type tys
 856         }
 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     n_args    = length tys
 872     tc_arity  = tyConArity tc
 873
 874     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
 875     ubx_tup_msg = ubxArgTyErr ty
 876
 877 ----------------------------------------
 878 forAllTyErr     ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
 879 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
 880 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
 881 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 882 \end{code}
 883
 884
 885
 886 %************************************************************************
 887 %*                                                                      *
 888 \subsection{Checking a theta or source type}
 889 %*                                                                      *
 890 %************************************************************************
 891
 892 \begin{code}
 893 -- Enumerate the contexts in which a "source type", <S>, can occur
 894 --      Eq a
 895 -- or   ?x::Int
 896 -- or   r <: {x::Int}
 897 -- or   (N a) where N is a newtype
 898
 899 data SourceTyCtxt
 900   = ClassSCCtxt Name    -- Superclasses of clas
 901                         --      class <S> => C a where ...
 902   | SigmaCtxt           -- Theta part of a normal for-all type
 903                         --      f :: <S> => a -> a
 904   | DataTyCtxt Name     -- Theta part of a data decl
 905                         --      data <S> => T a = MkT a
 906   | TypeCtxt            -- Source type in an ordinary type
 907                         --      f :: N a -> N a
 908   | InstThetaCtxt       -- Context of an instance decl
 909                         --      instance <S> => C [a] where ...
 910   | InstHeadCtxt        -- Head of an instance decl
 911                         --      instance ... => Eq a where ...
 912
 913 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
 914 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
 915 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
 916 pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
 917 pprSourceTyCtxt InstHeadCtxt    = ptext SLIT("the head of an instance declaration")
 918 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
 919 \end{code}
 920
 921 \begin{code}
 922 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
 923 checkValidTheta ctxt theta
 924   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
 925
 926 -------------------------
 927 check_valid_theta ctxt []
 928   = returnM ()
 929 check_valid_theta ctxt theta
 930   = getDOpts                                    `thenM` \ dflags ->
 931     warnTc (notNull dups) (dupPredWarn dups)    `thenM_`
 932         -- Actually, in instance decls and type signatures,
 933         -- duplicate constraints are eliminated by TcHsType.hoistForAllTys,
 934         -- so this error can only fire for the context of a class or
 935         -- data type decl.
 936     mappM_ (check_source_ty dflags ctxt) theta
 937   where
 938     (_,dups) = removeDups tcCmpPred theta
 939
 940 -------------------------
 941 check_source_ty dflags ctxt pred@(ClassP cls tys)
 942   =     -- Class predicates are valid in all contexts
 943     checkTc (arity == n_tys) arity_err          `thenM_`
 944
 945         -- Check the form of the argument types
 946     mappM_ check_arg_type tys                           `thenM_`
 947     checkTc (check_class_pred_tys dflags ctxt tys)
 948             (predTyVarErr pred $$ how_to_allow)
 949
 950   where
 951     class_name = className cls
 952     arity      = classArity cls
 953     n_tys      = length tys
 954     arity_err  = arityErr "Class" class_name arity n_tys
 955
 956     how_to_allow = case ctxt of
 957                      InstHeadCtxt  -> empty     -- Should not happen
 958                      InstThetaCtxt -> parens undecidableMsg
 959                      other         -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 960
 961 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
 962         -- Implicit parameters only allows in type
 963         -- signatures; not in instance decls, superclasses etc
 964         -- The reason for not allowing implicit params in instances is a bit subtle
 965         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
 966         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
 967         -- discharge all the potential usas of the ?x in e.   For example, a
 968         -- constraint Foo [Int] might come out of e,and applying the
 969         -- instance decl would show up two uses of ?x.
 970
 971 -- Catch-all
 972 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 973
 974 -------------------------
 975 check_class_pred_tys dflags ctxt tys
 976   = case ctxt of
 977         TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
 978         InstHeadCtxt  -> True   -- We check for instance-head
 979                                 -- formation in checkValidInstHead
 980         InstThetaCtxt -> undecidable_ok || distinct_tyvars tys
 981         other         -> gla_exts       || all tyvar_head tys
 982   where
 983     undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
 984     gla_exts       = dopt Opt_GlasgowExts dflags
 985
 986 -------------------------
 987 distinct_tyvars tys     -- Check that the types are all distinct type variables
 988   = all tcIsTyVarTy tys && null (findDupsEq tcEqType tys)
 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  = sep [ptext SLIT("Non-type variables, or repeated type variables,"),
1082                           nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1083 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1084
1085 arityErr kind name n m
1086   = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1087            n_arguments <> comma, text "but has been given", int m]
1088     where
1089         n_arguments | n == 0 = ptext SLIT("no arguments")
1090                     | n == 1 = ptext SLIT("1 argument")
1091                     | True   = hsep [int n, ptext SLIT("arguments")]
1092 \end{code}
1093
1094
1095 %************************************************************************
1096 %*                                                                      *
1097 \subsection{Checking for a decent instance head type}
1098 %*                                                                      *
1099 %************************************************************************
1100
1101 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1102 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1103
1104 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1105 flag is on, or (2)~the instance is imported (they must have been
1106 compiled elsewhere). In these cases, we let them go through anyway.
1107
1108 We can also have instances for functions: @instance Foo (a -> b) ...@.
1109
1110 \begin{code}
1111 checkValidInstHead :: Type -> TcM (Class, [TcType])
1112
1113 checkValidInstHead ty   -- Should be a source type
1114   = case tcSplitPredTy_maybe ty of {
1115         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1116         Just pred ->
1117
1118     case getClassPredTys_maybe pred of {
1119         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1120         Just (clas,tys) ->
1121
1122     getDOpts                                    `thenM` \ dflags ->
1123     mappM_ check_arg_type tys                   `thenM_`
1124     check_inst_head dflags clas tys             `thenM_`
1125     returnM (clas, tys)
1126     }}
1127
1128 check_inst_head dflags clas tys
1129         -- If GlasgowExts then check at least one isn't a type variable
1130   | dopt Opt_GlasgowExts dflags
1131   = check_tyvars dflags clas tys
1132
1133         -- WITH HASKELL 98, MUST HAVE C (T a b c)
1134   | isSingleton tys,
1135     tcValidInstHeadTy first_ty
1136   = returnM ()
1137
1138   | otherwise
1139   = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1140
1141   where
1142     (first_ty : _) = tys
1143
1144     head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1145                              text "where T is not a synonym, and a,b,c are distinct type variables")
1146
1147 check_tyvars dflags clas tys
1148         -- Check that at least one isn't a type variable
1149         -- unless -fallow-undecideable-instances
1150   | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1151   | not (all tcIsTyVarTy tys)                 = returnM ()
1152   | otherwise                                 = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1153   where
1154     msg =  parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1155                    $$ undecidableMsg)
1156
1157 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1158 \end{code}
1159
1160 \begin{code}
1161 instTypeErr pp_ty msg
1162   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1163          nest 4 msg]
1164 \end{code}