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 inot ano 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 check_tau_type rank ubx_tup ty@(PredTy _) = pprPanic "check_tau_type" (ppr ty)
 768
 769 check_tau_type rank ubx_tup (TyVarTy _)       = returnM ()
 770 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
 771   = check_poly_type rank UT_NotOk arg_ty        `thenM_`
 772     check_tau_type  rank UT_Ok    res_ty
 773
 774 check_tau_type rank ubx_tup (AppTy ty1 ty2)
 775   = check_arg_type ty1 `thenM_` check_arg_type ty2
 776
 777 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
 778         -- Synonym notes are built only when the synonym is
 779         -- saturated (see Type.mkSynTy)
 780   = doptM Opt_GlasgowExts                       `thenM` \ gla_exts ->
 781     (if gla_exts then
 782         -- If -fglasgow-exts then don't check the 'note' part.
 783         -- This  allows us to instantiate a synonym defn with a
 784         -- for-all type, or with a partially-applied type synonym.
 785         --      e.g.   type T a b = a
 786         --             type S m   = m ()
 787         --             f :: S (T Int)
 788         -- Here, T is partially applied, so it's illegal in H98.
 789         -- But if you expand S first, then T we get just
 790         --             f :: Int
 791         -- which is fine.
 792         returnM ()
 793     else
 794         -- For H98, do check the un-expanded part
 795         check_tau_type rank ubx_tup syn
 796     )                                           `thenM_`
 797
 798     check_tau_type rank ubx_tup ty
 799
 800 check_tau_type rank ubx_tup (NoteTy other_note ty)
 801   = check_tau_type rank ubx_tup ty
 802
 803 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
 804   | isSynTyCon tc
 805   =     -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
 806         -- synonym application, leaving it to checkValidType (i.e. right here)
 807         -- to find the error
 808     checkTc syn_arity_ok arity_msg      `thenM_`
 809     mappM_ check_arg_type tys
 810
 811   | isUnboxedTupleTyCon tc
 812   = doptM Opt_GlasgowExts                       `thenM` \ gla_exts ->
 813     checkTc (ubx_tup_ok gla_exts) ubx_tup_msg   `thenM_`
 814     mappM_ (check_tau_type (Rank 0) UT_Ok) tys
 815                 -- Args are allowed to be unlifted, or
 816                 -- more unboxed tuples, so can't use check_arg_ty
 817
 818   | otherwise
 819   = mappM_ check_arg_type tys
 820
 821   where
 822     ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
 823
 824     syn_arity_ok = tc_arity <= n_args
 825                 -- It's OK to have an *over-applied* type synonym
 826                 --      data Tree a b = ...
 827                 --      type Foo a = Tree [a]
 828                 --      f :: Foo a b -> ...
 829     n_args    = length tys
 830     tc_arity  = tyConArity tc
 831
 832     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
 833     ubx_tup_msg = ubxArgTyErr ty
 834
 835 ----------------------------------------
 836 forAllTyErr     ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
 837 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
 838 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
 839 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 840 \end{code}
 841
 842
 843
 844 %************************************************************************
 845 %*                                                                      *
 846 \subsection{Checking a theta or source type}
 847 %*                                                                      *
 848 %************************************************************************
 849
 850 \begin{code}
 851 -- Enumerate the contexts in which a "source type", <S>, can occur
 852 --      Eq a
 853 -- or   ?x::Int
 854 -- or   r <: {x::Int}
 855 -- or   (N a) where N is a newtype
 856
 857 data SourceTyCtxt
 858   = ClassSCCtxt Name    -- Superclasses of clas
 859                         --      class <S> => C a where ...
 860   | SigmaCtxt           -- Theta part of a normal for-all type
 861                         --      f :: <S> => a -> a
 862   | DataTyCtxt Name     -- Theta part of a data decl
 863                         --      data <S> => T a = MkT a
 864   | TypeCtxt            -- Source type in an ordinary type
 865                         --      f :: N a -> N a
 866   | InstThetaCtxt       -- Context of an instance decl
 867                         --      instance <S> => C [a] where ...
 868   | InstHeadCtxt        -- Head of an instance decl
 869                         --      instance ... => Eq a where ...
 870
 871 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
 872 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
 873 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
 874 pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
 875 pprSourceTyCtxt InstHeadCtxt    = ptext SLIT("the head of an instance declaration")
 876 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
 877 \end{code}
 878
 879 \begin{code}
 880 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
 881 checkValidTheta ctxt theta
 882   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
 883
 884 -------------------------
 885 check_valid_theta ctxt []
 886   = returnM ()
 887 check_valid_theta ctxt theta
 888   = getDOpts                                    `thenM` \ dflags ->
 889     warnTc (notNull dups) (dupPredWarn dups)    `thenM_`
 890         -- Actually, in instance decls and type signatures,
 891         -- duplicate constraints are eliminated by TcHsType.hoistForAllTys,
 892         -- so this error can only fire for the context of a class or
 893         -- data type decl.
 894     mappM_ (check_source_ty dflags ctxt) theta
 895   where
 896     (_,dups) = removeDups tcCmpPred theta
 897
 898 -------------------------
 899 check_source_ty dflags ctxt pred@(ClassP cls tys)
 900   =     -- Class predicates are valid in all contexts
 901     checkTc (arity == n_tys) arity_err          `thenM_`
 902
 903         -- Check the form of the argument types
 904     mappM_ check_arg_type tys                           `thenM_`
 905     checkTc (check_class_pred_tys dflags ctxt tys)
 906             (predTyVarErr pred $$ how_to_allow)
 907
 908   where
 909     class_name = className cls
 910     arity      = classArity cls
 911     n_tys      = length tys
 912     arity_err  = arityErr "Class" class_name arity n_tys
 913
 914     how_to_allow = case ctxt of
 915                      InstHeadCtxt  -> empty     -- Should not happen
 916                      InstThetaCtxt -> parens undecidableMsg
 917                      other         -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 918
 919 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
 920         -- Implicit parameters only allows in type
 921         -- signatures; not in instance decls, superclasses etc
 922         -- The reason for not allowing implicit params in instances is a bit subtle
 923         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
 924         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
 925         -- discharge all the potential usas of the ?x in e.   For example, a
 926         -- constraint Foo [Int] might come out of e,and applying the
 927         -- instance decl would show up two uses of ?x.
 928
 929 -- Catch-all
 930 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 931
 932 -------------------------
 933 check_class_pred_tys dflags ctxt tys
 934   = case ctxt of
 935         InstHeadCtxt  -> True   -- We check for instance-head
 936                                 -- formation in checkValidInstHead
 937         InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys
 938         other         -> gla_exts       || all tyvar_head tys
 939   where
 940     undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
 941     gla_exts       = dopt Opt_GlasgowExts dflags
 942
 943 -------------------------
 944 tyvar_head ty                   -- Haskell 98 allows predicates of form
 945   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
 946   | otherwise                   -- where a is a type variable
 947   = case tcSplitAppTy_maybe ty of
 948         Just (ty, _) -> tyvar_head ty
 949         Nothing      -> False
 950 \end{code}
 951
 952 Check for ambiguity
 953 ~~~~~~~~~~~~~~~~~~~
 954           forall V. P => tau
 955 is ambiguous if P contains generic variables
 956 (i.e. one of the Vs) that are not mentioned in tau
 957
 958 However, we need to take account of functional dependencies
 959 when we speak of 'mentioned in tau'.  Example:
 960         class C a b | a -> b where ...
 961 Then the type
 962         forall x y. (C x y) => x
 963 is not ambiguous because x is mentioned and x determines y
 964
 965 NB; the ambiguity check is only used for *user* types, not for types
 966 coming from inteface files.  The latter can legitimately have
 967 ambiguous types. Example
 968
 969    class S a where s :: a -> (Int,Int)
 970    instance S Char where s _ = (1,1)
 971    f:: S a => [a] -> Int -> (Int,Int)
 972    f (_::[a]) x = (a*x,b)
 973         where (a,b) = s (undefined::a)
 974
 975 Here the worker for f gets the type
 976         fw :: forall a. S a => Int -> (# Int, Int #)
 977
 978 If the list of tv_names is empty, we have a monotype, and then we
 979 don't need to check for ambiguity either, because the test can't fail
 980 (see is_ambig).
 981
 982 \begin{code}
 983 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
 984 checkAmbiguity forall_tyvars theta tau_tyvars
 985   = mappM_ complain (filter is_ambig theta)
 986   where
 987     complain pred     = addErrTc (ambigErr pred)
 988     extended_tau_vars = grow theta tau_tyvars
 989
 990         -- Only a *class* predicate can give rise to ambiguity
 991         -- An *implicit parameter* cannot.  For example:
 992         --      foo :: (?x :: [a]) => Int
 993         --      foo = length ?x
 994         -- is fine.  The call site will suppply a particular 'x'
 995     is_ambig pred     = isClassPred  pred &&
 996                         any ambig_var (varSetElems (tyVarsOfPred pred))
 997
 998     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
 999                         not (ct_var `elemVarSet` extended_tau_vars)
1000
1001 ambigErr pred
1002   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1003          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1004                  ptext SLIT("must be reachable from the type after the '=>'"))]
1005 \end{code}
1006
1007 In addition, GHC insists that at least one type variable
1008 in each constraint is in V.  So we disallow a type like
1009         forall a. Eq b => b -> b
1010 even in a scope where b is in scope.
1011
1012 \begin{code}
1013 checkFreeness forall_tyvars theta
1014   = mappM_ complain (filter is_free theta)
1015   where
1016     is_free pred     =  not (isIPPred pred)
1017                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1018     bound_var ct_var = ct_var `elem` forall_tyvars
1019     complain pred    = addErrTc (freeErr pred)
1020
1021 freeErr pred
1022   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1023                    ptext SLIT("are already in scope"),
1024          nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1025     ]
1026 \end{code}
1027
1028 \begin{code}
1029 checkThetaCtxt ctxt theta
1030   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1031           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1032
1033 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1034 predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
1035 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1036
1037 arityErr kind name n m
1038   = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1039            n_arguments <> comma, text "but has been given", int m]
1040     where
1041         n_arguments | n == 0 = ptext SLIT("no arguments")
1042                     | n == 1 = ptext SLIT("1 argument")
1043                     | True   = hsep [int n, ptext SLIT("arguments")]
1044 \end{code}
1045
1046
1047 %************************************************************************
1048 %*                                                                      *
1049 \subsection{Checking for a decent instance head type}
1050 %*                                                                      *
1051 %************************************************************************
1052
1053 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1054 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1055
1056 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1057 flag is on, or (2)~the instance is imported (they must have been
1058 compiled elsewhere). In these cases, we let them go through anyway.
1059
1060 We can also have instances for functions: @instance Foo (a -> b) ...@.
1061
1062 \begin{code}
1063 checkValidInstHead :: Type -> TcM (Class, [TcType])
1064
1065 checkValidInstHead ty   -- Should be a source type
1066   = case tcSplitPredTy_maybe ty of {
1067         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1068         Just pred ->
1069
1070     case getClassPredTys_maybe pred of {
1071         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1072         Just (clas,tys) ->
1073
1074     getDOpts                                    `thenM` \ dflags ->
1075     mappM_ check_arg_type tys                   `thenM_`
1076     check_inst_head dflags clas tys             `thenM_`
1077     returnM (clas, tys)
1078     }}
1079
1080 check_inst_head dflags clas tys
1081         -- If GlasgowExts then check at least one isn't a type variable
1082   | dopt Opt_GlasgowExts dflags
1083   = check_tyvars dflags clas tys
1084
1085         -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1086   | isSingleton tys,
1087     Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1088     not (isSynTyCon tycon),             -- ...but not a synonym
1089     all tcIsTyVarTy arg_tys,            -- Applied to type variables
1090     equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1091           -- This last condition checks that all the type variables are distinct
1092   = returnM ()
1093
1094   | otherwise
1095   = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1096
1097   where
1098     (first_ty : _)       = tys
1099
1100     head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1101                              text "where T is not a synonym, and a,b,c are distinct type variables")
1102
1103 check_tyvars dflags clas tys
1104         -- Check that at least one isn't a type variable
1105         -- unless -fallow-undecideable-instances
1106   | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1107   | not (all tcIsTyVarTy tys)                 = returnM ()
1108   | otherwise                                 = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1109   where
1110     msg =  parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1111                    $$ undecidableMsg)
1112
1113 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1114 \end{code}
1115
1116 \begin{code}
1117 instTypeErr pp_ty msg
1118   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1119          nest 4 msg]
1120 \end{code}