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