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