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