compiler/typecheck/TcMType.lhs

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