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