ghc/compiler/typecheck/TcType.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section[TcType]{Types used in the typechecker}
   5
   6 This module provides the Type interface for front-end parts of the
   7 compiler.  These parts
   8
   9         * treat "source types" as opaque:
  10                 newtypes, and predicates are meaningful.
  11         * look through usage types
  12
  13 The "tc" prefix is for "typechechecker", because the type checker
  14 is the principal client.
  15
  16 \begin{code}
  17 module TcType (
  18   --------------------------------
  19   -- Types
  20   TcType, TcSigmaType, TcPhiType, TcTauType, TcPredType, TcThetaType,
  21   TcTyVar, TcTyVarSet, TcKind,
  22
  23   --------------------------------
  24   -- TyVarDetails
  25   TyVarDetails(..), isUserTyVar, isSkolemTyVar, isHoleTyVar,
  26   tyVarBindingInfo,
  27
  28   --------------------------------
  29   -- Builders
  30   mkRhoTy, mkSigmaTy,
  31
  32   --------------------------------
  33   -- Splitters
  34   -- These are important because they do not look through newtypes
  35   tcSplitForAllTys, tcSplitRhoTy,
  36   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
  37   tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
  38   tcSplitAppTy_maybe, tcSplitAppTy, tcSplitSigmaTy,
  39   tcSplitMethodTy, tcGetTyVar_maybe, tcGetTyVar,
  40
  41   ---------------------------------
  42   -- Predicates.
  43   -- Again, newtypes are opaque
  44   tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
  45   isSigmaTy, isOverloadedTy,
  46   isDoubleTy, isFloatTy, isIntTy,
  47   isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy,
  48   isTauTy, tcIsTyVarTy, tcIsForAllTy,
  49   allDistinctTyVars,
  50
  51   ---------------------------------
  52   -- Misc type manipulators
  53   hoistForAllTys, deNoteType,
  54   namesOfType, namesOfDFunHead,
  55   getDFunTyKey,
  56
  57   ---------------------------------
  58   -- Predicate types
  59   PredType, getClassPredTys_maybe, getClassPredTys,
  60   isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
  61   mkDictTy, tcSplitPredTy_maybe, predTyUnique,
  62   isDictTy, tcSplitDFunTy, predTyUnique,
  63   mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName,
  64
  65   ---------------------------------
  66   -- Foreign import and export
  67   isFFIArgumentTy,     -- :: DynFlags -> Safety -> Type -> Bool
  68   isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
  69   isFFIExportResultTy, -- :: Type -> Bool
  70   isFFIExternalTy,     -- :: Type -> Bool
  71   isFFIDynArgumentTy,  -- :: Type -> Bool
  72   isFFIDynResultTy,    -- :: Type -> Bool
  73   isFFILabelTy,        -- :: Type -> Bool
  74
  75   ---------------------------------
  76   -- Unifier and matcher
  77   unifyTysX, unifyTyListsX, unifyExtendTysX,
  78   matchTy, matchTys, match,
  79
  80   --------------------------------
  81   -- Rexported from Type
  82   Kind,         -- Stuff to do with kinds is insensitive to pre/post Tc
  83   unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
  84   superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
  85   isTypeKind, isAnyTypeKind,
  86
  87   Type, SourceType(..), PredType, ThetaType,
  88   mkForAllTy, mkForAllTys,
  89   mkFunTy, mkFunTys, zipFunTys,
  90   mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
  91   mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
  92
  93   isUnLiftedType,       -- Source types are always lifted
  94   isUnboxedTupleType,   -- Ditto
  95   isPrimitiveType,
  96
  97   tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
  98   tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
  99   typeKind, eqKind, eqUsage,
 100
 101   tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
 102   ) where
 103
 104 #include "HsVersions.h"
 105
 106
 107 import {-# SOURCE #-} PprType( pprType )
 108
 109 -- friends:
 110 import TypeRep          ( Type(..), TyNote(..), funTyCon )  -- friend
 111
 112 import Type             (       -- Re-exports
 113                           tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
 114                           Kind, Type, SourceType(..), PredType, ThetaType,
 115                           unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
 116                           mkForAllTy, mkForAllTys, defaultKind, isTypeKind, isAnyTypeKind,
 117                           mkFunTy, mkFunTys, zipFunTys,
 118                           mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
 119                           mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
 120                           isUnLiftedType, isUnboxedTupleType, isPrimitiveType,
 121                           splitNewType_maybe, splitTyConApp_maybe,
 122                           tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
 123                           tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, eqKind, eqUsage,
 124                           hasMoreBoxityInfo, liftedBoxity, superBoxity, typeKind, superKind
 125                         )
 126 import TyCon            ( TyCon, isUnLiftedTyCon )
 127 import Class            ( classHasFDs, Class )
 128 import Var              ( TyVar, tyVarKind, isMutTyVar, mutTyVarDetails )
 129 import ForeignCall      ( Safety, playSafe )
 130 import VarEnv
 131 import VarSet
 132
 133 -- others:
 134 import CmdLineOpts      ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
 135 import Name             ( Name, NamedThing(..), mkLocalName, getSrcLoc )
 136 import OccName          ( OccName, mkDictOcc )
 137 import NameSet
 138 import PrelNames        -- Lots (e.g. in isFFIArgumentTy)
 139 import TysWiredIn       ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
 140 import BasicTypes       ( IPName(..), ipNameName )
 141 import Unique           ( Unique, Uniquable(..) )
 142 import SrcLoc           ( SrcLoc )
 143 import Util             ( cmpList, thenCmp, equalLength )
 144 import Maybes           ( maybeToBool, expectJust )
 145 import Outputable
 146 \end{code}
 147
 148
 149 %************************************************************************
 150 %*                                                                      *
 151 \subsection{Types}
 152 %*                                                                      *
 153 %************************************************************************
 154
 155 The type checker divides the generic Type world into the
 156 following more structured beasts:
 157
 158 sigma ::= forall tyvars. theta => phi
 159         -- A sigma type is a qualified type
 160         --
 161         -- Note that even if 'tyvars' is empty, theta
 162         -- may not be: e.g.   (?x::Int) => Int
 163
 164         -- Note that 'sigma' is in prenex form:
 165         -- all the foralls are at the front.
 166         -- A 'phi' type has no foralls to the right of
 167         -- an arrow
 168
 169 phi ::= sigma -> phi
 170      |  tau
 171
 172 -- A 'tau' type has no quantification anywhere
 173 -- Note that the args of a type constructor must be taus
 174 tau ::= tyvar
 175      |  tycon tau_1 .. tau_n
 176      |  tau_1 tau_2
 177      |  tau_1 -> tau_2
 178
 179 -- In all cases, a (saturated) type synonym application is legal,
 180 -- provided it expands to the required form.
 181
 182
 183 \begin{code}
 184 type SigmaType = Type
 185 type PhiType   = Type
 186 type TauType   = Type
 187 \end{code}
 188
 189 \begin{code}
 190 type TcTyVar    = TyVar         -- Might be a mutable tyvar
 191 type TcTyVarSet = TyVarSet
 192
 193 type TcType = Type              -- A TcType can have mutable type variables
 194         -- Invariant on ForAllTy in TcTypes:
 195         --      forall a. T
 196         -- a cannot occur inside a MutTyVar in T; that is,
 197         -- T is "flattened" before quantifying over a
 198
 199 type TcPredType     = PredType
 200 type TcThetaType    = ThetaType
 201 type TcSigmaType    = TcType
 202 type TcPhiType      = TcType
 203 type TcTauType      = TcType
 204 type TcKind         = TcType
 205 \end{code}
 206
 207
 208 %************************************************************************
 209 %*                                                                      *
 210 \subsection{TyVarDetails}
 211 %*                                                                      *
 212 %************************************************************************
 213
 214 TyVarDetails gives extra info about type variables, used during type
 215 checking.  It's attached to mutable type variables only.
 216 It's knot-tied back to Var.lhs.  There is no reason in principle
 217 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
 218
 219 \begin{code}
 220 data TyVarDetails
 221   = HoleTv      -- Used *only* by the type checker when passing in a type
 222                 -- variable that should be side-effected to the result type.
 223                 -- Always has kind openTypeKind.
 224                 -- Never appears in types
 225
 226   | SigTv       -- Introduced when instantiating a type signature,
 227                 -- prior to checking that the defn of a fn does
 228                 -- have the expected type.  Should not be instantiated.
 229                 --
 230                 --      f :: forall a. a -> a
 231                 --      f = e
 232                 -- When checking e, with expected type (a->a), we
 233                 -- should not instantiate a
 234
 235    | ClsTv      -- Scoped type variable introduced by a class decl
 236                 --      class C a where ...
 237
 238    | InstTv     -- Ditto, but instance decl
 239
 240    | PatSigTv   -- Scoped type variable, introduced by a pattern
 241                 -- type signature
 242                 --      \ x::a -> e
 243
 244    | VanillaTv  -- Everything else
 245
 246 isUserTyVar :: TcTyVar -> Bool  -- Avoid unifying these if possible
 247 isUserTyVar tv = case mutTyVarDetails tv of
 248                    VanillaTv -> False
 249                    other     -> True
 250
 251 isSkolemTyVar :: TcTyVar -> Bool
 252 isSkolemTyVar tv = case mutTyVarDetails tv of
 253                       SigTv  -> True
 254                       ClsTv  -> True
 255                       InstTv -> True
 256                       oteher -> False
 257
 258 isHoleTyVar :: TcTyVar -> Bool
 259 -- NB:  the hole might be filled in by now, and this
 260 --      function does not check for that
 261 isHoleTyVar tv = ASSERT( isMutTyVar tv )
 262                  case mutTyVarDetails tv of
 263                         HoleTv -> True
 264                         other  -> False
 265
 266 tyVarBindingInfo :: TyVar -> SDoc       -- Used in checkSigTyVars
 267 tyVarBindingInfo tv
 268   | isMutTyVar tv
 269   = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails tv),
 270          ptext SLIT("at") <+> ppr (getSrcLoc tv)]
 271   | otherwise
 272   = empty
 273   where
 274     details SigTv     = ptext SLIT("type signature")
 275     details ClsTv     = ptext SLIT("class declaration")
 276     details InstTv    = ptext SLIT("instance declaration")
 277     details PatSigTv  = ptext SLIT("pattern type signature")
 278     details HoleTv    = ptext SLIT("//hole//")          -- Should not happen
 279     details VanillaTv = ptext SLIT("//vanilla//")       -- Ditto
 280 \end{code}
 281
 282
 283 %************************************************************************
 284 %*                                                                      *
 285 \subsection{Tau, sigma and rho}
 286 %*                                                                      *
 287 %************************************************************************
 288
 289 \begin{code}
 290 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
 291
 292 mkRhoTy :: [SourceType] -> Type -> Type
 293 mkRhoTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
 294 \end{code}
 295
 296
 297 @isTauTy@ tests for nested for-alls.
 298
 299 \begin{code}
 300 isTauTy :: Type -> Bool
 301 isTauTy (TyVarTy v)      = True
 302 isTauTy (TyConApp _ tys) = all isTauTy tys
 303 isTauTy (AppTy a b)      = isTauTy a && isTauTy b
 304 isTauTy (FunTy a b)      = isTauTy a && isTauTy b
 305 isTauTy (SourceTy p)     = True         -- Don't look through source types
 306 isTauTy (NoteTy _ ty)    = isTauTy ty
 307 isTauTy other            = False
 308 \end{code}
 309
 310 \begin{code}
 311 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
 312                                 -- construct a dictionary function name
 313 getDFunTyKey (TyVarTy tv)            = getOccName tv
 314 getDFunTyKey (TyConApp tc _)         = getOccName tc
 315 getDFunTyKey (AppTy fun _)           = getDFunTyKey fun
 316 getDFunTyKey (NoteTy _ t)            = getDFunTyKey t
 317 getDFunTyKey (FunTy arg _)           = getOccName funTyCon
 318 getDFunTyKey (ForAllTy _ t)          = getDFunTyKey t
 319 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc    -- Newtypes are quite reasonable
 320 getDFunTyKey ty                      = pprPanic "getDFunTyKey" (pprType ty)
 321 -- SourceTy shouldn't happen
 322 \end{code}
 323
 324
 325 %************************************************************************
 326 %*                                                                      *
 327 \subsection{Expanding and splitting}
 328 %*                                                                      *
 329 %************************************************************************
 330
 331 These tcSplit functions are like their non-Tc analogues, but
 332         a) they do not look through newtypes
 333         b) they do not look through PredTys
 334         c) [future] they ignore usage-type annotations
 335
 336 However, they are non-monadic and do not follow through mutable type
 337 variables.  It's up to you to make sure this doesn't matter.
 338
 339 \begin{code}
 340 tcSplitForAllTys :: Type -> ([TyVar], Type)
 341 tcSplitForAllTys ty = split ty ty []
 342    where
 343      split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
 344      split orig_ty (NoteTy n  ty)   tvs = split orig_ty ty tvs
 345      split orig_ty t                tvs = (reverse tvs, orig_ty)
 346
 347 tcIsForAllTy (ForAllTy tv ty) = True
 348 tcIsForAllTy (NoteTy n ty)    = tcIsForAllTy ty
 349 tcIsForAllTy t                = False
 350
 351 tcSplitRhoTy :: Type -> ([PredType], Type)
 352 tcSplitRhoTy ty = split ty ty []
 353  where
 354   split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
 355                                         Just p  -> split res res (p:ts)
 356                                         Nothing -> (reverse ts, orig_ty)
 357   split orig_ty (NoteTy n ty)   ts = split orig_ty ty ts
 358   split orig_ty ty              ts = (reverse ts, orig_ty)
 359
 360 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
 361                         (tvs, rho) -> case tcSplitRhoTy rho of
 362                                         (theta, tau) -> (tvs, theta, tau)
 363
 364 tcTyConAppTyCon :: Type -> TyCon
 365 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
 366
 367 tcTyConAppArgs :: Type -> [Type]
 368 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
 369
 370 tcSplitTyConApp :: Type -> (TyCon, [Type])
 371 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
 372                         Just stuff -> stuff
 373                         Nothing    -> pprPanic "tcSplitTyConApp" (pprType ty)
 374
 375 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
 376 tcSplitTyConApp_maybe (TyConApp tc tys)         = Just (tc, tys)
 377 tcSplitTyConApp_maybe (FunTy arg res)           = Just (funTyCon, [arg,res])
 378 tcSplitTyConApp_maybe (NoteTy n ty)             = tcSplitTyConApp_maybe ty
 379 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
 380         -- Newtypes are opaque, so they may be split
 381         -- However, predicates are not treated
 382         -- as tycon applications by the type checker
 383 tcSplitTyConApp_maybe other                     = Nothing
 384
 385 tcSplitFunTys :: Type -> ([Type], Type)
 386 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
 387                         Nothing        -> ([], ty)
 388                         Just (arg,res) -> (arg:args, res')
 389                                        where
 390                                           (args,res') = tcSplitFunTys res
 391
 392 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
 393 tcSplitFunTy_maybe (FunTy arg res)  = Just (arg, res)
 394 tcSplitFunTy_maybe (NoteTy n ty)    = tcSplitFunTy_maybe ty
 395 tcSplitFunTy_maybe other            = Nothing
 396
 397 tcFunArgTy    ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
 398 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
 399
 400
 401 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
 402 tcSplitAppTy_maybe (FunTy ty1 ty2)           = Just (TyConApp funTyCon [ty1], ty2)
 403 tcSplitAppTy_maybe (AppTy ty1 ty2)           = Just (ty1, ty2)
 404 tcSplitAppTy_maybe (NoteTy n ty)             = tcSplitAppTy_maybe ty
 405 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys
 406         --- Don't forget that newtype!
 407 tcSplitAppTy_maybe (TyConApp tc tys)         = tc_split_app tc tys
 408 tcSplitAppTy_maybe other                     = Nothing
 409
 410 tc_split_app tc []  = Nothing
 411 tc_split_app tc tys = split tys []
 412                     where
 413                       split [ty2]    acc = Just (TyConApp tc (reverse acc), ty2)
 414                       split (ty:tys) acc = split tys (ty:acc)
 415
 416 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
 417                     Just stuff -> stuff
 418                     Nothing    -> pprPanic "tcSplitAppTy" (pprType ty)
 419
 420 tcGetTyVar_maybe :: Type -> Maybe TyVar
 421 tcGetTyVar_maybe (TyVarTy tv)   = Just tv
 422 tcGetTyVar_maybe (NoteTy _ t)   = tcGetTyVar_maybe t
 423 tcGetTyVar_maybe other          = Nothing
 424
 425 tcGetTyVar :: String -> Type -> TyVar
 426 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
 427
 428 tcIsTyVarTy :: Type -> Bool
 429 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
 430 \end{code}
 431
 432 The type of a method for class C is always of the form:
 433         Forall a1..an. C a1..an => sig_ty
 434 where sig_ty is the type given by the method's signature, and thus in general
 435 is a ForallTy.  At the point that splitMethodTy is called, it is expected
 436 that the outer Forall has already been stripped off.  splitMethodTy then
 437 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes or
 438 Usages stripped off.
 439
 440 \begin{code}
 441 tcSplitMethodTy :: Type -> (PredType, Type)
 442 tcSplitMethodTy ty = split ty
 443  where
 444   split (FunTy arg res) = case tcSplitPredTy_maybe arg of
 445                             Just p  -> (p, res)
 446                             Nothing -> panic "splitMethodTy"
 447   split (NoteTy n ty)   = split ty
 448   split _               = panic "splitMethodTy"
 449
 450 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
 451 -- Split the type of a dictionary function
 452 tcSplitDFunTy ty
 453   = case tcSplitSigmaTy ty       of { (tvs, theta, tau) ->
 454     case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
 455     (tvs, theta, clas, tys) }}
 456 \end{code}
 457
 458 (allDistinctTyVars tys tvs) = True
 459         iff
 460 all the types tys are type variables,
 461 distinct from each other and from tvs.
 462
 463 This is useful when checking that unification hasn't unified signature
 464 type variables.  For example, if the type sig is
 465         f :: forall a b. a -> b -> b
 466 we want to check that 'a' and 'b' havn't
 467         (a) been unified with a non-tyvar type
 468         (b) been unified with each other (all distinct)
 469         (c) been unified with a variable free in the environment
 470
 471 \begin{code}
 472 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
 473
 474 allDistinctTyVars []       acc
 475   = True
 476 allDistinctTyVars (ty:tys) acc
 477   = case tcGetTyVar_maybe ty of
 478         Nothing                       -> False  -- (a)
 479         Just tv | tv `elemVarSet` acc -> False  -- (b) or (c)
 480                 | otherwise           -> allDistinctTyVars tys (acc `extendVarSet` tv)
 481 \end{code}
 482
 483
 484 %************************************************************************
 485 %*                                                                      *
 486 \subsection{Predicate types}
 487 %*                                                                      *
 488 %************************************************************************
 489
 490 "Predicates" are particular source types, namelyClassP or IParams
 491
 492 \begin{code}
 493 isPred :: SourceType -> Bool
 494 isPred (ClassP _ _) = True
 495 isPred (IParam _ _) = True
 496 isPred (NType _ _)  = False
 497
 498 isPredTy :: Type -> Bool
 499 isPredTy (NoteTy _ ty)  = isPredTy ty
 500 isPredTy (SourceTy sty) = isPred sty
 501 isPredTy _              = False
 502
 503 tcSplitPredTy_maybe :: Type -> Maybe PredType
 504    -- Returns Just for predicates only
 505 tcSplitPredTy_maybe (NoteTy _ ty)           = tcSplitPredTy_maybe ty
 506 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
 507 tcSplitPredTy_maybe other                   = Nothing
 508
 509 predTyUnique :: PredType -> Unique
 510 predTyUnique (IParam n _)      = getUnique (ipNameName n)
 511 predTyUnique (ClassP clas tys) = getUnique clas
 512
 513 predHasFDs :: PredType -> Bool
 514 -- True if the predicate has functional depenencies;
 515 -- I.e. should participate in improvement
 516 predHasFDs (IParam _ _)   = True
 517 predHasFDs (ClassP cls _) = classHasFDs cls
 518
 519 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
 520 mkPredName uniq loc (ClassP cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc
 521 mkPredName uniq loc (IParam ip ty)   = mkLocalName uniq (getOccName (ipNameName ip)) loc
 522 \end{code}
 523
 524
 525 --------------------- Dictionary types ---------------------------------
 526
 527 \begin{code}
 528 mkClassPred clas tys = ClassP clas tys
 529
 530 isClassPred :: SourceType -> Bool
 531 isClassPred (ClassP clas tys) = True
 532 isClassPred other             = False
 533
 534 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
 535 isTyVarClassPred other             = False
 536
 537 getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
 538 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
 539 getClassPredTys_maybe _                 = Nothing
 540
 541 getClassPredTys :: PredType -> (Class, [Type])
 542 getClassPredTys (ClassP clas tys) = (clas, tys)
 543
 544 mkDictTy :: Class -> [Type] -> Type
 545 mkDictTy clas tys = mkPredTy (ClassP clas tys)
 546
 547 isDictTy :: Type -> Bool
 548 isDictTy (SourceTy p)   = isClassPred p
 549 isDictTy (NoteTy _ ty)  = isDictTy ty
 550 isDictTy other          = False
 551 \end{code}
 552
 553 --------------------- Implicit parameters ---------------------------------
 554
 555 \begin{code}
 556 isIPPred :: SourceType -> Bool
 557 isIPPred (IParam _ _) = True
 558 isIPPred other        = False
 559
 560 isInheritablePred :: PredType -> Bool
 561 -- Can be inherited by a context.  For example, consider
 562 --      f x = let g y = (?v, y+x)
 563 --            in (g 3 with ?v = 8,
 564 --                g 4 with ?v = 9)
 565 -- The point is that g's type must be quantifed over ?v:
 566 --      g :: (?v :: a) => a -> a
 567 -- but it doesn't need to be quantified over the Num a dictionary
 568 -- which can be free in g's rhs, and shared by both calls to g
 569 isInheritablePred (ClassP _ _) = True
 570 isInheritablePred other      = False
 571
 572 isLinearPred :: TcPredType -> Bool
 573 isLinearPred (IParam (Linear n) _) = True
 574 isLinearPred other                 = False
 575 \end{code}
 576
 577
 578 %************************************************************************
 579 %*                                                                      *
 580 \subsection{Comparison}
 581 %*                                                                      *
 582 %************************************************************************
 583
 584 Comparison, taking note of newtypes, predicates, etc,
 585 But ignoring usage types
 586
 587 \begin{code}
 588 tcEqType :: Type -> Type -> Bool
 589 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
 590
 591 tcEqTypes :: [Type] -> [Type] -> Bool
 592 tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
 593
 594 tcEqPred :: PredType -> PredType -> Bool
 595 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
 596
 597 -------------
 598 tcCmpType :: Type -> Type -> Ordering
 599 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
 600
 601 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
 602
 603 tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
 604 -------------
 605 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
 606
 607 -------------
 608 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
 609   -- The "env" maps type variables in ty1 to type variables in ty2
 610   -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
 611   -- we in effect substitute tv2 for tv1 in t1 before continuing
 612
 613     -- Look through NoteTy
 614 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
 615 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
 616
 617     -- Deal with equal constructors
 618 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
 619                                           Just tv1a -> tv1a `compare` tv2
 620                                           Nothing   -> tv1  `compare` tv2
 621
 622 cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
 623 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
 624 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
 625 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
 626 cmpTy env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTy (extendVarEnv env tv1 tv2) t1 t2
 627
 628     -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
 629 cmpTy env (AppTy _ _) (TyVarTy _) = GT
 630
 631 cmpTy env (FunTy _ _) (TyVarTy _) = GT
 632 cmpTy env (FunTy _ _) (AppTy _ _) = GT
 633
 634 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
 635 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
 636 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
 637
 638 cmpTy env (ForAllTy _ _) (TyVarTy _)    = GT
 639 cmpTy env (ForAllTy _ _) (AppTy _ _)    = GT
 640 cmpTy env (ForAllTy _ _) (FunTy _ _)    = GT
 641 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
 642
 643 cmpTy env (SourceTy _)   t2             = GT
 644
 645 cmpTy env _ _ = LT
 646 \end{code}
 647
 648 \begin{code}
 649 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
 650 cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
 651         -- Compare types as well as names for implicit parameters
 652         -- This comparison is used exclusively (I think) for the
 653         -- finite map built in TcSimplify
 654 cmpSourceTy env (IParam _ _)     sty              = LT
 655
 656 cmpSourceTy env (ClassP _ _)     (IParam _ _)     = GT
 657 cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
 658 cmpSourceTy env (ClassP _ _)     (NType _ _)      = LT
 659
 660 cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
 661 cmpSourceTy env (NType _ _)      sty              = GT
 662 \end{code}
 663
 664 PredTypes are used as a FM key in TcSimplify,
 665 so we take the easy path and make them an instance of Ord
 666
 667 \begin{code}
 668 instance Eq  SourceType where { (==)    = tcEqPred }
 669 instance Ord SourceType where { compare = tcCmpPred }
 670 \end{code}
 671
 672
 673 %************************************************************************
 674 %*                                                                      *
 675 \subsection{Predicates}
 676 %*                                                                      *
 677 %************************************************************************
 678
 679 isSigmaTy returns true of any qualified type.  It doesn't *necessarily* have
 680 any foralls.  E.g.
 681         f :: (?x::Int) => Int -> Int
 682
 683 \begin{code}
 684 isSigmaTy :: Type -> Bool
 685 isSigmaTy (ForAllTy tyvar ty) = True
 686 isSigmaTy (FunTy a b)         = isPredTy a
 687 isSigmaTy (NoteTy n ty)       = isSigmaTy ty
 688 isSigmaTy _                   = False
 689
 690 isOverloadedTy :: Type -> Bool
 691 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
 692 isOverloadedTy (FunTy a b)         = isPredTy a
 693 isOverloadedTy (NoteTy n ty)       = isOverloadedTy ty
 694 isOverloadedTy _                   = False
 695 \end{code}
 696
 697 \begin{code}
 698 isFloatTy      = is_tc floatTyConKey
 699 isDoubleTy     = is_tc doubleTyConKey
 700 isForeignPtrTy = is_tc foreignPtrTyConKey
 701 isIntegerTy    = is_tc integerTyConKey
 702 isIntTy        = is_tc intTyConKey
 703 isAddrTy       = is_tc addrTyConKey
 704 isBoolTy       = is_tc boolTyConKey
 705 isUnitTy       = is_tc unitTyConKey
 706
 707 is_tc :: Unique -> Type -> Bool
 708 -- Newtypes are opaque to this
 709 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
 710                         Just (tc, _) -> uniq == getUnique tc
 711                         Nothing      -> False
 712 \end{code}
 713
 714
 715 %************************************************************************
 716 %*                                                                      *
 717 \subsection{Misc}
 718 %*                                                                      *
 719 %************************************************************************
 720
 721 \begin{code}
 722 hoistForAllTys :: Type -> Type
 723 -- Used for user-written type signatures only
 724 -- Move all the foralls and constraints to the top
 725 -- e.g.  T -> forall a. a        ==>   forall a. T -> a
 726 --       T -> (?x::Int) -> Int   ==>   (?x::Int) -> T -> Int
 727 --
 728 -- We want to 'look through' type synonyms when doing this
 729 -- so it's better done on the Type than the HsType
 730
 731 hoistForAllTys ty
 732   = case hoist ty ty of
 733         (tvs, theta, body) -> mkForAllTys tvs (mkFunTys theta body)
 734   where
 735     hoist orig_ty (ForAllTy tv ty) = case hoist ty ty of
 736                                         (tvs,theta,tau) -> (tv:tvs,theta,tau)
 737     hoist orig_ty (FunTy arg res)
 738         | isPredTy arg             = case hoist res res of
 739                                         (tvs,theta,tau) -> (tvs,arg:theta,tau)
 740         | otherwise                = case hoist res res of
 741                                         (tvs,theta,tau) -> (tvs,theta,mkFunTy arg tau)
 742
 743     hoist orig_ty (NoteTy _ ty)    = hoist orig_ty ty
 744     hoist orig_ty ty               = ([], [], orig_ty)
 745 \end{code}
 746
 747
 748 \begin{code}
 749 deNoteType :: Type -> Type
 750         -- Remove synonyms, but not source types
 751 deNoteType ty@(TyVarTy tyvar)   = ty
 752 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
 753 deNoteType (SourceTy p)         = SourceTy (deNoteSourceType p)
 754 deNoteType (NoteTy _ ty)        = deNoteType ty
 755 deNoteType (AppTy fun arg)      = AppTy (deNoteType fun) (deNoteType arg)
 756 deNoteType (FunTy fun arg)      = FunTy (deNoteType fun) (deNoteType arg)
 757 deNoteType (ForAllTy tv ty)     = ForAllTy tv (deNoteType ty)
 758
 759 deNoteSourceType :: SourceType -> SourceType
 760 deNoteSourceType (ClassP c tys)   = ClassP c (map deNoteType tys)
 761 deNoteSourceType (IParam n ty)    = IParam n (deNoteType ty)
 762 deNoteSourceType (NType tc tys)   = NType tc (map deNoteType tys)
 763 \end{code}
 764
 765 Find the free names of a type, including the type constructors and classes it mentions
 766 This is used in the front end of the compiler
 767
 768 \begin{code}
 769 namesOfType :: Type -> NameSet
 770 namesOfType (TyVarTy tv)                = unitNameSet (getName tv)
 771 namesOfType (TyConApp tycon tys)        = unitNameSet (getName tycon) `unionNameSets` namesOfTypes tys
 772 namesOfType (NoteTy (SynNote ty1) ty2)  = namesOfType ty1
 773 namesOfType (NoteTy other_note    ty2)  = namesOfType ty2
 774 namesOfType (SourceTy (IParam n ty))    = namesOfType ty
 775 namesOfType (SourceTy (ClassP cl tys))  = unitNameSet (getName cl) `unionNameSets` namesOfTypes tys
 776 namesOfType (SourceTy (NType tc tys))   = unitNameSet (getName tc) `unionNameSets` namesOfTypes tys
 777 namesOfType (FunTy arg res)             = namesOfType arg `unionNameSets` namesOfType res
 778 namesOfType (AppTy fun arg)             = namesOfType fun `unionNameSets` namesOfType arg
 779 namesOfType (ForAllTy tyvar ty)         = namesOfType ty `delFromNameSet` getName tyvar
 780
 781 namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
 782
 783 namesOfDFunHead :: Type -> NameSet
 784 -- Find the free type constructors and classes
 785 -- of the head of the dfun instance type
 786 -- The 'dfun_head_type' is because of
 787 --      instance Foo a => Baz T where ...
 788 -- The decl is an orphan if Baz and T are both not locally defined,
 789 --      even if Foo *is* locally defined
 790 namesOfDFunHead dfun_ty = case tcSplitSigmaTy dfun_ty of
 791                                 (tvs,_,head_ty) -> delListFromNameSet (namesOfType head_ty)
 792                                                                       (map getName tvs)
 793 \end{code}
 794
 795
 796 %************************************************************************
 797 %*                                                                      *
 798 \subsection[TysWiredIn-ext-type]{External types}
 799 %*                                                                      *
 800 %************************************************************************
 801
 802 The compiler's foreign function interface supports the passing of a
 803 restricted set of types as arguments and results (the restricting factor
 804 being the )
 805
 806 \begin{code}
 807 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
 808 -- Checks for valid argument type for a 'foreign import'
 809 isFFIArgumentTy dflags safety ty
 810    = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
 811
 812 isFFIExternalTy :: Type -> Bool
 813 -- Types that are allowed as arguments of a 'foreign export'
 814 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
 815
 816 isFFIImportResultTy :: DynFlags -> Type -> Bool
 817 isFFIImportResultTy dflags ty
 818   = checkRepTyCon (legalFIResultTyCon dflags) ty
 819
 820 isFFIExportResultTy :: Type -> Bool
 821 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
 822
 823 isFFIDynArgumentTy :: Type -> Bool
 824 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
 825 -- or a newtype of either.
 826 isFFIDynArgumentTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
 827
 828 isFFIDynResultTy :: Type -> Bool
 829 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
 830 -- or a newtype of either.
 831 isFFIDynResultTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
 832
 833 isFFILabelTy :: Type -> Bool
 834 -- The type of a foreign label must be Ptr, FunPtr, Addr,
 835 -- or a newtype of either.
 836 isFFILabelTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
 837
 838 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
 839         -- Look through newtypes
 840         -- Non-recursive ones are transparent to splitTyConApp,
 841         -- but recursive ones aren't; hence the splitNewType_maybe
 842 checkRepTyCon check_tc ty
 843   | Just ty'    <- splitNewType_maybe ty  = checkRepTyCon check_tc ty'
 844   | Just (tc,_) <- splitTyConApp_maybe ty = check_tc tc
 845   | otherwise                             = False
 846 \end{code}
 847
 848 ----------------------------------------------
 849 These chaps do the work; they are not exported
 850 ----------------------------------------------
 851
 852 \begin{code}
 853 legalFEArgTyCon :: TyCon -> Bool
 854 -- It's illegal to return foreign objects and (mutable)
 855 -- bytearrays from a _ccall_ / foreign declaration
 856 -- (or be passed them as arguments in foreign exported functions).
 857 legalFEArgTyCon tc
 858   | getUnique tc `elem` [ foreignObjTyConKey, foreignPtrTyConKey,
 859                           byteArrayTyConKey, mutableByteArrayTyConKey ]
 860   = False
 861   -- It's also illegal to make foreign exports that take unboxed
 862   -- arguments.  The RTS API currently can't invoke such things.  --SDM 7/2000
 863   | otherwise
 864   = boxedMarshalableTyCon tc
 865
 866 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
 867 legalFIResultTyCon dflags tc
 868   | getUnique tc `elem`
 869         [ foreignObjTyConKey, foreignPtrTyConKey,
 870           byteArrayTyConKey, mutableByteArrayTyConKey ]  = False
 871   | tc == unitTyCon = True
 872   | otherwise       = marshalableTyCon dflags tc
 873
 874 legalFEResultTyCon :: TyCon -> Bool
 875 legalFEResultTyCon tc
 876   | getUnique tc `elem`
 877         [ foreignObjTyConKey, foreignPtrTyConKey,
 878           byteArrayTyConKey, mutableByteArrayTyConKey ]  = False
 879   | tc == unitTyCon = True
 880   | otherwise       = boxedMarshalableTyCon tc
 881
 882 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
 883 -- Checks validity of types going from Haskell -> external world
 884 legalOutgoingTyCon dflags safety tc
 885   | playSafe safety && getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
 886   = False
 887   | otherwise
 888   = marshalableTyCon dflags tc
 889
 890 marshalableTyCon dflags tc
 891   =  (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
 892   || boxedMarshalableTyCon tc
 893
 894 boxedMarshalableTyCon tc
 895    = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
 896                          , int32TyConKey, int64TyConKey
 897                          , wordTyConKey, word8TyConKey, word16TyConKey
 898                          , word32TyConKey, word64TyConKey
 899                          , floatTyConKey, doubleTyConKey
 900                          , addrTyConKey, ptrTyConKey, funPtrTyConKey
 901                          , charTyConKey, foreignObjTyConKey
 902                          , foreignPtrTyConKey
 903                          , stablePtrTyConKey
 904                          , byteArrayTyConKey, mutableByteArrayTyConKey
 905                          , boolTyConKey
 906                          ]
 907 \end{code}
 908
 909
 910 %************************************************************************
 911 %*                                                                      *
 912 \subsection{Unification with an explicit substitution}
 913 %*                                                                      *
 914 %************************************************************************
 915
 916 Unify types with an explicit substitution and no monad.
 917 Ignore usage annotations.
 918
 919 \begin{code}
 920 type MySubst
 921    = (TyVarSet,         -- Set of template tyvars
 922       TyVarSubstEnv)    -- Not necessarily idempotent
 923
 924 unifyTysX :: TyVarSet           -- Template tyvars
 925           -> Type
 926           -> Type
 927           -> Maybe TyVarSubstEnv
 928 unifyTysX tmpl_tyvars ty1 ty2
 929   = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
 930
 931 unifyExtendTysX :: TyVarSet             -- Template tyvars
 932                 -> TyVarSubstEnv        -- Substitution to start with
 933                 -> Type
 934                 -> Type
 935                 -> Maybe TyVarSubstEnv  -- Extended substitution
 936 unifyExtendTysX tmpl_tyvars subst ty1 ty2
 937   = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
 938
 939 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
 940               -> Maybe TyVarSubstEnv
 941 unifyTyListsX tmpl_tyvars tys1 tys2
 942   = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
 943
 944
 945 uTysX :: Type
 946       -> Type
 947       -> (MySubst -> Maybe result)
 948       -> MySubst
 949       -> Maybe result
 950
 951 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
 952 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
 953
 954         -- Variables; go for uVar
 955 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
 956   | tyvar1 == tyvar2
 957   = k subst
 958 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
 959   | tyvar1 `elemVarSet` tmpls
 960   = uVarX tyvar1 ty2 k subst
 961 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
 962   | tyvar2 `elemVarSet` tmpls
 963   = uVarX tyvar2 ty1 k subst
 964
 965         -- Predicates
 966 uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
 967   | n1 == n2 = uTysX t1 t2 k subst
 968 uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
 969   | c1 == c2 = uTyListsX tys1 tys2 k subst
 970 uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
 971   | tc1 == tc2 = uTyListsX tys1 tys2 k subst
 972
 973         -- Functions; just check the two parts
 974 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
 975   = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
 976
 977         -- Type constructors must match
 978 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
 979   | (con1 == con2 && equalLength tys1 tys2)
 980   = uTyListsX tys1 tys2 k subst
 981
 982         -- Applications need a bit of care!
 983         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 984         -- NB: we've already dealt with type variables and Notes,
 985         -- so if one type is an App the other one jolly well better be too
 986 uTysX (AppTy s1 t1) ty2 k subst
 987   = case tcSplitAppTy_maybe ty2 of
 988       Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
 989       Nothing       -> Nothing    -- Fail
 990
 991 uTysX ty1 (AppTy s2 t2) k subst
 992   = case tcSplitAppTy_maybe ty1 of
 993       Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
 994       Nothing       -> Nothing    -- Fail
 995
 996         -- Not expecting for-alls in unification
 997 #ifdef DEBUG
 998 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
 999 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
1000 #endif
1001
1002         -- Anything else fails
1003 uTysX ty1 ty2 k subst = Nothing
1004
1005
1006 uTyListsX []         []         k subst = k subst
1007 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
1008 uTyListsX tys1       tys2       k subst = Nothing   -- Fail if the lists are different lengths
1009 \end{code}
1010
1011 \begin{code}
1012 -- Invariant: tv1 is a unifiable variable
1013 uVarX tv1 ty2 k subst@(tmpls, env)
1014   = case lookupSubstEnv env tv1 of
1015       Just (DoneTy ty1) ->    -- Already bound
1016                      uTysX ty1 ty2 k subst
1017
1018       Nothing        -- Not already bound
1019                |  typeKind ty2 `eqKind` tyVarKind tv1
1020                && occur_check_ok ty2
1021                ->     -- No kind mismatch nor occur check
1022                   k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
1023
1024                | otherwise -> Nothing   -- Fail if kind mis-match or occur check
1025   where
1026     occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
1027     occur_check_ok_tv tv | tv1 == tv = False
1028                          | otherwise = case lookupSubstEnv env tv of
1029                                          Nothing           -> True
1030                                          Just (DoneTy ty)  -> occur_check_ok ty
1031 \end{code}
1032
1033
1034
1035 %************************************************************************
1036 %*                                                                      *
1037 \subsection{Matching on types}
1038 %*                                                                      *
1039 %************************************************************************
1040
1041 Matching is a {\em unidirectional} process, matching a type against a
1042 template (which is just a type with type variables in it).  The
1043 matcher assumes that there are no repeated type variables in the
1044 template, so that it simply returns a mapping of type variables to
1045 types.  It also fails on nested foralls.
1046
1047 @matchTys@ matches corresponding elements of a list of templates and
1048 types.  It and @matchTy@ both ignore usage annotations, unlike the
1049 main function @match@.
1050
1051 \begin{code}
1052 matchTy :: TyVarSet                     -- Template tyvars
1053         -> Type                         -- Template
1054         -> Type                         -- Proposed instance of template
1055         -> Maybe TyVarSubstEnv          -- Matching substitution
1056
1057
1058 matchTys :: TyVarSet                    -- Template tyvars
1059          -> [Type]                      -- Templates
1060          -> [Type]                      -- Proposed instance of template
1061          -> Maybe (TyVarSubstEnv,               -- Matching substitution
1062                    [Type])              -- Left over instance types
1063
1064 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
1065
1066 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
1067                                       (\ (senv,tys) -> Just (senv,tys))
1068                                       emptySubstEnv
1069 \end{code}
1070
1071 @match@ is the main function.  It takes a flag indicating whether
1072 usage annotations are to be respected.
1073
1074 \begin{code}
1075 match :: Type -> Type                           -- Current match pair
1076       -> TyVarSet                               -- Template vars
1077       -> (TyVarSubstEnv -> Maybe result)        -- Continuation
1078       -> TyVarSubstEnv                          -- Current subst
1079       -> Maybe result
1080
1081 -- When matching against a type variable, see if the variable
1082 -- has already been bound.  If so, check that what it's bound to
1083 -- is the same as ty; if not, bind it and carry on.
1084
1085 match (TyVarTy v) ty tmpls k senv
1086   | v `elemVarSet` tmpls
1087   =     -- v is a template variable
1088     case lookupSubstEnv senv v of
1089         Nothing | typeKind ty `eqKind` tyVarKind v
1090                         -- We do a kind check, just as in the uVarX above
1091                         -- The kind check is needed to avoid bogus matches
1092                         -- of   (a b) with (c d), where the kinds don't match
1093                         -- An occur check isn't needed when matching.
1094                 -> k (extendSubstEnv senv v (DoneTy ty))
1095
1096                 | otherwise  -> Nothing -- Fails
1097
1098         Just (DoneTy ty')  | ty' `tcEqType` ty   -> k senv   -- Succeeds
1099                            | otherwise           -> Nothing  -- Fails
1100
1101   | otherwise
1102   =     -- v is not a template variable; ty had better match
1103         -- Can't use (==) because types differ
1104     case tcGetTyVar_maybe ty of
1105         Just v' | v == v' -> k senv    -- Success
1106         other             -> Nothing   -- Failure
1107     -- This tcGetTyVar_maybe is *required* because it must strip Notes.
1108     -- I guess the reason the Note-stripping case is *last* rather than first
1109     -- is to preserve type synonyms etc., so I'm not moving it to the
1110     -- top; but this means that (without the deNotetype) a type
1111     -- variable may not match the pattern (TyVarTy v') as one would
1112     -- expect, due to an intervening Note.  KSW 2000-06.
1113
1114         -- Predicates
1115 match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
1116   | n1 == n2 = match t1 t2 tmpls k senv
1117 match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
1118   | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
1119 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1120   | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1121
1122         -- Functions; just check the two parts
1123 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1124   = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1125
1126 match (AppTy fun1 arg1) ty2 tmpls k senv
1127   = case tcSplitAppTy_maybe ty2 of
1128         Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1129         Nothing          -> Nothing     -- Fail
1130
1131 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1132   | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1133
1134 -- Newtypes are opaque; other source types should not happen
1135 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1136   | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1137
1138         -- With type synonyms, we have to be careful for the exact
1139         -- same reasons as in the unifier.  Please see the
1140         -- considerable commentary there before changing anything
1141         -- here! (WDP 95/05)
1142 match (NoteTy n1 ty1) ty2      tmpls k senv = match ty1 ty2 tmpls k senv
1143 match ty1      (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1144
1145 -- Catch-all fails
1146 match _ _ _ _ _ = Nothing
1147
1148 match_list_exactly tys1 tys2 tmpls k senv
1149   = match_list tys1 tys2 tmpls k' senv
1150   where
1151     k' (senv', tys2') | null tys2' = k senv'    -- Succeed
1152                       | otherwise  = Nothing    -- Fail
1153
1154 match_list []         tys2       tmpls k senv = k (senv, tys2)
1155 match_list (ty1:tys1) []         tmpls k senv = Nothing -- Not enough arg tys => failure
1156 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1157   = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv
1158 \end{code}