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