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                           tcEqType, 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, isTyVar,
  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 (NewTcApp tycon tys)       = mappM go tys        `thenM` \ tys' ->
 490                                     returnM (NewTcApp tycon tys')
 491
 492     go (NoteTy (SynNote ty1) ty2) = go ty1              `thenM` \ ty1' ->
 493                                     go ty2              `thenM` \ ty2' ->
 494                                     returnM (NoteTy (SynNote ty1') ty2')
 495
 496     go (NoteTy (FTVNote _) ty2)   = go ty2      -- Discard free-tyvar annotations
 497
 498     go (PredTy p)                 = go_pred p           `thenM` \ p' ->
 499                                     returnM (PredTy p')
 500
 501     go (FunTy arg res)            = go arg              `thenM` \ arg' ->
 502                                     go res              `thenM` \ res' ->
 503                                     returnM (FunTy arg' res')
 504
 505     go (AppTy fun arg)            = go fun              `thenM` \ fun' ->
 506                                     go arg              `thenM` \ arg' ->
 507                                     returnM (mkAppTy fun' arg')
 508                 -- NB the mkAppTy; we might have instantiated a
 509                 -- type variable to a type constructor, so we need
 510                 -- to pull the TyConApp to the top.
 511
 512         -- The two interesting cases!
 513     go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn rflag tyvar
 514
 515     go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
 516                              go ty              `thenM` \ ty' ->
 517                              returnM (ForAllTy tyvar ty')
 518
 519     go_pred (ClassP c tys) = mappM go tys       `thenM` \ tys' ->
 520                              returnM (ClassP c tys')
 521     go_pred (IParam n ty)  = go ty              `thenM` \ ty' ->
 522                              returnM (IParam n ty')
 523
 524 zonkTyVar :: (TcTyVar -> TcM Type)              -- What to do for an unbound mutable variable
 525           -> Bool                               -- Consult the type refinement?
 526           -> TcTyVar -> TcM TcType
 527 zonkTyVar unbound_var_fn rflag tyvar
 528   | not (isTcTyVar tyvar)       -- This can happen when
 529                                 -- zonking a forall type, when the bound type variable
 530                                 -- needn't be mutable
 531   = returnM (TyVarTy tyvar)
 532
 533   | otherwise
 534   =  condLookupTcTyVar rflag tyvar  `thenM` \ details ->
 535      case details of
 536           -- If b is true, the variable was refined, and therefore it is okay
 537           -- to continue refining inside.  Otherwise it was wobbly and we should
 538           -- not refine further inside.
 539           IndirectTv b ty -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
 540           FlexiTv         -> unbound_var_fn tyvar          -- Unbound flexi
 541           RigidTv         -> return (TyVarTy tyvar)       -- Rigid, no zonking necessary
 542 \end{code}
 543
 544
 545
 546 %************************************************************************
 547 %*                                                                      *
 548                         Zonking kinds
 549 %*                                                                      *
 550 %************************************************************************
 551
 552 \begin{code}
 553 readKindVar  :: KindVar -> TcM (Maybe TcKind)
 554 writeKindVar :: KindVar -> TcKind -> TcM ()
 555 readKindVar  (KVar _ ref)     = readMutVar ref
 556 writeKindVar (KVar _ ref) val = writeMutVar ref (Just val)
 557
 558 -------------
 559 zonkTcKind :: TcKind -> TcM TcKind
 560 zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
 561                                 ; k2' <- zonkTcKind k2
 562                                 ; returnM (FunKind k1' k2') }
 563 zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv
 564                                ; case mb_kind of
 565                                     Nothing -> returnM k
 566                                     Just k  -> zonkTcKind k }
 567 zonkTcKind other_kind = returnM other_kind
 568
 569 -------------
 570 zonkTcKindToKind :: TcKind -> TcM Kind
 571 zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
 572                                       ; k2' <- zonkTcKindToKind k2
 573                                       ; returnM (FunKind k1' k2') }
 574
 575 zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv
 576                                    ; case mb_kind of
 577                                        Nothing -> return liftedTypeKind
 578                                        Just k  -> zonkTcKindToKind k }
 579
 580 zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind  -- An "Open" kind defaults to *
 581 zonkTcKindToKind other_kind   = returnM other_kind
 582 \end{code}
 583
 584 %************************************************************************
 585 %*                                                                      *
 586 \subsection{Checking a user type}
 587 %*                                                                      *
 588 %************************************************************************
 589
 590 When dealing with a user-written type, we first translate it from an HsType
 591 to a Type, performing kind checking, and then check various things that should
 592 be true about it.  We don't want to perform these checks at the same time
 593 as the initial translation because (a) they are unnecessary for interface-file
 594 types and (b) when checking a mutually recursive group of type and class decls,
 595 we can't "look" at the tycons/classes yet.  Also, the checks are are rather
 596 diverse, and used to really mess up the other code.
 597
 598 One thing we check for is 'rank'.
 599
 600         Rank 0:         monotypes (no foralls)
 601         Rank 1:         foralls at the front only, Rank 0 inside
 602         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
 603
 604         basic ::= tyvar | T basic ... basic
 605
 606         r2  ::= forall tvs. cxt => r2a
 607         r2a ::= r1 -> r2a | basic
 608         r1  ::= forall tvs. cxt => r0
 609         r0  ::= r0 -> r0 | basic
 610
 611 Another thing is to check that type synonyms are saturated.
 612 This might not necessarily show up in kind checking.
 613         type A i = i
 614         data T k = MkT (k Int)
 615         f :: T A        -- BAD!
 616
 617
 618 \begin{code}
 619 data UserTypeCtxt
 620   = FunSigCtxt Name     -- Function type signature
 621   | ExprSigCtxt         -- Expression type signature
 622   | ConArgCtxt Name     -- Data constructor argument
 623   | TySynCtxt Name      -- RHS of a type synonym decl
 624   | GenPatCtxt          -- Pattern in generic decl
 625                         --      f{| a+b |} (Inl x) = ...
 626   | PatSigCtxt          -- Type sig in pattern
 627                         --      f (x::t) = ...
 628   | ResSigCtxt          -- Result type sig
 629                         --      f x :: t = ....
 630   | ForSigCtxt Name     -- Foreign inport or export signature
 631   | RuleSigCtxt Name    -- Signature on a forall'd variable in a RULE
 632   | DefaultDeclCtxt     -- Types in a default declaration
 633
 634 -- Notes re TySynCtxt
 635 -- We allow type synonyms that aren't types; e.g.  type List = []
 636 --
 637 -- If the RHS mentions tyvars that aren't in scope, we'll
 638 -- quantify over them:
 639 --      e.g.    type T = a->a
 640 -- will become  type T = forall a. a->a
 641 --
 642 -- With gla-exts that's right, but for H98 we should complain.
 643
 644
 645 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
 646 pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt (unLoc hs_ty) ctxt
 647
 648 pprUserTypeCtxt ty (FunSigCtxt n)  = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
 649 pprUserTypeCtxt ty ExprSigCtxt     = sep [ptext SLIT("In an expression type signature:"), nest 2 (ppr ty)]
 650 pprUserTypeCtxt ty (ConArgCtxt c)  = sep [ptext SLIT("In the type of the constructor"), pp_sig c ty]
 651 pprUserTypeCtxt ty (TySynCtxt c)   = sep [ptext SLIT("In the RHS of the type synonym") <+> quotes (ppr c) <> comma,
 652                                           nest 2 (ptext SLIT(", namely") <+> ppr ty)]
 653 pprUserTypeCtxt ty GenPatCtxt      = sep [ptext SLIT("In the type pattern of a generic definition:"), nest 2 (ppr ty)]
 654 pprUserTypeCtxt ty PatSigCtxt      = sep [ptext SLIT("In a pattern type signature:"), nest 2 (ppr ty)]
 655 pprUserTypeCtxt ty ResSigCtxt      = sep [ptext SLIT("In a result type signature:"), nest 2 (ppr ty)]
 656 pprUserTypeCtxt ty (ForSigCtxt n)  = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty]
 657 pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
 658 pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)]
 659
 660 pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
 661 \end{code}
 662
 663 \begin{code}
 664 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 665 -- Checks that the type is valid for the given context
 666 checkValidType ctxt ty
 667   = traceTc (text "checkValidType" <+> ppr ty)  `thenM_`
 668     doptM Opt_GlasgowExts       `thenM` \ gla_exts ->
 669     let
 670         rank | gla_exts = Arbitrary
 671              | otherwise
 672              = case ctxt of     -- Haskell 98
 673                  GenPatCtxt     -> Rank 0
 674                  PatSigCtxt     -> Rank 0
 675                  DefaultDeclCtxt-> Rank 0
 676                  ResSigCtxt     -> Rank 0
 677                  TySynCtxt _    -> Rank 0
 678                  ExprSigCtxt    -> Rank 1
 679                  FunSigCtxt _   -> Rank 1
 680                  ConArgCtxt _   -> Rank 1       -- We are given the type of the entire
 681                                                 -- constructor, hence rank 1
 682                  ForSigCtxt _   -> Rank 1
 683                  RuleSigCtxt _  -> Rank 1
 684
 685         actual_kind = typeKind ty
 686
 687         kind_ok = case ctxt of
 688                         TySynCtxt _  -> True    -- Any kind will do
 689                         ResSigCtxt   -> isOpenTypeKind   actual_kind
 690                         ExprSigCtxt  -> isOpenTypeKind   actual_kind
 691                         GenPatCtxt   -> isLiftedTypeKind actual_kind
 692                         ForSigCtxt _ -> isLiftedTypeKind actual_kind
 693                         other        -> isArgTypeKind       actual_kind
 694
 695         ubx_tup | not gla_exts = UT_NotOk
 696                 | otherwise    = case ctxt of
 697                                    TySynCtxt _ -> UT_Ok
 698                                    ExprSigCtxt -> UT_Ok
 699                                    other       -> UT_NotOk
 700                 -- Unboxed tuples ok in function results,
 701                 -- but for type synonyms we allow them even at
 702                 -- top level
 703     in
 704         -- Check that the thing has kind Type, and is lifted if necessary
 705     checkTc kind_ok (kindErr actual_kind)       `thenM_`
 706
 707         -- Check the internal validity of the type itself
 708     check_poly_type rank ubx_tup ty             `thenM_`
 709
 710     traceTc (text "checkValidType done" <+> ppr ty)
 711 \end{code}
 712
 713
 714 \begin{code}
 715 data Rank = Rank Int | Arbitrary
 716
 717 decRank :: Rank -> Rank
 718 decRank Arbitrary = Arbitrary
 719 decRank (Rank n)  = Rank (n-1)
 720
 721 ----------------------------------------
 722 data UbxTupFlag = UT_Ok | UT_NotOk
 723         -- The "Ok" version means "ok if -fglasgow-exts is on"
 724
 725 ----------------------------------------
 726 check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 727 check_poly_type (Rank 0) ubx_tup ty
 728   = check_tau_type (Rank 0) ubx_tup ty
 729
 730 check_poly_type rank ubx_tup ty
 731   = let
 732         (tvs, theta, tau) = tcSplitSigmaTy ty
 733     in
 734     check_valid_theta SigmaCtxt theta           `thenM_`
 735     check_tau_type (decRank rank) ubx_tup tau   `thenM_`
 736     checkFreeness tvs theta                     `thenM_`
 737     checkAmbiguity tvs theta (tyVarsOfType tau)
 738
 739 ----------------------------------------
 740 check_arg_type :: Type -> TcM ()
 741 -- The sort of type that can instantiate a type variable,
 742 -- or be the argument of a type constructor.
 743 -- Not an unboxed tuple, not a forall.
 744 -- Other unboxed types are very occasionally allowed as type
 745 -- arguments depending on the kind of the type constructor
 746 --
 747 -- For example, we want to reject things like:
 748 --
 749 --      instance Ord a => Ord (forall s. T s a)
 750 -- and
 751 --      g :: T s (forall b.b)
 752 --
 753 -- NB: unboxed tuples can have polymorphic or unboxed args.
 754 --     This happens in the workers for functions returning
 755 --     product types with polymorphic components.
 756 --     But not in user code.
 757 -- Anyway, they are dealt with by a special case in check_tau_type
 758
 759 check_arg_type ty
 760   = check_tau_type (Rank 0) UT_NotOk ty         `thenM_`
 761     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 762
 763 ----------------------------------------
 764 check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 765 -- Rank is allowed rank for function args
 766 -- No foralls otherwise
 767
 768 check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
 769 check_tau_type rank ubx_tup (PredTy sty)    = getDOpts          `thenM` \ dflags ->
 770                                                 check_source_ty dflags TypeCtxt sty
 771 check_tau_type rank ubx_tup (TyVarTy _)       = returnM ()
 772 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
 773   = check_poly_type rank UT_NotOk arg_ty        `thenM_`
 774     check_tau_type  rank UT_Ok    res_ty
 775
 776 check_tau_type rank ubx_tup (AppTy ty1 ty2)
 777   = check_arg_type ty1 `thenM_` check_arg_type ty2
 778
 779 check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
 780         -- Synonym notes are built only when the synonym is
 781         -- saturated (see Type.mkSynTy)
 782   = doptM Opt_GlasgowExts                       `thenM` \ gla_exts ->
 783     (if gla_exts then
 784         -- If -fglasgow-exts then don't check the 'note' part.
 785         -- This  allows us to instantiate a synonym defn with a
 786         -- for-all type, or with a partially-applied type synonym.
 787         --      e.g.   type T a b = a
 788         --             type S m   = m ()
 789         --             f :: S (T Int)
 790         -- Here, T is partially applied, so it's illegal in H98.
 791         -- But if you expand S first, then T we get just
 792         --             f :: Int
 793         -- which is fine.
 794         returnM ()
 795     else
 796         -- For H98, do check the un-expanded part
 797         check_tau_type rank ubx_tup syn
 798     )                                           `thenM_`
 799
 800     check_tau_type rank ubx_tup ty
 801
 802 check_tau_type rank ubx_tup (NoteTy other_note ty)
 803   = check_tau_type rank ubx_tup ty
 804
 805 check_tau_type rank ubx_tup (NewTcApp tc tys)
 806   = mappM_ check_arg_type tys
 807
 808 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
 809   | isSynTyCon tc
 810   =     -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
 811         -- synonym application, leaving it to checkValidType (i.e. right here)
 812         -- to find the error
 813     checkTc syn_arity_ok arity_msg      `thenM_`
 814     mappM_ check_arg_type tys
 815
 816   | isUnboxedTupleTyCon tc
 817   = doptM Opt_GlasgowExts                       `thenM` \ gla_exts ->
 818     checkTc (ubx_tup_ok gla_exts) ubx_tup_msg   `thenM_`
 819     mappM_ (check_tau_type (Rank 0) UT_Ok) tys
 820                 -- Args are allowed to be unlifted, or
 821                 -- more unboxed tuples, so can't use check_arg_ty
 822
 823   | otherwise
 824   = mappM_ check_arg_type tys
 825
 826   where
 827     ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
 828
 829     syn_arity_ok = tc_arity <= n_args
 830                 -- It's OK to have an *over-applied* type synonym
 831                 --      data Tree a b = ...
 832                 --      type Foo a = Tree [a]
 833                 --      f :: Foo a b -> ...
 834     n_args    = length tys
 835     tc_arity  = tyConArity tc
 836
 837     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
 838     ubx_tup_msg = ubxArgTyErr ty
 839
 840 ----------------------------------------
 841 forAllTyErr     ty = ptext SLIT("Illegal polymorphic type:") <+> ppr ty
 842 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
 843 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
 844 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 845 \end{code}
 846
 847
 848
 849 %************************************************************************
 850 %*                                                                      *
 851 \subsection{Checking a theta or source type}
 852 %*                                                                      *
 853 %************************************************************************
 854
 855 \begin{code}
 856 -- Enumerate the contexts in which a "source type", <S>, can occur
 857 --      Eq a
 858 -- or   ?x::Int
 859 -- or   r <: {x::Int}
 860 -- or   (N a) where N is a newtype
 861
 862 data SourceTyCtxt
 863   = ClassSCCtxt Name    -- Superclasses of clas
 864                         --      class <S> => C a where ...
 865   | SigmaCtxt           -- Theta part of a normal for-all type
 866                         --      f :: <S> => a -> a
 867   | DataTyCtxt Name     -- Theta part of a data decl
 868                         --      data <S> => T a = MkT a
 869   | TypeCtxt            -- Source type in an ordinary type
 870                         --      f :: N a -> N a
 871   | InstThetaCtxt       -- Context of an instance decl
 872                         --      instance <S> => C [a] where ...
 873   | InstHeadCtxt        -- Head of an instance decl
 874                         --      instance ... => Eq a where ...
 875
 876 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
 877 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
 878 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
 879 pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
 880 pprSourceTyCtxt InstHeadCtxt    = ptext SLIT("the head of an instance declaration")
 881 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
 882 \end{code}
 883
 884 \begin{code}
 885 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
 886 checkValidTheta ctxt theta
 887   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
 888
 889 -------------------------
 890 check_valid_theta ctxt []
 891   = returnM ()
 892 check_valid_theta ctxt theta
 893   = getDOpts                                    `thenM` \ dflags ->
 894     warnTc (notNull dups) (dupPredWarn dups)    `thenM_`
 895         -- Actually, in instance decls and type signatures,
 896         -- duplicate constraints are eliminated by TcHsType.hoistForAllTys,
 897         -- so this error can only fire for the context of a class or
 898         -- data type decl.
 899     mappM_ (check_source_ty dflags ctxt) theta
 900   where
 901     (_,dups) = removeDups tcCmpPred theta
 902
 903 -------------------------
 904 check_source_ty dflags ctxt pred@(ClassP cls tys)
 905   =     -- Class predicates are valid in all contexts
 906     checkTc (arity == n_tys) arity_err          `thenM_`
 907
 908         -- Check the form of the argument types
 909     mappM_ check_arg_type tys                           `thenM_`
 910     checkTc (check_class_pred_tys dflags ctxt tys)
 911             (predTyVarErr pred $$ how_to_allow)
 912
 913   where
 914     class_name = className cls
 915     arity      = classArity cls
 916     n_tys      = length tys
 917     arity_err  = arityErr "Class" class_name arity n_tys
 918
 919     how_to_allow = case ctxt of
 920                      InstHeadCtxt  -> empty     -- Should not happen
 921                      InstThetaCtxt -> parens undecidableMsg
 922                      other         -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 923
 924 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
 925         -- Implicit parameters only allows in type
 926         -- signatures; not in instance decls, superclasses etc
 927         -- The reason for not allowing implicit params in instances is a bit subtle
 928         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
 929         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
 930         -- discharge all the potential usas of the ?x in e.   For example, a
 931         -- constraint Foo [Int] might come out of e,and applying the
 932         -- instance decl would show up two uses of ?x.
 933
 934 -- Catch-all
 935 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 936
 937 -------------------------
 938 check_class_pred_tys dflags ctxt tys
 939   = case ctxt of
 940         InstHeadCtxt  -> True   -- We check for instance-head
 941                                 -- formation in checkValidInstHead
 942         InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys
 943         other         -> gla_exts       || all tyvar_head tys
 944   where
 945     undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
 946     gla_exts       = dopt Opt_GlasgowExts dflags
 947
 948 -------------------------
 949 tyvar_head ty                   -- Haskell 98 allows predicates of form
 950   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
 951   | otherwise                   -- where a is a type variable
 952   = case tcSplitAppTy_maybe ty of
 953         Just (ty, _) -> tyvar_head ty
 954         Nothing      -> False
 955 \end{code}
 956
 957 Check for ambiguity
 958 ~~~~~~~~~~~~~~~~~~~
 959           forall V. P => tau
 960 is ambiguous if P contains generic variables
 961 (i.e. one of the Vs) that are not mentioned in tau
 962
 963 However, we need to take account of functional dependencies
 964 when we speak of 'mentioned in tau'.  Example:
 965         class C a b | a -> b where ...
 966 Then the type
 967         forall x y. (C x y) => x
 968 is not ambiguous because x is mentioned and x determines y
 969
 970 NB; the ambiguity check is only used for *user* types, not for types
 971 coming from inteface files.  The latter can legitimately have
 972 ambiguous types. Example
 973
 974    class S a where s :: a -> (Int,Int)
 975    instance S Char where s _ = (1,1)
 976    f:: S a => [a] -> Int -> (Int,Int)
 977    f (_::[a]) x = (a*x,b)
 978         where (a,b) = s (undefined::a)
 979
 980 Here the worker for f gets the type
 981         fw :: forall a. S a => Int -> (# Int, Int #)
 982
 983 If the list of tv_names is empty, we have a monotype, and then we
 984 don't need to check for ambiguity either, because the test can't fail
 985 (see is_ambig).
 986
 987 \begin{code}
 988 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
 989 checkAmbiguity forall_tyvars theta tau_tyvars
 990   = mappM_ complain (filter is_ambig theta)
 991   where
 992     complain pred     = addErrTc (ambigErr pred)
 993     extended_tau_vars = grow theta tau_tyvars
 994
 995         -- Only a *class* predicate can give rise to ambiguity
 996         -- An *implicit parameter* cannot.  For example:
 997         --      foo :: (?x :: [a]) => Int
 998         --      foo = length ?x
 999         -- is fine.  The call site will suppply a particular 'x'
1000     is_ambig pred     = isClassPred  pred &&
1001                         any ambig_var (varSetElems (tyVarsOfPred pred))
1002
1003     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
1004                         not (ct_var `elemVarSet` extended_tau_vars)
1005
1006 ambigErr pred
1007   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1008          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1009                  ptext SLIT("must be reachable from the type after the '=>'"))]
1010 \end{code}
1011
1012 In addition, GHC insists that at least one type variable
1013 in each constraint is in V.  So we disallow a type like
1014         forall a. Eq b => b -> b
1015 even in a scope where b is in scope.
1016
1017 \begin{code}
1018 checkFreeness forall_tyvars theta
1019   = mappM_ complain (filter is_free theta)
1020   where
1021     is_free pred     =  not (isIPPred pred)
1022                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1023     bound_var ct_var = ct_var `elem` forall_tyvars
1024     complain pred    = addErrTc (freeErr pred)
1025
1026 freeErr pred
1027   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1028                    ptext SLIT("are already in scope"),
1029          nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1030     ]
1031 \end{code}
1032
1033 \begin{code}
1034 checkThetaCtxt ctxt theta
1035   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1036           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1037
1038 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1039 predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
1040 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1041
1042 arityErr kind name n m
1043   = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1044            n_arguments <> comma, text "but has been given", int m]
1045     where
1046         n_arguments | n == 0 = ptext SLIT("no arguments")
1047                     | n == 1 = ptext SLIT("1 argument")
1048                     | True   = hsep [int n, ptext SLIT("arguments")]
1049 \end{code}
1050
1051
1052 %************************************************************************
1053 %*                                                                      *
1054 \subsection{Checking for a decent instance head type}
1055 %*                                                                      *
1056 %************************************************************************
1057
1058 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1059 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1060
1061 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1062 flag is on, or (2)~the instance is imported (they must have been
1063 compiled elsewhere). In these cases, we let them go through anyway.
1064
1065 We can also have instances for functions: @instance Foo (a -> b) ...@.
1066
1067 \begin{code}
1068 checkValidInstHead :: Type -> TcM (Class, [TcType])
1069
1070 checkValidInstHead ty   -- Should be a source type
1071   = case tcSplitPredTy_maybe ty of {
1072         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1073         Just pred ->
1074
1075     case getClassPredTys_maybe pred of {
1076         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1077         Just (clas,tys) ->
1078
1079     getDOpts                                    `thenM` \ dflags ->
1080     mappM_ check_arg_type tys                   `thenM_`
1081     check_inst_head dflags clas tys             `thenM_`
1082     returnM (clas, tys)
1083     }}
1084
1085 check_inst_head dflags clas tys
1086         -- If GlasgowExts then check at least one isn't a type variable
1087   | dopt Opt_GlasgowExts dflags
1088   = check_tyvars dflags clas tys
1089
1090         -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
1091   | isSingleton tys,
1092     Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
1093     not (isSynTyCon tycon),             -- ...but not a synonym
1094     all tcIsTyVarTy arg_tys,            -- Applied to type variables
1095     equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
1096           -- This last condition checks that all the type variables are distinct
1097   = returnM ()
1098
1099   | otherwise
1100   = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
1101
1102   where
1103     (first_ty : _)       = tys
1104
1105     head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1106                              text "where T is not a synonym, and a,b,c are distinct type variables")
1107
1108 check_tyvars dflags clas tys
1109         -- Check that at least one isn't a type variable
1110         -- unless -fallow-undecideable-instances
1111   | dopt Opt_AllowUndecidableInstances dflags = returnM ()
1112   | not (all tcIsTyVarTy tys)                 = returnM ()
1113   | otherwise                                 = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1114   where
1115     msg =  parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1116                    $$ undecidableMsg)
1117
1118 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1119 \end{code}
1120
1121 \begin{code}
1122 instTypeErr pp_ty msg
1123   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1124          nest 4 msg]
1125 \end{code}