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