ghc/compiler/typecheck/TcMType.lhs

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