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   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 dflags ctxt pred@(ClassP cls tys)
 939   = do {        -- Class predicates are valid in all contexts
 940        ; checkTc (arity == n_tys) arity_err
 941
 942                 -- Check the form of the argument types
 943        ; mappM_ check_arg_type tys
 944        ; checkTc (check_class_pred_tys dflags ctxt tys)
 945                  (predTyVarErr pred $$ how_to_allow)
 946        }
 947   where
 948     class_name = className cls
 949     arity      = classArity cls
 950     n_tys      = length tys
 951     arity_err  = arityErr "Class" class_name arity n_tys
 952     how_to_allow = parens (ptext SLIT("Use -XFlexibleContexts to permit this"))
 953
 954 check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
 955   = do {        -- Equational constraints are valid in all contexts if type
 956                 -- families are permitted
 957        ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
 958
 959                 -- Check the form of the argument types
 960        ; check_eq_arg_type ty1
 961        ; check_eq_arg_type ty2
 962        }
 963   where
 964     check_eq_arg_type = check_poly_type (Rank 0) UT_NotOk
 965
 966 check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
 967         -- Implicit parameters only allowed in type
 968         -- signatures; not in instance decls, superclasses etc
 969         -- The reason for not allowing implicit params in instances is a bit
 970         -- subtle.
 971         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
 972         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
 973         -- discharge all the potential usas of the ?x in e.   For example, a
 974         -- constraint Foo [Int] might come out of e,and applying the
 975         -- instance decl would show up two uses of ?x.
 976
 977 -- Catch-all
 978 check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
 979
 980 -------------------------
 981 check_class_pred_tys dflags ctxt tys
 982   = case ctxt of
 983         TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
 984         InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
 985                                 -- Further checks on head and theta in
 986                                 -- checkInstTermination
 987         other         -> flexible_contexts || all tyvar_head tys
 988   where
 989     flexible_contexts = dopt Opt_FlexibleContexts dflags
 990     undecidable_ok = dopt Opt_UndecidableInstances dflags
 991
 992 -------------------------
 993 tyvar_head ty                   -- Haskell 98 allows predicates of form
 994   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
 995   | otherwise                   -- where a is a type variable
 996   = case tcSplitAppTy_maybe ty of
 997         Just (ty, _) -> tyvar_head ty
 998         Nothing      -> False
 999 \end{code}
1000
1001 Check for ambiguity
1002 ~~~~~~~~~~~~~~~~~~~
1003           forall V. P => tau
1004 is ambiguous if P contains generic variables
1005 (i.e. one of the Vs) that are not mentioned in tau
1006
1007 However, we need to take account of functional dependencies
1008 when we speak of 'mentioned in tau'.  Example:
1009         class C a b | a -> b where ...
1010 Then the type
1011         forall x y. (C x y) => x
1012 is not ambiguous because x is mentioned and x determines y
1013
1014 NB; the ambiguity check is only used for *user* types, not for types
1015 coming from inteface files.  The latter can legitimately have
1016 ambiguous types. Example
1017
1018    class S a where s :: a -> (Int,Int)
1019    instance S Char where s _ = (1,1)
1020    f:: S a => [a] -> Int -> (Int,Int)
1021    f (_::[a]) x = (a*x,b)
1022         where (a,b) = s (undefined::a)
1023
1024 Here the worker for f gets the type
1025         fw :: forall a. S a => Int -> (# Int, Int #)
1026
1027 If the list of tv_names is empty, we have a monotype, and then we
1028 don't need to check for ambiguity either, because the test can't fail
1029 (see is_ambig).
1030
1031 \begin{code}
1032 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1033 checkAmbiguity forall_tyvars theta tau_tyvars
1034   = mappM_ complain (filter is_ambig theta)
1035   where
1036     complain pred     = addErrTc (ambigErr pred)
1037     extended_tau_vars = grow theta tau_tyvars
1038
1039         -- Only a *class* predicate can give rise to ambiguity
1040         -- An *implicit parameter* cannot.  For example:
1041         --      foo :: (?x :: [a]) => Int
1042         --      foo = length ?x
1043         -- is fine.  The call site will suppply a particular 'x'
1044     is_ambig pred     = isClassPred  pred &&
1045                         any ambig_var (varSetElems (tyVarsOfPred pred))
1046
1047     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
1048                         not (ct_var `elemVarSet` extended_tau_vars)
1049
1050 ambigErr pred
1051   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1052          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1053                  ptext SLIT("must be reachable from the type after the '=>'"))]
1054 \end{code}
1055
1056 In addition, GHC insists that at least one type variable
1057 in each constraint is in V.  So we disallow a type like
1058         forall a. Eq b => b -> b
1059 even in a scope where b is in scope.
1060
1061 \begin{code}
1062 checkFreeness forall_tyvars theta
1063   = do  { flexible_contexts <- doptM Opt_FlexibleContexts
1064         ; unless flexible_contexts $ mappM_ complain (filter is_free theta) }
1065   where
1066     is_free pred     =  not (isIPPred pred)
1067                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1068     bound_var ct_var = ct_var `elem` forall_tyvars
1069     complain pred    = addErrTc (freeErr pred)
1070
1071 freeErr pred
1072   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
1073                    ptext SLIT("are already in scope"),
1074          nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
1075     ]
1076 \end{code}
1077
1078 \begin{code}
1079 checkThetaCtxt ctxt theta
1080   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1081           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1082
1083 badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1084 eqPredTyErr  sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty
1085                    $$
1086                    parens (ptext SLIT("Use -ftype-families to permit this"))
1087 predTyVarErr pred  = sep [ptext SLIT("Non type-variable argument"),
1088                           nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1089 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1090
1091 arityErr kind name n m
1092   = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1093            n_arguments <> comma, text "but has been given", int m]
1094     where
1095         n_arguments | n == 0 = ptext SLIT("no arguments")
1096                     | n == 1 = ptext SLIT("1 argument")
1097                     | True   = hsep [int n, ptext SLIT("arguments")]
1098 \end{code}
1099
1100
1101 %************************************************************************
1102 %*                                                                      *
1103 \subsection{Checking for a decent instance head type}
1104 %*                                                                      *
1105 %************************************************************************
1106
1107 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1108 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1109
1110 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1111 flag is on, or (2)~the instance is imported (they must have been
1112 compiled elsewhere). In these cases, we let them go through anyway.
1113
1114 We can also have instances for functions: @instance Foo (a -> b) ...@.
1115
1116 \begin{code}
1117 checkValidInstHead :: Type -> TcM (Class, [TcType])
1118
1119 checkValidInstHead ty   -- Should be a source type
1120   = case tcSplitPredTy_maybe ty of {
1121         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1122         Just pred ->
1123
1124     case getClassPredTys_maybe pred of {
1125         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1126         Just (clas,tys) ->
1127
1128     getDOpts                                    `thenM` \ dflags ->
1129     mappM_ check_arg_type tys                   `thenM_`
1130     check_inst_head dflags clas tys             `thenM_`
1131     returnM (clas, tys)
1132     }}
1133
1134 check_inst_head dflags clas tys
1135         -- If GlasgowExts then check at least one isn't a type variable
1136   = do checkTc (dopt Opt_TypeSynonymInstances dflags ||
1137                 all tcInstHeadTyNotSynonym tys)
1138                (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
1139        checkTc (dopt Opt_FlexibleInstances dflags ||
1140                 all tcInstHeadTyAppAllTyVars tys)
1141                (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
1142        checkTc (dopt Opt_MultiParamTypeClasses dflags ||
1143                 isSingleton tys)
1144                (instTypeErr (pprClassPred clas tys) head_one_type_msg)
1145        mapM_ check_one tys
1146   where
1147     head_type_synonym_msg = parens (
1148                 text "All instance types must be of the form (T t1 ... tn)" $$
1149                 text "where T is not a synonym." $$
1150                 text "Use -XTypeSynonymInstances if you want to disable this.")
1151
1152     head_type_args_tyvars_msg = parens (
1153                 text "All instance types must be of the form (T a1 ... an)" $$
1154                 text "where a1 ... an are distinct type *variables*" $$
1155                 text "Use -XFlexibleInstances if you want to disable this.")
1156
1157     head_one_type_msg = parens (
1158                 text "Only one type can be given in an instance head." $$
1159                 text "Use -XMultiParamTypeClasses if you want to allow more.")
1160
1161         -- For now, I only allow tau-types (not polytypes) in
1162         -- the head of an instance decl.
1163         --      E.g.  instance C (forall a. a->a) is rejected
1164         -- One could imagine generalising that, but I'm not sure
1165         -- what all the consequences might be
1166     check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
1167                       ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1168
1169 instTypeErr pp_ty msg
1170   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1171          nest 4 msg]
1172 \end{code}
1173
1174
1175 %************************************************************************
1176 %*                                                                      *
1177 \subsection{Checking instance for termination}
1178 %*                                                                      *
1179 %************************************************************************
1180
1181
1182 \begin{code}
1183 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1184 checkValidInstance tyvars theta clas inst_tys
1185   = do  { undecidable_ok <- doptM Opt_UndecidableInstances
1186
1187         ; checkValidTheta InstThetaCtxt theta
1188         ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1189
1190         -- Check that instance inference will terminate (if we care)
1191         -- For Haskell 98 this will already have been done by checkValidTheta,
1192         -- but as we may be using other extensions we need to check.
1193         ; unless undecidable_ok $
1194           mapM_ addErrTc (checkInstTermination inst_tys theta)
1195
1196         -- The Coverage Condition
1197         ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1198                   (instTypeErr (pprClassPred clas inst_tys) msg)
1199         }
1200   where
1201     msg  = parens (vcat [ptext SLIT("the Coverage Condition fails for one of the functional dependencies;"),
1202                          undecidableMsg])
1203 \end{code}
1204
1205 Termination test: the so-called "Paterson conditions" (see Section 5 of
1206 "Understanding functionsl dependencies via Constraint Handling Rules,
1207 JFP Jan 2007).
1208
1209 We check that each assertion in the context satisfies:
1210  (1) no variable has more occurrences in the assertion than in the head, and
1211  (2) the assertion has fewer constructors and variables (taken together
1212      and counting repetitions) than the head.
1213 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1214 (which have already been checked) guarantee termination.
1215
1216 The underlying idea is that
1217
1218     for any ground substitution, each assertion in the
1219     context has fewer type constructors than the head.
1220
1221
1222 \begin{code}
1223 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1224 checkInstTermination tys theta
1225   = mapCatMaybes check theta
1226   where
1227    fvs  = fvTypes tys
1228    size = sizeTypes tys
1229    check pred
1230       | not (null (fvPred pred \\ fvs))
1231       = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1232       | sizePred pred >= size
1233       = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1234       | otherwise
1235       = Nothing
1236
1237 predUndecErr pred msg = sep [msg,
1238                         nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1239
1240 nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
1241 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
1242 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1243 \end{code}
1244
1245
1246 %************************************************************************
1247 %*                                                                      *
1248 \subsection{Checking type instance well-formedness and termination}
1249 %*                                                                      *
1250 %************************************************************************
1251
1252 \begin{code}
1253 -- Check that a "type instance" is well-formed (which includes decidability
1254 -- unless -fallow-undecidable-instances is given).
1255 --
1256 checkValidTypeInst :: [Type] -> Type -> TcM ()
1257 checkValidTypeInst typats rhs
1258   = do { -- left-hand side contains no type family applications
1259          -- (vanilla synonyms are fine, though)
1260        ; mappM_ checkTyFamFreeness typats
1261
1262          -- the right-hand side is a tau type
1263        ; checkTc (isTauTy rhs) $
1264            polyTyErr rhs
1265
1266          -- we have a decidable instance unless otherwise permitted
1267        ; undecidable_ok <- doptM Opt_UndecidableInstances
1268        ; unless undecidable_ok $
1269            mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
1270        }
1271
1272 -- Make sure that each type family instance is
1273 --   (1) strictly smaller than the lhs,
1274 --   (2) mentions no type variable more often than the lhs, and
1275 --   (3) does not contain any further type family instances.
1276 --
1277 checkFamInst :: [Type]                  -- lhs
1278              -> [(TyCon, [Type])]       -- type family instances
1279              -> [Message]
1280 checkFamInst lhsTys famInsts
1281   = mapCatMaybes check famInsts
1282   where
1283    size = sizeTypes lhsTys
1284    fvs  = fvTypes lhsTys
1285    check (tc, tys)
1286       | not (all isTyFamFree tys)
1287       = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1288       | not (null (fvTypes tys \\ fvs))
1289       = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1290       | size <= sizeTypes tys
1291       = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1292       | otherwise
1293       = Nothing
1294       where
1295         famInst = TyConApp tc tys
1296
1297 -- Ensure that no type family instances occur in a type.
1298 --
1299 checkTyFamFreeness :: Type -> TcM ()
1300 checkTyFamFreeness ty
1301   = checkTc (isTyFamFree ty) $
1302       tyFamInstInIndexErr ty
1303
1304 -- Check that a type does not contain any type family applications.
1305 --
1306 isTyFamFree :: Type -> Bool
1307 isTyFamFree = null . tyFamInsts
1308
1309 -- Error messages
1310
1311 tyFamInstInIndexErr ty
1312   = hang (ptext SLIT("Illegal type family application in type instance") <>
1313          colon) 4 $
1314       ppr ty
1315
1316 polyTyErr ty
1317   = hang (ptext SLIT("Illegal polymorphic type in type instance") <> colon) 4 $
1318       ppr ty
1319
1320 famInstUndecErr ty msg
1321   = sep [msg,
1322          nest 2 (ptext SLIT("in the type family application:") <+>
1323                  pprType ty)]
1324
1325 nestedMsg     = ptext SLIT("Nested type family application")
1326 nomoreVarMsg  = ptext SLIT("Variable occurs more often than in instance head")
1327 smallerAppMsg = ptext SLIT("Application is no smaller than the instance head")
1328 \end{code}
1329
1330
1331 %************************************************************************
1332 %*                                                                      *
1333 \subsection{Auxiliary functions}
1334 %*                                                                      *
1335 %************************************************************************
1336
1337 \begin{code}
1338 -- Free variables of a type, retaining repetitions, and expanding synonyms
1339 fvType :: Type -> [TyVar]
1340 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1341 fvType (TyVarTy tv)        = [tv]
1342 fvType (TyConApp _ tys)    = fvTypes tys
1343 fvType (NoteTy _ ty)       = fvType ty
1344 fvType (PredTy pred)       = fvPred pred
1345 fvType (FunTy arg res)     = fvType arg ++ fvType res
1346 fvType (AppTy fun arg)     = fvType fun ++ fvType arg
1347 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1348
1349 fvTypes :: [Type] -> [TyVar]
1350 fvTypes tys                = concat (map fvType tys)
1351
1352 fvPred :: PredType -> [TyVar]
1353 fvPred (ClassP _ tys')     = fvTypes tys'
1354 fvPred (IParam _ ty)       = fvType ty
1355 fvPred (EqPred ty1 ty2)    = fvType ty1 ++ fvType ty2
1356
1357 -- Size of a type: the number of variables and constructors
1358 sizeType :: Type -> Int
1359 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1360 sizeType (TyVarTy _)       = 1
1361 sizeType (TyConApp _ tys)  = sizeTypes tys + 1
1362 sizeType (NoteTy _ ty)     = sizeType ty
1363 sizeType (PredTy pred)     = sizePred pred
1364 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
1365 sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
1366 sizeType (ForAllTy _ ty)   = sizeType ty
1367
1368 sizeTypes :: [Type] -> Int
1369 sizeTypes xs               = sum (map sizeType xs)
1370
1371 sizePred :: PredType -> Int
1372 sizePred (ClassP _ tys')   = sizeTypes tys'
1373 sizePred (IParam _ ty)     = sizeType ty
1374 sizePred (EqPred ty1 ty2)  = sizeType ty1 + sizeType ty2
1375
1376 -- Type family instances occuring in a type after expanding synonyms
1377 tyFamInsts :: Type -> [(TyCon, [Type])]
1378 tyFamInsts ty
1379   | Just exp_ty <- tcView ty    = tyFamInsts exp_ty
1380 tyFamInsts (TyVarTy _)          = []
1381 tyFamInsts (TyConApp tc tys)
1382   | isOpenSynTyCon tc           = [(tc, tys)]
1383   | otherwise                   = concat (map tyFamInsts tys)
1384 tyFamInsts (FunTy ty1 ty2)      = tyFamInsts ty1 ++ tyFamInsts ty2
1385 tyFamInsts (AppTy ty1 ty2)      = tyFamInsts ty1 ++ tyFamInsts ty2
1386 tyFamInsts (ForAllTy _ ty)      = tyFamInsts ty
1387 \end{code}