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