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